diff --git a/.gitignore b/.gitignore index 3776616d98..f7d8f2cb47 100644 --- a/.gitignore +++ b/.gitignore @@ -12,4 +12,4 @@ vcs/*.smt2 *.py.ion *.py.ion.core.st -Strata.code-workspace \ No newline at end of file +Strata.code-workspace diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean index 7e86c374a1..dce1a2eef3 100644 --- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean +++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean @@ -224,7 +224,7 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : { name := mkId s!"$witness_{ct.name.text}" inputs := [] outputs := [] - body := .Transparent ⟨.Block [witnessInit, assert] none, src⟩ + body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) [] preconditions := [] isFunctional := false decreases := none } diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index fecaf5350c..dae58c3caa 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -9,6 +9,7 @@ public import Strata.Languages.Laurel.Laurel public import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator public import Strata.Languages.Laurel.LaurelTypes public import Strata.Languages.Laurel.HeapParameterizationConstants +public import Strata.Languages.Laurel.MapStmtExpr public import Strata.Util.Tactics /- @@ -253,6 +254,10 @@ def resolveQualifiedFieldName (model: SemanticModel) (fieldName : Identifier) : | .unresolved _ => none | _ => dbg_trace s!"BUG: resolveQualifiedFieldName {fieldName} did resolved to something other than a field"; none +private def wrapList (source : Option FileRange) : List StmtExprMd → StmtExprMd + | [single] => single + | many => ⟨.Block many none, source⟩ + /-- Transform an expression, adding heap parameters where needed. - `heapVar`: the name of the heap variable to use @@ -260,22 +265,25 @@ Transform an expression, adding heap parameters where needed. - `valueUsed`: whether the result value of this expression is used (affects optimization of heap-writing calls) -/ def heapTransformExpr (heapVar : Identifier) (model: SemanticModel) (expr : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := - recurse expr valueUsed + recurseOne expr valueUsed where - recurse (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do + recurseOne (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := + wrapList exprMd.source <$> recurse exprMd valueUsed + termination_by (sizeOf exprMd, 1) + recurse (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM (List StmtExprMd) := do let ⟨expr, source⟩ := exprMd match _h : expr with | .Var (.Field selectTarget fieldName) => do let some qualifiedName := resolveQualifiedFieldName model fieldName - | return ⟨ .Hole, source ⟩ + | return [⟨ .Hole, source ⟩] let valTy := (model.get fieldName).getType let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩ -- Unwrap Box: apply the appropriate destructor recordBoxConstructor model valTy.val - return mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr] + return [mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr]] | .StaticCall callee args => - let args' ← args.mapM (recurse ·) + let args' ← args.mapM (recurseOne ·) let calleeReadsHeap ← readsHeap callee let calleeWritesHeap ← writesHeap callee if calleeWritesHeap then @@ -284,7 +292,7 @@ where let callWithHeap := ⟨ .Assign [mkVarMd (.Local heapVar), mkVarMd (.Declare ⟨freshVar, computeExprType model exprMd⟩)] (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩), source ⟩ - return ⟨ .Block [callWithHeap, mkMd (.Var (.Local freshVar))] none, source ⟩ + return [callWithHeap, mkMd (.Var (.Local freshVar))] else -- Generate throwaway Declare targets for any non-heap outputs let procOutputs := match model.get callee with @@ -294,18 +302,18 @@ where let extraTargets ← procOutputs.mapM fun out => do pure (mkVarMd (.Declare ⟨← freshVarName, out.type⟩)) let allTargets := mkVarMd (.Local heapVar) :: extraTargets - return ⟨ .Assign allTargets (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩), source ⟩ + return [⟨ .Assign allTargets (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩), source ⟩] else if calleeReadsHeap then - return ⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩ + return [⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩] else - return ⟨ .StaticCall callee args', source ⟩ + return [⟨ .StaticCall callee args', source ⟩] | .InstanceCall callTarget callee args => - let t ← recurse callTarget - let args' ← args.mapM (recurse ·) - return ⟨ .InstanceCall t callee args', source ⟩ + let t ← recurseOne callTarget + let args' ← args.mapM (recurseOne ·) + return [⟨ .InstanceCall t callee args', source ⟩] | .IfThenElse c t e => - let e' ← match e with | some x => some <$> recurse x valueUsed | none => pure none - return ⟨ .IfThenElse (← recurse c) (← recurse t valueUsed) e', source ⟩ + let e' ← match e with | some x => some <$> recurseOne x valueUsed | none => pure none + return [⟨ .IfThenElse (← recurseOne c) (← recurseOne t valueUsed) e', source ⟩] | .Block stmts label => let n := stmts.length let rec processStmts (idx : Nat) (remaining : List StmtExprMd) : TransformM (List StmtExprMd) := do @@ -315,16 +323,16 @@ where let isLast := idx == n - 1 let s' ← recurse s (isLast && valueUsed) let rest' ← processStmts (idx + 1) rest - pure (s' :: rest') - termination_by sizeOf remaining + pure (s' ++ rest') + termination_by (sizeOf remaining, 0) let stmts' ← processStmts 0 stmts - return ⟨ .Block stmts' label, source ⟩ + return [⟨ .Block stmts' label, source ⟩] | .While c invs d b => - let invs' ← invs.mapM (recurse ·) - return ⟨ .While (← recurse c) invs' d (← recurse b false), source ⟩ + let invs' ← invs.mapM (recurseOne ·) + return [⟨ .While (← recurseOne c) invs' d (← recurseOne b false), source ⟩] | .Return v => - let v' ← match v with | some x => some <$> recurse x | none => pure none - return ⟨ .Return v', source ⟩ + let v' ← match v with | some x => some <$> recurseOne x | none => pure none + return [⟨ .Return v', source ⟩] | .Assign targets v => -- Process field targets @@ -338,7 +346,7 @@ where let valTy := (model.get fieldName).getType recordBoxConstructor model valTy.val let freshVar ← freshVarName - let target' ← recurse target + let target' ← recurseOne target let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [mkMd (.Var (.Local freshVar))] let updateStmt : StmtExprMd := ⟨ .Assign [mkVarMd (.Local heapVar)] (mkMd (.StaticCall "updateField" [mkMd (.Var (.Local heapVar)), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source ⟩ @@ -350,7 +358,7 @@ where -- Detect calls and add a heap argument if needed let (v', addedHeap) <- match _hv : v.val with | .StaticCall callee args => do - let args' <- args.mapM recurse + let args' <- args.mapM recurseOne let calleeWritesHeap ← writesHeap callee let calleeReadsHeap ← readsHeap callee if calleeWritesHeap then @@ -360,11 +368,11 @@ where else pure (⟨ .StaticCall callee args', v.source ⟩, false) | .InstanceCall callTarget _callee args => do - let _callTarget' ← recurse callTarget - let _args' <- args.mapM recurse + let _callTarget' ← recurseOne callTarget + let _args' <- args.mapM recurseOne pure (⟨ .InstanceCall _callTarget' _callee _args', v.source ⟩, false) | _ => - pure (<- recurse v, false) + pure (<- recurseOne v, false) let allTargets := if addedHeap then ⟨ Variable.Local heapVar, v.source ⟩ :: processedTargets else processedTargets @@ -387,15 +395,12 @@ where else updateStatements pure (newAssign, suffixes) - -- Create a block if necessary - if suffixes.length > 0 then - return ⟨ StmtExpr.Block (newAssign :: suffixes) none, source ⟩ - else - return newAssign + -- Return the list of statements directly (flattened into enclosing block) + return newAssign :: suffixes - | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← recurse t) f (← recurse v), source ⟩ + | .PureFieldUpdate t f v => return [⟨ .PureFieldUpdate (← recurseOne t) f (← recurseOne v), source ⟩] | .PrimitiveOp op args => - let args' ← args.mapM (recurse ·) + let args' ← args.mapM (recurseOne ·) -- For == and != on Composite types, compare refs instead match op, args with | .Eq, [e1, _e2] => @@ -404,58 +409,58 @@ where | .UserDefined _ => let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!]) let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!]) - return ⟨ .PrimitiveOp .Eq [ref1, ref2], source ⟩ - | _ => return ⟨ .PrimitiveOp op args', source ⟩ + return [⟨ .PrimitiveOp .Eq [ref1, ref2], source ⟩] + | _ => return [⟨ .PrimitiveOp op args', source ⟩] | .Neq, [e1, _e2] => let ty := (computeExprType model e1).val match ty with | .UserDefined _ => let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!]) let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!]) - return ⟨ .PrimitiveOp .Neq [ref1, ref2], source ⟩ - | _ => return ⟨ .PrimitiveOp op args', source ⟩ - | _, _ => return ⟨ .PrimitiveOp op args', source ⟩ - | .New _ => return exprMd - | .ReferenceEquals l r => return ⟨ .ReferenceEquals (← recurse l) (← recurse r), source ⟩ + return [⟨ .PrimitiveOp .Neq [ref1, ref2], source ⟩] + | _ => return [⟨ .PrimitiveOp op args', source ⟩] + | _, _ => return [⟨ .PrimitiveOp op args', source ⟩] + | .New _ => return [exprMd] + | .ReferenceEquals l r => return [⟨ .ReferenceEquals (← recurseOne l) (← recurseOne r), source ⟩] | .AsType t ty => - let t' ← recurse t valueUsed + let t' ← recurseOne t valueUsed let isCheck := ⟨ .IsType t' ty, source ⟩ let assertStmt := ⟨ .Assert { condition := isCheck }, source ⟩ - return ⟨ .Block [assertStmt, t'] none, source ⟩ - | .IsType t ty => return ⟨ .IsType (← recurse t) ty, source ⟩ + return [⟨ .Block [assertStmt, t'] none, source ⟩] + | .IsType t ty => return [⟨ .IsType (← recurseOne t) ty, source ⟩] | .Quantifier mode p trigger b => - let trigger' ← trigger.attach.mapM fun ⟨t, _⟩ => recurse t - return ⟨.Quantifier mode p trigger' (← recurse b), source⟩ - | .Assigned n => return ⟨ .Assigned (← recurse n), source ⟩ - | .Old v => return ⟨ .Old (← recurse v), source ⟩ - | .Fresh v => return ⟨ .Fresh (← recurse v), source ⟩ + let trigger' ← trigger.attach.mapM fun ⟨t, _⟩ => recurseOne t + return [⟨.Quantifier mode p trigger' (← recurseOne b), source⟩] + | .Assigned n => return [⟨ .Assigned (← recurseOne n), source ⟩] + | .Old v => return [⟨ .Old (← recurseOne v), source ⟩] + | .Fresh v => return [⟨ .Fresh (← recurseOne v), source ⟩] | .Assert ⟨condExpr, summary⟩ => - return ⟨ .Assert { condition := ← recurse condExpr, summary }, 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 ⟩ - | _ => return exprMd - termination_by sizeOf exprMd - decreasing_by - all_goals simp_wf - all_goals (try have := AstNode.sizeOf_val_lt exprMd) - all_goals (try have := AstNode.sizeOf_val_lt v) - all_goals (try term_by_mem) - all_goals (try (cases exprMd; simp_all; omega)) - -- For field inner expressions in attach-based: - all_goals (try ( - have := List.sizeOf_lt_of_mem ‹_› - have := Variable.sizeOf_field_target_lt_of_eq _htv - omega)) - -- Remaining goals - all_goals ( - cases exprMd with | mk val src mmd => - simp_all - omega) + return [⟨ .Assert { condition := ← recurseOne condExpr, summary }, source ⟩] + | .Assume c => return [⟨ .Assume (← recurseOne c), source ⟩] + | .ProveBy v p => return [⟨ .ProveBy (← recurseOne v) (← recurseOne p), source ⟩] + | .ContractOf ty f => return [⟨ .ContractOf ty (← recurseOne f), source ⟩] + | _ => return [exprMd] + termination_by (sizeOf exprMd, 0) + decreasing_by + all_goals simp_wf + all_goals (try have := AstNode.sizeOf_val_lt exprMd) + all_goals (try have := AstNode.sizeOf_val_lt v) + all_goals (try term_by_mem) + all_goals (try (cases exprMd; simp_all; omega)) + -- For field inner expressions in attach-based: + all_goals (try ( + have := List.sizeOf_lt_of_mem ‹_› + have := Variable.sizeOf_field_target_lt_of_eq _htv + omega)) + -- Remaining goals + all_goals ( + cases exprMd with | mk val src => + simp_all + omega) def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : TransformM Procedure := do - let heapName : Identifier := "$heap" - let heapInName : Identifier := "$heap_in" + let heapName := heapVarName + let heapInName := heapInVarName let readsHeap := (← get).heapReaders.contains proc.name let writesHeap := (← get).heapWriters.contains proc.name diff --git a/Strata/Languages/Laurel/HeapParameterizationConstants.lean b/Strata/Languages/Laurel/HeapParameterizationConstants.lean index 758aa149a1..bfa76a4a59 100644 --- a/Strata/Languages/Laurel/HeapParameterizationConstants.lean +++ b/Strata/Languages/Laurel/HeapParameterizationConstants.lean @@ -15,6 +15,12 @@ namespace Strata.Laurel public section +/-- The name of the heap variable used by the heap parameterization pass. -/ +def heapVarName : Identifier := "$heap" + +/-- The name of the input heap parameter used by the heap parameterization pass. -/ +def heapInVarName : Identifier := "$heap_in" + /-- The Laurel Core prelude defines the heap model types and operations used by the Laurel-to-Core translator. These declarations are expressed diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index e809401ccc..54b97fdfd9 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean @@ -179,6 +179,9 @@ private def runLaurelPasses (options : LaurelTranslateOptions) -- Run resolve after the pass if needed if pass.needsResolves then let result := resolve program (some model) + let newErrors := result.errors.filter fun e => !resolutionErrors.contains e + if !newErrors.isEmpty then + emit pass.name "laurel.st" program program := result.program model := result.model emit pass.name "laurel.st" program diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index 20fd01445d..5fb37c60ad 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -9,6 +9,7 @@ public import Strata.Languages.Laurel.Laurel public import Strata.Languages.Laurel.LaurelTypes public import Strata.Languages.Core.Verifier public import Strata.Languages.Laurel.Resolution +import Strata.Languages.Laurel.HeapParameterizationConstants /- Modifies clause transformation (Laurel → Laurel). @@ -159,8 +160,8 @@ def transformModifiesClauses (model: SemanticModel) -- modifies * means the procedure can modify anything; no frame condition .ok { proc with body := .Opaque postconds impl [] } else if hasHeapOut proc then - let heapInName : Identifier := "$heap_in" - let heapName : Identifier := "$heap" + let heapInName := heapInVarName + let heapName := heapVarName let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName let postconds' := match frameCondition with | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }] diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index 411c61b95f..26b72ff23f 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -8,6 +8,7 @@ module public import Strata.Languages.Laurel.MapStmtExpr public import Strata.Languages.Laurel.LaurelTypes public import Strata.DL.Imperative.MetaData +import Strata.Languages.Laurel.HeapParameterizationConstants import Strata.Util.Tactics public section @@ -235,7 +236,7 @@ Lower `New name` to a block that: 3. Constructs a `MkComposite(counter, name_TypeTag())` value -/ def lowerNew (name : Identifier) (source : Option FileRange) : THM StmtExprMd := do - let heapVar : Identifier := "$heap" + let heapVar := heapVarName let freshVar ← freshVarName let getCounter := mkMd (.StaticCall "Heap..nextReference!" [mkMd (.Var (.Local heapVar))]) let saveCounter := mkMd (.Assign [mkVarMd (.Declare ⟨freshVar, ⟨.TInt, none⟩⟩)] getCounter) diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean index 86ce51e683..0811d5e955 100644 --- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean +++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean @@ -52,6 +52,7 @@ procedure test(n: int) ensures nat$constraint(r) { assert r >= 0; var y: int := n; assert nat$constraint(y); return y }; procedure $witness_nat() + opaque { var $witness: int := 0; assert nat$constraint($witness) }; -/ #guard_msgs in @@ -80,6 +81,7 @@ info: function pos$constraint(v: int): bool procedure test(b: bool) { if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } }; procedure $witness_pos() + opaque { var $witness: int := 1; assert pos$constraint($witness) }; -/ #guard_msgs in @@ -104,6 +106,7 @@ info: function posint$constraint(x: int): bool procedure f() { var x: int; assume posint$constraint(x); assert x == 1 }; procedure $witness_posint() + opaque { var $witness: int := 1; assert posint$constraint($witness) }; -/ #guard_msgs in diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean index 7dbf35022d..e46f03ef99 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean @@ -199,5 +199,5 @@ procedure fieldTargetInMultiAssign() }; "# -#guard_msgs(drop info, error) in +#guard_msgs (drop info, error) in #eval testInputWithOffset "MutableFields" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean index ec05fcfd3d..189295102d 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean @@ -15,8 +15,8 @@ namespace Strata.Laurel def instanceProcedureProgram := r" composite Counter { var count: int - procedure increment(self: Counter) -// ^^^^^^^^^ error: Instance procedure 'increment' on composite type 'Counter' is not yet supported + procedure self_increment(self: Counter) +// ^^^^^^^^^^^^^^ error: Instance procedure 'self_increment' on composite type 'Counter' is not yet supported opaque { self#count := self#count + 1 diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean index 5affbb2813..00d14ae804 100644 --- a/StrataTest/Languages/Laurel/TestExamples.lean +++ b/StrataTest/Languages/Laurel/TestExamples.lean @@ -36,4 +36,17 @@ def processLaurelFileWithOptions (options : LaurelVerifyOptions) (input : InputC def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := processLaurelFileWithOptions default input +/-- Path to the directory for intermediate files, inside the build directory. + Resolved from the current working directory so it works on any machine. -/ +def buildDir : IO String := do + let cwd ← IO.currentDir + return s!"{cwd}/.lake/build/intermediatePrograms/" + +/-- Debug helper: run the Laurel pipeline keeping intermediate pass outputs in `.lake/build/intermediatePrograms/`. + Not used by any test in this repo; invoke manually via `#eval processLaurelFileKeepIntermediates (stringInputContext …)` + when diagnosing pass-internal issues. -/ +def processLaurelFileKeepIntermediates (input : InputContext) : IO (Array Diagnostic) := do + let dir ← buildDir + processLaurelFileWithOptions { translateOptions := { keepAllFilesPrefix := dir}} input + end Laurel