Trigger generation code picks too strict triggers

[viper-admin]

Created by @mschwerhoff on 2015-10-26 22:03
Last updated on 2015-11-17 07:58

The auto-triggers picked for the pure quantifier(s) in triggering_problem.sil are too strict. logfile.smt2 show the failing SMT2 program generated by Silicon.

---

Attachments:

• triggering_problem.sil
• logfile.smt2
• triggering_problem_solution.sil

[viper-admin]

@mschwerhoff on 2015-10-26 22:04:

• edited the description

[viper-admin]

@mschwerhoff on 2015-10-27 08:33:

• changed component from (none) to Triggers

[viper-admin]

@alexanderjsummers commented on 2015-11-16 15:27

Which triggers would work, for this example?

[viper-admin]

@mschwerhoff commented on 2015-11-17 07:57

Fair question. I can manually edit the SMT file to essentially use this.nodes[i] as a trigger (or rather, its translation into SMT, (Seq.index t@1 i@2)), which makes Z3 succeed. But our current trigger generation code (at least when applied to the original Silver quantifier ) will of course not pick this.nodes[i] as a trigger.

The Silver file can be rewritten by introducing and using a "heap lookup function" nodes_at(this, i) to access this.nodes[i], in which case the example can be verified, see triggering_problem_solution.sil.
The expression has to be used explicitly as a trigger; unfortunately, both inside the predicate but also at the point where the quantifier is to be proven. The latter might be surprising to users, but it is (currently) needed because, in Silicon's case, the evaluation of the quantifier to be proven yields an auxiliary quantifier (whose body includes field value function definitional axioms) for which the trigger is taken from the original quantifier.

The example illustrates two additional issues with out trigger generation code (when applied to triggering_problem_solution.sil): one related to disjunctions, one related to Silicon's (current) handling of QPs.

1. Without explicit triggers, the trigger generation code picks foo(nodes_at(this, i).next) as a trigger (Note: I am surprised to see that it picks a trigger which contains a field dereference). This trigger, however, is only available on one side of the conditional (in the quantifier body), and Z3 then fails to show the last assertion (I manually edited the SMT file to observe this)

2. Let's assume that nodes_at(this, i).next were picked as a trigger. Since Silicon introduces a new field value function per field read (of a quantified field), the assumption quantifier(s) gained from unfolding the predicate introduce two field value functions (one per side of the conditional), and the same will happen when the quantifier is asserted (in the method body). That is, the four occurrences of nodes_at(this, i).next will be evaluated to (FVF.lookup_next fvf@1 (nodes_at ...)), (FVF.lookup_next fvf@2 (nodes_at ...)), etc. Picking any of these terms as a trigger will not allow Z3 to instantiate all quantifiers necessary to prove the assertion, because the non-quantified field value functions won't match. Z3 would be able to show equality between the field value functions (per side of the conditional), but only if it instantiated the aforementioned quantifiers, since the definitional axioms of the field value functions are nested under those. Caching/avoiding the generation of equivalent field value functions should overcome this problem in this specific example, but might fail in the general case, depending on how syntactic (and thus cheap) the caching strategy is.

[viper-admin]

@mschwerhoff commented on 2015-11-17 07:58

[viper-admin]

@mschwerhoff on 2015-11-17 07:58:

• changed attachment from (none) to triggering_problem_solution.sil