Fix trigger legality checks to consider inline function bodies

Source/Core/AST/Expression/FunctionCall.cs

@@ -103,6 +103,10 @@ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting)
     if (Func != null)
     {
       // already resolved
+      if (rc.TriggerMode && Func.Body != null)
+      {
+        CheckBodyTriggerLegality(Func, subjectForErrorReporting, rc, new HashSet<Function>());
+      }
       return;
     }
 
@@ -111,12 +115,78 @@ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting)
     {
       rc.Error(this.name, "use of undeclared function: {0}", name.Name);
     }
-    else if (name.Type == null)
+    else
     {
-      // We need set the type of this IdentifierExpr so ShallowType() works
-      Debug.Assert(name.Type == null);
-      Debug.Assert(Func.OutParams.Count > 0);
-      name.Type = Func.OutParams[0].TypedIdent.Type;
+      if (name.Type == null)
+      {
+        // We need set the type of this IdentifierExpr so ShallowType() works
+        Debug.Assert(name.Type == null);
+        Debug.Assert(Func.OutParams.Count > 0);
+        name.Type = Func.OutParams[0].TypedIdent.Type;
+      }
+      if (rc.TriggerMode && Func.Body != null)
+      {
+        CheckBodyTriggerLegality(Func, subjectForErrorReporting, rc, new HashSet<Function>());
+      }
+    }
+  }
+
+  private static void CheckBodyTriggerLegality(Function func, Expr subjectForErrorReporting,
+    ResolutionContext rc, HashSet<Function> visited)
+  {
+    if (!visited.Add(func))
+    {
+      return; // Already checking this function (cycle detection)
+    }
+    CheckExprTriggerLegality(func.Body, func.Name, subjectForErrorReporting, rc, visited);
+  }
+
+  private static void CheckExprTriggerLegality(Expr expr, string funcName, Expr subjectForErrorReporting,
+    ResolutionContext rc, HashSet<Function> visited)
+  {
+    if (expr is NAryExpr nary)
+    {
+      if (nary.Fun is UnaryOperator uop && uop.Op == UnaryOperator.Opcode.Not)
+      {
+        rc.Error(subjectForErrorReporting,
+          "trigger expression refers to the inline function '{0}' whose body contains boolean operators, which are not allowed in triggers",
+          funcName);
+      }
+      else if (nary.Fun is BinaryOperator bop)
+      {
+        switch (bop.Op)
+        {
+          case BinaryOperator.Opcode.Eq:
+            rc.Error(subjectForErrorReporting,
+              "trigger expression refers to the inline function '{0}' whose body contains equality, which is not allowed in triggers",
+              funcName);
+            break;
+          case BinaryOperator.Opcode.Gt:
+          case BinaryOperator.Opcode.Ge:
+          case BinaryOperator.Opcode.Lt:
+          case BinaryOperator.Opcode.Le:
+            rc.Error(subjectForErrorReporting,
+              "trigger expression refers to the inline function '{0}' whose body contains arithmetic comparisons, which are not allowed in triggers",
+              funcName);
+            break;
+          case BinaryOperator.Opcode.And:
+          case BinaryOperator.Opcode.Or:
+          case BinaryOperator.Opcode.Imp:
+          case BinaryOperator.Opcode.Iff:
+            rc.Error(subjectForErrorReporting,
+              "trigger expression refers to the inline function '{0}' whose body contains boolean operators, which are not allowed in triggers",
+              funcName);
+            break;
+        }
+      }
+      else if (nary.Fun is FunctionCall nestedFc && nestedFc.Func?.Body != null)
+      {
+        CheckBodyTriggerLegality(nestedFc.Func, subjectForErrorReporting, rc, visited);
+      }
+      foreach (var arg in nary.Args)
+      {
+        CheckExprTriggerLegality(arg, funcName, subjectForErrorReporting, rc, visited);
+      }
     }
   }
 

Test/inline/triggerLegality.bpl

@@ -0,0 +1,55 @@
+// RUN: %parallel-boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Test that trigger legality checks consider inline function bodies
+
+function Q(int): bool;
+
+// --- Illegal trigger: inline function with body containing boolean operators ---
+
+function {:inline} IllegalInline(x: int): bool {
+  0 <= x && x < 100
+}
+
+procedure P1() {
+  assume (forall z: int :: {IllegalInline(z)} IllegalInline(z) ==> Q(z));
+  assert Q(28);
+}
+
+// --- Legal trigger: inline function with legal body ---
+
+function {:inline} LegalInline(x: int): int {
+  x + 1
+}
+
+procedure P2() {
+  // This should be allowed: the body of LegalInline is a legal trigger expression
+  assume (forall z: int :: {LegalInline(z)} LegalInline(z) > 0 ==> Q(z));
+  assert Q(28);
+}
+
+// --- Illegal trigger: nested inline functions with illegal body ---
+
+function {:inline} OuterInline(x: int): bool {
+  InnerInline(x)
+}
+
+function {:inline} InnerInline(x: int): bool {
+  x > 0 && x < 100
+}
+
+procedure P3() {
+  assume (forall z: int :: {OuterInline(z)} OuterInline(z) ==> Q(z));
+  assert Q(28);
+}
+
+// --- Illegal trigger: inline function with equality in body ---
+
+function {:inline} HasEquality(x: int): bool {
+  x == 5
+}
+
+procedure P4() {
+  assume (forall z: int :: {HasEquality(z)} HasEquality(z) ==> Q(z));
+  assert Q(28);
+}

Test/inline/triggerLegality.bpl.expect

@@ -0,0 +1,8 @@
+triggerLegality.bpl(15,28): Error: trigger expression refers to the inline function 'IllegalInline' whose body contains boolean operators, which are not allowed in triggers
+triggerLegality.bpl(15,28): Error: trigger expression refers to the inline function 'IllegalInline' whose body contains arithmetic comparisons, which are not allowed in triggers
+triggerLegality.bpl(15,28): Error: trigger expression refers to the inline function 'IllegalInline' whose body contains arithmetic comparisons, which are not allowed in triggers
+triggerLegality.bpl(42,28): Error: trigger expression refers to the inline function 'InnerInline' whose body contains boolean operators, which are not allowed in triggers
+triggerLegality.bpl(42,28): Error: trigger expression refers to the inline function 'InnerInline' whose body contains arithmetic comparisons, which are not allowed in triggers
+triggerLegality.bpl(42,28): Error: trigger expression refers to the inline function 'InnerInline' whose body contains arithmetic comparisons, which are not allowed in triggers
+triggerLegality.bpl(53,28): Error: trigger expression refers to the inline function 'HasEquality' whose body contains equality, which is not allowed in triggers
+7 name resolution errors detected in triggerLegality.bpl