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

[vkuncak]

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       

[jad-hamza]

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

[jad-hamza]

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.

[vkuncak]

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

[samarion]

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).

[vkuncak]

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?

[samarion]

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.

[jad-hamza]

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

[jad-hamza]

toString here too

[vkuncak]

Replaced toString with asString in two places.