diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index 2cc71be22..b6fca8d2d 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -188,6 +188,7 @@ inductive SepFormat where | comma -- Comma separator (CommaSepBy) | space -- Space separator (SpaceSepBy) | spacePrefix -- Space before each element (SpacePrefixSepBy) +| newline -- Newline separator (NewlineSepBy) deriving Inhabited, Repr, BEq namespace SepFormat @@ -197,18 +198,21 @@ def toString : SepFormat → String | .comma => "commaSepBy" | .space => "spaceSepBy" | .spacePrefix => "spacePrefixSepBy" + | .newline => "newlineSepBy" def toIonName : SepFormat → String | .none => "seq" | .comma => "commaSepList" | .space => "spaceSepList" | .spacePrefix => "spacePrefixedList" + | .newline => "newlineSepList" def fromIonName? : String → Option SepFormat | "seq" => some .none | "commaSepList" => some .comma | "spaceSepList" => some .space | "spacePrefixedList" => some .spacePrefix + | "newlineSepList" => some .newline | _ => none theorem fromIonName_toIonName_roundtrip (sep : SepFormat) : diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean index 20ebfda38..927bb3600 100644 --- a/Strata/DDM/BuiltinDialects/Init.lean +++ b/Strata/DDM/BuiltinDialects/Init.lean @@ -20,6 +20,7 @@ def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init. def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] } def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] } def SyntaxCat.mkSpacePrefixSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixSepBy, args := #[c] } +def SyntaxCat.mkNewlineSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.NewlineSepBy, args := #[c] } def initDialect : Dialect := BuiltinM.create! "Init" #[] do let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident @@ -56,6 +57,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do declareCat q`Init.SpacePrefixSepBy #["a"] + declareCat q`Init.NewlineSepBy #["a"] + let QualifiedIdent := q`Init.QualifiedIdent declareCat QualifiedIdent declareOp { diff --git a/Strata/DDM/Elab.lean b/Strata/DDM/Elab.lean index a14f09015..5c7f97612 100644 --- a/Strata/DDM/Elab.lean +++ b/Strata/DDM/Elab.lean @@ -71,6 +71,11 @@ private partial def runCommand (leanEnv : Lean.Environment) (commands : Array Op return commands let (some tree, true) ← runChecked <| elabCommand leanEnv | return commands + -- Prevent infinite loop if parser makes no progress + let newPos := (←get).pos + if newPos <= iniPos then + logError { start := iniPos, stop := iniPos } "Syntax error: unrecognized syntax or unexpected token" + return commands let cmd := tree.info.asOp!.op let dialects := (← read).loader.dialects modify fun s => { s with diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 1ee5d3b69..30def37a0 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1208,6 +1208,8 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T elabSeqWith c .space "spaceSepBy" (·.getSepArgs) | q`Init.SpacePrefixSepBy => elabSeqWith c .spacePrefix "spacePrefixSepBy" (·.getArgs) + | q`Init.NewlineSepBy => + elabSeqWith c .newline "newlineSepBy" (·.getArgs) | _ => assert! c.args.isEmpty elabOperation diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean index 152db9ef2..c57a9d61d 100644 --- a/Strata/DDM/Format.lean +++ b/Strata/DDM/Format.lean @@ -318,7 +318,7 @@ private def SyntaxDefAtom.formatArgs (opts : FormatOptions) (args : Array PrecFo match stx with | .ident lvl prec _ => let ⟨r, innerPrec⟩ := args[lvl]! - if prec > 0 ∧ (innerPrec ≤ prec ∨ opts.alwaysParen) then + if prec > 0 ∧ (innerPrec < prec ∨ opts.alwaysParen) then f!"({r})" else r @@ -399,6 +399,9 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat | .spacePrefix => .atom <$> entries.foldlM (init := .nil) fun p a => return (p ++ " " ++ (← a.mformatM).format) + | .newline => + .atom <$> entries.foldlM (init := .nil) fun p a => + return (if p.isEmpty then p else p ++ "\n") ++ (← a.mformatM).format private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat := if rargs.isEmpty then diff --git a/Strata/DDM/Integration/Java/Gen.lean b/Strata/DDM/Integration/Java/Gen.lean index f38e65570..b57f424c7 100644 --- a/Strata/DDM/Integration/Java/Gen.lean +++ b/Strata/DDM/Integration/Java/Gen.lean @@ -118,14 +118,14 @@ partial def syntaxCatToJavaType (cat : SyntaxCat) : JavaType := else if abstractCategories.contains cat.name then .simple (abstractJavaName cat.name) else match cat.name with - | ⟨"Init", "Option"⟩ => + | q`Init.Option => match cat.args[0]? with | some inner => .optional (syntaxCatToJavaType inner) | none => panic! "Init.Option requires a type argument" - | ⟨"Init", "Seq"⟩ | ⟨"Init", "CommaSepBy"⟩ => + | q`Init.Seq | q`Init.CommaSepBy | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy => match cat.args[0]? with | some inner => .list (syntaxCatToJavaType inner) - | none => panic! "Init.Seq/CommaSepBy requires a type argument" + | none => panic! "List category requires a type argument" | ⟨"Init", _⟩ => panic! s!"Unknown Init category: {cat.name.name}" | ⟨_, name⟩ => .simple (escapeJavaName (toPascalCase name)) @@ -133,12 +133,23 @@ def argDeclKindToJavaType : ArgDeclKind → JavaType | .type _ => .simple "Expr" | .cat c => syntaxCatToJavaType c +/-- Get Ion separator name for a list category, or none if not a list. -/ +def getSeparator (c : SyntaxCat) : Option String := + match c.name with + | q`Init.Seq => some "seq" + | q`Init.CommaSepBy => some "commaSepList" + | q`Init.NewlineSepBy => some "newlineSepList" + | q`Init.SpaceSepBy => some "spaceSepList" + | q`Init.SpacePrefixSepBy => some "spacePrefixedList" + | _ => none + /-- Extract the QualifiedIdent for categories that need Java interfaces, or none for primitives. -/ partial def syntaxCatToQualifiedName (cat : SyntaxCat) : Option QualifiedIdent := if primitiveCategories.contains cat.name then none else if abstractCategories.contains cat.name then some cat.name else match cat.name with - | ⟨"Init", "Option"⟩ | ⟨"Init", "Seq"⟩ | ⟨"Init", "CommaSepBy"⟩ => + | q`Init.Option | q`Init.Seq | q`Init.CommaSepBy + | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy => cat.args[0]?.bind syntaxCatToQualifiedName | ⟨"Init", _⟩ => none | qid => some qid @@ -179,8 +190,7 @@ structure NameAssignments where /-! ## Code Generation -/ def argDeclToJavaField (decl : ArgDecl) : JavaField := - { name := escapeJavaName decl.ident - type := argDeclKindToJavaType decl.kind } + { name := escapeJavaName decl.ident, type := argDeclKindToJavaType decl.kind } def JavaField.toParam (f : JavaField) : String := s!"{f.type.toJava} {f.name}" @@ -226,8 +236,9 @@ def generateNodeInterface (package : String) (categories : List String) : String def generateStubInterface (package : String) (name : String) : String × String := (s!"{name}.java", s!"package {package};\n\npublic non-sealed interface {name} extends Node \{}\n") -def generateSerializer (package : String) : String := +def generateSerializer (package : String) (separatorMap : String) : String := serializerTemplate.replace templatePackage package + |>.replace "/*SEPARATOR_MAP*/" separatorMap /-- Assign unique Java names to all generated types -/ def assignAllNames (d : Dialect) : NameAssignments := @@ -241,7 +252,7 @@ def assignAllNames (d : Dialect) : NameAssignments := let cats := if cats.contains op.category then cats else cats.push op.category let refs := op.argDecls.toArray.foldl (init := refs) fun refs arg => match arg.kind with - | .type _ => refs.insert ⟨"Init", "Expr"⟩ + | .type _ => refs.insert q`Init.Expr | .cat c => match syntaxCatToQualifiedName c with | some qid => refs.insert qid | none => refs @@ -308,17 +319,30 @@ def opDeclToJavaRecord (dialectName : String) (names : NameAssignments) (op : Op fields := op.argDecls.toArray.map argDeclToJavaField } def generateBuilders (package : String) (dialectName : String) (d : Dialect) (names : NameAssignments) : String := - let method (op : OpDecl) := + let methods (op : OpDecl) := let fields := op.argDecls.toArray.map argDeclToJavaField - let (ps, as) := fields.foldl (init := (#[], #[])) fun (ps, as) f => + let (ps, as, checks) := fields.foldl (init := (#[], #[], #[])) fun (ps, as, checks) f => match f.type with - | .simple "java.math.BigInteger" _ => (ps.push s!"long {f.name}", as.push s!"java.math.BigInteger.valueOf({f.name})") - | .simple "java.math.BigDecimal" _ => (ps.push s!"double {f.name}", as.push s!"java.math.BigDecimal.valueOf({f.name})") - | t => (ps.push s!"{t.toJava} {f.name}", as.push f.name) + | .simple "java.math.BigInteger" _ => + (ps.push s!"long {f.name}", + as.push s!"java.math.BigInteger.valueOf({f.name})", + checks.push s!"if ({f.name} < 0) throw new IllegalArgumentException(\"{f.name} must be non-negative\");") + | .simple "java.math.BigDecimal" _ => (ps.push s!"double {f.name}", as.push s!"java.math.BigDecimal.valueOf({f.name})", checks) + | t => (ps.push s!"{t.toJava} {f.name}", as.push f.name, checks) let methodName := escapeJavaName op.name - s!" public static {names.categories[op.category]!} {methodName}({", ".intercalate ps.toList}) \{ return new {names.operators[(op.category, op.name)]!}(SourceRange.NONE{if as.isEmpty then "" else ", " ++ ", ".intercalate as.toList}); }" - let methods := d.declarations.filterMap fun | .op op => some (method op) | _ => none - s!"package {package};\n\npublic class {dialectName} \{\n{"\n".intercalate methods.toList}\n}\n" + let returnType := names.categories[op.category]! + let recordName := names.operators[(op.category, op.name)]! + let checksStr := if checks.isEmpty then "" else " ".intercalate checks.toList ++ " " + let argsStr := if as.isEmpty then "" else ", " ++ ", ".intercalate as.toList + let paramsStr := ", ".intercalate ps.toList + -- Overload with SourceRange parameter + let srParams := if ps.isEmpty then "SourceRange sourceRange" else s!"SourceRange sourceRange, {paramsStr}" + let withSR := s!" public static {returnType} {methodName}({srParams}) \{ {checksStr}return new {recordName}(sourceRange{argsStr}); }" + -- Convenience overload without SourceRange + let withoutSR := s!" public static {returnType} {methodName}({paramsStr}) \{ {checksStr}return new {recordName}(SourceRange.NONE{argsStr}); }" + s!"{withSR}\n{withoutSR}" + let allMethods := d.declarations.filterMap fun | .op op => some (methods op) | _ => none + s!"package {package};\n\npublic class {dialectName} \{\n{"\n\n".intercalate allMethods.toList}\n}\n" public def generateDialect (d : Dialect) (package : String) : Except String GeneratedFiles := do let names := assignAllNames d @@ -354,13 +378,32 @@ public def generateDialect (d : Dialect) (package : String) : Except String Gene sealedInterfaces ++ stubInterfaces |>.map (·.1.dropEnd 5 |>.toString) + -- Generate separator map for list fields + let separatorEntries := d.declarations.toList.filterMap fun decl => + match decl with + | .op op => + let opName := s!"{d.name}.{op.name}" + let fieldEntries := op.argDecls.toArray.toList.filterMap fun arg => + match arg.kind with + | .cat c => match getSeparator c with + | some sep => some s!"\"{escapeJavaName arg.ident}\", \"{sep}\"" + | none => none + | _ => none + if fieldEntries.isEmpty then none + else + let inner := fieldEntries.map fun e => s!"java.util.Map.entry({e})" + some s!" java.util.Map.entry(\"{opName}\", java.util.Map.ofEntries({", ".intercalate inner}))" + | _ => none + let separatorMap := if separatorEntries.isEmpty then "java.util.Map.of()" + else s!"java.util.Map.ofEntries(\n{",\n".intercalate separatorEntries})" + return { sourceRange := generateSourceRange package node := generateNodeInterface package allInterfaceNames interfaces := sealedInterfaces.toArray ++ stubInterfaces.toArray records := records.toArray builders := (s!"{names.builders}.java", generateBuilders package names.builders d names) - serializer := generateSerializer package + serializer := generateSerializer package separatorMap } /-! ## File Output -/ diff --git a/Strata/DDM/Integration/Java/templates/IonSerializer.java b/Strata/DDM/Integration/Java/templates/IonSerializer.java index 2a0157fca..ae1d51221 100644 --- a/Strata/DDM/Integration/Java/templates/IonSerializer.java +++ b/Strata/DDM/Integration/Java/templates/IonSerializer.java @@ -6,6 +6,8 @@ public class IonSerializer { private final IonSystem ion; + private static final java.util.Map> SEPARATORS = /*SEPARATOR_MAP*/; + public IonSerializer(IonSystem ion) { this.ion = ion; } @@ -22,14 +24,17 @@ public IonValue serialize(Node node) { private IonSexp serializeNode(Node node) { IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol(node.operationName())); + String opName = node.operationName(); + sexp.add(ion.newSymbol(opName)); sexp.add(serializeSourceRange(node.sourceRange())); + var fieldSeps = SEPARATORS.getOrDefault(opName, java.util.Map.of()); for (var component : node.getClass().getRecordComponents()) { if (component.getName().equals("sourceRange")) continue; try { java.lang.Object value = component.getAccessor().invoke(node); - sexp.add(serializeArg(value, component.getType(), component.getGenericType())); + String sep = fieldSeps.get(component.getName()); + sexp.add(serializeArg(value, sep, component.getType())); } catch (java.lang.Exception e) { throw new java.lang.RuntimeException("Failed to serialize " + component.getName(), e); } @@ -54,7 +59,7 @@ private IonValue serializeSourceRange(SourceRange sr) { return sexp; } - private IonValue serializeArg(java.lang.Object value, java.lang.Class type, java.lang.reflect.Type genericType) { + private IonValue serializeArg(java.lang.Object value, String sep, java.lang.Class type) { if (value == null) { return serializeOption(java.util.Optional.empty()); } @@ -80,7 +85,7 @@ private IonValue serializeArg(java.lang.Object value, java.lang.Class type, j return serializeOption(opt); } if (value instanceof java.util.List list) { - return serializeSeq(list, genericType); + return serializeSeq(list, sep != null ? sep : "seq"); } throw new java.lang.IllegalArgumentException("Unsupported type: " + type); } @@ -129,17 +134,17 @@ private IonValue serializeOption(java.util.Optional opt) { sexp.add(ion.newSymbol("option")); sexp.add(ion.newNull()); if (opt.isPresent()) { - sexp.add(serializeArg(opt.get(), opt.get().getClass(), opt.get().getClass())); + sexp.add(serializeArg(opt.get(), null, opt.get().getClass())); } return sexp; } - private IonValue serializeSeq(java.util.List list, java.lang.reflect.Type genericType) { + private IonValue serializeSeq(java.util.List list, String sepType) { IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol("seq")); + sexp.add(ion.newSymbol(sepType)); sexp.add(ion.newNull()); for (java.lang.Object item : list) { - sexp.add(serializeArg(item, item.getClass(), item.getClass())); + sexp.add(serializeArg(item, null, item.getClass())); } return sexp; } diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index 56fc9fa42..3c8e2d71e 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -666,6 +666,9 @@ partial def genCatTypeTerm (annType : Ident) (c : SyntaxCat) | q`Init.SpacePrefixSepBy, 1 => let inner := mkCApp ``Array #[args[0]] return if addAnn then mkCApp ``Ann #[inner, annType] else inner + | q`Init.NewlineSepBy, 1 => + let inner := mkCApp ``Array #[args[0]] + return if addAnn then mkCApp ``Ann #[inner, annType] else inner | q`Init.Option, 1 => let inner := mkCApp ``Option #[args[0]] return if addAnn then mkCApp ``Ann #[inner, annType] else inner @@ -869,6 +872,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) toAstApplyArgSeq v cat ``SepFormat.space | q`Init.SpacePrefixSepBy => do toAstApplyArgSeq v cat ``SepFormat.spacePrefix + | q`Init.NewlineSepBy => do + toAstApplyArgSeq v cat ``SepFormat.newline | q`Init.Seq => do toAstApplyArgSeq v cat ``SepFormat.none | q`Init.Option => do @@ -1101,6 +1106,8 @@ partial def genOfAstArgTerm (varName : String) (cat : SyntaxCat) genOfAstSeqArgTerm varName cat e ``SepFormat.space | q`Init.SpacePrefixSepBy => do genOfAstSeqArgTerm varName cat e ``SepFormat.spacePrefix + | q`Init.NewlineSepBy => do + genOfAstSeqArgTerm varName cat e ``SepFormat.newline | q`Init.Seq => do genOfAstSeqArgTerm varName cat e ``SepFormat.none | q`Init.Option => do @@ -1396,6 +1403,7 @@ def tryMakeInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor) | q`Init.CommaSepBy => true | q`Init.SpaceSepBy => true | q`Init.SpacePrefixSepBy => true + | q`Init.NewlineSepBy => true | q`Init.Option => true | c => c ∈ inhabited if !argsInhabited then diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index d86c3c09b..e44267402 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -40,6 +40,7 @@ instance : ToExpr SepFormat where | .comma => mkConst ``SepFormat.comma | .space => mkConst ``SepFormat.space | .spacePrefix => mkConst ``SepFormat.spacePrefix + | .newline => mkConst ``SepFormat.newline end SepFormat diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean index 3449f7dd6..ea22dcf44 100644 --- a/Strata/DDM/Parser.lean +++ b/Strata/DDM/Parser.lean @@ -228,16 +228,19 @@ private partial def whitespace : ParserFn := fun c s => let curr := c.get j match curr with | '/' => + -- Treat as comment unless a token starting with "//" exists (e.g., //@pre) match c.tokens.matchPrefix c.inputString i with - | some _ => s + | some tk => if tk.startsWith "//" then s + else andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j) | none => andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j) | '*' => + -- Treat as comment unless a token starting with "/*" exists match c.tokens.matchPrefix c.inputString i with - | some _ => s + | some tk => if tk.startsWith "/*" then s + else andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j)) | none => - let j := c.next j - andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c j) + andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j)) | _ => s else s @@ -897,7 +900,7 @@ partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metad assert! cat.args.size = 1 let isNonempty := q`StrataDDL.nonempty ∈ metadata commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]! - | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.Seq => + | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.NewlineSepBy | q`Init.Seq => assert! cat.args.size = 1 let isNonempty := q`StrataDDL.nonempty ∈ metadata (if isNonempty then many1Parser else manyParser) <$> catParser ctx cat.args[0]! diff --git a/Strata/DL/Lambda/LExprEval.lean b/Strata/DL/Lambda/LExprEval.lean index 6fa05b0bd..cb383801e 100644 --- a/Strata/DL/Lambda/LExprEval.lean +++ b/Strata/DL/Lambda/LExprEval.lean @@ -181,7 +181,7 @@ def eval (n : Nat) (σ : LState TBase) (e : (LExpr TBase.mono)) -- At least one argument in the function call is symbolic. new_e | none => - -- Not a call of a factory function. + -- Not a call of a factory function - go through evalCore evalCore n' σ e def evalCore (n' : Nat) (σ : LState TBase) (e : LExpr TBase.mono) : LExpr TBase.mono := diff --git a/Strata/DL/Lambda/LExprWF.lean b/Strata/DL/Lambda/LExprWF.lean index 5b3f70c8a..7b9b17505 100644 --- a/Strata/DL/Lambda/LExprWF.lean +++ b/Strata/DL/Lambda/LExprWF.lean @@ -290,11 +290,24 @@ theorem varOpen_of_varClose {T} {GenericTy} [BEq T.Metadata] [LawfulBEq T.Metada /-! ### Substitution on `LExpr`s -/ /-- -Substitute `(.fvar x _)` in `e` with `s`. Note that unlike `substK`, `varClose`, -and `varOpen`, this function is agnostic of types. +Increment bound variable indices in `e` by `n`. Only bvars at or above `cutoff` +are shifted; bvars below `cutoff` (bound within `e`) are left alone. The cutoff +increases when going under binders. +-/ +def liftBVars (n : Nat) (e : LExpr ⟨T, GenericTy⟩) (cutoff : Nat := 0) : LExpr ⟨T, GenericTy⟩ := + match e with + | .const _ _ => e | .op _ _ _ => e | .fvar _ _ _ => e + | .bvar m i => if i >= cutoff then .bvar m (i + n) else e + | .abs m ty e' => .abs m ty (liftBVars n e' (cutoff + 1)) + | .quant m qk ty tr' e' => .quant m qk ty (liftBVars n tr' (cutoff + 1)) (liftBVars n e' (cutoff + 1)) + | .app m fn e' => .app m (liftBVars n fn cutoff) (liftBVars n e' cutoff) + | .ite m c t e' => .ite m (liftBVars n c cutoff) (liftBVars n t cutoff) (liftBVars n e' cutoff) + | .eq m e1 e2 => .eq m (liftBVars n e1 cutoff) (liftBVars n e2 cutoff) -Also see function `subst`, where `subst s e` substitutes the outermost _bound_ -variable in `e` with `s`. +/-- +Substitute `(.fvar x _)` in `e` with `to`. Does NOT lift de Bruijn indices in `to` +when going under binders - safe when `to` contains no bvars (e.g., substituting +fvar→fvar). Use `substFvarLifting` when `to` contains bvars. -/ def substFvar [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (fr : T.Identifier) (to : LExpr ⟨T, GenericTy⟩) : (LExpr ⟨T, GenericTy⟩) := @@ -307,6 +320,28 @@ def substFvar [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (fr : T.Identifier) | .ite m c t e' => .ite m (substFvar c fr to) (substFvar t fr to) (substFvar e' fr to) | .eq m e1 e2 => .eq m (substFvar e1 fr to) (substFvar e2 fr to) +/-- +Like `substFvar`, but properly lifts de Bruijn indices in `to` when going under +binders. Use this when `to` contains bound variables that should be preserved. +-/ +def substFvarLifting [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (fr : T.Identifier) (to : LExpr ⟨T, GenericTy⟩) + : (LExpr ⟨T, GenericTy⟩) := + go e 0 +where + go (e : LExpr ⟨T, GenericTy⟩) (depth : Nat) : LExpr ⟨T, GenericTy⟩ := + match e with + | .const _ _ => e | .bvar _ _ => e | .op _ _ _ => e + | .fvar _ name _ => if name == fr then liftBVars depth to else e + | .abs m ty e' => .abs m ty (go e' (depth + 1)) + | .quant m qk ty tr' e' => .quant m qk ty (go tr' (depth + 1)) (go e' (depth + 1)) + | .app m fn e' => .app m (go fn depth) (go e' depth) + | .ite m c t f => .ite m (go c depth) (go t depth) (go f depth) + | .eq m e1 e2 => .eq m (go e1 depth) (go e2 depth) + +def substFvarsLifting [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (sm : Map T.Identifier (LExpr ⟨T, GenericTy⟩)) + : LExpr ⟨T, GenericTy⟩ := + List.foldl (fun e (var, s) => substFvarLifting e var s) e sm + def substFvars [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (sm : Map T.Identifier (LExpr ⟨T, GenericTy⟩)) : LExpr ⟨T, GenericTy⟩ := List.foldl (fun e (var, s) => substFvar e var s) e sm diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/DL/SMT/Encoder.lean index e2fdae45b..079ff39f7 100644 --- a/Strata/DL/SMT/Encoder.lean +++ b/Strata/DL/SMT/Encoder.lean @@ -89,6 +89,10 @@ def encodeType (ty : TermType) : EncoderM String := do | .trigger => return "Trigger" | .bitvec n => return s!"(_ BitVec {n})" | .option oty => return s!"(Option {← encodeType oty})" + | .constr "Map" [k, v] => + let k' ← encodeType k + let v' ← encodeType v + return s!"(Array {k'} {v'})" | .constr id targs => -- let targs' ← targs.mapM (fun t => encodeType t) let targs' ← go targs diff --git a/Strata/Languages/C_Simp/DDMTransform/Parse.lean b/Strata/Languages/C_Simp/DDMTransform/Parse.lean index 4cce404c3..7763c18b1 100644 --- a/Strata/Languages/C_Simp/DDMTransform/Parse.lean +++ b/Strata/Languages/C_Simp/DDMTransform/Parse.lean @@ -45,40 +45,40 @@ op monoDeclPush (dl : MonoDeclList, @[scope(dl)] b : MonoBind) : MonoDeclList => fn btrue : bool => "true"; fn bfalse : bool => "false"; -fn eq (tp : Type, x : tp, y : tp) : bool => x "==" y; +fn eq (tp : Type, x : tp, y : tp) : bool => x " == " y; -fn lt (x : int, y : int) : bool => x "<" y; -fn le (x : int, y : int) : bool => x "<=" y; -fn gt (x : int, y : int) : bool => x ">" y; -fn ge (x : int, y : int) : bool => x ">=" y; +fn lt (x : int, y : int) : bool => x " < " y; +fn le (x : int, y : int) : bool => x " <= " y; +fn gt (x : int, y : int) : bool => x " > " y; +fn ge (x : int, y : int) : bool => x " >= " y; -fn add (x : int, y : int) : int => x "+" y; -fn sub (x : int, y : int) : int => x "-" y; -fn mul (x : int, y : int) : int => x "*" y; -fn div (x : int, y : int) : int => x "/" y; -fn mod (x : int, y : int) : int => x "%" y; +fn add (x : int, y : int) : int => x " + " y; +fn sub (x : int, y : int) : int => x " - " y; +fn mul (x : int, y : int) : int => x " * " y; +fn div (x : int, y : int) : int => x " / " y; +fn mod (x : int, y : int) : int => x " % " y; fn not (x : bool) : bool => "!" x; -fn and (x : bool, y : bool) : bool => x "&&" y; -fn or (x : bool, y : bool) : bool => x "||" y; +fn and (x : bool, y : bool) : bool => x " && " y; +fn or (x : bool, y : bool) : bool => x " || " y; fn to_int (n : Num) : int => n; fn len (a : intArr) : int => "len(" a ")"; -fn get (a : intArr, i: int) : int => "get(" a "," i ")"; +fn get (a : intArr, i: int) : int => "get(" a ", " i ")"; category Statement; category Block; -op block (stmts : Seq Statement) : Block => "{\n" stmts "}\n"; +op block (stmts : NewlineSepBy Statement) : Block => "{" indent(2, "\n" stmts) "\n}"; @[declare(v, tp)] -op init_decl (v : Ident, tp : Type) : Statement => "var" v ":" tp ";\n"; +op init_decl (v : Ident, tp : Type) : Statement => "var " v ":" tp ";"; category Else; -op if_command (c : bool, t : Block, f : Else) : Statement => "if" "(" c ")" t f; -op else1 (f : Block) : Else => "else" f; +op if_command (c : bool, t : Block, f : Else) : Statement => "if" " (" c ") " t f; +op else1 (f : Block) : Else => " else " f; op else0 () : Else =>; category Binding; @@ -90,18 +90,18 @@ category Bindings; op mkBindings (bindings : CommaSepBy Binding) : Bindings => "(" bindings ")"; category MeasureCat; -op measure (e : int) : MeasureCat => "//@decreases" e; +op measure (e : int) : MeasureCat => "//@decreases " e; category InvariantCat; -op invariant (e : bool) : InvariantCat => "//@invariant" e; +op invariant (e : bool) : InvariantCat => "//@invariant " e; op while_command (g : bool, measure: Option MeasureCat, invariant: Option InvariantCat, - b : Block) : Statement => "while" "(" g ")\n" measure invariant b; + b : Block) : Statement => "while" " (" g ")" "\n" measure "\n" invariant "\n" b; -op assign (tp : Type, v : Ident, val : tp) : Statement => v "=" val ";\n"; -op return (tp: Type, e : tp) : Statement => "return" e ";\n"; +op assign (tp : Type, v : Ident, val : tp) : Statement => v " = " val ";"; +op return (tp: Type, e : tp) : Statement => "return " e ";"; op procedure (retType: Type, typeArgs: Option TypeArgs, @@ -110,13 +110,13 @@ op procedure (retType: Type, @[scope(b)] pre: bool, @[scope(b)] post: bool, @[scope(b)] body : Block) : Command => retType " procedure " name typeArgs b - "//@pre" indent(2, pre) ";\n" - "//@post" indent(2, post) ";\n" - indent(2, body); + indent(2, "\n//@pre " pre ";" + "\n//@post " post ";\n") + body; category Annotation; -op assert (lbl : Ident, c: bool) : Annotation => "//@assert [" lbl "]" c";\n"; -op assume (lbl : Ident, c: bool) : Annotation => "//@assume [" lbl "]" c";\n"; +op assert (lbl : Ident, c: bool) : Annotation => "//@assert [" lbl "] " c ";"; +op assume (lbl : Ident, c: bool) : Annotation => "//@assume [" lbl "] " c ";"; op annotation (a : Annotation) : Statement => a; #end @@ -144,3 +144,4 @@ int procedure simpleTest (x: int, y: int) } #end +-- #end diff --git a/Strata/Languages/C_Simp/DDMTransform/Translate.lean b/Strata/Languages/C_Simp/DDMTransform/Translate.lean index cda87b23e..ef47bf663 100644 --- a/Strata/Languages/C_Simp/DDMTransform/Translate.lean +++ b/Strata/Languages/C_Simp/DDMTransform/Translate.lean @@ -413,7 +413,7 @@ partial def translateStmt (bindings : TransBindings) (arg : Arg) : partial def translateBlock (bindings : TransBindings) (arg : Arg) : TransM (List Statement) := do let args ← checkOpArg arg q`C_Simp.block 1 - let .seq _ .none stmts := args[0]! + let .seq _ _ stmts := args[0]! | TransM.error s!"Invalid block {repr args[0]!}" let (a, _) ← stmts.foldlM (init := (#[], bindings)) fun (a, b) s => do let (s, b) ← translateStmt b s diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean index 0ca42f8ae..78f74b8e5 100644 --- a/Strata/Languages/C_Simp/Verify.lean +++ b/Strata/Languages/C_Simp/Verify.lean @@ -106,8 +106,8 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := -- C_Simp functions are Strata Core procedures def loop_elimination_function(f : C_Simp.Function) : Core.Procedure := - let core_preconditions := [("pre", {expr := translate_expr f.pre })] - let core_postconditions := [("post", {expr := translate_expr f.post })] + let core_preconditions := [("pre", {expr := translate_expr f.pre, md := .empty })] + let core_postconditions := [("post", {expr := translate_expr f.post, md := .empty })] {header := {name := f.name.name, typeArgs := [], inputs := f.inputs.map (λ p => (p.fst.name, p.snd)), outputs := [("return", f.ret_ty)]}, diff --git a/Strata/Languages/Core/DDMTransform/Parse.lean b/Strata/Languages/Core/DDMTransform/Parse.lean index 5b192686d..e0e517130 100644 --- a/Strata/Languages/Core/DDMTransform/Parse.lean +++ b/Strata/Languages/Core/DDMTransform/Parse.lean @@ -55,7 +55,7 @@ category DeclList; @[scope(b)] op declAtom (b : Bind) : DeclList => b; @[scope(b)] -op declPush (dl : DeclList, @[scope(dl)] b : Bind) : DeclList => dl "," b; +op declPush (dl : DeclList, @[scope(dl)] b : Bind) : DeclList => dl ", " b; category MonoBind; @[declare(v, tp)] @@ -67,7 +67,7 @@ category MonoDeclList; op monoDeclAtom (b : MonoBind) : MonoDeclList => b; @[scope(b)] op monoDeclPush (dl : MonoDeclList, @[scope(dl)] b : MonoBind) : MonoDeclList => - dl "," b; + dl ", " b; fn not (b : bool) : bool => "!" b; @@ -166,15 +166,15 @@ op triggersPush (triggers : Triggers, group : TriggerGroup) : Triggers => // Quantifiers without triggers fn forall (d : DeclList, @[scope(d)] b : bool) : bool => - "forall" d "::" b:3; + "forall " d "::" b:3; fn exists (d : DeclList, @[scope(d)] b : bool) : bool => - "exists" d "::" b:3; + "exists " d "::" b:3; // Quantifiers with triggers fn forallT (d : DeclList, @[scope(d)] triggers : Triggers, @[scope(d)] b : bool) : bool => - "forall" d "::" triggers b:3; + "forall " d "::" triggers b:3; fn existsT (d : DeclList, @[scope(d)] triggers : Triggers, @[scope(d)] b : bool) : bool => - "exists" d "::" triggers b:3; + "exists " d "::" triggers b:3; category Lhs; op lhsIdent (v : Ident) : Lhs => v; @@ -185,7 +185,7 @@ category Block; category Else; category Label; -op label (l : Ident) : Label => "[" l "]:"; +op label (l : Ident) : Label => "[" l "]: "; @[scope(dl)] op varStatement (dl : DeclList) : Statement => "var " dl ";\n"; diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean index 598af6a2f..22957df04 100644 --- a/Strata/Languages/Core/Env.lean +++ b/Strata/Languages/Core/Env.lean @@ -257,7 +257,7 @@ def Env.genFVar (E : Env) (xt : (Lambda.IdentT Lambda.LMonoTy Visibility)) : let (xid, E) := E.genVar xt.ident let xe := match xt.ty? with | none => .fvar () xid none - | some xty => .fvar () xid xty + | some xty => .fvar () xid (some xty) (xe, E) /-- diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index f84aa1b4d..1b405d72d 100644 --- a/Strata/Languages/Core/Procedure.lean +++ b/Strata/Languages/Core/Procedure.lean @@ -79,11 +79,11 @@ instance : Std.ToFormat Procedure.CheckAttr where structure Procedure.Check where expr : Expression.Expr attr : CheckAttr := .Default - md : Imperative.MetaData Expression := #[] + md : Imperative.MetaData Expression deriving Repr, DecidableEq instance : Inhabited Procedure.Check where - default := { expr := Inhabited.default } + default := { expr := Inhabited.default, md := #[] } instance : ToFormat Procedure.Check where format c := f!"{c.expr}{c.attr}" diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean index d71e8347b..2ddab4d5c 100644 --- a/Strata/Languages/Core/SMTEncoder.lean +++ b/Strata/Languages/Core/SMTEncoder.lean @@ -93,6 +93,7 @@ private def lMonoTyToSMTString (ty : LMonoTy) : String := | .tcons "real" [] => "Real" | .tcons "string" [] => "String" | .tcons "regex" [] => "RegLan" + | .tcons "Map" [k, v] => s!"(Array {lMonoTyToSMTString k} {lMonoTyToSMTString v})" | .tcons name args => if args.isEmpty then name else s!"({name} {String.intercalate " " (args.map lMonoTyToSMTString)})" @@ -295,13 +296,21 @@ partial def appToSMTTerm (E : Env) (bvs : BoundVars) (e : LExpr CoreLParams.mono let (op, retty, ctx) ← toSMTOp E fn fnty ctx let (e1t, ctx) ← toSMTTerm E bvs e1 ctx .ok (op (e1t :: acc) retty, ctx) - | .app _ (.fvar _ fn (.some (.arrow intty outty))) e1 => do + | .app _ (.fvar _ fn (.some fnty)) e1 => do + let tys := LMonoTy.destructArrow fnty + let outty := tys.getLast (by exact @LMonoTy.destructArrow_non_empty fnty) + let intys := tys.take (tys.length - 1) let (smt_outty, ctx) ← LMonoTy.toSMTType E outty ctx - let (smt_intty, ctx) ← LMonoTy.toSMTType E intty ctx - let argvars := [TermVar.mk (toString $ format intty) smt_intty] let (e1t, ctx) ← toSMTTerm E bvs e1 ctx + let allArgs := e1t :: acc + let mut argvars : List TermVar := [] + let mut ctx := ctx + for inty in intys do + let (smt_inty, ctx') ← LMonoTy.toSMTType E inty ctx + ctx := ctx' + argvars := argvars ++ [TermVar.mk (toString $ format inty) smt_inty] let uf := UF.mk (id := (toString $ format fn)) (args := argvars) (out := smt_outty) - .ok (((Term.app (.uf uf) [e1t] smt_outty)), ctx) + .ok (Term.app (.uf uf) allArgs smt_outty, ctx) | .app _ _ _ => .error f!"Cannot encode expression {e}" @@ -525,9 +534,9 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte | none => .ok (ctx.addUF uf, !ctx.ufs.contains uf) | some body => -- Substitute the formals in the function body with appropriate - -- `.bvar`s. + -- `.bvar`s. Use substFvarsLifting to properly lift indices under binders. let bvars := (List.range formals.length).map (fun i => LExpr.bvar () i) - let body := LExpr.substFvars body (formals.zip bvars) + let body := LExpr.substFvarsLifting body (formals.zip bvars) let (term, ctx) ← toSMTTerm E bvs body ctx .ok (ctx.addIF uf term, !ctx.ifs.contains ({ uf := uf, body := term })) if isNew then diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 0f6a444ed..a2ed63aba 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -75,19 +75,29 @@ instance : Inhabited HighType where default := .TVoid instance : Inhabited Parameter where - default := { name := "", type := .TVoid } + default := { name := "", type := ⟨.TVoid, #[]⟩ } -def translateHighType (arg : Arg) : TransM HighType := do +/-- Create a HighTypeMd with the given metadata -/ +def mkHighTypeMd (t : HighType) (md : MetaData Core.Expression) : HighTypeMd := ⟨t, md⟩ + +/-- Create a StmtExprMd with the given metadata -/ +def mkStmtExprMd (e : StmtExpr) (md : MetaData Core.Expression) : StmtExprMd := ⟨e, md⟩ + +partial def translateHighType (arg : Arg) : TransM HighTypeMd := do + let md ← getArgMetaData arg match arg with | .op op => match op.name, op.args with - | q`Laurel.intType, _ => return .TInt - | q`Laurel.boolType, _ => return .TBool - | q`Laurel.stringType, _ => return .TString + | q`Laurel.intType, _ => return mkHighTypeMd .TInt md + | q`Laurel.boolType, _ => return mkHighTypeMd .TBool md + | q`Laurel.stringType, _ => return mkHighTypeMd .TString md + | q`Laurel.arrayType, #[elemArg] => + let elemType ← translateHighType elemArg + return mkHighTypeMd (.Applied (mkHighTypeMd (.UserDefined "Array") md) [elemType]) md | q`Laurel.compositeType, #[nameArg] => let name ← translateIdent nameArg - return .UserDefined name - | _, _ => TransM.error s!"translateHighType expects intType, boolType, stringType or compositeType, got {repr op.name}" + return mkHighTypeMd (.UserDefined name) md + | _, _ => TransM.error s!"translateHighType expects intType, boolType, stringType, arrayType or compositeType, got {repr op.name}" | _ => TransM.error s!"translateHighType expects operation" def translateNat (arg : Arg) : TransM Nat := do @@ -124,15 +134,20 @@ instance : Inhabited Procedure where name := "" inputs := [] outputs := [] - precondition := .LiteralBool true - determinism := .nondeterministic + preconditions := [] decreases := none - body := .Transparent (.LiteralBool true) + body := .Transparent ⟨.LiteralBool true, #[]⟩ } def getBinaryOp? (name : QualifiedIdent) : Option Operation := match name with | q`Laurel.add => some Operation.Add + | q`Laurel.sub => some Operation.Sub + | q`Laurel.mul => some Operation.Mul + | q`Laurel.div => some Operation.Div + | q`Laurel.mod => some Operation.Mod + | q`Laurel.divT => some Operation.DivT + | q`Laurel.modT => some Operation.ModT | q`Laurel.eq => some Operation.Eq | q`Laurel.neq => some Operation.Neq | q`Laurel.gt => some Operation.Gt @@ -141,31 +156,37 @@ def getBinaryOp? (name : QualifiedIdent) : Option Operation := | q`Laurel.ge => some Operation.Geq | q`Laurel.and => some Operation.And | q`Laurel.or => some Operation.Or + | q`Laurel.implies => some Operation.Implies + | _ => none + +def getUnaryOp? (name : QualifiedIdent) : Option Operation := + match name with + | q`Laurel.not => some Operation.Not + | q`Laurel.neg => some Operation.Neg | _ => none mutual -partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do +partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do + let md ← getArgMetaData arg match arg with | .op op => match op.name, op.args with | q`Laurel.assert, #[arg0] => let cond ← translateStmtExpr arg0 - let md ← getArgMetaData (.op op) - return .Assert cond md + return mkStmtExprMd (.Assert cond) md | q`Laurel.assume, #[arg0] => let cond ← translateStmtExpr arg0 - let md ← getArgMetaData (.op op) - return .Assume cond md + return mkStmtExprMd (.Assume cond) md | q`Laurel.block, #[arg0] => let stmts ← translateSeqCommand arg0 - return .Block stmts none - | q`Laurel.literalBool, #[arg0] => return .LiteralBool (← translateBool arg0) + return mkStmtExprMd (.Block stmts none) md + | q`Laurel.literalBool, #[arg0] => return mkStmtExprMd (.LiteralBool (← translateBool arg0)) md | q`Laurel.int, #[arg0] => let n ← translateNat arg0 - return .LiteralInt n + return mkStmtExprMd (.LiteralInt n) md | q`Laurel.string, #[arg0] => let s ← translateString arg0 - return .LiteralString s + return mkStmtExprMd (.LiteralString s) md | q`Laurel.varDecl, #[arg0, typeArg, assignArg] => let name ← translateIdent arg0 let varType ← match typeArg with @@ -179,28 +200,27 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}" | .option _ none => pure none | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}" - return .LocalVariable name varType value + return mkStmtExprMd (.LocalVariable name varType value) md | q`Laurel.identifier, #[arg0] => let name ← translateIdent arg0 - return .Identifier name + return mkStmtExprMd (.Identifier name) md | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0 | q`Laurel.assign, #[arg0, arg1] => let target ← translateStmtExpr arg0 let value ← translateStmtExpr arg1 - let md ← getArgMetaData (.op op) - return .Assign [target] value md + return mkStmtExprMd (.Assign [target] value) md | q`Laurel.call, #[arg0, argsSeq] => let callee ← translateStmtExpr arg0 - let calleeName := match callee with + let calleeName := match callee.val with | .Identifier name => name | _ => "" let argsList ← match argsSeq with | .seq _ .comma args => args.toList.mapM translateStmtExpr | _ => pure [] - return .StaticCall calleeName argsList + return mkStmtExprMd (.StaticCall calleeName argsList) md | q`Laurel.return, #[arg0] => let value ← translateStmtExpr arg0 - return .Return (some value) + return mkStmtExprMd (.Return (some value)) md | q`Laurel.ifThenElse, #[arg0, arg1, elseArg] => let cond ← translateStmtExpr arg0 let thenBranch ← translateStmtExpr arg1 @@ -209,30 +229,62 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do | q`Laurel.optionalElse, #[elseArg0] => translateStmtExpr elseArg0 >>= (pure ∘ some) | _, _ => pure none | _ => pure none - return .IfThenElse cond thenBranch elseBranch + return mkStmtExprMd (.IfThenElse cond thenBranch elseBranch) md | q`Laurel.fieldAccess, #[objArg, fieldArg] => let obj ← translateStmtExpr objArg let field ← translateIdent fieldArg - return .FieldSelect obj field + return mkStmtExprMd (.FieldSelect obj field) md + | q`Laurel.arrayIndex, #[arrArg, idxArg] => + let arr ← translateStmtExpr arrArg + let idx ← translateStmtExpr idxArg + return mkStmtExprMd (.StaticCall "Array.Get" [arr, idx]) md + | q`Laurel.while, #[condArg, invSeqArg, bodyArg] => + let cond ← translateStmtExpr condArg + let invariants ← match invSeqArg with + | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with + | .op invOp => match invOp.name, invOp.args with + | q`Laurel.invariantClause, #[exprArg] => translateStmtExpr exprArg + | _, _ => TransM.error "Expected invariantClause" + | _ => TransM.error "Expected operation" + | _ => pure [] + let body ← translateStmtExpr bodyArg + return mkStmtExprMd (.While cond invariants none body) md + | _, #[arg0] => match getUnaryOp? op.name with + | some primOp => + let inner ← translateStmtExpr arg0 + return mkStmtExprMd (.PrimitiveOp primOp [inner]) md + | none => TransM.error s!"Unknown unary operation: {op.name}" + | q`Laurel.forallExpr, #[nameArg, tyArg, bodyArg] => + let name ← translateIdent nameArg + let ty ← translateHighType tyArg + let body ← translateStmtExpr bodyArg + return mkStmtExprMd (.Forall name ty body) md + | q`Laurel.existsExpr, #[nameArg, tyArg, bodyArg] => + let name ← translateIdent nameArg + let ty ← translateHighType tyArg + let body ← translateStmtExpr bodyArg + return mkStmtExprMd (.Exists name ty body) md | _, #[arg0, arg1] => match getBinaryOp? op.name with | some primOp => let lhs ← translateStmtExpr arg0 let rhs ← translateStmtExpr arg1 - return .PrimitiveOp primOp [lhs, rhs] + return mkStmtExprMd (.PrimitiveOp primOp [lhs, rhs]) md | none => TransM.error s!"Unknown operation: {op.name}" | _, _ => TransM.error s!"Unknown operation: {op.name}" | _ => TransM.error s!"translateStmtExpr expects operation" -partial def translateSeqCommand (arg : Arg) : TransM (List StmtExpr) := do - let .seq _ .none args := arg - | TransM.error s!"translateSeqCommand expects seq" - let mut stmts : List StmtExpr := [] +partial def translateSeqCommand (arg : Arg) : TransM (List StmtExprMd) := do + let args ← match arg with + | .seq _ .none args => pure args + | .seq _ .newline args => pure args -- NewlineSepBy for block statements + | _ => TransM.error s!"translateSeqCommand expects seq or newlineSepBy" + let mut stmts : List StmtExprMd := [] for arg in args do let stmt ← translateStmtExpr arg stmts := stmts ++ [stmt] return stmts -partial def translateCommand (arg : Arg) : TransM StmtExpr := do +partial def translateCommand (arg : Arg) : TransM StmtExprMd := do translateStmtExpr arg end @@ -263,31 +315,32 @@ def parseProcedure (arg : Arg) : TransM Procedure := do | .option _ none => pure [] | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}" | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}" - -- Parse precondition (requires clause) - let precondition ← match requiresArg with - | .option _ (some (.op requiresOp)) => match requiresOp.name, requiresOp.args with - | q`Laurel.optionalRequires, #[exprArg] => translateStmtExpr exprArg - | _, _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresOp.name}" - | .option _ none => pure (.LiteralBool true) - | _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresArg}" - -- Parse postcondition (ensures clause) - let postcondition ← match ensuresArg with - | .option _ (some (.op ensuresOp)) => match ensuresOp.name, ensuresOp.args with - | q`Laurel.optionalEnsures, #[exprArg] => translateStmtExpr exprArg >>= (pure ∘ some) - | _, _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresOp.name}" - | .option _ none => pure none - | _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresArg}" + -- Parse preconditions (requires clauses) + let preconditions ← match requiresArg with + | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with + | .op reqOp => match reqOp.name, reqOp.args with + | q`Laurel.requiresClause, #[exprArg] => translateStmtExpr exprArg + | _, _ => TransM.error "Expected requiresClause" + | _ => TransM.error "Expected operation" + | _ => pure [] + -- Parse postconditions (ensures clauses) + let postconditions ← match ensuresArg with + | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with + | .op ensOp => match ensOp.name, ensOp.args with + | q`Laurel.ensuresClause, #[exprArg] => translateStmtExpr exprArg + | _, _ => TransM.error "Expected ensuresClause" + | _ => TransM.error "Expected operation" + | _ => pure [] let body ← translateCommand bodyArg - -- If there's a postcondition, use Opaque body; otherwise use Transparent - let procBody := match postcondition with - | some post => Body.Opaque post (some body) none - | none => Body.Transparent body + -- If there are postconditions, use Opaque body; otherwise use Transparent + let procBody := match postconditions with + | [] => Body.Transparent body + | posts => Body.Opaque posts (some body) none return { name := name inputs := parameters outputs := returnParameters - precondition := precondition - determinism := .nondeterministic + preconditions := preconditions decreases := none body := procBody } @@ -296,6 +349,20 @@ def parseProcedure (arg : Arg) : TransM Procedure := do | _, _ => TransM.error s!"parseProcedure expects procedure, got {repr op.name}" +def parseConstrainedType (arg : Arg) : TransM ConstrainedType := do + let .op op := arg + | TransM.error s!"parseConstrainedType expects operation" + match op.name, op.args with + | q`Laurel.constrainedType, #[nameArg, valueNameArg, baseArg, constraintArg, witnessArg] => + let name ← translateIdent nameArg + let valueName ← translateIdent valueNameArg + let base ← translateHighType baseArg + let constraint ← translateStmtExpr constraintArg + let witness ← translateStmtExpr witnessArg + return { name, base, valueName, constraint, witness } + | _, _ => + TransM.error s!"parseConstrainedType expects constrainedType, got {repr op.name}" + def parseField (arg : Arg) : TransM Field := do let .op op := arg | TransM.error s!"parseField expects operation" @@ -324,19 +391,26 @@ def parseComposite (arg : Arg) : TransM TypeDefinition := do | _, _ => TransM.error s!"parseComposite expects composite, got {repr op.name}" -def parseTopLevel (arg : Arg) : TransM (Option Procedure × Option TypeDefinition) := do +inductive TopLevelItem where + | proc (p : Procedure) + | typeDef (t : TypeDefinition) + +def parseTopLevel (arg : Arg) : TransM (Option TopLevelItem) := do let .op op := arg | TransM.error s!"parseTopLevel expects operation" match op.name, op.args with | q`Laurel.topLevelProcedure, #[procArg] => let proc ← parseProcedure procArg - return (some proc, none) + return some (.proc proc) | q`Laurel.topLevelComposite, #[compositeArg] => let typeDef ← parseComposite compositeArg - return (none, some typeDef) + return some (.typeDef typeDef) + | q`Laurel.topLevelConstrainedType, #[ctArg] => + let ct ← parseConstrainedType ctArg + return some (.typeDef (.Constrained ct)) | _, _ => - TransM.error s!"parseTopLevel expects topLevelProcedure or topLevelComposite, got {repr op.name}" + TransM.error s!"parseTopLevel expects topLevelProcedure, topLevelComposite, or topLevelConstrainedType, got {repr op.name}" /-- Translate concrete Laurel syntax into abstract Laurel syntax @@ -360,13 +434,11 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do let mut procedures : List Procedure := [] let mut types : List TypeDefinition := [] for op in commands do - let (procOpt, typeOpt) ← parseTopLevel (.op op) - match procOpt with - | some proc => procedures := procedures ++ [proc] - | none => pure () - match typeOpt with - | some typeDef => types := types ++ [typeDef] - | none => pure () + let result ← parseTopLevel (.op op) + match result with + | some (.proc proc) => procedures := procedures ++ [proc] + | some (.typeDef td) => types := types ++ [td] + | none => pure () -- composite types are skipped for now return { staticProcedures := procedures staticFields := [] diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index 07b2c5934..9ce214bb0 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -5,6 +5,7 @@ category LaurelType; op intType : LaurelType => "int"; op boolType : LaurelType => "bool"; op stringType : LaurelType => "string"; +op arrayType (elemType: LaurelType): LaurelType => "Array" "<" elemType ">"; op compositeType (name: Ident): LaurelType => name; category StmtExpr; @@ -14,53 +15,78 @@ op string (s: Str): StmtExpr => s; // Variable declarations category OptionalType; -op optionalType(varType: LaurelType): OptionalType => ":" varType; +op optionalType(varType: LaurelType): OptionalType => ": " varType; category OptionalAssignment; -op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0; +op optionalAssignment(value: StmtExpr): OptionalAssignment => " := " value:0; op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr => @[prec(0)] "var " name varType assignment ";"; -op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")"; +op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => @[prec(95)] callee:85 "(" args ")"; // Field access op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field; +// Array indexing +op arrayIndex (arr: StmtExpr, idx: StmtExpr): StmtExpr => @[prec(90)] arr "[" idx "]"; + // Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier op identifier (name: Ident): StmtExpr => name; op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")"; // Assignment -op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target ":=" value ";"; +op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target " := " value ";"; // Binary operators op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " + " rhs; -op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " == " rhs; -op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " != " rhs; -op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " > " rhs; -op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " < " rhs; -op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " <= " rhs; -op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " >= " rhs; - -// Logical operators +op sub (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " - " rhs; +op mul (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " * " rhs; +op div (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " / " rhs; +op mod (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " % " rhs; +op divT (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " /t " rhs; +op modT (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " %t " rhs; +op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " == " rhs; +op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " != " rhs; +op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " > " rhs; +op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " < " rhs; +op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " <= " rhs; +op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " >= " rhs; op and (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(30), leftassoc] lhs " && " rhs; -op or (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(25), leftassoc] lhs " || " rhs; +op or (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(20), leftassoc] lhs " || " rhs; +op implies (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(15), rightassoc] lhs " ==> " rhs; + +// Unary operators +op not (inner: StmtExpr): StmtExpr => @[prec(80)] "!" inner; +op neg (inner: StmtExpr): StmtExpr => @[prec(80)] "-" inner; + +// Quantifiers +op forallExpr (name: Ident, ty: LaurelType, body: StmtExpr): StmtExpr + => "forall(" name ": " ty ") => " body:0; +op existsExpr (name: Ident, ty: LaurelType, body: StmtExpr): StmtExpr + => "exists(" name ": " ty ") => " body:0; // If-else category OptionalElse; -op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts; +op optionalElse(stmts : StmtExpr) : OptionalElse => "else " stmts:0; op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr => - @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0; + @[prec(20)] "if (" cond ") " thenBranch:0 " " elseBranch:0; op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";"; op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";"; op return (value : StmtExpr) : StmtExpr => "return " value ";"; -op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}"; +op block (stmts : NewlineSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{" indent(2, "\n" stmts) "\n}"; + +// While loops +category InvariantClause; +op invariantClause (cond: StmtExpr): InvariantClause => "\n invariant " cond:0; + +op while (cond: StmtExpr, invariants: Seq InvariantClause, body: StmtExpr): StmtExpr + => "while" "(" cond ")" invariants body:0; category Parameter; -op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType; +op parameter (name: Ident, paramType: LaurelType): Parameter => name ": " paramType; // Composite types category Field; @@ -74,11 +100,11 @@ op composite (name: Ident, fields: Seq Field): Composite => "composite " name "{ category OptionalReturnType; op optionalReturnType(returnType: LaurelType): OptionalReturnType => ":" returnType; -category OptionalRequires; -op optionalRequires(cond: StmtExpr): OptionalRequires => "requires" cond:0; +category RequiresClause; +op requiresClause(cond: StmtExpr): RequiresClause => "requires " cond:0; -category OptionalEnsures; -op optionalEnsures(cond: StmtExpr): OptionalEnsures => "ensures" cond:0; +category EnsuresClause; +op ensuresClause(cond: StmtExpr): EnsuresClause => "ensures " cond:0; category ReturnParameters; op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")"; @@ -87,13 +113,21 @@ category Procedure; op procedure (name : Ident, parameters: CommaSepBy Parameter, returnType: Option OptionalReturnType, returnParameters: Option ReturnParameters, - requires: Option OptionalRequires, - ensures: Option OptionalEnsures, + requires: NewlineSepBy RequiresClause, + ensures: NewlineSepBy EnsuresClause, body : StmtExpr) : Procedure => - "procedure " name "(" parameters ")" returnType returnParameters requires ensures body:0; + "procedure " name "(" parameters ")" returnType returnParameters indent(2, "\n" requires "\n" ensures) "\n" body:0; + +// Constrained types +category ConstrainedType; +op constrainedType (name: Ident, valueName: Ident, base: LaurelType, + constraint: StmtExpr, witness: StmtExpr): ConstrainedType + => "constrained " name " = " valueName ": " base " where " constraint:0 " witness " witness:0; category TopLevel; -op topLevelComposite(composite: Composite): TopLevel => composite; -op topLevelProcedure(procedure: Procedure): TopLevel => procedure; +op topLevelComposite(composite: Composite): TopLevel => composite "\n"; +op topLevelProcedure(procedure: Procedure): TopLevel => procedure "\n"; +op topLevelConstrainedType(ct: ConstrainedType): TopLevel => ct "\n"; + +op program (items: Seq TopLevel): Command => items; -op program (items: Seq TopLevel): Command => items; \ No newline at end of file diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 397a44ef0..29e545854 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -40,60 +40,85 @@ structure AnalysisResult where writesHeapDirectly : Bool := false callees : List Identifier := [] +mutual +def collectExprMd (expr : StmtExprMd) : StateM AnalysisResult Unit := collectExpr expr.val + termination_by sizeOf expr + decreasing_by simp_wf; have := StmtExprMd.sizeOf_val_lt expr; omega + def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do match _: expr with | .FieldSelect target _ => - modify fun s => { s with readsHeapDirectly := true }; collectExpr target - | .InstanceCall target _ args => collectExpr target; for a in args do collectExpr a - | .StaticCall callee args => modify fun s => { s with callees := callee :: s.callees }; for a in args do collectExpr a - | .IfThenElse c t e => collectExpr c; collectExpr t; if let some x := e then collectExpr x - | .Block stmts _ => for s in stmts do collectExpr s - | .LocalVariable _ _ i => if let some x := i then collectExpr x - | .While c i d b => collectExpr c; collectExpr b; if let some x := i then collectExpr x; if let some x := d then collectExpr x - | .Return v => if let some x := v then collectExpr x - | .Assign assignTargets v _ => + modify fun s => { s with readsHeapDirectly := true }; collectExprMd target + | .InstanceCall target _ args => collectExprMd target; for a in args do collectExprMd a + | .StaticCall callee args => modify fun s => { s with callees := callee :: s.callees }; for a in args do collectExprMd a + | .IfThenElse c t e => collectExprMd c; collectExprMd t; if let some x := e then collectExprMd x + | .Block stmts _ => for s in stmts do collectExprMd s + | .LocalVariable _ _ i => if let some x := i then collectExprMd x + | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x + | .Return v => if let some x := v then collectExprMd x + | .Assign assignTargets v => -- Check if any target is a field assignment (heap write) - for ⟨assignTarget, ht⟩ in assignTargets.attach do - match teq: assignTarget with - | .FieldSelect selectTarget _ => + for ⟨assignTarget, _⟩ in assignTargets.attach do + match assignTarget.val with + | .FieldSelect _ _ => modify fun s => { s with writesHeapDirectly := true } - have h: sizeOf selectTarget < sizeOf assignTargets := by (have := List.sizeOf_lt_of_mem ht; simp_all; try omega) - collectExpr selectTarget - | _ => collectExpr assignTarget - collectExpr v - | .PureFieldUpdate t _ v => collectExpr t; collectExpr v - | .PrimitiveOp _ args => for a in args do collectExpr a - | .ReferenceEquals l r => collectExpr l; collectExpr r - | .AsType t _ => collectExpr t - | .IsType t _ => collectExpr t - | .Forall _ _ b => collectExpr b - | .Exists _ _ b => collectExpr b - | .Assigned n => collectExpr n - | .Old v => collectExpr v - | .Fresh v => collectExpr v - | .Assert c _ => collectExpr c - | .Assume c _ => collectExpr c - | .ProveBy v p => collectExpr v; collectExpr p - | .ContractOf _ f => collectExpr f + | _ => pure () + collectExprMd assignTarget + collectExprMd v + | .PureFieldUpdate t _ v => collectExprMd t; collectExprMd v + | .PrimitiveOp _ args => for a in args do collectExprMd a + | .ReferenceEquals l r => collectExprMd l; collectExprMd r + | .AsType t _ => collectExprMd t + | .IsType t _ => collectExprMd t + | .Forall _ _ b => collectExprMd b + | .Exists _ _ b => collectExprMd b + | .Assigned n => collectExprMd n + | .Old v => collectExprMd v + | .Fresh v => collectExprMd v + | .Assert c => collectExprMd c + | .Assume c => collectExprMd c + | .ProveBy v p => collectExprMd v; collectExprMd p + | .ContractOf _ f => collectExprMd f | _ => pure () + termination_by sizeOf expr decreasing_by - all_goals (simp_wf; try omega) - all_goals (try subst_vars; try (rename_i x_in; have := List.sizeOf_lt_of_mem x_in); omega) + all_goals simp_wf + all_goals first + | omega + | (have := StmtExprMd.sizeOf_val_lt ‹_›; omega) + | (subst_vars; have := List.sizeOf_lt_of_mem ‹_›; omega) +end def analyzeProc (proc : Procedure) : AnalysisResult := let bodyResult := match proc.body with - | .Transparent b => (collectExpr b).run {} |>.2 - | .Opaque postcond impl _ => - let r1 := (collectExpr postcond).run {} |>.2 + | .Transparent b => (collectExprMd b).run {} |>.2 + | .Opaque postconds impl modif => + let r1 := postconds.foldl (fun (acc : AnalysisResult) p => + let r := (collectExprMd p).run {} |>.2 + { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, + writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, + callees := acc.callees ++ r.callees }) {} let r2 := match impl with - | some e => (collectExpr e).run {} |>.2 + | some e => (collectExprMd e).run {} |>.2 + | none => {} + let r3 := match modif with + | some e => (collectExprMd e).run {} |>.2 | none => {} - { readsHeapDirectly := r1.readsHeapDirectly || r2.readsHeapDirectly, - writesHeapDirectly := r1.writesHeapDirectly || r2.writesHeapDirectly, - callees := r1.callees ++ r2.callees } - | .Abstract postcond => (collectExpr postcond).run {} |>.2 - -- Also analyze precondition - let precondResult := (collectExpr proc.precondition).run {} |>.2 + { readsHeapDirectly := r1.readsHeapDirectly || r2.readsHeapDirectly || r3.readsHeapDirectly, + writesHeapDirectly := r1.writesHeapDirectly || r2.writesHeapDirectly || r3.writesHeapDirectly, + callees := r1.callees ++ r2.callees ++ r3.callees } + | .Abstract postconds => + postconds.foldl (fun (acc : AnalysisResult) p => + let r := (collectExprMd p).run {} |>.2 + { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, + writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, + callees := acc.callees ++ r.callees }) {} + -- Also analyze preconditions + let precondResult := proc.preconditions.foldl (fun (acc : AnalysisResult) p => + let r := (collectExprMd p).run {} |>.2 + { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, + writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, + callees := acc.callees ++ r.callees }) {} { readsHeapDirectly := bodyResult.readsHeapDirectly || precondResult.readsHeapDirectly, writesHeapDirectly := bodyResult.writesHeapDirectly || precondResult.writesHeapDirectly, callees := bodyResult.callees ++ precondResult.callees } @@ -130,16 +155,17 @@ structure TransformState where fieldConstants : List Constant := [] heapReaders : List Identifier heapWriters : List Identifier - fieldTypes : List (Identifier × HighType) := [] -- Maps field names to their value types + fieldTypes : List (Identifier × HighTypeMd) := [] -- Maps field names to their value types freshCounter : Nat := 0 -- Counter for generating fresh variable names + procedures : List Procedure := [] -- All procedures, for looking up return types abbrev TransformM := StateM TransformState -def addFieldConstant (name : Identifier) (valueType : HighType) : TransformM Unit := +def addFieldConstant (name : Identifier) (valueType : HighTypeMd) : TransformM Unit := modify fun s => if s.fieldConstants.any (·.name == name) then s - else { s with fieldConstants := { name := name, type := .TTypedField valueType } :: s.fieldConstants } + else { s with fieldConstants := { name := name, type := ⟨.TTypedField valueType, #[] ⟩ } :: s.fieldConstants } -def lookupFieldType (name : Identifier) : TransformM (Option HighType) := do +def lookupFieldType (name : Identifier) : TransformM (Option HighTypeMd) := do return (← get).fieldTypes.find? (·.1 == name) |>.map (·.2) def readsHeap (name : Identifier) : TransformM Bool := do @@ -153,114 +179,123 @@ def freshVarName : TransformM Identifier := do set { s with freshCounter := s.freshCounter + 1 } return s!"$tmp{s.freshCounter}" +def lookupCalleeReturnType (callee : Identifier) : TransformM HighTypeMd := do + let procs := (← get).procedures + match procs.find? (·.name == callee) with + | some proc => + match proc.outputs with + | [single] => return single.type + | _ => return ⟨.TInt, #[]⟩ + | none => return ⟨.TInt, #[]⟩ + +/-- Helper to wrap a StmtExpr into StmtExprMd, preserving source metadata from the original expression -/ +def mkMd (md : Imperative.MetaData Core.Expression) (e : StmtExpr) : StmtExprMd := ⟨e, md⟩ + /-- Transform an expression, adding heap parameters where needed. - `heapVar`: the name of the heap variable to use - `valueUsed`: whether the result value of this expression is used (affects optimization of heap-writing calls) -/ -def heapTransformExpr (heapVar : Identifier) (expr : StmtExpr) (valueUsed : Bool := true) : TransformM StmtExpr := - recurse expr valueUsed -where - recurse (expr : StmtExpr) (valueUsed : Bool := true) : TransformM StmtExpr := do - match _: expr with +def heapTransformExpr (heapVar : Identifier) (topExpr : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do + let md := topExpr.md + match _h : topExpr.val with | .FieldSelect selectTarget fieldName => let fieldType ← lookupFieldType fieldName - match fieldType with - | some ty => addFieldConstant fieldName ty - | none => addFieldConstant fieldName .TInt - return .StaticCall "heapRead" [.Identifier heapVar, ← recurse selectTarget, .Identifier fieldName] + addFieldConstant fieldName (fieldType.getD ⟨.TInt, #[]⟩) + let selectTarget' ← heapTransformExpr heapVar selectTarget + return ⟨ .StaticCall "heapRead" [mkMd md (.Identifier heapVar), selectTarget', mkMd md (.Identifier fieldName)], md ⟩ | .StaticCall callee args => - let args' ← args.mapM recurse + let args' ← args.mapM (heapTransformExpr heapVar) let calleeReadsHeap ← readsHeap callee let calleeWritesHeap ← writesHeap callee if calleeWritesHeap then if valueUsed then let freshVar ← freshVarName - let varDecl := StmtExpr.LocalVariable freshVar .TInt none - let callWithHeap := StmtExpr.Assign - [.Identifier heapVar, .Identifier freshVar] - (.StaticCall callee (StmtExpr.Identifier heapVar :: args')) - .empty - return .Block [varDecl, callWithHeap, .Identifier freshVar] none + let retType ← lookupCalleeReturnType callee + let varDecl := mkMd md (.LocalVariable freshVar retType none) + let callWithHeap := ⟨ .Assign + [mkMd md (.Identifier heapVar), mkMd md (.Identifier freshVar)] + (⟨ .StaticCall callee (mkMd md (.Identifier heapVar) :: args'), md ⟩), md ⟩ + return ⟨ .Block [varDecl, callWithHeap, mkMd md (.Identifier freshVar)] none, md ⟩ else - return .Assign [.Identifier heapVar] (.StaticCall callee (StmtExpr.Identifier heapVar :: args')) .empty + return ⟨ .Assign [mkMd md (.Identifier heapVar)] (⟨ .StaticCall callee (mkMd md (.Identifier heapVar) :: args'), md ⟩), md ⟩ else if calleeReadsHeap then - return .StaticCall callee (StmtExpr.Identifier heapVar :: args') + return ⟨ .StaticCall callee (mkMd md (.Identifier heapVar) :: args'), md ⟩ else - return .StaticCall callee args' + return ⟨ .StaticCall callee args', md ⟩ | .InstanceCall callTarget callee args => - let t ← recurse callTarget - let args' ← args.mapM recurse - return .InstanceCall t callee args' + let t ← heapTransformExpr heapVar callTarget + let args' ← args.mapM (heapTransformExpr heapVar) + return ⟨ .InstanceCall t callee args', md ⟩ | .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' + let e' ← match e with | some x => some <$> heapTransformExpr heapVar x valueUsed | none => pure none + return ⟨ .IfThenElse (← heapTransformExpr heapVar c) (← heapTransformExpr heapVar t valueUsed) e', md ⟩ | .Block stmts label => let n := stmts.length - let rec processStmts (idx : Nat) (remaining : List StmtExpr) : TransformM (List StmtExpr) := do - match remaining with - | [] => pure [] - | s :: rest => - let isLast := idx == n - 1 - let s' ← recurse s (isLast && valueUsed) - let rest' ← processStmts (idx + 1) rest - pure (s' :: rest') - termination_by SizeOf.sizeOf remaining - let stmts' ← processStmts 0 stmts - return .Block stmts' label + let stmts' ← stmts.attach.zipIdx.mapM fun (⟨s, _⟩, idx) => + heapTransformExpr heapVar s (idx == n - 1 && valueUsed) + return ⟨ .Block stmts' label, md ⟩ | .LocalVariable n ty i => - let i' ← match i with | some x => some <$> recurse x | none => pure none - return .LocalVariable n ty i' - | .While c i d b => - let i' ← match i with | some x => some <$> recurse x | none => pure none - let d' ← match d with | some x => some <$> recurse x | none => pure none - return .While (← recurse c) i' d' (← recurse b false) + let i' ← match i with | some x => some <$> heapTransformExpr heapVar x | none => pure none + return ⟨ .LocalVariable n ty i', md ⟩ + | .While c invs d b => + let invs' ← invs.mapM (heapTransformExpr heapVar) + let d' ← match d with | some x => some <$> heapTransformExpr heapVar x | none => pure none + return ⟨ .While (← heapTransformExpr heapVar c) invs' d' (← heapTransformExpr heapVar b false), md ⟩ | .Return v => - let v' ← match v with | some x => some <$> recurse x | none => pure none - return .Return v' - | .Assign targets v md => + let v' ← match v with | some x => some <$> heapTransformExpr heapVar x | none => pure none + return ⟨ .Return v', md ⟩ + | .Assign targets v => match targets with - | [StmtExpr.FieldSelect target fieldName] => + | [fieldSelectMd] => + match _h2 : fieldSelectMd.val with + | .FieldSelect target fieldName => let fieldType ← lookupFieldType fieldName match fieldType with | some ty => addFieldConstant fieldName ty - | none => addFieldConstant fieldName .TInt - let target' ← recurse target - let v' ← recurse v - let heapAssign := StmtExpr.Assign [StmtExpr.Identifier heapVar] (.StaticCall "heapStore" [.Identifier heapVar, target', .Identifier fieldName, v']) md + | none => addFieldConstant fieldName ⟨.TInt, #[]⟩ + let target' ← heapTransformExpr heapVar target + let v' ← heapTransformExpr heapVar v + let heapAssign := ⟨ .Assign [mkMd md (.Identifier heapVar)] (mkMd md (.StaticCall "heapStore" [mkMd md (.Identifier heapVar), target', mkMd md (.Identifier fieldName), v'])), md ⟩ if valueUsed then - return .Block [heapAssign, v'] none + return ⟨ .Block [heapAssign, v'] none, md ⟩ else return heapAssign + | _ => + let tgt' ← heapTransformExpr heapVar fieldSelectMd + return ⟨ .Assign [tgt'] (← heapTransformExpr heapVar v), md ⟩ | [] => - return .Assign [] (← recurse v) md + return ⟨ .Assign [] (← heapTransformExpr heapVar v), md ⟩ | tgt :: rest => - let tgt' ← recurse tgt - let targets' ← rest.mapM recurse - return .Assign (tgt' :: targets') (← recurse v) md - | .PureFieldUpdate t f v => return .PureFieldUpdate (← recurse t) f (← recurse v) + let tgt' ← heapTransformExpr heapVar tgt + let targets' ← rest.mapM (heapTransformExpr heapVar) + return ⟨ .Assign (tgt' :: targets') (← heapTransformExpr heapVar v), md ⟩ + | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← heapTransformExpr heapVar t) f (← heapTransformExpr heapVar v), md ⟩ | .PrimitiveOp op args => - let args' ← args.mapM recurse - return .PrimitiveOp op args' - | .ReferenceEquals l r => return .ReferenceEquals (← recurse l) (← recurse r) - | .AsType t ty => return .AsType (← recurse t) ty - | .IsType t ty => return .IsType (← recurse t) ty - | .Forall n ty b => return .Forall n ty (← recurse b) - | .Exists n ty b => return .Exists n ty (← recurse b) - | .Assigned n => return .Assigned (← recurse n) - | .Old v => return .Old (← recurse v) - | .Fresh v => return .Fresh (← recurse v) - | .Assert c md => return .Assert (← recurse c) md - | .Assume c md => return .Assume (← recurse c) md - | .ProveBy v p => return .ProveBy (← recurse v) (← recurse p) - | .ContractOf ty f => return .ContractOf ty (← recurse f) - | other => return other - termination_by sizeOf expr + let args' ← args.mapM (heapTransformExpr heapVar) + return ⟨ .PrimitiveOp op args', md ⟩ + | .ReferenceEquals l r => return ⟨ .ReferenceEquals (← heapTransformExpr heapVar l) (← heapTransformExpr heapVar r), md ⟩ + | .AsType t ty => return ⟨ .AsType (← heapTransformExpr heapVar t) ty, md ⟩ + | .IsType t ty => return ⟨ .IsType (← heapTransformExpr heapVar t) ty, md ⟩ + | .Forall n ty b => return ⟨ .Forall n ty (← heapTransformExpr heapVar b), md ⟩ + | .Exists n ty b => return ⟨ .Exists n ty (← heapTransformExpr heapVar b), md ⟩ + | .Assigned n => return ⟨ .Assigned (← heapTransformExpr heapVar n), md ⟩ + | .Old v => return ⟨ .Old (← heapTransformExpr heapVar v), md ⟩ + | .Fresh v => return ⟨ .Fresh (← heapTransformExpr heapVar v), md ⟩ + | .Assert c => return ⟨ .Assert (← heapTransformExpr heapVar c), md ⟩ + | .Assume c => return ⟨ .Assume (← heapTransformExpr heapVar c), md ⟩ + | .ProveBy v p => return ⟨ .ProveBy (← heapTransformExpr heapVar v) (← heapTransformExpr heapVar p), md ⟩ + | .ContractOf ty f => return ⟨ .ContractOf ty (← heapTransformExpr heapVar f), md ⟩ + | _ => return topExpr + termination_by sizeOf topExpr decreasing_by - all_goals (simp_wf; try subst_vars) - all_goals (try (rename_i h_in; have := List.sizeOf_lt_of_mem h_in; omega)) - all_goals(try omega) - rename_i h_in _; have := List.sizeOf_lt_of_mem h_in; omega + all_goals simp_wf + all_goals first + | (have := StmtExprMd.sizeOf_val_lt topExpr; rw [_h] at this; simp at this + try (have := StmtExprMd.sizeOf_val_lt fieldSelectMd; rw [_h2] at this; simp at this) + try have := List.sizeOf_lt_of_mem ‹_› + omega) + | (have := List.sizeOf_lt_of_mem ‹_›; have := StmtExprMd.sizeOf_val_lt; simp_all; grind) def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do let heapInName := "$heap_in" @@ -271,65 +306,67 @@ def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do if writesHeap then -- This procedure writes the heap - add heap_in as input and heap_out as output -- At the start, assign heap_in to heap_out, then use heap_out throughout - let heapInParam : Parameter := { name := heapInName, type := .THeap } - let heapOutParam : Parameter := { name := heapOutName, type := .THeap } + let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, #[]⟩ } + let heapOutParam : Parameter := { name := heapOutName, type := ⟨.THeap, #[]⟩ } let inputs' := heapInParam :: proc.inputs let outputs' := heapOutParam :: proc.outputs - -- Precondition uses heap_in (the input state) - let precondition' ← heapTransformExpr heapInName proc.precondition + -- Preconditions use heap_in (the input state) + let preconditions' ← proc.preconditions.mapM (heapTransformExpr heapInName) let body' ← match proc.body with | .Transparent bodyExpr => -- First assign heap_in to heap_out, then transform body using heap_out - let assignHeapOut := StmtExpr.Assign [StmtExpr.Identifier heapOutName] (StmtExpr.Identifier heapInName) .empty - let bodyExpr' ← heapTransformExpr heapOutName bodyExpr - pure (.Transparent (.Block [assignHeapOut, bodyExpr'] none)) - | .Opaque postcond impl modif => - -- Postcondition uses heap_out (the output state) - let postcond' ← heapTransformExpr heapOutName postcond + let bmd := bodyExpr.md + let assignHeapOut := mkMd bmd (.Assign [mkMd bmd (.Identifier heapOutName)] (mkMd bmd (.Identifier heapInName))) + let bodyExpr' ← heapTransformExpr heapOutName bodyExpr false + pure (.Transparent (mkMd bmd (.Block [assignHeapOut, bodyExpr'] none))) + | .Opaque postconds impl modif => + -- Postconditions use heap_out (the output state) + let postconds' ← postconds.mapM (heapTransformExpr heapOutName) let impl' ← match impl with | some implExpr => - let assignHeapOut := StmtExpr.Assign [StmtExpr.Identifier heapOutName] (StmtExpr.Identifier heapInName) .empty - let implExpr' ← heapTransformExpr heapOutName implExpr - pure (some (.Block [assignHeapOut, implExpr'] none)) + let imd := implExpr.md + let assignHeapOut := mkMd imd (.Assign [mkMd imd (.Identifier heapOutName)] (mkMd imd (.Identifier heapInName))) + let implExpr' ← heapTransformExpr heapOutName implExpr false + pure (some (mkMd imd (.Block [assignHeapOut, implExpr'] none))) | none => pure none let modif' ← modif.mapM (heapTransformExpr heapOutName) - pure (.Opaque postcond' impl' modif') - | .Abstract postcond => - let postcond' ← heapTransformExpr heapOutName postcond - pure (.Abstract postcond') + pure (.Opaque postconds' impl' modif') + | .Abstract postconds => + let postconds' ← postconds.mapM (heapTransformExpr heapOutName) + pure (.Abstract postconds') return { proc with inputs := inputs', outputs := outputs', - precondition := precondition', + preconditions := preconditions', body := body' } else if readsHeap then -- This procedure only reads the heap - add heap_in as input only - let heapInParam : Parameter := { name := heapInName, type := .THeap } + let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, #[]⟩ } let inputs' := heapInParam :: proc.inputs - let precondition' ← heapTransformExpr heapInName proc.precondition + let preconditions' ← proc.preconditions.mapM (heapTransformExpr heapInName) let body' ← match proc.body with | .Transparent bodyExpr => - let bodyExpr' ← heapTransformExpr heapInName bodyExpr + let bodyExpr' ← heapTransformExpr heapInName bodyExpr false pure (.Transparent bodyExpr') - | .Opaque postcond impl modif => - let postcond' ← heapTransformExpr heapInName postcond - let impl' ← impl.mapM (heapTransformExpr heapInName) + | .Opaque postconds impl modif => + let postconds' ← postconds.mapM (heapTransformExpr heapInName) + let impl' ← impl.mapM (heapTransformExpr heapInName · false) let modif' ← modif.mapM (heapTransformExpr heapInName) - pure (.Opaque postcond' impl' modif') - | .Abstract postcond => - let postcond' ← heapTransformExpr heapInName postcond - pure (.Abstract postcond') + pure (.Opaque postconds' impl' modif') + | .Abstract postconds => + let postconds' ← postconds.mapM (heapTransformExpr heapInName) + pure (.Abstract postconds') return { proc with inputs := inputs', - precondition := precondition', + preconditions := preconditions', body := body' } else @@ -344,10 +381,7 @@ def heapParameterization (program : Program) : Program := match typeDef with | .Composite ct => acc ++ ct.fields.map (fun f => (f.name, f.type)) | .Constrained _ => acc) [] - -- Debug: print heap readers and writers - dbg_trace s!"Heap readers: {heapReaders}" - dbg_trace s!"Heap writers: {heapWriters}" - let (procs', finalState) := (program.staticProcedures.mapM heapTransformProcedure).run { heapReaders, heapWriters, fieldTypes } + let (procs', finalState) := (program.staticProcedures.mapM heapTransformProcedure).run { heapReaders, heapWriters, fieldTypes, procedures := program.staticProcedures } { program with staticProcedures := procs', constants := program.constants ++ finalState.fieldConstants } end Strata.Laurel diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index c4a884a2e..01d75b917 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -24,7 +24,6 @@ Features currently not present: Design choices: - Pure contracts: contracts may only contain pure code. Pure code does not modify the heap, neither by modifying existing objects are creating new ones. - Procedures: instead of functions and methods we have a single more general concept called a 'procedure'. -- Determinism: procedures can be marked as deterministic or not. For deterministic procedures with a non-empty reads clause, we can assume the result is unchanged if the read references are the same. - Opacity: procedures can have a body that's transparant or opaque. Only an opaque body may declare a postcondition. - StmtExpr: Statements and expressions are part of the same type. This reduces duplication since the same concepts are needed in both, such as conditions and variable declarations. - Loops: The only loop is a while, but this can be used to compile do-while and for loops to as well. @@ -52,33 +51,39 @@ inductive Operation: Type where /- Works on Bool -/ /- Equality on composite types uses reference equality for impure types, and structural equality for pure ones -/ | Eq | Neq - | And | Or | Not + | And | Or | Not | Implies /- Works on Int/Float64 -/ - | Neg | Add | Sub | Mul | Div | Mod + | Neg | Add | Sub | Mul | Div | Mod | DivT | ModT | Lt | Leq | Gt | Geq deriving Repr -- Explicit instance needed for deriving Repr in the mutual block instance : Repr (Imperative.MetaData Core.Expression) := inferInstance - mutual +/-- A wrapper that adds metadata to any type -/ +structure HighTypeMd where + val : HighType + md : Imperative.MetaData Core.Expression + deriving Repr + +/-- A wrapper that adds metadata to StmtExpr -/ +structure StmtExprMd where + val : StmtExpr + md : Imperative.MetaData Core.Expression + deriving Repr + structure Procedure: Type where name : Identifier inputs : List Parameter outputs : List Parameter - precondition : StmtExpr - determinism : Determinism - decreases : Option StmtExpr -- optionally prove termination + preconditions : List StmtExprMd + decreases : Option StmtExprMd -- optionally prove termination body : Body -inductive Determinism where - | deterministic (reads: Option StmtExpr) - | nondeterministic - structure Parameter where name : Identifier - type : HighType + type : HighTypeMd inductive HighType : Type where | TVoid @@ -87,24 +92,24 @@ inductive HighType : Type where | TFloat64 /- Required for JavaScript (number). Used by Python (float) and Java (double) as well -/ | TString /- String type for text data -/ | THeap /- Internal type for heap parameterization pass. Not accessible via grammar. -/ - | TTypedField (valueType : HighType) /- Field constant with known value type. Not accessible via grammar. -/ + | TTypedField (valueType : HighTypeMd) /- Field constant with known value type. Not accessible via grammar. -/ | UserDefined (name: Identifier) - | Applied (base : HighType) (typeArguments : List HighType) + | Applied (base : HighTypeMd) (typeArguments : List HighTypeMd) /- Pure represents a composite type that does not support reference equality -/ - | Pure(base: HighType) + | Pure(base: HighTypeMd) /- Java has implicit intersection types. Example: ` ? RustanLeino : AndersHejlsberg` could be typed as `Scientist & Scandinavian`-/ - | Intersection (types : List HighType) + | Intersection (types : List HighTypeMd) deriving Repr /- No support for something like function-by-method yet -/ inductive Body where - | Transparent (body : StmtExpr) + | Transparent (body : StmtExprMd) /- Without an implementation, the postcondition is assumed -/ - | Opaque (postcondition : StmtExpr) (implementation : Option StmtExpr) (modifies : Option StmtExpr) + | Opaque (postconditions : List StmtExprMd) (implementation : Option StmtExprMd) (modifies : Option StmtExprMd) /- An abstract body is useful for types that are extending. A type containing any members with abstract bodies can not be instantiated. -/ - | Abstract (postcondition : StmtExpr) + | Abstract (postconditions : List StmtExprMd) /- A StmtExpr contains both constructs that we typically find in statements and those in expressions. @@ -119,16 +124,16 @@ for example in `Option (StmtExpr isPure)` -/ inductive StmtExpr : Type where /- Statement like -/ - | IfThenElse (cond : StmtExpr) (thenBranch : StmtExpr) (elseBranch : Option StmtExpr) - | Block (statements : List StmtExpr) (label : Option Identifier) + | IfThenElse (cond : StmtExprMd) (thenBranch : StmtExprMd) (elseBranch : Option StmtExprMd) + | Block (statements : List StmtExprMd) (label : Option Identifier) /- The initializer must be set if this StmtExpr is pure -/ - | LocalVariable (name : Identifier) (type : HighType) (initializer : Option StmtExpr) + | LocalVariable (name : Identifier) (type : HighTypeMd) (initializer : Option StmtExprMd) /- While is only allowed in an impure context - The invariant and decreases are always pure + The invariants and decreases are always pure -/ - | While (cond : StmtExpr) (invariant : Option StmtExpr) (decreases: Option StmtExpr) (body : StmtExpr) + | While (cond : StmtExprMd) (invariants : List StmtExprMd) (decreases: Option StmtExprMd) (body : StmtExprMd) | Exit (target: Identifier) - | Return (value : Option StmtExpr) + | Return (value : Option StmtExprMd) /- Expression like -/ | LiteralInt (value: Int) | LiteralBool (value: Bool) @@ -137,31 +142,31 @@ inductive StmtExpr : Type where /- For single target assignments, use a single-element list. Multiple targets are only allowed when the value is a StaticCall to a procedure with multiple outputs, and the number of targets must match the number of outputs. -/ - | Assign (targets : List StmtExpr) (value : StmtExpr) (md : Imperative.MetaData Core.Expression) + | Assign (targets : List StmtExprMd) (value : StmtExprMd) /- Used by itself for fields reads and in combination with Assign for field writes -/ - | FieldSelect (target : StmtExpr) (fieldName : Identifier) + | FieldSelect (target : StmtExprMd) (fieldName : Identifier) /- PureFieldUpdate is the only way to assign values to fields of pure types -/ - | PureFieldUpdate (target : StmtExpr) (fieldName : Identifier) (newValue : StmtExpr) - | StaticCall (callee : Identifier) (arguments : List StmtExpr) - | PrimitiveOp (operator: Operation) (arguments : List StmtExpr) + | PureFieldUpdate (target : StmtExprMd) (fieldName : Identifier) (newValue : StmtExprMd) + | StaticCall (callee : Identifier) (arguments : List StmtExprMd) + | PrimitiveOp (operator: Operation) (arguments : List StmtExprMd) /- Instance related -/ | This - | ReferenceEquals (lhs: StmtExpr) (rhs: StmtExpr) - | AsType (target: StmtExpr) (targetType: HighType) - | IsType (target : StmtExpr) (type: HighType) - | InstanceCall (target : StmtExpr) (callee : Identifier) (arguments : List StmtExpr) + | ReferenceEquals (lhs: StmtExprMd) (rhs: StmtExprMd) + | AsType (target: StmtExprMd) (targetType: HighTypeMd) + | IsType (target : StmtExprMd) (type: HighTypeMd) + | InstanceCall (target : StmtExprMd) (callee : Identifier) (arguments : List StmtExprMd) /- Verification specific -/ - | Forall (name: Identifier) (type: HighType) (body: StmtExpr) - | Exists (name: Identifier) (type: HighType) (body: StmtExpr) - | Assigned (name : StmtExpr) - | Old (value : StmtExpr) + | Forall (name: Identifier) (type: HighTypeMd) (body: StmtExprMd) + | Exists (name: Identifier) (type: HighTypeMd) (body: StmtExprMd) + | Assigned (name : StmtExprMd) + | Old (value : StmtExprMd) /- Fresh may only target impure composite types -/ - | Fresh(value : StmtExpr) + | Fresh(value : StmtExprMd) /- Related to proofs -/ - | Assert (condition: StmtExpr) (md : Imperative.MetaData Core.Expression) - | Assume (condition: StmtExpr) (md : Imperative.MetaData Core.Expression) + | Assert (condition: StmtExprMd) + | Assume (condition: StmtExprMd) /- ProveBy allows writing proof trees. Its semantics are the same as that of the given `value`, but the `proof` is used to help prove any assertions in `value`. @@ -174,10 +179,10 @@ ProveBy( ) ) -/ - | ProveBy (value: StmtExpr) (proof: StmtExpr) + | ProveBy (value: StmtExprMd) (proof: StmtExprMd) -- ContractOf allows extracting the contract of a function - | ContractOf (type: ContractType) (function: StmtExpr) + | ContractOf (type: ContractType) (function: StmtExprMd) /- Abstract can be used as the root expr in a contract for reads/modifies/precondition/postcondition. For example: `reads(abstract)` It can only be used for instance procedures and it makes the containing type abstract, meaning it can not be instantiated. @@ -195,7 +200,13 @@ end instance : Inhabited StmtExpr where default := .Hole -def highEq (a: HighType) (b: HighType) : Bool := match a, b with +instance : Inhabited HighTypeMd where + default := { val := HighType.TVoid, md := default } + +theorem StmtExprMd.sizeOf_val_lt (e : StmtExprMd) : sizeOf e.val < sizeOf e := by + cases e; rename_i val md; show sizeOf val < 1 + sizeOf val + sizeOf md; omega + +partial def highEq (a: HighTypeMd) (b: HighTypeMd) : Bool := match a.val, b.val with | HighType.TVoid, HighType.TVoid => true | HighType.TBool, HighType.TBool => true | HighType.TInt, HighType.TInt => true @@ -205,27 +216,25 @@ def highEq (a: HighType) (b: HighType) : Bool := match a, b with | HighType.TTypedField t1, HighType.TTypedField t2 => highEq t1 t2 | HighType.UserDefined n1, HighType.UserDefined n2 => n1 == n2 | HighType.Applied b1 args1, HighType.Applied b2 args2 => - highEq b1 b2 && args1.length == args2.length && (args1.attach.zip args2 |>.all (fun (a1, a2) => highEq a1.1 a2)) + highEq b1 b2 && args1.length == args2.length && (args1.zip args2 |>.all (fun (a1, a2) => highEq a1 a2)) + | HighType.Pure b1, HighType.Pure b2 => highEq b1 b2 | HighType.Intersection ts1, HighType.Intersection ts2 => - ts1.length == ts2.length && (ts1.attach.zip ts2 |>.all (fun (t1, t2) => highEq t1.1 t2)) + ts1.length == ts2.length && (ts1.zip ts2 |>.all (fun (t1, t2) => highEq t1 t2)) | _, _ => false - termination_by (SizeOf.sizeOf a) - decreasing_by - all_goals(simp_wf; try omega) - . cases a1; simp; rename_i hin; have := List.sizeOf_lt_of_mem hin; omega - . cases t1; simp; rename_i hin; have := List.sizeOf_lt_of_mem hin; omega -instance : BEq HighType where +instance : BEq HighTypeMd where beq := highEq def HighType.isBool : HighType → Bool | TBool => true | _ => false +def HighTypeMd.isBool (t : HighTypeMd) : Bool := t.val.isBool + structure Field where name : Identifier isMutable : Bool - type : HighType + type : HighTypeMd structure CompositeType where name : Identifier @@ -239,10 +248,10 @@ structure CompositeType where structure ConstrainedType where name : Identifier - base : HighType + base : HighTypeMd valueName : Identifier - constraint : StmtExpr - witness : StmtExpr + constraint : StmtExprMd + witness : StmtExprMd /- Note that there are no explicit 'inductive datatypes'. Typed unions are created by @@ -262,7 +271,7 @@ inductive TypeDefinition where structure Constant where name : Identifier - type : HighType + type : HighTypeMd structure Program where staticProcedures : List Procedure diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean index b50d80344..9ccc73bb4 100644 --- a/Strata/Languages/Laurel/LaurelFormat.lean +++ b/Strata/Languages/Laurel/LaurelFormat.lean @@ -11,12 +11,12 @@ namespace Laurel open Std (Format) -mutual def formatOperation : Operation → Format | .Eq => "==" | .Neq => "!=" | .And => "&&" | .Or => "||" + | .Implies => "==>" | .Not => "!" | .Neg => "-" | .Add => "+" @@ -24,12 +24,20 @@ def formatOperation : Operation → Format | .Mul => "*" | .Div => "/" | .Mod => "%" + | .DivT => "/t" + | .ModT => "%t" | .Lt => "<" | .Leq => "<=" | .Gt => ">" | .Geq => ">=" -def formatHighType : HighType → Format +mutual +def formatHighType (t : HighTypeMd) : Format := + have : sizeOf t.val < sizeOf t := by cases t; simp +arith + formatHighTypeVal t.val + termination_by sizeOf t + +def formatHighTypeVal : HighType → Format | .TVoid => "void" | .TBool => "bool" | .TInt => "int" @@ -44,8 +52,14 @@ def formatHighType : HighType → Format | .Pure base => "pure(" ++ formatHighType base ++ ")" | .Intersection types => Format.joinSep (types.map formatHighType) " & " + termination_by t => sizeOf t -def formatStmtExpr (s:StmtExpr) : Format := +def formatStmtExpr (s : StmtExprMd) : Format := + have : sizeOf s.val < sizeOf s := by cases s; simp +arith + formatStmtExprVal s.val + termination_by sizeOf s + +def formatStmtExprVal (s:StmtExpr) : Format := match s with | .IfThenElse cond thenBr elseBr => "if " ++ formatStmtExpr cond ++ " then " ++ formatStmtExpr thenBr ++ @@ -59,8 +73,10 @@ def formatStmtExpr (s:StmtExpr) : Format := match init with | none => "" | some e => " := " ++ formatStmtExpr e - | .While cond _ _ body => - "while " ++ formatStmtExpr cond ++ " " ++ formatStmtExpr body + | .While cond invs _ body => + "while " ++ formatStmtExpr cond ++ + (if invs.isEmpty then Format.nil else " invariant " ++ Format.joinSep (invs.map formatStmtExpr) "; ") ++ + " " ++ formatStmtExpr body | .Exit target => "exit " ++ Format.text target | .Return value => "return" ++ @@ -71,9 +87,9 @@ def formatStmtExpr (s:StmtExpr) : Format := | .LiteralBool b => if b then "true" else "false" | .LiteralString s => "\"" ++ Format.text s ++ "\"" | .Identifier name => Format.text name - | .Assign [single] value _ => + | .Assign [single] value => formatStmtExpr single ++ " := " ++ formatStmtExpr value - | .Assign targets value _ => + | .Assign targets value => "(" ++ Format.joinSep (targets.map formatStmtExpr) ", " ++ ")" ++ " := " ++ formatStmtExpr value | .FieldSelect target field => formatStmtExpr target ++ "#" ++ Format.text field @@ -104,41 +120,37 @@ def formatStmtExpr (s:StmtExpr) : Format := | .Assigned name => "assigned(" ++ formatStmtExpr name ++ ")" | .Old value => "old(" ++ formatStmtExpr value ++ ")" | .Fresh value => "fresh(" ++ formatStmtExpr value ++ ")" - | .Assert cond _ => "assert " ++ formatStmtExpr cond - | .Assume cond _ => "assume " ++ formatStmtExpr cond + | .Assert cond => "assert " ++ formatStmtExpr cond + | .Assume cond => "assume " ++ formatStmtExpr cond | .ProveBy value proof => "proveBy(" ++ formatStmtExpr value ++ ", " ++ formatStmtExpr proof ++ ")" | .ContractOf _ fn => "contractOf(" ++ formatStmtExpr fn ++ ")" | .Abstract => "abstract" | .All => "all" | .Hole => "" + termination_by sizeOf s def formatParameter (p : Parameter) : Format := Format.text p.name ++ ": " ++ formatHighType p.type -def formatDeterminism : Determinism → Format - | .deterministic none => "deterministic" - | .deterministic (some reads) => "deterministic reads " ++ formatStmtExpr reads - | .nondeterministic => "nondeterministic" - def formatBody : Body → Format | .Transparent body => formatStmtExpr body - | .Opaque post impl modif => + | .Opaque posts impl modif => + "opaque " ++ (match modif with | none => "" | some m => " modifies " ++ formatStmtExpr m) ++ - " ensures " ++ formatStmtExpr post ++ + Format.join (posts.map (fun p => " ensures " ++ formatStmtExpr p)) ++ match impl with | none => "" | some e => " := " ++ formatStmtExpr e - | .Abstract post => "abstract ensures " ++ formatStmtExpr post + | .Abstract posts => "abstract" ++ Format.join (posts.map (fun p => " ensures " ++ formatStmtExpr p)) def formatProcedure (proc : Procedure) : Format := "procedure " ++ Format.text proc.name ++ "(" ++ Format.joinSep (proc.inputs.map formatParameter) ", " ++ ") returns " ++ Format.line ++ "(" ++ Format.joinSep (proc.outputs.map formatParameter) ", " ++ ")" ++ Format.line ++ - "requires " ++ formatStmtExpr proc.precondition ++ Format.line ++ - formatDeterminism proc.determinism ++ Format.line ++ + Format.join (proc.preconditions.map (fun p => "requires " ++ formatStmtExpr p ++ Format.line)) ++ formatBody proc.body def formatField (f : Field) : Format := @@ -168,18 +180,21 @@ end instance : Std.ToFormat Operation where format := formatOperation -instance : Std.ToFormat HighType where +instance : Std.ToFormat HighTypeMd where format := formatHighType -instance : Std.ToFormat StmtExpr where +instance : Std.ToFormat HighType where + format := formatHighTypeVal + +instance : Std.ToFormat StmtExprMd where format := formatStmtExpr +instance : Std.ToFormat StmtExpr where + format := formatStmtExprVal + instance : Std.ToFormat Parameter where format := formatParameter -instance : Std.ToFormat Determinism where - format := formatDeterminism - instance : Std.ToFormat Body where format := formatBody diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 73365482a..38f4ce6db 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -11,277 +11,690 @@ import Strata.Languages.Core.Procedure import Strata.Languages.Core.Options import Strata.Languages.Laurel.Laurel import Strata.Languages.Laurel.LiftExpressionAssignments +import Strata.Languages.Laurel.LaurelFormat import Strata.Languages.Laurel.HeapParameterization import Strata.DL.Imperative.Stmt import Strata.DL.Imperative.MetaData import Strata.DL.Lambda.LExpr -import Strata.Languages.Laurel.LaurelFormat open Core (VCResult VCResults) -open Core (intAddOp intSubOp intMulOp intDivOp intModOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp) +open Core (intAddOp intSubOp intMulOp intDivOp intModOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp) namespace Strata.Laurel open Strata open Lambda (LMonoTy LTy LExpr) +def intDivTOp : Core.Expression.Expr := + .op () (Core.CoreIdent.unres "Int.DivT") (some (LMonoTy.arrow LMonoTy.int (LMonoTy.arrow LMonoTy.int LMonoTy.int))) + +def intModTOp : Core.Expression.Expr := + .op () (Core.CoreIdent.unres "Int.ModT") (some (LMonoTy.arrow LMonoTy.int (LMonoTy.arrow LMonoTy.int LMonoTy.int))) + +/-- Map from constrained type name to its definition -/ +abbrev ConstrainedTypeMap := Std.HashMap Identifier ConstrainedType + +/-- Pre-translated constraint: base type and Core expression with free variable for the value -/ +structure TranslatedConstraint where + base : HighType + valueName : Identifier + /-- Core expression for constraint, with valueName as free variable -/ + coreConstraint : Core.Expression.Expr + +/-- Map from constrained type name to pre-translated constraint -/ +abbrev TranslatedConstraintMap := Std.HashMap Identifier TranslatedConstraint + +/-- Build a map of constrained types from a program -/ +def buildConstrainedTypeMap (types : List TypeDefinition) : ConstrainedTypeMap := + types.foldl (init := {}) fun m td => + match td with + | .Constrained ct => m.insert ct.name ct + | _ => m + +/-- Get the base type for a type, resolving constrained types -/ +partial def resolveBaseType (ctMap : ConstrainedTypeMap) (ty : HighType) : HighType := + match ty with + | .UserDefined name => + match ctMap.get? name with + | some ct => resolveBaseType ctMap ct.base.val + | none => ty + | .Applied ctor args => + .Applied ctor (args.map fun arg => ⟨resolveBaseType ctMap arg.val, arg.md⟩) + | _ => ty + /- Translate Laurel HighType to Core Type -/ -def translateType (ty : HighType) : LMonoTy := +partial def translateType (ty : HighType) : LMonoTy := match ty with | .TInt => LMonoTy.int | .TBool => LMonoTy.bool | .TString => LMonoTy.string - | .TVoid => LMonoTy.bool -- Using bool as placeholder for void + | .TVoid => LMonoTy.bool | .THeap => .tcons "Heap" [] - | .TTypedField valueType => .tcons "Field" [translateType valueType] + | .TTypedField valueType => .tcons "Field" [translateType valueType.val] + | .Applied ctor [elemTy] => + match ctor.val with + | .UserDefined "Array" => .tcons "Array" [translateType elemTy.val] + | _ => panic s!"unsupported applied type {repr ty}" | .UserDefined _ => .tcons "Composite" [] | _ => panic s!"unsupported type {repr ty}" -abbrev TypeEnv := List (Identifier × HighType) +/-- Translate type, resolving constrained types to their base type recursively -/ +partial def translateTypeWithCT (ctMap : ConstrainedTypeMap) (ty : HighType) : LMonoTy := + match ty with + | .Applied ctor [elemTy] => + match ctor.val with + | .UserDefined "Array" => .tcons "Array" [translateTypeWithCT ctMap elemTy.val] + | _ => translateType (resolveBaseType ctMap ty) + | _ => translateType (resolveBaseType ctMap ty) -def lookupType (env : TypeEnv) (name : Identifier) : LMonoTy := - match env.find? (fun (n, _) => n == name) with - | some (_, ty) => translateType ty - | none => panic s!"could not find variable {name} in environment" +/-- Translate HighTypeMd, extracting the value -/ +def translateTypeMdWithCT (ctMap : ConstrainedTypeMap) (ty : HighTypeMd) : LMonoTy := + translateTypeWithCT ctMap ty.val + +abbrev TypeEnv := List (Identifier × HighTypeMd) -def isConstant (constants : List Constant) (name : Identifier) : Bool := - constants.any (fun c => c.name == name) +def lookupType (ctMap : ConstrainedTypeMap) (env : TypeEnv) (name : Identifier) : Except String LMonoTy := + match env.find? (fun (n, _) => n == name) with + | some (_, ty) => pure (translateTypeMdWithCT ctMap ty) + | none => throw s!"Unknown identifier: {name}" + +/-- Sequence bounds: array with start (inclusive) and end (exclusive) indices -/ +structure SeqBounds where + arr : Core.Expression.Expr -- the underlying array + start : Core.Expression.Expr -- start index (inclusive) + «end» : Core.Expression.Expr -- end index (exclusive) +deriving Inhabited + +/-- Expand array argument to include length parameter. + Note: Only works when the argument is a simple Identifier; complex expressions are passed through unchanged. -/ +def expandArrayArgs (env : TypeEnv) (args : List StmtExprMd) (translatedArgs : List Core.Expression.Expr) : List Core.Expression.Expr := + (args.zip translatedArgs).flatMap fun (arg, translated) => + match arg.val with + | .Identifier arrName => + match env.find? (fun (n, _) => n == arrName) with + | some (_, ty) => + match ty.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => [translated, .fvar () (Core.CoreIdent.locl (arrName ++ "_len")) (some LMonoTy.int)] + | _ => [translated] + | _ => [translated] + | _ => [translated] + | _ => [translated] + +/-- Translate a binary operation to Core -/ +def translateBinOp (op : Operation) (e1 e2 : Core.Expression.Expr) : Except String Core.Expression.Expr := + let binOp (bop : Core.Expression.Expr) := LExpr.mkApp () bop [e1, e2] + match op with + | .Eq => pure (.eq () e1 e2) + | .Neq => pure (.app () boolNotOp (.eq () e1 e2)) + | .And => pure (binOp boolAndOp) | .Or => pure (binOp boolOrOp) + | .Implies => pure (binOp boolImpliesOp) + | .Add => pure (binOp intAddOp) | .Sub => pure (binOp intSubOp) | .Mul => pure (binOp intMulOp) + | .Div => pure (binOp intDivOp) | .Mod => pure (binOp intModOp) + | .DivT => pure (binOp intDivTOp) | .ModT => pure (binOp intModTOp) + | .Lt => pure (binOp intLtOp) | .Leq => pure (binOp intLeOp) | .Gt => pure (binOp intGtOp) | .Geq => pure (binOp intGeOp) + | _ => throw s!"translateBinOp: unsupported {repr op}" + +/-- Translate a unary operation to Core -/ +def translateUnaryOp (op : Operation) (e : Core.Expression.Expr) : Except String Core.Expression.Expr := + match op with + | .Not => pure (.app () boolNotOp e) + | .Neg => pure (.app () intNegOp e) + | _ => throw s!"translateUnaryOp: unsupported {repr op}" + +def isHeapFunction (name : Identifier) : Bool := + name == "heapRead" || name == "heapStore" + +/-- Translate simple expressions (for constraints - no quantifiers) -/ +partial def translateSimpleExpr (ctMap : ConstrainedTypeMap) (env : TypeEnv) (expr : StmtExprMd) : Except String Core.Expression.Expr := + match expr.val with + | .LiteralBool b => pure (.const () (.boolConst b)) + | .LiteralInt i => pure (.const () (.intConst i)) + | .LiteralString s => pure (.const () (.strConst s)) + | .Identifier name => do + let ty ← lookupType ctMap env name + pure (.fvar () (Core.CoreIdent.locl name) (some ty)) + | .PrimitiveOp op [e] => do + let e' ← translateSimpleExpr ctMap env e + translateUnaryOp op e' + | .PrimitiveOp op [e1, e2] => do + let e1' ← translateSimpleExpr ctMap env e1 + let e2' ← translateSimpleExpr ctMap env e2 + translateBinOp op e1' e2' + | .Forall _ _ _ => throw "Quantifiers not supported in constrained type constraints" + | .Exists _ _ _ => throw "Quantifiers not supported in constrained type constraints" + | _ => throw "Unsupported expression in constrained type constraint" + +/-- Build map of pre-translated constraints -/ +def buildTranslatedConstraintMap (ctMap : ConstrainedTypeMap) : Except String TranslatedConstraintMap := + ctMap.foldM (init := {}) fun m name ct => do + let env : TypeEnv := [(ct.valueName, ct.base)] + let coreExpr ← translateSimpleExpr ctMap env ct.constraint + pure (m.insert name { base := ct.base.val, valueName := ct.valueName, coreConstraint := coreExpr }) + +/-- Close free variable by name, converting fvar to bvar at depth k -/ +def varCloseByName (k : Nat) (x : Core.CoreIdent) (e : Core.Expression.Expr) : Core.Expression.Expr := + match e with + | .const m c => .const m c + | .op m o ty => .op m o ty + | .bvar m i => .bvar m i + | .fvar m y yty => if x == y then .bvar m k else .fvar m y yty + | .abs m ty e' => .abs m ty (varCloseByName (k + 1) x e') + | .quant m qk ty tr e' => .quant m qk ty (varCloseByName (k + 1) x tr) (varCloseByName (k + 1) x e') + | .app m e1 e2 => .app m (varCloseByName k x e1) (varCloseByName k x e2) + | .ite m c t f => .ite m (varCloseByName k x c) (varCloseByName k x t) (varCloseByName k x f) + | .eq m e1 e2 => .eq m (varCloseByName k x e1) (varCloseByName k x e2) + +/-- Translate simple expression (identifier or literal) to Core - for sequence bounds -/ +def translateSimpleBound (expr : StmtExprMd) : Except String Core.Expression.Expr := + match expr.val with + | .Identifier name => pure (.fvar () (Core.CoreIdent.locl name) (some LMonoTy.int)) + | .LiteralInt i => pure (.const () (.intConst i)) + | _ => throw "Expected simple bound expression (identifier or literal)" + +/-- Normalize callee name by removing «» quotes if present -/ +def normalizeCallee (callee : Identifier) : Identifier := + if callee.startsWith "«" && callee.endsWith "»" then + (callee.drop 1 |>.dropEnd 1).toString + else + callee + +/-- Extract sequence bounds from Seq.From/Take/Drop chain. + Note: Seq.From only works with simple Identifier arguments; complex expressions are not supported. -/ +partial def translateSeqBounds (env : TypeEnv) (expr : StmtExprMd) : Except String SeqBounds := + match expr.val with + | .StaticCall callee [arr] => + if normalizeCallee callee == "Seq.From" then + match arr.val with + | .Identifier name => + -- Validate that name is an array + match env.find? (fun (n, _) => n == name) with + | some (_, ty) => + match ty.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => + pure { arr := .fvar () (Core.CoreIdent.locl name) none + , start := .const () (.intConst 0) + , «end» := .fvar () (Core.CoreIdent.locl (name ++ "_len")) (some LMonoTy.int) } + | _ => throw s!"Seq.From expects array, got {repr ty}" + | _ => throw s!"Seq.From expects array, got {repr ty}" + | none => throw s!"Unknown identifier in Seq.From: {name}" + | _ => throw "Seq.From on complex expressions not supported" + else + throw s!"Not a sequence expression: {callee}" + | .StaticCall callee [seq, n] => + let norm := normalizeCallee callee + if norm == "Seq.Take" then do + let inner ← translateSeqBounds env seq + let bound ← translateSimpleBound n + pure { inner with «end» := bound } + else if norm == "Seq.Drop" then do + let inner ← translateSeqBounds env seq + let bound ← translateSimpleBound n + pure { inner with start := bound } + else + throw s!"Not a sequence expression: {callee}" + | _ => throw "Not a sequence expression" + +/-- Inject constraint into quantifier body. For forall uses ==>, for exists uses &&. -/ +def injectQuantifierConstraint (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) + (isForall : Bool) (ty : HighTypeMd) (coreIdent : Core.CoreIdent) (closedBody : Core.Expression.Expr) : Core.Expression.Expr := + match ty.val with + | .UserDefined typeName => match tcMap.get? typeName with + | some tc => + let substConstraint := tc.coreConstraint.substFvar (Core.CoreIdent.locl tc.valueName) + (.fvar () coreIdent (some (translateTypeMdWithCT ctMap ty))) + let op := if isForall then boolImpliesOp else boolAndOp + LExpr.mkApp () op [varCloseByName 0 coreIdent substConstraint, closedBody] + | none => closedBody + | _ => closedBody /-- Translate Laurel StmtExpr to Core Expression -/ -def translateExpr (constants : List Constant) (env : TypeEnv) (expr : StmtExpr) : Core.Expression.Expr := - match h: expr with - | .LiteralBool b => .const () (.boolConst b) - | .LiteralInt i => .const () (.intConst i) - | .LiteralString s => .const () (.strConst s) - | .Identifier name => - -- Check if this is a constant (field constant) or local variable - if isConstant constants name then - -- Constants are global identifiers (functions with no arguments) - let ident := Core.CoreIdent.glob name - -- Field constants are declared as functions () → Field T - -- We just reference them as operations without application - .op () ident none - else - -- Regular variables are local identifiers - let ident := Core.CoreIdent.locl name - .fvar () ident (some (lookupType env name)) - | .PrimitiveOp op [e] => - match op with - | .Not => .app () boolNotOp (translateExpr constants env e) - | .Neg => .app () intNegOp (translateExpr constants env e) - | _ => panic! s!"translateExpr: Invalid unary op: {repr op}" - | .PrimitiveOp op [e1, e2] => - let binOp (bop : Core.Expression.Expr): Core.Expression.Expr := - LExpr.mkApp () bop [translateExpr constants env e1, translateExpr constants env e2] - match op with - | .Eq => .eq () (translateExpr constants env e1) (translateExpr constants env e2) - | .Neq => .app () boolNotOp (.eq () (translateExpr constants env e1) (translateExpr constants env e2)) - | .And => binOp boolAndOp - | .Or => binOp boolOrOp - | .Add => binOp intAddOp - | .Sub => binOp intSubOp - | .Mul => binOp intMulOp - | .Div => binOp intDivOp - | .Mod => binOp intModOp - | .Lt => binOp intLtOp - | .Leq => binOp intLeOp - | .Gt => binOp intGtOp - | .Geq => binOp intGeOp - | _ => panic! s!"translateExpr: Invalid binary op: {repr op}" +partial def translateExpr (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (env : TypeEnv) (expr : StmtExprMd) : Except String Core.Expression.Expr := + match expr.val with + | .LiteralBool b => pure (.const () (.boolConst b)) + | .LiteralInt i => pure (.const () (.intConst i)) + | .LiteralString s => pure (.const () (.strConst s)) + | .Identifier name => do + -- Check if it's in the environment + match env.find? (fun (n, _) => n == name) with + | some (_, ty) => + -- Check if it's a field constant (TTypedField type) + match ty.val with + | .TTypedField _ => + -- Field constants are nullary functions, translate as global op + pure (.op () (Core.CoreIdent.glob name) none) + | _ => + let coreTy := translateTypeMdWithCT ctMap ty + pure (.fvar () (Core.CoreIdent.locl name) (some coreTy)) + | none => + -- Not in env - assume it's a global constant + pure (.op () (Core.CoreIdent.glob name) none) + | .PrimitiveOp op [e] => do + let e' ← translateExpr ctMap tcMap env e + translateUnaryOp op e' + | .PrimitiveOp op [e1, e2] => do + let e1' ← translateExpr ctMap tcMap env e1 + let e2' ← translateExpr ctMap tcMap env e2 + translateBinOp op e1' e2' | .PrimitiveOp op args => - panic! s!"translateExpr: PrimitiveOp {repr op} with {args.length} args" - | .IfThenElse cond thenBranch elseBranch => - let bcond := translateExpr constants env cond - let bthen := translateExpr constants env thenBranch - let belse := match elseBranch with - | some e => translateExpr constants env e - | none => .const () (.intConst 0) - .ite () bcond bthen belse - | .Assign _ value _ => translateExpr constants env value - | .StaticCall name args => - let ident := Core.CoreIdent.glob name - let fnOp := .op () ident none - args.foldl (fun acc arg => .app () acc (translateExpr constants env arg)) fnOp - | .Block [single] _ => translateExpr constants env single - | .FieldSelect target fieldName => - -- Field selects should have been eliminated by heap parameterization - -- If we see one here, it's an error in the pipeline - panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" - | _ => panic! Std.Format.pretty (Std.ToFormat.format expr) - decreasing_by - all_goals (simp_wf; try omega) - rename_i x_in; have := List.sizeOf_lt_of_mem x_in; omega + throw s!"translateExpr: PrimitiveOp {repr op} with {args.length} args" + | .IfThenElse cond thenBranch elseBranch => do + let bcond ← translateExpr ctMap tcMap env cond + let bthen ← translateExpr ctMap tcMap env thenBranch + let belse ← match elseBranch with + | some e => translateExpr ctMap tcMap env e + | none => pure (.const () (.intConst 0)) + pure (.ite () bcond bthen belse) + | .Assign _ value => translateExpr ctMap tcMap env value + | .StaticCall callee [arg] => + let norm := normalizeCallee callee + if norm == "Array.Length" then + match arg.val with + | .Identifier name => pure (.fvar () (Core.CoreIdent.locl (name ++ "_len")) (some LMonoTy.int)) + | _ => throw "Array.Length on complex expressions not supported" + else do + let calleeOp := LExpr.op () (Core.CoreIdent.glob norm) none + let translated ← translateExpr ctMap tcMap env arg + let expandedArgs := expandArrayArgs env [arg] [translated] + pure (expandedArgs.foldl (fun acc a => .app () acc a) calleeOp) + | .StaticCall callee [arg1, arg2] => + let norm := normalizeCallee callee + if norm == "Array.Get" then do + let arrExpr ← translateExpr ctMap tcMap env arg1 + let idxExpr ← translateExpr ctMap tcMap env arg2 + -- Note: Element type constraints (e.g., Array) are not currently enforced on access + let selectOp := LExpr.op () (Core.CoreIdent.unres "select") none + pure (LExpr.mkApp () selectOp [arrExpr, idxExpr]) + else if norm == "Seq.Contains" then do + -- exists i :: start <= i < end && arr[i] == elem + let bounds ← translateSeqBounds env arg1 + let elemExpr ← translateExpr ctMap tcMap env arg2 + let i := LExpr.bvar () 0 + -- start <= i + let geStart := LExpr.mkApp () intLeOp [bounds.start, i] + -- i < end + let ltEnd := LExpr.mkApp () intLtOp [i, bounds.«end»] + -- arr[i] + let selectOp := LExpr.op () (Core.CoreIdent.unres "select") none + let arrAtI := LExpr.mkApp () selectOp [bounds.arr, i] + -- arr[i] == elem + let eqElem := LExpr.eq () arrAtI elemExpr + -- start <= i && i < end && arr[i] == elem + let body := LExpr.mkApp () boolAndOp [geStart, LExpr.mkApp () boolAndOp [ltEnd, eqElem]] + pure (LExpr.quant () .exist (some LMonoTy.int) (LExpr.noTrigger ()) body) + else do + -- Default: treat as function call with array expansion + let calleeOp := LExpr.op () (Core.CoreIdent.glob norm) none + let e1 ← translateExpr ctMap tcMap env arg1 + let e2 ← translateExpr ctMap tcMap env arg2 + let expandedArgs := expandArrayArgs env [arg1, arg2] [e1, e2] + pure (expandedArgs.foldl (fun acc a => .app () acc a) calleeOp) + | .StaticCall name args => do + let normName := normalizeCallee name + -- Use glob for all functions including heap functions + let fnIdent := Core.CoreIdent.glob normName + let fnOp := LExpr.op () fnIdent none + let translatedArgs ← args.mapM (translateExpr ctMap tcMap env) + let expandedArgs := expandArrayArgs env args translatedArgs + pure (expandedArgs.foldl (fun acc a => .app () acc a) fnOp) + | .ReferenceEquals e1 e2 => do + let e1' ← translateExpr ctMap tcMap env e1 + let e2' ← translateExpr ctMap tcMap env e2 + pure (.eq () e1' e2') + | .Block [single] _ => translateExpr ctMap tcMap env single + | .Forall _name ty body => do + let coreType := translateTypeMdWithCT ctMap ty + let env' := (_name, ty) :: env + let bodyExpr ← translateExpr ctMap tcMap env' body + let coreIdent := Core.CoreIdent.locl _name + let closedBody := varCloseByName 0 coreIdent bodyExpr + let finalBody := injectQuantifierConstraint ctMap tcMap true ty coreIdent closedBody + pure (LExpr.quant () .all (some coreType) (LExpr.noTrigger ()) finalBody) + | .Exists _name ty body => do + let coreType := translateTypeMdWithCT ctMap ty + let env' := (_name, ty) :: env + let bodyExpr ← translateExpr ctMap tcMap env' body + let coreIdent := Core.CoreIdent.locl _name + let closedBody := varCloseByName 0 coreIdent bodyExpr + let finalBody := injectQuantifierConstraint ctMap tcMap false ty coreIdent closedBody + pure (LExpr.quant () .exist (some coreType) (LExpr.noTrigger ()) finalBody) + | .Return (some e) => translateExpr ctMap tcMap env e + | _ => throw s!"translateExpr: unsupported {Std.Format.pretty (Std.ToFormat.format expr.val)}" def getNameFromMd (md : Imperative.MetaData Core.Expression): String := let fileRange := (Imperative.getFileRange md).get! s!"({fileRange.range.start})" +def genConstraintCheck (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (param : Parameter) : Option Core.Expression.Expr := + match param.type.val with + | .UserDefined name => + match tcMap.get? name with + | some tc => + let paramIdent := Core.CoreIdent.locl param.name + let valueIdent := Core.CoreIdent.locl tc.valueName + let baseTy := translateTypeMdWithCT ctMap param.type + some (tc.coreConstraint.substFvar valueIdent (.fvar () paramIdent (some baseTy))) + | none => none + | _ => none + +def genConstraintAssert (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (name : Identifier) (ty : HighTypeMd) : List Core.Statement := + match genConstraintCheck ctMap tcMap { name, type := ty } with + | some expr => [Core.Statement.assert s!"{name}_constraint" expr ty.md] + | none => [] + +def defaultExprForType (ctMap : ConstrainedTypeMap) (ty : HighTypeMd) : Core.Expression.Expr := + let resolved := resolveBaseType ctMap ty.val + match resolved with + | .TInt => .const () (.intConst 0) + | .TBool => .const () (.boolConst false) + | .TString => .const () (.strConst "") + | _ => + -- For types without a natural default (arrays, composites, etc.), + -- use a fresh free variable. This is only used when the value is + -- immediately overwritten by a procedure call. + let coreTy := translateType resolved + .fvar () (Core.CoreIdent.locl "$default") (some coreTy) + +/-- Check if a StaticCall should be translated as an expression (not a procedure call) -/ +def isExpressionCall (callee : Identifier) : Bool := + let norm := normalizeCallee callee + isHeapFunction norm || norm.startsWith "Seq." || norm.startsWith "Array." + +/-- +Get element type name if `arr` is `Array` (identifier only). +Generates assumes for constrained array accesses. Limitation: no `obj.field[i]`. +-/ +def getArrayElemConstrainedType (env : TypeEnv) (arr : StmtExprMd) : Option Identifier := + match arr.val with + | .Identifier name => + if let some (_, { val := .Applied { val := .UserDefined "Array", ..} [{ val := .UserDefined elemName, ..}], ..}) := env.find? (fun (n, _) => n == name) then + some elemName + else none + | _ => none + +/-- Collect Array.Get accesses with constrained element types -/ +partial def collectConstrainedArrayAccesses (env : TypeEnv) (tcMap : TranslatedConstraintMap) (expr : StmtExprMd) : List (StmtExprMd × StmtExprMd × TranslatedConstraint) := + let rec go e := match e.val with + | .StaticCall callee [arr, idx] => + let sub := go arr ++ go idx + if normalizeCallee callee == "Array.Get" then + match getArrayElemConstrainedType env arr >>= tcMap.get? with + | some tc => (arr, idx, tc) :: sub + | none => sub + else sub + | .PrimitiveOp _ args | .StaticCall _ args => args.flatMap go + | .IfThenElse c t e => go c ++ go t ++ (e.map go |>.getD []) + | .Assign ts v => ts.flatMap go ++ go v + | .Return (some v) | .Assert v | .Assume v => go v + | .LocalVariable _ _ (some init) => go init + | _ => [] + go expr + +/-- Generate assume statements for constrained array element accesses -/ +def genArrayElemAssumes (tcMap : TranslatedConstraintMap) (env : TypeEnv) (expr : StmtExprMd) + (translateExprFn : StmtExprMd → Except String Core.Expression.Expr) : Except String (List Core.Statement) := do + let accesses := collectConstrainedArrayAccesses env tcMap expr + accesses.mapM fun (arr, idx, tc) => do + let arrExpr ← translateExprFn arr + let idxExpr ← translateExprFn idx + let selectExpr := LExpr.mkApp () (LExpr.op () (Core.CoreIdent.unres "select") none) [arrExpr, idxExpr] + let constraintExpr := tc.coreConstraint.substFvar (Core.CoreIdent.locl tc.valueName) selectExpr + pure (Core.Statement.assume "array_elem_constraint" constraintExpr expr.md) + /-- Translate Laurel StmtExpr to Core Statements -Takes the constants list, type environment and output parameter names +Takes the type environment, output parameter names, and postconditions to assert at returns -/ -def translateStmt (constants : List Constant) (env : TypeEnv) - (outputParams : List Parameter) (stmt : StmtExpr) : TypeEnv × List Core.Statement := - match stmt with - | @StmtExpr.Assert cond md => - let boogieExpr := translateExpr constants env cond - (env, [Core.Statement.assert ("assert" ++ getNameFromMd md) boogieExpr md]) - | @StmtExpr.Assume cond md => - let boogieExpr := translateExpr constants env cond - (env, [Core.Statement.assume ("assume" ++ getNameFromMd md) boogieExpr md]) - | .Block stmts _ => - let (env', stmtsList) := stmts.foldl (fun (e, acc) s => - let (e', ss) := translateStmt constants e outputParams s - (e', acc ++ ss)) (env, []) - (env', stmtsList) - | .LocalVariable name ty initializer => +partial def translateStmt (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (env : TypeEnv) (outputParams : List Parameter) (postconds : List (String × Core.Expression.Expr)) (stmt : StmtExprMd) : Except String (TypeEnv × List Core.Statement) := do + -- Generate assumes for constrained array element accesses before the statement + let arrayElemAssumes ← genArrayElemAssumes tcMap env stmt (translateExpr ctMap tcMap env) + let mkReturnStmts (valueOpt : Option Core.Expression.Expr) : Except String (TypeEnv × List Core.Statement) := do + let postAsserts := postconds.map fun (label, expr) => Core.Statement.assert label expr stmt.md + let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) stmt.md + match valueOpt, outputParams.head? with + | some value, some outParam => + let assignStmt := Core.Statement.set (Core.CoreIdent.locl outParam.name) value + pure (env, arrayElemAssumes ++ [assignStmt] ++ postAsserts ++ [noFallThrough]) + | none, _ => pure (env, arrayElemAssumes ++ postAsserts ++ [noFallThrough]) + | some _, none => throw "Return statement with value but procedure has no output parameters" + match stmt.val with + | .Assert cond => do + let coreExpr ← translateExpr ctMap tcMap env cond + pure (env, arrayElemAssumes ++ [Core.Statement.assert ("assert" ++ getNameFromMd stmt.md) coreExpr stmt.md]) + | .Assume cond => do + let coreExpr ← translateExpr ctMap tcMap env cond + pure (env, arrayElemAssumes ++ [Core.Statement.assume ("assume" ++ getNameFromMd stmt.md) coreExpr stmt.md]) + | .Block stmts _ => do + let mut env' := env + let mut stmtsList := [] + for s in stmts do + let (e', ss) ← translateStmt ctMap tcMap env' outputParams postconds s + env' := e' + stmtsList := stmtsList ++ ss + pure (env', stmtsList) + | .LocalVariable name ty initializer => do let env' := (name, ty) :: env - let boogieMonoType := translateType ty - let boogieType := LTy.forAll [] boogieMonoType + let coreType := LTy.forAll [] (translateTypeMdWithCT ctMap ty) let ident := Core.CoreIdent.locl name + let constraintCheck := genConstraintAssert ctMap tcMap name ty match initializer with - | some (.StaticCall callee args) => - -- Check if this is a heap function (heapRead/heapStore) or a regular procedure call - -- Heap functions should be translated as expressions, not call statements - if callee == "heapRead" || callee == "heapStore" then - -- Translate as expression (function application) - let boogieExpr := translateExpr constants env (.StaticCall callee args) - (env', [Core.Statement.init ident boogieType boogieExpr]) - else - -- Translate as: var name; call name := callee(args) - let boogieArgs := args.map (translateExpr constants env) - let defaultExpr := match ty with - | .TInt => .const () (.intConst 0) - | .TBool => .const () (.boolConst false) - | .TString => .const () (.strConst "") - | _ => .const () (.intConst 0) - let initStmt := Core.Statement.init ident boogieType defaultExpr - let callStmt := Core.Statement.call [ident] callee boogieArgs - (env', [initStmt, callStmt]) - | some initExpr => - let boogieExpr := translateExpr constants env initExpr - (env', [Core.Statement.init ident boogieType boogieExpr]) - | none => - let defaultExpr := match ty with - | .TInt => .const () (.intConst 0) - | .TBool => .const () (.boolConst false) - | .TString => .const () (.strConst "") - | _ => .const () (.intConst 0) - (env', [Core.Statement.init ident boogieType defaultExpr]) - | .Assign targets value _ => + | some init => + match init.val with + | .StaticCall callee args => + if isExpressionCall callee then do + let coreExpr ← translateExpr ctMap tcMap env init + pure (env', arrayElemAssumes ++ [Core.Statement.init ident coreType coreExpr] ++ constraintCheck) + else do + let coreArgs ← args.mapM (translateExpr ctMap tcMap env) + let expandedArgs := expandArrayArgs env args coreArgs + let defaultVal := defaultExprForType ctMap ty + let initStmt := Core.Statement.init ident coreType defaultVal + let callStmt := Core.Statement.call [ident] callee expandedArgs + pure (env', arrayElemAssumes ++ [initStmt, callStmt] ++ constraintCheck) + | _ => do + let coreExpr ← translateExpr ctMap tcMap env init + pure (env', arrayElemAssumes ++ [Core.Statement.init ident coreType coreExpr] ++ constraintCheck) + | none => do + let defaultVal := defaultExprForType ctMap ty + pure (env', arrayElemAssumes ++ [Core.Statement.init ident coreType defaultVal] ++ constraintCheck) + | .Assign targets value => match targets with - | [.Identifier name] => - let ident := Core.CoreIdent.locl name - let boogieExpr := translateExpr constants env value - (env, [Core.Statement.set ident boogieExpr]) + | [target] => + match target.val with + | .Identifier name => do + let ident := Core.CoreIdent.locl name + let constraintCheck := + match env.find? (fun (n, _) => n == name) with + | some (_, ty) => genConstraintAssert ctMap tcMap name ty + | none => [] + match value.val with + | .StaticCall callee args => + if isExpressionCall callee then do + let coreExpr ← translateExpr ctMap tcMap env value + pure (env, arrayElemAssumes ++ [Core.Statement.set ident coreExpr] ++ constraintCheck) + else do + let coreArgs ← args.mapM (translateExpr ctMap tcMap env) + let expandedArgs := expandArrayArgs env args coreArgs + pure (env, arrayElemAssumes ++ [Core.Statement.call [ident] callee expandedArgs] ++ constraintCheck) + | _ => do + let coreExpr ← translateExpr ctMap tcMap env value + pure (env, arrayElemAssumes ++ [Core.Statement.set ident coreExpr] ++ constraintCheck) + | _ => throw s!"translateStmt: unsupported assignment target {Std.Format.pretty (Std.ToFormat.format target.val)}" | _ => - -- Parallel assignment: (var1, var2, ...) := expr - -- Example use is heap-modifying procedure calls: (result, heap) := f(heap, args) - match value with - | .StaticCall callee args => - let boogieArgs := args.map (translateExpr constants env) - let lhsIdents := targets.filterMap fun t => - match t with - | .Identifier name => some (Core.CoreIdent.locl name) - | _ => none - (env, [Core.Statement.call lhsIdents callee boogieArgs]) - | _ => - panic "Assignments with multiple target but without a RHS call should not be constructed" - | .IfThenElse cond thenBranch elseBranch => - let bcond := translateExpr constants env cond - let (_, bthen) := translateStmt constants env outputParams thenBranch - let belse := match elseBranch with - | some e => (translateStmt constants env outputParams e).2 - | none => [] - (env, [Imperative.Stmt.ite bcond bthen belse .empty]) - | .StaticCall name args => - -- Heap functions (heapRead/heapStore) should not appear as standalone statements - -- Only translate actual procedure calls to call statements - if name == "heapRead" || name == "heapStore" then - -- This shouldn't happen in well-formed programs, but handle gracefully - (env, []) - else - let boogieArgs := args.map (translateExpr constants env) - (env, [Core.Statement.call [] name boogieArgs]) - | .Return valueOpt => - match valueOpt, outputParams.head? with - | some value, some outParam => - let ident := Core.CoreIdent.locl outParam.name - let boogieExpr := translateExpr constants env value - let assignStmt := Core.Statement.set ident boogieExpr - let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty - (env, [assignStmt, noFallThrough]) - | none, _ => - let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty - (env, [noFallThrough]) - | some _, none => - panic! "Return statement with value but procedure has no output parameters" - | _ => (env, []) - -/-- -Translate Laurel Parameter to Core Signature entry --/ -def translateParameterToCore (param : Parameter) : (Core.CoreIdent × LMonoTy) := + -- Multi-target assignment: (var1, var2, ...) := call(args) + match value.val with + | .StaticCall callee args => do + let lhsIdents := targets.filterMap fun t => + match t.val with + | .Identifier name => some (Core.CoreIdent.locl name) + | _ => none + let coreArgs ← args.mapM (translateExpr ctMap tcMap env) + let expandedArgs := expandArrayArgs env args coreArgs + pure (env, arrayElemAssumes ++ [Core.Statement.call lhsIdents callee expandedArgs]) + | _ => throw "Assignments with multiple targets but without a RHS call should not be constructed" + | .IfThenElse cond thenBranch elseBranch => do + let bcond ← translateExpr ctMap tcMap env cond + let (_, bthen) ← translateStmt ctMap tcMap env outputParams postconds thenBranch + let belse ← match elseBranch with + | some e => do let (_, s) ← translateStmt ctMap tcMap env outputParams postconds e; pure s + | none => pure [] + pure (env, arrayElemAssumes ++ [Imperative.Stmt.ite bcond bthen belse stmt.md]) + | .While cond invariants _decOpt body => do + let condExpr ← translateExpr ctMap tcMap env cond + -- Combine multiple invariants with && for Core (which expects single invariant) + let invExpr ← match invariants with + | [] => pure none + | [single] => do let e ← translateExpr ctMap tcMap env single; pure (some e) + | first :: rest => do + let firstExpr ← translateExpr ctMap tcMap env first + let combined ← rest.foldlM (fun acc inv => do + let invExpr ← translateExpr ctMap tcMap env inv + pure (LExpr.mkApp () boolAndOp [acc, invExpr])) firstExpr + pure (some combined) + let (_, bodyStmts) ← translateStmt ctMap tcMap env outputParams postconds body + pure (env, arrayElemAssumes ++ [Imperative.Stmt.loop condExpr none invExpr bodyStmts stmt.md]) + | .StaticCall name args => do + if isHeapFunction (normalizeCallee name) then pure (env, arrayElemAssumes) + else do + let coreArgs ← args.mapM (translateExpr ctMap tcMap env) + let expandedArgs := expandArrayArgs env args coreArgs + pure (env, arrayElemAssumes ++ [Core.Statement.call [] name expandedArgs]) + | .Return valueOpt => do + match valueOpt with + | some value => do + let coreExpr ← translateExpr ctMap tcMap env value + mkReturnStmts (some coreExpr) + | none => mkReturnStmts none + | _ => + -- Expression-like statements: treat as implicit return if output param exists + match outputParams.head? with + | some _ => do + let coreExpr ← translateExpr ctMap tcMap env stmt + mkReturnStmts (some coreExpr) + | none => pure (env, []) -- No output param - ignore expression result + +/-- Translate parameter with constrained type resolution -/ +def translateParameterToCoreWithCT (ctMap : ConstrainedTypeMap) (param : Parameter) : (Core.CoreIdent × LMonoTy) := let ident := Core.CoreIdent.locl param.name - let ty := translateType param.type + let ty := translateTypeMdWithCT ctMap param.type (ident, ty) +/-- Expand array parameter to (arr, arr_len) pair -/ +def expandArrayParam (ctMap : ConstrainedTypeMap) (param : Parameter) : List (Core.CoreIdent × LMonoTy) := + match param.type.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => + [ (Core.CoreIdent.locl param.name, translateTypeMdWithCT ctMap param.type) + , (Core.CoreIdent.locl (param.name ++ "_len"), LMonoTy.int) ] + | _ => [translateParameterToCoreWithCT ctMap param] + | _ => [translateParameterToCoreWithCT ctMap param] + /-- Translate Laurel Procedure to Core Procedure -/ -def translateProcedure (constants : List Constant) (proc : Procedure) : Core.Procedure := - let inputPairs := proc.inputs.map translateParameterToCore - let inputs := inputPairs - - let outputs := proc.outputs.map translateParameterToCore - +def translateProcedure (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) + (constants : List Constant) (_heapWriters : List Identifier) (proc : Procedure) : Except String Core.Decl := do + let inputs := proc.inputs.flatMap (expandArrayParam ctMap) let header : Core.Procedure.Header := { name := proc.name typeArgs := [] inputs := inputs - outputs := outputs + outputs := proc.outputs.flatMap (expandArrayParam ctMap) } + -- Build type environment with original types (for constraint checks) + -- Include array length parameters + let arrayLenEnv : TypeEnv := proc.inputs.filterMap (fun p => + match p.type.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => some (p.name ++ "_len", ⟨.TInt, p.type.md⟩) + | _ => none + | _ => none) let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) ++ proc.outputs.map (fun p => (p.name, p.type)) ++ + arrayLenEnv ++ constants.map (fun c => (c.name, c.type)) - -- Translate precondition if it's not just LiteralBool true - let preconditions : ListMap Core.CoreLabel Core.Procedure.Check := - match proc.precondition with - | .LiteralBool true => [] - | precond => - let check : Core.Procedure.Check := { expr := translateExpr constants initEnv precond } - [("requires", check)] - -- Translate postcondition for Opaque bodies - let postconditions : ListMap Core.CoreLabel Core.Procedure.Check := - match proc.body with - | .Opaque postcond _ _ => - let check : Core.Procedure.Check := { expr := translateExpr constants initEnv postcond } - [("ensures", check)] - | _ => [] - let modifies : List Core.Expression.Ident := [] + -- Generate constraint checks for input parameters with constrained types + let inputConstraints : List (Core.CoreLabel × Core.Procedure.Check) ← + proc.inputs.filterMapM (fun p => do + match genConstraintCheck ctMap tcMap p with + | some expr => pure (some (s!"{proc.name}_input_{p.name}_constraint", { expr, md := p.type.md })) + | none => pure none) + -- Array lengths are implicitly >= 0 + let arrayLenConstraints : List (Core.CoreLabel × Core.Procedure.Check) := + proc.inputs.filterMap (fun p => + match p.type.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => + let lenVar := LExpr.fvar () (Core.CoreIdent.locl (p.name ++ "_len")) (some LMonoTy.int) + let zero := LExpr.intConst () 0 + let geZero := LExpr.mkApp () intLeOp [zero, lenVar] + some (s!"{proc.name}_input_{p.name}_len_constraint", { expr := geZero, md := p.type.md }) + | _ => none + | _ => none) + -- Translate explicit preconditions + let mut explicitPreconditions : List (Core.CoreLabel × Core.Procedure.Check) := [] + for h : i in [:proc.preconditions.length] do + let precond := proc.preconditions[i] + let expr ← translateExpr ctMap tcMap initEnv precond + let check : Core.Procedure.Check := { expr, md := precond.md } + explicitPreconditions := explicitPreconditions ++ [(s!"{proc.name}_pre_{i}", check)] + let preconditions := inputConstraints ++ arrayLenConstraints ++ explicitPreconditions + -- Generate constraint checks for output parameters with constrained types + let outputConstraints : List (Core.CoreLabel × Core.Procedure.Check) ← + proc.outputs.filterMapM (fun p => do + match genConstraintCheck ctMap tcMap p with + | some expr => pure (some (s!"{proc.name}_output_{p.name}_constraint", { expr, md := p.type.md })) + | none => pure none) + -- Translate explicit postconditions for Opaque bodies + let mut explicitPostconditions : List (Core.CoreLabel × Core.Procedure.Check) := [] + match proc.body with + | .Opaque posts _ _ => + for h : i in [:posts.length] do + let postcond := posts[i] + let expr ← translateExpr ctMap tcMap initEnv postcond + let check : Core.Procedure.Check := { expr, md := postcond.md } + explicitPostconditions := explicitPostconditions ++ [(s!"{proc.name}_post_{i}", check)] + | _ => pure () + let postconditions := explicitPostconditions ++ outputConstraints + -- Extract postcondition expressions for early return checking + let postcondExprs : List (String × Core.Expression.Expr) := + postconditions.map fun (label, check) => (label, check.expr) + -- Heap is now passed as parameters ($heap_in/$heap_out), no global to modify + let modifies := [] let spec : Core.Procedure.Spec := { - modifies, - preconditions, - postconditions, + modifies := modifies + preconditions := preconditions + postconditions := postconditions } - let body : List Core.Statement := + let body : List Core.Statement ← match proc.body with - | .Transparent bodyExpr => (translateStmt constants initEnv proc.outputs bodyExpr).2 - | .Opaque _postcond (some impl) _ => (translateStmt constants initEnv proc.outputs impl).2 - | _ => [] - { + | .Transparent bodyExpr => do + let (_, stmts) ← translateStmt ctMap tcMap initEnv proc.outputs postcondExprs bodyExpr + pure stmts + | .Opaque _posts (some impl) _ => do + let (_, stmts) ← translateStmt ctMap tcMap initEnv proc.outputs postcondExprs impl + pure stmts + | _ => pure [] + pure <| Core.Decl.proc ({ header := header spec := spec body := body - } + }) .empty def heapTypeDecl : Core.Decl := .type (.con { name := "Heap", numargs := 0 }) def fieldTypeDecl : Core.Decl := .type (.con { name := "Field", numargs := 1 }) def compositeTypeDecl : Core.Decl := .type (.con { name := "Composite", numargs := 0 }) +def arrayTypeSynonym : Core.Decl := .type (.syn { name := "Array", typeArgs := ["T"], type := .tcons "Map" [.int, .ftvar "T"] }) def readFunction : Core.Decl := let heapTy := LMonoTy.tcons "Heap" [] @@ -314,102 +727,126 @@ def updateFunction : Core.Decl := body := none } --- Axiom 1: read-over-write-same --- forall h, r, f, v :: read(store(h, r, f, v), r, f) == v +-- Axiom: forall h, o, f, v :: heapRead(heapStore(h, o, f, v), o, f) == v +-- Using int for field values since Core doesn't support polymorphism in axioms def readUpdateSameAxiom : Core.Decl := let heapTy := LMonoTy.tcons "Heap" [] let compTy := LMonoTy.tcons "Composite" [] let fieldTy := LMonoTy.tcons "Field" [LMonoTy.int] - -- Quantifier order (outer to inner): int (v), Field int (f), Composite (r), Heap (h) - -- So: h is bvar 0, r is bvar 1, f is bvar 2, v is bvar 3 + -- Build: heapRead(heapStore(h, o, f, v), o, f) == v using de Bruijn indices + -- Quantifier order (outer to inner): int (v), Field int (f), Composite (o), Heap (h) + -- So: h is bvar 0, o is bvar 1, f is bvar 2, v is bvar 3 let h := LExpr.bvar () 0 - let r := LExpr.bvar () 1 + let o := LExpr.bvar () 1 let f := LExpr.bvar () 2 let v := LExpr.bvar () 3 - let storeOp := LExpr.op () (Core.CoreIdent.glob "heapStore") none + let updateOp := LExpr.op () (Core.CoreIdent.glob "heapStore") none let readOp := LExpr.op () (Core.CoreIdent.glob "heapRead") none - let storeExpr := LExpr.mkApp () storeOp [h, r, f, v] - let readExpr := LExpr.mkApp () readOp [storeExpr, r, f] + let updateExpr := LExpr.mkApp () updateOp [h, o, f, v] + let readExpr := LExpr.mkApp () readOp [updateExpr, o, f] let eqBody := LExpr.eq () readExpr v + -- Wrap in foralls: forall v:int, f:Field int, o:Composite, h:Heap let body := LExpr.all () (some LMonoTy.int) <| LExpr.all () (some fieldTy) <| LExpr.all () (some compTy) <| LExpr.all () (some heapTy) eqBody - .ax { name := "read_over_write_same", e := body } + .ax { name := "heapRead_heapStore_same", e := body } --- Axiom 2: read-over-write-diff --- forall h, r1, r2, f1, f2, v :: --- (r1 != r2 || f1 != f2) ==> read(store(h, r1, f1, v), r2, f2) == read(h, r2, f2) +-- Axiom: forall h, o1, o2, f1, f2, v :: (o1 != o2 || f1 != f2) ==> heapRead(heapStore(h, o1, f1, v), o2, f2) == heapRead(h, o2, f2) def readUpdateDiffAxiom : Core.Decl := let heapTy := LMonoTy.tcons "Heap" [] let compTy := LMonoTy.tcons "Composite" [] let fieldTy := LMonoTy.tcons "Field" [LMonoTy.int] - -- Quantifier order (outer to inner): int (v), Field (f2), Field (f1), Composite (r2), Composite (r1), Heap (h) - -- So: h is bvar 0, r1 is bvar 1, r2 is bvar 2, f1 is bvar 3, f2 is bvar 4, v is bvar 5 + -- Quantifier order (outer to inner): int (v), Field (f2), Field (f1), Composite (o2), Composite (o1), Heap (h) + -- So: h is bvar 0, o1 is bvar 1, o2 is bvar 2, f1 is bvar 3, f2 is bvar 4, v is bvar 5 let h := LExpr.bvar () 0 - let r1 := LExpr.bvar () 1 - let r2 := LExpr.bvar () 2 + let o1 := LExpr.bvar () 1 + let o2 := LExpr.bvar () 2 let f1 := LExpr.bvar () 3 let f2 := LExpr.bvar () 4 let v := LExpr.bvar () 5 - let storeOp := LExpr.op () (Core.CoreIdent.glob "heapStore") none + let updateOp := LExpr.op () (Core.CoreIdent.glob "heapStore") none let readOp := LExpr.op () (Core.CoreIdent.glob "heapRead") none - let storeExpr := LExpr.mkApp () storeOp [h, r1, f1, v] - let readAfterStore := LExpr.mkApp () readOp [storeExpr, r2, f2] - let readOriginal := LExpr.mkApp () readOp [h, r2, f2] - let refsDiff := LExpr.app () boolNotOp (LExpr.eq () r1 r2) + let updateExpr := LExpr.mkApp () updateOp [h, o1, f1, v] + let lhs := LExpr.mkApp () readOp [updateExpr, o2, f2] + let rhs := LExpr.mkApp () readOp [h, o2, f2] + let objsDiff := LExpr.app () boolNotOp (LExpr.eq () o1 o2) let fieldsDiff := LExpr.app () boolNotOp (LExpr.eq () f1 f2) - let precond := LExpr.app () (LExpr.app () boolOrOp refsDiff) fieldsDiff - let conclusion := LExpr.eq () readAfterStore readOriginal - let implBody := LExpr.app () (LExpr.app () Core.boolImpliesOp precond) conclusion + let precond := LExpr.mkApp () boolOrOp [objsDiff, fieldsDiff] + let implBody := LExpr.mkApp () boolImpliesOp [precond, LExpr.eq () lhs rhs] let body := LExpr.all () (some LMonoTy.int) <| LExpr.all () (some fieldTy) <| LExpr.all () (some fieldTy) <| LExpr.all () (some compTy) <| LExpr.all () (some compTy) <| LExpr.all () (some heapTy) implBody - .ax { name := "read_over_write_diff", e := body } + .ax { name := "heapRead_heapStore_diff", e := body } + +/-- Truncating division (Java/C semantics): truncates toward zero -/ +def intDivTFunc : Core.Decl := + let a := LExpr.fvar () (Core.CoreIdent.locl "a") (some LMonoTy.int) + let b := LExpr.fvar () (Core.CoreIdent.locl "b") (some LMonoTy.int) + let zero := LExpr.intConst () 0 + let aGeZero := LExpr.mkApp () intGeOp [a, zero] + let bGeZero := LExpr.mkApp () intGeOp [b, zero] + let sameSign := LExpr.eq () aGeZero bGeZero + let euclidDiv := LExpr.mkApp () intDivOp [a, b] + let negA := LExpr.mkApp () intNegOp [a] + let negADivB := LExpr.mkApp () intDivOp [negA, b] + let negResult := LExpr.mkApp () intNegOp [negADivB] + let body := LExpr.ite () sameSign euclidDiv negResult + .func { + name := Core.CoreIdent.unres "Int.DivT" + typeArgs := [] + inputs := [(Core.CoreIdent.locl "a", LMonoTy.int), (Core.CoreIdent.locl "b", LMonoTy.int)] + output := LMonoTy.int + body := some body + } + +/-- Truncating modulo (Java/C semantics): a %t b = a - (a /t b) * b -/ +def intModTFunc : Core.Decl := + let a := LExpr.fvar () (Core.CoreIdent.locl "a") (some LMonoTy.int) + let b := LExpr.fvar () (Core.CoreIdent.locl "b") (some LMonoTy.int) + let divT := LExpr.mkApp () intDivTOp [a, b] + let mulDivB := LExpr.mkApp () intMulOp [divT, b] + let body := LExpr.mkApp () intSubOp [a, mulDivB] + .func { + name := Core.CoreIdent.unres "Int.ModT" + typeArgs := [] + inputs := [(Core.CoreIdent.locl "a", LMonoTy.int), (Core.CoreIdent.locl "b", LMonoTy.int)] + output := LMonoTy.int + body := some body + } def translateConstant (c : Constant) : Core.Decl := - match c.type with - | .TTypedField valueType => - -- Field constants with known type: () → Field - let valueTy := translateType valueType - .func { - name := Core.CoreIdent.glob c.name - typeArgs := [] - inputs := [] - output := .tcons "Field" [valueTy] - body := none - } - | _ => - let ty := translateType c.type - .func { - name := Core.CoreIdent.glob c.name - typeArgs := [] - inputs := [] - output := ty - body := none - } + let ty := translateType c.type.val + .func { + name := Core.CoreIdent.glob c.name + typeArgs := [] + inputs := [] + output := ty + body := none + } /-- Check if a StmtExpr is a pure expression (can be used as a Core function body). Pure expressions don't contain statements like assignments, loops, or local variables. A Block with a single pure expression is also considered pure. -/ -def isPureExpr : StmtExpr → Bool - | .LiteralBool _ => true - | .LiteralInt _ => true - | .LiteralString _ => true - | .Identifier _ => true - | .PrimitiveOp _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a) - | .IfThenElse c t none => isPureExpr c && isPureExpr t - | .IfThenElse c t (some e) => isPureExpr c && isPureExpr t && isPureExpr e - | .StaticCall _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a) - | .ReferenceEquals e1 e2 => isPureExpr e1 && isPureExpr e2 - | .Block [single] _ => isPureExpr single +partial def isPureExpr : StmtExprMd → Bool + | ⟨.LiteralBool _, _⟩ => true + | ⟨.LiteralInt _, _⟩ => true + | ⟨.LiteralString _, _⟩ => true + | ⟨.Identifier _, _⟩ => true + | ⟨.PrimitiveOp _ args, _⟩ => args.all isPureExpr + | ⟨.IfThenElse c t (some e), _⟩ => isPureExpr c && isPureExpr t && isPureExpr e + | ⟨.StaticCall _ args, _⟩ => args.all isPureExpr + | ⟨.ReferenceEquals e1 e2, _⟩ => isPureExpr e1 && isPureExpr e2 + | ⟨.Block [single] _, _⟩ => isPureExpr single + | ⟨.Forall _ _ body, _⟩ => isPureExpr body + | ⟨.Exists _ _ body, _⟩ => isPureExpr body + | ⟨.Return (some e), _⟩ => isPureExpr e | _ => false -termination_by e => sizeOf e /-- Check if a procedure can be translated as a Core function. @@ -417,52 +854,65 @@ A procedure can be a function if: - It has a transparent body that is a pure expression - It has no precondition (or just `true`) - It has exactly one output parameter (the return type) +- The output parameter does not have a constrained type (constraints need postcondition checks) -/ -def canBeBoogieFunction (proc : Procedure) : Bool := +def canBeCoreFunction (ctMap : ConstrainedTypeMap) (proc : Procedure) : Bool := match proc.body with | .Transparent bodyExpr => isPureExpr bodyExpr && - (match proc.precondition with | .LiteralBool true => true | _ => false) && - proc.outputs.length == 1 + proc.preconditions.isEmpty && + proc.outputs.length == 1 && + proc.outputs.all (fun p => match p.type.val with + | .UserDefined name => !ctMap.contains name + | _ => true) | _ => false /-- Translate a Laurel Procedure to a Core Function (when applicable) -/ -def translateProcedureToFunction (constants : List Constant) (proc : Procedure) : Core.Decl := - let inputs := proc.inputs.map translateParameterToCore - let outputTy := match proc.outputs.head? with - | some p => translateType p.type - | none => LMonoTy.int - let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) - let body := match proc.body with - | .Transparent bodyExpr => some (translateExpr constants initEnv bodyExpr) - | _ => none - .func { +def translateProcedureToFunction (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (proc : Procedure) : Except String Core.Decl := do + let inputs := proc.inputs.flatMap (expandArrayParam ctMap) + let outputTy ← match proc.outputs.head? with + | some p => pure (translateTypeMdWithCT ctMap p.type) + | none => throw s!"translateProcedureToFunction: {proc.name} has no output parameter" + let arrayLenEnv : TypeEnv := proc.inputs.filterMap (fun p => + match p.type.val with + | .Applied ctor _ => + match ctor.val with + | .UserDefined "Array" => some (p.name ++ "_len", ⟨.TInt, p.type.md⟩) + | _ => none + | _ => none) + let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) ++ arrayLenEnv + let body ← match proc.body with + | .Transparent bodyExpr => do + let expr ← translateExpr ctMap tcMap initEnv bodyExpr + pure (some expr) + | _ => pure none + pure (.func { name := Core.CoreIdent.glob proc.name typeArgs := [] inputs := inputs output := outputTy body := body - } + }) /-- Translate Laurel Program to Core Program -/ def translate (program : Program) : Except (Array DiagnosticModel) Core.Program := do - let program := heapParameterization program - let program ← liftExpressionAssignments program - dbg_trace "=== Program after heapParameterization + liftExpressionAssignments ===" - dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) - dbg_trace "=================================" + let heapWriters := computeWritesHeap program.staticProcedures + let heapProgram := heapParameterization program + let sequencedProgram ← liftExpressionAssignments heapProgram + -- Build constrained type maps + let ctMap := buildConstrainedTypeMap sequencedProgram.types + let tcMap ← buildTranslatedConstraintMap ctMap |>.mapError fun e => #[{ fileRange := default, message := e }] -- Separate procedures that can be functions from those that must be procedures - let (funcProcs, procProcs) := program.staticProcedures.partition canBeBoogieFunction - let procedures := procProcs.map (translateProcedure program.constants) - let procDecls := procedures.map (fun p => Core.Decl.proc p .empty) - let laurelFuncDecls := funcProcs.map (translateProcedureToFunction program.constants) - let constDecls := program.constants.map translateConstant - let typeDecls := [heapTypeDecl, fieldTypeDecl, compositeTypeDecl] - let funcDecls := [readFunction, updateFunction] + let (funcProcs, procProcs) := sequencedProgram.staticProcedures.partition (canBeCoreFunction ctMap) + let procDecls ← procProcs.mapM (translateProcedure ctMap tcMap sequencedProgram.constants heapWriters) |>.mapError fun e => #[{ fileRange := default, message := e }] + let laurelFuncDecls ← funcProcs.mapM (translateProcedureToFunction ctMap tcMap) |>.mapError fun e => #[{ fileRange := default, message := e }] + let constDecls := sequencedProgram.constants.map translateConstant + let typeDecls := [heapTypeDecl, fieldTypeDecl, compositeTypeDecl, arrayTypeSynonym] + let funcDecls := [readFunction, updateFunction, intDivTFunc, intModTFunc] let axiomDecls := [readUpdateSameAxiom, readUpdateDiffAxiom] return { decls := typeDecls ++ funcDecls ++ axiomDecls ++ constDecls ++ laurelFuncDecls ++ procDecls } @@ -473,20 +923,15 @@ def verifyToVcResults (smtsolver : String) (program : Program) (options : Options := Options.default) (tempDir : Option String := .none) : IO (Except (Array DiagnosticModel) VCResults) := do - let strataCoreProgramExcept := translate program + let coreProgramExcept := translate program -- Enable removeIrrelevantAxioms to avoid polluting simple assertions with heap axioms let options := { options with removeIrrelevantAxioms := true } - -- Debug: Print the generated Strata Core program - match strataCoreProgramExcept with + match coreProgramExcept with | .error e => return .error e - | .ok strataCoreProgram => - dbg_trace "=== Generated Strata Core Program ===" - dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format strataCoreProgram))) - dbg_trace "=================================" - + | .ok coreProgram => let runner tempDir := EIO.toIO (fun f => IO.Error.userError (toString f)) - (Core.verify smtsolver strataCoreProgram tempDir .none options) + (Core.verify smtsolver coreProgram tempDir .none options) let ioResult ← match tempDir with | .none => IO.FS.withTempDir runner diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean index 28e6efdfc..f14ed5d74 100644 --- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean +++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean @@ -25,16 +25,14 @@ Becomes: if (x1 == y1) { ... } -/ -private abbrev TypeEnv := List (Identifier × HighType) +private abbrev TypeEnv := List (Identifier × HighTypeMd) -private def lookupType (env : TypeEnv) (name : Identifier) : HighType := - match env.find? (fun (n, _) => n == name) with - | some (_, ty) => ty - | none => .TInt -- Default fallback +private def lookupType (env : TypeEnv) (name : Identifier) : HighTypeMd := + (env.find? (fun (n, _) => n == name)).get!.snd structure SequenceState where insideCondition : Bool - prependedStmts : List StmtExpr := [] + prependedStmts : List StmtExprMd := [] diagnostics : List DiagnosticModel -- Maps variable names to their counter for generating unique temp names varCounters : List (Identifier × Nat) := [] @@ -47,14 +45,14 @@ structure SequenceState where abbrev SequenceM := StateM SequenceState -def SequenceM.addPrependedStmt (stmt : StmtExpr) : SequenceM Unit := +def SequenceM.addPrependedStmt (stmt : StmtExprMd) : SequenceM Unit := modify fun s => { s with prependedStmts := stmt :: s.prependedStmts } def SequenceM.addDiagnostic (d : DiagnosticModel) : SequenceM Unit := modify fun s => { s with diagnostics := d :: s.diagnostics } def checkOutsideCondition(md: Imperative.MetaData Core.Expression): SequenceM Unit := do - let state <- get + let state ← get if state.insideCondition then let fileRange := (Imperative.getFileRange md).get! SequenceM.addDiagnostic { @@ -62,9 +60,6 @@ def checkOutsideCondition(md: Imperative.MetaData Core.Expression): SequenceM Un message := "Could not lift assigment in expression that is evaluated conditionally" } -def SequenceM.setInsideCondition : SequenceM Unit := do - modify fun s => { s with insideCondition := true } - def SequenceM.withInsideCondition (m : SequenceM α) : SequenceM α := do let oldInsideCondition := (← get).insideCondition modify fun s => { s with insideCondition := true } @@ -72,7 +67,7 @@ def SequenceM.withInsideCondition (m : SequenceM α) : SequenceM α := do modify fun s => { s with insideCondition := oldInsideCondition } return result -def SequenceM.takePrependedStmts : SequenceM (List StmtExpr) := do +def SequenceM.takePrependedStmts : SequenceM (List StmtExprMd) := do let stmts := (← get).prependedStmts modify fun s => { s with prependedStmts := [] } return stmts.reverse @@ -89,20 +84,20 @@ def SequenceM.getSnapshot (varName : Identifier) : SequenceM (Option Identifier) def SequenceM.setSnapshot (varName : Identifier) (snapshotName : Identifier) : SequenceM Unit := do modify fun s => { s with varSnapshots := (varName, snapshotName) :: s.varSnapshots.filter (·.1 != varName) } -def SequenceM.getVarType (varName : Identifier) : SequenceM HighType := do +def SequenceM.getVarType (varName : Identifier) : SequenceM HighTypeMd := do return lookupType (← get).env varName -def SequenceM.addToEnv (varName : Identifier) (ty : HighType) : SequenceM Unit := do +def SequenceM.addToEnv (varName : Identifier) (ty : HighTypeMd) : SequenceM Unit := do modify fun s => { s with env := (varName, ty) :: s.env } -def transformTarget (expr : StmtExpr) : SequenceM StmtExpr := do - match expr with +partial def transformTarget (expr : StmtExprMd) : SequenceM StmtExprMd := do + match expr.val with | .PrimitiveOp op args => let seqArgs ← args.mapM transformTarget - return .PrimitiveOp op seqArgs + return ⟨ .PrimitiveOp op seqArgs, expr.md ⟩ | .StaticCall name args => let seqArgs ← args.mapM transformTarget - return .StaticCall name seqArgs + return ⟨ .StaticCall name seqArgs, expr.md ⟩ | _ => return expr -- Identifiers and other targets stay as-is (no snapshot substitution) mutual @@ -110,42 +105,43 @@ mutual Process an expression, extracting any assignments to preceding statements. Returns the transformed expression with assignments replaced by variable references. -/ -def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do - match expr with - | .Assign targets value md => +def transformExpr (expr : StmtExprMd) : SequenceM StmtExprMd := do + let md := expr.md + match _h : expr.val with + | .Assign targets value => checkOutsideCondition md -- This is an assignment in expression context -- We need to: 1) execute the assignment, 2) capture the value in a temporary -- This prevents subsequent assignments to the same variable from changing the value let seqValue ← transformExpr value - let assignStmt := StmtExpr.Assign targets seqValue md + let assignStmt := ⟨ StmtExpr.Assign targets seqValue, md ⟩ SequenceM.addPrependedStmt assignStmt -- For each target, create a snapshot variable so subsequent references -- to that variable will see the value after this assignment for target in targets do - match target with + match target.val with | .Identifier varName => let snapshotName ← SequenceM.freshTempFor varName let snapshotType ← SequenceM.getVarType varName - let snapshotDecl := StmtExpr.LocalVariable snapshotName snapshotType (some (.Identifier varName)) + let snapshotDecl : StmtExprMd := ⟨.LocalVariable snapshotName snapshotType (some ⟨.Identifier varName, md⟩), md⟩ SequenceM.addPrependedStmt snapshotDecl SequenceM.setSnapshot varName snapshotName | _ => pure () -- Create a temporary variable to capture the assigned value (for expression result) -- Use TInt as the type (could be refined with type inference) -- For multi-target assigns, use the first target - let firstTarget := targets.head?.getD (.Identifier "__unknown") + let firstTarget := targets.head?.map (·.val) |>.getD (.Identifier "__unknown") let tempName ← match firstTarget with | .Identifier name => SequenceM.freshTempFor name | _ => SequenceM.freshTempFor "__expr" - let tempDecl := StmtExpr.LocalVariable tempName .TInt (some firstTarget) + let tempDecl : StmtExprMd := ⟨.LocalVariable tempName ⟨.TInt, #[]⟩ (some ⟨firstTarget, md⟩), md⟩ SequenceM.addPrependedStmt tempDecl -- Return the temporary variable as the expression value - return .Identifier tempName + return ⟨.Identifier tempName, md⟩ | .PrimitiveOp op args => let seqArgs ← args.mapM transformExpr - return .PrimitiveOp op seqArgs + return ⟨.PrimitiveOp op seqArgs, md⟩ | .IfThenElse cond thenBranch elseBranch => let seqCond ← transformExpr cond @@ -154,22 +150,22 @@ def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do let seqElse ← match elseBranch with | some e => transformExpr e >>= (pure ∘ some) | none => pure none - return .IfThenElse seqCond seqThen seqElse + return ⟨ .IfThenElse seqCond seqThen seqElse, md ⟩ | .StaticCall name args => let seqArgs ← args.mapM transformExpr - return .StaticCall name seqArgs + return ⟨.StaticCall name seqArgs, md⟩ | .Block stmts metadata => -- Block in expression position: move all but last statement to prepended -- Process statements in order, handling assignments specially to set snapshots - let rec processBlock (remStmts : List StmtExpr) : SequenceM StmtExpr := do + let rec processBlock (remStmts : List StmtExprMd) : SequenceM StmtExprMd := do match _: remStmts with - | [] => return .Block [] metadata + | [] => return ⟨ .Block [] metadata, md ⟩ | [last] => transformExpr last | head :: tail => match head with - | .Assign targets value md => + | ⟨.Assign targets value, headMd⟩ => /- Because we are lifting all assignments and the last one will overwrite the previous one @@ -180,16 +176,16 @@ def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do -/ let seqTargets ← targets.mapM transformTarget let seqValue ← transformExpr value - let assignStmt := StmtExpr.Assign seqTargets seqValue md + let assignStmt : StmtExprMd := ⟨.Assign seqTargets seqValue, headMd⟩ SequenceM.addPrependedStmt assignStmt -- Create snapshot for variables so subsequent reads -- see the value after this assignment (not after later assignments) for target in seqTargets do - match target with + match target.val with | .Identifier varName => let snapshotName ← SequenceM.freshTempFor varName let snapshotType ← SequenceM.getVarType varName - let snapshotDecl := StmtExpr.LocalVariable snapshotName snapshotType (some (.Identifier varName)) + let snapshotDecl : StmtExprMd := ⟨.LocalVariable snapshotName snapshotType (some ⟨.Identifier varName, headMd⟩), headMd⟩ SequenceM.addPrependedStmt snapshotDecl SequenceM.setSnapshot varName snapshotName | _ => pure () @@ -198,94 +194,102 @@ def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do for s in seqStmt do SequenceM.addPrependedStmt s processBlock tail - termination_by SizeOf.sizeOf remStmts + termination_by sizeOf remStmts decreasing_by - all_goals (simp_wf; try omega) - subst_vars; rename_i heq; cases heq; omega + all_goals (simp_wf; try (have := StmtExprMd.sizeOf_val_lt ‹_›; omega)) + subst_vars; rename_i heq; cases heq; omega processBlock stmts - - -- Base cases: no assignments to extract | .LiteralBool _ => return expr | .LiteralInt _ => return expr | .Identifier varName => do -- If this variable has a snapshot (from a lifted assignment), use the snapshot match ← SequenceM.getSnapshot varName with - | some snapshotName => return .Identifier snapshotName + | some snapshotName => return ⟨.Identifier snapshotName, md⟩ | none => return expr | .LocalVariable _ _ _ => return expr | _ => return expr -- Other cases - termination_by SizeOf.sizeOf expr + termination_by sizeOf expr + decreasing_by + all_goals (simp_wf; have := StmtExprMd.sizeOf_val_lt expr; rw [_h] at this; simp at this) + all_goals (try have := List.sizeOf_lt_of_mem ‹_›) + all_goals omega /- Process a statement, handling any assignments in its sub-expressions. Returns a list of statements (the original one may be split into multiple). -/ -def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do - match stmt with - | @StmtExpr.Assert cond md => +def transformStmt (stmt : StmtExprMd) : SequenceM (List StmtExprMd) := do + let md := stmt.md + match _h : stmt.val with + | .Assert cond => -- Process the condition, extracting any assignments let seqCond ← transformExpr cond - SequenceM.addPrependedStmt <| StmtExpr.Assert seqCond md + SequenceM.addPrependedStmt ⟨.Assert seqCond, md⟩ SequenceM.takePrependedStmts - | @StmtExpr.Assume cond md => + | .Assume cond => let seqCond ← transformExpr cond - SequenceM.addPrependedStmt <| StmtExpr.Assume seqCond md + SequenceM.addPrependedStmt ⟨.Assume seqCond, md⟩ SequenceM.takePrependedStmts | .Block stmts metadata => let seqStmts ← stmts.mapM transformStmt - return [.Block (seqStmts.flatten) metadata] + return [⟨.Block (seqStmts.flatten) metadata, md⟩] | .LocalVariable name ty initializer => SequenceM.addToEnv name ty match initializer with | some initExpr => do let seqInit ← transformExpr initExpr - SequenceM.addPrependedStmt <| .LocalVariable name ty (some seqInit) + SequenceM.addPrependedStmt ⟨.LocalVariable name ty (some seqInit), md⟩ SequenceM.takePrependedStmts | none => return [stmt] - | .Assign targets value md => + | .Assign targets value => let seqTargets ← targets.mapM transformTarget let seqValue ← transformExpr value - SequenceM.addPrependedStmt <| .Assign seqTargets seqValue md + SequenceM.addPrependedStmt ⟨ .Assign seqTargets seqValue, md ⟩ SequenceM.takePrependedStmts | .IfThenElse cond thenBranch elseBranch => let seqCond ← transformExpr cond SequenceM.withInsideCondition do let seqThen ← transformStmt thenBranch - let thenBlock := .Block seqThen none + let thenBlock : StmtExprMd := ⟨.Block seqThen none, md⟩ let seqElse ← match elseBranch with | some e => let se ← transformStmt e - pure (some (.Block se none)) + pure (some ⟨ .Block se none, md ⟩) | none => pure none - SequenceM.addPrependedStmt <| .IfThenElse seqCond thenBlock seqElse + SequenceM.addPrependedStmt ⟨ .IfThenElse seqCond thenBlock seqElse, md ⟩ SequenceM.takePrependedStmts | .StaticCall name args => let seqArgs ← args.mapM transformExpr - SequenceM.addPrependedStmt <| .StaticCall name seqArgs + SequenceM.addPrependedStmt ⟨.StaticCall name seqArgs, md⟩ SequenceM.takePrependedStmts | _ => return [stmt] - termination_by SizeOf.sizeOf stmt + termination_by sizeOf stmt + decreasing_by + all_goals (simp_wf; have := StmtExprMd.sizeOf_val_lt stmt; rw [_h] at this; simp at this) + all_goals (try have := List.sizeOf_lt_of_mem ‹_›) + all_goals omega + end -def transformProcedureBody (body : StmtExpr) : SequenceM StmtExpr := do +def transformProcedureBody (body : StmtExprMd) : SequenceM StmtExprMd := do let seqStmts ← transformStmt body match seqStmts with | [single] => pure single - | multiple => pure <| .Block multiple.reverse none + | multiple => pure ⟨.Block multiple none, body.md⟩ def transformProcedure (proc : Procedure) : SequenceM Procedure := do -- Initialize environment with procedure parameters diff --git a/StrataMain.lean b/StrataMain.lean index a85fd2729..70ffdebfb 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -333,14 +333,12 @@ def deserializeIonToLaurelFiles (bytes : ByteArray) : IO (List Strata.StrataFile | .ok files => pure files | .error msg => exitFailure msg -def laurelAnalyzeCommand : Command where - name := "laurelAnalyze" +def laurelAnalyzeBinaryCommand : Command where + name := "laurelAnalyzeBinary" args := [] - help := "Analyze a Laurel Ion program from stdin. Write diagnostics to stdout." + help := "Analyze a Laurel program from binary (Ion) stdin. Write diagnostics to stdout." callback := fun _ _ => do - -- Read bytes from stdin let stdinBytes ← (← IO.getStdin).readBinToEnd - let strataFiles ← deserializeIonToLaurelFiles stdinBytes let mut combinedProgram : Strata.Laurel.Program := { @@ -350,12 +348,10 @@ def laurelAnalyzeCommand : Command where } for strataFile in strataFiles do - let transResult := Strata.Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Strata.Laurel.parseProgram strataFile.program) match transResult with | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}" | .ok laurelProgram => - combinedProgram := { staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields @@ -368,8 +364,108 @@ def laurelAnalyzeCommand : Command where for diag in diagnostics do IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}" +def laurelParseCommand : Command where + name := "laurelParse" + args := [ "file" ] + help := "Parse a Laurel source file (no verification)." + callback := fun _ v => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok _ => IO.println "Parse successful" + +def laurelAnalyzeCommand : Command where + name := "laurelAnalyze" + args := [ "file" ] + help := "Analyze a Laurel source file. Write diagnostics to stdout." + callback := fun _ v => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok laurelProgram => + let results ← Strata.Laurel.verifyToVcResults "z3" laurelProgram Options.default none + match results with + | .error errors => + IO.println s!"==== ERRORS ====" + for err in errors do + IO.println s!"{err.message}" + | .ok vcResults => + IO.println s!"==== RESULTS ====" + for vc in vcResults do + IO.println s!"{vc.obligation.label}: {repr vc.result}" + +def laurelPrintCommand : Command where + name := "laurelPrint" + args := [] + help := "Read Laurel Ion from stdin and print in concrete syntax to stdout." + callback := fun _ _ => do + let stdinBytes ← (← IO.getStdin).readBinToEnd + let strataFiles ← deserializeIonToLaurelFiles stdinBytes + for strataFile in strataFiles do + IO.println s!"// File: {strataFile.filePath}" + let p := strataFile.program + let c := p.formatContext {} + let s := p.formatState + let fmt := p.commands.foldl (init := f!"") fun f cmd => + f ++ (Strata.mformat cmd c s).format + IO.println (fmt.pretty 100) + IO.println "" + +def prettyPrintCore (p : Core.Program) : String := + let decls := p.decls.map fun d => + let s := toString (Std.format d) + -- Add newlines after major sections in procedures + s.replace "preconditions:" "\n preconditions:" + |>.replace "postconditions:" "\n postconditions:" + |>.replace "body:" "\n body:\n " + |>.replace "assert [" "\n assert [" + |>.replace "init (" "\n init (" + |>.replace "while (" "\n while (" + |>.replace "if (" "\n if (" + |>.replace "call [" "\n call [" + |>.replace "else{" "\n else {" + |>.replace "}}" "}\n }" + String.intercalate "\n" decls + +def laurelToCoreCommand : Command where + name := "laurelToCore" + args := [ "file" ] + help := "Translate a Laurel source file to Core and print to stdout." + callback := fun _ v => do + let path : System.FilePath := v[0] + let content ← IO.FS.readFile path + let input := Strata.Parser.stringInputContext path content + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[Strata.initDialect, Strata.Laurel.Laurel] + let strataProgram ← Strata.Elab.parseStrataProgramFromDialect dialects Strata.Laurel.Laurel.name input + + let uri := Strata.Uri.file path.toString + let transResult := Strata.Laurel.TransM.run uri (Strata.Laurel.parseProgram strataProgram) + match transResult with + | .error transErrors => exitFailure s!"Translation errors: {transErrors}" + | .ok laurelProgram => + match Strata.Laurel.translate laurelProgram with + | .error diags => exitFailure s!"Core translation errors: {diags.map (·.message)}" + | .ok coreProgram => IO.println (prettyPrintCore coreProgram) + def commandList : List Command := [ javaGenCommand, + laurelPrintCommand, + laurelParseCommand, + laurelToCoreCommand, checkCommand, toIonCommand, printCommand, @@ -378,6 +474,7 @@ def commandList : List Command := [ pyTranslateCommand, pySpecsCommand, laurelAnalyzeCommand, + laurelAnalyzeBinaryCommand, ] def commandMap : Std.HashMap String Command := diff --git a/StrataTest/DDM/Bool.lean b/StrataTest/DDM/Bool.lean index c27f40002..8ae4d9f1b 100644 --- a/StrataTest/DDM/Bool.lean +++ b/StrataTest/DDM/Bool.lean @@ -45,7 +45,7 @@ print if true then false else true; #end /-- -info: "program TestBool;\nprint if true then false else (true);" +info: "program TestBool;\nprint if true then false else true;" -/ #guard_msgs in #eval toString testIfThenElse.format @@ -57,7 +57,7 @@ print if true then if false then true else false else true; #end /-- -info: "program TestBool;\nprint if true then if false then true else (false) else (true);" +info: "program TestBool;\nprint if true then if false then true else false else true;" -/ #guard_msgs in #eval toString testNested.format diff --git a/StrataTest/DDM/Integration/Lean/Gen.lean b/StrataTest/DDM/Integration/Lean/Gen.lean index 3fa31b4d6..2b1ab816b 100644 --- a/StrataTest/DDM/Integration/Lean/Gen.lean +++ b/StrataTest/DDM/Integration/Lean/Gen.lean @@ -46,26 +46,26 @@ op cmd (tp : Type, a : tp) : Command => "cmd " a; /-- -trace: [Strata.generator] Generating EmptyExprDialectType ---- -trace: [Strata.generator] Generating EmptyExprDialectType.toAst ---- -trace: [Strata.generator] Generating EmptyExprDialectType.ofAst ---- trace: [Strata.generator] Generating Expr --- trace: [Strata.generator] Generating Expr.toAst --- trace: [Strata.generator] Generating Expr.ofAst --- +trace: [Strata.generator] Generating EmptyExprDialectType +--- +trace: [Strata.generator] Generating EmptyExprDialectType.toAst +--- +trace: [Strata.generator] Generating EmptyExprDialectType.ofAst +--- trace: [Strata.generator] Generating Command --- trace: [Strata.generator] Generating Command.toAst --- trace: [Strata.generator] Generating Command.ofAst --- -trace: [Strata.generator] Declarations group: [Init.Type] -[Strata.generator] Declarations group: [Init.Expr] +trace: [Strata.generator] Declarations group: [Init.Expr] +[Strata.generator] Declarations group: [Init.Type] [Strata.generator] Declarations group: [Init.Command] -/ #guard_msgs in diff --git a/StrataTest/Languages/B3/DDMFormatDeclarationsTests.lean b/StrataTest/Languages/B3/DDMFormatDeclarationsTests.lean index 6e8971574..e89cbf873 100644 --- a/StrataTest/Languages/B3/DDMFormatDeclarationsTests.lean +++ b/StrataTest/Languages/B3/DDMFormatDeclarationsTests.lean @@ -666,7 +666,7 @@ info: B3: .program (.intLit () 0)))])] --- info: -procedure withAutoinv(x : int autoinv x + y >= 0, y : int autoinv y >= -(x)) +procedure withAutoinv(x : int autoinv x + y >= 0, y : int autoinv y >= -x) { check x >= 0 } diff --git a/StrataTest/Languages/B3/DDMFormatExpressionsTests.lean b/StrataTest/Languages/B3/DDMFormatExpressionsTests.lean index aa0f574e2..c69029667 100644 --- a/StrataTest/Languages/B3/DDMFormatExpressionsTests.lean +++ b/StrataTest/Languages/B3/DDMFormatExpressionsTests.lean @@ -633,7 +633,7 @@ info: B3: .binaryOp (.literal () (.boolLit () false)) (.literal () (.boolLit () true))) --- -info: true <== (false <== true) +info: true <== false <== true -/ #guard_msgs in #eval roundtripExpr $ #strata program B3CST; check true <== (false <== true) #end @@ -688,7 +688,7 @@ info: B3: .binaryOp (.literal () (.boolLit () false))) (.literal () (.boolLit () true)) --- -info: (true ==> false) ==> true +info: true ==> false ==> true -/ #guard_msgs in #eval roundtripExpr $ #strata program B3CST; check (true ==> false) ==> true #end diff --git a/StrataTest/Languages/B3/Verifier/VerifierTests.lean b/StrataTest/Languages/B3/Verifier/VerifierTests.lean index 0b42af9f3..a83c27c18 100644 --- a/StrataTest/Languages/B3/Verifier/VerifierTests.lean +++ b/StrataTest/Languages/B3/Verifier/VerifierTests.lean @@ -313,16 +313,16 @@ procedure test_fail() { /-- info: test_all_expressions: ✗ unknown - (0,127): check (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -(5) == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) + (0,127): check (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -5 == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) └─ (0,213): could not prove notalwaystrue(1, 2) under the assumptions - forall x : int pattern f(x) f(x) == (x + 1 == 6) + forall x : int pattern f(x) f(x) == x + 1 == 6 false || true if true true else false f(5) └─ (0,353): it is impossible that 1 + 2 == 4 under the assumptions - forall x : int pattern f(x) f(x) == (x + 1 == 6) + forall x : int pattern f(x) f(x) == x + 1 == 6 false || true if true true else false f(5) @@ -480,10 +480,10 @@ procedure test_reach_diagnosis() { /-- info: test_all_expressions: ✗ refuted - (0,127): reach (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -(5) == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) + (0,127): reach (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -5 == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) └─ (0,353): it is impossible that 1 + 2 == 4 under the assumptions - forall x : int pattern f(x) f(x) == (x + 1 == 6) + forall x : int pattern f(x) f(x) == x + 1 == 6 false || true if true true else false f(5) diff --git a/StrataTest/Languages/C_Simp/Examples/Coprime.lean b/StrataTest/Languages/C_Simp/Examples/Coprime.lean index 664391a37..0db1b8791 100644 --- a/StrataTest/Languages/C_Simp/Examples/Coprime.lean +++ b/StrataTest/Languages/C_Simp/Examples/Coprime.lean @@ -37,24 +37,26 @@ bool procedure coprime (a: int, b: int) /-- info: program C_Simp; -bool procedure coprime(a:int, b:int)//@pre(a>(0))&&(b>(0)); -//@posttrue; - ({ - vari:int; - i=a; - if(b(1)) - //@decreasesi//@invariant(true)({ - if(((b%i)==(0))&&((a%i)==(0))){ - returnfalse; - } - ()i=i-(1); +bool procedure coprime(a:int, b:int) + //@pre a > 0 && b > 0; + //@post true; +{ + var i:int; + i = a; + if (b < a) { + i = b; } - )returntrue; + while (i > 1) + //@decreases i + //@invariant true + { + if (b % i == 0 && a % i == 0) { + return false; + } + i = i - 1; } - ) + return true; +} -/ #guard_msgs in #eval IO.println CoprimePgm diff --git a/StrataTest/Languages/C_Simp/Examples/LinearSearch.lean b/StrataTest/Languages/C_Simp/Examples/LinearSearch.lean index 9d71ea267..a84433f2d 100644 --- a/StrataTest/Languages/C_Simp/Examples/LinearSearch.lean +++ b/StrataTest/Languages/C_Simp/Examples/LinearSearch.lean @@ -36,21 +36,23 @@ bool procedure linearSearch (arr: intArr, e: int) /-- info: program C_Simp; -bool procedure linearSearch(arr:intArr, e:int)//@pretrue; -//@posttrue; - ({ - varidx:int; - idx=0; - while(idx<(len(arr))) - //@decreases((len(arr))-idx)//@invariant(true)({ - if(e==(get(arr,idx))){ - returntrue; - } - ()idx=idx+(1); - } - )returnfalse; +bool procedure linearSearch(arr:intArr, e:int) + //@pre true; + //@post true; +{ + var idx:int; + idx = 0; + while (idx < len(arr)) + //@decreases len(arr) - idx + //@invariant true + { + if (e == get(arr, idx)) { + return true; + } + idx = idx + 1; } - ) + return false; +} -/ #guard_msgs in #eval IO.println LinearSearchEnv diff --git a/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean b/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean index 88b262a93..97de42096 100644 --- a/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean +++ b/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean @@ -35,22 +35,24 @@ int procedure loopSimple (n: int) /-- info: program C_Simp; -int procedure loopSimple(n:int)//@pren>=(0); -//@posttrue; - ({ - varsum:int; - vari:int; - sum=0; - i=0; - while(i= 0; + //@post true; +{ + var sum:int; + var i:int; + sum = 0; + i = 0; + while (i < n) + //@decreases n - i + //@invariant i <= n && i * i - 1 / 2 == sum + { + sum = sum + i; + i = i + 1; } - ) + //@assert [sum_assert] n * n - 1 / 2 == sum; + return sum; +} -/ #guard_msgs in #eval IO.println LoopSimplePgm diff --git a/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean b/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean index aefbc79ba..e3bee3b2c 100644 --- a/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean +++ b/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean @@ -34,19 +34,21 @@ int procedure loopTrivial (n: int) /-- info: program C_Simp; -int procedure loopTrivial(n:int)//@pren>=(0); -//@posttrue; - ({ - vari:int; - i=0; - while(i= 0; + //@post true; +{ + var i:int; + i = 0; + while (i < n) + //@decreases n - i + //@invariant i <= n + { + i = i + 1; } - ) + //@assert [i_eq_n] i == n; + return i; +} -/ #guard_msgs in #eval IO.println LoopTrivialPgm diff --git a/StrataTest/Languages/C_Simp/Examples/Min.lean b/StrataTest/Languages/C_Simp/Examples/Min.lean index d95779bb8..e82b8087b 100644 --- a/StrataTest/Languages/C_Simp/Examples/Min.lean +++ b/StrataTest/Languages/C_Simp/Examples/Min.lean @@ -26,17 +26,16 @@ int procedure min (a: int, b: int) /-- info: program C_Simp; -int procedure min(a:int, b:int)//@pretrue; -//@posttrue; - ({ - if(a(0); -//@posttrue; - ({ - varz:int; - z=x+y; - //@assert [test_assert]z>x; - if(z>(10)){ - z=z-(1); - } - (else({ - z=z+(1); - } - ))//@assume [test_assume]z>(0); - return0; +int procedure simpleTest(x:int, y:int) + //@pre y > 0; + //@post true; +{ + var z:int; + z = x + y; + //@assert [test_assert] z > x; + if (z > 10) { + z = z - 1; + } else { + z = z + 1; } - ) + //@assume [test_assume] z > 0; + return 0; +} -/ #guard_msgs in #eval IO.println SimpleTestEnv diff --git a/StrataTest/Languages/C_Simp/Examples/Trivial.lean b/StrataTest/Languages/C_Simp/Examples/Trivial.lean index cac9f4b03..9b60028b5 100644 --- a/StrataTest/Languages/C_Simp/Examples/Trivial.lean +++ b/StrataTest/Languages/C_Simp/Examples/Trivial.lean @@ -22,12 +22,12 @@ bool procedure trivial () /-- info: program C_Simp; -bool procedure trivial()//@pretrue; -//@posttrue; - ({ - returntrue; - } - ) +bool procedure trivial() + //@pre true; + //@post true; +{ + return true; +} -/ #guard_msgs in #eval IO.println TrivialPgm diff --git a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean index 86e7b72e5..c4692d96f 100644 --- a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean +++ b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean @@ -87,8 +87,8 @@ def extractAxiomsWithFreeTypeVars (pgm: Program) (typeArgs: List String): (List info: program Core; type k; type v; -axiom [updateSelect]:forall((m:(Map v k)),(kk:k)),(vv:v)::(m[kk:=vv])[kk]==vv; -axiom [updatePreserves]:forall(((m:(Map v k)),(okk:k)),(kk:k)),(vv:v)::(m[kk:=vv])[okk]==m[okk]; +axiom [updateSelect]: forall m:(Map v k), kk:k, vv:v::m[kk:=vv][kk]==vv; +axiom [updatePreserves]: forall m:(Map v k), okk:k, kk:k, vv:v::m[kk:=vv][okk]==m[okk]; -/ #guard_msgs in #eval IO.println examplePgm diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T01_AssertAssume.lean similarity index 87% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T01_AssertAssume.lean index 79f93745f..16fef59c9 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T01_AssertAssume.lean @@ -28,4 +28,4 @@ procedure bar() { " #guard_msgs(drop info, error) in -#eval testInputWithOffset "AssertFalse" program 14 processLaurelFile +#eval testInputWithOffset "AssertAssume" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T02_Operators.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T02_Operators.lean new file mode 100644 index 000000000..37d2a74f5 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T02_Operators.lean @@ -0,0 +1,61 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util + +namespace Strata +namespace Laurel + +def program := r" +procedure testArithmetic() { + var a: int := 10; + var b: int := 3; + var x: int := a - b; + assert x == 7; + var y: int := x * 2; + assert y == 14; + var z: int := y / 2; + assert z == 7; + var r: int := 17 % 5; + assert r == 2; +} + +procedure testLogical() { + var t: bool := true; + var f: bool := false; + var a: bool := t && f; + assert a == false; + var b: bool := t || f; + assert b == true; + var c: bool := !f; + assert c == true; + assert t ==> t; + assert f ==> t; +} + +procedure testUnary() { + var x: int := 5; + var y: int := -x; + assert y == 0 - 5; +} + +procedure testTruncatingDiv() { + // Truncating division rounds toward zero (Java/C semantics) + // For positive numbers, same as Euclidean + assert 7 /t 3 == 2; + assert 7 %t 3 == 1; + // For negative dividend, truncates toward zero (not floor) + // -7 /t 3 = -2 (not -3), -7 %t 3 = -1 (not 2) + assert (0 - 7) /t 3 == 0 - 2; + assert (0 - 7) %t 3 == 0 - 1; +} +" + +#guard_msgs(drop info, error) in +#eval testInputWithOffset "Operators" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T03_Variables.lean similarity index 64% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T03_Variables.lean index 14cd81c47..7f41f294b 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T03_Variables.lean @@ -22,15 +22,17 @@ procedure NestedImpureStatements() { assert z == y; } -procedure multipleAssignments() { - var x: int; - var y: int := ((x := 1;) + x) + (x := 2;); - assert y == 4; +// Regression test: assignment lifting after a conditional should work +procedure AssignmentAfterConditional(x: int) { + var y: int := 0; + if (x > 0) { y := 1; } + var z: int := y := y + 1;; + assert z == y; } " #guard_msgs (error, drop all) in -#eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFile +#eval! testInputWithOffset "Variables" program 14 processLaurelFile end Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T04_VariablesNotSupported.lean similarity index 87% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T04_VariablesNotSupported.lean index d4add1741..39cd8bbca 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T04_VariablesNotSupported.lean @@ -27,7 +27,7 @@ procedure conditionalAssignmentInExpression(x: int) { " #guard_msgs(drop info, error) in -#eval! testInputWithOffset "T2_ImpureExpressionsNotSupported" program 14 processLaurelFile +#eval! testInputWithOffset "VariablesNotSupported" program 14 processLaurelFile end Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T05_ControlFlow.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T05_ControlFlow.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T06_WhileLoops.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T06_WhileLoops.lean new file mode 100644 index 000000000..4dd6594ec --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T06_WhileLoops.lean @@ -0,0 +1,40 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util + +namespace Strata +namespace Laurel + +def program := r" +procedure countDown() { + var i: int := 3; + while(i > 0) + invariant i >= 0 + { + i := i - 1; + } + assert i == 0; +} + +procedure countUp() { + var n: int := 5; + var i: int := 0; + while(i < n) + invariant i >= 0 + invariant i <= n + { + i := i + 1; + } + assert i == n; +} +" + +#guard_msgs(drop info, error) in +#eval testInputWithOffset "WhileLoops" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T07_Contracts.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T07_Contracts.lean new file mode 100644 index 000000000..d72d31779 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T07_Contracts.lean @@ -0,0 +1,30 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples +open StrataTest.Util +namespace Strata.Laurel + +def program := r" +procedure test(x: int) + requires forall(i: int) => i >= 0 + ensures exists(j: int) => j == x +{} + +procedure multiContract(x: int) returns (r: int) + requires x >= 0 + requires x <= 100 + ensures r >= x + ensures r <= x + 10 +{ + return x + 5; +} +" + +#guard_msgs(drop info) in +#eval testInputWithOffset "Contracts" program 5 processLaurelFile + +end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T08_ContractsCalls.lean similarity index 92% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T08_ContractsCalls.lean index db36e2ca0..828d62d93 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T08_ContractsCalls.lean @@ -45,4 +45,4 @@ procedure caller() { " #guard_msgs(drop info, error) in -#eval! testInputWithOffset "T5_ProcedureCallsStrataCore" program 20 processLaurelFile +#eval! testInputWithOffset "ContractsCalls" program 20 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T09_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T09_ConstrainedTypes.lean new file mode 100644 index 000000000..7e10f500f --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T09_ConstrainedTypes.lean @@ -0,0 +1,30 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util + +namespace Strata +namespace Laurel + +def program := r" +constrained nat = x: int where x >= 0 witness 0 + +procedure double(n: nat) returns (r: nat) + ensures r == n + n +{ + return n + n; +} + +procedure testQuantifier() + ensures forall(n: nat) => n + 1 > 0 +{} +" + +#guard_msgs(drop info, error) in +#eval testInputWithOffset "ConstrainedTypes" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_Arrays.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_Arrays.lean new file mode 100644 index 000000000..86fe3c9c0 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_Arrays.lean @@ -0,0 +1,42 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples +open StrataTest.Util +namespace Strata.Laurel + +def program := r" +procedure getFirst(arr: Array, len: int) returns (r: int) + requires len > 0 +ensures r == arr[0] +{ + return arr[0]; +} + +procedure sumTwo(arr: Array, len: int) returns (r: int) + requires len >= 2 + ensures r == arr[0] + arr[1] +{ + return arr[0] + arr[1]; +} + +// Test passing arrays to other procedures +constrained int32 = x: int where x >= -2147483648 && x <= 2147483647 witness 0 +procedure helper(arr: Array): int32 + requires Array.Length(arr) > 0 +{ return 0; } +procedure callWithArray(arr: Array): int32 + requires Array.Length(arr) > 0 +{ + var x: int32 := helper(arr); + return x; +} +" + +#guard_msgs(drop info, error) in +#eval testInputWithOffset "Arrays" program 5 processLaurelFile + +end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean deleted file mode 100644 index 3ad972ee0..000000000 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean +++ /dev/null @@ -1,30 +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 Laurel - -def program := r" -constrained nat = x: int where x >= 0 witness 0 - -composite Option {} -composite Some extends Option { - value: int -} -composite None extends Option -constrained SealedOption = x: Option where x is Some || x is None witness None - -procedure foo() returns (r: nat) { -} -" - --- Not working yet --- #eval! testInput "ConstrainedTypes" program processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T11_Sequences.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T11_Sequences.lean new file mode 100644 index 000000000..0ba9b7a3f --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T11_Sequences.lean @@ -0,0 +1,32 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples +open StrataTest.Util +namespace Strata.Laurel + +def program := r" +procedure containsTarget(arr: Array, len: int, target: int) returns (r: bool) + requires len >= 0 + ensures r == Seq.Contains(Seq.From(arr), target) +{ + return Seq.Contains(Seq.From(arr), target); +} + +procedure containsInPrefix(arr: Array, len: int, n: int, target: int) returns (r: bool) + requires len >= 0 + requires n >= 0 + requires n <= len + ensures r == Seq.Contains(Seq.Take(Seq.From(arr), n), target) +{ + return Seq.Contains(Seq.Take(Seq.From(arr), n), target); +} +" + +#guard_msgs(drop info, error) in +#eval testInputWithOffset "Sequences" program 5 processLaurelFile + +end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_LoopJumps.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T12_LoopJumps.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_ProcedureCalls.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T13_ProcedureCalls.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Preconditions.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Preconditions.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_Decreases.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T15_Decreases.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_Postconditions.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T16_Postconditions.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_Nondeterministic.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T17_Nondeterministic.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T_11_String.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_String.lean similarity index 100% rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T_11_String.lean rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T18_String.lean diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean index 8cdecd812..536d3ceef 100644 --- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean +++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean @@ -39,12 +39,14 @@ procedure useBool(c: Container) returns (r: bool) { } procedure caller(c: Container, d: Container) { + assume c != d; assume d#intValue == 1; var x: int := foo(c, d); assert d#intValue == 3; } procedure allowHeapMutatingCallerInExpression(c: Container, d: Container) { + assume c != d; assume d#intValue == 1; var x: int := foo(c, d) + 1; assert d#intValue == 3;