Add modifies * wildcard support to Laurel (strata-org#1031)

Adds `modifies *` wildcard syntax to Laurel, as described in strata-org#1030.

## Changes

**Grammar** (`LaurelGrammar.st`): Added `modifiesWildcard` rule that
parses `modifies *`.

**Parser** (`ConcreteToAbstractTreeTranslator.lean`): Handles
`modifiesWildcard` by producing `StmtExpr.All` in the modifies list.

**Formatter** (`AbstractToConcreteTreeTranslator.lean`): Formats a
modifies list containing `All` back as `modifies *`.

**ModifiesClauses pass** (`ModifiesClauses.lean`):
- Added `hasModifiesWildcard` to detect `All` in the modifies list.
- `transformModifiesClauses` skips frame condition generation for
`modifies *` — the procedure may modify anything on the heap.
- `filterBodyNonCompositeModifies` preserves the wildcard through the
filter pass.

**HeapParameterization**: No changes needed — the existing
`!modif.isEmpty` check already marks procedures with `modifies *` as
heap writers, even without a body.

**Tests** (`T2_ModifiesClauses.lean`): Added three test cases:
- `modifiesWildcardBodiless`: bodiless procedure with `modifies *`
- `modifiesWildcardBodilessCaller`: caller that verifies heap state is
lost after calling a `modifies *` procedure (assertion correctly fails)
- `modifiesWildcardWithBody`: procedure with body and `modifies *` (no
frame condition error)

All 48 Laurel tests pass.

Closes strata-org#1030

---------

Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Co-authored-by: thanhnguyen-aws <ntson@amazon.com>
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: Michael Tautschnig <mt@debian.org>

Author: 5 people

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -188,9 +188,12 @@ private def ensuresClauseToArg (c : Condition) : Arg :=
     laurelOp "errorSummary" #[.strlit sr msg])
   laurelOp "ensuresClause" #[stmtExprToArg c.condition, errOpt]
 
-private def modifiesClauseToArg (modifies : List StmtExprMd) : Arg :=
-  let refs := modifies.map stmtExprToArg |>.toArray
-  laurelOp "modifiesClause" #[commaSep refs]
+private def modifiesClausesToArgs (modifies : List StmtExprMd) : Array Arg :=
+  let (wildcards, specific) := modifies.partition StmtExprMd.isWildcard
+  let wildcardArgs := wildcards.map (fun _ => laurelOp "modifiesWildcard" #[]) |>.toArray
+  let specificArgs := if specific.isEmpty then #[]
+    else #[laurelOp "modifiesClause" #[commaSep (specific.map stmtExprToArg |>.toArray)]]
+  wildcardArgs ++ specificArgs
 
 private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let opName := if proc.isFunctional then "function" else "procedure"
@@ -219,7 +222,7 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
       (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
-      let mods := if modifies.isEmpty then #[] else #[modifiesClauseToArg modifies]
+      let mods := if modifies.isEmpty then #[] else modifiesClausesToArgs modifies
       let body := optionArg (impl.map fun e => laurelOp "body" #[stmtExprToArg e])
       (optionArg (some (laurelOp "opaqueSpec" #[seqArg ens, seqArg mods])), body)
     | .Abstract postconds =>

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -378,6 +378,11 @@ def translateModifiesClauses (arg : Arg) : TransM (List StmtExprMd) := do
         | q`Laurel.modifiesClause, #[refsArg] =>
           let refs ← translateModifiesExprs refsArg
           allModifies := allModifies ++ refs
+        | q`Laurel.modifiesWildcard, #[] =>
+          let src ← match (← get).uri with
+            | some uri => pure (some (SourceRange.toFileRange uri clauseOp.ann))
+            | none => pure none
+          allModifies := allModifies ++ [mkStmtExprMd .All src]
         | _, _ => TransM.error s!"Expected modifiesClause operation, got {repr clauseOp.name}"
       | _ => TransM.error s!"Expected modifiesClause operation in modifies sequence"
     pure allModifies

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: added opaque keyword between invokeOn and ensures in procedure/function ops.
+-- Last grammar change: added modifiesWildcard for `modifies *` and opaque keyword
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -157,6 +157,7 @@ op ensuresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): EnsuresClau
 
 category ModifiesClause;
 op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "\n  modifies " refs;
+op modifiesWildcard: ModifiesClause => "\n  modifies *";
 
 category ReturnParameters;
 op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "\n  returns " "(" parameters ")";

Strata/Languages/Laurel/Laurel.lean

@@ -402,6 +402,13 @@ def HighType.isBool : HighType → Bool
   | TBool => true
   | _ => false
 
+/-- Check whether a single modifies entry is the wildcard (`*`). -/
+def StmtExprMd.isWildcard (m : StmtExprMd) : Bool := match m.val with | .All => true | _ => false
+
+/-- Check whether a modifies list contains the wildcard (`*`). -/
+def hasModifiesWildcard (modifiesExprs : List StmtExprMd) : Bool :=
+  modifiesExprs.any StmtExprMd.isWildcard
+
 def Body.isExternal : Body → Bool
   | .External => true
   | _ => false

Strata/Languages/Laurel/ModifiesClauses.lean

@@ -140,6 +140,9 @@ def hasHeapOut (proc : Procedure) : Bool :=
 Transform a single procedure: if it has modifies clauses, generate the frame
 condition and conjoin it with the postcondition, then clear the modifies list.
 
+If the procedure has `modifies *`, no frame condition is generated (the procedure
+may modify anything on the heap), and the modifies list is simply cleared.
+
 If the procedure has a `$heap` but no modifies clause, adds a postcondition
 that all allocated objects are preserved between heaps:
   `forall $obj: Composite, $fld: Field => $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)`
@@ -149,7 +152,10 @@ def transformModifiesClauses (model: SemanticModel)
   match proc.body with
   | .External => .ok proc
   | .Opaque postconds impl modifiesExprs =>
-      if hasHeapOut proc then
+      if hasModifiesWildcard modifiesExprs then
+        -- modifies * means the procedure can modify anything; no frame condition
+        .ok { proc with body := .Opaque postconds impl [] }
+      else if hasHeapOut proc then
         let heapInName : Identifier := "$heap_in"
         let heapName : Identifier := "$heap"
         let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName
@@ -172,10 +178,13 @@ def filterBodyNonCompositeModifies (model : SemanticModel) (body : Body)
   match body with
   | .Opaque posts impl mods =>
     let (kept, diags) := mods.foldl (fun (acc, ds) e =>
-      let ty := (computeExprType model e).val
-      if isHeapRelevantType ty then (acc ++ [e], ds)
-      else
-        (acc, ds ++ [diagnosticFromSource e.source s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
+      match e.val with
+      | .All => (acc ++ [e], ds)  -- wildcard is always kept
+      | _ =>
+        let ty := (computeExprType model e).val
+        if isHeapRelevantType ty then (acc ++ [e], ds)
+        else
+          (acc, ds ++ [diagnosticFromSource e.source s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
     ) ([], [])
     (.Opaque posts impl kept, diags)
   | other => (other, [])

StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean

@@ -105,6 +105,41 @@ procedure newObjectDoNotCountForModifies()
   var c: Container := new Container;
   c#value := 1
 };
+
+procedure modifiesWildcardBodiless(c: Container, d: Container)
+  opaque
+  modifies *;
+
+procedure modifiesWildcardBodilessCaller() {
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  modifiesWildcardBodiless(c, d);
+  assert x == d#value // this should fail because modifies * means anything can change
+//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+};
+
+procedure modifiesWildcardWithBody(c: Container, d: Container)
+  opaque
+  modifies *
+{
+  c#value := 2;
+  d#value := 3
+};
+
+procedure modifiesWildcardAndSpecific(c: Container, d: Container)
+  opaque
+  modifies c
+  modifies *;
+
+procedure modifiesWildcardAndSpecificCaller() {
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  modifiesWildcardAndSpecific(c, d);
+  assert x == d#value // fails because modifies * subsumes modifies c
+//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+};
 "
 
 #guard_msgs (drop info, error) in