Fix trigger legality checks to consider inline function bodies

[Copilot]

Boogie's trigger legality checks were not inspecting the bodies of {:inline} functions used in triggers. A trigger like {InlinedFunction(z)} would pass validation even if the inlined body contained boolean operators or arithmetic comparisons, resulting in illegal SMT triggers being silently emitted.

Root cause: Trigger legality is enforced during resolution via rc.TriggerMode, but function bodies are resolved without that flag set. When FunctionCall.Resolve is called inside a trigger, only the call site was checked—not the body.

Fix — FunctionCall.cs:

• After resolving an inline function (Func.Body != null) while rc.TriggerMode is true, recursively check the body for illegal trigger expressions
• Added CheckBodyTriggerLegality / CheckExprTriggerLegality helpers that walk the expression tree detecting:
  • Boolean operators (&&, ||, !, ==>, <==>), equality (==), arithmetic comparisons (<, <=, >, >=)
  • Calls to transitively-inlined functions (with cycle detection via HashSet<Function>)
• Handles the "already resolved" early-return path so pre-constructed FunctionCall(Function f) nodes are also checked

Example — previously undetected, now caught:

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

procedure P() {
  // ERROR: trigger body contains arithmetic comparisons and boolean operators
  assume (forall z: int :: {InlinedFunction(z)} InlinedFunction(z) ==> Q(z));
}

b.bpl(5,28): Error: trigger expression refers to the inline function 'InlinedFunction'
             whose body contains boolean operators, which are not allowed in triggers

Legal inline functions (e.g., bodies with only arithmetic, map selects, or !=) remain unaffected.

Test — Test/inline/triggerLegality.bpl: Covers direct illegal bodies, legal bodies (no false positives), nested inline chains, and equality in bodies.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Trigger legality checks do not consider inlining</issue_title>
<issue_description>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: dafny-lang/dafny#1150</issue_description>

Comments on the Issue (you are @copilot in this section)

@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.</comment_new>
<comment_new>@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:

boogie/Source/Core/AbsyExpr.cs

Line 1644 in fcb674a

void Resolve(ResolutionContext /*!*/ rc, Expr /*!*/ subjectForErrorReporting);

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.</comment_new>
<comment_new>@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...

• Fixes Trigger legality checks do not consider inlining #368

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.