feat: add purity checking to Verifier
#7683
Conversation
| /** | ||
| * Throw `InternalCompilerException` because the `expected` purity does not match the `found` purity | ||
| */ | ||
| private def failUnexpectedPurity(found: Purity, expected: Purity, loc: SourceLocation): Nothing = |
There was a problem hiding this comment.
yea... any suggestions for improvements? I thought that parameterizing type of found/expected was ugly.
maybe there is some elegant Scala-way?
There was a problem hiding this comment.
Ah sorry, didn't see that the one used a string. maybe you could make one call the other?
| /** | ||
| * Asserts that `p` is either `Impure` or `ControlImpure` | ||
| */ | ||
| private def checkImpure(p: Purity, loc: SourceLocation): Purity = { |
There was a problem hiding this comment.
To avoid ambiguous language I think i'd call it checkNotPure. This Impure/Control-impure is quite new so the words have not been totally decided
| case Constant.Str(_) => check(expected = MonoType.String)(actual = tpe, loc) | ||
| case Constant.Regex(_) => check(expected = MonoType.Regex)(actual = tpe, loc) | ||
| } | ||
| (t, Purity.Pure) |
There was a problem hiding this comment.
its a bit weird with this AST node and some others, in that it does have a purity, just not in its "pattern" (see the definition of Expr.Cst). I think its the most consistent to check that it is pure, even though its defined as pure always.
| case Expr.Cst(cst, tpe, loc) => | ||
| val t = cst match { | ||
| case Constant.Unit => check(expected = MonoType.Unit)(actual = tpe, loc) | ||
| case Constant.Null => tpe |
There was a problem hiding this comment.
unrelated note: in the jvm PR you have the power to check that tpe is an object type
|
|
||
| op match { | ||
| case AtomicOp.Unary(sop) => | ||
| val List(t) = ts | ||
| val (List(t), List(p)) = rs.unzip | ||
| val opTpe = sop match { | ||
| case SemanticOp.BoolOp.Not => MonoType.Bool |
There was a problem hiding this comment.
it could make sense to, for each case, return its effect. so every line would say (MonoType.Something, Purity.Pure) and the combine that with the result. It doesn't do anything but it makes it more robust to future modifications
There was a problem hiding this comment.
same thing in binary
There was a problem hiding this comment.
In general, if it doesn't hurt the code to much, it would be nice that in a given expression it is clear what its inherent effect is and what the "nested" effect is
| tpe | ||
| ( | ||
| checkEq(arrType, tpe, loc), | ||
| checkEq(pur, Purity.combine3(pur, p1, p2), loc) |
There was a problem hiding this comment.
I don't think pur should be in the combination
There was a problem hiding this comment.
oh its because we don't know the inherent effect of the array creating because we don't have the region anymore?
There was a problem hiding this comment.
oh and we cant assume impure because some code is cheating with Array[t, Pure] hmmm
| case _ => failMismatchedShape(t1, "Ref", loc) | ||
| } | ||
|
|
||
| // Match- and Hole-errors match with any type | ||
| case AtomicOp.HoleError(_) => | ||
| tpe | ||
| (tpe, pur) |
There was a problem hiding this comment.
i might be mistaken, but i think these error should always be pure
There was a problem hiding this comment.
i ran into some cases where Hole/MatchError's were impure.
| val defn = root.defs(sym) | ||
| val signature = MonoType.Arrow(defn.fparams.map(_.tpe), defn.tpe) | ||
|
|
||
| val decl = MonoType.Arrow(defn.cparams.map(_.tpe), signature) | ||
| val actual = MonoType.Arrow(ts, tpe) | ||
|
|
||
| checkEq(decl, actual, loc) | ||
| tpe | ||
| (tpe, pur) |
There was a problem hiding this comment.
pur should still reflect the combination of all the rs effects
|
|
||
| case AtomicOp.Region => | ||
| check(expected = MonoType.Region)(actual = tpe, loc) | ||
| case AtomicOp.Region => // TODO: VERIFIER: purity checking for Region/Spawn |
There was a problem hiding this comment.
region itself is always a pure expression
| val lamType1 = visitExpr(exp) | ||
| val lamType2 = MonoType.Arrow(exps.map(visitExpr), tpe) | ||
| case Expr.ApplyClo(exp, exps, ct, tpe, pur, loc) => // TODO: VERIFIER: purity checking for function calls/TryWith/Do/NewObject (+ a discussion about Purity in MonoType.Arrow?) | ||
| val lamType1 = visitExpr(exp)._1 |
There was a problem hiding this comment.
the ignored parts of visitExpr should also be combined and checked against pur. even without the arrow purity, we still know that the combination must be less than or equal to pur.
|
Its looking good but you've found some complications we need to solve, am i missing something?
|
Currently many errors thrown. Many regarding combination of purities in
Letexpressions.