From c70e614a5bdeadff98a899731478fe3a598288fb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 4 Mar 2025 11:29:54 +0100 Subject: [PATCH] chore: harden use of panics in `Lean.Environment` (#7321) * avoid `panic!`s that return `Unit` or some otherwise unused value lest they get optimized away * make some fallback values explicit to avoid follow-up errors * avoid redundant declaration names in panic messages --- src/Lean/Environment.lean | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e99bef54f6..93ddf96b22 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -441,7 +441,8 @@ deriving Inhabited private def AsyncConsts.add (aconsts : AsyncConsts) (aconst : AsyncConst) : AsyncConsts := let normalizedName := privateToUserName aconst.constInfo.name if let some aconst' := aconsts.normalizedTrie.find? normalizedName then - panic! s!"AsyncConsts.add: duplicate normalized declaration name {aconst.constInfo.name} vs. {aconst'.constInfo.name}" + let _ : Inhabited AsyncConsts := ⟨aconsts⟩ + panic! s!"duplicate normalized declaration name {aconst.constInfo.name} vs. {aconst'.constInfo.name}" else { aconsts with size := aconsts.size + 1 revList := aconst :: aconsts.revList @@ -675,10 +676,12 @@ definitely too late. def enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) : BaseIO Environment := do if env.findAsync? c |>.isNone then - panic! s!"Environment.enableRealizationsForConst: declaration {c} not found in environment" + panic! s!"declaration {c} not found in environment" + return env if let some asyncCtx := env.asyncCtx? then if !asyncCtx.mayContain c then - panic! s!"Environment.enableRealizationsForConst: {c} is outside current context {asyncCtx.declPrefix}" + panic! s!"{c} is outside current context {asyncCtx.declPrefix}" + return env if env.realizedLocalConsts.contains c then return env return { env with realizedLocalConsts := env.realizedLocalConsts.insert c { @@ -806,7 +809,7 @@ private def mkFallbackConstInfo (constName : Name) (kind : ConstantKind) : Const | .axiom => .axiomInfo { fallbackVal with isUnsafe := false } - | k => panic! s!"Environment.mkFallbackConstInfo: unsupported constant kind {repr k}" + | k => panic! s!"unsupported constant kind {repr k}" /-- Starts the asynchronous addition of a constant to the environment. The environment is split into a @@ -921,8 +924,8 @@ def allImportedModuleNames (env : Environment) : Array Name := def setMainModule (env : Environment) (m : Name) : Environment := Id.run do if env.realizedImportedConsts?.isSome then - panic! "Environment.setMainModule: cannot set after `enableRealizationsForImports`" - return env + let _ : Inhabited Environment := ⟨env⟩ + return panic! "cannot set after `enableRealizationsForImports`" env.modifyCheckedAsync ({ · with header.mainModule := m }) def mainModule (env : Environment) : Name := @@ -1068,6 +1071,7 @@ private unsafe def setStateImpl {σ} (ext : EnvExtension σ) (exts : Array EnvEx if h : ext.idx < exts.size then exts.set ext.idx (unsafeCast s) else + -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses have : Inhabited (Array EnvExtensionState) := ⟨exts⟩ panic! invalidExtMsg @@ -1078,6 +1082,7 @@ private unsafe def modifyStateImpl {σ : Type} (ext : EnvExtension σ) (exts : A let s : σ := f s unsafeCast s else + -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses have : Inhabited (Array EnvExtensionState) := ⟨exts⟩ panic! invalidExtMsg @@ -1099,11 +1104,13 @@ Note that in modes `sync` and `async`, `f` will be called twice, on the local an state. -/ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := Id.run do + -- for panics + let _ : Inhabited Environment := ⟨env⟩ -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ` match ext.asyncMode with | .mainOnly => if let some asyncCtx := env.asyncCtx? then - panic! s!"Environment.modifyState: environment extension is marked as `mainOnly` but used in \ + return panic! s!"environment extension is marked as `mainOnly` but used in \ {if asyncCtx.realizing then "realization" else "async"} context '{asyncCtx.declPrefix}'" return { env with checkedWithoutAsync.extensions := unsafe ext.modifyStateImpl env.checkedWithoutAsync.extensions f } | .local => @@ -1111,7 +1118,7 @@ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ | _ => if ext.replay?.isNone then if let some asyncCtx := env.asyncCtx?.filter (·.realizing) then - panic! s!"Environment.modifyState: environment extension must set `replay?` field to be \ + return panic! s!"environment extension must set `replay?` field to be \ used in realization context '{asyncCtx.declPrefix}'" env.modifyCheckedAsync fun env => { env with extensions := unsafe ext.modifyStateImpl env.extensions f } @@ -1129,7 +1136,7 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ` match asyncMode with | .sync => ext.getStateImpl env.checked.get.extensions - | .async => panic! "EnvExtension.getState: called on `async` extension, use `findStateAsync` \ + | .async => panic! "called on `async` extension, use `findStateAsync` \ instead or pass `(asyncMode := .local)` to explicitly access local state" | _ => ext.getStateImpl env.checkedWithoutAsync.extensions @@ -1950,17 +1957,19 @@ where -- generator. kenv := kenv.add info continue - let decl := match info with + -- for panics + let _ : Inhabited Kernel.Environment := ⟨kenv⟩ + let decl ← match info with | .thmInfo thm => .thmDecl thm | .defnInfo defn => .defnDecl defn - | _ => panic! s!"Environment.realizeConst: {c.constInfo.name} must be definition/theorem" + | _ => + return panic! s!"{c.constInfo.name} must be definition/theorem" -- realized kernel additions cannot be interrupted - which would be bad anyway as they can be -- reused between snapshots match kenv.addDeclCore 0 decl none with | .ok kenv' => kenv := kenv' | .error e => - let _ : Inhabited Kernel.Environment := ⟨kenv⟩ - panic! s!"Environment.realizeConst: failed to add {c.constInfo.name} to environment\n{e.toRawString}" + return panic! s!"failed to add {c.constInfo.name} to environment\n{e.toRawString}" for ext in exts do if let some replay := ext.replay? then kenv := { kenv with