diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp new file mode 100644 index 000000000..b083bf686 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp @@ -0,0 +1,45 @@ +class petagons_tests { + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + non_strict_abstraction(b, x, y) { + if(b) { + x = 0; y = 3; + } else { + x = -2; y = 1; + } + } + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + strict_abstraction(b, x, y) { + if(b) { + x = 0; y = 3; + } else { + x = -2; y = 0; + } + } + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + common_code_pattern_01(x, y, r) { + if(x >= 0 && y >= 0) + if (x > y) { + r = x - y; + assert r >= 0; + } + } + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + common_code_pattern_02(x, len) { + if(len >= 0) { + def r = x % len; + assert r < len; + } + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json new file mode 100644 index 000000000..785518ce3 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json @@ -0,0 +1,38 @@ +{ + "warnings" : [ ], + "files" : [ "report.json", "untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json", "untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], + "info" : { + "cfgs" : "4", + "duration" : "418ms", + "end" : "2024-01-10T15:05:51.619+01:00", + "expressions" : "40", + "files" : "4", + "globals" : "0", + "members" : "4", + "programs" : "1", + "start" : "2024-01-10T15:05:51.201+01:00", + "statements" : "21", + "units" : "1", + "version" : "0.1b8", + "warnings" : "0" + }, + "configuration" : { + "analysisGraphs" : "NONE", + "descendingPhaseType" : "NONE", + "dumpForcesUnwinding" : "false", + "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "glbThreshold" : "5", + "hotspots" : "unset", + "jsonOutput" : "true", + "openCallPolicy" : "WorstCasePolicy", + "optimize" : "false", + "recursionWideningThreshold" : "5", + "semanticChecks" : "", + "serializeInputs" : "false", + "serializeResults" : "true", + "syntacticChecks" : "", + "useWideningPoints" : "true", + "wideningThreshold" : "5", + "workdir" : "test-outputs/numeric/pentagons" + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json new file mode 100644 index 000000000..f1c92d216 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::common_code_pattern_01(petagons_tests* this, untyped x, untyped y, untyped r)","description":null,"nodes":[{"id":0,"subNodes":[1,4],"text":"&&(>=(x, 0), >=(y, 0))"},{"id":1,"subNodes":[2,3],"text":">=(x, 0)"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":">=(y, 0)"},{"id":5,"text":"y"},{"id":6,"text":"0"},{"id":7,"subNodes":[8,9],"text":">(x, y)"},{"id":8,"text":"x"},{"id":9,"text":"y"},{"id":10,"subNodes":[11,12],"text":"r = -(x, y)"},{"id":11,"text":"r"},{"id":12,"subNodes":[13,14],"text":"-(x, y)"},{"id":13,"text":"x"},{"id":14,"text":"y"},{"id":15,"subNodes":[16],"text":"assert >=(r, 0)"},{"id":16,"subNodes":[17,18],"text":">=(r, 0)"},{"id":17,"text":"r"},{"id":18,"text":"0"},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":7,"kind":"TrueEdge"},{"sourceId":0,"destId":19,"kind":"FalseEdge"},{"sourceId":7,"destId":10,"kind":"TrueEdge"},{"sourceId":7,"destId":19,"kind":"FalseEdge"},{"sourceId":10,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x >= 0 && y >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x > y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":11,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":12,"description":{"expressions":["x - y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":13,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":14,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":15,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":16,"description":{"expressions":["r >= 0"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":17,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":18,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json new file mode 100644 index 000000000..a04b8a587 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::common_code_pattern_02(petagons_tests* this, untyped x, untyped len)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":">=(len, 0)"},{"id":1,"text":"len"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"r = %(x, len)"},{"id":4,"text":"r"},{"id":5,"subNodes":[6,7],"text":"%(x, len)"},{"id":6,"text":"x"},{"id":7,"text":"len"},{"id":8,"subNodes":[9],"text":"assert <(r, len)"},{"id":9,"subNodes":[10,11],"text":"<(r, len)"},{"id":10,"text":"r"},{"id":11,"text":"len"},{"id":12,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"TrueEdge"},{"sourceId":0,"destId":12,"kind":"FalseEdge"},{"sourceId":3,"destId":8,"kind":"SequentialEdge"},{"sourceId":8,"destId":12,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["len >= 0"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":5,"description":{"expressions":["x % len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["r < len"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":11,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json new file mode 100644 index 000000000..b7cb9b550 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::non_strict_abstraction(petagons_tests* this, untyped b, untyped x, untyped y)","description":null,"nodes":[{"id":0,"text":"b"},{"id":1,"subNodes":[2,3],"text":"x = 0"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":"y = 3"},{"id":5,"text":"y"},{"id":6,"text":"3"},{"id":7,"subNodes":[8,9],"text":"x = -2"},{"id":8,"text":"x"},{"id":9,"text":"-2"},{"id":10,"subNodes":[11,12],"text":"y = 1"},{"id":11,"text":"y"},{"id":12,"text":"1"},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":1,"kind":"TrueEdge"},{"sourceId":0,"destId":7,"kind":"FalseEdge"},{"sourceId":1,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":13,"kind":"SequentialEdge"},{"sourceId":7,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], (y)","y":"[3, 3], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["3"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["-2"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], (y)","y":"[1, 1], {}"}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, 0], (y)","y":"[1, 3], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json new file mode 100644 index 000000000..35d01401f --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::strict_abstraction(petagons_tests* this, untyped b, untyped x, untyped y)","description":null,"nodes":[{"id":0,"text":"b"},{"id":1,"subNodes":[2,3],"text":"x = 0"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":"y = 3"},{"id":5,"text":"y"},{"id":6,"text":"3"},{"id":7,"subNodes":[8,9],"text":"x = -2"},{"id":8,"text":"x"},{"id":9,"text":"-2"},{"id":10,"subNodes":[11,12],"text":"y = 0"},{"id":11,"text":"y"},{"id":12,"text":"0"},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":1,"kind":"TrueEdge"},{"sourceId":0,"destId":7,"kind":"FalseEdge"},{"sourceId":1,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":13,"kind":"SequentialEdge"},{"sourceId":7,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], (y)","y":"[3, 3], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["3"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["-2"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], (y)","y":"[0, 0], {}"}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, 0], (y)","y":"[0, 3], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java new file mode 100644 index 000000000..aa0bea437 --- /dev/null +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java @@ -0,0 +1,330 @@ +package it.unive.lisa.analysis.numeric; + +import it.unive.lisa.analysis.BaseLattice; +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.analysis.value.ValueDomain; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.BinaryExpression; +import it.unive.lisa.symbolic.value.Constant; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.RemainderOperator; +import it.unive.lisa.symbolic.value.operator.SubtractionOperator; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; +import it.unive.lisa.util.numeric.MathNumber; +import it.unive.lisa.util.representation.MapRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; +import org.apache.commons.collections4.CollectionUtils; + +/** + * /** The pentagons abstract domain, a weakly relational numeric abstract + * domain. This abstract domain captures properties of the form of x \in [a, b] + * ∧ x < y. It is more precise than the well known interval domain, but + * it is less precise than the octagon domain. It is implemented as a + * {@link ValueDomain}. + * + * @author Luca Negrini + * @author Vincenzo Arceri + * + * @see Pentagons: + * A weakly relational abstract domain for the efficient validation of + * array accesses + */ +public class Pentagon implements ValueDomain, BaseLattice { + + /** + * The interval environment. + */ + private final ValueEnvironment intervals; + + /** + * The upper bounds environment. + */ + private final ValueEnvironment upperBounds; + + /** + * Builds the pentagons. + */ + public Pentagon() { + this.intervals = new ValueEnvironment<>(new Interval()).top(); + this.upperBounds = new ValueEnvironment<>(new UpperBounds(true)).top(); + } + + /** + * Builds the pentagons. + * + * @param intervals the interval environment + * @param upperBounds the upper bounds environment + */ + public Pentagon( + ValueEnvironment intervals, + ValueEnvironment upperBounds) { + this.intervals = intervals; + this.upperBounds = upperBounds; + } + + @Override + public Pentagon assign( + Identifier id, + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + ValueEnvironment newBounds = upperBounds.assign(id, expression, pp, oracle); + ValueEnvironment newIntervals = intervals.assign(id, expression, pp, oracle); + + // we add the semantics for assignments here as we have access to the + // whole assignment + if (expression instanceof BinaryExpression) { + BinaryExpression be = (BinaryExpression) expression; + BinaryOperator op = be.getOperator(); + if (op instanceof SubtractionOperator) { + if (be.getLeft() instanceof Identifier) { + Identifier x = (Identifier) be.getLeft(); + + if (be.getRight() instanceof Constant) + // r = x - c + newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); + else if (be.getRight() instanceof Identifier) { + // r = x - y + Identifier y = (Identifier) be.getRight(); + + if (newBounds.getState(y).contains(x)) + newIntervals = newIntervals.putState(id, newIntervals.getState(id) + .glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); + } + } + } else if (op instanceof RemainderOperator && be.getRight() instanceof Identifier) { + // r = u % d + Identifier d = (Identifier) be.getRight(); + MathNumber low = intervals.getState(d).interval.getLow(); + if (low.isPositive() || low.isZero()) + newBounds = newBounds.putState(id, new UpperBounds(Collections.singleton(d))); + else + newBounds = newBounds.putState(id, new UpperBounds().top()); + } + } + + return new Pentagon( + newIntervals, + newBounds).closure(); + } + + @Override + public Pentagon smallStepSemantics( + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new Pentagon( + intervals.smallStepSemantics(expression, pp, oracle), + upperBounds.smallStepSemantics(expression, pp, oracle)); + } + + @Override + public Pentagon assume( + ValueExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + return new Pentagon( + intervals.assume(expression, src, dest, oracle), + upperBounds.assume(expression, src, dest, oracle)); + } + + @Override + public Pentagon forgetIdentifier( + Identifier id) + throws SemanticException { + return new Pentagon( + intervals.forgetIdentifier(id), + upperBounds.forgetIdentifier(id)); + } + + @Override + public Pentagon forgetIdentifiersIf( + Predicate test) + throws SemanticException { + return new Pentagon( + intervals.forgetIdentifiersIf(test), + upperBounds.forgetIdentifiersIf(test)); + } + + @Override + public Satisfiability satisfies( + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return intervals.satisfies(expression, pp, oracle).glb(upperBounds.satisfies(expression, pp, oracle)); + } + + @Override + public Pentagon pushScope( + ScopeToken token) + throws SemanticException { + return new Pentagon(intervals.pushScope(token), upperBounds.pushScope(token)); + } + + @Override + public Pentagon popScope( + ScopeToken token) + throws SemanticException { + return new Pentagon(intervals.popScope(token), upperBounds.popScope(token)); + } + + @Override + public StructuredRepresentation representation() { + if (isTop()) + return Lattice.topRepresentation(); + if (isBottom()) + return Lattice.bottomRepresentation(); + Map mapping = new HashMap<>(); + for (Identifier id : CollectionUtils.union(intervals.getKeys(), upperBounds.getKeys())) + mapping.put(new StringRepresentation(id), + new StringRepresentation(intervals.getState(id).toString() + ", " + + upperBounds.getState(id).representation())); + return new MapRepresentation(mapping); + } + + @Override + public Pentagon top() { + return new Pentagon(intervals.top(), upperBounds.top()); + } + + @Override + public boolean isTop() { + return intervals.isTop() && upperBounds.isTop(); + } + + @Override + public Pentagon bottom() { + return new Pentagon(intervals.bottom(), upperBounds.bottom()); + } + + @Override + public boolean isBottom() { + return intervals.isBottom() && upperBounds.isBottom(); + } + + private Pentagon closure() throws SemanticException { + ValueEnvironment< + UpperBounds> newBounds = new ValueEnvironment(upperBounds.lattice, upperBounds.getMap()); + + for (Identifier id1 : intervals.getKeys()) { + Set closure = new HashSet<>(); + for (Identifier id2 : intervals.getKeys()) + if (!id1.equals(id2)) + if (intervals.getState(id1).interval.getHigh() + .compareTo(intervals.getState(id2).interval.getLow()) < 0) + closure.add(id2); + if (!closure.isEmpty()) + // glb is the union + newBounds = newBounds.putState(id1, + newBounds.getState(id1).glb(new UpperBounds(closure))); + + } + + return new Pentagon(intervals, newBounds); + } + + @Override + public Pentagon lubAux( + Pentagon other) + throws SemanticException { + ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); + for (Entry entry : upperBounds) { + Set closure = new HashSet<>(); + for (Identifier bound : entry.getValue()) + if (other.intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(other.intervals.getState(bound).interval.getLow()) < 0) + closure.add(bound); + if (!closure.isEmpty()) + // glb is the union + newBounds = newBounds.putState(entry.getKey(), + newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); + } + + for (Entry entry : other.upperBounds) { + Set closure = new HashSet<>(); + for (Identifier bound : entry.getValue()) + if (intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(intervals.getState(bound).interval.getLow()) < 0) + closure.add(bound); + if (!closure.isEmpty()) + // glb is the union + newBounds = newBounds.putState(entry.getKey(), + newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); + } + + return new Pentagon(intervals.lub(other.intervals), newBounds); + } + + @Override + public Pentagon wideningAux( + Pentagon other) + throws SemanticException { + return new Pentagon(intervals.widening(other.intervals), upperBounds.widening(other.upperBounds)); + } + + @Override + public boolean lessOrEqualAux( + Pentagon other) + throws SemanticException { + if (!intervals.lessOrEqual(other.intervals)) + return false; + for (Entry entry : other.upperBounds) + for (Identifier bound : entry.getValue()) + if (!(upperBounds.getState(entry.getKey()).contains(bound) + || intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(intervals.getState(bound).interval.getLow()) < 0)) + return false; + + return true; + } + + @Override + public int hashCode() { + return Objects.hash(intervals, upperBounds); + } + + @Override + public boolean equals( + Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Pentagon other = (Pentagon) obj; + return Objects.equals(intervals, other.intervals) && Objects.equals(upperBounds, other.upperBounds); + } + + @Override + public String toString() { + return representation().toString(); + } + + @Override + public boolean knowsIdentifier( + Identifier id) { + return intervals.knowsIdentifier(id) || upperBounds.knowsIdentifier(id); + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java new file mode 100644 index 000000000..89d05308a --- /dev/null +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java @@ -0,0 +1,249 @@ +package it.unive.lisa.analysis.numeric; + +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonGe; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonGt; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonLe; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonLt; +import it.unive.lisa.util.representation.SetRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Objects; +import java.util.Set; +import java.util.TreeSet; + +/** + * The upper bounds abstract domain. It is implemented as a + * {@link BaseNonRelationalValueDomain}. + * + * @author Luca Negrini + * @author Vincenzo Arceri + */ +public class UpperBounds implements BaseNonRelationalValueDomain, Iterable { + + /** + * The abstract top element. + */ + private static final UpperBounds TOP = new UpperBounds(true); + + /** + * The abstract bottom element. + */ + private static final UpperBounds BOTTOM = new UpperBounds(new TreeSet<>()); + + /** + * The flag to set abstract top state. + */ + private final boolean isTop; + + /** + * The set containing the bounds. + */ + private final Set bounds; + + /** + * Builds the upper bounds. + */ + public UpperBounds() { + this(true); + } + + /** + * Builds the upper bounds. + * + * @param isTop {@code true} if the abstract domain is top; otherwise + * {@code false}. + */ + public UpperBounds( + boolean isTop) { + this.bounds = null; + this.isTop = isTop; + } + + /** + * Builds the upper bounds. + * + * @param bounds the bounds to set + */ + public UpperBounds( + Set bounds) { + this.bounds = bounds; + this.isTop = false; + } + + @Override + public StructuredRepresentation representation() { + if (isTop()) + return new StringRepresentation("{}"); + if (isBottom()) + return Lattice.bottomRepresentation(); + return new SetRepresentation(bounds, StringRepresentation::new); + } + + @Override + public UpperBounds top() { + return TOP; + } + + @Override + public UpperBounds bottom() { + return BOTTOM; + } + + @Override + public boolean isBottom() { + return !isTop && bounds.isEmpty(); + } + + @Override + public UpperBounds lubAux( + UpperBounds other) + throws SemanticException { + Set lub = new HashSet<>(bounds); + lub.retainAll(other.bounds); + return new UpperBounds(lub); + } + + @Override + public UpperBounds glbAux( + UpperBounds other) + throws SemanticException { + Set lub = new HashSet<>(bounds); + lub.addAll(other.bounds); + return new UpperBounds(lub); + } + + @Override + public boolean lessOrEqualAux( + UpperBounds other) + throws SemanticException { + return bounds.containsAll(other.bounds); + } + + @Override + public UpperBounds wideningAux( + UpperBounds other) + throws SemanticException { + return other.bounds.containsAll(bounds) ? other : TOP; + } + + @Override + public boolean equals( + Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + UpperBounds other = (UpperBounds) obj; + return Objects.equals(bounds, other.bounds) && isTop == other.isTop; + } + + @Override + public int hashCode() { + return Objects.hash(bounds, isTop); + } + + @Override + public ValueEnvironment assumeBinaryExpression( + ValueEnvironment environment, + BinaryOperator operator, + ValueExpression left, + ValueExpression right, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + if (!(left instanceof Identifier && right instanceof Identifier)) + return environment; + + Identifier x = (Identifier) left; + Identifier y = (Identifier) right; + + // glb is the union! + + if (operator instanceof ComparisonEq) { + // x == y + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(x, set).putState(y, set); + } + + if (operator instanceof ComparisonLt) { + // x < y + UpperBounds set = environment.getState(x).glb(environment.getState(y)) + .glb(new UpperBounds(Collections.singleton(y))); + return environment.putState(x, set); + } + + if (operator instanceof ComparisonLe) { + // x <= y + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(x, set); + } + + if (operator instanceof ComparisonGt) { + // x > y ---> y < x + UpperBounds set = environment.getState(x).glb(environment.getState(y)) + .glb(new UpperBounds(Collections.singleton(x))); + return environment.putState(y, set); + } + + if (operator instanceof ComparisonGe) { + // x >= y --- > y <= x + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(y, set); + } + + return environment; + } + + @Override + public Iterator iterator() { + if (bounds == null) + return Collections.emptyIterator(); + return bounds.iterator(); + } + + /** + * Checks if this bounds contains a specified identifier of a program + * variable. + * + * @param id the identifier to check + * + * @return {@code true} if this bounds contains the specified identifier; + * otherwise, {@code false}. + */ + public boolean contains( + Identifier id) { + return bounds != null && bounds.contains(id); + } + + /** + * Adds the specified identifier of a program variable in the bounds. + * + * @param id the identifier to add in the bounds. + * + * @return the updated bounds. + */ + public UpperBounds add( + Identifier id) { + Set res = new HashSet<>(); + if (!isTop() && !isBottom()) + res.addAll(bounds); + res.add(id); + return new UpperBounds(res); + } +} diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java index 014d4dc97..4c4628c33 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java @@ -8,6 +8,7 @@ import it.unive.lisa.analysis.numeric.IntegerConstantPropagation; import it.unive.lisa.analysis.numeric.Interval; import it.unive.lisa.analysis.numeric.Parity; +import it.unive.lisa.analysis.numeric.Pentagon; import it.unive.lisa.analysis.numeric.Sign; import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; import org.junit.Test; @@ -90,4 +91,18 @@ public void testNonRedundantSetOfInterval() { conf.compareWithOptimization = false; perform(conf); } + + @Test + public void testPentagons() { + CronConfiguration conf = new CronConfiguration(); + conf.serializeResults = true; + conf.abstractState = DefaultConfiguration.simpleState( + DefaultConfiguration.defaultHeapDomain(), + new Pentagon(), + DefaultConfiguration.defaultTypeDomain()); + conf.testDir = "numeric"; + conf.testSubDir = "pentagons"; + conf.programFile = "pentagons.imp"; + perform(conf); + } }