diff --git a/lisa/lisa-analyses/imp-testcases/string/strings-subs.imp b/lisa/lisa-analyses/imp-testcases/string/strings-subs.imp
index e87b61f13..3bda5c960 100644
--- a/lisa/lisa-analyses/imp-testcases/string/strings-subs.imp
+++ b/lisa/lisa-analyses/imp-testcases/string/strings-subs.imp
@@ -104,7 +104,8 @@ class strings {
def z = "b";
def w = y + z;
}
-
+
+
paper2(){
def x = "";
def y = "";
@@ -114,7 +115,6 @@ class strings {
x = y + "c";
}
-
paper3(x){
def v = "";
if (x % 2)
@@ -155,5 +155,27 @@ class strings {
s = s + "c";
}
+ replace(){
+ def y = "c";
+ def x = strrep("ab", "ab", "a") + "b" + y;
+ def z = "b" + y;
+ }
+
+ replace2(){
+ def y = "xyz";
+ def x = "ab" + strrep(y, "x", "yz") + "c";
+ }
+
+ substring(){
+ def y = "c";
+ def x = strsub("ab", 0, 1) + "b" + y;
+ def z = "b" + y;
+ }
+
+ substring2(){
+ def y = "xyz";
+ def x = "ab" + strsub(y, 0, 1) + "c";
+ }
+
}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json b/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json
index 75979178f..b3881975f 100644
--- a/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json
@@ -3,14 +3,14 @@
"files" : [ "report.json", "untyped_strings.constants(strings__this).json", "untyped_strings.replace(strings__this,_untyped_s).json" ],
"info" : {
"cfgs" : "2",
- "duration" : "11ms",
- "end" : "2024-04-25T12:26:36.264+02:00",
+ "duration" : "9ms",
+ "end" : "2024-06-22T12:58:22.543+02:00",
"expressions" : "29",
"files" : "2",
"globals" : "0",
"members" : "2",
"programs" : "1",
- "start" : "2024-04-25T12:26:36.253+02:00",
+ "start" : "2024-06-22T12:58:22.534+02:00",
"statements" : "12",
"units" : "1",
"version" : "0.1b9",
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json
index 951f3609f..b1186d127 100644
--- a/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json
@@ -1,17 +1,17 @@
{
"warnings" : [ ],
- "files" : [ "report.json", "untyped_strings.assume(strings__this).json", "untyped_strings.branching(strings__this,_untyped_x).json", "untyped_strings.closure(strings__this).json", "untyped_strings.closure2(strings__this).json", "untyped_strings.closure3(strings__this).json", "untyped_strings.constants(strings__this).json", "untyped_strings.iftest1(strings__this).json", "untyped_strings.iftest2(strings__this).json", "untyped_strings.iftestand(strings__this).json", "untyped_strings.iftestor(strings__this).json", "untyped_strings.integers(strings__this).json", "untyped_strings.interassign(strings__this).json", "untyped_strings.loops(strings__this,_untyped_x).json", "untyped_strings.paper1(strings__this).json", "untyped_strings.paper2(strings__this).json", "untyped_strings.paper3(strings__this,_untyped_x).json", "untyped_strings.scopetest(strings__this,_untyped_x).json", "untyped_strings.stringconcat(strings__this).json", "untyped_strings.type(strings__this,_untyped_x).json" ],
+ "files" : [ "report.json", "untyped_strings.assume(strings__this).json", "untyped_strings.branching(strings__this,_untyped_x).json", "untyped_strings.closure(strings__this).json", "untyped_strings.closure2(strings__this).json", "untyped_strings.closure3(strings__this).json", "untyped_strings.constants(strings__this).json", "untyped_strings.iftest1(strings__this).json", "untyped_strings.iftest2(strings__this).json", "untyped_strings.iftestand(strings__this).json", "untyped_strings.iftestor(strings__this).json", "untyped_strings.integers(strings__this).json", "untyped_strings.interassign(strings__this).json", "untyped_strings.loops(strings__this,_untyped_x).json", "untyped_strings.paper1(strings__this).json", "untyped_strings.paper2(strings__this).json", "untyped_strings.paper3(strings__this,_untyped_x).json", "untyped_strings.replace(strings__this).json", "untyped_strings.replace2(strings__this).json", "untyped_strings.scopetest(strings__this,_untyped_x).json", "untyped_strings.stringconcat(strings__this).json", "untyped_strings.substring(strings__this).json", "untyped_strings.substring2(strings__this).json", "untyped_strings.type(strings__this,_untyped_x).json" ],
"info" : {
- "cfgs" : "19",
- "duration" : "92ms",
- "end" : "2024-06-14T23:04:08.375+02:00",
- "expressions" : "206",
- "files" : "19",
+ "cfgs" : "23",
+ "duration" : "107ms",
+ "end" : "2024-06-22T12:54:35.326+02:00",
+ "expressions" : "258",
+ "files" : "23",
"globals" : "0",
- "members" : "19",
+ "members" : "23",
"programs" : "1",
- "start" : "2024-06-14T23:04:08.283+02:00",
- "statements" : "100",
+ "start" : "2024-06-22T12:54:35.219+02:00",
+ "statements" : "114",
"units" : "1",
"version" : "0.1b9",
"warnings" : "0"
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json
index ebf768c1a..103be06d2 100644
--- a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json
@@ -1 +1 @@
-{"name":"untyped strings::paper2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"\""},{"id":1,"text":"x"},{"id":2,"text":"\"\""},{"id":3,"subNodes":[4,5],"text":"y = \"\""},{"id":4,"text":"y"},{"id":5,"text":"\"\""},{"id":6,"subNodes":[7,8],"text":"equals(x, y)"},{"id":7,"text":"x"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"x = +(x, \"c\")"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, \"c\")"},{"id":12,"text":"x"},{"id":13,"text":"\"c\""},{"id":14,"subNodes":[15,16],"text":"x = +(y, \"c\")"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(y, \"c\")"},{"id":17,"text":"y"},{"id":18,"text":"\"c\""},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":19,"kind":"SequentialEdge"},{"sourceId":14,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["x strcmp y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\""]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":11,"description":{"expressions":["x strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":13,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y","y strcat \"c\""]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":16,"description":{"expressions":["y strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":18,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\""]}}}}]}
\ No newline at end of file
+{"name":"untyped strings::paper2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"\""},{"id":1,"text":"x"},{"id":2,"text":"\"\""},{"id":3,"subNodes":[4,5],"text":"y = \"\""},{"id":4,"text":"y"},{"id":5,"text":"\"\""},{"id":6,"subNodes":[7,8],"text":"equals(x, y)"},{"id":7,"text":"x"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"x = +(x, \"c\")"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, \"c\")"},{"id":12,"text":"x"},{"id":13,"text":"\"c\""},{"id":14,"subNodes":[15,16],"text":"x = +(y, \"c\")"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(y, \"c\")"},{"id":17,"text":"y"},{"id":18,"text":"\"c\""},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":19,"kind":"SequentialEdge"},{"sourceId":14,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["x strcmp y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y"]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":11,"description":{"expressions":["x strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":13,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y","y strcat \"c\""]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":16,"description":{"expressions":["y strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":18,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y"]}}}}]}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace(strings__this).json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace(strings__this).json
new file mode 100644
index 000000000..f730c75a9
--- /dev/null
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace(strings__this).json
@@ -0,0 +1 @@
+{"name":"untyped strings::replace(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"y = \"c\""},{"id":1,"text":"y"},{"id":2,"text":"\"c\""},{"id":3,"subNodes":[4,5],"text":"x = +(+(replace(\"ab\", \"ab\", \"a\"), \"b\"), y)"},{"id":4,"text":"x"},{"id":5,"subNodes":[6,12],"text":"+(+(replace(\"ab\", \"ab\", \"a\"), \"b\"), y)"},{"id":6,"subNodes":[7,11],"text":"+(replace(\"ab\", \"ab\", \"a\"), \"b\")"},{"id":7,"subNodes":[8,9,10],"text":"replace(\"ab\", \"ab\", \"a\")"},{"id":8,"text":"\"ab\""},{"id":9,"text":"\"ab\""},{"id":10,"text":"\"a\""},{"id":11,"text":"\"b\""},{"id":12,"text":"y"},{"id":13,"subNodes":[14,15],"text":"z = +(\"b\", y)"},{"id":14,"text":"z"},{"id":15,"subNodes":[16,17],"text":"+(\"b\", y)"},{"id":16,"text":"\"b\""},{"id":17,"text":"y"},{"id":18,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":13,"kind":"SequentialEdge"},{"sourceId":13,"destId":18,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":1,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":5,"description":{"expressions":["\"ab\" strreplace(\"ab\", \"a\") strcat \"b\" strcat y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":6,"description":{"expressions":["\"ab\" strreplace(\"ab\", \"a\") strcat \"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":7,"description":{"expressions":["\"ab\" strreplace(\"ab\", \"a\")"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":8,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":9,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":10,"description":{"expressions":["\"a\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":11,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":12,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":13,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y","z"],"y":["\"c\""],"z":["\"b\"","\"b\" strcat y","\"c\"","y"]}}}},{"nodeId":14,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":15,"description":{"expressions":["\"b\" strcat y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":16,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":18,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y","z"],"y":["\"c\""],"z":["\"b\"","\"b\" strcat y","\"c\"","y"]}}}}]}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace2(strings__this).json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace2(strings__this).json
new file mode 100644
index 000000000..8142ceec7
--- /dev/null
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace2(strings__this).json
@@ -0,0 +1 @@
+{"name":"untyped strings::replace2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"y = \"xyz\""},{"id":1,"text":"y"},{"id":2,"text":"\"xyz\""},{"id":3,"subNodes":[4,5],"text":"x = +(+(\"ab\", replace(y, \"x\", \"yz\")), \"c\")"},{"id":4,"text":"x"},{"id":5,"subNodes":[6,12],"text":"+(+(\"ab\", replace(y, \"x\", \"yz\")), \"c\")"},{"id":6,"subNodes":[7,8],"text":"+(\"ab\", replace(y, \"x\", \"yz\"))"},{"id":7,"text":"\"ab\""},{"id":8,"subNodes":[9,10,11],"text":"replace(y, \"x\", \"yz\")"},{"id":9,"text":"y"},{"id":10,"text":"\"x\""},{"id":11,"text":"\"yz\""},{"id":12,"text":"\"c\""},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":1,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"xyz\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"b\"","\"c\""],"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":5,"description":{"expressions":["\"ab\" strcat y strreplace(\"x\", \"yz\") strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":6,"description":{"expressions":["\"ab\" strcat y strreplace(\"x\", \"yz\")"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":7,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":8,"description":{"expressions":["y strreplace(\"x\", \"yz\")"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":9,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":10,"description":{"expressions":["\"x\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":11,"description":{"expressions":["\"yz\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":12,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"b\"","\"c\""],"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}}]}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring(strings__this).json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring(strings__this).json
new file mode 100644
index 000000000..756404695
--- /dev/null
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring(strings__this).json
@@ -0,0 +1 @@
+{"name":"untyped strings::substring(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"y = \"c\""},{"id":1,"text":"y"},{"id":2,"text":"\"c\""},{"id":3,"subNodes":[4,5],"text":"x = +(+(substring(\"ab\", 0, 1), \"b\"), y)"},{"id":4,"text":"x"},{"id":5,"subNodes":[6,12],"text":"+(+(substring(\"ab\", 0, 1), \"b\"), y)"},{"id":6,"subNodes":[7,11],"text":"+(substring(\"ab\", 0, 1), \"b\")"},{"id":7,"subNodes":[8,9,10],"text":"substring(\"ab\", 0, 1)"},{"id":8,"text":"\"ab\""},{"id":9,"text":"0"},{"id":10,"text":"1"},{"id":11,"text":"\"b\""},{"id":12,"text":"y"},{"id":13,"subNodes":[14,15],"text":"z = +(\"b\", y)"},{"id":14,"text":"z"},{"id":15,"subNodes":[16,17],"text":"+(\"b\", y)"},{"id":16,"text":"\"b\""},{"id":17,"text":"y"},{"id":18,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":13,"kind":"SequentialEdge"},{"sourceId":13,"destId":18,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":1,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":5,"description":{"expressions":["\"ab\" substr(0, 1) strcat \"b\" strcat y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":6,"description":{"expressions":["\"ab\" substr(0, 1) strcat \"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":7,"description":{"expressions":["\"ab\" substr(0, 1)"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":8,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":9,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":10,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":11,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":12,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"c\""]}}}},{"nodeId":13,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y","z"],"y":["\"c\""],"z":["\"b\"","\"b\" strcat y","\"c\"","y"]}}}},{"nodeId":14,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":15,"description":{"expressions":["\"b\" strcat y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":16,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y"],"y":["\"c\""]}}}},{"nodeId":18,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":{"x":["\"a\"","\"ab\"","\"ab\" strcat y","\"b\"","\"b\" strcat y","\"c\"","y","z"],"y":["\"c\""],"z":["\"b\"","\"b\" strcat y","\"c\"","y"]}}}}]}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring2(strings__this).json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring2(strings__this).json
new file mode 100644
index 000000000..292c60e7c
--- /dev/null
+++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring2(strings__this).json
@@ -0,0 +1 @@
+{"name":"untyped strings::substring2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"y = \"xyz\""},{"id":1,"text":"y"},{"id":2,"text":"\"xyz\""},{"id":3,"subNodes":[4,5],"text":"x = +(+(\"ab\", substring(y, 0, 1)), \"c\")"},{"id":4,"text":"x"},{"id":5,"subNodes":[6,12],"text":"+(+(\"ab\", substring(y, 0, 1)), \"c\")"},{"id":6,"subNodes":[7,8],"text":"+(\"ab\", substring(y, 0, 1))"},{"id":7,"text":"\"ab\""},{"id":8,"subNodes":[9,10,11],"text":"substring(y, 0, 1)"},{"id":9,"text":"y"},{"id":10,"text":"0"},{"id":11,"text":"1"},{"id":12,"text":"\"c\""},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":1,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"xyz\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"b\"","\"c\""],"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":5,"description":{"expressions":["\"ab\" strcat y substr(0, 1) strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":6,"description":{"expressions":["\"ab\" strcat y substr(0, 1)"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":7,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":8,"description":{"expressions":["y substr(0, 1)"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":9,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":10,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":11,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":12,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"y":["string"]},"value":{"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"a\"","\"ab\"","\"b\"","\"c\""],"y":["\"x\"","\"xy\"","\"xyz\"","\"y\"","\"yz\"","\"z\""]}}}}]}
\ No newline at end of file
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/StringConstantPropagation.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/StringConstantPropagation.java
index f4f3df253..38da7f383 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/StringConstantPropagation.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/StringConstantPropagation.java
@@ -17,6 +17,7 @@
import it.unive.lisa.symbolic.value.operator.binary.ComparisonNe;
import it.unive.lisa.symbolic.value.operator.binary.StringConcat;
import it.unive.lisa.symbolic.value.operator.ternary.StringReplace;
+import it.unive.lisa.symbolic.value.operator.ternary.StringSubstring;
import it.unive.lisa.symbolic.value.operator.ternary.TernaryOperator;
import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
import it.unive.lisa.util.representation.StringRepresentation;
@@ -29,7 +30,7 @@
* {@link BaseLattice#lub}, {@link BaseLattice#widening} and
* {@link BaseLattice#lessOrEqual}, respectively.
*
- * @author Michele
+ * @author Michele
* Martelli
* @author Vincenzo Arceri
*/
@@ -159,6 +160,7 @@ public StringConstantPropagation evalTernaryExpression(
return new StringConstantPropagation(replaced);
}
+
return top();
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomain.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomain.java
index 988cf93bf..eee3df2e5 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomain.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomain.java
@@ -13,6 +13,7 @@
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.TernaryExpression;
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.symbolic.value.Variable;
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
@@ -23,6 +24,9 @@
import it.unive.lisa.symbolic.value.operator.binary.StringEndsWith;
import it.unive.lisa.symbolic.value.operator.binary.StringEquals;
import it.unive.lisa.symbolic.value.operator.binary.StringStartsWith;
+import it.unive.lisa.symbolic.value.operator.ternary.StringReplace;
+import it.unive.lisa.symbolic.value.operator.ternary.StringSubstring;
+import it.unive.lisa.type.NumericType;
import it.unive.lisa.type.Type;
import java.util.ArrayList;
import java.util.Collections;
@@ -42,7 +46,7 @@
* in
* this paper.
*
- * @author Michele
+ * @author Michele
* Martelli
* @author Vincenzo Arceri
*/
@@ -144,13 +148,13 @@ public SubstringDomain assign(
// expression
strType = expression.getStaticType();
- Set identifiers = extrPlus(expression, strType);
+ Set expressions = extrPlus(expression, pp, oracle, strType);
SubstringDomain result = mk(lattice, mkNewFunction(function, false));
- result = result.remove(identifiers, id);
+ result = result.remove(expressions, id);
- result = result.add(identifiers, id);
+ result = result.add(expressions, id);
result = result.interasg(id, expression);
@@ -164,7 +168,7 @@ public SubstringDomain smallStepSemantics(
ValueExpression expression,
ProgramPoint pp,
SemanticOracle oracle)
- throws SemanticException {
+ throws SemanticException {
return this;
}
@@ -176,8 +180,6 @@ public SubstringDomain assume(
SemanticOracle oracle)
throws SemanticException {
- SubstringDomain result = mk(lattice, mkNewFunction(function, false));
-
/*
* Assume only binary expressions
*/
@@ -215,21 +217,30 @@ public SubstringDomain assume(
if (!(right instanceof ValueExpression))
throw new SemanticException("instanceof right");
- Set extracted = extrPlus((ValueExpression) right, strType);
+ Set extracted = extrPlus((ValueExpression) right, src, oracle, strType);
+
+ SubstringDomain result = mk(lattice, mkNewFunction(function, false));
result = result.add(extracted, (Identifier) left);
result = result.closure();
+
+ return result.clear();
} else if (binaryOperator instanceof StringEquals) {
/*
* Case both operands are identifiers
*/
if ((left instanceof Identifier) && (right instanceof Identifier)) {
- result = result.add(extrPlus((ValueExpression) left, strType), (Identifier) right);
- result = result.add(extrPlus((ValueExpression) right, strType), (Identifier) left);
+
+ SubstringDomain result = mk(lattice, mkNewFunction(function, false));
+
+ result = result.add(left, (Identifier) right);
+ result = result.add(right, (Identifier) left);
result = result.closure();
+
+ return result.clear();
}
/*
@@ -249,11 +260,15 @@ else if ((left instanceof Identifier) || (right instanceof Identifier)) {
if (!(right instanceof ValueExpression))
throw new SemanticException("instanceof right != ValueExpression.class");
- Set add = extrPlus((ValueExpression) right, strType);
+ Set add = extrPlus((ValueExpression) right, src, oracle, strType);
+
+ SubstringDomain result = mk(lattice, mkNewFunction(function, false));
result = result.add(add, (Identifier) left);
result = result.closure();
+
+ return result.clear();
}
} else if (binaryOperator instanceof LogicalOr || binaryOperator instanceof LogicalAnd) {
@@ -269,15 +284,15 @@ else if ((left instanceof Identifier) || (right instanceof Identifier)) {
SubstringDomain rightDomain = assume(rightValueExpression, src, dest, oracle);
if (binaryOperator instanceof LogicalOr) {
- result = leftDomain.lub(rightDomain);
+ return leftDomain.lub(rightDomain).clear();
} else {
- result = leftDomain.glb(rightDomain);
+ return leftDomain.glb(rightDomain).clear();
}
}
}
- return result.clear();
+ return this;
}
@Override
@@ -309,14 +324,11 @@ public SubstringDomain forgetIdentifier(
Map newFunction = mkNewFunction(function, false); // function
// !=
// null
-
newFunction.remove(id);
newFunction.replaceAll((
key,
- value) -> new ExpressionInverseSet(value.elements.stream()
- .filter(v -> !appears(id, v))
- .collect(Collectors.toSet())));
+ value) -> removeFromSet(value, id));
return mk(lattice, newFunction);
}
@@ -328,12 +340,9 @@ public SubstringDomain forgetIdentifiersIf(
if (function == null || function.keySet().isEmpty())
return this;
- Map newFunction = mkNewFunction(function, false); // function
- // !=
- // null
-
+ // Get all identifiers
Set ids = new HashSet<>();
- for (Map.Entry entry : newFunction.entrySet()) {
+ for (Map.Entry entry : function.entrySet()) {
ids.add(entry.getKey());
for (SymbolicExpression s : entry.getValue().elements()) {
if (s instanceof Identifier) {
@@ -342,20 +351,17 @@ public SubstringDomain forgetIdentifiersIf(
}
}
}
+
+ SubstringDomain result = mk(lattice, mkNewFunction(function, false));
for (Identifier id : ids) {
+ // Test each identifier
if (test.test(id)) {
- newFunction.remove(id);
-
- newFunction.replaceAll((
- key,
- value) -> new ExpressionInverseSet(value.elements.stream()
- .filter(v -> !appears(id, v))
- .collect(Collectors.toSet())));
+ result = result.forgetIdentifier(id);
}
}
- return mk(lattice, newFunction);
+ return result;
}
@Override
@@ -439,24 +445,21 @@ public SubstringDomain popScope(
* @param expression to extract
* @return List containing the sub-expressions
*/
- private static List extr(
+ private static List extr(
ValueExpression expression) {
- List result = new ArrayList<>();
- if (expression instanceof BinaryExpression) {
+ List result = new ArrayList<>();
+ if (expression instanceof BinaryExpression && ((BinaryExpression)expression).getOperator() instanceof StringConcat) {
BinaryExpression binaryExpression = (BinaryExpression) expression;
- BinaryOperator binaryOperator = binaryExpression.getOperator();
- if (!(binaryOperator instanceof StringConcat))
- return Collections.emptyList();
ValueExpression left = (ValueExpression) binaryExpression.getLeft();
ValueExpression right = (ValueExpression) binaryExpression.getRight();
result.addAll(extr(left));
result.addAll(extr(right));
- } else if (expression instanceof Variable || expression instanceof Constant) {
+ } else
result.add(expression);
- }
+
return result;
}
@@ -467,94 +470,155 @@ private static List extr(
* @param strType
* @return
*/
- private static Set extrPlus(
+ private Set extrPlus(
ValueExpression expression,
- Type strType) {
- List extracted = extr(expression);
-
+ ProgramPoint pp,
+ SemanticOracle oracle,
+ Type strType) throws SemanticException {
+ List extracted = extr(expression);
+
/*
* If there are more than 2 consecutive constants, merge them into a
* single constant
*/
- extracted = mergeStringLiterals(extracted, strType);
+ List> sub_expressions = split(extracted, pp, oracle, strType);
+
+ for (int i = 0; i < sub_expressions.size(); i++) {
+ List list = sub_expressions.get(i);
+ sub_expressions.set(i, mergeStringLiterals(list, strType));
+ }
Set result = new HashSet<>();
+
+ // Iterate sublists splitted from StringReplace expressions
+ for (List list : sub_expressions) {
+ // Iterate over the length of the expression
+ for (int l = 1; l <= list.size(); l++) {
+ // Iterate from the start to the end according to the size of the
+ // expression to create
+ for (int i = 0; i <= (list.size() - l); i++) {
+ List subList = list.subList(i, i + l);
+ result.add(composeExpression(subList));
+
+ if (subList.size() == 1 && subList.get(0) instanceof Constant) {
+ /*
+ * Case the expression to ass is a single constant -> add
+ * its substrings
+ */
+ Set substrings = getSubstrings((Constant) subList.get(0));
- // Iterate over the length of the expression
- for (int l = 1; l <= extracted.size(); l++) {
- // Iterate from the start to the end according to the size of the
- // expression to create
- for (int i = 0; i <= (extracted.size() - l); i++) {
- List subList = extracted.subList(i, i + l);
- result.add(composeExpression(subList));
+ for (Constant substring : substrings) {
+ List newList = new ArrayList<>();
+ newList.add(substring);
- if (subList.size() == 1 && subList.get(0) instanceof Constant) {
- /*
- * Case the expression to ass is a single constant -> add
- * its substrings
- */
- Set substrings = getSubstrings((Constant) subList.get(0));
+ result.add(composeExpression(newList));
- for (SymbolicExpression substring : substrings) {
- List newList = new ArrayList<>();
- newList.add(substring);
+ }
+ } else if (subList.get(0) instanceof Constant) {
+ /*
+ * Case the first expression of the expression to add is a
+ * constant -> add an expression for each suffix of the
+ * constant
+ */
+ Set suffixes = getSuffix((Constant) subList.get(0));
- result.add(composeExpression(newList));
+ for (Constant suffix : suffixes) {
+ List newList = new ArrayList<>(subList);
+ newList.set(0, suffix);
- }
- } else if (subList.get(0) instanceof Constant) {
- /*
- * Case the first expression of the expression to add is a
- * constant -> add an expression for each suffix of the
- * constant
- */
- Set suffixes = getSuffix((Constant) subList.get(0));
-
- for (SymbolicExpression suffix : suffixes) {
- List newList = new ArrayList<>(subList);
- newList.set(0, suffix);
-
- if (subList.get(subList.size() - 1) instanceof Constant) {
-
- /*
- * Case the last expression of the expression to add
- * is a constant -> add an expression for each
- * prefix of the constant
- */
- Set prefixes = getPrefix((Constant) subList.get(subList.size() - 1));
-
- for (SymbolicExpression prefix : prefixes) {
- newList.set(newList.size() - 1, prefix);
+ if (subList.get(subList.size() - 1) instanceof Constant) {
+ /*
+ * Case the last expression of the expression to add
+ * is a constant -> add an expression for each
+ * prefix of the constant
+ */
+ Set prefixes = getPrefix((Constant) subList.get(subList.size() - 1));
+
+ for (Constant prefix : prefixes) {
+ newList.set(newList.size() - 1, prefix);
+
+ result.add(composeExpression(newList));
+ }
+ } else
result.add(composeExpression(newList));
- }
- } else
- result.add(composeExpression(newList));
- }
- } else if (subList.get(subList.size() - 1) instanceof Constant) {
+ }
+ } else if (subList.get(subList.size() - 1) instanceof Constant) {
- /*
- * Case the last expression of the expression to add is a
- * constant -> add an expression for each prefix of the
- * constant
- */
+ /*
+ * Case the last expression of the expression to add is a
+ * constant -> add an expression for each prefix of the
+ * constant
+ */
- Set prefixes = getPrefix((Constant) subList.get(subList.size() - 1));
+ Set prefixes = getPrefix((Constant) subList.get(subList.size() - 1));
- for (SymbolicExpression prefix : prefixes) {
- List newList = new ArrayList<>(subList);
- newList.set(newList.size() - 1, prefix);
+ for (Constant prefix : prefixes) {
+ List newList = new ArrayList<>(subList);
+ newList.set(newList.size() - 1, prefix);
- result.add(composeExpression(newList));
+ result.add(composeExpression(newList));
+ }
}
- }
+ }
}
}
-
return new HashSet<>(result);
}
+
+ private List> split(List extracted, ProgramPoint pp, SemanticOracle oracle, Type strType) throws SemanticException{
+ List> result = new ArrayList<>();
+
+ List temp = new ArrayList<>();
+
+ for(ValueExpression s : extracted) {
+ if (!(s instanceof Identifier || s instanceof Constant)) {
+ // s in not Identifier or Constant -> eval s semantics
+
+ if (s instanceof TernaryExpression) {
+ TernaryExpression ternaryExpression = (TernaryExpression) s;
+ if (ternaryExpression.getLeft() instanceof Constant && ternaryExpression.getMiddle() instanceof Constant && ternaryExpression.getRight() instanceof Constant) {
+ Constant c1 = (Constant) ternaryExpression.getLeft();
+ Constant c2 = (Constant) ternaryExpression.getMiddle();
+ Constant c3 = (Constant) ternaryExpression.getRight();
+
+ if (ternaryExpression.getOperator() instanceof StringReplace) {
+ String s1 = c1.getValue() instanceof String ? (String) c1.getValue() : c1.getValue().toString();
+ String s2 = c2.getValue() instanceof String ? (String) c2.getValue() : c2.getValue().toString();
+ String s3 = c3.getValue() instanceof String ? (String) c3.getValue() : c3.getValue().toString();
+
+ // Special case: add the constant and do not split list
+ temp.add(new Constant(strType, s1.replace(s2, s3), SyntheticLocation.INSTANCE));
+ continue;
+ }
+ if (ternaryExpression.getOperator() instanceof StringSubstring && c2.getValue() instanceof Integer && c3.getValue() instanceof Integer) {
+ String s1 = c1.getValue() instanceof String ? (String) c1.getValue() : c1.getValue().toString();
+ Integer i1 = (Integer) c2.getValue();
+ Integer i2 = (Integer) c3.getValue();
+
+ // Special case: add the constant and do not split list
+ temp.add(new Constant(strType, s1.substring(i1, i2), SyntheticLocation.INSTANCE));
+ continue;
+ }
+ }
+ }
+
+ // Split list
+ result.add(new ArrayList<>(temp));
+ temp.clear();
+
+ } else {
+ // s instance of Identifier || s instance of Constant
+ temp.add(s);
+ }
+ }
+
+ result.add(temp);
+
+ return result;
+ }
/*
* Returns a list with no more than one consecutive constant where if {@code
@@ -563,13 +627,13 @@ private static Set extrPlus(
* @param strType
* @return The list without consecutive constants.
*/
- private static List mergeStringLiterals(
- List extracted,
+ private static List mergeStringLiterals(
+ List extracted,
Type strType) {
- List result = new ArrayList<>();
+ List result = new ArrayList<>();
StringBuilder recent = new StringBuilder();
- for (SymbolicExpression expr : extracted) {
+ for (ValueExpression expr : extracted) {
if (expr instanceof Constant) {
// Update the string builder value adding the value of the
// constant
@@ -604,9 +668,9 @@ private static List mergeStringLiterals(
* @param c Constant to analyze
* @return The set containing the substrings of a Constant
*/
- private static Set getSubstrings(
+ private static Set getSubstrings(
Constant c) {
- Set result = new HashSet<>();
+ Set result = new HashSet<>();
String str = c.getValue() instanceof String ? (String) c.getValue() : c.getValue().toString();
@@ -614,7 +678,7 @@ private static Set getSubstrings(
for (int l = 1; l < str.length(); l++) {
// Iterate over the starting char
for (int i = 0; i <= str.length() - l; i++) {
- ValueExpression substring = new Constant(c.getStaticType(), str.substring(i, i + l),
+ Constant substring = new Constant(c.getStaticType(), str.substring(i, i + l),
SyntheticLocation.INSTANCE);
result.add(substring);
@@ -629,14 +693,14 @@ private static Set getSubstrings(
* @param c Constant to analyze
* @return The set containing the prefixes of a Constant
*/
- private static Set getPrefix(
+ private static Set getPrefix(
Constant c) {
- Set result = new HashSet<>();
+ Set result = new HashSet<>();
String str = c.getValue() instanceof String ? (String) c.getValue() : c.getValue().toString();
// Iterate over the length
for (int i = 1; i <= str.length(); i++) {
- ValueExpression prefix = new Constant(c.getStaticType(), str.substring(0, i), SyntheticLocation.INSTANCE);
+ Constant prefix = new Constant(c.getStaticType(), str.substring(0, i), SyntheticLocation.INSTANCE);
result.add(prefix);
}
@@ -649,15 +713,15 @@ private static Set getPrefix(
* @param c Constant to analyze
* @return The set containing the suffixes of a Constant
*/
- private static Set getSuffix(
+ private static Set getSuffix(
Constant c) {
- Set result = new HashSet<>();
+ Set result = new HashSet<>();
String str = c.getValue() instanceof String ? (String) c.getValue() : c.getValue().toString();
int length = str.length();
// Iterate over the length
for (int i = 1; i <= length; i++) {
- ValueExpression suffix = new Constant(c.getStaticType(), str.substring(length - i, length),
+ Constant suffix = new Constant(c.getStaticType(), str.substring(length - i, length),
SyntheticLocation.INSTANCE);
result.add(suffix);
@@ -674,7 +738,7 @@ private static Set getSuffix(
* the list.
*/
private static SymbolicExpression composeExpression(
- List expressions) {
+ List expressions) {
if (expressions.size() == 1)
return expressions.get(0);
@@ -703,16 +767,16 @@ protected SubstringDomain add(
// Don't add the expressions that contain the key variable (ex: x -> x,
// x -> x + y will not be added)
- Set expressionsToRemove = new HashSet<>();
+ Set expressionsToAdd = new HashSet<>();
for (SymbolicExpression se : exprs) {
if (!appears(id, se))
- expressionsToRemove.add(se);
+ expressionsToAdd.add(se);
}
- if (expressionsToRemove.isEmpty())
+ if (expressionsToAdd.isEmpty())
return this;
- ExpressionInverseSet newSet = new ExpressionInverseSet(expressionsToRemove);
+ ExpressionInverseSet newSet = new ExpressionInverseSet(expressionsToAdd);
if (!(newFunction.get(id) == null))
newSet = newSet.glb(newFunction.get(id));
@@ -721,6 +785,16 @@ protected SubstringDomain add(
return mk(lattice, newFunction);
}
+
+ protected SubstringDomain add(
+ SymbolicExpression expr,
+ Identifier id)
+ throws SemanticException {
+ Set expression = new HashSet<>();
+ expression.add(expr);
+
+ return add(expression, id);
+ }
/*
* First step of assignment, removing obsolete relations.
@@ -743,19 +817,24 @@ private SubstringDomain remove(
// Remove relations containing id from the other entries
for (Map.Entry entry : newFunction.entrySet()) {
- Set newSet = entry.getValue().elements.stream()
- .filter(element -> !appears(id, element))
- .collect(Collectors.toSet());
-
- ExpressionInverseSet value = newSet.isEmpty() ? new ExpressionInverseSet().top()
- : new ExpressionInverseSet(newSet);
-
- entry.setValue(value);
+ ExpressionInverseSet newSet = removeFromSet(entry.getValue(), id);
+ entry.setValue(newSet);
}
return mk(lattice, newFunction);
}
+
+ /*
+ * Returns a set without expressions containing id starting from source
+ */
+ private static ExpressionInverseSet removeFromSet(ExpressionInverseSet source, Identifier id){
+ Set newSet = source.elements.stream()
+ .filter(element -> !appears(id, element))
+ .collect(Collectors.toSet());
+
+ return newSet.isEmpty() ? new ExpressionInverseSet().top() : new ExpressionInverseSet(newSet);
+ }
/**
* Performs the inter-assignment phase
@@ -863,31 +942,14 @@ protected SubstringDomain closure() throws SemanticException {
}
- /*
- * Removes values mapped to empty set (top)
- * @return A copy of the domain without variables mapped to empty set
- * @throws SemanticException
- */
private SubstringDomain clear() throws SemanticException {
- SubstringDomain result = mk(lattice, mkNewFunction(function, false));
-
- Map iterate = mkNewFunction(result.function, false);
- for (Map.Entry entry : iterate.entrySet()) {
- if (entry.getValue().isTop()) {
- result = result.forgetIdentifier(entry.getKey());
- }
+ Map newMap = mkNewFunction(function, false);
- }
+ newMap.entrySet().removeIf(entry -> entry.getValue().isTop());
- return result;
+ return new SubstringDomain(lattice, newMap);
}
- /*
- * Checks if a variable appears in an expression
- * @param id Variable to check
- * @param expr expression to analyze
- * @return {@code true} if {@code id} appears, {@code false} otherwise
- */
private static boolean appears(
Identifier id,
SymbolicExpression expr) {
@@ -906,7 +968,6 @@ private static boolean appears(
}
return false;
-
}
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomainWithConstants.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomainWithConstants.java
index d5ec5613e..d43232f6d 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomainWithConstants.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomainWithConstants.java
@@ -20,7 +20,7 @@
* in
* this paper.
*
- * @author Michele
+ * @author Michele
* Martelli
* @author Vincenzo Arceri
*/
@@ -66,11 +66,7 @@ public SubstringDomainWithConstants assign(
continue;
if (elem.getValue().equals(compare)) {
- Set add = new HashSet<>();
- add.add(elem.getKey());
- add.add(id);
-
- b = b.add(add, id).add(add, elem.getKey()).closure();
+ b = b.add(elem.getKey(), id).add(id, elem.getKey()).closure();
}
}
}
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SubstringDomainTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SubstringDomainTest.java
index af6583b44..4d02cc182 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SubstringDomainTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SubstringDomainTest.java
@@ -9,11 +9,13 @@
import it.unive.lisa.analysis.lattices.Satisfiability;
import it.unive.lisa.program.SyntheticLocation;
import it.unive.lisa.program.type.BoolType;
+import it.unive.lisa.program.type.Int16Type;
import it.unive.lisa.program.type.StringType;
import it.unive.lisa.symbolic.SymbolicExpression;
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.TernaryExpression;
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.symbolic.value.Variable;
import it.unive.lisa.symbolic.value.operator.binary.LogicalAnd;
@@ -23,6 +25,9 @@
import it.unive.lisa.symbolic.value.operator.binary.StringEndsWith;
import it.unive.lisa.symbolic.value.operator.binary.StringEquals;
import it.unive.lisa.symbolic.value.operator.binary.StringStartsWith;
+import it.unive.lisa.symbolic.value.operator.ternary.StringReplace;
+import it.unive.lisa.symbolic.value.operator.ternary.StringSubstring;
+
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
@@ -922,4 +927,72 @@ public void testLub5() throws SemanticException {
assertEquals(lub, BOTTOM);
}
+
+ @Test
+ public void testExtr1() throws SemanticException {
+ ValueExpression replaceYAC = new TernaryExpression(StringType.INSTANCE, y, a, c, StringReplace.INSTANCE, SyntheticLocation.INSTANCE);
+
+ ValueExpression ABConcatX = new BinaryExpression(StringType.INSTANCE, ab, x, StringConcat.INSTANCE,
+ SyntheticLocation.INSTANCE);
+ ValueExpression BConcatX = new BinaryExpression(StringType.INSTANCE, b, x, StringConcat.INSTANCE,
+ SyntheticLocation.INSTANCE);
+
+ ValueExpression assignExpr = new BinaryExpression(StringType.INSTANCE, replaceYAC, ABConcatX, StringConcat.INSTANCE, SyntheticLocation.INSTANCE);
+
+ SubstringDomain result = domainE.assign(z, assignExpr, null, null);
+
+ assertTrue(result.getState(z).contains(ABConcatX));
+ assertTrue(result.getState(z).contains(BConcatX));
+
+ }
+
+ @Test
+ public void testExtr2() throws SemanticException {
+ ValueExpression cb = new Constant(StringType.INSTANCE, "cb", SyntheticLocation.INSTANCE);
+
+ ValueExpression replaceCbCA = new TernaryExpression(StringType.INSTANCE, cb, c, a, StringReplace.INSTANCE, SyntheticLocation.INSTANCE);
+
+ ValueExpression assignExpr = new BinaryExpression(StringType.INSTANCE, replaceCbCA, c, StringConcat.INSTANCE, SyntheticLocation.INSTANCE);
+
+ SubstringDomain result = new SubstringDomain().assign(x, assignExpr, null, null);
+
+ assertTrue(result.getState(x).contains(abc));
+ }
+
+ @Test
+ public void testExtr3() throws SemanticException {
+ ValueExpression zero = new Constant(Int16Type.INSTANCE, 0, SyntheticLocation.INSTANCE);
+ ValueExpression two = new Constant(Int16Type.INSTANCE, 2, SyntheticLocation.INSTANCE);
+ ValueExpression substringAbc02 = new TernaryExpression(StringType.INSTANCE, abc, zero, two, StringSubstring.INSTANCE, SyntheticLocation.INSTANCE);
+
+ ValueExpression assignExpr = new BinaryExpression(StringType.INSTANCE, substringAbc02, c, StringConcat.INSTANCE, SyntheticLocation.INSTANCE);
+
+ SubstringDomain result = new SubstringDomain().assign(x, assignExpr, null, null);
+
+ assertTrue(result.getState(x).contains(abc));
+ }
+
+ @Test
+ public void testExtr4() throws SemanticException {
+ ValueExpression replaceXCA = new TernaryExpression(StringType.INSTANCE, x, c, a, StringReplace.INSTANCE, SyntheticLocation.INSTANCE);
+
+ ValueExpression assignExpr = new BinaryExpression(StringType.INSTANCE, replaceXCA, c, StringConcat.INSTANCE, SyntheticLocation.INSTANCE);
+
+ SubstringDomain result = new SubstringDomain().assign(x, assignExpr, null, null);
+
+ assertTrue(result.getState(x).contains(c));
+ }
+
+ @Test
+ public void testExtr5() throws SemanticException {
+ ValueExpression zero = new Constant(Int16Type.INSTANCE, 0, SyntheticLocation.INSTANCE);
+ ValueExpression two = new Constant(Int16Type.INSTANCE, 2, SyntheticLocation.INSTANCE);
+ ValueExpression substringY02 = new TernaryExpression(StringType.INSTANCE, y, zero, two, StringSubstring.INSTANCE, SyntheticLocation.INSTANCE);
+
+ ValueExpression assignExpr = new BinaryExpression(StringType.INSTANCE, substringY02, c, StringConcat.INSTANCE, SyntheticLocation.INSTANCE);
+
+ SubstringDomain result = new SubstringDomain().assign(x, assignExpr, null, null);
+
+ assertTrue(result.getState(x).contains(c));
+ }
}
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/StringAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/StringAnalysesTest.java
index 37ad7e412..eeb2f0a67 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/StringAnalysesTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/StringAnalysesTest.java
@@ -12,6 +12,8 @@
import it.unive.lisa.analysis.string.bricks.Bricks;
import it.unive.lisa.analysis.string.fsa.FSA;
import it.unive.lisa.analysis.string.tarsis.Tarsis;
+import it.unive.lisa.conf.LiSAConfiguration.GraphType;
+
import org.junit.Test;
public class StringAnalysesTest extends AnalysisTestExecutor {