feat: catch deep recursion at MetaM, TermElabM and CommandElabM

cc @Kha

src/Init/Lean/Elab/Command.lean

@@ -30,16 +30,18 @@ structure State :=
 (messages       : MessageLog := {})
 (scopes         : List Scope := [{ kind := "root", header := "" }])
 (nextMacroScope : Nat := 1)
+(maxRecDepth    : Nat)
 
-instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
+instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _, maxRecDepth := 0 }⟩
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State :=
-{ env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }] }
+{ env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }], maxRecDepth := getMaxRecDepth opts }
 
 structure Context :=
 (fileName       : String)
 (fileMap        : FileMap)
 (stateRef       : IO.Ref State)
+(currRecDepth   : Nat := 0)
 (cmdPos         : String.Pos := 0)
 (macroStack     : List Syntax := [])
 (currMacroScope : MacroScope := 0)
@@ -180,6 +182,11 @@ def mkCommandElabAttribute : IO CommandElabAttribute :=
 mkElabAttribute CommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" builtinCommandElabTable
 @[init mkCommandElabAttribute] constant commandElabAttribute : CommandElabAttribute := arbitrary _
 
+@[inline] def withIncRecDepth {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
+ctx ← read; s ← get;
+when (ctx.currRecDepth == s.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
+adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
+
 private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM Unit
 | []                => do
   refFmt ← prettyPrint stx;
@@ -190,7 +197,7 @@ private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM
     | Exception.unsupportedSyntax => elabCommandUsing elabFns)
 
 def elabCommand (stx : Syntax) : CommandElabM Unit :=
-match stx with
+withIncRecDepth stx $ match stx with
 | Syntax.node _ _ => do
   s ← get;
   let table := (commandElabAttribute.ext.getState s.env).table;
@@ -215,6 +222,8 @@ let scope := s.scopes.head!;
 { config         := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
   fileName       := ctx.fileName,
   fileMap        := ctx.fileMap,
+  currRecDepth   := ctx.currRecDepth,
+  maxRecDepth    := s.maxRecDepth,
   cmdPos         := ctx.cmdPos,
   declName?      := declName?,
   macroStack     := ctx.macroStack,
@@ -520,8 +529,10 @@ fun stx => do
 def setOption (ref : Syntax) (optionName : Name) (val : DataValue) : CommandElabM Unit := do
 decl ← liftIO ref $ getOptionDecl optionName;
 unless (decl.defValue.sameCtor val) $ throwError ref "type mismatch at set_option";
-modifyScope $ fun scope => { opts := scope.opts.insert optionName val, .. scope }
-
+modifyScope $ fun scope => { opts := scope.opts.insert optionName val, .. scope };
+match optionName, val with
+| `maxRecDepth, DataValue.ofNat max => modify $ fun s => { maxRecDepth := max, .. s}
+| _,            _                   => pure ()
 
 @[builtinCommandElab «set_option»] def elabSetOption : CommandElab :=
 fun stx => do

src/Init/Lean/Elab/Quotation.lean

@@ -430,7 +430,7 @@ structure OldContext :=
 
 private def oldRunTermElabM {α} (ctx : OldContext) (x : TermElabM α) : Except String α := do
 match x {fileName := "foo", fileMap := FileMap.ofString "", cmdPos := 0,
-  currNamespace := ctx.env.getNamespace,
+  currNamespace := ctx.env.getNamespace, currRecDepth := 0, maxRecDepth := 10000,
   openDecls := ctx.open_nss.map $ fun n => OpenDecl.simple n [],
   lctx := ctx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty ()}
   {env := ctx.env} with

src/Init/Lean/Elab/Term.lean

@@ -8,6 +8,7 @@ import Init.Lean.Util.Sorry
 import Init.Lean.Structure
 import Init.Lean.Meta
 import Init.Lean.Hygiene
+import Init.Lean.Util.RecDepth
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
 import Init.Lean.Elab.ResolveName
@@ -156,6 +157,11 @@ throw (Exception.ex (Elab.Exception.error msg))
 def throwUnsupportedSyntax {α} : TermElabM α :=
 throw (Exception.ex Elab.Exception.unsupportedSyntax)
 
+@[inline] def withIncRecDepth {α} (ref : Syntax) (x : TermElabM α) : TermElabM α := do
+ctx ← read;
+when (ctx.currRecDepth == ctx.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
+adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
+
 protected def getCurrMacroScope : TermElabM MacroScope := do
 ctx ← read;
 pure ctx.currMacroScope
@@ -523,7 +529,7 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
   The option `catchExPostpone == false` is used to implement `resumeElabTerm`
   to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errToSorry := true) : TermElabM Expr :=
-withFreshMacroScope $ withNode stx $ fun node => do
+withFreshMacroScope $ withIncRecDepth stx $ withNode stx $ fun node => do
   trace `Elab.step stx $ fun _ => stx;
   s ← get;
   let table := (termElabAttribute.ext.getState s.env).table;

src/Init/Lean/Meta/Basic.lean

@@ -11,6 +11,7 @@ import Init.Lean.Environment
 import Init.Lean.Class
 import Init.Lean.ReducibilityAttrs
 import Init.Lean.Util.Trace
+import Init.Lean.Util.RecDepth
 import Init.Lean.Meta.Exception
 import Init.Lean.Meta.DiscrTreeTypes
 import Init.Lean.Eval
@@ -113,6 +114,8 @@ structure Context :=
 (config         : Config         := {})
 (lctx           : LocalContext   := {})
 (localInstances : LocalInstances := #[])
+(currRecDepth   : Nat)
+(maxRecDepth    : Nat)
 
 structure PostponedEntry :=
 (lhs       : Level)
@@ -131,6 +134,11 @@ abbrev MetaM := ReaderT Context (EStateM Exception State)
 instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
 ⟨fun c s => EStateM.Result.error (arbitrary _) s⟩
 
+@[inline] def withIncRecDepth {α} (x : MetaM α) : MetaM α := do
+ctx ← read;
+when (ctx.currRecDepth == ctx.maxRecDepth) $ throw $ Exception.other maxRecDepthErrorMessage;
+adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
+
 @[inline] def getLCtx : MetaM LocalContext := do
 ctx ← read; pure ctx.lctx
 
@@ -186,25 +194,29 @@ registerEnvExtension $ do
 @[init mkMetaExtension]
 constant metaExt : EnvExtension MetaExtState := arbitrary _
 
-def whnf (e : Expr) : MetaM Expr := do
-env ← getEnv;
-(metaExt.getState env).whnf e
+def whnf (e : Expr) : MetaM Expr :=
+withIncRecDepth $ do
+  env ← getEnv;
+  (metaExt.getState env).whnf e
 
 def whnfForall (e : Expr) : MetaM Expr := do
 e' ← whnf e;
 if e'.isForall then pure e' else pure e
 
-def inferType (e : Expr) : MetaM Expr := do
-env ← getEnv;
-(metaExt.getState env).inferType e
+def inferType (e : Expr) : MetaM Expr :=
+withIncRecDepth $ do
+  env ← getEnv;
+  (metaExt.getState env).inferType e
 
-def isExprDefEqAux (t s : Expr) : MetaM Bool := do
-env ← getEnv;
-(metaExt.getState env).isDefEqAux t s
+def isExprDefEqAux (t s : Expr) : MetaM Bool :=
+withIncRecDepth $ do
+  env ← getEnv;
+  (metaExt.getState env).isDefEqAux t s
 
-def synthPending (e : Expr) : MetaM Bool := do
-env ← getEnv;
-(metaExt.getState env).synthPending e
+def synthPending (e : Expr) : MetaM Bool :=
+withIncRecDepth $ do
+  env ← getEnv;
+  (metaExt.getState env).synthPending e
 
 def mkFreshId : MetaM Name := do
 s ← get;
@@ -761,7 +773,7 @@ finally x (modify $ fun s => { mctx := mctx', .. s })
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
 ⟨fun env opts x => do
-   match x { config := { opts := opts } } { env := env } with
+   match x { config := { opts := opts }, currRecDepth := 0, maxRecDepth := getMaxRecDepth opts } { env := env } with
    | EStateM.Result.ok a s    => do
      s.traceState.traces.forM $ fun m => IO.println $ format m;
      MetaHasEval.eval s.env opts a
@@ -780,6 +792,6 @@ open Lean.Meta
 
 /-- Helper function for running `MetaM` methods in attributes -/
 @[inline] def IO.runMeta {α} (x : MetaM α) (env : Environment) (cfg : Config := {}) : IO (α × Environment) :=
-match (x { config := cfg }).run { env := env } with
+match (x { config := cfg, currRecDepth := 0, maxRecDepth := defaultMaxRecDepth }).run { env := env } with
 | EStateM.Result.ok a s     => pure (a, s.env)
 | EStateM.Result.error ex _ => throw (IO.userError (toString ex))

src/Init/Lean/Meta/Message.lean

@@ -15,7 +15,7 @@ namespace Meta
 namespace Exception
 
 private def run? {α} (ctx : ExceptionContext) (x : MetaM α) : Option α :=
-match x { lctx := ctx.lctx } { env := ctx.env, mctx := ctx.mctx, ngen := { namePrefix := `_meta_exception } } with
+match x { lctx := ctx.lctx, currRecDepth := 0, maxRecDepth := getMaxRecDepth ctx.opts } { env := ctx.env, mctx := ctx.mctx, ngen := { namePrefix := `_meta_exception } } with
 | EStateM.Result.ok a _ => some a
 | EStateM.Result.error _ _ => none
 

src/Init/Lean/Util/RecDepth.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Data.Options
+
+namespace Lean
+
+def defaultMaxRecDepth := 512
+
+def getMaxRecDepth (opts : Options) : Nat :=
+opts.getNat `maxRecDepth defaultMaxRecDepth
+
+@[init] def maxRecDepth : IO Unit :=
+registerOption `maxRecDepth { defValue := defaultMaxRecDepth, group := "", descr := "maximum recursion depth for many Lean procedures" }
+
+def maxRecDepthErrorMessage : String :=
+"maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+
+end Lean