Merge pull request #306 from michelemartelli2002/strings-domains

Substring relational domains

.gitignore

@@ -0,0 +1,3 @@
+/.metadata/
+/.metadata/
+.DS_Store

lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json

@@ -0,0 +1,38 @@
+{
+  "warnings" : [ ],
+  "files" : [ "report.json", "untyped_strings.constants(strings__this).json", "untyped_strings.replace(strings__this,_untyped_s).json", "untyped_strings.replace2(strings__this).json", "untyped_strings.replace3(strings__this).json", "untyped_strings.replace4(strings__this).json" ],
+  "info" : {
+    "cfgs" : "5",
+    "duration" : "16ms",
+    "end" : "2024-06-25T19:08:32.428+02:00",
+    "expressions" : "72",
+    "files" : "5",
+    "globals" : "0",
+    "members" : "5",
+    "programs" : "1",
+    "start" : "2024-06-25T19:08:32.412+02:00",
+    "statements" : "24",
+    "units" : "1",
+    "version" : "0.1b9",
+    "warnings" : "0"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/string/subs-domain-constants"
+  }
+}

lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/strings-subs-constants.imp

@@ -0,0 +1,37 @@
+class strings {
+
+	constants(){
+		def x = "ab";
+		def y = "a";
+		def z = "b";
+		def w = y + z;
+	}
+
+	replace(s){
+		def x = "aaaaa";
+		def y = "bba";
+		def k = "bb" + "a";
+		def z = strrep(x, "aa", "b");
+
+		if (streq(s, k))
+			def i = 1 + 1;
+	}
+
+	replace2(){
+		def y = "xyz";
+		def x = "a" + strrep(y, "x", "z") + "c";
+	}
+
+	replace3(){
+		def y = "xyz";
+		def z = "w";
+    	def x = "ab" + strrep(z + y, "x", "yz") + "c";
+	}
+
+	replace4(){
+		def k = "z";
+		def x = "abc" + k;
+		def y = "abc";
+		def z = "a" + strrep(y, "abc", "b") + "c";
+	}
+}

lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/untyped_strings.constants(strings__this).json

@@ -0,0 +1 @@
+{"name":"untyped strings::constants(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"ab\""},{"id":1,"text":"x"},{"id":2,"text":"\"ab\""},{"id":3,"subNodes":[4,5],"text":"y = \"a\""},{"id":4,"text":"y"},{"id":5,"text":"\"a\""},{"id":6,"subNodes":[7,8],"text":"z = \"b\""},{"id":7,"text":"z"},{"id":8,"text":"\"b\""},{"id":9,"subNodes":[10,11],"text":"w = +(y, z)"},{"id":10,"text":"w"},{"id":11,"subNodes":[12,13],"text":"+(y, z)"},{"id":12,"text":"y"},{"id":13,"text":"z"},{"id":14,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":[{"x":"ab"},{"x":["\"a\"","\"ab\"","\"b\""]}]}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":["#TOP#","#TOP#"]}}},{"nodeId":2,"description":{"expressions":["\"ab\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":["#TOP#","#TOP#"]}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":[{"x":"ab","y":"a"},{"x":["\"a\"","\"ab\"","\"b\"","y"],"y":["\"a\""]}]}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":[{"x":"ab"},{"x":["\"a\"","\"ab\"","\"b\""]}]}}},{"nodeId":5,"description":{"expressions":["\"a\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":[{"x":"ab"},{"x":["\"a\"","\"ab\"","\"b\""]}]}}},{"nodeId":6,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"x":"ab","y":"a","z":"b"},{"x":["\"a\"","\"ab\"","\"b\"","y","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":7,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":[{"x":"ab","y":"a"},{"x":["\"a\"","\"ab\"","\"b\"","y"],"y":["\"a\""]}]}}},{"nodeId":8,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":[{"x":"ab","y":"a"},{"x":["\"a\"","\"ab\"","\"b\"","y"],"y":["\"a\""]}]}}},{"nodeId":9,"description":{"expressions":["w"],"state":{"heap":"monolith","type":{"this":["strings*"],"w":["string"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"w":"ab","x":"ab","y":"a","z":"b"},{"w":["\"a\"","\"ab\"","\"b\"","x","y","y strcat z","z"],"x":["\"a\"","\"ab\"","\"b\"","w","y","y strcat z","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":10,"description":{"expressions":["w"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"x":"ab","y":"a","z":"b"},{"x":["\"a\"","\"ab\"","\"b\"","y","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":11,"description":{"expressions":["y strcat z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"x":"ab","y":"a","z":"b"},{"x":["\"a\"","\"ab\"","\"b\"","y","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":12,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"x":"ab","y":"a","z":"b"},{"x":["\"a\"","\"ab\"","\"b\"","y","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":13,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"x":"ab","y":"a","z":"b"},{"x":["\"a\"","\"ab\"","\"b\"","y","z"],"y":["\"a\""],"z":["\"b\""]}]}}},{"nodeId":14,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"w":["string"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"w":"ab","x":"ab","y":"a","z":"b"},{"w":["\"a\"","\"ab\"","\"b\"","x","y","y strcat z","z"],"x":["\"a\"","\"ab\"","\"b\"","w","y","y strcat z","z"],"y":["\"a\""],"z":["\"b\""]}]}}}]}

lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/untyped_strings.replace(strings__this,_untyped_s).json

@@ -0,0 +1 @@
+{"name":"untyped strings::replace(strings* this, untyped s)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"aaaaa\""},{"id":1,"text":"x"},{"id":2,"text":"\"aaaaa\""},{"id":3,"subNodes":[4,5],"text":"y = \"bba\""},{"id":4,"text":"y"},{"id":5,"text":"\"bba\""},{"id":6,"subNodes":[7,8],"text":"k = +(\"bb\", \"a\")"},{"id":7,"text":"k"},{"id":8,"subNodes":[9,10],"text":"+(\"bb\", \"a\")"},{"id":9,"text":"\"bb\""},{"id":10,"text":"\"a\""},{"id":11,"subNodes":[12,13],"text":"z = replace(x, \"aa\", \"b\")"},{"id":12,"text":"z"},{"id":13,"subNodes":[14,15,16],"text":"replace(x, \"aa\", \"b\")"},{"id":14,"text":"x"},{"id":15,"text":"\"aa\""},{"id":16,"text":"\"b\""},{"id":17,"subNodes":[18,19],"text":"equals(s, k)"},{"id":18,"text":"s"},{"id":19,"text":"k"},{"id":20,"subNodes":[21,22],"text":"i = +(1, 1)"},{"id":21,"text":"i"},{"id":22,"subNodes":[23,24],"text":"+(1, 1)"},{"id":23,"text":"1"},{"id":24,"text":"1"},{"id":25,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":20,"kind":"TrueEdge"},{"sourceId":17,"destId":25,"kind":"FalseEdge"},{"sourceId":20,"destId":25,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"]},"value":[{"s":"#TOP#","x":"aaaaa"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""]}]}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"]},"value":[{"s":"#TOP#"},"#TOP#"]}}},{"nodeId":2,"description":{"expressions":["\"aaaaa\""],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"]},"value":[{"s":"#TOP#"},"#TOP#"]}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"s":"#TOP#","x":"aaaaa","y":"bba"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\""]}]}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"]},"value":[{"s":"#TOP#","x":"aaaaa"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""]}]}}},{"nodeId":5,"description":{"expressions":["\"bba\""],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"]},"value":[{"s":"#TOP#","x":"aaaaa"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""]}]}}},{"nodeId":6,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":7,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"s":"#TOP#","x":"aaaaa","y":"bba"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\""]}]}}},{"nodeId":8,"description":{"expressions":["\"bb\" strcat \"a\""],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"s":"#TOP#","x":"aaaaa","y":"bba"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\""]}]}}},{"nodeId":9,"description":{"expressions":["\"bb\""],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"s":"#TOP#","x":"aaaaa","y":"bba"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\""]}]}}},{"nodeId":10,"description":{"expressions":["\"a\""],"state":{"heap":"monolith","type":{"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"s":"#TOP#","x":"aaaaa","y":"bba"},{"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\""]}]}}},{"nodeId":11,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y"]}]}}},{"nodeId":12,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":13,"description":{"expressions":["x strreplace(\"aa\", \"b\")"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":15,"description":{"expressions":["\"aa\""],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":16,"description":{"expressions":["\"b\""],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k"]}]}}},{"nodeId":17,"description":{"expressions":["s strcmp k"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y"]}]}}},{"nodeId":18,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y"]}]}}},{"nodeId":19,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y"]}]}}},{"nodeId":20,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"i":["int32"],"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","s","y","z"],"s":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","y"]}]}}},{"nodeId":21,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","s","y","z"],"s":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","y"]}]}}},{"nodeId":22,"description":{"expressions":["1 + 1"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","s","y","z"],"s":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","y"]}]}}},{"nodeId":23,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","s","y","z"],"s":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","y"]}]}}},{"nodeId":24,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","s","y","z"],"s":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","s","y"]}]}}},{"nodeId":25,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"k":["string"],"s":"#TOP#","this":["strings*"],"x":["string"],"y":["string"],"z":["string"]},"value":[{"k":"bba","s":"#TOP#","x":"aaaaa","y":"bba","z":"bba"},{"k":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","y","z"],"x":["\"a\"","\"aa\"","\"aaa\"","\"aaaa\"","\"aaaaa\""],"y":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","z"],"z":["\"a\"","\"b\"","\"ba\"","\"bb\"","\"bba\"","k","y"]}]}}}]}