-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Refactor the abstract domain of global init checker to compile http4s #22179
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
Changes from 1 commit
637a5f6
7db959e
44ed0b3
bf18e95
f51f91b
fdcb455
7ee0726
6b5d6a4
e72efed
773880f
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
- Loading branch information
There are no files selected for viewing
8000
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -644,6 +644,12 @@ class Objects(using Context @constructorOnly): | |
case (ValueSet(values), b : ValueElement) => ValueSet(values + b) | ||
case (a : ValueElement, b : ValueElement) => ValueSet(ListSet(a, b)) | ||
|
||
def remove(b: Value): Value = (a, b) match | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Are we sure that There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Removing from |
||
case (ValueSet(values1), b: ValueElement) => ValueSet(values1 - b) | ||
case (ValueSet(values1), ValueSet(values2)) => ValueSet(values1.removedAll(values2)) | ||
case (a: Ref, b: Ref) if a.equals(b) => Bottom | ||
case _ => a | ||
|
||
def widen(height: Int)(using Context): Value = | ||
if height == 0 then Cold | ||
else | ||
|
@@ -1386,29 +1392,25 @@ class Objects(using Context @constructorOnly): | |
def getMemberMethod(receiver: Type, name: TermName, tp: Type): Denotation = | ||
receiver.member(name).suchThat(receiver.memberInfo(_) <:< tp) | ||
|
||
def evalCase(caseDef: CaseDef): Value = | ||
evalPattern(scrutinee, caseDef.pat) | ||
eval(caseDef.guard, thisV, klass) | ||
eval(caseDef.body, thisV, klass) | ||
|
||
/** Abstract evaluation of patterns. | ||
* | ||
* It augments the local environment for bound pattern variables. As symbols are globally | ||
* unique, we can put them in a single environment. | ||
* | ||
* Currently, we assume all cases are reachable, thus all patterns are assumed to match. | ||
*/ | ||
def evalPattern(scrutinee: Value, pat: Tree): Value = log("match " + scrutinee.show + " against " + pat.show, printer, (_: Value).show): | ||
def evalPattern(scrutinee: Value, pat: Tree): (Type, Value) = log("match " + scrutinee.show + " against " + pat.show, printer, (_: (Type, Value))._2.show): | ||
val trace2 = Trace.trace.add(pat) | ||
pat match | ||
case Alternative(pats) => | ||
for pat <- pats do evalPattern(scrutinee, pat) | ||
scrutinee | ||
val (types, values) = pats.map(evalPattern(scrutinee, _)).unzip() | ||
val orType = types.fold(defn.NothingType)(OrType(_, _, false)) | ||
(orType, values.join) | ||
|
||
case bind @ Bind(_, pat) => | ||
val value = evalPattern(scrutinee, pat) | ||
val (tpe, value) = evalPattern(scrutinee, pat) | ||
initLocal(bind.symbol, value) | ||
scrutinee | ||
(tpe, value) | ||
|
||
case UnApply(fun, implicits, pats) => | ||
given Trace = trace2 | ||
|
@@ -1417,6 +1419,10 @@ class Objects(using Context @constructorOnly): | |
val funRef = fun1.tpe.asInstanceOf[TermRef] | ||
val unapplyResTp = funRef.widen.finalResultType | ||
|
||
val receiverType = fun1 match | ||
case ident: Ident => funRef.prefix | ||
case select: Select => select.qualifier.tpe | ||
|
||
val receiver = fun1 match | ||
case ident: Ident => | ||
evalType(funRef.prefix, thisV, klass) | ||
|
@@ -1505,17 +1511,18 @@ class Objects(using Context @constructorOnly): | |
end if | ||
end if | ||
end if | ||
scrutinee | ||
(receiverType, scrutinee.filterType(receiverType)) | ||
|
||
case Ident(nme.WILDCARD) | Ident(nme.WILDCARD_STAR) => | ||
scrutinee | ||
(defn.ThrowableType, scrutinee) | ||
|
||
case Typed(pat, _) => | ||
evalPattern(scrutinee, pat) | ||
case Typed(pat, typeTree) => | ||
val (_, value) = evalPattern(scrutinee.filterType(typeTree.tpe), pat) | ||
(typeTree.tpe, value) | ||
|
||
case tree => | ||
// For all other trees, the semantics is normal. | ||
eval(tree, thisV, klass) | ||
(defn.ThrowableType, eval(tree, thisV, klass)) | ||
|
||
end evalPattern | ||
|
||
|
@@ -1539,12 +1546,12 @@ class Objects(using Context @constructorOnly): | |
if isWildcardStarArgList(pats) then | ||
if pats.size == 1 then | ||
// call .toSeq | ||
val toSeqDenot = getMemberMethod(scrutineeType, nme.toSeq, toSeqType(elemType)) | ||
val toSeqDenot = scrutineeType.member(nme.toSeq).suchThat(_.info.isParameterless) | ||
val toSeqRes = call(scrutinee, toSeqDenot.symbol, Nil, scrutineeType, superType = NoType, needResolve = true) | ||
evalPattern(toSeqRes, pats.head) | ||
else | ||
// call .drop | ||
val dropDenot = getMemberMethod(scrutineeType, nme.drop, dropType(elemType)) | ||
val dropDenot = getMemberMethod(scrutineeType, nme.drop, applyType(elemType)) | ||
val dropRes = call(scrutinee, dropDenot.symbol, ArgInfo(Bottom, summon[Trace], EmptyTree) :: Nil, scrutineeType, superType = NoType, needResolve = true) | ||
for pat <- pats.init do evalPattern(applyRes, pat) | ||
evalPattern(dropRes, pats.last) | ||
|
@@ -1555,8 +1562,21 @@ class Objects(using Context @constructorOnly): | |
end if | ||
end evalSeqPatterns | ||
|
||
def canSkipCase(remainingScrutinee: Value, catchValue: Value) = | ||
(remainingScrutinee == Bottom && scrutinee != Bottom) || | ||
(catchValue == Bottom && remainingScrutinee != Bottom) | ||
|
||
cases.map(evalCase).join | ||
var remainingScrutinee = scrutinee | ||
val caseResults: mutable.ArrayBuffer[Value] = mutable.ArrayBuffer() | ||
for caseDef <- cases do | ||
val (tpe, value) = evalPattern(remainingScrutinee, caseDef.pat) | ||
eval(caseDef.guard, thisV, klass) | ||
if !canSkipCase(remainingScrutinee, value) then | ||
caseResults.addOne(eval(caseDef.body, thisV, klass)) | ||
if catchesAllOf(caseDef, tpe) then | ||
remainingScrutinee = remainingScrutinee.remove(value) | ||
|
||
caseResults.join | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Dealing with pattern matches is a headache. The code above improves the situation. Another possibility is to just print a warning and skip analyzing it. This is a thought after reading the rule 10 of Nasa's 10 rules: https://spinroot.com/gerard/pdf/P10.pdf I think there is still a design spot where the analysis can give up for some complicated cases while remain useful and sound for most use cases. We just need to clearly define the boundary and have nice messages. |
||
end patternMatch | ||
|
||
/** Handle semantics of leaf nodes | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this
ListSet
and not justSet
?