Precondition reason

[pieter-bos]

We rely on the fact that we can recover the section of the precondition of a method that fails by storing metadata in the info of precondition nodes and then inspecting the error reason. I noticed that the error reason will report the expression in a form where all parameters are substituted with their actual value, which in the extreme case can make all information about the precondition disappear if an assertion is directly a parameter:

method req(x: Bool, y: Bool)
requires x && y
{

}

method use()
{
  req(false, false)
}

reports:

The precondition of method req might not hold. Assertion false might not hold. (output-0.vpr@9.3--9.20)

Didactically this makes sense to me, but I don't see a way for us to now know whether x or y is false. Is there a nice trick to resolve this? We can resort to some hack like encoding (x || false) instead but I would prefer not to :)

[Aurel300]

Are you relying on error messages/is the interaction with Viper based on generating Viper files? When constructing the AST you can provide IDs for nodes, then recover those from the verification error.

[pieter-bos]

No, we make ASTs directly. By adding id's do you just mean store information in the info? We do that, the point is there is no node left to represent the declared precondition.

[marcoeilers]

You could attach information (through an Info or a custom Position object) to the argument expressions themselves (i.e., here the two false literals) I guess?

[pieter-bos]

Even then it would require scanning to obtain the position in the declared contract where the parameter occurs as a direct cause of failing the contract, to attach the equivalent metadata to the argument expression. Anyway it's more an aesthetic concern so I think we'll just encode true ==> x or so when an argument occurs in a position like this, thanks for the pointers :)