From be717f03ef370a5d25f1a50d48064e9c763546f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jul 2024 20:25:02 +0200 Subject: [PATCH] fix: missing assignment validation at `closeMainGoal` (#4777) This primitive is used by the `exact` tactic. This issue allowed users to create loops in the metavariable assignment. closes #4773 --- src/Lean/Elab/Tactic/Basic.lean | 16 ++++++++++++---- src/Lean/Elab/Tactic/ElabTerm.lean | 21 +++++++++++---------- src/Lean/Meta/Basic.lean | 10 +++++++--- src/Lean/Meta/ExprDefEq.lean | 9 +++++++++ tests/lean/run/2243.lean | 2 +- tests/lean/run/4773.lean | 11 +++++++++++ 6 files changed, 51 insertions(+), 18 deletions(-) create mode 100644 tests/lean/run/4773.lean diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 4b4f59d8bb..b6798e9ea6 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude +import Lean.Meta.Tactic.Util import Lean.Elab.Term namespace Lean.Elab @@ -398,12 +399,19 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do if e.hasExprMVar then throwError "tactic failed, resulting expression contains metavariables{indentExpr e}" -/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/ -def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do +/-- +Closes main goal using the given expression. +If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. +Returns `true` if `val` was successfully used to close the goal. +-/ +def closeMainGoal (tacName : Name) (val : Expr) (checkUnassigned := true): TacticM Unit := do if checkUnassigned then ensureHasNoMVars val - (← getMainGoal).assign val - replaceMainGoal [] + let mvarId ← getMainGoal + if (← mvarId.checkedAssign val) then + replaceMainGoal [] + else + throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure" @[inline] def liftMetaMAtMain (x : MVarId → MetaM α) : TacticM α := do withMainContext do x (← getMainGoal) diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 52ec86459b..ca9eae6138 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -56,9 +56,9 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo return e /-- Try to close main goal using `x target`, where `target` is the type of the main goal. -/ -def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit := +def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit := withMainContext do - closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget)) + closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget)) def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do if (← Term.logUnassignedUsingErrorInfos mvarIds) then @@ -68,13 +68,14 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar let mctx ← getMCtx return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved -@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => +@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do match stx with - | `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do - let mvarCounterSaved := (← getMCtx).mvarCounter - let r ← elabTermEnsuringType e type - logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved) - return r + | `(tactic| exact $e) => + closeMainGoalUsing `exact (checkUnassigned := false) fun type => do + let mvarCounterSaved := (← getMCtx).mvarCounter + let r ← elabTermEnsuringType e type + logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved) + return r | _ => throwUnsupportedSyntax def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do @@ -393,7 +394,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do return inst @[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ => - closeMainGoalUsing fun expectedType => do + closeMainGoalUsing `decide fun expectedType => do let expectedType ← preprocessPropToDecide expectedType let d ← mkDecide expectedType let d ← instantiateMVars d @@ -472,7 +473,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na pure auxName @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ => - closeMainGoalUsing fun expectedType => do + closeMainGoalUsing `nativeDecide fun expectedType => do let expectedType ← preprocessPropToDecide expectedType let d ← mkDecide expectedType let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 6df729bd87..51d55d9929 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1865,9 +1865,13 @@ abbrev isDefEqGuarded (t s : Expr) : MetaM Bool := def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool := approxDefEq <| isDefEq t s -/-- Shorthand for `isDefEq (mkMVar mvarId) val` -/ -def _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool := - isDefEq (mkMVar mvarId) val +/-- +Returns `true` if `mvarId := val` was successfully assigned. +This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match. +-/ +-- Remark: this method is implemented at `ExprDefEq` +@[extern "lean_checked_assign"] +opaque _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool /-- Eta expand the given expression. diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index f6935eea7d..b79df57879 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1046,6 +1046,15 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O return none return some v +-- Implementation for `_root_.Lean.MVarId.checkedAssign` +@[export lean_checked_assign] +def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do + if let some val ← checkAssignment mvarId #[] val then + mvarId.assign val + return true + else + return false + private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool := match v with | .mdata _ e => processAssignmentFOApproxAux mvar args e diff --git a/tests/lean/run/2243.lean b/tests/lean/run/2243.lean index 893e482a8f..35dcaef322 100644 --- a/tests/lean/run/2243.lean +++ b/tests/lean/run/2243.lean @@ -2,7 +2,7 @@ import Lean open Lean Elab Tactic in elab "exact_false" : tactic => - closeMainGoal (mkConst ``Bool.false) + closeMainGoal `exact_false (mkConst ``Bool.false) def f (b : Bool := by exact_false) : Nat := bif b then 1 else 0 diff --git a/tests/lean/run/4773.lean b/tests/lean/run/4773.lean new file mode 100644 index 0000000000..fcc334ae21 --- /dev/null +++ b/tests/lean/run/4773.lean @@ -0,0 +1,11 @@ +/-- +error: tactic 'exact' failed, attempting to close the goal using + ?loop +this is often due occurs-check failure +case loop +⊢ False +-/ +#guard_msgs in +example : False := by + refine ?loop + exact ?loop