Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Propagating field information #294

Merged
merged 7 commits into from
Oct 27, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
Original file line number Diff line number Diff line change
@@ -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#"}}}]}
{"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#"}}}]}
Original file line number Diff line number Diff line change
@@ -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#"}}]}
{"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#"}}]}
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
Original file line number Diff line number Diff line change
@@ -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#"}}}]}
{"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#"}}}]}
Original file line number Diff line number Diff line change
@@ -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#"}}]}
{"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#"}}]}
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,13 @@ public MonolithicHeap mk(
return TOP;
}

@Override
public MonolithicHeap mk(
MonolithicHeap reference,
List<HeapReplacement> replacements) {
return TOP;
}

@Override
public MonolithicHeap semanticsOf(
HeapExpression expression,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,14 @@ public List<HeapReplacement> getSubstitution() {
@Override
public TypeBasedHeap mk(
TypeBasedHeap reference) {
return this;
return new TypeBasedHeap(reference.names);
}

@Override
public TypeBasedHeap mk(
TypeBasedHeap reference,
List<HeapReplacement> replacements) {
return new TypeBasedHeap(reference.names);
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<AllocationSites> 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<AllocationSites> heapEnv,
List<HeapReplacement> replacements);
A reference,
HeapEnvironment<AllocationSites> heapEnv);

@Override
public A assign(
Expand All @@ -146,7 +130,7 @@ public A assign(
// so that x and y become aliases
Identifier lhs_ref = ((MemoryPointer) id).getReferencedLocation();
HeapEnvironment<AllocationSites> 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
Expand All @@ -155,12 +139,12 @@ public A assign(
else {
// aliasing: id and star_y points to the same object
HeapEnvironment<AllocationSites> 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);
}

/**
Expand Down Expand Up @@ -199,6 +183,7 @@ protected Set<AllocationSite> getAllocatedAt(
*
* @throws SemanticException if something goes wrong during the analysis
*/
@SuppressWarnings("unchecked")
public A shallowCopy(
Identifier id,
StackAllocationSite site,
Expand All @@ -218,7 +203,7 @@ public A shallowCopy(
replacement.addTarget(site);
replacements.add(replacement);

return mk(tmp);
return mk((A) this, tmp);
}

@Override
Expand Down
Loading
Loading