diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d01fc1ed7c..87c3f2190d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -324,6 +324,7 @@ jobs: strata-benchmarks: name: Run internal benchmarks of Strata + if: github.repository == 'strata-org/Strata' runs-on: ubuntu-latest permissions: id-token: write diff --git a/Examples/expected/HeapReasoning.core.expected b/Examples/expected/HeapReasoning.core.expected index f19f38c7a6..a936adc936 100644 --- a/Examples/expected/HeapReasoning.core.expected +++ b/Examples/expected/HeapReasoning.core.expected @@ -2,7 +2,6 @@ Successfully parsed. HeapReasoning.core.st(98, 2) [modifiesFrameRef1]: ✅ pass HeapReasoning.core.st(103, 2) [modifiesFrameRef1]: ✅ pass HeapReasoning.core.st(108, 2) [modifiesFrameRef1]: ✅ pass - [Container_ctor_ensures_4]: ✅ pass HeapReasoning.core.st(86, 2) [Container_ctor_ensures_7]: ✅ pass HeapReasoning.core.st(87, 2) [Container_ctor_ensures_8]: ✅ pass HeapReasoning.core.st(88, 2) [Container_ctor_ensures_9]: ✅ pass @@ -12,7 +11,6 @@ HeapReasoning.core.st(169, 2) [modifiesFrameRef2]: ✅ pass HeapReasoning.core.st(172, 2) [modifiesFrameRef1Next]: ✅ pass HeapReasoning.core.st(177, 2) [modifiesFrameRef2Next]: ✅ pass HeapReasoning.core.st(132, 2) [UpdateContainers_ensures_5]: ✅ pass - [UpdateContainers_ensures_6]: ✅ pass HeapReasoning.core.st(150, 2) [UpdateContainers_ensures_14]: ✅ pass HeapReasoning.core.st(151, 2) [UpdateContainers_ensures_15]: ✅ pass HeapReasoning.core.st(152, 2) [UpdateContainers_ensures_16]: ✅ pass @@ -51,5 +49,4 @@ HeapReasoning.core.st(238, 2) [c2Pineapple0]: ✅ pass HeapReasoning.core.st(240, 2) [c1NextEqC2]: ✅ pass HeapReasoning.core.st(241, 2) [c2NextEqC1]: ✅ pass HeapReasoning.core.st(195, 2) [Main_ensures_1]: ✅ pass - [Main_ensures_2]: ✅ pass -All 53 goals passed. +All 50 goals passed. diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index 9ea328f41b..fcf6721d20 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -93,13 +93,13 @@ def eval (E : Env) (p : Procedure) : Env × Statistics := match check.attr with | .Free => -- NOTE: A free postcondition is not checked. - -- We simply change a free-postcondition to "true", but + -- We simply change a free-postcondition to "assume true", but -- keep a record in the metadata field. -- TODO: Perhaps introduce an "opaque" expression construct -- that hides the expression from the evaluator, allowing us -- to retain the postcondition body instead of replacing it -- with "true". - (.assert label (.true ()) + (.assume label (.true ()) ((Imperative.MetaData.pushElem #[] (.label label) diff --git a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean index 2df59b8ceb..23b8a2ec7b 100644 --- a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean +++ b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean @@ -27,16 +27,21 @@ program Laurel; datatype LaurelResolutionErrorPlaceholder {} datatype Float64IsNotSupportedYet {} +datatype LaurelUnit { MkLaurelUnit() } // The types for these Map functions are incorrect. // We'll fix them when Laurel supports polymorphism -function select(map: int, key: int) : int +// And then we can remove the datatype Box as well +// And remove the hacky filter in HeapParameterization +datatype Box { MkBox() } + +function select(map: int, key: int) : Box external; -function update(map: int, key: int, value: int) : int +function update(map: int, key: int, value: int) : Box external; -function const(value: int) : int +function const(value: int) : Box external; #end diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index f75057d88f..77b51d869f 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -5,9 +5,10 @@ -/ module -public import Strata.Languages.Laurel.Laurel +public import Strata.Languages.Laurel.TransparencyPass import Strata.DL.Lambda.LExpr import Strata.DDM.Util.Graph.Tarjan +import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator /-! ## Grouping and Ordering for Core Translation @@ -15,8 +16,6 @@ import Strata.DDM.Util.Graph.Tarjan Utilities for computing the grouping and topological ordering of Laurel declarations before they are emitted as Strata Core declarations. -- `groupDatatypesByScc` — groups mutually recursive datatypes into SCC groups - using Tarjan's SCC algorithm. - `computeSccDecls` — builds the procedure call graph, runs Tarjan's SCC algorithm, and returns each SCC as a list of procedures paired with a flag indicating whether the SCC is recursive. The result is in reverse topological @@ -90,7 +89,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String := | .InstanceCall t _ args => collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a) | .Old v | .Fresh v | .Assume v => collectStaticCallNames v - | .Assert ⟨cond, _summary⟩ => collectStaticCallNames cond + | .Assert ⟨cond, _summary, _⟩ => collectStaticCallNames cond | .ProveBy v p => collectStaticCallNames v ++ collectStaticCallNames p | .ReferenceEquals l r => collectStaticCallNames l ++ collectStaticCallNames r | .AsType t _ | .IsType t _ => collectStaticCallNames t @@ -113,27 +112,24 @@ Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC as a list of procedures paired with a flag indicating whether the SCC is recursive. Results are in reverse topological order: dependencies before dependents. -Procedures with an `invokeOn` trigger are placed as early as possible — before -unrelated procedures without one — by stably partitioning them first before building +Procedures with `invokeOn` are placed as early as possible — before +unrelated procedures without them — by stably partitioning them first before building the graph. Tarjan then naturally assigns them lower indices, causing them to appear earlier in the output. - -External procedures are excluded. -/ -public def computeSccDecls (program : Program) : List (List Procedure × Bool) := - -- External procedures are completely ignored (not translated to Core). +public def computeSccDecls (program : UnorderedCoreWithLaurelTypes) : List (List Procedure × Bool) := -- Stable partition: procedures with invokeOn come first, preserving relative -- order within each group. Tarjan then places them earlier in the topological output. + let allProcs := program.functions ++ program.coreProcedures let (withInvokeOn, withoutInvokeOn) := - (program.staticProcedures.filter (fun p => !p.body.isExternal)) - |>.partition (fun p => p.invokeOn.isSome) - let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn + allProcs.partition (fun p => p.invokeOn.isSome) + let orderedProcs : List Procedure := withInvokeOn ++ withoutInvokeOn - -- Build a call-graph over all non-external procedures. + -- Build a call-graph over all procedures. -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee. - let nonExternalArr : Array Procedure := nonExternal.toArray + let procsArr : Array Procedure := orderedProcs.toArray let nameToIdx : Std.HashMap String Nat := - nonExternalArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc => + procsArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc => (acc.1.insert proc.name.text acc.2, acc.2 + 1)) ({}, 0) |>.1 -- Collect all callee names from a procedure's body and contracts. @@ -149,9 +145,9 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) : (bodyExprs ++ contractExprs).flatMap collectStaticCallNames -- Build the OutGraph for Tarjan. - let n := nonExternalArr.size + let n := procsArr.size let graph : Strata.OutGraph n := - nonExternalArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc => + procsArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc => let callerIdx := acc.2 let g := acc.1 let callees := procCallees proc @@ -167,7 +163,7 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) : sccs.toList.filterMap fun scc => let procs := scc.toList.filterMap fun idx => - nonExternalArr[idx.val]? + procsArr[idx.val]? if procs.isEmpty then none else let isRecursive := procs.length > 1 || (match scc.toList.head? with @@ -176,60 +172,85 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) : some (procs, isRecursive) /-- -A single declaration in an ordered Laurel program. Declarations are in +A single declaration in a CoreWithLaurelTypes program. Declarations are in dependency order (dependencies before dependents). -/ public inductive OrderedDecl where - /-- A group of functions (single non-recursive, or mutually recursive). -/ - | procs (procs : List Procedure) (isRecursive : Bool) + /-- A group of functions (single non-recursive, or mutually recursive). + Invariant: `funcs.length > 1 → isRecursive = true`. -/ + | funcs (funcs : List Procedure) (isRecursive : Bool) + /-- A single (non-functional) procedure. -/ + | procedure (procedure : Procedure) /-- A group of (possibly mutually recursive) datatypes. -/ | datatypes (dts : List DatatypeDefinition) /-- A named constant. -/ | constant (c : Constant) /-- -A Laurel program whose declarations have been grouped and topologically ordered. -Produced by `orderProgram` from a `Program`. +A program whose declarations have been grouped and topologically ordered, +using Laurel types. Produced by `orderFunctionsAndProcedures` from a +`UnorderedCoreWithLaurelTypes`. -/ -public structure OrderedLaurel where +public structure CoreWithLaurelTypes where decls : List OrderedDecl -/-- -Group mutually recursive datatypes into SCC groups using Tarjan's SCC algorithm. -Returns groups in topological order (dependencies before dependents). --/ -public def groupDatatypesByScc (program : Program) : List (List DatatypeDefinition) := - let laurelDatatypes := program.types.filterMap fun td => match td with - | .Datatype dt => some dt - | _ => none - let n := laurelDatatypes.length - if n == 0 then [] else - let nameToIdx : Std.HashMap String Nat := - laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {} - let edges : List (Nat × Nat) := - laurelDatatypes.foldlIdx (fun acc i dt => - (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) [] - let g := OutGraph.ofEdges! n edges - let dtsArr := laurelDatatypes.toArray - OutGraph.tarjan g |>.toList.filterMap fun comp => - let members := comp.toList.filterMap fun idx => dtsArr[idx]? - if members.isEmpty then none else some members +open Std (Format ToFormat) -/-- -Group procedures into SCC groups and wrap them as `OrderedDecl.procs`. --/ -public def groupProcsByScc (program : Program) : List OrderedDecl := - (computeSccDecls program).map fun (procs, isRecursive) => - OrderedDecl.procs procs isRecursive +public section + +def formatOrderedDecl : OrderedDecl → Format + | .funcs funcs _ => Format.joinSep (funcs.map ToFormat.format) "\n\n" + | .procedure proc => ToFormat.format proc + | .datatypes dts => Format.joinSep (dts.map ToFormat.format) "\n\n" + | .constant c => ToFormat.format c + +instance : ToFormat OrderedDecl where + format := formatOrderedDecl + +def formatCoreWithLaurelTypes (p : CoreWithLaurelTypes) : Format := + Format.joinSep (p.decls.map formatOrderedDecl) "\n\n" + +instance : ToFormat CoreWithLaurelTypes where + format := formatCoreWithLaurelTypes + +end -- public section /-- -Produce an `OrderedLaurel` from a `Program` by grouping and ordering -procedures via SCC, collecting datatypes, and constants. +Produce a `CoreWithLaurelTypes` from a `UnorderedCoreWithLaurelTypes` by +computing a combined ordering of functions and proofs using the call graph, +then collecting datatypes and constants. + +Functions are grouped into SCCs (for mutual recursion). Proofs are emitted +as individual `procedure` decls. Both participate in the topological ordering +so that axioms are available to functions that need them. -/ -public def orderProgram (program : Program) : OrderedLaurel := - let datatypeDecls := (groupDatatypesByScc program).map OrderedDecl.datatypes +public def orderFunctionsAndProcedures (program : UnorderedCoreWithLaurelTypes) : CoreWithLaurelTypes := + let datatypeDecls := (groupDatatypesByScc' program).map OrderedDecl.datatypes let constantDecls := program.constants.map OrderedDecl.constant - let procDecls := groupProcsByScc program - { decls := datatypeDecls ++ constantDecls ++ procDecls } + let funcNames : Std.HashSet String := + program.functions.foldl (fun s p => s.insert p.name.text) {} + let orderedDecls := (computeSccDecls program).flatMap fun (procs, isRecursive) => + -- Split the SCC into functions and proofs + let (funcs, proofs) := procs.partition (fun p => funcNames.contains p.name.text) + let funcDecl := if funcs.isEmpty then [] else [OrderedDecl.funcs funcs isRecursive] + let proofDecls := proofs.map OrderedDecl.procedure + funcDecl ++ proofDecls + { decls := datatypeDecls ++ constantDecls ++ orderedDecls } +where + /-- Group datatypes from a UnorderedCoreWithLaurelTypes by SCC. -/ + groupDatatypesByScc' (program : UnorderedCoreWithLaurelTypes) : List (List DatatypeDefinition) := + let laurelDatatypes := program.datatypes + let n := laurelDatatypes.length + if n == 0 then [] else + let nameToIdx : Std.HashMap String Nat := + laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {} + let edges : List (Nat × Nat) := + laurelDatatypes.foldlIdx (fun acc i dt => + (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) [] + let g := OutGraph.ofEdges! n edges + let dtsArr := laurelDatatypes.toArray + OutGraph.tarjan g |>.toList.filterMap fun comp => + let members := comp.toList.filterMap fun idx => dtsArr[idx]? + if members.isEmpty then none else some members end Strata.Laurel diff --git a/Strata/Languages/Laurel/DesugarShortCircuit.lean b/Strata/Languages/Laurel/DesugarShortCircuit.lean index 6f4e9c5218..cea271aeeb 100644 --- a/Strata/Languages/Laurel/DesugarShortCircuit.lean +++ b/Strata/Languages/Laurel/DesugarShortCircuit.lean @@ -26,7 +26,7 @@ public section private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩ /-- Local rewrite of a single short-circuit node. Recursion is handled by `mapStmtExpr`. -/ -private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd := +private def desugarShortCircuitNode (imperativeCallees : List String) (expr : StmtExprMd) : StmtExprMd := let source := expr.source match expr.val with | .PrimitiveOp op args => @@ -35,20 +35,22 @@ private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) -- short-circuits converted to IfThenElse). The check still works because -- `containsAssignmentOrImperativeCall` recurses into IfThenElse. | .AndThen, [a, b] | .Implies, [a, b] => - if containsAssignmentOrImperativeCall model b then + if containsAssignmentOrImperativeCall imperativeCallees b then let elseVal := match op with | .AndThen => false | _ => true ⟨.IfThenElse a b (some (bare (.LiteralBool elseVal))), source⟩ else expr | .OrElse, [a, b] => - if containsAssignmentOrImperativeCall model b then + if containsAssignmentOrImperativeCall imperativeCallees b then ⟨.IfThenElse a (bare (.LiteralBool true)) (some b), source⟩ else expr | _, _ => expr | _ => expr /-- Desugar short-circuit operators in a program. -/ -def desugarShortCircuit (model : SemanticModel) (program : Program) : Program := - mapProgram (mapStmtExpr (desugarShortCircuitNode model)) program +def desugarShortCircuit (_model : SemanticModel) (program : Program) : Program := + let imperativeCallees := program.staticProcedures.filter (fun p => !p.isFunctional) + |>.map (fun p => p.name.text) + mapProgram (mapStmtExpr (desugarShortCircuitNode imperativeCallees)) program end -- public section end Strata.Laurel diff --git a/Strata/Languages/Laurel/EliminateValueReturns.lean b/Strata/Languages/Laurel/EliminateValueReturns.lean index f465c6055c..f80d6f8dd4 100644 --- a/Strata/Languages/Laurel/EliminateValueReturns.lean +++ b/Strata/Languages/Laurel/EliminateValueReturns.lean @@ -6,6 +6,7 @@ module public import Strata.Languages.Laurel.MapStmtExpr +public import Strata.Languages.Laurel.TransparencyPass /-! # Eliminate Value Returns @@ -79,13 +80,15 @@ def eliminateValueReturnsInProc (proc : Procedure) : Procedure × Array Diagnost public section -/-- Transform a program by eliminating value returns in all imperative procedures. -/ -def eliminateValueReturnsTransform (program : Program) : Program × Array DiagnosticModel := - let (procs, diags) := program.staticProcedures.foldl (fun (ps, ds) proc => +/-- Transform an `UnorderedCoreWithLaurelTypes` by eliminating value returns + in all core (non-functional) procedures. -/ +def eliminateValueReturnsTransform (uc : UnorderedCoreWithLaurelTypes) + : UnorderedCoreWithLaurelTypes × Array DiagnosticModel := + let (procs, diags) := uc.coreProcedures.foldl (fun (ps, ds) proc => let (proc', procDiags) := eliminateValueReturnsInProc proc (proc' :: ps, ds ++ procDiags) ) ([], #[]) - ({ program with staticProcedures := procs.reverse }, diags) + ({ uc with coreProcedures := procs.reverse }, diags) end -- public section diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index c185d90edc..02e2159643 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/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: block format uses indent(2) with leading spaces for vertical layout. +-- Last grammar change: multiAssign supports field access targets, added opaque keyword. public import Strata.DDM.Integration.Lean public meta import Strata.DDM.Integration.Lean diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index f68b93c031..7f3eb48250 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -84,7 +84,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do | .Assigned n => collectExprMd n | .Old v => collectExprMd v | .Fresh v => collectExprMd v - | .Assert ⟨c, _⟩ => collectExprMd c + | .Assert ⟨c, _, _⟩ => collectExprMd c | .Assume c => collectExprMd c | .ProveBy v p => collectExprMd v; collectExprMd p | .ContractOf _ f => collectExprMd f @@ -433,8 +433,8 @@ where | .Assigned n => return ⟨ .Assigned (← recurse n), source ⟩ | .Old v => return ⟨ .Old (← recurse v), source ⟩ | .Fresh v => return ⟨ .Fresh (← recurse v), source ⟩ - | .Assert ⟨condExpr, summary⟩ => - return ⟨ .Assert { condition := ← recurse condExpr, summary }, source ⟩ + | .Assert ⟨condExpr, summary, free⟩ => + return ⟨ .Assert { condition := ← recurse condExpr, summary, free }, source ⟩ | .Assume c => return ⟨ .Assume (← recurse c), source ⟩ | .ProveBy v p => return ⟨ .ProveBy (← recurse v) (← recurse p), source ⟩ | .ContractOf ty f => return ⟨ .ContractOf ty (← recurse f), source ⟩ @@ -566,9 +566,14 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program := -- Generate Box datatype from all constructors used during transformation let boxDatatype : TypeDefinition := .Datatype { name := "Box", typeArgs := [], constructors := state2.usedBoxConstructors } + let types := fieldDatatype :: boxDatatype :: heapConstants.types ++ + -- The filter is a hack to deal with another hack, + -- the box that was added in CoreDefinitionsForLaurel.lean + -- because Laurel does not support polymorphism yet + types'.filter (fun td => td.name.text != "Box") { program with staticProcedures := heapConstants.staticProcedures ++ procs', - types := fieldDatatype :: boxDatatype :: heapConstants.types ++ types' } + types } end Strata.Laurel diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean index d56ad86881..c184995e35 100644 --- a/Strata/Languages/Laurel/InferHoleTypes.lean +++ b/Strata/Languages/Laurel/InferHoleTypes.lean @@ -139,9 +139,10 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol | some d => pure (some (← inferExpr d (⟨ .TInt, source ⟩))) | none => pure none return ⟨.While (← inferExpr cond ⟨ .TBool, source ⟩) (← invs.mapM (inferExpr · ⟨ .TBool, source ⟩)) dec' (← inferExpr body ⟨ .TVoid, source⟩), source⟩ - | .Assert ⟨condExpr, summary⟩ => - return ⟨.Assert { condition := ← inferExpr condExpr ⟨ .TBool, source ⟩, summary }, source⟩ - | .Assume cond => return ⟨.Assume (← inferExpr cond ⟨ .TBool, source ⟩), source⟩ + | .Assert ⟨condExpr, summary, free⟩ => + return ⟨.Assert { condition := ← inferExpr condExpr ⟨ .TBool, source ⟩, summary, free }, source⟩ + | .Assume cond => + return ⟨.Assume (← inferExpr cond ⟨ .TBool, source ⟩), source⟩ | .Return (some retExpr) => return ⟨.Return (some (← inferExpr retExpr (← get).currentOutputType)), source⟩ | .Old v => return ⟨.Old (← inferExpr v expectedType), source⟩ @@ -170,6 +171,7 @@ private def inferProcedure (proc : Procedure) : InferHoleM Procedure := do /-- Annotate every `.Hole` in the program with a type inferred from context. +Returns the updated program and any diagnostics (e.g. holes whose type could not be inferred). -/ def inferHoleTypes (model : SemanticModel) (program : Program) : Program × List DiagnosticModel × Statistics := let initState : InferHoleState := { model := model, currentOutputType := { val := .Unknown, source := none }} diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index a5cd11439c..442985f73b 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -219,6 +219,11 @@ structure Condition where condition : AstNode StmtExpr /-- Optional human-readable summary describing the property being checked. -/ summary : Option String := none + /-- When `true`, this condition is *free*: assumed but not checked. + A free precondition is assumed by the implementation but not asserted at + call sites. A free postcondition is assumed upon return from calls but + not checked on exit from implementations. -/ + free : Bool := false /-- The body of a procedure. A body can be transparent (with a visible diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index 011e4d536f..506939a724 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean @@ -8,8 +8,11 @@ module public import Strata.Languages.Laurel.LaurelToCoreTranslator import Strata.Languages.Laurel.DesugarShortCircuit import Strata.Languages.Laurel.EliminateReturnsInExpression + import Strata.Languages.Laurel.EliminateValueReturns import Strata.Languages.Laurel.ConstrainedTypeElim + +import Strata.Languages.Laurel.PackMultipleOutputs import Strata.Languages.Laurel.TypeAliasElim import Strata.Languages.Core.Verifier import Strata.Util.Profile @@ -25,8 +28,9 @@ to Strata Core. The pipeline is: 2. Run a sequence of Laurel-to-Laurel lowering passes (resolution, heap parameterization, type hierarchy, modifies clauses, hole inference, desugaring, lifting, constrained type elimination). -3. Group and order declarations into an `OrderedLaurel`. -4. Translate the `OrderedLaurel` to a `Core.Program`. +3. Run the transparency pass to produce an `UnorderedCoreWithLaurelTypes`. +4. Group and order declarations into a `CoreWithLaurelTypes`. +5. Translate the `CoreWithLaurelTypes` to a `Core.Program`. -/ open Core (VCResult VCResults VerifyOptions) @@ -94,10 +98,6 @@ private def laurelPipeline : Array LaurelPass := #[ run := fun p m => let (p', diags) := filterNonCompositeModifies m p (p', diags, {}) }, - { name := "EliminateValueReturns" - run := fun p _m => - let (p', diags) := eliminateValueReturnsTransform p - (p', diags.toList, {}) }, { name := "HeapParameterization" needsResolves := true run := fun p m => @@ -124,7 +124,7 @@ private def laurelPipeline : Array LaurelPass := #[ (desugarShortCircuit m p, [], {}) }, { name := "LiftExpressionAssignments" run := fun p m => - (liftExpressionAssignments m p, [], {}) }, + (liftExpressionAssignments p m [], [], {}) }, { name := "EliminateReturns" needsResolves := true run := fun p _m => @@ -195,6 +195,65 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra return (program, model, allDiags, allStats) +/-- +Convert an `UnorderedCoreWithLaurelTypes` to a flat `Program` suitable for +resolution and program-level passes. Composite types from the original Laurel +program are included so that references to composite types resolve correctly. +-/ +private def toProgram (uc : UnorderedCoreWithLaurelTypes) (laurelProgram : Program) + : Program := + { staticProcedures := uc.functions ++ uc.coreProcedures, + staticFields := [], + types := uc.datatypes.map TypeDefinition.Datatype ++ + -- Hack to compensate for references to composite types not having been updated yet. + laurelProgram.types.filter (fun t => match t with | .Composite _ => true | _ => false), + constants := uc.constants } + +/-- +Reconstruct an `UnorderedCoreWithLaurelTypes` from a resolved `Program`, +preserving the structure of the original `UnorderedCoreWithLaurelTypes`. +-/ +private def fromResolvedProgram (resolvedProgram : Program) + (_original : UnorderedCoreWithLaurelTypes) : UnorderedCoreWithLaurelTypes := + let resolvedProcs := resolvedProgram.staticProcedures + let resolvedDatatypes := resolvedProgram.types.filterMap fun td => + match td with | .Datatype dt => some dt | _ => none + { functions := resolvedProcs.filter (·.isFunctional) + coreProcedures := resolvedProcs.filter (!·.isFunctional) + datatypes := resolvedDatatypes + constants := resolvedProgram.constants } + +/-- +Resolve an `UnorderedCoreWithLaurelTypes` by converting to a flat `Program`, +running the resolution pass, and reconstructing the result. Returns the +resolved `UnorderedCoreWithLaurelTypes` and the `SemanticModel`. +-/ +def resolveUnorderedCore (uc : UnorderedCoreWithLaurelTypes) + (laurelProgram : Program) (existingModel : Option SemanticModel := none) + : UnorderedCoreWithLaurelTypes × SemanticModel := + let fnProgram := toProgram uc laurelProgram + let fnResolveResult := resolve fnProgram existingModel + (fromResolvedProgram fnResolveResult.program uc, fnResolveResult.model) + +/-- +Apply `liftExpressionAssignments` to the core (non-functional) procedures in an +`UnorderedCoreWithLaurelTypes`. Only procedures whose names appear in the core +procedure list are transformed; functions are left unchanged. +-/ +def liftImperativeExpressionsInCore (uc : UnorderedCoreWithLaurelTypes) + (model : SemanticModel) : UnorderedCoreWithLaurelTypes := + let imperativeCallees := uc.coreProcedures.map (·.name.text) + if imperativeCallees.isEmpty then uc + else + let allProcs := uc.functions ++ uc.coreProcedures + let liftedProgram := liftExpressionAssignments + { staticProcedures := allProcs, staticFields := [], types := [], constants := [] } + model imperativeCallees + let liftedProcs := liftedProgram.staticProcedures + { uc with + functions := liftedProcs.filter (·.isFunctional) + coreProcedures := liftedProcs.filter (!·.isFunctional) } + /-- Translate Laurel Program to Core Program, also returning the lowered Laurel program. @@ -205,7 +264,28 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program) : IO TranslateResultWithLaurel := runPipelineM options.keepAllFilesPrefix do let (program, model, passDiags, stats) ← runLaurelPasses options program - let ordered := orderProgram program + let unorderedCore := transparencyPass program + emit "transparencyPass" "core.st" unorderedCore + -- Eliminate value returns after the transparency pass so that the rewrite + -- applies to the core procedures produced by transparency. + let (unorderedCore, elimDiags) := eliminateValueReturnsTransform unorderedCore + let passDiags := passDiags ++ elimDiags.toList + emit "EliminateValueReturns" "core.st" unorderedCore + let unorderedCore := packMultipleOutputsInFunctions unorderedCore + -- let unorderedCore := inlineLocalVariablesInExpressions unorderedCore + + -- Resolve so that identifiers introduced by earlier passes get uniqueIds. + let (unorderedCore, model) := resolveUnorderedCore unorderedCore program (some model) + + -- Lift imperative expressions in the proof procedures. + let unorderedCore := liftImperativeExpressionsInCore unorderedCore model + emit "secondLiftingPass" "core.st" unorderedCore + + -- Re-resolve after lifting so that freshly introduced variables (e.g. $cndtn_N) + -- created by liftExpressionAssignments also get uniqueIds in the model. + let (unorderedCore, fnModel) := resolveUnorderedCore unorderedCore program (some model) + + let coreWithLaurelTypes := orderFunctionsAndProcedures unorderedCore -- This early return is a simple way to protect against duplicative errors. Without this return, -- resolution errors reported by Laurel would also be reported by Core. @@ -214,21 +294,23 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program) if passDiags.any (·.type != .Warning) then return (none, passDiags, program, stats) - let initState : TranslateState := { model := model, overflowChecks := options.overflowChecks } + emit "CoreWithLaurelTypes" "core.st" coreWithLaurelTypes + let initState : TranslateState := { model := fnModel, overflowChecks := options.overflowChecks } let (coreProgramOption, translateState) := - runTranslateM initState (translateLaurelToCore options program ordered) - if let some coreProgram := coreProgramOption then - emit "CoreProgram" "core.st" coreProgram - let mut allDiagnostics := passDiags ++ translateState.diagnostics + runTranslateM initState (translateLaurelToCore options program coreWithLaurelTypes) + -- Because of the duplication between functions and procedures, this translation is liable to create duplicate diagnostics + -- User errors should be checked in an earlier phase, and all dumb translation errors are Strata bugs + let mut allDiagnostics: List DiagnosticModel := passDiags ++ translateState.diagnostics.eraseDups; if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then -- The program was suppressed but no diagnostics explain why — report the core diagnostics -- that have a known source location (those without one are not actionable for the user). - let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown) - allDiagnostics := allDiagnostics ++ locatedDiags + allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics + if coreProgramOption.isSome then + emit "Core" "core.st" coreProgramOption.get! let coreProgramOption := - if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption + if translateState.coreDiagnostics.isEmpty then coreProgramOption else none return (coreProgramOption, allDiagnostics, program, stats) /-- diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index e1b30d7b72..728cb1d7e5 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -32,7 +32,7 @@ import Strata.Languages.Laurel.ConstrainedTypeElim import Strata.Util.Tactics open Core (VCResult VCResults VerifyOptions) -open Core (intAddOp intSubOp intMulOp intSafeDivOp intSafeModOp intSafeDivTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp) +open Core (intAddOp intSubOp intMulOp intDivOp intSafeDivOp intModOp intSafeModOp intDivTOp intSafeDivTOp intModTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp) open Core (realAddOp realSubOp realMulOp realDivOp realNegOp realLtOp realLeOp realGtOp realGeOp) namespace Strata.Laurel @@ -67,6 +67,11 @@ structure TranslateState where why the program was deemed invalid so that if no other diagnostics explain the suppression, these can be surfaced to the user. -/ coreDiagnostics : List DiagnosticModel := [] + /-- When `true`, use safe division (`intSafeDivOp`) and safe datatype selectors + (with preconditions). When `false`, use unsafe division (`intDivOp`) and + unsafe datatype selectors (without preconditions). + Set to `true` for proof procedures and `false` for functions. -/ + proof : Bool := false /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/ @[expose] abbrev TranslateM := OptionT (StateM TranslateState) @@ -75,6 +80,25 @@ structure TranslateState where def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit := modify fun s => { s with diagnostics := s.diagnostics ++ [d] } +/-- Adjust a datatype selector (destructor) name based on the `proof` flag. + Destructor names contain `..` (e.g. `IntList..head`, `IntList..head!`). + Tester names also contain `..` but start with `is` after the separator. + - `proof = true` → use safe selectors (strip `!` suffix) + - `proof = false` → use unsafe selectors (add `!` suffix) -/ +private def adjustSelectorName (name : String) (proof : Bool) : String := + -- Only adjust destructor names (contain ".." but are not testers) + match name.splitOn ".." with + | [_, suffix] => + if suffix.startsWith "is" then name -- tester, leave unchanged + else if proof then + name + -- Safe: strip trailing "!" + -- if name.endsWith "!" then (name.dropEnd 1).toString else name + else + -- Unsafe: add trailing "!" if not already present + if name.endsWith "!" then name else name ++ "!" + | _ => name -- not a destructor name, leave unchanged + private def invalidCoreType (source : Option FileRange) (reason : String) : TranslateM LMonoTy := do modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [diagnosticFromSource source reason DiagnosticType.StrataBug] } @@ -102,7 +126,8 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do | some (.datatypeConstructor typeName _) => return .tcons typeName.text [] | _ => do -- resolution should have already emitted a diagnostic modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ - [diagnosticFromSource ty.source s!"UserDefined type could not be resolved to a composite or datatype" DiagnosticType.StrataBug] } + [diagnosticFromSource ty.source s!"UserDefined type could not be resolved to a composite or datatype" DiagnosticType.StrataBug] + } return .tcons "Composite" [] | .TCore s => return .tcons s [] | .TReal => return LMonoTy.real @@ -121,9 +146,6 @@ def lookupType (name : Identifier) : TranslateM LMonoTy := do def runTranslateM (s : TranslateState) (m : TranslateM α) : (Option α × TranslateState) := m s -def returnNone: TranslateM α := - StateT.pure none - /-- Allocate a fresh unique ID. -/ private def freshId : TranslateM Nat := do let s ← get @@ -135,8 +157,7 @@ private def freshId : TranslateM Nat := do def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do emitDiagnostic d modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] } - let id ← freshId - return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none + return default /-- Translate Laurel StmtExpr to Core Expression using the `TranslateM` monad. @@ -157,6 +178,7 @@ def translateExpr (expr : StmtExprMd) let s ← get let model := s.model let md := astNodeToCoreMd expr + let proof := (← get).proof let disallowed (source : Option FileRange) (msg : String) : TranslateM Core.Expression.Expr := do if isPureContext then throwExprDiagnostic $ diagnosticFromSource source msg @@ -213,10 +235,10 @@ def translateExpr (expr : StmtExprMd) | .Add => return binOp (if isReal then realAddOp else intAddOp) | .Sub => return binOp (if isReal then realSubOp else intSubOp) | .Mul => return binOp (if isReal then realMulOp else intMulOp) - | .Div => return binOp (if isReal then realDivOp else intSafeDivOp) - | .Mod => return binOp intSafeModOp - | .DivT => return binOp intSafeDivTOp - | .ModT => return binOp intSafeModTOp + | .Div => return binOp (if isReal then realDivOp else if proof then intSafeDivOp else intDivOp) + | .Mod => return binOp (if (← get).proof then intSafeModOp else intModOp) + | .DivT => return binOp (if (← get).proof then intSafeDivTOp else intDivTOp) + | .ModT => return binOp (if (← get).proof then intSafeModTOp else intModTOp) | .Lt => return binOp (if isReal then realLtOp else intLtOp) | .Leq => return binOp (if isReal then realLeOp else intLeOp) | .Gt => return binOp (if isReal then realGtOp else intGtOp) @@ -241,9 +263,10 @@ def translateExpr (expr : StmtExprMd) | .StaticCall callee args => -- In a pure context, only Core functions (not procedures) are allowed if isPureContext && !model.isFunction callee then - disallowed expr.source "calls to procedures are not supported in functions or contracts" + disallowed expr.source s!"calls to procedures are not supported in contracts. Callee: {callee}" else - let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none + let calleeName := adjustSelectorName callee.text (← get).proof + let fnOp : Core.Expression.Expr := .op () ⟨calleeName, ()⟩ none args.attach.foldlM (fun acc ⟨arg, _⟩ => do let re ← translateExpr arg boundVars isPureContext return .app () acc re) fnOp @@ -299,7 +322,7 @@ def translateExpr (expr : StmtExprMd) -- If we see one here, it's an error in the pipeline throwExprDiagnostic $ diagnosticFromSource expr.source s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldId.text}" DiagnosticType.StrataBug | .Block _ _ => - throwExprDiagnostic $ diagnosticFromSource expr.source "block expression should have been lowered in a separate pass" DiagnosticType.StrataBug + throwExprDiagnostic $ diagnosticFromSource expr.source s!"block expression should have been lowered in a separate pass, expr: {repr expr}" DiagnosticType.StrataBug | .Return _ => disallowed expr.source "return expression should be lowered in a separate pass" | .AsType target _ => throwExprDiagnostic $ diagnosticFromSource expr.source "AsType expression translation" DiagnosticType.NotYetImplemented @@ -320,8 +343,9 @@ def translateExpr (expr : StmtExprMd) all_goals (have := AstNode.sizeOf_val_lt expr; term_by_mem) def getNameFromMd (md : Imperative.MetaData Core.Expression): String := - let fileRange := (Imperative.getFileRange md).getD (dbg_trace "BUG: metadata without a filerange"; default) - s!"({fileRange.range.start})" + match Imperative.getFileRange md with + | some fileRange => s!"({fileRange.range.start})" + | none => "(generated)" def defaultExprForType (ty : HighTypeMd) : TranslateM Core.Expression.Expr := do match ty.val with @@ -343,9 +367,10 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core. : TranslateM (List Core.Statement) := do let coreExpr ← translateExpr expr let id ← freshId + let model := (← get).model let ident : Core.CoreIdent := ⟨s!"$unused_{id}", ()⟩ - let tyVarName := s!"$__ty_unused_{id}" - let coreType := LTy.forAll [tyVarName] (.ftvar tyVarName) + let ty ← translateType (computeExprType model expr) + let coreType := LTy.forAll [] ty return [Core.Statement.init ident coreType (.det coreExpr) md] def throwStmtDiagnostic (d : DiagnosticModel): TranslateM (List Core.Statement) := do @@ -527,7 +552,7 @@ def translateStmt (stmt : StmtExprMd) Translate a list of checks (preconditions or postconditions) to Core checks. Each check gets a label like `"requires"` or `"requires_0"`, `"requires_1"`, etc. -/ -private def translateChecks (checks : List Condition) (labelBase : String) +private def translateChecks (checks : List Condition) (labelBase : String) (overrideFree: Bool) : TranslateM (ListMap Core.CoreLabel Core.Procedure.Check) := checks.mapIdxM (fun i check => do let label := if checks.length == 1 then labelBase else s!"{labelBase}_{i}" @@ -536,7 +561,8 @@ private def translateChecks (checks : List Condition) (labelBase : String) let md := match check.summary with | some msg => baseMd.pushElem Imperative.MetaData.propertySummary (.msg msg) | none => baseMd - let c : Core.Procedure.Check := { expr := checkExpr, md } + let attr := if check.free || overrideFree then Core.Procedure.CheckAttr.Free else .Default + let c : Core.Procedure.Check := { expr := checkExpr, attr, md } return (label, c)) /-- @@ -563,26 +589,33 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do outputs := outputs } -- Translate preconditions - let preconditions ← translateChecks proc.preconditions "requires" + let preconditions ← translateChecks proc.preconditions "requires" false - -- Translate postconditions for Opaque and Abstract bodies - let postconditions : ListMap Core.CoreLabel Core.Procedure.Check ← - match proc.body with - | .Opaque postconds _ _ | .Abstract postconds => - translateChecks postconds "postcondition" - | _ => pure [] - let bodyStmts : List Core.Statement ← + let bodyStmts : Option (List Core.Statement) ← match proc.body with - | .Transparent bodyExpr => translateStmt bodyExpr - | .Opaque _postconds (some impl) _ => translateStmt impl + | .Transparent bodyExpr => + let r ← translateStmt bodyExpr + pure $ some r + | .Opaque _postconds (some impl) _ => + let r ← translateStmt impl + pure $ some r | _ => + pure none -- Bodiless procedure: assume postconditions so that verification of the -- procedure itself passes trivially, and inlining only introduces the -- postconditions as assumptions (not the unsound `assume false`). - pure (postconditions.map fun (label, check) => - Core.Statement.assume label check.expr mdWithUnknownLoc) + -- pure (postconditions.map fun (label, check) => + -- Core.Statement.assume label check.expr mdWithUnknownLoc) -- Wrap body in a labeled block so early returns (exit) work correctly. - let body : List Core.Statement := [.block "$body" bodyStmts mdWithUnknownLoc] + + -- Translate postconditions for Opaque and Abstract bodies + let postconditions : ListMap Core.CoreLabel Core.Procedure.Check ← + match proc.body with + | .Opaque postconds _ _ | .Abstract postconds => + translateChecks postconds s!"postcondition{(bodyStmts.getD []).length}" bodyStmts.isNone + | _ => pure [] + + let body : List Core.Statement := [.block "$body" (bodyStmts.getD []) mdWithUnknownLoc] let spec : Core.Procedure.Spec := { preconditions, postconditions } return { header, spec, body } @@ -718,35 +751,33 @@ def translateDatatypeDefinition (dt : DatatypeDefinition) abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel) /-- -Translate an `OrderedLaurel` program to a `Core.Program`. +Translate a `CoreWithLaurelTypes` program to a `Core.Program`. The `program` parameter is the lowered Laurel program, used for type definitions. -/ -def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program) (ordered : OrderedLaurel): TranslateM Core.Program := do +def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program) (ordered : CoreWithLaurelTypes): TranslateM Core.Program := do let coreDecls ← ordered.decls.flatMapM fun - | .procs procs isRecursive => do - -- For each SCC, determine if it is purely functional or contains procedures. - let isFuncSCC := procs.all (·.isFunctional) - if isFuncSCC then - let funcs ← procs.mapM (translateProcedureToFunction options isRecursive) - if isRecursive then - let coreFuncs := funcs.filterMap (fun d => match d with - | .func f _ => some f - | _ => none) - return [Core.Decl.recFuncBlock coreFuncs mdWithUnknownLoc] - else - return funcs + | .funcs funcs isRecursive => do + modify fun s => { s with proof := false } + let nonExternal := funcs.filter (fun p => !p.body.isExternal) + let coreFuncs ← nonExternal.mapM (translateProcedureToFunction options isRecursive) + if isRecursive then + let coreFuncValues := coreFuncs.filterMap (fun d => match d with + | .func f _ => some f + | _ => none) + return [Core.Decl.recFuncBlock coreFuncValues mdWithUnknownLoc] else - let procDecls ← procs.flatMapM fun proc => do - let procDecl ← translateProcedure proc - -- Turn free postconditions into axioms placed right behind the related procedure - let axiomDecls : List Core.Decl ← match proc.invokeOn with - | none => pure [] - | some trigger => do - let axDecl? ← translateInvokeOnAxiom proc trigger - pure axDecl?.toList - return [Core.Decl.proc procDecl (identifierToCoreMd proc.name)] ++ axiomDecls - return procDecls + return coreFuncs + | .procedure proc => do + modify fun s => { s with proof := true } + let procDecl ← translateProcedure proc + -- Translate axioms from invokeOn + let invokeOnDecls ← match proc.invokeOn with + | some trigger => do + let axDecl? ← translateInvokeOnAxiom proc trigger + pure axDecl?.toList + | none => pure [] + return [Core.Decl.proc procDecl (identifierToCoreMd proc.name)] ++ invokeOnDecls | .datatypes dts => do let ldatatypes ← dts.mapM translateDatatypeDefinition return [Core.Decl.type (.data ldatatypes) mdWithUnknownLoc] @@ -769,6 +800,7 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program) emitDiagnostic $ diagnosticFromSource proc.name.source s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported" DiagnosticType.NotYetImplemented + pure { decls := coreDecls } end -- public section diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 7c63b6870f..6a00bf7d42 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -82,6 +82,8 @@ structure LiftState where condCounter : Nat := 0 /-- All procedures in the program, used to look up return types of imperative calls -/ procedures : List Procedure := [] + /-- Names of callees whose calls should be treated as imperative (lifted) -/ + imperativeCallees : List String := [] @[expose] abbrev LiftM := StateM LiftState @@ -102,7 +104,7 @@ private def freshTempFor (varName : Identifier) : LiftM Identifier := do private def freshCondVar : LiftM Identifier := do let n := (← get).condCounter modify fun s => { s with condCounter := n + 1 } - return s!"$c_{n}" + return s!"$cndtn_{n}" private def prepend (stmt : StmtExprMd) : LiftM Unit := modify fun s => { s with prependedStmts := stmt :: s.prependedStmts } @@ -115,27 +117,10 @@ private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (Li let nonLast ← stmts.dropLast.flatMapM (fun s => match s.val with | .Var (.Declare ..) | .Assign ([⟨.Declare .., _⟩]) _ => do - -- This addPrepend is a hack to work around Core not having let expressions - -- Otherwise we could keep them in the block + -- Lift declarations out of the block so they are visible to + -- assignments that were already lifted by transformExpr. prepend s pure [] - | .Assert _ => do - -- Hack to work around Core not supporting assert expressions - -- Otherwise we could keep them in the block - prepend s - pure [] - | .Assume _ => do - -- Hack to work around Core not supporting assume expressions - -- Otherwise we could keep them in the block - prepend s - pure [] - - /- - Any other impure StmtExpr, like .Assign, .Exit or .Return, - should already have been processed by translateExpr, - so we can assume this StmtExpr is pure and can be dropped. - TODO: currently .Exit and .Return are not processed by translateExpr, this is a bug - -/ | _ => pure [] ) return nonLast ++ [last] @@ -172,7 +157,11 @@ def containsAssignment (expr : StmtExprMd) : Bool := | _ => false termination_by expr decreasing_by - all_goals ((try cases x); simp_all; try term_by_mem) + all_goals (try cases x) + all_goals (try simp_all) + all_goals (try have := Condition.sizeOf_condition_lt ‹_›) + all_goals (try term_by_mem) + all_goals omega /-- Check if an expression contains any non-functional procedure calls (recursively). -/ def containsImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool := @@ -195,9 +184,52 @@ def containsImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool := decreasing_by all_goals ((try cases x); simp_all; try term_by_mem) -/-- Check if an expression contains any assignments or non-functional procedure calls (recursively). -/ -def containsAssignmentOrImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool := - containsAssignment expr || containsImperativeCall model expr +def containsAssignmentOrImperativeCall (imperativeCallees : List String) (expr : StmtExprMd) : Bool := + match expr with + | AstNode.mk val _ => + match val with + | .Assign .. => true + | .StaticCall name args1 => + imperativeCallees.contains name.text || + args1.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val) + | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val) + | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val) + | .IfThenElse cond th el => + containsAssignmentOrImperativeCall imperativeCallees cond || + containsAssignmentOrImperativeCall imperativeCallees th || + match el with | some e => containsAssignmentOrImperativeCall imperativeCallees e | none => false + | .Assume cond => containsAssignmentOrImperativeCall imperativeCallees cond + | .Assert cond => containsAssignmentOrImperativeCall imperativeCallees cond.condition + | .InstanceCall target _ args => + containsAssignmentOrImperativeCall imperativeCallees target || + args.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val) + | .Quantifier _ _ trigger body => + containsAssignmentOrImperativeCall imperativeCallees body || + match trigger with | some t => containsAssignmentOrImperativeCall imperativeCallees t | none => false + | .Old value => containsAssignmentOrImperativeCall imperativeCallees value + | .Fresh value => containsAssignmentOrImperativeCall imperativeCallees value + | .ProveBy value proof => + containsAssignmentOrImperativeCall imperativeCallees value || + containsAssignmentOrImperativeCall imperativeCallees proof + | .ReferenceEquals lhs rhs => + containsAssignmentOrImperativeCall imperativeCallees lhs || + containsAssignmentOrImperativeCall imperativeCallees rhs + | .PureFieldUpdate target _ newValue => + containsAssignmentOrImperativeCall imperativeCallees target || + containsAssignmentOrImperativeCall imperativeCallees newValue + | .AsType target _ => containsAssignmentOrImperativeCall imperativeCallees target + | .IsType target _ => containsAssignmentOrImperativeCall imperativeCallees target + | .Assigned name => containsAssignmentOrImperativeCall imperativeCallees name + | .ContractOf _ func => containsAssignmentOrImperativeCall imperativeCallees func + | .Return (some v) => containsAssignmentOrImperativeCall imperativeCallees v + | _ => false + termination_by expr + decreasing_by + all_goals (try cases x) + all_goals (try simp_all) + all_goals (try have := Condition.sizeOf_condition_lt ‹_›) + all_goals (try term_by_mem) + all_goals omega /-- Shared logic for lifting an assignment in expression position: @@ -225,6 +257,7 @@ Process an expression in expression context, traversing arguments right to left. Assignments are lifted to prependedStmts and replaced with snapshot variable references. -/ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do + let model := (← get).model match expr with | AstNode.mk val source => match val with @@ -271,10 +304,10 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.PrimitiveOp op seqArgs.reverse, source⟩ | .StaticCall callee args => - let model := (← get).model + let imperativeCallees := (← get).imperativeCallees let seqArgs ← args.reverse.mapM transformExpr let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩ - if model.isFunction callee then + if !imperativeCallees.contains callee.text then return seqCall else -- Imperative call in expression position: lift to an assignment. @@ -298,10 +331,10 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return bare (.Var (.Local callResultVar)) | .IfThenElse cond thenBranch elseBranch => - let model := (← get).model - let thenHasAssign := containsAssignmentOrImperativeCall model thenBranch + let imperativeCallees := (← get).imperativeCallees + let thenHasAssign := containsAssignmentOrImperativeCall imperativeCallees thenBranch let elseHasAssign := match elseBranch with - | some e => containsAssignmentOrImperativeCall model e + | some e => containsAssignmentOrImperativeCall imperativeCallees e | none => false if thenHasAssign || elseHasAssign then -- Lift the entire if-then-else. Introduce a fresh variable for the result. @@ -358,10 +391,85 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do else return expr + | .Assume cond => + let seqCond ← transformExpr cond + prepend ⟨.Assume seqCond, source⟩ + default + + | .Assert cond => + let seqCondExpr ← transformExpr cond.condition + prepend ⟨.Assert { cond with condition := seqCondExpr }, source⟩ + default + + | .Return (some retExpr) => + let seqRet ← transformExpr retExpr + return ⟨.Return (some seqRet), source⟩ + + | .While cond invs dec body => + let seqCond ← transformExpr cond + let seqInvs ← invs.mapM transformExpr + let seqDec ← match dec with + | some d => pure (some (← transformExpr d)) + | none => pure none + let seqBody ← transformExpr body + return ⟨.While seqCond seqInvs seqDec seqBody, source⟩ + + | .PureFieldUpdate target fieldName newValue => + let seqTarget ← transformExpr target + let seqNewValue ← transformExpr newValue + return ⟨.PureFieldUpdate seqTarget fieldName seqNewValue, source⟩ + + | .ReferenceEquals lhs rhs => + let seqRhs ← transformExpr rhs + let seqLhs ← transformExpr lhs + return ⟨.ReferenceEquals seqLhs seqRhs, source⟩ + + | .AsType target ty => + let seqTarget ← transformExpr target + return ⟨.AsType seqTarget ty, source⟩ + + | .IsType target ty => + let seqTarget ← transformExpr target + return ⟨.IsType seqTarget ty, source⟩ + + | .InstanceCall target callee args => + let seqArgs ← args.reverse.mapM transformExpr + let seqTarget ← transformExpr target + return ⟨.InstanceCall seqTarget callee seqArgs.reverse, source⟩ + + | .Quantifier mode param trigger body => + let seqBody ← transformExpr body + let seqTrigger ← match trigger with + | some t => pure (some (← transformExpr t)) + | none => pure none + return ⟨.Quantifier mode param seqTrigger seqBody, source⟩ + + | .Old value => + let seqValue ← transformExpr value + return ⟨.Old seqValue, source⟩ + + | .Fresh value => + let seqValue ← transformExpr value + return ⟨.Fresh seqValue, source⟩ + + | .Assigned name => + let seqName ← transformExpr name + return ⟨.Assigned seqName, source⟩ + + | .ProveBy value proof => + let seqValue ← transformExpr value + let seqProof ← transformExpr proof + return ⟨.ProveBy seqValue seqProof, source⟩ + + | .ContractOf ty func => + let seqFunc ← transformExpr func + return ⟨.ContractOf ty seqFunc, source⟩ + | _ => return expr termination_by (sizeOf expr, 0) decreasing_by - all_goals (simp_all; try term_by_mem) + all_goals (simp_all; try have := Condition.sizeOf_condition_lt ‹_›; try term_by_mem) + all_goals (apply Prod.Lex.left; try term_by_mem; try omega) /-- Process a statement, handling any assignments in its sub-expressions. @@ -374,24 +482,24 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do | .Assert cond => -- Do not transform assert conditions with assignments — they must be rejected. -- But nondeterministic holes and imperative calls need to be lifted. - if !containsAssignment cond.condition then + -- if !containsAssignment cond.condition then let seqCond ← transformExpr cond.condition let prepends ← takePrepends modify fun s => { s with subst := [] } return prepends ++ [⟨.Assert { cond with condition := seqCond }, source⟩] - else - return [stmt] + -- else + -- return [stmt] | .Assume cond => -- Do not transform assume conditions with assignments — they must be rejected. -- But nondeterministic holes and imperative calls need to be lifted. - if !containsAssignment cond then + -- if !containsAssignment cond then let seqCond ← transformExpr cond let prepends ← takePrepends modify fun s => { s with subst := [] } return prepends ++ [⟨.Assume seqCond, source⟩] - else - return [stmt] + -- else + -- return [stmt] | .Block stmts metadata => let seqStmts ← stmts.mapM transformStmt @@ -407,8 +515,8 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do | AstNode.mk value _ => match _: value with | .StaticCall callee args => - let model := (← get).model - if model.isFunction callee then + let imperativeCallees := (← get).imperativeCallees + if !imperativeCallees.contains callee.text then let seqValue ← transformExpr valueMd let prepends ← takePrepends modify fun s => { s with subst := [] } @@ -464,6 +572,10 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do modify fun s => { s with subst := [] } return prepends ++ [⟨.Return (some seqRet), source⟩] + | .PrimitiveOp name args => + let seqArgs ← args.mapM transformExpr + let prepends ← takePrepends + return prepends ++ [⟨.PrimitiveOp name seqArgs, source⟩] | _ => return [stmt] termination_by (sizeOf stmt, 0) @@ -494,10 +606,15 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do /-- Transform a program to lift all assignments that occur in an expression context. +When `procedureNames` is non-empty, only procedures whose name appears in the +list are transformed; all others are left unchanged. When `procedureNames` is +empty, no procedures are transformed. -/ -def liftExpressionAssignments (model: SemanticModel) (program : Program) : Program := - let initState : LiftState := { model := model } - let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState +def liftExpressionAssignments (program : Program) + (model : SemanticModel) (imperativeCallees : List String) : Program := + let initState : LiftState := { model := model, imperativeCallees := imperativeCallees } + let transform := program.staticProcedures.mapM transformProcedure + let (seqProcedures, _) := transform.run initState { program with staticProcedures := seqProcedures } end -- public section diff --git a/Strata/Languages/Laurel/PackMultipleOutputs.lean b/Strata/Languages/Laurel/PackMultipleOutputs.lean new file mode 100644 index 0000000000..270f0919d7 --- /dev/null +++ b/Strata/Languages/Laurel/PackMultipleOutputs.lean @@ -0,0 +1,166 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.Laurel.TransparencyPass + +/-! +# Eliminate Multiple Outputs + +Transforms bodiless functions with multiple outputs into functions that return +a single synthesized result datatype. Call sites are rewritten to destructure +the result using the generated accessors. + +This pass operates on `UnorderedCoreWithLaurelTypes → UnorderedCoreWithLaurelTypes`. +-/ + +namespace Strata.Laurel + +public section + + +private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none } +private def mkVarMd (v : Variable) : VariableMd := { val := v, source := none } +private def mkTy (t : HighType) : HighTypeMd := { val := t, source := none } + +/-- Info about a function whose multiple outputs have been collapsed into a result datatype. -/ +private structure MultiOutInfo where + funcName : String + resultTypeName : String + constructorName : String + /-- Original output parameters (name, type). -/ + outputs : List Parameter + /-- Number of input parameters (used to detect implicit heap args at call sites). -/ + inputCount : Nat + +/-- Identify bodiless functions with multiple outputs and build info records. -/ +private def collectMultiOutFunctions (funcs : List Procedure) : List MultiOutInfo := + funcs.filterMap fun f => + if f.outputs.length > 1 && !f.body.isTransparent then + some { + funcName := f.name.text + resultTypeName := s!"{f.name.text}$result" + constructorName := s!"{f.name.text}$result$mk" + outputs := f.outputs + inputCount := f.inputs.length + } + else none + +/-- Generate a result datatype for a multi-output function. -/ +private def mkResultDatatype (info : MultiOutInfo) : DatatypeDefinition := + let args := info.outputs.zipIdx.map fun (p, i) => + { name := mkId s!"out{i}", type := p.type : Parameter } + { name := mkId info.resultTypeName + typeArgs := [] + constructors := [{ name := mkId info.constructorName, args := args }] } + +/-- Transform a multi-output function to return the result datatype. -/ +private def transformFunction (info : MultiOutInfo) (proc : Procedure) : Procedure := + let resultOutput : Parameter := + { name := mkId "$result", type := mkTy (.UserDefined (mkId info.resultTypeName)) } + { proc with outputs := [resultOutput] } + +/-- Destructor name for field `outN` of the result datatype. -/ +private def destructorName (info : MultiOutInfo) (idx : Nat) : String := + s!"{info.resultTypeName}..out{idx}" + +/-- Check whether a statement is an Assume node. -/ +private def isAssume (stmt : StmtExprMd) : Bool := + match stmt.val with + | .Assume _ => true + | _ => false + +/-- Rewrite a single multi-output Assign into a temp declaration + destructuring + assignments. Any `Assume` statements from `following` that appear immediately + after the call are collected and placed after the destructuring assignments, + so they observe the post-call variable values. + Returns the rewritten statements and the number of consumed following statements. -/ +private def rewriteAssign (infoMap : Std.HashMap String MultiOutInfo) + (targets : List VariableMd) (callee : Identifier) (args : List StmtExprMd) + (callSrc : Option FileRange) + (following : List StmtExprMd) (counter : Nat) : Option (List StmtExprMd × Nat) := + match infoMap.get? callee.text with + | some info => + if targets.length ≤ info.outputs.length then + let tempName := s!"${callee.text}$temp{counter}" + let fullArgs := args + let tempDecl := mkMd (.Assign [mkVarMd (.Declare ⟨mkId tempName, mkTy (.UserDefined (mkId info.resultTypeName))⟩)] + ⟨.StaticCall callee fullArgs, callSrc⟩) + let assigns := targets.zipIdx.map fun (tgt, i) => + mkMd (.Assign [tgt] + (mkMd (.StaticCall (mkId (destructorName info i)) + [mkMd (.Var (.Local (mkId tempName)))]))) + -- Collect any Assume statements that immediately follow the call. + -- These are placed after the destructuring assignments so they + -- observe the post-call values of output variables. + let assumes := following.takeWhile isAssume + let consumed := assumes.length + some (tempDecl :: assigns ++ assumes, consumed) + else none + | none => none + +/-- Rewrite a statement list, replacing multi-output call patterns. + When a multi-output Assign is followed by Assume statements (inserted by + the contract pass), the Assumes are placed after the destructuring + assignments so they reference post-call variable values. -/ +private def rewriteStmts (infoMap : Std.HashMap String MultiOutInfo) + (stmts : List StmtExprMd) : List StmtExprMd := + let rec go (remaining : List StmtExprMd) (acc : List StmtExprMd) (counter : Nat) : List StmtExprMd := + match remaining with + | [] => acc.reverse + | stmt :: rest => + match stmt.val with + | .Assign targets ⟨.StaticCall callee args, callSrc⟩ => + match rewriteAssign infoMap targets callee args callSrc rest counter with + | some (expanded, consumed) => go (rest.drop consumed) (expanded.reverse ++ acc) (counter + 1) + | none => go rest (stmt :: acc) counter + | _ => go rest (stmt :: acc) counter + termination_by remaining.length + go stmts [] 0 + +/-- Rewrite blocks in a StmtExprMd tree to handle multi-output calls. -/ +private def rewriteExpr (infoMap : Std.HashMap String MultiOutInfo) + (expr : StmtExprMd) : StmtExprMd := + mapStmtExpr (fun e => + match e.val with + | .Block stmts label => ⟨.Block (rewriteStmts infoMap stmts) label, e.source⟩ + | _ => e) expr + +/-- Rewrite all procedure bodies. -/ +private def rewriteProcedure (infoMap : Std.HashMap String MultiOutInfo) + (proc : Procedure) : Procedure := + match proc.body with + | .Transparent b => + -- Wrap in a block so rewriteStmts can process top-level statements + let wrapped := mkMd (.Block [b] none) + let rewritten := rewriteExpr infoMap wrapped + { proc with body := .Transparent rewritten } + | .Opaque posts (some impl) mods => + let wrapped := mkMd (.Block [impl] none) + let rewritten := rewriteExpr infoMap wrapped + { proc with body := .Opaque posts (some rewritten) mods } + | _ => proc + +/-- Eliminate multiple outputs from a UnorderedCoreWithLaurelTypes. -/ +def packMultipleOutputsInFunctions (program : UnorderedCoreWithLaurelTypes) + : UnorderedCoreWithLaurelTypes := + let infos := collectMultiOutFunctions program.functions + if infos.isEmpty then program else + let infoMap : Std.HashMap String MultiOutInfo := + infos.foldl (fun m info => m.insert info.funcName info) {} + let newDatatypes := infos.map mkResultDatatype + let functions := program.functions.map fun f => + match infoMap.get? f.name.text with + | some info => rewriteProcedure infoMap (transformFunction info f) + | none => rewriteProcedure infoMap f + let coreProcedures := program.coreProcedures.map fun p => rewriteProcedure infoMap p + { program with + functions := functions + coreProcedures := coreProcedures + datatypes := program.datatypes ++ newDatatypes } + +end -- public section +end Strata.Laurel diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 16bcf1333f..2ffb921501 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -164,8 +164,15 @@ structure SemanticModel where def SemanticModel.get (model: SemanticModel) (iden: Identifier): ResolvedNode := match iden.uniqueId with - | some key => (model.refToDef.get? key).getD default - | none => default + | some key => + match model.refToDef.get? key with + | some node => node + | none => + -- An ID was assigned during Phase 1 but the reference was never registered in + -- Phase 2 (buildRefToDef). This is a bug in the resolution pass itself. + dbg_trace s!"SOUND BUG: identifier '{iden.text}' (id={key}) has a uniqueId but is missing from refToDef" + .unresolved iden.source + | none => .unresolved iden.source def SemanticModel.isFunction (model: SemanticModel) (id: Identifier): Bool := match model.get id with @@ -223,7 +230,6 @@ private def freshId : ResolveM Nat := do set { s with nextId := id + 1 } return id - /-- Like `defineName`, but reports a diagnostic if the name already exists in the current scope. Inserts an `.unresolved` node so subsequent references still resolve without cascading errors. -/ def defineNameCheckDup (iden : Identifier) (node : ResolvedNode) (overrideResolutionName: Option String := none) : ResolveM Identifier := do @@ -403,9 +409,7 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let name' ← defineNameCheckDup param.name (.var param.name ty') pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd) let value' ← resolveStmtExpr value - -- Check that LHS target count matches the number of outputs from the RHS. - -- This fires for procedure calls (which can have multiple outputs). - -- Functions always have exactly 1 output in the model, so single-target function calls pass trivially. + -- Check that LHS target count matches the number of outputs from the RHS let expectedOutputCount ← match value'.val with | .StaticCall callee _ => do let s ← get @@ -481,9 +485,9 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do | .Fresh val => let val' ← resolveStmtExpr val pure (.Fresh val') - | .Assert ⟨condExpr, summary⟩ => + | .Assert ⟨condExpr, summary, free⟩ => let cond' ← resolveStmtExpr condExpr - pure (.Assert { condition := cond', summary }) + pure (.Assert { condition := cond', summary, free }) | .Assume cond => let cond' ← resolveStmtExpr cond pure (.Assume cond') @@ -536,10 +540,6 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr) let dec' ← proc.decreases.mapM resolveStmtExpr let body' ← resolveBody proc.body - if !proc.isFunctional && body'.isTransparent then - let diag := diagnosticFromSource proc.name.source - s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque" - modify fun s => { s with errors := s.errors.push diag } let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr return { name := procName', inputs := inputs', outputs := outputs', isFunctional := proc.isFunctional, @@ -569,9 +569,9 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr) let dec' ← proc.decreases.mapM resolveStmtExpr let body' ← resolveBody proc.body - if !proc.isFunctional && body'.isTransparent then + if !proc.isFunctional && body'.isTransparent && !proc.name.text.any (· == '$') then let diag := diagnosticFromSource proc.name.source - s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque" + s!"transparent statement bodies are not supported. Add 'opaque' to make the procedure opaque" modify fun s => { s with errors := s.errors.push diag } let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr modify fun s => { s with instanceTypeName := savedInstType } @@ -729,7 +729,7 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp | .Assigned name => collectStmtExpr map name | .Old val => collectStmtExpr map val | .Fresh val => collectStmtExpr map val - | .Assert ⟨cond, _⟩ => collectStmtExpr map cond + | .Assert ⟨cond, _, _⟩ => collectStmtExpr map cond | .Assume cond => collectStmtExpr map cond | .ProveBy val proof => let map := collectStmtExpr map val @@ -856,8 +856,18 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do /-- Run the full resolution pass on a Laurel program. -/ def resolve (program : Program) (existingModel: Option SemanticModel := none) : ResolutionResult := + -- Phase 1: pre-register all top-level names, then assign IDs and resolve references let phase1 : ResolveM Program := do + + for td in program.types do + if let .Composite ct := td then + for proc in ct.instanceProcedures do + let diag := diagnosticFromSource proc.name.source + s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported" + DiagnosticType.NotYetImplemented + modify fun s => { s with errors := s.errors.push diag } + preRegisterTopLevel program let types' ← program.types.mapM resolveTypeDefinition let constants' ← program.constants.mapM resolveConstant diff --git a/Strata/Languages/Laurel/TransparencyPass.lean b/Strata/Languages/Laurel/TransparencyPass.lean new file mode 100644 index 0000000000..b7b298eade --- /dev/null +++ b/Strata/Languages/Laurel/TransparencyPass.lean @@ -0,0 +1,159 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.Laurel.MapStmtExpr +public import Strata.Languages.Laurel.Laurel +import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator + +/-! +## Transparency Pass + +For each Core procedure, generate a function with the same signature and name +suffixed with `$asFunction`. If a Core procedure is marked as transparent, +attempt to add a body to its function version. In the functional body, +assertions are erased and all calls are to functional versions. If the function +has a body, add a free postcondition to the related procedure that equates the +two. + +This IR sits between Laurel and CoreWithLaurelTypes in the pipeline: + Laurel → UnorderedCoreWithLaurelTypes → CoreWithLaurelTypes → Core +-/ + +namespace Strata.Laurel + +public section + +/-- +An intermediate representation produced by the transparency pass. +Functions are pure computational procedures (suffixed `$asFunction`); +coreProcedures are the original procedures with any free postconditions +embedded in their `Body.Opaque` postcondition lists. +-/ +public structure UnorderedCoreWithLaurelTypes where + functions : List Procedure + coreProcedures : List Procedure + datatypes : List DatatypeDefinition + constants : List Constant + +/-- Deep traversal that strips all Assert and Assume nodes from a StmtExpr tree. + Assert/Assume nodes are replaced with `LiteralBool true`, and Block nodes + are collapsed by filtering out trivial `LiteralBool true` leftovers. -/ +def stripAssertAssume (expr : StmtExprMd) : StmtExprMd := + mapStmtExpr (fun e => + match e.val with + | .Assert _ | .Assume _ => ⟨.LiteralBool true, e.source⟩ + | .Block stmts label => + let stmts' := stmts.filter fun s => + match s.val with | .LiteralBool true => false | _ => true + match stmts' with + | [] => ⟨.LiteralBool true, e.source⟩ + | [s] => if label.isNone then s else ⟨.Block [s] label, e.source⟩ + | _ => ⟨.Block stmts' label, e.source⟩ + | _ => e) expr + +/-- Rewrite StaticCall callees to their `$asFunction` versions, + but only for procedures whose names appear in `nonExternalNames`. -/ +private def rewriteCallsToFunctional (asFunctionNames : List String) (expr : StmtExprMd) : StmtExprMd := + mapStmtExpr (fun e => + match e.val with + | .StaticCall callee args => + if asFunctionNames.contains callee.text then + let funcCallee := { callee with text := callee.text ++ "$asFunction", uniqueId := none } + ⟨.StaticCall funcCallee args, e.source⟩ + else e + | _ => e) expr + +/-- Build a free postcondition equating the procedure's output to its functional version. + For a procedure `foo(a, b) returns (r)`, produces: + `r == foo$asFunction(a, b)` -/ +private def mkFreePostcondition (proc : Procedure) : StmtExprMd := + let source := proc.name.source + let funcName := { proc.name with text := proc.name.text ++ "$asFunction", uniqueId := none } + let inputArgs := proc.inputs.map fun p => (⟨ .Var (.Local p.name), source ⟩ : StmtExprMd) + let funcCall: StmtExprMd := ⟨ .StaticCall funcName inputArgs, source ⟩ + match proc.outputs with + | [out] => ⟨ .PrimitiveOp .Eq [⟨ .Var (.Local out.name), source⟩, funcCall], source ⟩ + | _ => ⟨ .LiteralBool true, source ⟩ + +/-- Create the function copy of a procedure (suffixed `$asFunction`). + If the procedure is transparent, include a functional body. + Otherwise the function is opaque. -/ +private def mkFunctionCopy (asFunctionNames : List String) (proc : Procedure) : Procedure := + let funcName := { proc.name with text := proc.name.text ++ "$asFunction", uniqueId := none } + let body := match proc.body with + | .Transparent b => .Transparent (rewriteCallsToFunctional asFunctionNames (stripAssertAssume b)) + | .Opaque _ _ _ => .Opaque [] none [] + | x => x + { proc with name := funcName, isFunctional := true, body := body, preconditions := [] } + +/-- Check whether a function copy has a body (i.e. the procedure was transparent). -/ +private def functionHasBody (proc : Procedure) : Bool := + match proc.body with + | .Transparent _ => true + | _ => false + +/-- Append a free postcondition to a procedure's body postconditions. + For Opaque and Abstract bodies, the free condition is appended to the + existing postcondition list. For Transparent bodies, the body is promoted + to Opaque so the free postcondition can be carried. -/ +private def addFreePostcondition (proc : Procedure) (freePost : StmtExprMd) : Procedure := + match freePost.val with + | .LiteralBool true => proc -- trivial, skip + | _ => + let freeCond : Condition := { condition := freePost, free := true } + match proc.body with + | .Opaque postconds impl modif => + { proc with body := .Opaque (postconds ++ [freeCond]) impl modif } + | .Abstract postconds => + { proc with body := .Abstract (postconds ++ [freeCond]) } + | .Transparent body => + { proc with body := .Opaque [freeCond] (some body) [] } + | _ => proc + +/-- +Transparency pass: translate a Laurel program to the UnorderedCoreWithLaurelTypes IR. + +For each procedure: +- Generate a function with the same signature, named `foo$asFunction` +- If transparent, the function gets a functional body (assertions erased, calls to functional versions) +- If the function has a body, add a free postcondition equating the procedure output to the function +-/ +def transparencyPass (program : Program) : UnorderedCoreWithLaurelTypes := + let (skipped, notSkipped) := program.staticProcedures.partition (fun p => p.body.isExternal || + -- Skip transparent functions until we introduce a contract pass, + -- which enables lifting procedure calls from contracts + (p.isFunctional && p.body.isTransparent)) + let asFunctionNames := notSkipped.map (fun p => p.name.text) + let asFunctions := notSkipped.map (mkFunctionCopy asFunctionNames) + + -- External procedures get a plain function copy (they have no $asFunction version) + let (skippedFunctions, skippedProcedures) := skipped.partition (fun p => p.isFunctional) + let functions := skippedFunctions ++ asFunctions + let coreProcedures := notSkipped.map fun p => + let freePostcondition := mkFreePostcondition p + let p := addFreePostcondition p freePostcondition + { p with isFunctional := false } + let datatypes := program.types.filterMap fun td => match td with + | .Datatype dt => some dt + | _ => none + let procs: List Procedure := skippedProcedures ++ coreProcedures + { functions, coreProcedures := procs, datatypes, constants := program.constants } + +open Std (Format ToFormat) + +def formatUnorderedCoreWithLaurelTypes (p : UnorderedCoreWithLaurelTypes) : Format := + let datatypeFmts := p.datatypes.map ToFormat.format + let constantFmts := p.constants.map ToFormat.format + let functionFmts := p.functions.map ToFormat.format + let procFmts := p.coreProcedures.map ToFormat.format + Format.joinSep (datatypeFmts ++ constantFmts ++ functionFmts ++ procFmts) "\n\n" + +instance : ToFormat UnorderedCoreWithLaurelTypes where + format := formatUnorderedCoreWithLaurelTypes + +end -- public section +end Strata.Laurel diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 0622ad6473..1f56d7618f 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -2355,6 +2355,73 @@ def extractClassFields (ctx : TranslationContext) (classBody : Array (Python.stm return fields +/-- Translate a Python method to a Laurel instance procedure -/ +def translateMethod (ctx : TranslationContext) (className : String) + (methodStmt : Python.stmt SourceRange) + : Except TranslationError Procedure := do + match methodStmt with + | .FunctionDef _ name args body _ _ret _ _ => do + let methodName := name.val + + -- First parameter is self (typed as Composite to match call-site convention) + let selfParam : Parameter := { + name := "self" + type := mkHighTypeMd (.UserDefined (mkId className)) + } + + -- Translate remaining parameters (all typed as Any to match the + -- Python→Laurel pipeline's Any-wrapping convention for call sites). + let mut inputs : List Parameter := [selfParam] + match args with + | .mk_arguments _ _ argsList _ _ _ _ _ => + -- Skip first arg (self), process rest + if argsList.val.size > 0 then + for arg in argsList.val.toList.tail! do + match arg with + | .mk_arg _ paramName _paramAnnotation _ => + inputs := inputs ++ [{name := paramName.val, type := AnyTy}] + let mut kwargsName : Option String := none + match args with + | .mk_arguments _ _ _ _ _ _ kwargs _ => + match kwargs.val with + | some (.mk_arg _ name _ _ ) => + inputs:= inputs ++ [{ name := name.val, type := mkCoreType PyLauType.DictStrAny }] + kwargsName := some name.val + | _ => pure () + + -- Translate return type + -- All methods return Any (void methods return Any via from_None) + let outputs : List Parameter := [{name := "LaurelResult", type := AnyTy}] + + -- Translate method body with class context + -- Add method parameters to variableTypes so that hoisting (e.g. in + -- try/except) does not re-declare them as local variables. + let paramTypes : List (String × String) := inputs.map fun p => + if p.name.text == "self" then (p.name.text, className) else (p.name.text, PyLauType.Any) + let ctxWithClass := {ctx with currentClassName := some className, + variableTypes := paramTypes} + let newDecls := collectDeclaredNamesAndTypes ctxWithClass body.val.toList + let (varDecls, ctxWithClass) ← createVarDeclStmtsAndCtx ctxWithClass newDecls + let (_, bodyStmts) ← translateStmtList ctxWithClass body.val.toList + let bodyStmts := prependExceptHandlingHelper (varDecls ++ bodyStmts) + let (renamedInputs, paramCopies) := renameInputParams inputs + (fun n => n == "self" || kwargsName == some n) + let bodyStmts := paramCopies ++ bodyStmts + let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) + + let source := sourceRangeToSource ctx.filePath methodStmt.ann + return { + name := { text := manglePythonMethod className methodName, source := source } + inputs := renamedInputs + outputs := outputs + preconditions := [{ condition := mkStmtExprMd (StmtExpr.LiteralBool true) }] + isFunctional := false + decreases := none + body := .Opaque [] (some bodyBlock) wildcardModifies + } + | _ => throw (.internalError "Expected FunctionDef for method") + + /-- Extract fields from __init__ method body by scanning for self.field : type = expr patterns -/ def extractFieldsFromInit (ctx : TranslationContext) (initBody : Array (Python.stmt SourceRange)) : Except TranslationError (List Field) := do @@ -2533,10 +2600,13 @@ def translateClass (ctx : TranslationContext) (classStmt : Python.stmt SourceRan -- and the resolution pass may not handle all constructs in method bodies. let inHierarchy := ctx.classesInHierarchy.contains className let mut instanceProcedures : Array Procedure := #[] - - for (funcDecl, sr, funcBody) in classFunDeclsAndBody do - let (proc, _) ← translateFunction ctx sr funcDecl $ if inHierarchy then none else funcBody - instanceProcedures := instanceProcedures.push proc + for stmt in body do + if let .FunctionDef .. := stmt then + let proc ← translateMethod ctx className stmt + if inHierarchy then + instanceProcedures := instanceProcedures.push { proc with body := .Opaque [] .none wildcardModifies } + else + instanceProcedures := instanceProcedures.push proc -- Add synthesized default __init__ if needed if let some initProc := defaultInitProc then instanceProcedures := instanceProcedures.push initProc diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean index da75cc4076..a88d57175f 100644 --- a/Strata/Languages/Python/Specs/ToLaurel.lean +++ b/Strata/Languages/Python/Specs/ToLaurel.lean @@ -414,9 +414,10 @@ def buildSpecBody (allArgs : Array Arg) (returnType : SpecType) (source : Option FileRange) (ctx : SpecExprContext) - : ToLaurelM Body := do + : ToLaurelM (List Condition × Body) := do let fileSource ← mkFileSource let mut stmts : Array StmtExprMd := #[] + let mut preconds : Array Condition := #[] -- 1. Havoc the result: result := Hole(nondet) let holeExpr : StmtExprMd := { val := .Hole (deterministic := false), source := source } let resultId : AstNode Variable := { val := Variable.Local (mkId "result"), source := source } @@ -451,6 +452,7 @@ def buildSpecBody (allArgs : Array Arg) let (⟨condType, condExpr⟩, success) ← runChecked <| specExprToLaurel assertion.formula source ctx if success then if let .TBool := condType then + preconds := preconds.push { condition := condExpr.stmt, summary := some msg } let assertStmt ← mkStmtWithLoc (.Assert { condition := condExpr.stmt, summary := some msg }) default stmts := stmts.push assertStmt else @@ -479,7 +481,7 @@ def buildSpecBody (allArgs : Array Arg) val := .Block stmts.toList none, source := fileSource } - return .Opaque [] (some body) [{ val := .All, source := none }] + return (preconds.toList, .Opaque [] (some body) [{ val := .All, source := none }]) /-! ## Declaration Translation -/ @@ -519,14 +521,14 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl) inputs.foldl (init := ({} : Std.HashMap String HighType).insert "result" Laurel.tyAny) fun m p => m.insert p.name.text p.type.val let specCtx : SpecExprContext := { procName, argTypes } - let body ← buildSpecBody allArgs func.preconditions func.postconditions + let (preconds, body) ← buildSpecBody allArgs func.preconditions func.postconditions func.returnType none specCtx let src ← mkSourceWithFileRange func.loc return { name := { text := procName, source := src } inputs := inputs.toList outputs := outputs - preconditions := [] + preconditions := preconds decreases := none isFunctional := false body := body diff --git a/StrataTest/Backends/CBMC/contracts/test_contract.lr.st b/StrataTest/Backends/CBMC/contracts/test_contract.lr.st index 5660809918..20505c2cbc 100644 --- a/StrataTest/Backends/CBMC/contracts/test_contract.lr.st +++ b/StrataTest/Backends/CBMC/contracts/test_contract.lr.st @@ -6,7 +6,9 @@ procedure add(x: int, y: int) returns (r: int) r := x + y; }; -procedure main() { +procedure main() + opaque +{ var a: int := 42; assert a > 0; }; diff --git a/StrataTest/Backends/CBMC/contracts/test_contracts_e2e.sh b/StrataTest/Backends/CBMC/contracts/test_contracts_e2e.sh index eef32397e1..0ab00ccab1 100755 --- a/StrataTest/Backends/CBMC/contracts/test_contracts_e2e.sh +++ b/StrataTest/Backends/CBMC/contracts/test_contracts_e2e.sh @@ -66,12 +66,15 @@ echo "--- Test 1: Procedure with requires/ensures (full DFCC + CBMC) ---" build_goto "contract" 'procedure add(x: int, y: int, out r: int) requires x >= 0 + opaque ensures r >= x { r := x + y; } -procedure main() { +procedure main() + opaque +{ var a: int := 42; assert a > 0; }' @@ -102,7 +105,9 @@ echo "" # ---- Test 2: Simple assert (full CBMC verification) ---- echo "--- Test 2: Simple assert (full DFCC + CBMC) ---" -build_goto "assert" 'procedure main() { +build_goto "assert" 'procedure main() + opaque +{ var x: int := 10; var y: int := x + 5; assert y > x; @@ -122,12 +127,15 @@ echo "--- Test 3: Procedure with ensures (full DFCC + CBMC) ---" build_goto "ensures" 'procedure inc(x: int, out r: int) requires x >= 0 + opaque ensures r > x { r := x + 1; } -procedure main() { +procedure main() + opaque +{ var v: int := 10; assert v > 0; }' @@ -146,6 +154,7 @@ echo "--- Test 4: Loop with invariant (full DFCC + CBMC) ---" build_goto "loop" 'procedure sum_to_n(n: int, out s: int) requires n >= 0 + opaque ensures s >= 0 { var i: int := 0; @@ -159,7 +168,9 @@ build_goto "loop" 'procedure sum_to_n(n: int, out s: int) } } -procedure main() { +procedure main() + opaque +{ var x: int := 5; assert x > 0; }' @@ -179,12 +190,15 @@ echo "--- Test 5: Procedure call (full DFCC + CBMC) ---" build_goto "call" 'procedure double(x: int, out r: int) requires x >= 0 + opaque ensures r == x + x { r := x + x; } -procedure main() { +procedure main() + opaque +{ var a: int := 3; assert a > 0; }' @@ -217,6 +231,7 @@ echo "--- Test 6: Multiple procedures with contracts ---" build_goto "multi" 'procedure inc(x: int, out r: int) requires x >= 0 + opaque ensures r == x + 1 { r := x + 1; @@ -224,12 +239,15 @@ build_goto "multi" 'procedure inc(x: int, out r: int) procedure dec(x: int, out r: int) requires x > 0 + opaque ensures r == x - 1 { r := x - 1; } -procedure main() { +procedure main() + opaque +{ var x: int := 5; assert x > 0; }' @@ -263,12 +281,15 @@ echo "--- Test 7: Call inside if-then-else (GOTO output) ---" build_goto "nested_call" 'procedure inc(x: int, out r: int) requires x >= 0 + opaque ensures r == x + 1 { r := x + 1; } -procedure main() { +procedure main() + opaque +{ var a: int := 3; var b: int; if (a > 0) { @@ -299,12 +320,15 @@ echo "--- Test 8: Call inside loop (GOTO output) ---" build_goto "loop_call" 'procedure inc(x: int, out r: int) requires x >= 0 + opaque ensures r == x + 1 { r := x + 1; } -procedure main() { +procedure main() + opaque +{ var i: int := 0; var s: int := 0; while (i < 3) diff --git a/StrataTest/Languages/Boole/deterministic.lean b/StrataTest/Languages/Boole/deterministic.lean index c45c756007..f5ac8b1603 100644 --- a/StrataTest/Languages/Boole/deterministic.lean +++ b/StrataTest/Languages/Boole/deterministic.lean @@ -44,14 +44,12 @@ procedure Check(x1:int, x2:int) returns () #end -/-- info: -Obligation: Foo_ensures_0_251 -Property: assert -Result: ✅ pass - +/-- +info: Obligation: assert_1_557 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" deterministic (options := .quiet) diff --git a/StrataTest/Languages/Core/Examples/FreeRequireEnsure.lean b/StrataTest/Languages/Core/Examples/FreeRequireEnsure.lean index 43b4c86f13..b9eeb0fa0d 100644 --- a/StrataTest/Languages/Core/Examples/FreeRequireEnsure.lean +++ b/StrataTest/Languages/Core/Examples/FreeRequireEnsure.lean @@ -42,13 +42,6 @@ g_eq_15: g@1 == 15 Obligation: g@1 > 10 -Label: g_lt_10 -Property: assert -Assumptions: -g_eq_15: g@1 == 15 -Obligation: -true - Label: g_eq_15_internal Property: assert Assumptions: @@ -62,15 +55,11 @@ Obligation: g_gt_10_internal Property: assert Result: ✅ pass -Obligation: g_lt_10 -Property: assert -Result: ✅ pass - Obligation: g_eq_15_internal Property: assert Result: ❓ unknown Model: -(g@5, 0) (g@1, 0) +(g@5, 0) -/ #guard_msgs in #eval verify freeReqEnsPgm diff --git a/StrataTest/Languages/Core/Tests/PolymorphicProcedureTest.lean b/StrataTest/Languages/Core/Tests/PolymorphicProcedureTest.lean index 4ac4de001b..fe110bef30 100644 --- a/StrataTest/Languages/Core/Tests/PolymorphicProcedureTest.lean +++ b/StrataTest/Languages/Core/Tests/PolymorphicProcedureTest.lean @@ -92,11 +92,6 @@ info: [Strata.Core] Type checking succeeded. VCs: -Label: MkCons_ensures_0 -Property: assert -Obligation: -true - Label: assert_0 Property: assert Assumptions: @@ -113,10 +108,6 @@ true --- info: -Obligation: MkCons_ensures_0 -Property: assert -Result: ✅ pass - Obligation: assert_0 Property: assert Result: ✅ pass diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean index 5134de4f39..f6352c4487 100644 --- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean +++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean @@ -65,7 +65,9 @@ info: procedure foo() }; -/ #guard_msgs in -#eval do IO.println (← roundtrip r"procedure foo() opaque { assert true; assert false };") +#eval do IO.println (← roundtrip r"procedure foo() + opaque +{ assert true; assert false };") /-- info: procedure add(x: int, y: int): int @@ -75,7 +77,9 @@ info: procedure add(x: int, y: int): int }; -/ #guard_msgs in -#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int opaque { x + y };") +#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int + opaque +{ x + y };") /-- info: function aFunction(x: int): int @@ -84,7 +88,8 @@ info: function aFunction(x: int): int }; -/ #guard_msgs in -#eval do IO.println (← roundtrip r"function aFunction(x: int): int { x };") +#eval do IO.println (← roundtrip r"function aFunction(x: int): int +{ x };") /-- info: composite Point { var x: int var y: int } @@ -105,7 +110,9 @@ info: procedure test(x: int): int }; -/ #guard_msgs in -#eval do IO.println (← roundtrip r"procedure test(x: int): int opaque { if x > 0 then x else 0 - x };") +#eval do IO.println (← roundtrip r"procedure test(x: int): int + opaque +{ if x > 0 then x else 0 - x };") /-- info: procedure divide(x: int, y: int): int @@ -135,7 +142,9 @@ info: procedure test() -/ #guard_msgs in #eval do IO.println (← roundtrip r" -procedure test() opaque { +procedure test() + opaque +{ assert forall(x: int) => x == x; assert exists(y: int) => y > 0 }; @@ -158,7 +167,9 @@ composite Point { var x: int var y: int } -procedure test(): int opaque { +procedure test(): int + opaque +{ var p: Point := new Point; p#x := 5; p#x @@ -192,7 +203,9 @@ procedure test(a: Animal): bool #eval do IO.println (← roundtrip r" composite Animal {} composite Dog extends Animal {} -procedure test(a: Animal): bool opaque { a is Dog }; +procedure test(a: Animal): bool + opaque +{ a is Dog }; ") -- Additional coverage: while loops @@ -210,7 +223,9 @@ info: procedure test() -/ #guard_msgs in #eval do IO.println (← roundtrip r" -procedure test() opaque { +procedure test() + opaque +{ var x: int := 0; while(x < 10) invariant x >= 0 @@ -260,6 +275,8 @@ info: procedure test(): int }; -/ #guard_msgs in -#eval do IO.println (← roundtrip r"procedure test(): int opaque { };") +#eval do IO.println (← roundtrip r"procedure test(): int + opaque +{ };") end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean index 8a293059d5..2e5fb6c3f1 100644 --- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean +++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean @@ -23,7 +23,9 @@ namespace Strata.Laurel def testProgram : String := r" constrained nat = x: int where x >= 0 witness 0 -procedure test(n: nat) returns (r: nat) { +procedure test(n: nat) returns (r: nat) + opaque +{ assert r >= 0; var y: nat := n; return y @@ -74,7 +76,9 @@ procedure $witness_nat() -- Scope management: constrained variable in if-branch must not leak into sibling block def scopeProgram : String := r" constrained pos = v: int where v > 0 witness 1 -procedure test(b: bool) { +procedure test(b: bool) + opaque +{ if b then { var x: pos := 1 }; @@ -91,6 +95,7 @@ info: function pos$constraint(v: int): bool v > 0 }; procedure test(b: bool) + opaque { if b then { var x: int := 1; @@ -118,7 +123,9 @@ procedure $witness_pos() -- The variable has no known value, only the type constraint is assumed. def uninitProgram : String := r" constrained posint = x: int where x > 0 witness 1 -procedure f() opaque { +procedure f() + opaque +{ var x: posint; assert x == 1 }; diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean index e58d25cea1..d5d5671ade 100644 --- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean +++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean @@ -59,7 +59,7 @@ procedure callPureDivUnsafe(x: int) }; " -#guard_msgs (drop info, error) in -#eval testInputWithOffset "DivByZeroE2E" e2eProgram 22 processLaurelFile +#guard_msgs(drop info, error) in +#eval testInputWithOffset "DivByZeroE2E" e2eProgram 20 processLaurelFile end Laurel diff --git a/StrataTest/Languages/Laurel/DuplicateNameTests.lean b/StrataTest/Languages/Laurel/DuplicateNameTests.lean index beb1a06737..08c5085dea 100644 --- a/StrataTest/Languages/Laurel/DuplicateNameTests.lean +++ b/StrataTest/Languages/Laurel/DuplicateNameTests.lean @@ -72,25 +72,33 @@ composite Foo { /-! ## Duplicate parameter names in a procedure -/ def dupParams := r" -procedure foo(x: int, x: bool) opaque { }; +procedure foo(x: int, x: bool) // ^ error: Duplicate definition 'x' is already defined in this scope + opaque +{ }; " #guard_msgs (error, drop all) in -#eval testInputWithOffset "DupParams" dupParams 61 processResolution +#eval testInputWithOffset "DupParams" dupParams 77 processResolution /-! ## Duplicate instance procedure names in a composite type -/ def dupInstanceProcs := r" composite Foo { - procedure bar() opaque { }; - procedure bar() opaque { }; + procedure bar() +// ^^^ error: Instance procedure 'bar' on composite type 'Foo' is not yet supported + opaque + { }; + procedure bar() +// ^^^ error: Instance procedure 'bar' on composite type 'Foo' is not yet supported // ^^^ error: Duplicate definition 'bar' is already defined in this scope + opaque + { }; } " #guard_msgs (error, drop all) in -#eval testInputWithOffset "DupInstanceProcs" dupInstanceProcs 71 processResolution +#eval testInputWithOffset "DupInstanceProcs" dupInstanceProcs 89 processResolution /-! ## Duplicate local variable names in the same block -/ diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean index c86b0e3c9c..1fca021343 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean @@ -13,11 +13,17 @@ namespace Strata namespace Laurel def transparentBodyProgram := r" -procedure transparentBody() -// ^^^^^^^^^^^^^^^ error: transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque +procedure transparentBody(): int { - assert true + assert true; + 3 }; + +// No support for transparent void procedures yet +// procedure transparentBody() +// { +// assert true +// }; " #guard_msgs(drop info, error) in diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index e65d283f57..f0f83fc2a5 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -80,7 +80,6 @@ procedure nestedImpureStatementsAndOpaque() // An imperative procedure call in expression position is lifted before the // surrounding expression is evaluated. procedure imperativeProc(x: int) returns (r: int) - // ensures clause required because Core's symbolic verification does not support transparent proceduces yet opaque ensures r == x + 1 { @@ -139,18 +138,15 @@ procedure addProcCaller(): int { var x: int := 0; var y: int := addProc({x := 1; x}, {x := x + 10; x}); - assert y == 11 + assert y == 12; - // The next statement is not translated correctly. - // I think it's a bug in the handling of StaticCall - // Where a reference is substituted when it should not be - // var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3); - // assert z == 14 + var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3); + assert z == 15 }; " #guard_msgs (error, drop all) in -#eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFile +#eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFileKeepIntermediates end Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean index 2b3767391c..feeadbea31 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean @@ -13,7 +13,7 @@ open Strata namespace Strata.Laurel def program: String := r" -procedure impure(): int +procedure hasMutatingAssignment(): int opaque { var x: int := 0; @@ -21,29 +21,28 @@ procedure impure(): int x }; -function impureFunction1(x: int): int +function functionWithMutatingAssignment(x: int): int { x := x + 1 //^^^^^^^^^^ error: destructive assignments are not supported in functions or contracts }; -function impureFunction2(x: int): int +function functionWithWhile(x: int): int { while(false) {} //^^^^^^^^^^^^^^^ error: loops are not supported in functions or contracts }; -function impureFunction3(x: int): int +function functionCallingHasMutationAssignment(x: int): int { - impure() -//^^^^^^^^ error: calls to procedures are not supported in functions or contracts + hasMutatingAssignment() }; procedure impureContractIsNotLegal1(x: int) - requires x == impure() -// ^^^^^^^^ error: calls to procedures are not supported in functions or contracts + requires x == hasMutatingAssignment() +// ^^^^^^^^^^^^^^^^^^^^^^^ error: calls to procedures are not supported in contracts opaque { - assert impure() == 1 + assert hasMutatingAssignment() == 1 }; procedure impureContractIsNotLegal2(x: int) @@ -52,7 +51,6 @@ procedure impureContractIsNotLegal2(x: int) opaque { assert (x := 2) == 2 -// ^^^^^^ error: destructive assignments are not supported in functions or contracts }; " diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index 6e79453261..5a52a1d512 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -13,7 +13,16 @@ open Strata namespace Strata.Laurel def program := r" -function returnAtEnd(x: int) returns (r: int) { +procedure assertAndAssumeInFunctions(a: int) returns (r: int) +{ + assert 2 == 3; +//^^^^^^^^^^^^^ error: assertion does not hold + assume true; + a +}; + +function returnAtEnd(x: int) returns (r: int) +{ if x > 0 then { if x == 1 then { return 1 @@ -25,11 +34,13 @@ function returnAtEnd(x: int) returns (r: int) { } }; -function elseWithCall(): int { +function elseWithCall(): int +{ if true then 3 else returnAtEnd(3) }; -function guardInFunction(x: int) returns (r: int) { +function guardInFunction(x: int) returns (r: int) +{ if x > 0 then { if x == 1 then { return 1 @@ -46,11 +57,11 @@ procedure testFunctions() { assert returnAtEnd(1) == 1; assert returnAtEnd(1) == 2; -//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved assert guardInFunction(1) == 1; assert guardInFunction(1) == 2 -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved }; procedure guards(a: int) returns (r: int) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean index 3ebe4eb4cf..ad7ccf17e6 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean @@ -13,15 +13,6 @@ open Strata namespace Strata.Laurel def program := r" -function assertAndAssumeInFunctions(a: int) returns (r: int) -{ - assert 2 == 3; -//^^^^^^^^^^^^^ error: asserts are not YET supported in functions or contracts - assume true; -//^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts - a -}; - function letsInFunction() returns (r: int) { var x: int := 0; var y: int := x + 1; @@ -29,6 +20,11 @@ function letsInFunction() returns (r: int) { z }; +procedure callLetsInFunction() opaque { + var x: int := letsInFunction(); + assert x == 2 +}; + function localVariableWithoutInitializer(): int { var x: int; //^^^^^^^^^^ error: local variables in functions must have initializers diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean index 040bf3a186..6fa2eaab2e 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean @@ -13,7 +13,9 @@ open Strata namespace Laurel def program := r" -procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: int): int { +procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: int): int + opaque +{ var counter = 0 { while(steps > 0) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean index e1e5c0cfd8..b014d1c7cd 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean @@ -14,7 +14,7 @@ namespace Strata.Laurel def program := r" procedure fooReassign(): int - opaque + opaque // required because we don't yet support destructive assignment in transparent bodies { var x: int := 0; x := x + 1; @@ -24,7 +24,6 @@ procedure fooReassign(): int }; procedure fooSingleAssign(): int - opaque { var x: int := 0; var x2: int := x + 1; @@ -38,7 +37,7 @@ procedure fooProof() var x: int := fooReassign(); var y: int := fooSingleAssign() // The following assertions fails while it should succeed, -// because Core does not yet support transparent procedures +// because we don't yet support making fooReassign transparent // assert x == y; }; diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean index c7f1742a88..b22eee3776 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean @@ -44,7 +44,7 @@ procedure aFunctionWithPreconditionCaller() opaque { var x: int := aFunctionWithPrecondition(0) -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold // Error ranges are too wide because Core does not use expression locations }; @@ -61,7 +61,7 @@ procedure multipleRequiresCaller() { var a: int := multipleRequires(1, 2); var b: int := multipleRequires(-1, 2) -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved }; function funcMultipleRequires(x: int, y: int): int @@ -76,7 +76,7 @@ procedure funcMultipleRequiresCaller() { var a: int := funcMultipleRequires(1, 2); var b: int := funcMultipleRequires(1, -1) -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved }; " diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean index ee5cfc149d..1fd5cdfbca 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean @@ -19,6 +19,7 @@ A procedure with a decreases clause may be called in an erased context. def program := r" procedure noDecreases(x: int): boolean; + procedure caller(x: int) requires noDecreases(x) // ^ error: noDecreases can not be called from a pure context, because it is not proven to terminate diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean index 526a03dd92..28f6227e8e 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean @@ -13,6 +13,24 @@ open Strata namespace Strata.Laurel def program := r" +function opaqueFunction(x: int) returns (r: int) + requires x > 0 + opaque + ensures r > 0 +// ^^^^^ error: assertion does not hold +{ + x +}; + +procedure callerOfOpaqueFunction() + opaque +{ + var x: int := opaqueFunction(3); + assert x > 0; + assert x == 3 +//^^^^^^^^^^^^^ error: assertion could not be proved +}; + procedure opaqueBody(x: int) returns (r: int) opaque ensures r > 0 @@ -31,9 +49,9 @@ procedure callerOfOpaqueProcedure() }; procedure invalidPostcondition(x: int) - opaque - ensures false -// ^^^^^ error: assertion does not hold + opaque + ensures false +// ^^^^^ error: assertion does not hold { }; " diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean deleted file mode 100644 index d61c5849da..0000000000 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean +++ /dev/null @@ -1,39 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import StrataTest.Util.TestDiagnostics -import StrataTest.Languages.Laurel.TestExamples - -open StrataTest.Util -open Strata - -namespace Strata.Laurel - -def program := r" - -function opaqueFunction(x: int) returns (r: int) -// ^^^^^^^^^^^^^^ error: functions with postconditions are not yet supported -// The above limitation is because Core does not yet support functions with postconditions - requires x > 0 - opaque - ensures r > 0 -// The above limitation is because functions in Core do not support postconditions -{ - x -}; - -procedure callerOfOpaqueFunction() - opaque -{ - var x: int := opaqueFunction(3); - assert x > 0; -// The following assertion should fail but does not - assert x == 3 -}; -" - -#guard_msgs (drop info, error) in -#eval testInputWithOffset "Postconditions" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean index 34ef67a97e..0e6c623a03 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean @@ -5,6 +5,8 @@ -/ import Strata.SimpleAPI +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples /-! # Bodiless Procedure Inlining Test @@ -16,6 +18,9 @@ the inlined call is correctly rejected. -/ namespace Strata.Laurel.BodilessInliningTest +open StrataTest.Util +open Strata + private def laurelSource := " procedure bodilessProcedure() returns (r: int) opaque @@ -28,32 +33,12 @@ procedure caller() var x: int := bodilessProcedure(); assert x > 0; assert false +//^^^^^^^^^^^^ error: assertion could not be proved }; " -/-- info: "assert(161): ❌ fail" -/ -#guard_msgs in -#eval show IO String from do - let laurelProg ← Strata.parseLaurelText "test.laurel" laurelSource - let coreProg ← match ← Strata.laurelToCore laurelProg with - | .ok p => pure p - | .error e => throw (IO.userError s!"Translation failed: {e}") - let inlined ← match Strata.Core.inlineProcedures coreProg {} with - | .ok p => pure p - | .error e => throw (IO.userError s!"Inlining failed: {e}") - let vcResults ← - EIO.toIO (fun e => IO.Error.userError e) - (Strata.Core.verifyProgram inlined - { Core.VerifyOptions.default with verbose := .quiet } - (proceduresToVerify := some ["caller"])) - -- Collect only failing results - let failures := vcResults.filter fun vcr => - match vcr.outcome with - | .ok o => o.validityProperty != .unsat - | .error _ => true - let mut output := "" - for vcr in failures do - output := output ++ s!"{vcr.obligation.label}: {vcr.formatOutcome}" - return output +#guard_msgs (drop info, error) in +#eval testInputWithOffset "Postconditions" laurelSource 23 + (fun p => processLaurelFileWithOptions { translateOptions := { inlineFunctionsWhenPossible := true} } p) end Strata.Laurel.BodilessInliningTest diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean index d8dbacf369..1be2b5405c 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean @@ -20,7 +20,8 @@ nondet procedure nonDeterministic(x: int): (r: int) assumed }; -procedure caller() { +procedure caller() +{ var x = nonDeterministic(1) assert x > 0; var y = nonDeterministic(1) diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean index e46f03ef99..b75a63c5de 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean @@ -67,20 +67,21 @@ procedure updatesAndAliasing() assert dAlias#intValue == d#intValue }; -procedure subsequentHeapMutations(c: Container) +procedure subsequentHeapMutations() opaque - modifies c { + var c: Container := new Container; + // The additional parenthesis on the next line are needed to let the parser succeed. Joe, any idea why this is needed? var sum: int := ((c#intValue := 1) + c#intValue) + (c#intValue := 2); assert sum == 4 }; -procedure implicitEquality(c: Container, d: Container) +procedure implicitEquality() opaque - modifies c - modifies d { + var c: Container := new Container; + var d: Container := new Container; c#intValue := 1; d#intValue := 2; if c#intValue == d#intValue then { @@ -101,11 +102,11 @@ composite SameFieldName { var intValue: bool } -procedure sameFieldNameDifferentType(a: Container, b: SameFieldName) +procedure sameFieldNameDifferentType() opaque - modifies a - modifies b { + var a: Container := new Container; + var b: SameFieldName := new SameFieldName; a#intValue := 1; b#intValue := true; diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean index 52a16146c5..4ea1ec4ffc 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean @@ -127,7 +127,7 @@ procedure modifiesWildcardBodilessCaller() 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 +//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved }; procedure modifiesWildcardWithBody(c: Container, d: Container) @@ -152,7 +152,7 @@ procedure modifiesWildcardAndSpecificCaller() var x: int := d#value; modifiesWildcardAndSpecific(c, d); assert x == d#value // fails because modifies * subsumes modifies c -//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved }; " diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st index d95606784d..5732c7d40c 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st @@ -16,10 +16,11 @@ composite Container { procedure opaqueProcedure(c: Container): int reads c - ensures true + opaque ; procedure foo(c: Container, d: Container) + opaque { var x = opaqueProcedure(c); d.value = 1; @@ -33,6 +34,7 @@ procedure foo(c: Container, d: Container) procedure permissionLessReader(c: Container): int reads {} + opaque { c.value } // ^^^^^^^ error: enclosing procedure 'permissionLessReader' does not have permission to read 'c.value' ; diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st index d92a44c6bd..f287c7f84d 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st @@ -9,6 +9,7 @@ composite ImmutableContainer { } procedure valueReader(c: ImmutableContainer): int + opaque { c.value } // no reads clause needed because value is immutable ; @@ -18,7 +19,8 @@ Translation towards SMT: type Composite; function ImmutableContainer_value(c: Composite): int -function valueReader(c: Composite): int { +function valueReader(c: Composite): int +{ ImmutableContainer_value(c) } diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean index ba406b0ddc..50a880c4f6 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean @@ -89,7 +89,7 @@ procedure diamondInheritance() }; // Currently does not pass. Implementation needs b type invariant mechanism that we have yet to add. -//procedure typedParameter(b: Bottom) { +//procedure typedParameter(b: Bottom) opaque { // var b: Bottom := b; // assert b is Left; // assert b is Right; diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean index 76bb786239..cb0a8c69a1 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean @@ -27,7 +27,7 @@ composite Container { procedure incWithPrimitiveModifies(x: int) returns (r: int) opaque modifies x -// ^ error: non-composite type +// ^ error: modifies clause entry has non-composite type 'int' and will be ignored { r := x + 1 }; @@ -36,7 +36,7 @@ procedure modifyContainerAndPrimitive(c: Container, x: int) opaque modifies c modifies x -// ^ error: non-composite type +// ^ error: modifies clause entry has non-composite type 'int' and will be ignored { c#value := 1 }; diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st index cc0377ee27..dd02787340 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st @@ -23,7 +23,8 @@ composite Immutable { }; } -procedure foo() { +procedure foo() +{ val immutable = Immutable.construct(); // constructor instance method can be called as a static. }; @@ -33,7 +34,7 @@ composite ImmutableChainOfTwo { invariant other.other == this // reading other.other is allowed because the field is immutable - procedure construct() + procedure construct() constructor requires contructing == {this} ensures constructing == {} @@ -55,7 +56,8 @@ composite ImmutableChainOfTwo { }; } -procedure foo2() { +procedure foo2() +{ val immutable = ImmutableChainOfTwo.construct(); val same = immutable.other.other; assert immutable =&= same; @@ -66,7 +68,7 @@ composite UsesHelperConstructor { val x: int val y: int - procedure setXhelper() + procedure setXhelper() constructor requires constructing == {this} ensures constructing == {this} && assigned(this.x) @@ -74,7 +76,7 @@ composite UsesHelperConstructor { this.x = 3; }; - procedure construct() + procedure construct() constructor requires contructing == {this} ensures constructing == {} diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st index 5d2c02cfd5..2d9a5afaa4 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st @@ -26,14 +26,15 @@ composite Immutable { // implicit: assert modifiesOf(construct()).forall(x -> x.invariant()); }; - procedure assignToY() + procedure assignToY() constructs Immutable { this.y = 3; }; } -procedure foo() { +procedure foo() +{ var c = new Immutable.construct(); var temp = c.x; c.z = 1; @@ -41,7 +42,8 @@ procedure foo() { assert temp == c.x; // pass }; -procedure pureCompositeAllocator(): boolean { +procedure pureCompositeAllocator(): boolean +{ // can be called in a determinstic context var i: Immutable = Immutable.construct(); var j: Immutable = Immutable.construct(); diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st index 6d94f9a08d..813865f4e7 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st @@ -19,7 +19,8 @@ composite Extended2 extends Base { var z: int } -procedure typeTests(e: Extended1) { +procedure typeTests(e: Extended1) +{ var b: Base = e as Base; // even upcasts are not implicit, but they pass statically var e2 = e as Extended2; // ^^ error: could not prove 'e' is of type 'Extended2' diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st index 73a72a4738..212df76ab8 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st +++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st @@ -100,17 +100,19 @@ procedure hasClosure() returns (r: int) // Option B: type closures composite ATrait { - procedure foo() returns (r: int) ensures r > 0 { + procedure foo() returns (r: int) ensures r > 0 + { abstract }; } procedure hasClosure() returns (r: int) + opaque ensures r == 7 { var x = 3; var aClosure := closure extends ATrait { - procedure foo() returns (r: int) + procedure foo() returns (r: int) { r = x + 4; }; diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean index 02b5729dc8..c5f150cb95 100644 --- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean +++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean @@ -15,7 +15,7 @@ namespace Laurel def program := r#" procedure testStringKO() -returns (result: string) + returns (result: string) opaque { var message: string := "Hello"; diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean index 98e1706a3f..65d86b9e4f 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean @@ -41,14 +41,16 @@ def parseLaurelAndLift (input : String) : IO Program := do | .ok program => let result := resolve program let (program, model) := (result.program, result.model) - pure (liftExpressionAssignments model program) + let imperativeCallees := program.staticProcedures.filter (fun p => !p.isFunctional) + |>.map (fun p => p.name.text) + pure (liftExpressionAssignments program model imperativeCallees) /-- info: procedure assertInBlockExpr() opaque { var x: int := 0; - assert x == 0; + assert $x_0 == 0; var $x_0: int := x; x := 1; var y: int := { diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean index 08966a3321..857a0da7aa 100644 --- a/StrataTest/Languages/Laurel/LiftHolesTest.lean +++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean @@ -53,7 +53,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := 1 + }; +procedure test() + opaque +{ var x: int := 1 + }; " -- Bare Hole as Assign Declare initializer → replaced with call (no longer preserved as havoc). @@ -69,7 +71,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := }; +procedure test() + opaque +{ var x: int := }; " -- Hole in comparison arg inside assert → int (inferred from sibling literal). @@ -85,7 +89,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { assert > 0 }; +procedure test() + opaque +{ assert > 0 }; " -- Hole directly as assert condition → bool. @@ -101,7 +107,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { assert }; +procedure test() + opaque +{ assert }; " -- Hole directly as assume condition → bool. @@ -117,7 +125,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { assume }; +procedure test() + opaque +{ assume }; " -- Hole as if-then-else condition → bool. @@ -135,7 +145,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { if then { assert true } }; +procedure test() + opaque +{ if then { assert true } }; " -- Hole in then-branch of if-then-else inside typed local variable → int. @@ -151,7 +163,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := if true then else 0 }; +procedure test() + opaque +{ var x: int := if true then else 0 }; " -- Hole as while-loop condition → bool. @@ -169,7 +183,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { while() {} }; +procedure test() + opaque +{ while() {} }; " -- Hole as while-loop invariant → bool. @@ -188,7 +204,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { while(true) invariant {} }; +procedure test() + opaque +{ while(true) invariant {} }; " /-! ## Operators -/ @@ -206,7 +224,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { assert true && }; +procedure test() + opaque +{ assert true && }; " -- Hole in Neg inside typed local variable → int. @@ -222,7 +242,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := - }; +procedure test() + opaque +{ var x: int := - }; " -- Hole in StrConcat inside typed local variable → string. @@ -231,14 +253,13 @@ info: function $hole_0() returns ($result: string) opaque; procedure test() - opaque { var s: string := "hello" ++ $hole_0() }; -/ #guard_msgs in #eval! parseElimAndPrint - "procedure test() opaque { var s: string := \"hello\" ++ };" + "procedure test() { var s: string := \"hello\" ++ };" /-! ## Multiple holes -/ @@ -258,7 +279,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := + }; +procedure test() + opaque +{ var x: int := + }; " -- Holes across statements: Mul arg (int) then assert condition (bool). @@ -278,7 +301,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := 2 * ; assert }; +procedure test() + opaque +{ var x: int := 2 * ; assert }; " /-! ## Combinations: holes in nested contexts -/ @@ -298,7 +323,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { if 1 + > 0 then { assert true } }; +procedure test() + opaque +{ if 1 + > 0 then { assert true } }; " -- Hole in Implies inside while invariant → bool. @@ -318,7 +345,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var p: bool; while(true) invariant p ==> {} }; +procedure test() + opaque +{ var p: bool; while(true) invariant p ==> {} }; " -- Hole in Mul inside typed local variable with real type → real. @@ -334,7 +363,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var r: real := 3.14 * }; +procedure test() + opaque +{ var r: real := 3.14 * }; " /-! ## Call argument and return type inference -/ @@ -352,7 +383,9 @@ procedure test(n: int) -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test(n: int) opaque { assert n > }; +procedure test(n: int) + opaque +{ assert n > }; " /-! ## Holes in functions -/ @@ -370,7 +403,9 @@ function test(x: int): int -/ #guard_msgs in #eval! parseElimAndPrint r" -function test(x: int): int opaque { }; +function test(x: int): int + opaque +{ }; " /-! ## Nondeterministic holes () -/ @@ -385,7 +420,9 @@ info: procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { assert }; +procedure test() + opaque +{ assert }; " -- Mixed: det hole eliminated, nondet hole preserved. @@ -402,7 +439,9 @@ procedure test() -/ #guard_msgs in #eval! parseElimAndPrint r" -procedure test() opaque { var x: int := ; assert }; +procedure test() + opaque +{ var x: int := ; assert }; " -- Nondet hole in function → should be rejected (not tested here since diff --git a/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean index f44067848c..1ee8f98d55 100644 --- a/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean +++ b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean @@ -31,7 +31,7 @@ private def parseLaurelAndLift (input : String) : IO Program := do | .ok program => let result := resolve program let (program, model) := (result.program, result.model) - pure (liftExpressionAssignments model program) + pure (liftExpressionAssignments program model []) private def printLifted (input : String) : IO Unit := do let program ← parseLaurelAndLift input @@ -49,9 +49,7 @@ info: procedure impure(): int }; procedure test() { - var $c_0: int; - $c_0 := impure(); - assert $c_0 == 1 + assert impure() == 1 }; -/ #guard_msgs in @@ -94,9 +92,7 @@ info: procedure impure(): int }; procedure test() { - var $c_0: int; - $c_0 := impure(); - assume $c_0 == 1 + assume impure() == 1 }; -/ #guard_msgs in @@ -124,9 +120,7 @@ info: procedure multi_out(x: int) }; procedure test() { - var $c_0: BUG_MultiValuedExpr; - $c_0 := multi_out(5); - assert $c_0 == 6 + assert multi_out(5) == 6 }; -/ #guard_msgs in diff --git a/StrataTest/Languages/Laurel/StatisticsTest.lean b/StrataTest/Languages/Laurel/StatisticsTest.lean index 00bc6c7b24..94deaaf6d9 100644 --- a/StrataTest/Languages/Laurel/StatisticsTest.lean +++ b/StrataTest/Languages/Laurel/StatisticsTest.lean @@ -66,6 +66,7 @@ procedure p1(a: bool, b: bool) returns (r: bool) }; procedure p2(x: int) returns (y: int) + opaque { y := x + }; diff --git a/StrataTest/Languages/Python/ToLaurelTest.lean b/StrataTest/Languages/Python/ToLaurelTest.lean index 534056eafa..42f0fd1cda 100644 --- a/StrataTest/Languages/Python/ToLaurelTest.lean +++ b/StrataTest/Languages/Python/ToLaurelTest.lean @@ -422,7 +422,7 @@ info: errors: 1 -- Regression test for issue #800: nested dict access `kwargs["Outer"]["Inner"]` -- should generate `Any_get` (dict lookup), not `FieldSelect`. /-- -info: body contains Any_get: true +info: preconditions contain Any_get: true body contains FieldSelect: false -/ #guard_msgs in @@ -443,11 +443,13 @@ body contains FieldSelect: false assert! result.errors.size = 0 match result.program.staticProcedures with | proc :: _ => + let precondStr := proc.preconditions.map (fun (p : Strata.Laurel.Condition) => toString (Strata.Laurel.formatStmtExpr p.condition)) + |> String.intercalate ", " let bodyStr := match proc.body with | .Transparent body => toString (Strata.Laurel.formatStmtExpr body) | .Opaque _ (some body) _ => toString (Strata.Laurel.formatStmtExpr body) | _ => "" - IO.println s!"body contains Any_get: {bodyStr.contains "Any_get"}" + IO.println s!"preconditions contain Any_get: {precondStr.contains "Any_get"}" IO.println s!"body contains FieldSelect: {bodyStr.contains "#"}" | [] => IO.println "no procedures" @@ -678,7 +680,13 @@ private def translatePrecondResult (preconditions : Array Assertion) private def translatePrecond (preconditions : Array Assertion) (args : Array Arg := #[]) : String × Nat := let result := translatePrecondResult preconditions args - (getBody result |>.getD "", result.errors.size) + let precondStr := match result.program.staticProcedures with + | proc :: _ => + let formatted := proc.preconditions.map (fun (p : Strata.Laurel.Condition) => toString (Strata.Laurel.formatStmtExpr p.condition)) + if formatted.isEmpty then getBody result |>.getD "" + else "{ " ++ (String.intercalate "; " formatted) ++ " }" + | [] => "" + (precondStr, result.errors.size) -- enumMember: or and eq via `|` and `==` infix syntax #eval do @@ -718,12 +726,13 @@ private def translatePrecond (preconditions : Array Assertion) message := #[], formula := .containsKey (.var "kwargs" loc) "key" loc }] postconditions := #[] }] "" - let body := getBody result |>.getD "" assertEq result.errors.size 0 - assert! body.contains "result := " - assert! body.contains "Any..isfrom_None(key) | Any..isfrom_str(key)" - assert! body.contains "assert !Any..isfrom_None(key) summary \"precondition 0\"" - assert! body.contains "assume Any..isfrom_str(result)" + match result.program.staticProcedures with + | proc :: _ => + let precondStr := proc.preconditions.map (fun (p : Strata.Laurel.Condition) => toString (Strata.Laurel.formatStmtExpr p.condition)) + |> String.intercalate ", " + assert! precondStr.contains "!Any..isfrom_None(key)" + | [] => assert! false -- containsKey on a non-kwargs dict: DictStrAny_contains in an assert -- (would have been silently dropped before fix #2) diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected index 2583076f7e..bbe3923445 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected @@ -1,3 +1,3 @@ -test_class_decl.py(9, 4): ✅ pass - (CircularBuffer@__init__ requires) Type constraint of n +test_class_decl.py(9, 4): ✅ pass - callElimAssert_requires_15 DETAIL: 1 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected index c6e5abb610..ddc56f0a86 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected @@ -1,3 +1,4 @@ +test_class_field_any.py(5, 0): ✅ pass - callElimAssert_requires_5 test_class_field_any.py(6, 0): ❓ unknown - assert(113) -DETAIL: 0 passed, 0 failed, 1 inconclusive +DETAIL: 1 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected b/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected index 703165c2c1..e2c3e24d2e 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected @@ -1,3 +1,4 @@ +test_class_inheritance_no_dispatch.py(24, 4): ✅ pass - callElimAssert_requires_4 test_class_inheritance_no_dispatch.py(25, 4): ❓ unknown - assert(714) -DETAIL: 0 passed, 0 failed, 1 inconclusive +DETAIL: 1 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected index 0047be2edb..6910ccfc27 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected @@ -1,6 +1,6 @@ test_class_method_call_from_main.py(10, 8): ❓ unknown - name must not be empty -test_class_method_call_from_main.py(9, 23): ❓ unknown - (Greeter@greet ensures) Return type constraint -test_class_method_call_from_main.py(14, 4): ✅ pass - (Greeter@__init__ requires) Type constraint of name -test_class_method_call_from_main.py(15, 4): ✅ pass - assert(415) +test_class_method_call_from_main.py(14, 4): ✅ pass - callElimAssert_requires_10 +test_class_method_call_from_main.py(15, 4): ✅ pass - callElimAssert_requires_3 +test_class_method_call_from_main.py(15, 4): ❓ unknown - assert(415) DETAIL: 2 passed, 0 failed, 2 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected index 29b6682a29..38d03f1a2c 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected @@ -1,5 +1,4 @@ -test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4 test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__ -DETAIL: 2 passed, 0 failed, 1 inconclusive -RESULT: Inconclusive +DETAIL: 2 passed, 0 failed, 0 inconclusive +RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected b/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected index 9380a52945..a20220ac72 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected @@ -1,3 +1,3 @@ -test_composite_return.py(10, 4): ✅ pass - (MyService@__init__ requires) Type constraint of name +test_composite_return.py(10, 4): ✅ pass - callElimAssert_requires_5 DETAIL: 1 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_field_write.expected b/StrataTest/Languages/Python/expected_laurel/test_field_write.expected index cb51cb69f9..b949adc131 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_field_write.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_field_write.expected @@ -1,4 +1,4 @@ -test_field_write.py(8, 4): ✅ pass - (Cell@__init__ requires) Type constraint of val +test_field_write.py(8, 4): ✅ pass - callElimAssert_requires_5 test_field_write.py(10, 4): ✅ pass - field overwritten DETAIL: 2 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected index 315f62f13d..dd2e51989d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected @@ -1,9 +1,4 @@ -test_method_call_with_kwargs.py(5, 82): ✅ pass - (MyClass@some_method ensures) Return type constraint -test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip1 -test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip2 -test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip3 -test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1 -test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip2 -test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip3 -DETAIL: 7 passed, 0 failed, 0 inconclusive +test_method_call_with_kwargs.py(8, 0): ✅ pass - callElimAssert_requires_14 +test_method_call_with_kwargs.py(9, 0): ✅ pass - callElimAssert_requires_6 +DETAIL: 2 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected index 56de827e26..4976db9c39 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected @@ -1,12 +1,10 @@ -test_method_kwargs_no_hierarchy.py(5, 41): ❓ unknown - (Calculator@add ensures) Return type constraint -test_method_kwargs_no_hierarchy.py(9, 4): ✅ pass - (Calculator@__init__ requires) Type constraint of base +test_method_kwargs_no_hierarchy.py(9, 4): ✅ pass - callElimAssert_requires_12 unknown location: ✅ pass - assert_assert(0)_calls_Any_get_or_none_0 unknown location: ✅ pass - assert(0) test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - init_calls_Any_get_or_none_0 -test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of x -test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of y -test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254) +test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - callElimAssert_requires_5 +test_method_kwargs_no_hierarchy.py(11, 4): ❓ unknown - assert(254) test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286) test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint -DETAIL: 8 passed, 0 failed, 2 inconclusive +DETAIL: 6 passed, 0 failed, 2 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected b/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected index 86faeff6d1..62320a336f 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected @@ -1,4 +1,7 @@ +test_with_void_enter.py(12, 4): ✅ pass - callElimAssert_requires_14 +unknown location: ✅ pass - callElimAssert_requires_9 test_with_void_enter.py(14, 8): ✅ pass - assert(272) +test_with_void_enter.py(13, 4): ✅ pass - callElimAssert_requires_4 test_with_void_enter.py(15, 4): ✅ pass - assert(287) -DETAIL: 2 passed, 0 failed, 0 inconclusive +DETAIL: 5 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index 1e12630061..0b63cb9bbb 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -67,7 +67,11 @@ "test_with_statement", "test_fstrings", } -SKIP_TESTS_LAUREL = BOTH_SKIP +SKIP_TESTS_LAUREL = BOTH_SKIP | { + "test_try_except", # TVoid type from raise statements not supported in function copies + "test_multiple_except", # TVoid type from raise statements not supported in function copies + "test_datetime_now_tz", # Resolution failure: timezone/utc not defined +} def run(test_file: str, *, laurel: bool) -> bool: diff --git a/StrataTest/Languages/Python/tests/cbmc_expected.txt b/StrataTest/Languages/Python/tests/cbmc_expected.txt index 0dc6283317..b078d4aaff 100644 --- a/StrataTest/Languages/Python/tests/cbmc_expected.txt +++ b/StrataTest/Languages/Python/tests/cbmc_expected.txt @@ -33,6 +33,7 @@ test_if_elif.py.ion SKIP test_variable_reassign.py.ion SKIP test_datetime_now_tz.py.ion SKIP test_timedelta_expr.py.ion SKIP +test_composite_return.py.ion PASS test_multi_assign.py.ion FAIL test_multi_assign_triple.py.ion FAIL test_multi_assign_side_effect.py.ion SKIP diff --git a/StrataTest/Util/TestDiagnostics.lean b/StrataTest/Util/TestDiagnostics.lean index ebfb9f8ecb..3a23a20c4b 100644 --- a/StrataTest/Util/TestDiagnostics.lean +++ b/StrataTest/Util/TestDiagnostics.lean @@ -137,6 +137,10 @@ def testInputWithOffset (filename: String) (input : String) (lineOffset : Nat) IO.println s!"\nUnexpected diagnostics:" for diag in unmatchedDiagnostics do IO.println s!" - Line {diag.start.line}, Col {diag.start.column}-{diag.ending.column}: {diag.message}" + + if unmatchedExpectations.length == 0 && unmatchedDiagnostics.length == 0 then + IO.println s!"Duplicate diagnostics: {repr diagnostics}" + throw (IO.userError "Test failed") def testInput (filename: String) (input : String) (process : Lean.Parser.InputContext -> IO (Array Diagnostic)) : IO Unit :=