From e183dff7c7d24ae71865434e6659d9c8e966c6de Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 19 Jan 2026 17:37:24 -0600 Subject: [PATCH 1/4] Add check for bad usage of return vars in requires clauses of procedures --- Strata/Languages/Core/Procedure.lean | 6 +++ Strata/Languages/Core/ProcedureType.lean | 65 ++++++++++++++---------- 2 files changed, 45 insertions(+), 26 deletions(-) diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index e1fd6bf4..fb73e8b7 100644 --- a/Strata/Languages/Core/Procedure.lean +++ b/Strata/Languages/Core/Procedure.lean @@ -103,6 +103,12 @@ instance : ToFormat Procedure.Spec where preconditions: {format p.preconditions}\n\ postconditions: {format p.postconditions}" +def Procedure.Spec.preconditionNames (s : Procedure.Spec) : List CoreLabel := + s.preconditions.map (fun (n, _) => n) + +def Procedure.Spec.postconditionNames (s : Procedure.Spec) : List CoreLabel := + s.postconditions.map (fun (n, _) => n) + def Procedure.Spec.eraseTypes (s : Procedure.Spec) : Procedure.Spec := { s with preconditions := s.preconditions.map (fun (l, c) => (l, c.eraseTypes)), diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean index 4e1a9495..a391be67 100644 --- a/Strata/Languages/Core/ProcedureType.lean +++ b/Strata/Languages/Core/ProcedureType.lean @@ -60,45 +60,58 @@ def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Modification allowed for these variables: {allowedVars}" else let preconditions := Procedure.Spec.getCheckExprs proc.spec.preconditions + dbg_trace f!"MetaData: {proc.spec.preconditions.values.map (fun v => v.md)}" if preconditions.any (fun p => OldExpressions.containsOldExpr p) then .error f!"{sourceLoc}[{proc.header.name}]: Preconditions cannot contain applications of\ the `old` function!" else - -- 1. Temporarily add the formals and returns into the context. + -- 1. Temporarily add the formals into the context. let Env := Env.pushEmptyContext - let (mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs - (proc.header.inputs ++ proc.header.outputs) + let (inp_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs + proc.header.inputs |>.mapError errorWithSourceLoc - let lty_sig := Lambda.LMonoTySignature.toTrivialLTy mty_sig + let lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig let Env := Env.addToContext lty_sig - -- 2. Normalize the old expressions in the postconditions. The evaluator - -- depends on this step! See also note in `OldExpressions.lean`. - let postcondition_checks := OldExpressions.normalizeOldChecks proc.spec.postconditions - -- 3. Ensure that the preconditions and postconditions are of type boolean. - let postconditions := postcondition_checks.map (fun (_, c) => c.expr) + -- 2. Type check preconditions under `Env` -- note: `Env` does not have + -- the return variables in the context, which means that the presence + -- of any return variables in the preconditions will flag an error. let (preconditions_a, Env) ← Lambda.LExpr.resolves C Env preconditions |>.mapError errorWithSourceLoc let pre_tys := preconditions_a.map Lambda.LExpr.toLMonoTy let preconditions := preconditions_a.map Lambda.LExpr.unresolved + for (pre, ty) in proc.spec.preconditionNames.zip pre_tys do + if ty != .tcons "bool" [] then + .error f!"{sourceLoc}[{proc.header.name}]: Expected precondition {pre} to be of type Bool, but got {ty}!" + -- 3. Normalize the old expressions in the postconditions. The evaluator + -- depends on this step! See also note in `OldExpressions.lean`. + let postcondition_checks := OldExpressions.normalizeOldChecks proc.spec.postconditions + -- 4. Type check postconditions, after adding returns to `Env`. + let (out_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs + proc.header.outputs + |>.mapError errorWithSourceLoc + let lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig + let Env := Env.addToContext lty_sig + let postconditions := postcondition_checks.map (fun (_, c) => c.expr) let (postconditions_a, Env) ← Lambda.LExpr.resolves C Env postconditions |>.mapError errorWithSourceLoc let post_tys := postconditions_a.map Lambda.LExpr.toLMonoTy let postconditions := postconditions_a.map Lambda.LExpr.unresolved - if (pre_tys ++ post_tys).any (fun ty => ty != .tcons "bool" []) then - .error f!"{sourceLoc}[{proc.header.name}]: Expected pre- and post-conditions to be of type Bool!" - else - -- 4. Typecheck the body of the procedure. - -- Note that `Statement.typeCheck` already reports source locations in - -- error messages. - let (annotated_body, Env) ← Statement.typeCheck C Env p (.some proc) proc.body - -- Remove formals and returns from the context. - let Env := Env.popContext - let preconditions := Procedure.Spec.updateCheckExprs preconditions proc.spec.preconditions - let postconditions := Procedure.Spec.updateCheckExprs postconditions proc.spec.postconditions - let new_hdr := { proc.header with typeArgs := [], - inputs := mty_sig.take proc.header.inputs.length, - outputs := mty_sig.drop proc.header.inputs.length } - let new_spec := { proc.spec with preconditions := preconditions, postconditions := postconditions } - let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } - .ok (new_proc, Env) + for (post, ty) in proc.spec.postconditionNames.zip post_tys do + if ty != .tcons "bool" [] then + .error f!"{sourceLoc}[{proc.header.name}]: Expected postcondition {post} to be of type Bool, but got {ty}!" + -- 5. Typecheck the body of the procedure. + -- Note that `Statement.typeCheck` already reports source locations in + -- error messages. + let (annotated_body, Env) ← Statement.typeCheck C Env p (.some proc) proc.body + -- 6. Remove formals and returns from the `Env`. + let Env := Env.popContext + let preconditions := Procedure.Spec.updateCheckExprs preconditions proc.spec.preconditions + let postconditions := Procedure.Spec.updateCheckExprs postconditions proc.spec.postconditions + -- Type arguments are empty below because we've replaced polytypes with monotypes. + let new_hdr := { proc.header with typeArgs := [], + inputs := inp_mty_sig, + outputs := out_mty_sig } + let new_spec := { proc.spec with preconditions := preconditions, postconditions := postconditions } + let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } + .ok (new_proc, Env) --------------------------------------------------------------------- end Procedure From f66b7e574bb5e8e75bfffc2553ab707c546a44cf Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 19 Jan 2026 18:37:56 -0600 Subject: [PATCH 2/4] Finer-grained error reporting --- Strata/DL/Imperative/MetaData.lean | 6 +- Strata/Languages/Core/Procedure.lean | 4 +- Strata/Languages/Core/ProcedureType.lean | 81 +++++++++++++++--------- 3 files changed, 56 insertions(+), 35 deletions(-) diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean index 71e2fc5a..e8a143d5 100644 --- a/Strata/DL/Imperative/MetaData.lean +++ b/Strata/DL/Imperative/MetaData.lean @@ -201,11 +201,11 @@ def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : | .file path => (path.splitToList (· == '/')).getLast! if includeEnd? then if m.start.line == m.ending.line then - return f!"{baseName}({m.start.line}, ({m.start.column}-{m.ending.column}))" + return f!"{baseName}:{m.start.line}:{m.start.column}-{m.ending.column}" else - return f!"{baseName}(({m.start.line}, {m.start.column})-({m.ending.line}, {m.ending.column}))" + return f!"{baseName}:{m.start.line}:{m.start.column}-{m.ending.line}:{m.ending.column}" else -- don't include the end position. - return f!"{baseName}({m.start.line}, {m.start.column})" + return f!"{baseName}:{m.start.line}:{m.start.column}" | _ => none def MetaData.formatFileRangeD {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : Bool := false) diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index fb73e8b7..f84aa1b4 100644 --- a/Strata/Languages/Core/Procedure.lean +++ b/Strata/Languages/Core/Procedure.lean @@ -104,10 +104,10 @@ instance : ToFormat Procedure.Spec where postconditions: {format p.postconditions}" def Procedure.Spec.preconditionNames (s : Procedure.Spec) : List CoreLabel := - s.preconditions.map (fun (n, _) => n) + s.preconditions.keys def Procedure.Spec.postconditionNames (s : Procedure.Spec) : List CoreLabel := - s.postconditions.map (fun (n, _) => n) + s.postconditions.keys def Procedure.Spec.eraseTypes (s : Procedure.Spec) : Procedure.Spec := { s with diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean index a391be67..7010308e 100644 --- a/Strata/Languages/Core/ProcedureType.lean +++ b/Strata/Languages/Core/ProcedureType.lean @@ -20,6 +20,24 @@ open Imperative (MetaData) namespace Procedure +-- Error message prefix for errors in processing procedure pre/post conditions. +def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel) + (md : MetaData Expression) : Format := + let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := true) + f!"{sourceLoc} [{procName}:{condName}]:" + +open Lambda.LTy.Syntax in +-- Type checking procedure pre/post conditions. +def conditionTypeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) + (expr : Expression.Expr) (errorMsgPrefix : Format) : + Except Format (Expression.Expr × Core.Expression.TyEnv) := do + let (condAnnotated, newEnv) ← Lambda.LExpr.resolve C Env expr + |>.mapError (fun e => f!"{errorMsgPrefix} {e}") + if condAnnotated.toLMonoTy != mty[bool] then + .error f!"{errorMsgPrefix}: Expected condition to be of type Bool,\ + but got {condAnnotated.toLMonoTy}!" + return (condAnnotated.unresolved, newEnv) + def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Program) (proc : Procedure) (md : MetaData Expression) : Except Format (Procedure × Core.Expression.TyEnv) := let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := false) @@ -59,57 +77,60 @@ def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Variables actually modified: {modifiedVars}\n\ Modification allowed for these variables: {allowedVars}" else - let preconditions := Procedure.Spec.getCheckExprs proc.spec.preconditions - dbg_trace f!"MetaData: {proc.spec.preconditions.values.map (fun v => v.md)}" - if preconditions.any (fun p => OldExpressions.containsOldExpr p) then - .error f!"{sourceLoc}[{proc.header.name}]: Preconditions cannot contain applications of\ - the `old` function!" - else -- 1. Temporarily add the formals into the context. let Env := Env.pushEmptyContext let (inp_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs proc.header.inputs |>.mapError errorWithSourceLoc - let lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig - let Env := Env.addToContext lty_sig + let inp_lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig + let Env := Env.addToContext inp_lty_sig -- 2. Type check preconditions under `Env` -- note: `Env` does not have -- the return variables in the context, which means that the presence -- of any return variables in the preconditions will flag an error. - let (preconditions_a, Env) ← Lambda.LExpr.resolves C Env preconditions |>.mapError errorWithSourceLoc - let pre_tys := preconditions_a.map Lambda.LExpr.toLMonoTy - let preconditions := preconditions_a.map Lambda.LExpr.unresolved - for (pre, ty) in proc.spec.preconditionNames.zip pre_tys do - if ty != .tcons "bool" [] then - .error f!"{sourceLoc}[{proc.header.name}]: Expected precondition {pre} to be of type Bool, but got {ty}!" - -- 3. Normalize the old expressions in the postconditions. The evaluator - -- depends on this step! See also note in `OldExpressions.lean`. - let postcondition_checks := OldExpressions.normalizeOldChecks proc.spec.postconditions - -- 4. Type check postconditions, after adding returns to `Env`. + let mut preconditions := (#[] : Array Expression.Expr) + let mut precondEnv := Env + for (name, precond) in (proc.spec.preconditions.keys, proc.spec.preconditions.values) do + let precondErrorMsgPfx := conditionErrorMsgPrefix proc.header.name name precond.md + if OldExpressions.containsOldExpr precond.expr then + .error f!"{precondErrorMsgPfx} Preconditions cannot contain applications of \ + the `old` function!" + let (precond, newEnv) ← conditionTypeCheck C precondEnv precond.expr precondErrorMsgPfx + preconditions := preconditions.push precond + precondEnv := newEnv + -- End of for loop. + -- 3. Temporarily add the returns into the context. + let Env := precondEnv let (out_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs proc.header.outputs |>.mapError errorWithSourceLoc - let lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig - let Env := Env.addToContext lty_sig - let postconditions := postcondition_checks.map (fun (_, c) => c.expr) - let (postconditions_a, Env) ← Lambda.LExpr.resolves C Env postconditions |>.mapError errorWithSourceLoc - let post_tys := postconditions_a.map Lambda.LExpr.toLMonoTy - let postconditions := postconditions_a.map Lambda.LExpr.unresolved - for (post, ty) in proc.spec.postconditionNames.zip post_tys do - if ty != .tcons "bool" [] then - .error f!"{sourceLoc}[{proc.header.name}]: Expected postcondition {post} to be of type Bool, but got {ty}!" + let out_lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig + let Env := Env.addToContext out_lty_sig + -- 4. Type check postconditions. + let mut postconditions := (#[] : Array Expression.Expr) + let mut postcondEnv := Env + for (name, postcond) in (proc.spec.postconditions.keys, proc.spec.postconditions.values) do + -- Normalize the old expressions in the postconditions. The evaluator + -- depends on this step! See also note in `OldExpressions.lean`. + let postcondNormalizedExpr := OldExpressions.normalizeOldExpr postcond.expr + let postcondErrorMsgPfx := conditionErrorMsgPrefix proc.header.name name postcond.md + let (postcond, newEnv) ← conditionTypeCheck C postcondEnv postcondNormalizedExpr postcondErrorMsgPfx + postconditions := postconditions.push postcond + postcondEnv := newEnv + -- End of for loop. + let Env := postcondEnv -- 5. Typecheck the body of the procedure. -- Note that `Statement.typeCheck` already reports source locations in -- error messages. let (annotated_body, Env) ← Statement.typeCheck C Env p (.some proc) proc.body -- 6. Remove formals and returns from the `Env`. let Env := Env.popContext - let preconditions := Procedure.Spec.updateCheckExprs preconditions proc.spec.preconditions - let postconditions := Procedure.Spec.updateCheckExprs postconditions proc.spec.postconditions + let finalPreconds := Procedure.Spec.updateCheckExprs preconditions.toList proc.spec.preconditions + let finalPostConds := Procedure.Spec.updateCheckExprs postconditions.toList proc.spec.postconditions -- Type arguments are empty below because we've replaced polytypes with monotypes. let new_hdr := { proc.header with typeArgs := [], inputs := inp_mty_sig, outputs := out_mty_sig } - let new_spec := { proc.spec with preconditions := preconditions, postconditions := postconditions } + let new_spec := { proc.spec with preconditions := finalPreconds, postconditions := finalPostConds } let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } .ok (new_proc, Env) From fc4c48292c698914e3dcfc86e54abf169019802e Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 19 Jan 2026 20:32:37 -0600 Subject: [PATCH 3/4] Clean up Procedure type checking code; add a test showing source locations when a precondition type error is encountered --- Examples/ProcedureTypeError.core.st | 9 + .../expected/ProcedureTypeError.core.expected | 3 + Strata/DL/Imperative/MetaData.lean | 6 +- Strata/Languages/Core/ProcedureType.lean | 230 ++++++++++-------- 4 files changed, 144 insertions(+), 104 deletions(-) create mode 100644 Examples/ProcedureTypeError.core.st create mode 100644 Examples/expected/ProcedureTypeError.core.expected diff --git a/Examples/ProcedureTypeError.core.st b/Examples/ProcedureTypeError.core.st new file mode 100644 index 00000000..c90c8303 --- /dev/null +++ b/Examples/ProcedureTypeError.core.st @@ -0,0 +1,9 @@ +program Core; +procedure SumPositive(a: int, b: int) returns (c: int) +spec { + requires [precond1]: 0 <= a; + requires [precond2]: c <= b; +} +{ + c := a + b; +}; \ No newline at end of file diff --git a/Examples/expected/ProcedureTypeError.core.expected b/Examples/expected/ProcedureTypeError.core.expected new file mode 100644 index 00000000..06622654 --- /dev/null +++ b/Examples/expected/ProcedureTypeError.core.expected @@ -0,0 +1,3 @@ +Successfully parsed. +❌ Type checking error. +ProcedureTypeError.core.st(5, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean index e8a143d5..71e2fc5a 100644 --- a/Strata/DL/Imperative/MetaData.lean +++ b/Strata/DL/Imperative/MetaData.lean @@ -201,11 +201,11 @@ def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : | .file path => (path.splitToList (· == '/')).getLast! if includeEnd? then if m.start.line == m.ending.line then - return f!"{baseName}:{m.start.line}:{m.start.column}-{m.ending.column}" + return f!"{baseName}({m.start.line}, ({m.start.column}-{m.ending.column}))" else - return f!"{baseName}:{m.start.line}:{m.start.column}-{m.ending.line}:{m.ending.column}" + return f!"{baseName}(({m.start.line}, {m.start.column})-({m.ending.line}, {m.ending.column}))" else -- don't include the end position. - return f!"{baseName}:{m.start.line}:{m.start.column}" + return f!"{baseName}({m.start.line}, {m.start.column})" | _ => none def MetaData.formatFileRangeD {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : Bool := false) diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean index 7010308e..4cd2df30 100644 --- a/Strata/Languages/Core/ProcedureType.lean +++ b/Strata/Languages/Core/ProcedureType.lean @@ -20,120 +20,148 @@ open Imperative (MetaData) namespace Procedure --- Error message prefix for errors in processing procedure pre/post conditions. -def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel) - (md : MetaData Expression) : Format := - let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := true) - f!"{sourceLoc} [{procName}:{condName}]:" - -open Lambda.LTy.Syntax in --- Type checking procedure pre/post conditions. -def conditionTypeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) - (expr : Expression.Expr) (errorMsgPrefix : Format) : - Except Format (Expression.Expr × Core.Expression.TyEnv) := do - let (condAnnotated, newEnv) ← Lambda.LExpr.resolve C Env expr - |>.mapError (fun e => f!"{errorMsgPrefix} {e}") - if condAnnotated.toLMonoTy != mty[bool] then - .error f!"{errorMsgPrefix}: Expected condition to be of type Bool,\ - but got {condAnnotated.toLMonoTy}!" - return (condAnnotated.unresolved, newEnv) - -def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Program) - (proc : Procedure) (md : MetaData Expression) : Except Format (Procedure × Core.Expression.TyEnv) := - let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := false) - let sourceLoc := if sourceLoc.isEmpty then sourceLoc else f!"{sourceLoc} " - let errorWithSourceLoc := fun e => if sourceLoc.isEmpty then e else f!"{sourceLoc} {e}" +private def checkNoDuplicates (proc : Procedure) (sourceLoc : Format) : + Except Format Unit := do if !proc.header.inputs.keys.Nodup then .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the formals!" - else if !proc.header.outputs.keys.Nodup then + if !proc.header.outputs.keys.Nodup then .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the return variables!" - else if !proc.spec.modifies.Nodup then + if !proc.spec.modifies.Nodup then .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the modifies clause!" - else if proc.spec.modifies.any (fun v => v ∈ proc.header.inputs.keys) then + +private def checkVariableScoping (proc : Procedure) (sourceLoc : Format) : + Except Format Unit := do + if proc.spec.modifies.any (fun v => v ∈ proc.header.inputs.keys) then .error f!"{sourceLoc}[{proc.header.name}] Variables in the modifies clause must \ not appear in the formals.\n\ - Modifies: {proc.spec.modifies}\n + Modifies: {proc.spec.modifies}\n\ Formals: {proc.header.inputs.keys}" - else if proc.spec.modifies.any (fun v => v ∈ proc.header.outputs.keys) then + if proc.spec.modifies.any (fun v => v ∈ proc.header.outputs.keys) then .error f!"{sourceLoc}[{proc.header.name}] Variables in the modifies clause must \ not appear in the return values.\n\ - Modifies: {proc.spec.modifies}\n + Modifies: {proc.spec.modifies}\n\ Returns: {proc.header.outputs.keys}" - else if proc.header.inputs.keys.any (fun v => v ∈ proc.header.outputs.keys) then - .error f!"{sourceLoc}[{proc.header.name}] Variables in the formals must not appear \ - in the return values.\n\ - Formals: {proc.header.inputs.keys}\n + if proc.header.inputs.keys.any (fun v => v ∈ proc.header.outputs.keys) then + .error f!"{sourceLoc}[{proc.header.name}] Variables in the formals must \ + not appear in the return values.\n\ + Formals: {proc.header.inputs.keys}\n\ Returns: {proc.header.outputs.keys}" - else if proc.spec.modifies.any (fun v => (Env.context.types.find? v).isNone) then - .error f!"{sourceLoc}[{proc.header.name}]: All the variables in the modifies \ - clause must exist in the context! \ + +private def checkModifiesClause (proc : Procedure) (Env : Core.Expression.TyEnv) + (sourceLoc : Format) : Except Format Unit := do + if proc.spec.modifies.any (fun v => (Env.context.types.find? v).isNone) then + .error f!"{sourceLoc}[{proc.header.name}]: All the variables in the modifies clause \ + must exist in the context!\n\ Modifies: {proc.spec.modifies}" - else do - let modifiedVars := (Imperative.Block.modifiedVars proc.body).eraseDups - let definedVars := (Imperative.Block.definedVars proc.body).eraseDups - let allowedVars := proc.header.outputs.keys ++ proc.spec.modifies ++ definedVars - if modifiedVars.any (fun v => v ∉ allowedVars) then - .error f!"{sourceLoc}[{proc.header.name}]: This procedure modifies variables it is not allowed to!\n\ - Variables actually modified: {modifiedVars}\n\ - Modification allowed for these variables: {allowedVars}" - else - -- 1. Temporarily add the formals into the context. - let Env := Env.pushEmptyContext - let (inp_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs - proc.header.inputs - |>.mapError errorWithSourceLoc - let inp_lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig - let Env := Env.addToContext inp_lty_sig - -- 2. Type check preconditions under `Env` -- note: `Env` does not have - -- the return variables in the context, which means that the presence - -- of any return variables in the preconditions will flag an error. - let mut preconditions := (#[] : Array Expression.Expr) - let mut precondEnv := Env - for (name, precond) in (proc.spec.preconditions.keys, proc.spec.preconditions.values) do - let precondErrorMsgPfx := conditionErrorMsgPrefix proc.header.name name precond.md - if OldExpressions.containsOldExpr precond.expr then - .error f!"{precondErrorMsgPfx} Preconditions cannot contain applications of \ - the `old` function!" - let (precond, newEnv) ← conditionTypeCheck C precondEnv precond.expr precondErrorMsgPfx - preconditions := preconditions.push precond - precondEnv := newEnv - -- End of for loop. - -- 3. Temporarily add the returns into the context. - let Env := precondEnv - let (out_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs - proc.header.outputs - |>.mapError errorWithSourceLoc - let out_lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig - let Env := Env.addToContext out_lty_sig - -- 4. Type check postconditions. - let mut postconditions := (#[] : Array Expression.Expr) - let mut postcondEnv := Env - for (name, postcond) in (proc.spec.postconditions.keys, proc.spec.postconditions.values) do - -- Normalize the old expressions in the postconditions. The evaluator - -- depends on this step! See also note in `OldExpressions.lean`. - let postcondNormalizedExpr := OldExpressions.normalizeOldExpr postcond.expr - let postcondErrorMsgPfx := conditionErrorMsgPrefix proc.header.name name postcond.md - let (postcond, newEnv) ← conditionTypeCheck C postcondEnv postcondNormalizedExpr postcondErrorMsgPfx - postconditions := postconditions.push postcond - postcondEnv := newEnv - -- End of for loop. - let Env := postcondEnv - -- 5. Typecheck the body of the procedure. - -- Note that `Statement.typeCheck` already reports source locations in - -- error messages. - let (annotated_body, Env) ← Statement.typeCheck C Env p (.some proc) proc.body - -- 6. Remove formals and returns from the `Env`. - let Env := Env.popContext - let finalPreconds := Procedure.Spec.updateCheckExprs preconditions.toList proc.spec.preconditions - let finalPostConds := Procedure.Spec.updateCheckExprs postconditions.toList proc.spec.postconditions - -- Type arguments are empty below because we've replaced polytypes with monotypes. - let new_hdr := { proc.header with typeArgs := [], - inputs := inp_mty_sig, - outputs := out_mty_sig } - let new_spec := { proc.spec with preconditions := finalPreconds, postconditions := finalPostConds } - let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } - .ok (new_proc, Env) + +private def checkModificationRights (proc : Procedure) (sourceLoc : Format) : + Except Format Unit := do + let modifiedVars := (Imperative.Block.modifiedVars proc.body).eraseDups + let definedVars := (Imperative.Block.definedVars proc.body).eraseDups + let allowedVars := proc.header.outputs.keys ++ proc.spec.modifies ++ definedVars + if modifiedVars.any (fun v => v ∉ allowedVars) then + .error f!"{sourceLoc}[{proc.header.name}]: This procedure modifies variables it \ + is not allowed to!\n\ + Variables actually modified: {modifiedVars}\n\ + Modification allowed for these variables: {allowedVars}" + +private def setupInputEnv (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) + (proc : Procedure) (errorWithSourceLoc : Format → Format) : + Except Format (@Lambda.LMonoTySignature Visibility × Core.Expression.TyEnv) := do + let Env := Env.pushEmptyContext + let (inp_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs + proc.header.inputs |>.mapError errorWithSourceLoc + let inp_lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig + let Env := Env.addToContext inp_lty_sig + return (inp_mty_sig, Env) + +-- Error message prefix for errors in processing procedure pre/post conditions. +def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel) + (md : MetaData Expression) : Format := + let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := true) + f!"{sourceLoc} [{procName}:{condName}]:" + +-- Type checking procedure pre/post conditions. +-- We flag occurrences of `old` expressions in the preconditions and normalize +-- them in the postconditions. +open Lambda.LTy.Syntax in +private def typeCheckConditions (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) + (conditions : ListMap CoreLabel Check) (procName : CoreIdent) (checkOldExprs : Bool) : + Except Format (Array Expression.Expr × Core.Expression.TyEnv) := do + let mut results := #[] + let mut currentEnv := Env + for (name, condition) in (conditions.keys, conditions.values) do + let errorPrefix := conditionErrorMsgPrefix procName name condition.md + if checkOldExprs && OldExpressions.containsOldExpr condition.expr then + .error f!"{errorPrefix} Preconditions cannot contain applications of the `old` function!" + let expr := if checkOldExprs then condition.expr else OldExpressions.normalizeOldExpr condition.expr + let (annotatedExpr, newEnv) ← Lambda.LExpr.resolve C currentEnv expr + |>.mapError (fun e => f!"{errorPrefix} {e}") + if annotatedExpr.toLMonoTy != mty[bool] then + .error f!"{errorPrefix}: Expected condition to be of type Bool,\ + but got {annotatedExpr.toLMonoTy}!" + results := results.push annotatedExpr.unresolved + currentEnv := newEnv + return (results, currentEnv) + +def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Program) + (proc : Procedure) (md : MetaData Expression) : Except Format (Procedure × Core.Expression.TyEnv) := do + let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := false) + let sourceLoc := if sourceLoc.isEmpty then sourceLoc else f!"{sourceLoc} " + let errorWithSourceLoc := fun e => if sourceLoc.isEmpty then e else f!"{sourceLoc} {e}" + + -- Validate well-formedness of formals, returns, and modifies clause. + checkNoDuplicates proc sourceLoc + checkVariableScoping proc sourceLoc + checkModifiesClause proc Env sourceLoc + checkModificationRights proc sourceLoc + + -- Temporarily add the formals into the context. + let (inp_mty_sig, envWithInputs) ← setupInputEnv C Env proc errorWithSourceLoc + + -- Type check preconditions. + -- Note: `envWithInputs` does not have the return variables in the context, + -- which means that the presence of any return variables in the preconditions + -- will rightfully flag an error. + let (preconditions, envAfterPreconds) ← typeCheckConditions C envWithInputs + proc.spec.preconditions proc.header.name + (checkOldExprs := true) + + -- Temporarily add returns into the context. + let (out_mty_sig, envWithOutputs) ← Lambda.LMonoTySignature.instantiate C + envAfterPreconds proc.header.typeArgs + proc.header.outputs |>.mapError errorWithSourceLoc + let out_lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig + let envWithOutputs := envWithOutputs.addToContext out_lty_sig + + -- Type check postconditions. + let (postconditions, envAfterPostconds) ← typeCheckConditions C envWithOutputs + proc.spec.postconditions proc.header.name + (checkOldExprs := false) + + -- Type check body. + -- Note that `Statement.typeCheck` already reports source locations in + -- error messages. + let (annotated_body, finalEnv) ← Statement.typeCheck C envAfterPostconds p (.some proc) proc.body + + -- Remove formals and returns from the context -- they ought to be local to + -- the procedure body. + let finalEnv := finalEnv.popContext + + -- Construct final result. + let finalPreconditions := Procedure.Spec.updateCheckExprs preconditions.toList proc.spec.preconditions + let finalPostconditions := Procedure.Spec.updateCheckExprs postconditions.toList proc.spec.postconditions + -- Type arguments are empty below because we've replaced polytypes with monotypes. + let new_hdr := { proc.header with typeArgs := [], + inputs := inp_mty_sig, + outputs := out_mty_sig } + let new_spec := { proc.spec with preconditions := finalPreconditions, + postconditions := finalPostconditions } + let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } + + return (new_proc, finalEnv) --------------------------------------------------------------------- + end Procedure end Core From 6d925fd12c9b5eb179b8a71fd8ebc3ee293631ee Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 19 Jan 2026 20:56:06 -0600 Subject: [PATCH 4/4] Add copyright header --- Examples/ProcedureTypeError.core.st | 16 ++++++++++++++++ .../expected/ProcedureTypeError.core.expected | 2 +- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Examples/ProcedureTypeError.core.st b/Examples/ProcedureTypeError.core.st index c90c8303..a79e3c06 100644 --- a/Examples/ProcedureTypeError.core.st +++ b/Examples/ProcedureTypeError.core.st @@ -1,4 +1,20 @@ program Core; +// +// Copyright Strata Contributors +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + procedure SumPositive(a: int, b: int) returns (c: int) spec { requires [precond1]: 0 <= a; diff --git a/Examples/expected/ProcedureTypeError.core.expected b/Examples/expected/ProcedureTypeError.core.expected index 06622654..c819c196 100644 --- a/Examples/expected/ProcedureTypeError.core.expected +++ b/Examples/expected/ProcedureTypeError.core.expected @@ -1,3 +1,3 @@ Successfully parsed. ❌ Type checking error. -ProcedureTypeError.core.st(5, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c +ProcedureTypeError.core.st(21, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c