From 710ba7de7864fb10ff2391ab3d4037373a0a4f38 Mon Sep 17 00:00:00 2001 From: Michele Date: Sat, 22 Jun 2024 13:17:20 +0200 Subject: [PATCH] Fixed StringReplace and Substring expressions in extraction --- .../imp-testcases/string/strings-subs.imp | 26 +- .../string/subs-domain-constants/report.json | 6 +- .../string/subs-domain/report.json | 18 +- ...untyped_strings.paper2(strings__this).json | 2 +- ...ntyped_strings.replace(strings__this).json | 1 + ...typed_strings.replace2(strings__this).json | 1 + ...yped_strings.substring(strings__this).json | 1 + ...ped_strings.substring2(strings__this).json | 1 + .../string/StringConstantPropagation.java | 4 +- .../lisa/analysis/string/SubstringDomain.java | 359 ++++++++++-------- .../string/SubstringDomainWithConstants.java | 8 +- .../analysis/string/SubstringDomainTest.java | 73 ++++ .../unive/lisa/cron/StringAnalysesTest.java | 2 + 13 files changed, 331 insertions(+), 171 deletions(-) create mode 100644 lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace(strings__this).json create mode 100644 lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.replace2(strings__this).json create mode 100644 lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring(strings__this).json create mode 100644 lisa/lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.substring2(strings__this).json 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 {