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.

Sign up for GitHub

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

Print evaluator type and values of free variable of assertion failure predicate #1084

Open
wants to merge 3 commits into
base: scala-2
Choose a base branch
from
Open

Print evaluator type and values of free variable of assertion failure predicate #1084

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
efac9ba
Print evaluator type and values of free variable of assertion failure…
vkuncak May 29, 2021
375c3f1
Display require failure with a similar binding
vkuncak May 29, 2021
0a44f0d
Use asString on id and pred instead of toString
vkuncak May 30, 2021
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
12 changes: 9 additions & 3 deletions core/src/main/scala/stainless/evaluators/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,15 @@ import inox.evaluators.DeterministicEvaluator
object optCodeGen extends inox.FlagOptionDef("codegen", false)

object Evaluator {
val RecursiveEvaluatorName: String = "default recursive evaluator"
val CodeGenEvaluatorName: String = "codegen evaluator"
var kind: String = RecursiveEvaluatorName
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we include the names into the evaluators instead of using the global variable kind? I'm afraid this requires changing Inox though to add a name field.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I did not want to chage Inox this time. Maybe later.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of storing this in a global var, you could also compute the evaluator name to output inside the EvaluatorComponent based on ctx.options.findOptionOrDefault(optCodeGen) (especially since the property isn't really global).

Copy link
Collaborator Author

@vkuncak vkuncak May 31, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't like checking the option since it's not telling me what the evaluator actually is, but what it should have been set to and there is complex initialization logic that determines that. Unfortunately I cannot use reflection and print dynamic class name e.g.with .getClass.getSimpleName() because somewhere in the code an anonymous class is created and the actual class name is lost.

Another question: how do I make --check-models benefit from this?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reflection should work, I think there's something like getClass.getSimpleName which isn't too mangled.

Model checking currently takes place in Inox. The easiest way to get it to benefit from the new behavior would be to always disable optCheckModels in Inox (like here) and check models inside Stainless. The logic on the Inox side is here. Model checking in Stainless could actually be more powerful because we have access to the type checker, but you might need to be careful about running into loops.

def apply(p: StainlessProgram, ctx: inox.Context):
DeterministicEvaluator { val program: p.type } = {
if (ctx.options.findOptionOrDefault(optCodeGen)) CodeGenEvaluator(p, ctx)
else RecursiveEvaluator(p, ctx)
DeterministicEvaluator { val program: p.type } =
{
if (ctx.options.findOptionOrDefault(optCodeGen)) {
kind = CodeGenEvaluatorName
CodeGenEvaluator(p, ctx)
} else RecursiveEvaluator(p, ctx)
}
}
6 changes: 5 additions & 1 deletion core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,11 @@ class EvaluatorRun(override val pipeline: extraction.StainlessPipeline)
}

// Build an evaluator once and only if there is something to evaluate
lazy val evaluator = p.getSemantics.getEvaluator
lazy val evaluator = {
val e = p.getSemantics.getEvaluator
reporter.info(s"using ${Evaluator.kind}")
e
}

// Evaluate an expression, logging events
def evaluate(title: String, e: Expr): Either[String, Expr] = evaluator eval e match {
Expand Down
34 changes: 28 additions & 6 deletions core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
package stainless
package evaluators


trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
val program: Program

Expand All @@ -11,11 +12,31 @@ trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
import program.trees._
import program.symbols._

import inox.utils.Position

def showPredicateFailure(kind: String, pred: Expr, err: Option[String])(implicit rctx: RC): Unit = {
val msg = (err match {
case Some(m) => m + ": "
case None => ""
}) + pred.asString
reporter.info(s"${Position.smartPos(pred.getPos)} ${kind} failure of ${msg}")
reporter.info(s"Relevant variables at ${kind} failure point:")
val m = rctx.mappings
val fvs = exprOps.variablesOf(pred)
def showBinding(v: Variable): String = {
" " + v.id.asString + " -> " + m.get(v.toVal).getOrElse("?").toString
}
val fvDump: String = fvs.map(showBinding).mkString("\n")
reporter.info(fvDump)
}


override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Require(pred, body) =>
if (!ignoreContracts && e(pred) != BooleanLiteral(true))
throw RuntimeError("Requirement did not hold @" + expr.getPos)
e(body)
if (!ignoreContracts && e(pred) != BooleanLiteral(true)) {
showPredicateFailure("require", pred, None)
throw RuntimeError("Requirement did not hold @" + Position.smartPos(expr.getPos))
} else e(body)

case en @ Ensuring(body, pred) =>
e(en.toAssert)
Expand All @@ -24,9 +45,10 @@ trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
e(body)

case Assert(pred, err, body) =>
if (!ignoreContracts && e(pred) != BooleanLiteral(true))
throw RuntimeError(err.getOrElse("Assertion failed @" + expr.getPos))
e(body)
if (!ignoreContracts && e(pred) != BooleanLiteral(true)) {
showPredicateFailure("assertion", pred, err)
throw RuntimeError(err.getOrElse("Assertion failed @" + Position.smartPos(pred.getPos)))
} else e(body)

case MatchExpr(scrut, cases) =>
val rscrut = e(scrut)
Expand Down