diff --git a/Examples/ProcedureTypeError.core.st b/Examples/ProcedureTypeError.core.st new file mode 100644 index 00000000..a79e3c06 --- /dev/null +++ b/Examples/ProcedureTypeError.core.st @@ -0,0 +1,25 @@ +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; + 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..c819c196 --- /dev/null +++ b/Examples/expected/ProcedureTypeError.core.expected @@ -0,0 +1,3 @@ +Successfully parsed. +❌ Type checking error. +ProcedureTypeError.core.st(21, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index e1fd6bf4..f84aa1b4 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.keys + +def Procedure.Spec.postconditionNames (s : Procedure.Spec) : List CoreLabel := + s.postconditions.keys + 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..4cd2df30 100644 --- a/Strata/Languages/Core/ProcedureType.lean +++ b/Strata/Languages/Core/ProcedureType.lean @@ -20,86 +20,148 @@ open Imperative (MetaData) namespace Procedure -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 - let preconditions := Procedure.Spec.getCheckExprs proc.spec.preconditions - 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. - let Env := Env.pushEmptyContext - let (mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs - (proc.header.inputs ++ proc.header.outputs) - |>.mapError errorWithSourceLoc - let lty_sig := Lambda.LMonoTySignature.toTrivialLTy 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) - 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 - 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) + +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