Merge pull request #260 from lisa-analyzer/interproc-fixes

Interprocedural fixes: recursions, call caches, determinism
lisa-analyzer · Apr 20, 2023 · 99aa72a · 99aa72a
2 parents 8034988 + 0e2be86
commit 99aa72a
Show file tree

Hide file tree

Showing 507 changed files with 18,617 additions and 1,126 deletions.
diff --git a/lisa/lisa-analyses/imp-testcases/available-expressions/report.json b/lisa/lisa-analyses/imp-testcases/available-expressions/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_ae.f0(ae__this).json", "untyped_ae.f1(ae__this).json", "untyped_ae.f2(ae__this).json", "untyped_ae.f3(ae__this).json", "untyped_ae.f4(ae__this).json" ],
   "info" : {
     "cfgs" : "5",
-    "duration" : "1s 166ms",
-    "end" : "2023-03-16T22:39:53.870+01:00",
+    "duration" : "1s 596ms",
+    "end" : "2023-04-20T12:45:16.971+02:00",
     "expressions" : "151",
     "files" : "5",
     "globals" : "0",
     "members" : "5",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:52.704+01:00",
+    "start" : "2023-04-20T12:45:15.375+02:00",
     "statements" : "54",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/bricks/report.json b/lisa/lisa-analyses/imp-testcases/bricks/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_bricks.m1(bricks__this).json", "untyped_bricks.m2(bricks__this,_untyped_x).json", "untyped_bricks.m3(bricks__this,_untyped_x).json" ],
   "info" : {
     "cfgs" : "3",
-    "duration" : "840ms",
-    "end" : "2023-03-17T17:37:31.334+01:00",
+    "duration" : "69ms",
+    "end" : "2023-04-20T12:45:39.221+02:00",
     "expressions" : "24",
     "files" : "3",
     "globals" : "0",
     "members" : "3",
     "programs" : "1",
-    "start" : "2023-03-17T17:37:30.494+01:00",
+    "start" : "2023-04-20T12:45:39.152+02:00",
     "statements" : "13",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/char-inclusion/report.json b/lisa/lisa-analyses/imp-testcases/char-inclusion/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_ci.m1(ci__this).json", "untyped_ci.m2(ci__this,_untyped_x).json", "untyped_ci.m3(ci__this,_untyped_x).json" ],
   "info" : {
     "cfgs" : "3",
-    "duration" : "53ms",
-    "end" : "2023-03-16T22:40:04.706+01:00",
+    "duration" : "44ms",
+    "end" : "2023-04-20T12:45:39.324+02:00",
     "expressions" : "24",
     "files" : "3",
     "globals" : "0",
     "members" : "3",
     "programs" : "1",
-    "start" : "2023-03-16T22:40:04.653+01:00",
+    "start" : "2023-04-20T12:45:39.280+02:00",
     "statements" : "13",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/constant-propagation-df/report.json b/lisa/lisa-analyses/imp-testcases/constant-propagation-df/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_cp.f0(cp__this).json", "untyped_cp.f1(cp__this,_untyped_x,_untyped_y).json", "untyped_cp.f2(cp__this).json", "untyped_cp.f3(cp__this,_untyped_x,_untyped_y).json", "untyped_cp.f4(cp__this,_untyped_x,_untyped_y).json" ],
   "info" : {
     "cfgs" : "5",
-    "duration" : "133ms",
-    "end" : "2023-03-16T22:39:55.346+01:00",
+    "duration" : "167ms",
+    "end" : "2023-04-20T12:45:18.621+02:00",
     "expressions" : "71",
     "files" : "5",
     "globals" : "0",
     "members" : "5",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:55.213+01:00",
+    "start" : "2023-04-20T12:45:18.454+02:00",
     "statements" : "33",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/descending-maxglb/report.json b/lisa/lisa-analyses/imp-testcases/descending-maxglb/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_tutorial.doublewhile(tutorial__this,_untyped_t).json", "untyped_tutorial.intv_dec(tutorial__this).json", "untyped_tutorial.sat(tutorial__this).json", "untyped_tutorial.sat2(tutorial__this).json" ],
   "info" : {
     "cfgs" : "4",
-    "duration" : "100ms",
-    "end" : "2023-03-16T22:39:56.785+01:00",
+    "duration" : "129ms",
+    "end" : "2023-04-20T12:45:20.846+02:00",
     "expressions" : "52",
     "files" : "4",
     "globals" : "0",
     "members" : "4",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:56.685+01:00",
+    "start" : "2023-04-20T12:45:20.717+02:00",
     "statements" : "21",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/descending-widening/report.json b/lisa/lisa-analyses/imp-testcases/descending-widening/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_tutorial.doublewhile(tutorial__this,_untyped_t).json", "untyped_tutorial.intv_dec(tutorial__this).json", "untyped_tutorial.sat(tutorial__this).json", "untyped_tutorial.sat2(tutorial__this).json" ],
   "info" : {
     "cfgs" : "4",
-    "duration" : "142ms",
-    "end" : "2023-03-16T22:39:56.340+01:00",
+    "duration" : "254ms",
+    "end" : "2023-04-20T12:45:20.238+02:00",
     "expressions" : "52",
     "files" : "4",
     "globals" : "0",
     "members" : "4",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:56.198+01:00",
+    "start" : "2023-04-20T12:45:19.984+02:00",
     "statements" : "21",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/fsa/report.json b/lisa/lisa-analyses/imp-testcases/fsa/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_fsa.branching(fsa__this,_untyped_x).json", "untyped_fsa.constants(fsa__this).json", "untyped_fsa.loops(fsa__this,_untyped_x).json" ],
   "info" : {
     "cfgs" : "3",
-    "duration" : "387ms",
-    "end" : "2023-03-16T22:40:05.294+01:00",
+    "duration" : "384ms",
+    "end" : "2023-04-20T12:45:39.848+02:00",
     "expressions" : "20",
     "files" : "3",
     "globals" : "0",
     "members" : "3",
     "programs" : "1",
-    "start" : "2023-03-16T22:40:04.907+01:00",
+    "start" : "2023-04-20T12:45:39.464+02:00",
     "statements" : "12",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/heap/point-based-heap/field-insensitive/report.json b/lisa/lisa-analyses/imp-testcases/heap/point-based-heap/field-insensitive/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_A.f1(A__this).json", "untyped_A.f10(A__this).json", "untyped_A.f2(A__this).json", "untyped_A.f3(A__this).json", "untyped_A.f4(A__this).json", "untyped_A.f5(A__this).json", "untyped_A.f6(A__this).json", "untyped_A.f7(A__this).json", "untyped_A.f8(A__this).json", "untyped_A.f9(A__this).json" ],
   "info" : {
     "cfgs" : "10",
-    "duration" : "185ms",
-    "end" : "2023-03-16T22:39:58.192+01:00",
+    "duration" : "216ms",
+    "end" : "2023-04-20T12:45:22.710+02:00",
     "expressions" : "144",
     "files" : "10",
     "globals" : "2",
     "members" : "10",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:58.007+01:00",
+    "start" : "2023-04-20T12:45:22.494+02:00",
     "statements" : "56",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/heap/point-based-heap/field-sensitive/report.json b/lisa/lisa-analyses/imp-testcases/heap/point-based-heap/field-sensitive/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_A.f1(A__this).json", "untyped_A.f2(A__this).json", "untyped_A.f3(A__this).json", "untyped_A.f4(A__this).json", "untyped_A.f5(A__this).json", "untyped_A.f6(A__this).json", "untyped_A.f7(A__this).json", "untyped_A.f8(A__this).json", "untyped_A.f9(A__this).json" ],
   "info" : {
     "cfgs" : "9",
-    "duration" : "271ms",
-    "end" : "2023-03-16T22:39:57.402+01:00",
+    "duration" : "313ms",
+    "end" : "2023-04-20T12:45:21.670+02:00",
     "expressions" : "143",
     "files" : "9",
     "globals" : "2",
     "members" : "9",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:57.131+01:00",
+    "start" : "2023-04-20T12:45:21.357+02:00",
     "statements" : "55",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/heap/type-based-heap/report.json b/lisa/lisa-analyses/imp-testcases/heap/type-based-heap/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_A.f1(A__this).json", "untyped_A.f2(A__this).json", "untyped_A.f3(A__this).json", "untyped_A.f4(A__this).json", "untyped_A.f5(A__this).json" ],
   "info" : {
     "cfgs" : "5",
-    "duration" : "877ms",
-    "end" : "2023-03-17T11:41:28.345+01:00",
+    "duration" : "153ms",
+    "end" : "2023-04-20T12:45:23.512+02:00",
     "expressions" : "75",
     "files" : "5",
     "globals" : "2",
     "members" : "5",
     "programs" : "1",
-    "start" : "2023-03-17T11:41:27.468+01:00",
+    "start" : "2023-04-20T12:45:23.359+02:00",
     "statements" : "27",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/int-const/report.json b/lisa/lisa-analyses/imp-testcases/int-const/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_tutorial.constants(tutorial__this).json", "untyped_tutorial.div(tutorial__this,_untyped_i,_untyped_j).json", "untyped_tutorial.gcd(tutorial__this,_untyped_a,_untyped_b).json", "untyped_tutorial.glb(tutorial__this,_untyped_x,_untyped_y).json", "untyped_tutorial.intv_dec(tutorial__this).json", "untyped_tutorial.sign_parity_example(tutorial__this).json", "untyped_tutorial.ub_example(tutorial__this,_untyped_y,_untyped_z).json" ],
   "info" : {
     "cfgs" : "7",
-    "duration" : "92ms",
-    "end" : "2023-03-16T22:40:03.327+01:00",
+    "duration" : "109ms",
+    "end" : "2023-04-20T12:45:38.052+02:00",
     "expressions" : "77",
     "files" : "7",
     "globals" : "0",
     "members" : "7",
     "programs" : "1",
-    "start" : "2023-03-16T22:40:03.235+01:00",
+    "start" : "2023-04-20T12:45:37.943+02:00",
     "statements" : "32",
     "units" : "1",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_A.foo(A__this).json", "untyped_B.foo(B__this).json", "untyped_tests.subtyping(tests__this).json" ],
   "info" : {
     "cfgs" : "3",
-    "duration" : "36ms",
-    "end" : "2023-03-16T22:40:00.497+01:00",
+    "duration" : "45ms",
+    "end" : "2023-04-20T12:45:26.007+02:00",
     "expressions" : "11",
     "files" : "3",
     "globals" : "0",
     "members" : "3",
     "programs" : "1",
-    "start" : "2023-03-16T22:40:00.461+01:00",
+    "start" : "2023-04-20T12:45:25.962+02:00",
     "statements" : "8",
     "units" : "3",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json
@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_A.foo(A__this).json", "untyped_B.foo(B__this).json", "untyped_tests.subtyping(tests__this).json" ],
   "info" : {
     "cfgs" : "3",
-    "duration" : "34ms",
-    "end" : "2023-03-16T22:40:00.385+01:00",
+    "duration" : "43ms",
+    "end" : "2023-04-20T12:45:25.834+02:00",
     "expressions" : "11",
     "files" : "3",
     "globals" : "0",
     "members" : "3",
     "programs" : "1",
-    "start" : "2023-03-16T22:40:00.351+01:00",
+    "start" : "2023-04-20T12:45:25.791+02:00",
     "statements" : "8",
     "units" : "3",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTAContextSensitive1/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTAContextSensitive1/report.json
@@ -1,16 +1,16 @@
 {
   "warnings" : [ ],
-  "files" : [ "report.json", "untyped_A.A(A__this)_-1137467753.json", "untyped_A.getOne(A__this)_-1136543333.json", "untyped_A.getPositive(A__this,_untyped_i)_-1134695237.json", "untyped_A.getPositive(A__this,_untyped_i)_-1135618727.json", "untyped_tests.main(tests__this).json" ],
+  "files" : [ "report.json", "untyped_A.A(A__this)_1677856240.json", "untyped_A.getOne(A__this)_1677863959.json", "untyped_A.getPositive(A__this,_untyped_i)_1677876514.json", "untyped_A.getPositive(A__this,_untyped_i)_1677877444.json", "untyped_tests.main(tests__this).json" ],
   "info" : {
     "cfgs" : "5",
-    "duration" : "123ms",
-    "end" : "2023-03-16T22:39:59.237+01:00",
+    "duration" : "142ms",
+    "end" : "2023-04-20T12:45:23.913+02:00",
     "expressions" : "26",
     "files" : "5",
     "globals" : "0",
     "members" : "5",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:59.114+01:00",
+    "start" : "2023-04-20T12:45:23.771+02:00",
     "statements" : "14",
     "units" : "2",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/...ve1/untyped_A.A(A__this)_-1137467753.json → ...ive1/untyped_A.A(A__this)_1677856240.json b/...ve1/untyped_A.A(A__this)_-1137467753.json → ...ive1/untyped_A.A(A__this)_1677856240.json
diff --git a/...ntyped_A.getOne(A__this)_-1136543333.json → ...untyped_A.getOne(A__this)_1677863959.json b/...ntyped_A.getOne(A__this)_-1136543333.json → ...untyped_A.getOne(A__this)_1677863959.json
diff --git a/...tive(A__this,_untyped_i)_-1134695237.json → ...itive(A__this,_untyped_i)_1677876514.json b/...tive(A__this,_untyped_i)_-1134695237.json → ...itive(A__this,_untyped_i)_1677876514.json
diff --git a/...tive(A__this,_untyped_i)_-1135618727.json → ...itive(A__this,_untyped_i)_1677877444.json b/...tive(A__this,_untyped_i)_-1135618727.json → ...itive(A__this,_untyped_i)_1677877444.json
diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTAContextSensitive2/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTAContextSensitive2/report.json
@@ -1,16 +1,16 @@
 {
   "warnings" : [ ],
-  "files" : [ "report.json", "untyped_A.A(A__this)_-1429946402.json", "untyped_A.identity(A__this,_untyped_i)_-1402239687.json", "untyped_A.identity(A__this,_untyped_i)_-1426250396.json", "untyped_A.identity(A__this,_untyped_i)_-1428098244.json", "untyped_tests.helper(tests__this,_untyped_i,_untyped_dispatcher)_-1425327712.json", "untyped_tests.main(tests__this).json" ],
+  "files" : [ "report.json", "untyped_A.A(A__this)_1678785558.json", "untyped_A.identity(A__this,_untyped_i)_1678799291.json", "untyped_A.identity(A__this,_untyped_i)_1678800035.json", "untyped_A.identity(A__this,_untyped_i)_1678804902.json", "untyped_tests.helper(tests__this,_untyped_i,_untyped_dispatcher)_1678799167.json", "untyped_tests.main(tests__this).json" ],
   "info" : {
     "cfgs" : "6",
-    "duration" : "93ms",
-    "end" : "2023-03-16T22:39:59.450+01:00",
+    "duration" : "141ms",
+    "end" : "2023-04-20T12:45:24.270+02:00",
     "expressions" : "35",
     "files" : "6",
     "globals" : "0",
     "members" : "6",
     "programs" : "1",
-    "start" : "2023-03-16T22:39:59.357+01:00",
+    "start" : "2023-04-20T12:45:24.129+02:00",
     "statements" : "17",
     "units" : "2",
     "version" : "0.1b7",
@@ -26,6 +26,7 @@
     "jsonOutput" : "true",
     "openCallPolicy" : "WorstCasePolicy",
     "optimize" : "false",
+    "recursionWideningThreshold" : "5",
     "semanticChecks" : "",
     "serializeInputs" : "false",
     "serializeResults" : "true",

diff --git a/...ve2/untyped_A.A(A__this)_-1429946402.json → ...ive2/untyped_A.A(A__this)_1678785558.json b/...ve2/untyped_A.A(A__this)_-1429946402.json → ...ive2/untyped_A.A(A__this)_1678785558.json
diff --git a/...tity(A__this,_untyped_i)_-1402239687.json → ...ntity(A__this,_untyped_i)_1678799291.json b/...tity(A__this,_untyped_i)_-1402239687.json → ...ntity(A__this,_untyped_i)_1678799291.json
diff --git a/...tity(A__this,_untyped_i)_-1428098244.json → ...ntity(A__this,_untyped_i)_1678800035.json b/...tity(A__this,_untyped_i)_-1428098244.json → ...ntity(A__this,_untyped_i)_1678800035.json
diff --git a/...tity(A__this,_untyped_i)_-1426250396.json → ...ntity(A__this,_untyped_i)_1678804902.json b/...tity(A__this,_untyped_i)_-1426250396.json → ...ntity(A__this,_untyped_i)_1678804902.json
diff --git a/...d_i,_untyped_dispatcher)_-1425327712.json → ...ed_i,_untyped_dispatcher)_1678799167.json b/...d_i,_untyped_dispatcher)_-1425327712.json → ...ed_i,_untyped_dispatcher)_1678799167.json