diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json index a9c0898ea..847b6c655 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_A.foo(A__this).json", "untyped_B.foo(B__this).json", "untyped_tests.subtyping(tests__this).json" ], "info" : { "cfgs" : "3", - "duration" : "55ms", - "end" : "2023-09-27T12:48:20.804+02:00", + "duration" : "411ms", + "end" : "2023-10-25T15:03:57.903+02:00", "expressions" : "11", "files" : "3", "globals" : "0", "members" : "3", "programs" : "1", - "start" : "2023-09-27T12:48:20.749+02:00", + "start" : "2023-10-25T15:03:57.492+02:00", "statements" : "8", "units" : "3", "version" : "0.1b8", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_A.foo(A__this).json b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_A.foo(A__this).json index 64f05eaef..c08b83de5 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_A.foo(A__this).json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_A.foo(A__this).json @@ -1 +1 @@ -{"name":"untyped A::foo(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"return 1"},{"id":1,"text":"1"}],"edges":[],"descriptions":[{"nodeId":0,"description":{"expressions":["ret_value@foo"],"state":{"heap":"monolith","type":{"ret_value@foo":["int32"],"this":["A*"]},"value":{"ret_value@foo":"+"}}}},{"nodeId":1,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["A*"]},"value":"#TOP#"}}}]} \ No newline at end of file +{"name":"untyped A::foo(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"return 1"},{"id":1,"text":"1"}],"edges":[],"descriptions":[{"nodeId":0,"description":{"expressions":["ret_value@foo"],"state":{"heap":"monolith","type":{"ret_value@foo":["int32"],"this":["A*","B*"]},"value":{"ret_value@foo":"+"}}}},{"nodeId":1,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["A*","B*"]},"value":"#TOP#"}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_tests.subtyping(tests__this).json b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_tests.subtyping(tests__this).json index b67f4a41e..8e149a297 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_tests.subtyping(tests__this).json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/CHA/untyped_tests.subtyping(tests__this).json @@ -1 +1 @@ -{"name":"untyped tests::subtyping(tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = new B()"},{"id":1,"text":"a"},{"id":2,"text":"new B()"},{"id":3,"subNodes":[4,5],"text":"b = 0"},{"id":4,"text":"b"},{"id":5,"text":"0"},{"id":6,"subNodes":[7,8],"text":"<(b, 10)"},{"id":7,"text":"b"},{"id":8,"text":"10"},{"id":9,"subNodes":[10,11],"text":"a = new A()"},{"id":10,"text":"a"},{"id":11,"text":"new A()"},{"id":12,"subNodes":[13],"text":"foo(a)"},{"id":13,"text":"a"},{"id":14,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":12,"kind":"FalseEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new B"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["b < 10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":7,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":8,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":9,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":10,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":11,"description":{"expressions":["ref$new A"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":12,"description":{"expressions":["open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11"],"state":"#TOP#"}},{"nodeId":13,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":14,"description":{"expressions":["skip"],"state":"#TOP#"}}]} \ No newline at end of file +{"name":"untyped tests::subtyping(tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = new B()"},{"id":1,"text":"a"},{"id":2,"text":"new B()"},{"id":3,"subNodes":[4,5],"text":"b = 0"},{"id":4,"text":"b"},{"id":5,"text":"0"},{"id":6,"subNodes":[7,8],"text":"<(b, 10)"},{"id":7,"text":"b"},{"id":8,"text":"10"},{"id":9,"subNodes":[10,11],"text":"a = new A()"},{"id":10,"text":"a"},{"id":11,"text":"new A()"},{"id":12,"subNodes":[13],"text":"foo(a)"},{"id":13,"text":"a"},{"id":14,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":12,"kind":"FalseEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new B"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["b < 10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":7,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":8,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":9,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*","B*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":10,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":11,"description":{"expressions":["ref$new A"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":12,"description":{"expressions":["open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11"],"state":"#TOP#"}},{"nodeId":13,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*","B*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":14,"description":{"expressions":["skip"],"state":"#TOP#"}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json index 2785bb11d..8384fca1d 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_A.foo(A__this).json", "untyped_B.foo(B__this).json", "untyped_tests.subtyping(tests__this).json" ], "info" : { "cfgs" : "3", - "duration" : "530ms", - "end" : "2023-09-27T12:48:20.351+02:00", + "duration" : "29ms", + "end" : "2023-10-25T15:03:58.360+02:00", "expressions" : "11", "files" : "3", "globals" : "0", "members" : "3", "programs" : "1", - "start" : "2023-09-27T12:48:19.821+02:00", + "start" : "2023-10-25T15:03:58.331+02:00", "statements" : "8", "units" : "3", "version" : "0.1b8", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_A.foo(A__this).json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_A.foo(A__this).json index 64f05eaef..c08b83de5 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_A.foo(A__this).json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_A.foo(A__this).json @@ -1 +1 @@ -{"name":"untyped A::foo(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"return 1"},{"id":1,"text":"1"}],"edges":[],"descriptions":[{"nodeId":0,"description":{"expressions":["ret_value@foo"],"state":{"heap":"monolith","type":{"ret_value@foo":["int32"],"this":["A*"]},"value":{"ret_value@foo":"+"}}}},{"nodeId":1,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["A*"]},"value":"#TOP#"}}}]} \ No newline at end of file +{"name":"untyped A::foo(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"return 1"},{"id":1,"text":"1"}],"edges":[],"descriptions":[{"nodeId":0,"description":{"expressions":["ret_value@foo"],"state":{"heap":"monolith","type":{"ret_value@foo":["int32"],"this":["A*","B*"]},"value":{"ret_value@foo":"+"}}}},{"nodeId":1,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["A*","B*"]},"value":"#TOP#"}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_tests.subtyping(tests__this).json b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_tests.subtyping(tests__this).json index b67f4a41e..8e149a297 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_tests.subtyping(tests__this).json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/RTA/untyped_tests.subtyping(tests__this).json @@ -1 +1 @@ -{"name":"untyped tests::subtyping(tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = new B()"},{"id":1,"text":"a"},{"id":2,"text":"new B()"},{"id":3,"subNodes":[4,5],"text":"b = 0"},{"id":4,"text":"b"},{"id":5,"text":"0"},{"id":6,"subNodes":[7,8],"text":"<(b, 10)"},{"id":7,"text":"b"},{"id":8,"text":"10"},{"id":9,"subNodes":[10,11],"text":"a = new A()"},{"id":10,"text":"a"},{"id":11,"text":"new A()"},{"id":12,"subNodes":[13],"text":"foo(a)"},{"id":13,"text":"a"},{"id":14,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":12,"kind":"FalseEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new B"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["b < 10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":7,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":8,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":9,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":10,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":11,"description":{"expressions":["ref$new A"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":12,"description":{"expressions":["open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11"],"state":"#TOP#"}},{"nodeId":13,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":14,"description":{"expressions":["skip"],"state":"#TOP#"}}]} \ No newline at end of file +{"name":"untyped tests::subtyping(tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = new B()"},{"id":1,"text":"a"},{"id":2,"text":"new B()"},{"id":3,"subNodes":[4,5],"text":"b = 0"},{"id":4,"text":"b"},{"id":5,"text":"0"},{"id":6,"subNodes":[7,8],"text":"<(b, 10)"},{"id":7,"text":"b"},{"id":8,"text":"10"},{"id":9,"subNodes":[10,11],"text":"a = new A()"},{"id":10,"text":"a"},{"id":11,"text":"new A()"},{"id":12,"subNodes":[13],"text":"foo(a)"},{"id":13,"text":"a"},{"id":14,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":12,"kind":"FalseEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new B"],"state":{"heap":"monolith","type":{"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":4,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"a":["B*"],"heap[w]:heap":["B"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["b < 10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":7,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":8,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"a":["B*"],"b":["int32"],"heap[w]:heap":["B"]},"value":{"b":"0"}}}},{"nodeId":9,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*","B*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":10,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":11,"description":{"expressions":["ref$new A"],"state":{"heap":"monolith","type":{"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":12,"description":{"expressions":["open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11"],"state":"#TOP#"}},{"nodeId":13,"description":{"expressions":["a"],"state":{"heap":"monolith","type":{"a":["A*","B*"],"heap[w]:heap":["A","B"]},"value":"#TOP#"}}},{"nodeId":14,"description":{"expressions":["skip"],"state":"#TOP#"}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java index d18c636ef..9ec46a304 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java @@ -72,6 +72,13 @@ public MonolithicHeap mk( return TOP; } + @Override + public MonolithicHeap mk( + MonolithicHeap reference, + List replacements) { + return TOP; + } + @Override public MonolithicHeap semanticsOf( HeapExpression expression, diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java index d9282a1a5..36249a0a5 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java @@ -146,7 +146,14 @@ public List getSubstitution() { @Override public TypeBasedHeap mk( TypeBasedHeap reference) { - return this; + return new TypeBasedHeap(reference.names); + } + + @Override + public TypeBasedHeap mk( + TypeBasedHeap reference, + List replacements) { + return new TypeBasedHeap(reference.names); } @Override diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java index aa7c44fab..a6dc81e94 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java @@ -92,35 +92,19 @@ public AllocationSiteBasedAnalysis( this.replacements = replacements.isEmpty() ? Collections.emptyList() : replacements; } - @Override - public A mk( - A reference) { - return mk(reference.heapEnv, Collections.emptyList()); - } - - /** - * Builds a new instance of this class given its components. - * - * @param heapEnv the heap environment that this instance tracks - * - * @return the new instance - */ - protected A mk( - HeapEnvironment heapEnv) { - return mk(heapEnv, Collections.emptyList()); - } - /** - * Builds a new instance of this class given its components. + * Builds a new instance of this class by copying abstract information from + * {@code reference} and using the given environment for storing points-to + * information. * - * @param heapEnv the heap environment that this instance tracks - * @param replacements the heap replacements of this instance + * @param reference the domain whose abstract information needs to be copied + * @param heapEnv the heap environment that this instance tracks * * @return the new instance */ protected abstract A mk( - HeapEnvironment heapEnv, - List replacements); + A reference, + HeapEnvironment heapEnv); @Override public A assign( @@ -146,7 +130,7 @@ public A assign( // so that x and y become aliases Identifier lhs_ref = ((MemoryPointer) id).getReferencedLocation(); HeapEnvironment heap = sss.heapEnv.assign(lhs_ref, rhs_ref, pp, oracle); - result = result.lub(mk(heap)); + result = result.lub(mk(sss, heap)); } else if (rhs_ref instanceof StackAllocationSite && !getAllocatedAt(((StackAllocationSite) rhs_ref).getLocationName()).isEmpty()) // for stack elements, assignment works as a shallow copy @@ -155,12 +139,12 @@ public A assign( else { // aliasing: id and star_y points to the same object HeapEnvironment heap = sss.heapEnv.assign(id, rhs_ref, pp, oracle); - result = result.lub(mk(heap)); + result = result.lub(mk(sss, heap)); } } else result = result.lub(sss); - return mk(result.heapEnv, replacements); + return mk(result, replacements); } /** @@ -199,6 +183,7 @@ protected Set getAllocatedAt( * * @throws SemanticException if something goes wrong during the analysis */ + @SuppressWarnings("unchecked") public A shallowCopy( Identifier id, StackAllocationSite site, @@ -218,7 +203,7 @@ public A shallowCopy( replacement.addTarget(site); replacements.add(replacement); - return mk(tmp); + return mk((A) this, tmp); } @Override diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java index 4ceed70d7..368bf3736 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java @@ -39,7 +39,7 @@ public class FieldSensitivePointBasedHeap extends AllocationSiteBasedAnalysis fields; + public final GenericMapLattice fields; /** * Builds a new instance of field-sensitive point-based heap. @@ -93,10 +93,23 @@ public FieldSensitivePointBasedHeap( } @Override - protected FieldSensitivePointBasedHeap mk( - HeapEnvironment heapEnv, + public FieldSensitivePointBasedHeap mk( + FieldSensitivePointBasedHeap reference) { + return reference; + } + + @Override + public FieldSensitivePointBasedHeap mk( + FieldSensitivePointBasedHeap reference, List replacements) { - return new FieldSensitivePointBasedHeap(heapEnv, replacements, fields); + return new FieldSensitivePointBasedHeap(reference.heapEnv, replacements, reference.fields); + } + + @Override + protected FieldSensitivePointBasedHeap mk( + FieldSensitivePointBasedHeap reference, + HeapEnvironment heapEnv) { + return new FieldSensitivePointBasedHeap(heapEnv, reference.replacements, reference.fields); } @Override @@ -144,7 +157,7 @@ public FieldSensitivePointBasedHeap shallowCopy( replacement.addTarget(site); replacements.add(replacement); - return new FieldSensitivePointBasedHeap(heap, new GenericMapLattice<>(fields.lattice, newFields)); + return mk(new FieldSensitivePointBasedHeap(heap, new GenericMapLattice<>(fields.lattice, newFields))); } @Override @@ -184,8 +197,8 @@ public FieldSensitivePointBasedHeap smallStepSemantics( addField(site, child, mapping); } - return new FieldSensitivePointBasedHeap(heapEnv, heapEnv.getSubstitution(), - new GenericMapLattice<>(fields.lattice, mapping)); + return mk(new FieldSensitivePointBasedHeap(heapEnv, heapEnv.getSubstitution(), + new GenericMapLattice<>(fields.lattice, mapping))); } else if (expression instanceof MemoryAllocation) { String loc = expression.getCodeLocation().getCodeLocation(); Set alreadyAllocated = getAllocatedAt(loc); @@ -232,12 +245,12 @@ public FieldSensitivePointBasedHeap smallStepSemantics( env = new HeapEnvironment<>(env.lattice, map); } - return new FieldSensitivePointBasedHeap(env, replacements, fields); + return mk(new FieldSensitivePointBasedHeap(env, replacements, fields)); } } FieldSensitivePointBasedHeap sss = super.smallStepSemantics(expression, pp, oracle); - return new FieldSensitivePointBasedHeap(sss.heapEnv, fields); + return mk(new FieldSensitivePointBasedHeap(sss.heapEnv, fields)); } private void addField( @@ -373,19 +386,19 @@ public boolean equals( public FieldSensitivePointBasedHeap popScope( ScopeToken scope) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.popScope(scope), fields); + return mk(new FieldSensitivePointBasedHeap(heapEnv.popScope(scope), fields)); } @Override public FieldSensitivePointBasedHeap pushScope( ScopeToken scope) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.pushScope(scope), fields); + return mk(new FieldSensitivePointBasedHeap(heapEnv.pushScope(scope), fields)); } @Override public FieldSensitivePointBasedHeap top() { - return new FieldSensitivePointBasedHeap(heapEnv.top(), Collections.emptyList(), fields.top()); + return mk(new FieldSensitivePointBasedHeap(heapEnv.top(), Collections.emptyList(), fields.top())); } @Override @@ -395,7 +408,7 @@ public boolean isTop() { @Override public FieldSensitivePointBasedHeap bottom() { - return new FieldSensitivePointBasedHeap(heapEnv.bottom(), Collections.emptyList(), fields.bottom()); + return mk(new FieldSensitivePointBasedHeap(heapEnv.bottom(), Collections.emptyList(), fields.bottom())); } @Override @@ -407,18 +420,18 @@ public boolean isBottom() { public FieldSensitivePointBasedHeap lubAux( FieldSensitivePointBasedHeap other) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.lub(other.heapEnv), + return mk(new FieldSensitivePointBasedHeap(heapEnv.lub(other.heapEnv), Collections.emptyList(), - fields.lub(other.fields)); + fields.lub(other.fields))); } @Override public FieldSensitivePointBasedHeap glbAux( FieldSensitivePointBasedHeap other) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.glb(other.heapEnv), + return mk(new FieldSensitivePointBasedHeap(heapEnv.glb(other.heapEnv), Collections.emptyList(), - fields.glb(other.fields)); + fields.glb(other.fields))); } @Override @@ -432,13 +445,13 @@ public boolean lessOrEqualAux( public FieldSensitivePointBasedHeap forgetIdentifier( Identifier id) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.forgetIdentifier(id), fields); + return mk(new FieldSensitivePointBasedHeap(heapEnv.forgetIdentifier(id), fields)); } @Override public FieldSensitivePointBasedHeap forgetIdentifiersIf( Predicate test) throws SemanticException { - return new FieldSensitivePointBasedHeap(heapEnv.forgetIdentifiersIf(test), fields); + return mk(new FieldSensitivePointBasedHeap(heapEnv.forgetIdentifiersIf(test), fields)); } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java index 5d49b4f55..5f2bc5f2f 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java @@ -52,20 +52,33 @@ public PointBasedHeap( } @Override - protected PointBasedHeap mk( - HeapEnvironment heapEnv, + public PointBasedHeap mk( + PointBasedHeap reference) { + return reference; + } + + @Override + public PointBasedHeap mk( + PointBasedHeap reference, List replacements) { - return new PointBasedHeap(heapEnv, replacements); + return new PointBasedHeap(reference.heapEnv, replacements); + } + + @Override + protected PointBasedHeap mk( + PointBasedHeap reference, + HeapEnvironment heapEnv) { + return new PointBasedHeap(heapEnv, reference.replacements); } @Override public PointBasedHeap top() { - return new PointBasedHeap(heapEnv.top()); + return mk(new PointBasedHeap(heapEnv.top())); } @Override public PointBasedHeap bottom() { - return new PointBasedHeap(heapEnv.bottom()); + return mk(new PointBasedHeap(heapEnv.bottom())); } @Override @@ -77,14 +90,14 @@ public List getSubstitution() { public PointBasedHeap lubAux( PointBasedHeap other) throws SemanticException { - return new PointBasedHeap(heapEnv.lub(other.heapEnv)); + return mk(new PointBasedHeap(heapEnv.lub(other.heapEnv))); } @Override public PointBasedHeap glbAux( PointBasedHeap other) throws SemanticException { - return new PointBasedHeap(heapEnv.glb(other.heapEnv)); + return mk(new PointBasedHeap(heapEnv.glb(other.heapEnv))); } @Override @@ -98,27 +111,27 @@ public boolean lessOrEqualAux( public PointBasedHeap popScope( ScopeToken scope) throws SemanticException { - return new PointBasedHeap(heapEnv.popScope(scope)); + return mk(new PointBasedHeap(heapEnv.popScope(scope))); } @Override public PointBasedHeap pushScope( ScopeToken scope) throws SemanticException { - return new PointBasedHeap(heapEnv.pushScope(scope)); + return mk(new PointBasedHeap(heapEnv.pushScope(scope))); } @Override public PointBasedHeap forgetIdentifier( Identifier id) throws SemanticException { - return new PointBasedHeap(heapEnv.forgetIdentifier(id)); + return mk(new PointBasedHeap(heapEnv.forgetIdentifier(id))); } @Override public PointBasedHeap forgetIdentifiersIf( Predicate test) throws SemanticException { - return new PointBasedHeap(heapEnv.forgetIdentifiersIf(test)); + return mk(new PointBasedHeap(heapEnv.forgetIdentifiersIf(test))); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java index cc71a3c85..736626be6 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java @@ -19,6 +19,7 @@ import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; import java.util.HashSet; +import java.util.List; import java.util.Set; /** @@ -84,9 +85,25 @@ default H smallStepSemantics( * * @return a new instance of this domain */ - public abstract H mk( + H mk( H reference); + /** + * Creates a new instance of this domain containing the same abstract + * information of reference. The returned object is effectively a new + * instance, but with the given substitution. If this domain does not apply + * substitutions, it is fine to return {@code this}. + * + * @param reference the domain whose abstract information needs to be + * copied + * @param replacements the heap replacements of this instance + * + * @return the new instance + */ + H mk( + H reference, + List replacements); + @Override @SuppressWarnings("unchecked") default H pushScope( diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/ReferenceType.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/ReferenceType.java index 82df53388..e7f67f5fd 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/ReferenceType.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/ReferenceType.java @@ -1,6 +1,6 @@ package it.unive.lisa.type; -import java.util.Collections; +import java.util.HashSet; import java.util.Set; /** @@ -30,19 +30,29 @@ public ReferenceType( @Override public boolean canBeAssignedTo( Type other) { - return other instanceof PointerType || other.isUntyped(); + return other instanceof ReferenceType && getInnerType().canBeAssignedTo(other.asReferenceType().getInnerType()) + || other.isUntyped(); } @Override public Type commonSupertype( Type other) { - return equals(other) ? this : Untyped.INSTANCE; + if (equals(other)) + return this; + else if (other instanceof ReferenceType) + return new ReferenceType(getInnerType().commonSupertype(other.asReferenceType().getInnerType())); + + return Untyped.INSTANCE; } @Override public Set allInstances( TypeSystem types) { - return Collections.singleton(this); + Set instances = new HashSet<>(); + for (Type inner : getInnerType().allInstances(types)) + instances.add(new ReferenceType(inner)); + instances.add(this); + return instances; } @Override