Modified abstract domain in global initialization checker #23138
Conversation
EnzeXing
force-pushed
the
global-init-checker-redesign
branch
from
5591de9 to
dbdfe1a
Compare
EnzeXing
changed the title
EnzeXing
force-pushed
the
global-init-checker-redesign
branch
from
dbdfe1a to
7582cf9
Compare
There was a problem hiding this comment.
I like this redesign, great work @EnzeXing 🎉
I left some comments, but I see no issue block the merge given that we expect further PRs coming up soon.
@EnzeXing You can decide which comments to address in this PR and which are left to later PRs.
We can discuss the comment related to Cartesian Product Algorithm in next meeting.
| * ThisValue ::= Ref | vs // possible values for 'this' | ||
| * LocalEnv(meth, ownerObject) // represents environments for methods or functions | ||
| * Scope ::= Ref | LocalEnv | ||
| * ScopeSet ::= Set(Scope) |
There was a problem hiding this comment.
Minor: The name Scope, ScopeSet, and LocalEnv are actually keys to the heap. ScopeBody is not intuitive enough. Better names will help understanding and maintenance.
It's a minor issue (the same for other naming issues mentioned below), we can delay it to a later PR if it's not easy to come up with better names.
| instance.initOuter(klass, outer) | ||
| val owner = State.currentObject | ||
| val instance = new OfClass(klass, owner, ctor, outerScope.level + 1, summon[Regions.Data]) | ||
| instance.initOuter(klass, outerScope) | ||
| instance |
There was a problem hiding this comment.
Minor: I was thinking, given that now we simplied OfClass, maybe we can remove this helper method.
Advantage: the initialization code for the outer will be at the place where we initialize the object, which will be more regular than before.
There was a problem hiding this comment.
I worried about missing the call to initOuter when initializing the object
| given Join[Value] with | ||
| extension (a: Value) | ||
| def join(b: Value): Value = | ||
| assert(!a.isInstanceOf[Package] && !b.isInstanceOf[Package], "Unexpected join between " + a + " and " + b) |
There was a problem hiding this comment.
For future: If Package causes troubles and is not essential, we could simply remove it from the abstract domain.
There was a problem hiding this comment.
Agreed. Package led to many edge cases where we have to report internal errors.
| if sym.is(Flags.Lazy) then | ||
| val rhs = sym.defTree.asInstanceOf[ValDef].rhs | ||
| eval(rhs, thisV, sym.enclosingClass.asClass, cacheResult = true) | ||
| else | ||
| // Assume forward reference check is doing a good job | ||
| val value = Env.valValue(sym) | ||
| val value = scopeSet.scopes.map(_.varValue(sym)).join |
There was a problem hiding this comment.
For future: Might be good to define a helper method in scopeSet to hide the abstract domain details from the semantic logic. It will be more robust to refactoring changes.
| given State.Data = new State.Data | ||
| given Trace = Trace.empty | ||
| given Heap.MutableData = Heap.empty |
There was a problem hiding this comment.
Given that now the heap is shared globally, maybe add a TODO to do garbage collection on the heap.
| recur(scopeSet.scopes.map(_.outer).join) | ||
| else | ||
| recur(scopeSet.scopes.map(_.outer).join) | ||
| end recur |
There was a problem hiding this comment.
For future: if possible, try to hide abstract domain details from the semantic logic. That would make the code more robust against refactoring and easier to understand.
| if scopes.isEmpty then | ||
| Env.NoEnv | ||
| else | ||
| scopes.reduce { (s1, s2) => s1.join(s2) } |
There was a problem hiding this comment.
Nit: Can be more concise by values.foldLeft(Bottom)(_ join _) and scopes.foldLeft(Env.NoEnv)(_ join _)
EnzeXing
force-pushed
the
global-init-checker-redesign
branch
from
2d7916f to
b9922ce
Compare
This PR modifies the abstract domain of the global object initialization checker. It closely follows the abstract definitional interpreter framework, but changes the heap to map from scopes (including abstract objects or local environments) to a pair of
valsMapandoutersMap, both of which over-approximates the information of scope bodies of the concrete scopes they represent.[test_scala2_library_tasty]