Skip to content

Commit

Permalink
Fixed StringReplace and Substring expressions in extraction
Browse files Browse the repository at this point in the history
  • Loading branch information
@michelemartelli2002
michelemartelli2002 committed Jun 22, 2024
1 parent 654f1fb commit 710ba7d
Show file tree
Hide file tree
Showing 13 changed files with 331 additions and 171 deletions.
26 changes: 24 additions & 2 deletions lisa/lisa-analyses/imp-testcases/string/strings-subs.imp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,8 @@ class strings {
def z = "b";
def w = y + z;
}



paper2(){
def x = "";
def y = "";
Expand All @@ -114,7 +115,6 @@ class strings {
x = y + "c";
}


paper3(x){
def v = "";
if (x % 2)
Expand Down Expand Up @@ -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";
}


}
6 changes: 3 additions & 3 deletions lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
18 changes: 9 additions & 9 deletions lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json
View file
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
2 changes: 1 addition & 1 deletion ...lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json
View file
Original file line number Diff line number Diff line change
@@ -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\""]}}}}]}
{"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"]}}}}]}
1 change: 1 addition & 0 deletions ...isa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace(strings__this).json
View file
Original file line number Diff line number Diff line change
@@ -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"]}}}}]}
Loading

0 comments on commit 710ba7d

Please sign in to comment.