Trigger legality checks do not consider inlining

[RustanLeino]

Boogie ordinarily checks triggers to be legal trigger expressions. For example, operators && and <= are not legal in triggers, so Boogie complains about the following program:

function Q(int): bool;

procedure P() {
  assume (forall z: int :: {0 <= z && z < 100} 0 <= z && z < 100 ==> Q(z));
  assert Q(28);
}

b.bpl(4,35): Error: boolean operators are not allowed in triggers
b.bpl(4,30): Error: arithmetic comparisons are not allowed in triggers
b.bpl(4,40): Error: arithmetic comparisons are not allowed in triggers
3 name resolution errors detected in b.bpl

Alas, the trigger legality checking does not dip into {:inline} functions. Therefore, if a trigger mentions an {:inline} function and that function has a body that would be illegal in a trigger, then the SMT formulas that Boogie generates will contain illegal triggers.

Repro. The following program passes through Boogie without error:

function Q(int): bool;

function {:inline} InlinedFunction(x: int): bool {
  0 <= x && x < 100
}

procedure P() {
  assume (forall z: int :: {InlinedFunction(z)} 0 <= z && z < 100 ==> Q(z));
  assert Q(28);
}

The SMT it generates contains the illegal, inlined trigger:

(forall ((z Int) ) (!  (=> (and (<= 0 z) (< z 100)) (Q z))
 :qid |bbpl.8:18|
 :skolemid |0|
 :pattern (  (and (<= 0 z) (< z 100)))
 ))

This trigger is indeed illegal also at the SMT level, as is demonstrated by adding the /proverWarnings:1 flag to Boogie:

$ boogied b.bpl /proverWarnings:1
Prover warning: (30,1): 'and' cannot be used in patterns.

Boogie program verifier finished with 1 verified, 0 errors

PS. This bug was detected due to a latent bug in Dafny that generated such illegal triggers: https://github.com/dafny-lang/dafny/issues/1150

[shazqadeer]

@RustanLeino : Are there useful scenarios where calls to inlined functions are useful in triggers? What if we reported an error if that happens?

[shazqadeer]

@RustanLeino : Another ping on my question on this issue.

[RustanLeino]

Yes, there are use scenarios where triggers mention inlined functions. Dafny uses a function read for reading the heap:

function {:inline} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha
{
  H[r][f]
}

type Heap = [ref]<alpha>[Field alpha]alpha;

This function was introduced so that it would be easy to switch out the type Heap. Up until a few years ago, Dafny had instead used:

function {:inline} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha
{
  H[r, f]
}

type Heap = <alpha>[ref, Field alpha]alpha;

The read function frequently gets produced into triggers that Dafny passes down to Boogie.

This is convenient, but it would also be possible for Dafny to expand this function as it's generating Boogie code.

[shazqadeer]

I looked at the code implementing trigger legality checks. Currently, the checks are being done during resolution. If we want error reporting to take into account function calls, then the right place to do the checks would be at type checking time when all function calls have been resolved.

The method at the following line is the basis for all this checking:

https://github.com/boogie-org/boogie/blob/fcb674ae369ab7f8666131989bafec597f2e8a06/Source/Core/AbsyExpr.cs#L1644

The argument subjectForErrorReporting for this method is used precisely for reporting errors on triggers.

Overall, if we want to do the legal trigger checking during type checking:

• We would have to move the argument subjectForErrorReporting to the method Typecheck.
• We would also have to move the field TriggerMode from ResolutionContext to TypecheckingContext.
• We would add a field to each function to record whether it is suitable to be used inside a trigger. This field would have to be computed based on call dependencies.
• We would check function calls when TriggerMode==true.

Question: Should we go down this path? If not, we would have to outlaw calls to inlined functions in triggers.

[RustanLeino]

What you're describing sounds like an overall improvement to me. I'd argue that doing trigger checking before type checking was a design mistake. In fact, one could even imagine doing trigger checking as a separate pass that happens after type checking. Then, the phases would like like (0) resolution, (1) type checking, (2) trigger checking and other kinds of checking that rely on type information and resolution.

That's what I would recommend.