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

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

Conversation

vkuncak
Copy link
Collaborator

@vkuncak vkuncak commented May 29, 2021

Currently --eval does not helpfully show the bindings of variables when we encounter assertion failure. This PR makes a small change to RecursiveEvaluator to show the values of free variables of assertion failing predicate. It also displays the type of evaluator (recursive or codegen) when evaluating each function.

Given this input:

object VarDefault {
  case class AA(var x: Int = 555, var y: Int = 222)
  def addMe: Unit = {
    val aa = AA(2147483647, 1073741823)
    assert(0 <= aa.x && 0 <= aa.y, "both positive")
    val x = aa.x
    val y = aa.y
    val z = x + y
    assert(0 <= x + aa.y, "sum positive")
  }
}

the output with --eval --no-colors is:

Evaluating addMe
using default recursive evaluator
VarDefault.scala:9:12:  assertion failure of sum positive: 0 <= x + aa.y
Relevant variables at assertion failure point:
x -> 2147483647
aa -> AA(2147483647, 1073741823)
Result for addMe @3:3:
warning:  => CRASHED
warning:   sum positive
  
 stainless summary 
                                                                   
VarDefault.scala:3:3:                             addMe        crashed          0.0    
........................................................................................
total: 1    valid: 0    (0 from cache) invalid: 1    unknown: 0    time:     0.0       

@vkuncak vkuncak requested a review from jad-hamza May 29, 2021 20:32
Copy link
Contributor

@jad-hamza jad-hamza left a comment

Choose a reason for hiding this comment

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

Nice! I was missing that (similar) feature from leon-web :)

@@ -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

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.

val msg = (err match {
case Some(m) => m.toString + ": "
case None => ""
}) + pred.toString
Copy link
Contributor

Choose a reason for hiding this comment

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

We generally use asString instead of toString, so that printing respects options such as --print-ids.

reporter.info("Relevant variables at assertion failure point:")
val m = rctx.mappings
val fvs = exprOps.variablesOf(pred)
val fvDump: String = fvs.map(v => v.id.toString + " -> " + m.get(v.toVal).getOrElse("?").toString)
Copy link
Contributor

Choose a reason for hiding this comment

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

toString here too

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Replaced toString with asString in two places.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants