From b85c4801b20ea2a3dd9567342f511d4792908967 Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Fri, 12 Jun 2026 10:00:26 -0700 Subject: [PATCH 01/10] Merge main into main2 (2026-06-11) (#1363) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary - Periodic merge of `main` into `main2` to keep main2 up to date with core improvements - 46 new commits from main since PR #1346 (mostly repo-removal PRs: #1339, #1351, #1343, #1329, #1334, plus code changes) - All conflicts resolved by keeping main2's versions (sub-repos stay local, no module migration, preserves main2-only features like Procedure.Body sum type, transparent procs, array axiomatization) - Fixed duplicate StrataDDM git entries that auto-merged into `docs/api/lake-manifest.json` and `docs/verso/lake-manifest.json` --------- Co-authored-by: Aaron Tomb Co-authored-by: Michael Tautschnig Co-authored-by: Kiro Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: keyboardDrummer-bot Co-authored-by: Mikaël Mayer Co-authored-by: thanhnguyen-aws Co-authored-by: Fabio Madge Co-authored-by: Joe Hendrix Co-authored-by: Claude Opus 4.6 Co-authored-by: June Lee Co-authored-by: David Deng Co-authored-by: David Deng Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Co-authored-by: Mikael Mayer Co-authored-by: Remy Willems Co-authored-by: keyboardDrummer-bot Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com> --- .kiro/steering/structure.md | 6 +- README.md | 29 +--- Scripts/JavaGenTestData.lean | 79 +++++++++++ Scripts/LaurelToCBMC.lean | 134 ++++++++++++++++++ .../CBMC/GOTO/test_property_summary_e2e.sh | 3 +- .../Backends/CBMC/cbmc-string-support.patch | 61 ++++++++ .../Languages/Laurel/run_laurel_cbmc_tests.sh | 7 +- 7 files changed, 286 insertions(+), 33 deletions(-) create mode 100644 Scripts/JavaGenTestData.lean create mode 100644 Scripts/LaurelToCBMC.lean create mode 100644 StrataTest/Backends/CBMC/cbmc-string-support.patch diff --git a/.kiro/steering/structure.md b/.kiro/steering/structure.md index 4445fa325b..e29800ee73 100644 --- a/.kiro/steering/structure.md +++ b/.kiro/steering/structure.md @@ -15,8 +15,6 @@ Strata is a Lean4 verification framework using **dialects** as composable langua - `Strata/` - Core implementation (DDM, dialects, languages, transforms, backends) - `StrataTest/` - Unit tests (mirrors Strata/ structure) - `Examples/` - Sample programs (`.st` files, naming: `..st`) -- `Tools/` - External tools (BoogieToStrata, Python utilities) -- `vcs/` - Generated SMT2 verification conditions ### Core Components @@ -34,9 +32,7 @@ Strata is a Lean4 verification framework using **dialects** as composable langua - `Core/` - Primary verification language (procedures, contracts, VCG, SMT encoding) - `C_Simp/` - Simplified C-like language - `Dyn/` - Dynamic language example -- `Laurel/` - A common representation for front-end languages like Java, Python and JavaScript. -Translated to Core. -- `Python/` - The well-known Python language +- `Laurel/` - A common representation for front-end languages like Java, Python and JavaScript. Translated to Core. **`Strata/Transform/`** - Program Transformations - Each transformation has implementation + optional correctness proof (`*Correct.lean`) diff --git a/README.md b/README.md index e39b1ebd6d..3102b9c54d 100644 --- a/README.md +++ b/README.md @@ -28,13 +28,10 @@ changes!** (`cvc5` and `z3`). See [Installing dependencies → SMT Solvers](#smt-solvers) below. -3. **Python 3.11+**: required for Python-related tests and the `strata` - Python tooling. See [Installing dependencies → Python](#python) below. - -4. **Java JDK (11 or later)**: required for Java code generation tests. +3. **Java JDK (11 or later)**: required for Java code generation tests. See [Installing dependencies → Java](#java-for-code-generation-tests) below. -5. **ion-java jar (1.11.11)**: required for the Java/Ion integration test. +4. **ion-java jar (1.11.11)**: required for the Java/Ion integration test. See [Installing dependencies → Java](#java-for-code-generation-tests) below. ### Installing dependencies @@ -54,18 +51,6 @@ cp /path/to/cvc5 /path/to/z3 ~/.local/bin/ # or: sudo cp /path/to/cvc5 /path/to/z3 /usr/local/bin/ ``` -#### Python - -Python 3.11 or later is required. Install the `strata` Python package inside a -virtual environment (recommended; avoids PEP 668's `externally-managed-environment` -error on Debian/Ubuntu 23.04+): - -```bash -python3 -m venv .venv -source .venv/bin/activate -pip install ./Tools/Python -``` - #### Java (for code generation tests) A JDK (11+) providing `javac` must be on your `PATH`. For running the @@ -81,7 +66,6 @@ wget -q -O StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar \ ```bash cvc5 --version # should print version info z3 --version # should print version info -python3 --version # should be 3.11+ ``` ## Build @@ -111,13 +95,10 @@ Two kinds of tests coexist in this repo: These accept prefix filters: ```bash -# Run all extra tests except Python (which requires the Python package) -lake test -- --exclude Languages.Python - -# Run only Python extra tests (requires `pip install ./Tools/Python`) -lake test -- Languages.Python +# Run all extra tests except those in the Imperative namespace +lake test -- --exclude DL.Imperative -# Run all extra tests (Python tests will fail without the Python package above) +# Run all extra tests lake test ``` diff --git a/Scripts/JavaGenTestData.lean b/Scripts/JavaGenTestData.lean new file mode 100644 index 0000000000..00a2e890dc --- /dev/null +++ b/Scripts/JavaGenTestData.lean @@ -0,0 +1,79 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataDDM + +/-! +# Java test data generation helper + +Usage: + lake env lean --run Scripts/JavaGenTestData.lean javaGen + lake env lean --run Scripts/JavaGenTestData.lean print --include + +Note: Unlike the former CLI `javaGen` command, this script only loads dialects +from files — it does not support referencing preloaded dialect names directly. +This is sufficient for the testdata regeneration workflow. +-/ + +open StrataDDM + +def javaGen (dialectPath packageName outputDir : String) : IO Unit := do + let fm ← mkDialectFileMap + let d ← readStrataDialectFile fm dialectPath + match StrataDDM.Java.generateDialect d packageName with + | .ok files => + StrataDDM.Java.writeJavaFiles outputDir packageName files + IO.println s!"Generated Java files for {d.name} in {outputDir}/{StrataDDM.Java.packageToPath packageName}" + | .error msg => + IO.eprintln s!"Error generating Java: {msg}" + IO.Process.exit 1 + +def printFile (includeDirs : List String) (file : String) : IO Unit := do + let fm ← mkDialectFileMap + let mut fm := fm + for dir in includeDirs do + match ← fm.addSearchPath dir |>.toBaseIO with + | .error msg => + IO.eprintln msg + IO.Process.exit 1 + | .ok fm' => fm := fm' + let ld ← fm.getLoaded + if mem : file ∈ ld.dialects then + IO.print <| ld.dialects.format file mem + return + match ← readStrataFile fm file with + | .dialect d => + let ld ← fm.getLoaded + if mem : d.name ∈ ld.dialects then + IO.print <| ld.dialects.format d.name mem + else + IO.eprintln "Internal error reading file." + IO.Process.exit 1 + | .program pgm => + IO.print <| toString pgm + +private def parseIncludeArgs (args : List String) : List String × List String := + go args [] +where + go : List String → List String → List String × List String + | "--include" :: dir :: rest, includes => go rest (dir :: includes) + | other, includes => (includes.reverse, other) + +def main (args : List String) : IO Unit := do + match args with + | "javaGen" :: dialectPath :: packageName :: outputDir :: _ => + javaGen dialectPath packageName outputDir + | "print" :: rest => + let (includeDirs, fileArgs) := parseIncludeArgs rest + match fileArgs with + | [file] => printFile includeDirs file + | _ => + IO.eprintln "Usage: ... print [--include ]... " + IO.Process.exit 1 + | _ => + IO.eprintln "Usage:" + IO.eprintln " lake env lean --run Scripts/JavaGenTestData.lean javaGen " + IO.eprintln " lake env lean --run Scripts/JavaGenTestData.lean print [--include ]... " + IO.Process.exit 1 diff --git a/Scripts/LaurelToCBMC.lean b/Scripts/LaurelToCBMC.lean new file mode 100644 index 0000000000..61388af488 --- /dev/null +++ b/Scripts/LaurelToCBMC.lean @@ -0,0 +1,134 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline +import Strata.Languages.Laurel + +/-! # LaurelToCBMC + +Script that replaces `laurel_to_cbmc.sh`. Translates a Laurel `.lr.st` source +file through the full Strata pipeline to CBMC verification: + +1. Parse Laurel source → Laurel AST +2. Translate Laurel → Core +3. Inline procedures, type-check, generate CProver GOTO JSON +4. Invoke `symtab2gb` to produce a GOTO binary +5. Invoke `goto-cc` to add C scaffolding +6. Invoke `goto-instrument --dfcc` for contract instrumentation +7. Invoke `cbmc` for bounded model checking + +Usage: + lake env lean --run Scripts/LaurelToCBMC.lean + +Environment variables: + CBMC - path to cbmc binary (default: cbmc) + GOTO_CC - path to goto-cc binary (default: goto-cc) + GOTO_INSTRUMENT - path to goto-instrument binary (default: goto-instrument) +-/ + +open Strata + +/-- Strip well-known Strata file suffixes from a file path's basename. -/ +private def deriveBaseName (file : String) : String := + let name := System.FilePath.fileName file |>.getD file + let suffixes := [".lr.st", ".laurel.st", ".st"] + match suffixes.find? (name.endsWith ·) with + | some sfx => (name.dropEnd sfx.length).toString + | none => name + +/-- Read an environment variable, returning a default if unset or empty. -/ +private def getEnvOrDefault (var : String) (default : String) : IO String := do + match ← IO.getEnv var with + | some v => if v.isEmpty then pure default else pure v + | none => pure default + +/-- Run an external process. Prints stdout/stderr to the caller's streams and + returns the exit code. -/ +private def runProcess (step : String) (cmd : String) (args : Array String) : IO UInt32 := do + let proc ← IO.Process.spawn { + cmd := cmd + args := args + stdout := .inherit + stderr := .inherit + stdin := .inherit + } + let exitCode ← proc.wait + if exitCode != 0 then + IO.eprintln s!"Error: {step} failed (exit code {exitCode})" + return exitCode + +/-- The Laurel-to-GOTO translation pipeline. Parses a Laurel source file, + translates to Core, inlines procedures, type-checks, and emits CProver GOTO + JSON files (`.symtab.json` and `.goto.json`) in the + given output directory. -/ +private def laurelAnalyzeToGoto (path : System.FilePath) (outputDir : System.FilePath) + (baseName : String) : IO Unit := do + let content ← IO.FS.readFile path + let laurelProgram ← Strata.parseLaurelText path content + match ← Strata.Laurel.translate {} laurelProgram with + | (none, diags) => + throw (IO.userError s!"Core translation errors: {diags.map (·.message)}") + | (some coreProgram, _) => + -- Use the output directory as a prefix so files land in tmpDir + let outputBaseName := (outputDir / baseName).toString + match ← Strata.inlineCoreToGotoFiles coreProgram outputBaseName + (sourceText := some content) |>.toBaseIO with + | .ok () => pure () + | .error msg => throw (IO.userError msg) + +def main (args : List String) : IO UInt32 := do + match args with + | [file] => + unless file.endsWith ".lr.st" || file.endsWith ".laurel.st" do + IO.eprintln s!"Error: expected a .lr.st file, got: {file}" + return 1 + let path : System.FilePath := file + unless ← path.pathExists do + IO.eprintln s!"Error: file not found: {file}" + return 1 + let baseName := deriveBaseName file + + -- Use a temporary directory for intermediate files (cleaned up automatically) + IO.FS.withTempDir fun tmpDir => do + + -- Step 1: Laurel → GOTO JSON (in tmp dir) + let result ← (laurelAnalyzeToGoto path tmpDir baseName).toBaseIO + match result with + | .error e => + IO.eprintln s!"Error: {e}" + return 1 + | .ok () => pure () + + let symTabFile := (tmpDir / s!"{baseName}.symtab.json").toString + let gotoFile := (tmpDir / s!"{baseName}.goto.json").toString + let gbFile := (tmpDir / s!"{baseName}.gb").toString + let ccGbFile := (tmpDir / s!"{baseName}_cc.gb").toString + let dfccGbFile := (tmpDir / s!"{baseName}_dfcc.gb").toString + + -- Step 2: symtab2gb + let rc ← runProcess "symtab2gb" "symtab2gb" + #[symTabFile, "--goto-functions", gotoFile, "--out", gbFile] + if rc != 0 then return rc + + -- Step 3: goto-cc (add C scaffolding) + let gotoCC ← getEnvOrDefault "GOTO_CC" "goto-cc" + let rc ← runProcess "goto-cc" gotoCC + #["--function", "main", "-o", ccGbFile, gbFile] + if rc != 0 then return rc + + -- Step 4: goto-instrument --dfcc + let gotoInstrument ← getEnvOrDefault "GOTO_INSTRUMENT" "goto-instrument" + let rc ← runProcess "goto-instrument --dfcc" gotoInstrument + #["--dfcc", "main", ccGbFile, dfccGbFile] + if rc != 0 then return rc + + -- Step 5: cbmc verification + let cbmc ← getEnvOrDefault "CBMC" "cbmc" + runProcess "cbmc" cbmc + #[dfccGbFile, "--function", "main", "--z3", "--verbosity", "9"] + + | _ => + IO.eprintln "Usage: LaurelToCBMC " + return 1 diff --git a/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh b/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh index 47b1871cdc..cfd20dceda 100755 --- a/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh +++ b/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh @@ -8,7 +8,6 @@ set -eo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)" -LAUREL_TO_CBMC="$PROJECT_ROOT/StrataTest/Languages/Laurel/laurel_to_cbmc.sh" WORK=$(mktemp -d) trap 'rm -rf "$WORK"' EXIT @@ -26,7 +25,7 @@ procedure main() LAUREL # Run the full pipeline (strata → symtab2gb → goto-cc → goto-instrument → cbmc) -cbmc_out=$("$LAUREL_TO_CBMC" "$WORK/test.lr.st" 2>&1 || true) +cbmc_out=$(lake -d "$PROJECT_ROOT" env lean --run "$PROJECT_ROOT/Scripts/LaurelToCBMC.lean" "$WORK/test.lr.st" 2>&1 || true) # Verify CBMC output contains property summaries for summary in "addition equals eight" "difference equals two"; do diff --git a/StrataTest/Backends/CBMC/cbmc-string-support.patch b/StrataTest/Backends/CBMC/cbmc-string-support.patch new file mode 100644 index 0000000000..225f336438 --- /dev/null +++ b/StrataTest/Backends/CBMC/cbmc-string-support.patch @@ -0,0 +1,61 @@ +diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp +index e00becc56e..43bd7888d3 100644 +--- a/src/solvers/smt2/smt2_conv.cpp ++++ b/src/solvers/smt2/smt2_conv.cpp +@@ -2707,8 +2707,24 @@ void smt2_convt::convert_expr(const exprt &expr) + else if(expr.id() == ID_function_application) + { + const auto &function_application_expr = to_function_application_expr(expr); ++ ++ // Check for string operations by looking at the function symbol name ++ std::string fn_name; ++ if(function_application_expr.function().id() == ID_symbol) ++ fn_name = id2string( ++ to_symbol_expr(function_application_expr.function()).get_identifier()); ++ ++ if(fn_name == "Str.Concat" && ++ function_application_expr.arguments().size() == 2) ++ { ++ out << "(str.++ "; ++ convert_expr(function_application_expr.arguments()[0]); ++ out << ' '; ++ convert_expr(function_application_expr.arguments()[1]); ++ out << ')'; ++ } + // do not use parentheses if there function is a constant +- if(function_application_expr.arguments().empty()) ++ else if(function_application_expr.arguments().empty()) + { + convert_expr(function_application_expr.function()); + } +@@ -3763,6 +3779,21 @@ void smt2_convt::convert_constant(const constant_exprt &expr) + out << "(_ bv" << (value_int - range_type.get_from()) << " " << width + << ")"; + } ++ else if(expr_type.id()==ID_string) ++ { ++ const std::string &value = id2string(expr.get_value()); ++ out << "\""; ++ for(char c : value) ++ { ++ if(c == '"') ++ out << "\"\""; ++ else if(c == '\\') ++ out << "\\\\"; ++ else ++ out << c; ++ } ++ out << "\""; ++ } + else + UNEXPECTEDCASE("unknown constant: "+expr_type.id_string()); + } +@@ -5991,6 +6022,8 @@ void smt2_convt::convert_type(const typet &type) + UNEXPECTEDCASE("unsuppored range type"); + out << "(_ BitVec " << address_bits(size) << ")"; + } ++ else if(type.id()==ID_string) ++ out << "String"; + else + { + UNEXPECTEDCASE("unsupported type: "+type.id_string()); diff --git a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh index fd700d2a43..8ca1b74b17 100755 --- a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh +++ b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh @@ -8,12 +8,15 @@ # appears in CBMC output with the correct status. # # Environment variables: -# CBMC - path to cbmc binary (default: cbmc) +# CBMC - path to cbmc binary (default: cbmc) +# GOTO_CC - path to goto-cc binary (default: goto-cc) +# GOTO_INSTRUMENT - path to goto-instrument binary (default: goto-instrument) set -o pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" TESTS_DIR="$SCRIPT_DIR/tests" +PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" EXPECTED="$TESTS_DIR/cbmc_expected.txt" passed=0 @@ -40,7 +43,7 @@ for lr_file in "$TESTS_DIR"/*.lr.st; do fi # Run the pipeline - output=$("$SCRIPT_DIR/laurel_to_cbmc.sh" "$lr_file" 2>&1) + output=$(lake -d "$PROJECT_ROOT" env lean --run "$PROJECT_ROOT/Scripts/LaurelToCBMC.lean" "$lr_file" 2>&1) if [ $? -ne 0 ] && ! echo "$output" | grep -q "VERIFICATION"; then echo "ERR: $bn (pipeline error)" echo "$output" | tail -3 From d52ad5925353d774c67bcb0920547fe121af6f33 Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 19 Jun 2026 15:51:15 -0700 Subject: [PATCH 02/10] Laurel: pass translate options into LaurelPass.run Each `LaurelPass.run` now receives `LaurelTranslateOptions`, instead of passes being parameterized at construction. `LaurelTranslateOptions` moves into `LaurelPass`, the pipeline threads the options into every pass, and the `comesBefore` lists no longer carry an arbitrary placeholder argument. No behavioural change: every pass ignores the new argument here. --- .../Languages/Laurel/ConstrainedTypeElim.lean | 2 +- .../Languages/Laurel/DesugarShortCircuit.lean | 2 +- .../Laurel/EliminateDeterministicHoles.lean | 2 +- .../Laurel/EliminateValueInReturns.lean | 2 +- .../Languages/Laurel/HeapParameterization.lean | 2 +- Strata/Languages/Laurel/InferHoleTypes.lean | 2 +- .../Laurel/LaurelCompilationPipeline.lean | 9 +++++---- Strata/Languages/Laurel/LaurelPass.lean | 17 +++++++++++++++-- .../Laurel/LaurelToCoreTranslator.lean | 9 +-------- .../Laurel/LiftImperativeExpressions.lean | 2 +- .../Languages/Laurel/MergeAndLiftReturns.lean | 2 +- Strata/Languages/Laurel/ModifiesClauses.lean | 4 ++-- Strata/Languages/Laurel/TypeAliasElim.lean | 2 +- Strata/Languages/Laurel/TypeHierarchy.lean | 2 +- 14 files changed, 33 insertions(+), 26 deletions(-) diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean index 0d8e9fb387..4a3b45c199 100644 --- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean +++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean @@ -254,7 +254,7 @@ public def constrainedTypeElimPass : LaurelPass where name := "ConstrainedTypeElim" documentation := "Eliminates constrained types by replacing them with their base types and generating constraint-checking functions and witness procedures. Type tests against constrained types are rewritten to call the generated constraint function." needsResolves := true - run := fun p m => + run := fun _ p m => let (p', diags) := constrainedTypeElim m p (p', diags, {}) diff --git a/Strata/Languages/Laurel/DesugarShortCircuit.lean b/Strata/Languages/Laurel/DesugarShortCircuit.lean index acd1c02eb4..ba9e1d9645 100644 --- a/Strata/Languages/Laurel/DesugarShortCircuit.lean +++ b/Strata/Languages/Laurel/DesugarShortCircuit.lean @@ -58,7 +58,7 @@ end -- public section public def desugarShortCircuitPass : LaurelPass where name := "DesugarShortCircuit" documentation := "Rewrites short-circuit boolean operators (`&&` and `||`) into equivalent conditional expressions. This simplifies subsequent passes and the final translation to Core, which does not have short-circuit semantics built in." - run := fun p m => + run := fun _ p m => (desugarShortCircuit m p, [], {}) comesBefore := [ ⟨ liftExpressionAssignmentsPass, "The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass."⟩] diff --git a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean index c1784d41fc..28d16e53f0 100644 --- a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean +++ b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean @@ -93,7 +93,7 @@ end -- public section public def eliminateDeterministicHolesPass : LaurelPass where name := "EliminateDeterministicHoles" documentation := "Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes `InferHoleTypes` has already annotated holes with types." - run := fun p _m => + run := fun _ p _m => let (p', stats) := eliminateDeterministicHoles p (p', [], stats) diff --git a/Strata/Languages/Laurel/EliminateValueInReturns.lean b/Strata/Languages/Laurel/EliminateValueInReturns.lean index 938d3a00f0..d325937aa0 100644 --- a/Strata/Languages/Laurel/EliminateValueInReturns.lean +++ b/Strata/Languages/Laurel/EliminateValueInReturns.lean @@ -97,7 +97,7 @@ end -- public section public def eliminateValueInReturnsPass : LaurelPass where name := "EliminateValueInReturns" documentation := "Rewrites `return expr` into `outParam := expr; return` for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns." - run := fun p _m => + run := fun _ p _m => let (p', diags) := eliminateValueInReturnsTransform p (p', diags.toList, {}) comesBefore := [⟨ heapParameterizationPass, "eliminate value in returns need to come before any passes that change the amount of output parameters of procedures." ⟩] diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 13d8a2eced..c798d2b39a 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -580,7 +580,7 @@ public def heapParameterizationPass : LaurelPass where name := "HeapParameterization" documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions." needsResolves := true - run := fun p m => + run := fun _ p m => (heapParameterization m p, [], {}) comesBefore := [ ⟨ typeHierarchyTransformPass, "the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass." ⟩, diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean index 400de87c3a..efa17c33c5 100644 --- a/Strata/Languages/Laurel/InferHoleTypes.lean +++ b/Strata/Languages/Laurel/InferHoleTypes.lean @@ -195,7 +195,7 @@ end -- public section public def inferHoleTypesPass : LaurelPass where name := "InferHoleTypes" documentation := "Annotates every verification hole (`.Hole`) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values." - run := fun p m => + run := fun _ p m => let (p', diags, stats) := inferHoleTypes m p (p', diags, stats) comesBefore := [ diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index 57115a59cc..8103eaa9ad 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean @@ -130,7 +130,7 @@ program state after each named Laurel pass is written to `{prefix}.{n}.{passName}.laurel.st`. -/ private def runLaurelPasses - (pctx : Strata.Pipeline.PipelineContext) (program : Program) + (pctx : Strata.Pipeline.PipelineContext) (program : Program) (options : LaurelTranslateOptions) : PipelineM (Program × SemanticModel × List DiagnosticModel × Statistics) := do let program := { program with staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures, @@ -150,8 +150,9 @@ private def runLaurelPasses let mut allDiags : List DiagnosticModel := resolutionErrors let mut allStats : Statistics := {} - for pass in laurelPipeline do - let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model) + let passes := laurelPipeline + for pass in passes do + let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run options program model) program := program' allDiags := allDiags ++ diags allStats := allStats.merge stats @@ -180,7 +181,7 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program) | some ctx => pure ctx | none => Strata.Pipeline.PipelineContext.create (outputMode := .quiet) runPipelineM options.keepAllFilesPrefix do - let (program, model, passDiags, stats) ← runLaurelPasses pctx program + let (program, model, passDiags, stats) ← runLaurelPasses pctx program options let unorderedCore := transparencyPass program emit "transparencyPass" "core.st" unorderedCore diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean index 5a682db402..42e8d6ca4b 100644 --- a/Strata/Languages/Laurel/LaurelPass.lean +++ b/Strata/Languages/Laurel/LaurelPass.lean @@ -7,11 +7,24 @@ module public import Strata.Languages.Laurel.SemanticModel public import Strata.Util.Statistics +public import Strata.Languages.Core.Options namespace Strata.Laurel public section +/-- Options controlling Laurel-to-Core translation, threaded into every pass's `run`. -/ +structure LaurelTranslateOptions where + inlineFunctionsWhenPossible : Bool := false + overflowChecks : Core.OverflowChecks := {} + /-- Encode the heap `Map` as the SMT-LIB theory of arrays. Inside the modifies pass + this selects the enumerated (quantifier-free) frame for single-reference clauses. -/ + useArrayTheory : Bool := false + keepAllFilesPrefix : Option String := none + +instance : Inhabited LaurelTranslateOptions where + default := {} + mutual structure ComesBefore where pass : LaurelPass @@ -25,8 +38,8 @@ structure LaurelPass where name : String /-- Whether `resolve` should be run after the pass. -/ needsResolves : Bool := false - /-- The pass action. -/ - run : Program → SemanticModel → Program × List DiagnosticModel × Statistics + /-- The pass action; `options` carries the translate settings (e.g. the modifies-frame choice). -/ + run : LaurelTranslateOptions → Program → SemanticModel → Program × List DiagnosticModel × Statistics /-- A description of what this pass does, used for documentation generation. -/ documentation : String comesBefore : List ComesBefore := [] diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index f5c8d2bbab..d74ae2c8f7 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -8,6 +8,7 @@ module public import Strata.Languages.Core.Program public import Strata.Languages.Core.Options public import Strata.Languages.Laurel.CoreGroupingAndOrdering +public import Strata.Languages.Laurel.LaurelPass import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Util.Tactics public import Strata.Languages.Laurel.Resolution @@ -615,14 +616,6 @@ where let inner ← buildQuants rest body trigger return LExpr.all () p.name.text (some (← translateType p.type)) inner -structure LaurelTranslateOptions where - inlineFunctionsWhenPossible : Bool := false - overflowChecks : Core.OverflowChecks := {} - keepAllFilesPrefix : Option String := none - -instance : Inhabited LaurelTranslateOptions where - default := {} - structure LaurelVerifyOptions where translateOptions : LaurelTranslateOptions := {} verifyOptions : Core.VerifyOptions := .default diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 190df0031a..e064a10a23 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -539,7 +539,7 @@ end -- public section public def liftExpressionAssignmentsPass : LaurelPass where name := "LiftExpressionAssignments" documentation := "Lifts assignments that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed." - run := fun p m => + run := fun _ p m => (liftExpressionAssignments m p, [], {}) end Laurel diff --git a/Strata/Languages/Laurel/MergeAndLiftReturns.lean b/Strata/Languages/Laurel/MergeAndLiftReturns.lean index 567dd276fc..1f9deafab9 100644 --- a/Strata/Languages/Laurel/MergeAndLiftReturns.lean +++ b/Strata/Languages/Laurel/MergeAndLiftReturns.lean @@ -123,7 +123,7 @@ public def mergeAndLiftReturnsPass : LaurelPass where name := "MergeAndLiftReturns" documentation := "Attempts to merge and lift returns so that only a single outer return remains, enabling the procedure to be more easily converted to a functional form." needsResolves := true - run := fun p _m => + run := fun _ p _m => (mergeAndLiftReturns p, [], {}) end Laurel diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index f2fcc0a791..2b0f3ad603 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -237,7 +237,7 @@ end -- public section public def filterNonCompositeModifiesPass : LaurelPass where name := "FilterNonCompositeModifies" documentation := "Filters modifies clauses that refer to non-composite types (e.g. primitives), which cannot be heap-parameterized. Emits a warning for each removed clause. Should run before heap parameterization so that phase remains agnostic to modifies clauses." - run := fun p m => + run := fun _ p m => let (p', diags) := filterNonCompositeModifies m p (p', diags, {}) @@ -246,7 +246,7 @@ public def modifiesClausesTransformPass : LaurelPass where name := "ModifiesClausesTransform" documentation := "Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap." needsResolves := true - run := fun p m => + run := fun _ p m => let (p', diags) := modifiesClausesTransform m p (p', diags, {}) diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean index 1aa069e5f0..c5bffb9819 100644 --- a/Strata/Languages/Laurel/TypeAliasElim.lean +++ b/Strata/Languages/Laurel/TypeAliasElim.lean @@ -121,6 +121,6 @@ public def typeAliasElimPass : LaurelPass where name := "TypeAliasElim" documentation := "Eliminates type aliases by replacing all UserDefined references to alias names with their resolved target types. Chained aliases are resolved transitively. Alias entries are removed from the type list." needsResolves := true - run := fun p m => (typeAliasElim m p, [], {}) + run := fun _ p m => (typeAliasElim m p, [], {}) end Strata.Laurel diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index 599fc40492..31115b59a0 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -162,7 +162,7 @@ public def typeHierarchyTransformPass : LaurelPass where name := "TypeHierarchyTransform" documentation := "Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains." needsResolves := true - run := fun p m => + run := fun _ p m => (typeHierarchyTransform m p, [], {}) end Strata.Laurel From 49f5081cbc954fa94c1a62238f42c4d7890b1bba Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 19 Jun 2026 15:52:28 -0700 Subject: [PATCH 03/10] Laurel: quantifier-free modifies frame under --use-array-theory MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Under `--use-array-theory` the heap `Map` is an SMT array, so for a `modifies` clause naming only individual references we can emit an enumerated, quantifier-free frame (`buildEnumeratedFrame`: overwrite the named rows) instead of the `∀`-based `buildPointwiseFrame`. The dispatch (`onlyIndividualRefs`) is restricted to bodiless procedures: a body that allocates cannot prove the whole-array equality, so bodies keep the pointwise frame, whose `< nextReference` guard tolerates allocation. --- Strata/Cli/VerifyOptions.lean | 3 +- Strata/Languages/Laurel/ModifiesClauses.lean | 88 ++++++++++++++------ 2 files changed, 63 insertions(+), 28 deletions(-) diff --git a/Strata/Cli/VerifyOptions.lean b/Strata/Cli/VerifyOptions.lean index ac27060ebb..5329084559 100644 --- a/Strata/Cli/VerifyOptions.lean +++ b/Strata/Cli/VerifyOptions.lean @@ -173,7 +173,8 @@ def parseLaurelVerifyOptions (pflags : ParsedFlags) let translateOptions : LaurelTranslateOptions := { base.translateOptions with keepAllFilesPrefix - overflowChecks := verifyOptions.overflowChecks } + overflowChecks := verifyOptions.overflowChecks + useArrayTheory := verifyOptions.useArrayTheory } return { translateOptions, verifyOptions } end -- public section diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 2b0f3ad603..fec1bd9542 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -90,45 +90,75 @@ def conjoinAll (exprs : List StmtExprMd) : StmtExprMd := | first :: rest => rest.foldl (fun acc e => mkMd <| .PrimitiveOp .And [acc, e]) first /-- -Build the modifies frame condition as a Laurel StmtExpr. - -Generates a single quantified formula: +Pointwise frame: every allocated object the `modifies` clause does not name keeps +all of its field values across the call. forall $obj: Composite, $fld: Field => - notModified($obj) && $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld) - -Returns `none` if there are no entries. + $obj < $heap_in.nextReference && notModified($obj) + ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld) -/ -def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs : List StmtExprMd) - (heapInName heapOutName : Identifier) : Option StmtExprMd := - let entries := extractModifiesEntries model modifiesExprs +def buildPointwiseFrame (proc : Procedure) (entries : List ModifiesEntry) + (heapIn heapOut : StmtExprMd) : StmtExprMd := let objName : Identifier := "$modifies_obj" let fldName : Identifier := "$modifies_fld" let obj := mkMd <| .Var (.Local objName) let fld := mkMd <| .Var (.Local fldName) - let heapIn := mkMd <| .Var (.Local heapInName) - let heapOut := mkMd <| .Var (.Local heapOutName) - -- Build the "obj is allocated" condition: Composite..ref($obj) < $heap_in.nextReference let heapCounter := mkMd <| .StaticCall "Heap..nextReference!" [heapIn] let objRef := mkMd <| .StaticCall "Composite..ref!" [obj] let objAllocated := mkMd <| .PrimitiveOp .Lt [objRef, heapCounter] let antecedent := if entries.isEmpty then objAllocated else - -- Build the "not modified" precondition from all entries - -- Combine: $obj < $heap_in.nextReference && notModified($obj) let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj)) mkMd <| .PrimitiveOp .And [objAllocated, notModified] - -- Build: readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld) let readIn := mkMd <| .StaticCall "readField" [heapIn, obj, fld] let readOut := mkMd <| .StaticCall "readField" [heapOut, obj, fld] - let heapUnchanged := mkMd <| .PrimitiveOp .Eq [readIn, readOut] - -- Build: antecedent ==> heapUnchanged - let implBody := mkMd <| .PrimitiveOp .Implies [antecedent, heapUnchanged] - -- Build: forall $obj: Composite, $fld: Field => ... + let fieldUnchanged := mkMd <| .PrimitiveOp .Eq [readIn, readOut] + let implBody := mkMd <| .PrimitiveOp .Implies [antecedent, fieldUnchanged] let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .TTypedField { val := .TInt, source := none }, source := none } ⟩ none implBody - let outerForall : StmtExprMd := { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source } - some outerForall + { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source } + +/-- +Enumerated frame for a `modifies` clause naming only individual references: the +output heap's data equals the input's with just the named (changed) rows overwritten, +so the frame carries no quantifier. Reads of any untouched row collapse through the +array read-over-write axiom. `nextReference` is asserted monotone, so a procedure may +allocate fresh references but never reuses them. +-/ +def buildEnumeratedFrame (proc : Procedure) (entries : List ModifiesEntry) + (heapIn heapOut : StmtExprMd) : StmtExprMd := + let data h := mkMd <| .StaticCall "Heap..data!" [h] + let nextRef h := mkMd <| .StaticCall "Heap..nextReference!" [h] + let dataOut := data heapOut + let modifiedRefs := entries.filterMap fun e => match e with | .single r => some r | _ => none + let framedData := modifiedRefs.foldr + (fun ref acc => mkMd <| .StaticCall "update" [acc, ref, mkMd <| .StaticCall "select" [dataOut, ref]]) + (data heapIn) + let dataPreserved := mkMd <| .PrimitiveOp .Eq [dataOut, framedData] + let refsMonotone := mkMd <| .PrimitiveOp .Leq [nextRef heapIn, nextRef heapOut] + { val := .PrimitiveOp .And [dataPreserved, refsMonotone], source := proc.name.source } + +/-- True when the `modifies` clause is non-empty and names only individual references +(no set-valued entries), so the enumerated frame applies. -/ +def onlyIndividualRefs (entries : List ModifiesEntry) : Bool := + !entries.isEmpty && entries.all fun e => match e with | .single _ => true | _ => false + +/-- +Build the `modifies` frame condition relating a procedure's input and output heap. + +When `useEnumeratedFrame` is set and the clause names only individual references, +emit the quantifier-free `buildEnumeratedFrame`; every other case (set-valued or +empty `modifies`, or the flag off) uses the `∀`-based `buildPointwiseFrame`. +-/ +def buildModifiesEnsures (proc : Procedure) (model : SemanticModel) (modifiesExprs : List StmtExprMd) + (heapInName heapOutName : Identifier) (useEnumeratedFrame : Bool := false) : Option StmtExprMd := + let entries := extractModifiesEntries model modifiesExprs + let heapIn := mkMd <| .Var (.Local heapInName) + let heapOut := mkMd <| .Var (.Local heapOutName) + if useEnumeratedFrame && onlyIndividualRefs entries then + some (buildEnumeratedFrame proc entries heapIn heapOut) + else + some (buildPointwiseFrame proc entries heapIn heapOut) /-- Check whether a procedure has a `$heap` output parameter, @@ -152,7 +182,7 @@ If the modifies clause uses a wildcard (`*`), the frame condition is skipped entirely — the procedure may modify anything. -/ def transformModifiesClauses (model: SemanticModel) - (proc : Procedure) : Except (Array DiagnosticModel) Procedure := + (proc : Procedure) (useEnumeratedFrame : Bool := false) : Except (Array DiagnosticModel) Procedure := match proc.body with | .External => .ok proc | .Opaque postconds impl modifiesExprs => @@ -162,7 +192,11 @@ def transformModifiesClauses (model: SemanticModel) else if hasHeapOut proc then let heapInName := heapInVarName let heapName := heapVarName - let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName + -- Only bodiless procedures get the enumerated frame: a body that allocates cannot prove + -- the whole-array equality, so bodies keep the allocation-tolerant pointwise frame. + -- (`impl.isNone` is a conservative proxy for "cannot grow the heap".) + let enumerate := useEnumeratedFrame && impl.isNone + let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName enumerate let postconds' := match frameCondition with | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }] | none => postconds @@ -223,9 +257,9 @@ This is a Laurel → Laurel pass that should run after heap parameterization. Always returns the (best-effort) transformed program together with any diagnostics, so that later passes can continue and report additional errors. -/ -def modifiesClausesTransform (model: SemanticModel) (program : Program) : Program × List DiagnosticModel := +def modifiesClausesTransform (model: SemanticModel) (program : Program) (useEnumeratedFrame : Bool := false) : Program × List DiagnosticModel := let (procs', errors) := program.staticProcedures.foldl (fun (acc, errs) proc => - match transformModifiesClauses model proc with + match transformModifiesClauses model proc useEnumeratedFrame with | .ok proc' => (acc ++ [proc'], errs) | .error newErrs => (acc ++ [proc], errs ++ newErrs.toList) ) ([], []) @@ -246,8 +280,8 @@ public def modifiesClausesTransformPass : LaurelPass where name := "ModifiesClausesTransform" documentation := "Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap." needsResolves := true - run := fun _ p m => - let (p', diags) := modifiesClausesTransform m p + run := fun options p m => + let (p', diags) := modifiesClausesTransform m p (useEnumeratedFrame := options.useArrayTheory) (p', diags, {}) end Strata.Laurel From d5ece2c83765d27a6442a962ea45336f7d54501c Mon Sep 17 00:00:00 2001 From: Jules Date: Fri, 19 Jun 2026 15:53:26 -0700 Subject: [PATCH 04/10] Laurel: test the modifies frame Structural #guards that the enumerated frame is quantifier-free while the pointwise frame is not (ModifiesFrameQuantifierFreeTest), the array-theory path including allocating bodies (T2c), and a perf/completeness regression for a chained spec procedure (T2e). --- .../T2c_ModifiesClausesArrayTheory.lean | 112 ++++++++++++++++ .../Objects/T2e_ModifiesArrayTheoryPerf.lean | 121 ++++++++++++++++++ .../ModifiesFrameQuantifierFreeTest.lean | 34 +++++ 3 files changed, 267 insertions(+) create mode 100644 StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean create mode 100644 StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean create mode 100644 StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean new file mode 100644 index 0000000000..6bcb1971e4 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean @@ -0,0 +1,112 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +Under `--use-array-theory`, the `ModifiesClauses` pass emits a quantifier-free +heap-equation frame — + `data!($heap) == update(data!(old), ref, select(data!($heap), ref))` +— instead of the `forall obj fld. notModified(obj) ==> readField(old) == readField(new)` +form. The same procedures must verify under either encoding; this pins the +array-theory path. Mirrors `T2_ModifiesClauses` but with `useArrayTheory := true`. +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +#eval testLaurel + (options := { defaultLaurelTestOptions with + translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure modifyContainerOpaque(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := c#value + 1; + true +}; + +procedure caller() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var x: int := d#value; + var b: bool := modifyContainerOpaque(c); + assert x == d#value // pass: d#value is preserved (d ∉ modifies) +}; + +procedure multipleModifiesClauses(c: Container, d: Container, e: Container) + opaque + modifies c + modifies d +; + +procedure multipleModifiesClausesCaller() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var e: Container := new Container; + var x: int := e#value; + multipleModifiesClauses(c, d, e); + assert x == e#value // pass: e is preserved (not in the modifies set) +}; + +procedure newObjectDoNotCountForModifies() + opaque +{ + var c: Container := new Container; + c#value := 1 +}; + +// Regression: an allocating body verifies under array theory (bodies use the pointwise frame). +procedure allocatesInModifiesBody(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := c#value + 1; + var t: Container := new Container; + t#value := 99; + true +}; + +// Regression: a body that allocates via a CALL still verifies (the callee +// newObjectDoNotCountForModifies grows the heap); the pointwise frame tolerates it. +procedure allocatesViaCall(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := c#value + 1; + newObjectDoNotCountForModifies(); + true +}; + +// Soundness: writes outside the modifies clause are still rejected. + +procedure modifyContainerWithoutPermission2(c: Container, d: Container) +// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies d +{ + c#value := 2 +}; + +procedure modifyContainerWithoutPermission3(c: Container, d: Container) +// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved + opaque + modifies d +{ + var i: bool := modifyContainerOpaque(c) +}; +#end diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean new file mode 100644 index 0000000000..60f78db451 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean @@ -0,0 +1,121 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +Perf / regression: the array-theory frame is not merely faster, it is more +complete on heap-heavy code. + +`stress` makes a deep chain of opaque heap-modifying calls on freshly allocated +objects, then asserts that an object allocated *before* the chain is untouched. + + - Under the `∀` frame (array theory off) the solver cannot instantiate the + quantified frame across the whole chain: the assertion "could not be proved". + This is a definite verdict in ~2s, not a wall-clock timeout. + - Under the quantifier-free frame (`--use-array-theory`) the same assertion + verifies: each step is a `store` on a single row, so the read of the + untouched object is a pure array rewrite with nothing to instantiate. + +The two blocks are identical apart from `useArrayTheory`. + +Note: the `∀` outcome depends on the SMT solver's quantifier heuristics. If a +future solver discharges it, the annotation below must be updated. +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +-- ∀ frame (array theory off): the chain defeats quantifier instantiation. +#eval testLaurel + (options := { defaultLaurelTestOptions with + translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := false }, + verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := false } }) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure modifyOne(c: Container) + opaque + modifies c; + +procedure stress() + opaque + modifies * +{ + var target: Container := new Container; + var x: int := target#value; + var c0: Container := new Container; modifyOne(c0); + var c1: Container := new Container; modifyOne(c1); + var c2: Container := new Container; modifyOne(c2); + var c3: Container := new Container; modifyOne(c3); + var c4: Container := new Container; modifyOne(c4); + var c5: Container := new Container; modifyOne(c5); + var c6: Container := new Container; modifyOne(c6); + var c7: Container := new Container; modifyOne(c7); + var c8: Container := new Container; modifyOne(c8); + var c9: Container := new Container; modifyOne(c9); + var c10: Container := new Container; modifyOne(c10); + var c11: Container := new Container; modifyOne(c11); + var c12: Container := new Container; modifyOne(c12); + var c13: Container := new Container; modifyOne(c13); + var c14: Container := new Container; modifyOne(c14); + var c15: Container := new Container; modifyOne(c15); + var c16: Container := new Container; modifyOne(c16); + var c17: Container := new Container; modifyOne(c17); + var c18: Container := new Container; modifyOne(c18); + var c19: Container := new Container; modifyOne(c19); + assert x == target#value +//^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved +}; +#end + +-- Quantifier-free frame (--use-array-theory): the same program verifies. +#eval testLaurel + (options := { defaultLaurelTestOptions with + translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure modifyOne(c: Container) + opaque + modifies c; + +procedure stress() + opaque + modifies * +{ + var target: Container := new Container; + var x: int := target#value; + var c0: Container := new Container; modifyOne(c0); + var c1: Container := new Container; modifyOne(c1); + var c2: Container := new Container; modifyOne(c2); + var c3: Container := new Container; modifyOne(c3); + var c4: Container := new Container; modifyOne(c4); + var c5: Container := new Container; modifyOne(c5); + var c6: Container := new Container; modifyOne(c6); + var c7: Container := new Container; modifyOne(c7); + var c8: Container := new Container; modifyOne(c8); + var c9: Container := new Container; modifyOne(c9); + var c10: Container := new Container; modifyOne(c10); + var c11: Container := new Container; modifyOne(c11); + var c12: Container := new Container; modifyOne(c12); + var c13: Container := new Container; modifyOne(c13); + var c14: Container := new Container; modifyOne(c14); + var c15: Container := new Container; modifyOne(c15); + var c16: Container := new Container; modifyOne(c16); + var c17: Container := new Container; modifyOne(c17); + var c18: Container := new Container; modifyOne(c18); + var c19: Container := new Container; modifyOne(c19); + assert x == target#value +}; +#end diff --git a/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean new file mode 100644 index 0000000000..28f180660c --- /dev/null +++ b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean @@ -0,0 +1,34 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +Structural check, independent of the solver: the enumerated modifies frame +(`buildEnumeratedFrame`) must contain no quantifier, so there is nothing for the +solver to instantiate. The `∀`-based frame it replaces (`buildPointwiseFrame`) +does contain one; asserting both pins the property and shows the check +discriminates between the two encodings. +-/ + +import Strata.Languages.Laurel.ModifiesClauses + +open Strata.Laurel + +namespace StrataTest.Laurel.ModifiesFrameQuantifierFree + +private def selfRef : StmtExprMd := { val := .Var (.Local "self"), source := none } +private def heapIn : StmtExprMd := { val := .Var (.Local "$heap_in"), source := none } +private def heapOut : StmtExprMd := { val := .Var (.Local "$heap"), source := none } +private def singleRefModifies : List ModifiesEntry := [.single selfRef] + +/-- Whether the (pretty-printed) frame mentions a quantifier. -/ +private def hasQuantifier (e : StmtExprMd) : Bool := + let s := reprStr e + (s.splitOn "forall").length > 1 || (s.splitOn "exists").length > 1 + +#guard !hasQuantifier (buildEnumeratedFrame default singleRefModifies heapIn heapOut) +#guard hasQuantifier (buildPointwiseFrame default singleRefModifies heapIn heapOut) + +end StrataTest.Laurel.ModifiesFrameQuantifierFree From 56468d4a02270f7ab007a3314731f603b365b45a Mon Sep 17 00:00:00 2001 From: Jules Date: Mon, 22 Jun 2026 13:23:18 -0700 Subject: [PATCH 05/10] Laurel: extend the quantifier-free modifies frame to bodies For an individual-ref modifies clause under array theory, callers now assume the quantifier-free enumerated frame as a free ensures, while the body proves the allocation-tolerant pointwise frame via asserts inserted before every exit, so callers never assume the quantifier. This drops the bodiless-only restriction: allocating bodies and writes-via-calls verify, and illegal writes are still rejected. --- Strata/Languages/Laurel/ModifiesClauses.lean | 101 ++---- .../T2c_ModifiesClausesArrayTheory.lean | 14 + .../Objects/T2d_ModifiesFrameSoundness.lean | 298 ++++++++++++++++++ .../Laurel/ModifiesFrameExitChecksTest.lean | 32 ++ 4 files changed, 376 insertions(+), 69 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean create mode 100644 StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 0ace9a2fb1..46ff636e9a 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -10,28 +10,12 @@ public import Strata.Languages.Laurel.LaurelPass import Strata.Languages.Laurel.HeapParameterizationConstants import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Languages.Laurel.LaurelTypes +import Strata.Languages.Laurel.MapStmtExpr /- -Modifies clause transformation (Laurel → Laurel). - -Transforms procedures with modifies clauses by generating a frame condition -and conjoining it with the postcondition. After this pass, the modifies list -is cleared since its semantics have been absorbed into the postcondition. - -This pass should run after heap parameterization, which has already: -- Added explicit heap parameter ($heap as inout) -- Transformed field accesses to readField/updateField calls -- Collected field constants - -The frame condition states: for every object not mentioned in the modifies clause, -all field values are preserved between the input and output heaps. - -Generates: - forall $obj: Composite, $fld: Field => - $obj < old($heap).nextReference && notModified($obj) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld) - -where `notModified($obj)` is the conjunction of `$obj != e` for each single entry `e`, -and `!(select(s, $obj))` for each set entry `s`. +Modifies clause transformation (Laurel → Laurel), run after heap parameterization: +generate a frame per `modifies` clause and clear it. Under array theory with only +individual refs, callers assume a quantifier-free frame and the body checks it per exit. -/ namespace Strata.Laurel @@ -117,13 +101,8 @@ def buildPointwiseFrame (proc : Procedure) (entries : List ModifiesEntry) let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .UserDefined "Field", source := none } ⟩ none implBody { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source } -/-- -Enumerated frame for a `modifies` clause naming only individual references: the -output heap's data equals the input's with just the named (changed) rows overwritten, -so the frame carries no quantifier. Reads of any untouched row collapse through the -array read-over-write axiom. `nextReference` is asserted monotone, so a procedure may -allocate fresh references but never reuses them. --/ +/-- Quantifier-free frame: output `data` equals input with only the named rows +overwritten, and `nextReference` is monotone. -/ def buildEnumeratedFrame (proc : Procedure) (entries : List ModifiesEntry) (heapIn heapOut : StmtExprMd) : StmtExprMd := let data h := mkMd <| .StaticCall "Heap..data!" [h] @@ -142,22 +121,17 @@ def buildEnumeratedFrame (proc : Procedure) (entries : List ModifiesEntry) def onlyIndividualRefs (entries : List ModifiesEntry) : Bool := !entries.isEmpty && entries.all fun e => match e with | .single _ => true | _ => false -/-- -Build the `modifies` frame condition relating a procedure's input and output heap. - -When `useEnumeratedFrame` is set and the clause names only individual references, -emit the quantifier-free `buildEnumeratedFrame`; every other case (set-valued or -empty `modifies`, or the flag off) uses the `∀`-based `buildPointwiseFrame`. --/ -def buildModifiesEnsures (proc : Procedure) (model : SemanticModel) (modifiesExprs : List StmtExprMd) - (heapName : Identifier) (useEnumeratedFrame : Bool := false) : Option StmtExprMd := - let entries := extractModifiesEntries model modifiesExprs - let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapName))) - let heapOut := mkMd <| .Var (.Local heapName) - if useEnumeratedFrame && onlyIndividualRefs entries then - some (buildEnumeratedFrame proc entries heapIn heapOut) - else - some (buildPointwiseFrame proc entries heapIn heapOut) +/-- Assert `frame` before every exit of `body` (`return` and body-block `exit`) and at its end. -/ +def insertFrameChecks (proc : Procedure) (frame : StmtExprMd) (body : StmtExprMd) : StmtExprMd := + let src := proc.name.source + let check : StmtExprMd := { val := .Assert { condition := frame, summary := "modifies clause" }, source := src } + let wrap (e : StmtExprMd) : StmtExprMd := { val := .Block [check, e] none, source := e.source } + let beforeExits := mapStmtExpr (fun e => + match e.val with + | .Return _ => wrap e + | .Exit l => if l == bodyLabel then wrap e else e + | _ => e) body + { val := .Block [beforeExits, check] none, source := src } /-- Check whether a procedure has a `$heap` output parameter, @@ -166,39 +140,28 @@ indicating it mutates the heap. def hasHeapOut (proc : Procedure) : Bool := proc.outputs.any (fun p => p.name.text == "$heap") -/-- -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 < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)` - -If the modifies clause uses a wildcard (`*`), the frame condition is skipped -entirely — the procedure may modify anything. --/ +/-- Build and attach `proc`'s modifies frame, then clear the clause. -/ def transformModifiesClauses (model: SemanticModel) (proc : Procedure) (useEnumeratedFrame : Bool := false) : Except (Array DiagnosticModel) Procedure := match proc.body with | .External => .ok proc | .Opaque postconds impl modifiesExprs => 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 heapName := heapVarName - -- Only bodiless procedures get the enumerated frame: a body that allocates cannot prove - -- the whole-array equality, so bodies keep the allocation-tolerant pointwise frame. - -- (`impl.isNone` is a conservative proxy for "cannot grow the heap".) - let enumerate := useEnumeratedFrame && impl.isNone - let frameCondition := buildModifiesEnsures proc model modifiesExprs heapName enumerate - let postconds' := match frameCondition with - | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }] - | none => postconds - .ok { proc with body := .Opaque postconds' impl [] } + let entries := extractModifiesEntries model modifiesExprs + let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapVarName))) + let heapOut := mkMd <| .Var (.Local heapVarName) + let pointwise := buildPointwiseFrame proc entries heapIn heapOut + let useEnumerated := useEnumeratedFrame && onlyIndividualRefs entries + let framePost : Condition := + if useEnumerated then + { condition := buildEnumeratedFrame proc entries heapIn heapOut, + summary := "modifies clause", free := true } + else + { condition := pointwise, summary := "modifies clause" } + let impl' := if useEnumerated then impl.map (insertFrameChecks proc pointwise) else impl + .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] } else .ok proc | _ => .ok proc @@ -276,7 +239,7 @@ public def filterNonCompositeModifiesPass : LaurelPass where /-- Pipeline pass: translate modifies clauses into ensures clauses. -/ public def modifiesClausesTransformPass : LaurelPass where name := "ModifiesClausesTransform" - documentation := "Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap." + documentation := "Translate modifies clauses into frame conditions on the contract." needsResolves := true run := fun options p m => let (p', diags) := modifiesClausesTransform m p (useEnumeratedFrame := options.useArrayTheory) diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean index 6bcb1971e4..d516c972e3 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean @@ -109,4 +109,18 @@ procedure modifyContainerWithoutPermission3(c: Container, d: Container) { var i: bool := modifyContainerOpaque(c) }; + +// Soundness: an illegal write on an EARLY-RETURN path is rejected. Exercises the +// frame assert inserted before each exit, not just the fall-through tail. +procedure modifyOnEarlyReturnPath(c: Container, d: Container) returns (b: bool) +// ^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies d +{ + if c#value > 0 then { + c#value := 1; + return true + }; + return false +}; #end diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean new file mode 100644 index 0000000000..7cde154825 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean @@ -0,0 +1,298 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +Soundness of the quantifier-free modifies frame under `--use-array-theory`: illegal +writes are rejected, legal shapes verify, callers may assume the free frame, and a +fresh object exposed to a caller is not pinned by it. +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +private def arrayTheoryOpts := + { defaultLaurelTestOptions with + translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } } + +/-! ## 1. Illegal writes are rejected -/ + +#eval testLaurel (options := arrayTheoryOpts) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure writeNonFrameConditional(c: Container, d: Container) +// ^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies d +{ + if d#value > 0 then { + c#value := 7 + } +}; + +procedure writeAfterEarlyReturn(c: Container, d: Container) returns (b: bool) +// ^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies d +{ + if d#value > 100 then { + return true + }; + c#value := 7; + return false +}; + +procedure writeOneOfManyNonFrame(c: Container, d: Container, e: Container) +// ^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies c + modifies d +{ + e#value := 9 +}; + +procedure writeFrameAndNonFrame(c: Container, d: Container) +// ^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies c +{ + c#value := 1; + d#value := 2 +}; + +procedure writeNestedIf(c: Container, d: Container) +// ^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies d +{ + if d#value > 0 then { + if d#value > 5 then { + c#value := 1 + } + } +}; +#end + +/-! ## 2. Legal shapes still verify -/ + +#eval testLaurel (options := arrayTheoryOpts) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure writeFrameConditional(c: Container) + opaque + modifies c +{ + if c#value > 0 then { + c#value := c#value + 1 + } +}; + +procedure modifyThenEarlyReturn(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := 1; + if c#value > 0 then { + return true + }; + return false +}; + +procedure modifyTwoDeclared(c: Container, d: Container) + opaque + modifies c + modifies d +{ + c#value := 1; + d#value := 2 +}; + +procedure allocThenModifyDeclared(c: Container) + opaque + modifies c +{ + var t: Container := new Container; + t#value := 99; + c#value := 5 +}; +#end + +/-! ## 3. Callers may assume the free frame; it does not over-promise -/ + +#eval testLaurel (options := arrayTheoryOpts) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure bodyModifier(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := c#value + 1; + true +}; + +procedure allocatingBody(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := c#value + 1; + var t: Container := new Container; + t#value := 99; + true +}; + +procedure bodyModifierTwo(c: Container, d: Container) + opaque + modifies c + modifies d +{ + c#value := 1; + d#value := 2 +}; + +procedure callerUnrelatedPreserved() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var x: int := d#value; + var b: bool := bodyModifier(c); + assert x == d#value +}; + +procedure callerModifiedNotPreserved() + opaque +{ + var c: Container := new Container; + var x: int := c#value; + var b: bool := bodyModifier(c); + assert x == c#value +//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved +}; + +procedure callerExactValuePreserved() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + d#value := 5; + var b: bool := bodyModifier(c); + assert d#value == 5 +}; + +procedure callerOfAllocatingBody() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var x: int := d#value; + var b: bool := allocatingBody(c); + assert x == d#value +}; + +procedure callerMultiUnrelated() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var e: Container := new Container; + var x: int := e#value; + bodyModifierTwo(c, d); + assert x == e#value +}; +#end + +/-! ## 4. Multiple exits and bodiless/body parity -/ + +#eval testLaurel (options := arrayTheoryOpts) <| +#strata +program Laurel; +composite Container { + var value: int +} + +procedure multiExitAllLegal(c: Container) returns (b: bool) + opaque + modifies c +{ + c#value := 1; + if c#value > 0 then { + c#value := 2; + return true + }; + c#value := 3; + return false +}; + +procedure illegalAfterLegalEarlyExit(c: Container, d: Container) returns (b: bool) +// ^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold + opaque + modifies c +{ + if c#value > 0 then { + c#value := 1; + return true + }; + d#value := 9; + return false +}; + +procedure bodilessModifier(c: Container) + opaque + modifies c; + +procedure callerOfBodiless() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var x: int := d#value; + bodilessModifier(c); + assert x == d#value +}; +#end + +/-! ## 5. A fresh object exposed to a caller is not pinned by the frame -/ + +#eval testLaurel (options := arrayTheoryOpts) <| +#strata +program Laurel; +composite Container { + var value: int + var child: Container +} + +procedure stashFresh(c: Container) + opaque + modifies c +{ + var t: Container := new Container; + t#value := 42; + c#child := t +}; + +procedure callerCannotPinFreshField() + opaque +{ + var c: Container := new Container; + stashFresh(c); + assert c#child#value == 42 +//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved +}; +#end diff --git a/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean b/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean new file mode 100644 index 0000000000..51087b7eec --- /dev/null +++ b/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean @@ -0,0 +1,32 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +`insertFrameChecks` asserts the frame before every procedure exit (a `return` or an +`exit` of the body block) and at the fall-through tail, but not before an `exit` of +another label. Each wrap plus the tail adds one `assert`, so the counts pin which +exits are instrumented, including the `exit bodyLabel` arm no frontend reaches. +-/ + +import Strata.Languages.Laurel.ModifiesClauses + +open Strata.Laurel + +namespace StrataTest.Laurel.ModifiesFrameExitChecks + +private def frame : StmtExprMd := { val := .LiteralBool true, source := none } +private def node (e : StmtExpr) : StmtExprMd := { val := e, source := none } +private def assertCount (e : StmtExprMd) : Nat := + (reprStr e |>.splitOn "assert").length - 1 + +#guard assertCount (insertFrameChecks default frame (node (.Return none))) == 2 +#guard assertCount (insertFrameChecks default frame (node (.Exit bodyLabel))) == 2 +#guard assertCount (insertFrameChecks default frame (node (.Exit "loop"))) == 1 +#guard assertCount + (insertFrameChecks default frame + (node (.Block [node (.Exit bodyLabel), node (.Exit "loop")] none))) == 2 + +end StrataTest.Laurel.ModifiesFrameExitChecks From a826a38f1e61c5b1c429e01ba83683f7d63b2e4b Mon Sep 17 00:00:00 2001 From: Jules Date: Tue, 23 Jun 2026 09:41:26 -0700 Subject: [PATCH 06/10] Laurel: scope pointwise frame to its usage branch --- Strata/Languages/Laurel/ModifiesClauses.lean | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 46ff636e9a..04a3c4da62 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -152,16 +152,20 @@ def transformModifiesClauses (model: SemanticModel) let entries := extractModifiesEntries model modifiesExprs let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapVarName))) let heapOut := mkMd <| .Var (.Local heapVarName) - let pointwise := buildPointwiseFrame proc entries heapIn heapOut - let useEnumerated := useEnumeratedFrame && onlyIndividualRefs entries - let framePost : Condition := - if useEnumerated then + if useEnumeratedFrame && onlyIndividualRefs entries then + -- Callers assume the quantifier-free frame; the body re-checks the + -- pointwise frame at every exit. + let pointwise := buildPointwiseFrame proc entries heapIn heapOut + let framePost : Condition := { condition := buildEnumeratedFrame proc entries heapIn heapOut, summary := "modifies clause", free := true } - else - { condition := pointwise, summary := "modifies clause" } - let impl' := if useEnumerated then impl.map (insertFrameChecks proc pointwise) else impl - .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] } + let impl' := impl.map (insertFrameChecks proc pointwise) + .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] } + else + let framePost : Condition := + { condition := buildPointwiseFrame proc entries heapIn heapOut, + summary := "modifies clause" } + .ok { proc with body := .Opaque (postconds ++ [framePost]) impl [] } else .ok proc | _ => .ok proc From e327cb545eb7bccc29ef97482201470f305537d7 Mon Sep 17 00:00:00 2001 From: Jules Date: Tue, 23 Jun 2026 09:45:45 -0700 Subject: [PATCH 07/10] Laurel: rename translate option useArrayTheory to enumeratedModifiesClauses --- Strata/Cli/VerifyOptions.lean | 2 +- Strata/Languages/Laurel/LaurelPass.lean | 8 +++++--- Strata/Languages/Laurel/ModifiesClauses.lean | 2 +- .../Examples/Objects/T2c_ModifiesClausesArrayTheory.lean | 2 +- .../Examples/Objects/T2d_ModifiesFrameSoundness.lean | 2 +- .../Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean | 4 ++-- 6 files changed, 11 insertions(+), 9 deletions(-) diff --git a/Strata/Cli/VerifyOptions.lean b/Strata/Cli/VerifyOptions.lean index 5329084559..71d8d55e6d 100644 --- a/Strata/Cli/VerifyOptions.lean +++ b/Strata/Cli/VerifyOptions.lean @@ -174,7 +174,7 @@ def parseLaurelVerifyOptions (pflags : ParsedFlags) { base.translateOptions with keepAllFilesPrefix overflowChecks := verifyOptions.overflowChecks - useArrayTheory := verifyOptions.useArrayTheory } + enumeratedModifiesClauses := verifyOptions.useArrayTheory } return { translateOptions, verifyOptions } end -- public section diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean index 42e8d6ca4b..dfb04b577a 100644 --- a/Strata/Languages/Laurel/LaurelPass.lean +++ b/Strata/Languages/Laurel/LaurelPass.lean @@ -17,9 +17,11 @@ public section structure LaurelTranslateOptions where inlineFunctionsWhenPossible : Bool := false overflowChecks : Core.OverflowChecks := {} - /-- Encode the heap `Map` as the SMT-LIB theory of arrays. Inside the modifies pass - this selects the enumerated (quantifier-free) frame for single-reference clauses. -/ - useArrayTheory : Bool := false + /-- Select the enumerated (quantifier-free) modifies frame for clauses that name + only single references. This is only beneficial when the heap `Map` is encoded + with SMT-LIB array theory, so it is set together with the verifier's + `useArrayTheory`. -/ + enumeratedModifiesClauses : Bool := false keepAllFilesPrefix : Option String := none instance : Inhabited LaurelTranslateOptions where diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 04a3c4da62..823498d664 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -246,7 +246,7 @@ public def modifiesClausesTransformPass : LaurelPass where documentation := "Translate modifies clauses into frame conditions on the contract." needsResolves := true run := fun options p m => - let (p', diags) := modifiesClausesTransform m p (useEnumeratedFrame := options.useArrayTheory) + let (p', diags) := modifiesClausesTransform m p (useEnumeratedFrame := options.enumeratedModifiesClauses) (p', diags, {}) end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean index d516c972e3..b6c820e22d 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean @@ -20,7 +20,7 @@ open Strata #eval testLaurel (options := { defaultLaurelTestOptions with - translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true }, verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <| #strata program Laurel; diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean index 7cde154825..a4eb274bd9 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean @@ -17,7 +17,7 @@ open Strata private def arrayTheoryOpts := { defaultLaurelTestOptions with - translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true }, verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } } /-! ## 1. Illegal writes are rejected -/ diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean index 60f78db451..9b1acea61d 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean @@ -32,7 +32,7 @@ open Strata -- ∀ frame (array theory off): the chain defeats quantifier instantiation. #eval testLaurel (options := { defaultLaurelTestOptions with - translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := false }, + translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := false }, verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := false } }) <| #strata program Laurel; @@ -78,7 +78,7 @@ procedure stress() -- Quantifier-free frame (--use-array-theory): the same program verifies. #eval testLaurel (options := { defaultLaurelTestOptions with - translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true }, + translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true }, verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <| #strata program Laurel; From debf7fe6bd215d6f8fca3ef49a7b154bd34482b0 Mon Sep 17 00:00:00 2001 From: Jules Date: Tue, 23 Jun 2026 09:46:09 -0700 Subject: [PATCH 08/10] Laurel: document that set-valued modifies clauses keep the quantified frame --- Strata/Languages/Laurel/LaurelPass.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean index dfb04b577a..0dcb5f0260 100644 --- a/Strata/Languages/Laurel/LaurelPass.lean +++ b/Strata/Languages/Laurel/LaurelPass.lean @@ -17,10 +17,8 @@ public section structure LaurelTranslateOptions where inlineFunctionsWhenPossible : Bool := false overflowChecks : Core.OverflowChecks := {} - /-- Select the enumerated (quantifier-free) modifies frame for clauses that name - only single references. This is only beneficial when the heap `Map` is encoded - with SMT-LIB array theory, so it is set together with the verifier's - `useArrayTheory`. -/ + /-- Quantifier-free modifies frame for single-reference clauses. Set-valued entries + keep the quantified frame. Use with the verifier's `useArrayTheory`. -/ enumeratedModifiesClauses : Bool := false keepAllFilesPrefix : Option String := none From 2d04b8f1f8ece4402706a10568b34fe857c1ed62 Mon Sep 17 00:00:00 2001 From: Jules Date: Tue, 23 Jun 2026 09:48:45 -0700 Subject: [PATCH 09/10] Laurel: rename buildPointwiseFrame to buildQuantifiedFrame --- Strata/Languages/Laurel/ModifiesClauses.lean | 8 ++++---- .../Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 823498d664..577aec759a 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -74,13 +74,13 @@ def conjoinAll (exprs : List StmtExprMd) : StmtExprMd := | first :: rest => rest.foldl (fun acc e => mkMd <| .PrimitiveOp .And [acc, e]) first /-- -Pointwise frame: every allocated object the `modifies` clause does not name keeps +Quantified (pointwise) frame: every allocated object the `modifies` clause does not name keeps all of its field values across the call. forall $obj: Composite, $fld: Field => notModified($obj) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld) -/ -def buildPointwiseFrame (proc : Procedure) (entries : List ModifiesEntry) +def buildQuantifiedFrame (proc : Procedure) (entries : List ModifiesEntry) (heapIn heapOut : StmtExprMd) : StmtExprMd := let objName : Identifier := "$modifies_obj" let fldName : Identifier := "$modifies_fld" @@ -155,7 +155,7 @@ def transformModifiesClauses (model: SemanticModel) if useEnumeratedFrame && onlyIndividualRefs entries then -- Callers assume the quantifier-free frame; the body re-checks the -- pointwise frame at every exit. - let pointwise := buildPointwiseFrame proc entries heapIn heapOut + let pointwise := buildQuantifiedFrame proc entries heapIn heapOut let framePost : Condition := { condition := buildEnumeratedFrame proc entries heapIn heapOut, summary := "modifies clause", free := true } @@ -163,7 +163,7 @@ def transformModifiesClauses (model: SemanticModel) .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] } else let framePost : Condition := - { condition := buildPointwiseFrame proc entries heapIn heapOut, + { condition := buildQuantifiedFrame proc entries heapIn heapOut, summary := "modifies clause" } .ok { proc with body := .Opaque (postconds ++ [framePost]) impl [] } else diff --git a/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean index 28f180660c..6dd53c1b45 100644 --- a/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean +++ b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean @@ -7,7 +7,7 @@ /- Structural check, independent of the solver: the enumerated modifies frame (`buildEnumeratedFrame`) must contain no quantifier, so there is nothing for the -solver to instantiate. The `∀`-based frame it replaces (`buildPointwiseFrame`) +solver to instantiate. The `∀`-based frame it replaces (`buildQuantifiedFrame`) does contain one; asserting both pins the property and shows the check discriminates between the two encodings. -/ @@ -29,6 +29,6 @@ private def hasQuantifier (e : StmtExprMd) : Bool := (s.splitOn "forall").length > 1 || (s.splitOn "exists").length > 1 #guard !hasQuantifier (buildEnumeratedFrame default singleRefModifies heapIn heapOut) -#guard hasQuantifier (buildPointwiseFrame default singleRefModifies heapIn heapOut) +#guard hasQuantifier (buildQuantifiedFrame default singleRefModifies heapIn heapOut) end StrataTest.Laurel.ModifiesFrameQuantifierFree From 622f60c2c0412bb330ecfc804e31620add4eec48 Mon Sep 17 00:00:00 2001 From: Jules Date: Tue, 23 Jun 2026 09:50:16 -0700 Subject: [PATCH 10/10] Laurel: drop redundant useEnumeratedFrame defaults in helpers --- Strata/Languages/Laurel/ModifiesClauses.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 577aec759a..ace1777ee1 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -142,7 +142,7 @@ def hasHeapOut (proc : Procedure) : Bool := /-- Build and attach `proc`'s modifies frame, then clear the clause. -/ def transformModifiesClauses (model: SemanticModel) - (proc : Procedure) (useEnumeratedFrame : Bool := false) : Except (Array DiagnosticModel) Procedure := + (proc : Procedure) (useEnumeratedFrame : Bool) : Except (Array DiagnosticModel) Procedure := match proc.body with | .External => .ok proc | .Opaque postconds impl modifiesExprs => @@ -222,7 +222,7 @@ This is a Laurel → Laurel pass that should run after heap parameterization. Always returns the (best-effort) transformed program together with any diagnostics, so that later passes can continue and report additional errors. -/ -def modifiesClausesTransform (model: SemanticModel) (program : Program) (useEnumeratedFrame : Bool := false) : Program × List DiagnosticModel := +def modifiesClausesTransform (model: SemanticModel) (program : Program) (useEnumeratedFrame : Bool) : Program × List DiagnosticModel := let (procs', errors) := program.staticProcedures.foldl (fun (acc, errs) proc => match transformModifiesClauses model proc useEnumeratedFrame with | .ok proc' => (acc ++ [proc'], errs)