Potential problem with using partial functions as quantifier triggers

[viper-admin]

Created by @mschwerhoff on 2017-04-04 13:38 Last updated on 2017-04-04 13:46

Silicon currently doesn't differentiate between regular program expressions and trigger expressions, i.e. they are symbolically evaluated alike. This can cause problems if partial functions (functions with preconditions) are used as triggers. Consider the following example:

forall i: Int :: {xs[i]} 0 <= i && i < |xs| ==> xs[i] != 0

Symbolically evaluating the trigger expression xs[i] would fail because index i might be invalid (out of bounds). However, since xs[i] also occurs in the quantifier body, in a context where i is constrained appropriately, this example does not pose a problem: instead of evaluating the trigger expression, simply reuses the result of the evaluation from the body.

However, the problem remains for trigger expressions that do not occur in the quantifier body, as in the following example:

forall i: Int :: {xs[i]} 0 <= i && i < |xs| ==> fun(i) != 0

Another, less apparent problematic example is the following:

forall i: Int :: 0 < i && i < n ==> bar(i, xs[i-1]) != 0   // where n <= |xs|

Out trigger generation code can rewrite this quantifier as follows:

forall i, j: Int :: {bar(i, xs[j])} 0 < i && i < n ==> bar(i, xs[i-1]) != 0

Now, the trigger expression does not occur in the body and symbolically evaluating the trigger will fail.

[viper-admin]

@mschwerhoff commented on 2017-04-04 13:40

I have a solution in mind, but I'll delay its implementation until we decided on how to handle heap-dependent triggers.

[viper-admin]

@mschwerhoff commented on 2017-04-04 13:46

Currently affected tests:

• quantifiedpermissions/third_party/testHistogram.sil
• quantifiedpermissions/issues/issue_0147.sil