Liveness analysis #120

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;
+	}
+}

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"
+  }
+}

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":[]}}}]}

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"]}}}]}

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"]}}}]}