diff --git a/lisa/lisa-analyses/imp-testcases/liveness/liveness.imp b/lisa/lisa-analyses/imp-testcases/liveness/liveness.imp new file mode 100644 index 000000000..5e5da15a3 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/liveness.imp @@ -0,0 +1,53 @@ +class ae { + + f0(a, b) { + def x = a + b; + def y = a * b; + def z = x * y; + def d = y + 7; + def w = x + y; + + return; + } + + f1(a, b) { + def x = a + b; + def y = a * b; + + while (y > a) { + a = a + 1; + x = a + b; + } + + return x; + } + + f2(c) { + def a = 0; + + while (a < 10) { + def b = a + 1; + c = c + b; + a = b * 2; + } + + return c; + } + + + f3() { + def x = 2; + def y = 4; + x = 1; + def z = 0; + + if (y > 0) { + z = x; + } else { + z = y * y; + } + + x = z; + return x; + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/liveness/report.json b/lisa/lisa-analyses/imp-testcases/liveness/report.json new file mode 100644 index 000000000..79365e4ef --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/report.json @@ -0,0 +1,38 @@ +{ + "warnings" : [ ], + "files" : [ "report.json", "untyped_ae.f0(ae__this,_untyped_a,_untyped_b).json", "untyped_ae.f1(ae__this,_untyped_a,_untyped_b).json", "untyped_ae.f2(ae__this,_untyped_c).json", "untyped_ae.f3(ae__this).json" ], + "info" : { + "cfgs" : "4", + "duration" : "445ms", + "end" : "2023-10-06T17:11:36.375+02:00", + "expressions" : "75", + "files" : "4", + "globals" : "0", + "members" : "4", + "programs" : "1", + "start" : "2023-10-06T17:11:35.930+02:00", + "statements" : "27", + "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/liveness" + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f0(ae__this,_untyped_a,_untyped_b).json b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f0(ae__this,_untyped_a,_untyped_b).json new file mode 100644 index 000000000..d2a40c0b3 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f0(ae__this,_untyped_a,_untyped_b).json @@ -0,0 +1 @@ +{"name":"untyped ae::f0(ae* this, untyped a, untyped b)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = +(a, b)"},{"id":1,"text":"x"},{"id":2,"subNodes":[3,4],"text":"+(a, b)"},{"id":3,"text":"a"},{"id":4,"text":"b"},{"id":5,"subNodes":[6,7],"text":"y = *(a, b)"},{"id":6,"text":"y"},{"id":7,"subNodes":[8,9],"text":"*(a, b)"},{"id":8,"text":"a"},{"id":9,"text":"b"},{"id":10,"subNodes":[11,12],"text":"z = *(x, y)"},{"id":11,"text":"z"},{"id":12,"subNodes":[13,14],"text":"*(x, y)"},{"id":13,"text":"x"},{"id":14,"text":"y"},{"id":15,"subNodes":[16,17],"text":"d = +(y, 7)"},{"id":16,"text":"d"},{"id":17,"subNodes":[18,19],"text":"+(y, 7)"},{"id":18,"text":"y"},{"id":19,"text":"7"},{"id":20,"subNodes":[21,22],"text":"w = +(x, y)"},{"id":21,"text":"w"},{"id":22,"subNodes":[23,24],"text":"+(x, y)"},{"id":23,"text":"x"},{"id":24,"text":"y"},{"id":25,"text":"ret"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":20,"kind":"SequentialEdge"},{"sourceId":20,"destId":25,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"x":["float32","int32","string"]},"value":["a","b"]}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x"]}}},{"nodeId":2,"description":{"expressions":["a + b","a strcat b"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x"]}}},{"nodeId":3,"description":{"expressions":["a"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x"]}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x"]}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"y":["float32","int32"]},"value":["a","b","x"]}}},{"nodeId":6,"description":{"expressions":["y"],"state":{"heap":"monolith","type":"#TOP#","value":["x","y"]}}},{"nodeId":7,"description":{"expressions":["a * b"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x","y"]}}},{"nodeId":8,"description":{"expressions":["a"],"state":{"heap":"monolith","type":"#TOP#","value":["a","b","x","y"]}}},{"nodeId":9,"description":{"expressions":["b"],"state":{"heap":"monolith","type":"#TOP#","value":["b","x","y"]}}},{"nodeId":10,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"z":["float32","int32"]},"value":["x","y"]}}},{"nodeId":11,"description":{"expressions":["z"],"state":{"heap":"monolith","type":"#TOP#","value":["x","y","z"]}}},{"nodeId":12,"description":{"expressions":["x * y"],"state":{"heap":"monolith","type":"#TOP#","value":["x","y","z"]}}},{"nodeId":13,"description":{"expressions":["x"],"state":{"heap":"monolith","type":"#TOP#","value":["x","y","z"]}}},{"nodeId":14,"description":{"expressions":["y"],"state":{"heap":"monolith","type":"#TOP#","value":["x","y","z"]}}},{"nodeId":15,"description":{"expressions":["d"],"state":{"heap":"monolith","type":{"d":["float32","int32"]},"value":["x","y"]}}},{"nodeId":16,"description":{"expressions":["d"],"state":{"heap":"monolith","type":"#TOP#","value":["d","x","y"]}}},{"nodeId":17,"description":{"expressions":["y + 7"],"state":{"heap":"monolith","type":"#TOP#","value":["d","x","y"]}}},{"nodeId":18,"description":{"expressions":["y"],"state":{"heap":"monolith","type":"#TOP#","value":["d","x","y"]}}},{"nodeId":19,"description":{"expressions":["7"],"state":{"heap":"monolith","type":"#TOP#","value":["d","x","y"]}}},{"nodeId":20,"description":{"expressions":["w"],"state":{"heap":"monolith","type":{"w":["float32","int32","string"]},"value":["x","y"]}}},{"nodeId":21,"description":{"expressions":["w"],"state":{"heap":"monolith","type":"#TOP#","value":["w"]}}},{"nodeId":22,"description":{"expressions":["x + y","x strcat y"],"state":{"heap":"monolith","type":"#TOP#","value":["w","x","y"]}}},{"nodeId":23,"description":{"expressions":["x"],"state":{"heap":"monolith","type":"#TOP#","value":["w","x","y"]}}},{"nodeId":24,"description":{"expressions":["y"],"state":{"heap":"monolith","type":"#TOP#","value":["w","y"]}}},{"nodeId":25,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":"#TOP#","value":[]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f1(ae__this,_untyped_a,_untyped_b).json b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f1(ae__this,_untyped_a,_untyped_b).json new file mode 100644 index 000000000..23b1be3e2 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f1(ae__this,_untyped_a,_untyped_b).json @@ -0,0 +1 @@ +{"name":"untyped ae::f1(ae* this, untyped a, untyped b)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = +(a, b)"},{"id":1,"text":"x"},{"id":2,"subNodes":[3,4],"text":"+(a, b)"},{"id":3,"text":"a"},{"id":4,"text":"b"},{"id":5,"subNodes":[6,7],"text":"y = *(a, b)"},{"id":6,"text":"y"},{"id":7,"subNodes":[8,9],"text":"*(a, b)"},{"id":8,"text":"a"},{"id":9,"text":"b"},{"id":10,"subNodes":[11,12],"text":">(y, a)"},{"id":11,"text":"y"},{"id":12,"text":"a"},{"id":13,"subNodes":[14,15],"text":"a = +(a, 1)"},{"id":14,"text":"a"},{"id":15,"subNodes":[16,17],"text":"+(a, 1)"},{"id":16,"text":"a"},{"id":17,"text":"1"},{"id":18,"subNodes":[19,20],"text":"x = +(a, b)"},{"id":19,"text":"x"},{"id":20,"subNodes":[21,22],"text":"+(a, b)"},{"id":21,"text":"a"},{"id":22,"text":"b"},{"id":23,"subNodes":[24],"text":"return x"},{"id":24,"text":"x"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"TrueEdge"},{"sourceId":10,"destId":23,"kind":"FalseEdge"},{"sourceId":13,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":10,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b"]}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#"},"value":["a","b","x"]}}},{"nodeId":2,"description":{"expressions":["a + b","a strcat b"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#"},"value":["a","b","x"]}}},{"nodeId":3,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#"},"value":["a","b","x"]}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#"},"value":["a","b","x"]}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"],"y":["float32","int32"]},"value":["a","b","x"]}}},{"nodeId":6,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":7,"description":{"expressions":["a * b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":8,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":9,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":10,"description":{"expressions":["y > a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":12,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":13,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":14,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":15,"description":{"expressions":["a + 1"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":16,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":17,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":18,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","y"]}}},{"nodeId":19,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":20,"description":{"expressions":["a + b","a strcat b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":21,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":22,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f1":"#TOP#","x":["float32","int32","string"]},"value":["a","b","x","y"]}}},{"nodeId":23,"description":{"expressions":["ret_value@f1"],"state":{"heap":"monolith","type":{"ret_value@f1":"#TOP#"},"value":["x"]}}},{"nodeId":24,"description":{"expressions":["x"],"state":{"heap":"monolith","type":"#TOP#","value":["x"]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f2(ae__this,_untyped_c).json b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f2(ae__this,_untyped_c).json new file mode 100644 index 000000000..6b186e2e9 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f2(ae__this,_untyped_c).json @@ -0,0 +1 @@ +{"name":"untyped ae::f2(ae* this, untyped c)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = 0"},{"id":1,"text":"a"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"<(a, 10)"},{"id":4,"text":"a"},{"id":5,"text":"10"},{"id":6,"subNodes":[7,8],"text":"b = +(a, 1)"},{"id":7,"text":"b"},{"id":8,"subNodes":[9,10],"text":"+(a, 1)"},{"id":9,"text":"a"},{"id":10,"text":"1"},{"id":11,"subNodes":[12,13],"text":"c = +(c, b)"},{"id":12,"text":"c"},{"id":13,"subNodes":[14,15],"text":"+(c, b)"},{"id":14,"text":"c"},{"id":15,"text":"b"},{"id":16,"subNodes":[17,18],"text":"a = *(b, 2)"},{"id":17,"text":"a"},{"id":18,"subNodes":[19,20],"text":"*(b, 2)"},{"id":19,"text":"b"},{"id":20,"text":"2"},{"id":21,"subNodes":[22],"text":"return c"},{"id":22,"text":"c"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"TrueEdge"},{"sourceId":3,"destId":21,"kind":"FalseEdge"},{"sourceId":6,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["int32"],"ret_value@f2":"#TOP#"},"value":["c"]}}},{"nodeId":1,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":3,"description":{"expressions":["a < 10"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":4,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":5,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":6,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"b":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":7,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":8,"description":{"expressions":["a + 1"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","b","c"]}}},{"nodeId":9,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["a","b","c"]}}},{"nodeId":10,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":11,"description":{"expressions":["c"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"c":["float32","int32","string"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":12,"description":{"expressions":["c"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":13,"description":{"expressions":["c + b","c strcat b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":14,"description":{"expressions":["c"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":15,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":16,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["float32","int32"],"ret_value@f2":"#TOP#"},"value":["b","c"]}}},{"nodeId":17,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":18,"description":{"expressions":["b * 2"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","b","c"]}}},{"nodeId":19,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","b","c"]}}},{"nodeId":20,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["a","c"]}}},{"nodeId":21,"description":{"expressions":["ret_value@f2"],"state":{"heap":"monolith","type":{"ret_value@f2":"#TOP#"},"value":["c"]}}},{"nodeId":22,"description":{"expressions":["c"],"state":{"heap":"monolith","type":"#TOP#","value":["c"]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f3(ae__this).json b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f3(ae__this).json new file mode 100644 index 000000000..eb457b249 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/liveness/untyped_ae.f3(ae__this).json @@ -0,0 +1 @@ +{"name":"untyped ae::f3(ae* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 2"},{"id":1,"text":"x"},{"id":2,"text":"2"},{"id":3,"subNodes":[4,5],"text":"y = 4"},{"id":4,"text":"y"},{"id":5,"text":"4"},{"id":6,"subNodes":[7,8],"text":"x = 1"},{"id":7,"text":"x"},{"id":8,"text":"1"},{"id":9,"subNodes":[10,11],"text":"z = 0"},{"id":10,"text":"z"},{"id":11,"text":"0"},{"id":12,"subNodes":[13,14],"text":">(y, 0)"},{"id":13,"text":"y"},{"id":14,"text":"0"},{"id":15,"subNodes":[16,17],"text":"z = x"},{"id":16,"text":"z"},{"id":17,"text":"x"},{"id":18,"subNodes":[19,20],"text":"z = *(y, y)"},{"id":19,"text":"z"},{"id":20,"subNodes":[21,22],"text":"*(y, y)"},{"id":21,"text":"y"},{"id":22,"text":"y"},{"id":23,"subNodes":[24,25],"text":"x = z"},{"id":24,"text":"x"},{"id":25,"text":"z"},{"id":26,"subNodes":[27],"text":"return x"},{"id":27,"text":"x"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":15,"kind":"TrueEdge"},{"sourceId":12,"destId":18,"kind":"FalseEdge"},{"sourceId":15,"destId":23,"kind":"SequentialEdge"},{"sourceId":18,"destId":23,"kind":"SequentialEdge"},{"sourceId":23,"destId":26,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":[]}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":["x"]}}},{"nodeId":2,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":["x"]}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"],"y":["int32"]},"value":[]}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":["y"]}}},{"nodeId":5,"description":{"expressions":["4"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":["y"]}}},{"nodeId":6,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":["int32"]},"value":["y"]}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["x","y"]}}},{"nodeId":8,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["x","y"]}}},{"nodeId":9,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":["int32"]},"value":["x","y"]}}},{"nodeId":10,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x","y","z"]}}},{"nodeId":11,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x","y","z"]}}},{"nodeId":12,"description":{"expressions":["y > 0"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x","y"]}}},{"nodeId":13,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x","y"]}}},{"nodeId":14,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x","y"]}}},{"nodeId":15,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":"#TOP#"},"value":["x"]}}},{"nodeId":16,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["z"]}}},{"nodeId":17,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["x","z"]}}},{"nodeId":18,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#","z":["float32","int32"]},"value":["y"]}}},{"nodeId":19,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["z"]}}},{"nodeId":20,"description":{"expressions":["y * y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["y","z"]}}},{"nodeId":21,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["y","z"]}}},{"nodeId":22,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["y","z"]}}},{"nodeId":23,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#","x":"#TOP#"},"value":["z"]}}},{"nodeId":24,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#"},"value":["x"]}}},{"nodeId":25,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#"},"value":["x","z"]}}},{"nodeId":26,"description":{"expressions":["ret_value@f3"],"state":{"heap":"monolith","type":{"ret_value@f3":"#TOP#"},"value":["x"]}}},{"nodeId":27,"description":{"expressions":["x"],"state":{"heap":"monolith","type":"#TOP#","value":["x"]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/Liveness.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/Liveness.java new file mode 100644 index 000000000..2a628683c --- /dev/null +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/Liveness.java @@ -0,0 +1,163 @@ +package it.unive.lisa.analysis.dataflow; + +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.BinaryExpression; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.TernaryExpression; +import it.unive.lisa.symbolic.value.UnaryExpression; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Objects; +import java.util.stream.Collectors; + +/** + * An implementation of the liveness dataflow analysis, that determines which + * values might be used later on in the program. + * + * @author Luca Negrini + */ +public class Liveness + implements + DataflowElement, Liveness> { + + private final Identifier id; + + /** + * Builds an empty liveness element. + */ + public Liveness() { + this(null); + } + + /** + * Builds the liveness element for the specified id. + * + * @param id the id + */ + public Liveness( + Identifier id) { + this.id = id; + } + + private static Collection getIdentifierOperands( + ValueExpression expression) { + Collection result = new HashSet<>(); + + if (expression == null) + return result; + + if (expression instanceof Identifier) + result.add((Identifier) expression); + + if (expression instanceof UnaryExpression) + result.addAll(getIdentifierOperands((ValueExpression) ((UnaryExpression) expression).getExpression())); + + if (expression instanceof BinaryExpression) { + BinaryExpression binary = (BinaryExpression) expression; + result.addAll(getIdentifierOperands((ValueExpression) binary.getLeft())); + result.addAll(getIdentifierOperands((ValueExpression) binary.getRight())); + } + + if (expression instanceof TernaryExpression) { + TernaryExpression ternary = (TernaryExpression) expression; + result.addAll(getIdentifierOperands((ValueExpression) ternary.getLeft())); + result.addAll(getIdentifierOperands((ValueExpression) ternary.getMiddle())); + result.addAll(getIdentifierOperands((ValueExpression) ternary.getRight())); + } + + return result; + } + + @Override + public Liveness pushScope( + ScopeToken token) + throws SemanticException { + return new Liveness((Identifier) id.pushScope(token)); + } + + @Override + public Liveness popScope( + ScopeToken token) + throws SemanticException { + return new Liveness((Identifier) id.popScope(token)); + } + + @Override + public Collection getInvolvedIdentifiers() { + return Collections.singleton(id); + } + + @Override + public StructuredRepresentation representation() { + return new StringRepresentation(id); + } + + @Override + public String toString() { + return representation().toString(); + } + + @Override + public int hashCode() { + return Objects.hash(id); + } + + @Override + public boolean equals( + Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Liveness other = (Liveness) obj; + return Objects.equals(id, other.id); + } + + @Override + public Collection gen( + Identifier id, + ValueExpression expression, + ProgramPoint pp, + PossibleDataflowDomain domain) + throws SemanticException { + Collection ids = getIdentifierOperands(expression); + return ids.stream().map(Liveness::new).collect(Collectors.toSet()); + } + + @Override + public Collection gen( + ValueExpression expression, + ProgramPoint pp, + PossibleDataflowDomain domain) + throws SemanticException { + Collection ids = getIdentifierOperands(expression); + return ids.stream().map(Liveness::new).collect(Collectors.toSet()); + } + + @Override + public Collection kill( + Identifier id, + ValueExpression expression, + ProgramPoint pp, + PossibleDataflowDomain domain) + throws SemanticException { + return Collections.singleton(new Liveness(id)); + } + + @Override + public Collection kill( + ValueExpression expression, + ProgramPoint pp, + PossibleDataflowDomain domain) + throws SemanticException { + return Collections.emptySet(); + } +} diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java index 373023f95..4b17045a7 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java @@ -6,12 +6,10 @@ import it.unive.lisa.analysis.dataflow.AvailableExpressions; import it.unive.lisa.analysis.dataflow.ConstantPropagation; import it.unive.lisa.analysis.dataflow.DefiniteDataflowDomain; +import it.unive.lisa.analysis.dataflow.Liveness; import it.unive.lisa.analysis.dataflow.PossibleDataflowDomain; import it.unive.lisa.analysis.dataflow.ReachingDefinitions; -import it.unive.lisa.conf.LiSAConfiguration.GraphType; import it.unive.lisa.interprocedural.BackwardModularWorstCaseAnalysis; - -import org.junit.Ignore; import org.junit.Test; public class DataflowAnalysesTest extends AnalysisTestExecutor { @@ -56,19 +54,16 @@ public void testReachingDefinitions() { } @Test - @Ignore public void testLiveness() { CronConfiguration conf = new CronConfiguration(); conf.serializeResults = true; conf.interproceduralAnalysis = new BackwardModularWorstCaseAnalysis<>(); conf.abstractState = DefaultConfiguration.simpleState( DefaultConfiguration.defaultHeapDomain(), - new DefiniteDataflowDomain<>(new AvailableExpressions()), + new PossibleDataflowDomain<>(new Liveness()), DefaultConfiguration.defaultTypeDomain()); conf.testDir = "liveness"; conf.programFile = "liveness.imp"; - conf.analysisGraphs = GraphType.HTML_WITH_SUBNODES; - conf.forceUpdate = true; perform(conf); } } \ No newline at end of file diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InformationFlowTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InformationFlowTest.java index 5f26b2528..7566ae603 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InformationFlowTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InformationFlowTest.java @@ -1,9 +1,5 @@ package it.unive.lisa.cron; -import java.util.Collection; - -import org.junit.Test; - import it.unive.lisa.AnalysisTestExecutor; import it.unive.lisa.CronConfiguration; import it.unive.lisa.DefaultConfiguration; @@ -37,6 +33,8 @@ import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.ValueExpression; +import java.util.Collection; +import org.junit.Test; public class InformationFlowTest extends AnalysisTestExecutor { diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InterproceduralAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InterproceduralAnalysesTest.java index 75969b0c8..d62167944 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InterproceduralAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InterproceduralAnalysesTest.java @@ -12,7 +12,6 @@ import it.unive.lisa.interprocedural.callgraph.RTACallGraph; import it.unive.lisa.interprocedural.context.ContextBasedAnalysis; import it.unive.lisa.interprocedural.context.FullStackToken; - import org.junit.Test; public class InterproceduralAnalysesTest extends AnalysisTestExecutor { diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/MemoryAbstractionsTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/MemoryAbstractionsTest.java index b80c48e6b..1135e54e3 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/MemoryAbstractionsTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/MemoryAbstractionsTest.java @@ -6,7 +6,6 @@ import it.unive.lisa.analysis.heap.TypeBasedHeap; import it.unive.lisa.analysis.heap.pointbased.FieldSensitivePointBasedHeap; import it.unive.lisa.analysis.heap.pointbased.PointBasedHeap; - import org.junit.Test; public class MemoryAbstractionsTest extends AnalysisTestExecutor { diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java index 74888d4ab..0e26a3445 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java @@ -487,7 +487,7 @@ public > AnalyzedCFG backwardFixpoint( throws FixpointException { Map> start = new HashMap<>(); getAllExitpoints().forEach(e -> start.put(e, exitState)); - return fixpoint(exitState, start, interprocedural, ws, conf, id); + return backwardFixpoint(exitState, start, interprocedural, ws, conf, id); } /** @@ -536,7 +536,7 @@ public > AnalyzedCFG backwardFixpoint( throws FixpointException { Map> start = new HashMap<>(); exitpoints.forEach(e -> start.put(e, exitState)); - return fixpoint(exitState, start, interprocedural, ws, conf, id); + return backwardFixpoint(exitState, start, interprocedural, ws, conf, id); } /**