From d13e7e924437b043f83b6a47bfefda69379264b7 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 4 Jun 2019 14:39:29 +0200 Subject: Raise an anomaly when looking up unknown constant/inductive If you have access to a kernel name you also should have the environment in which it is defined, barring hacks. In order to disfavor hacks we make the standard lookups raise anomalies so that people are forced to admit they rely on the internals of the environment. We find that hackers operated on the code for side effects, for finding inductive schemes, for simpl and for Print Assumptions. They attempted to operate on funind but the error handling code they wrote would have raised another Not_found instead of being useful. All these uses are indeed hacky so I am satisfied that we are not forcing new hacks on callers. --- kernel/environ.ml | 16 ++++++++++------ kernel/environ.mli | 10 +++++++--- kernel/names.ml | 3 +++ kernel/names.mli | 15 +++++++++------ kernel/safe_typing.ml | 12 +++++------- 5 files changed, 34 insertions(+), 22 deletions(-) (limited to 'kernel') diff --git a/kernel/environ.ml b/kernel/environ.ml index 98d66cafa1..2bee2f7a8e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -231,22 +231,26 @@ let fold_inductives f env acc = (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.Globals.constants + Cmap_env.get kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.Globals.constants) + fst (lookup_constant_key kn env) + +let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants (* Mutual Inductives *) +let lookup_mind_key kn env = + Mindmap_env.get kn env.env_globals.Globals.inductives + let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.Globals.inductives) + fst (lookup_mind_key kn env) + +let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.Globals.inductives - let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in diff --git a/kernel/environ.mli b/kernel/environ.mli index 5af2a7288b..782ea1c666 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,10 +201,12 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool +val mem_constant : Constant.t -> env -> bool + (** New-style polymorphism *) val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool @@ -215,7 +217,7 @@ val type_in_type_constant : Constant.t -> env -> bool [c] is opaque, [NotEvaluableConst NoBody] if it has no body, [NotEvaluableConst IsProj] if [c] is a projection, [NotEvaluableConst (IsPrimitive p)] if [c] is primitive [p] - and [Not_found] if it does not exist in [env] *) + and an anomaly if it does not exist in [env] *) type const_evaluation_result = | NoBody @@ -254,9 +256,11 @@ val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +val mem_mind : MutInd.t -> env -> bool + (** The universe context associated to the inductive, empty if not polymorphic *) val mind_context : env -> MutInd.t -> Univ.AUContext.t diff --git a/kernel/names.ml b/kernel/names.ml index 9802d4f531..b755ff0e08 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -675,6 +675,7 @@ module InductiveOrdered_env = struct end module Indset = Set.Make(InductiveOrdered) +module Indset_env = Set.Make(InductiveOrdered_env) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) @@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct let compare = constructor_user_ord end +module Constrset = Set.Make(ConstructorOrdered) +module Constrset_env = Set.Make(ConstructorOrdered_env) module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 78eb9295d4..0c92a2f2bc 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -471,7 +471,7 @@ end module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset -module Mindmap_env : CSig.MapS with type key = MutInd.t +module Mindmap_env : CMap.ExtS with type key = MutInd.t (** Designation of a (particular) inductive type. *) type inductive = MutInd.t (* the name of the inductive type *) @@ -484,11 +484,14 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) -module Indset : CSig.SetS with type elt = inductive -module Indmap : CSig.MapS with type key = inductive -module Constrmap : CSig.MapS with type key = constructor -module Indmap_env : CSig.MapS with type key = inductive -module Constrmap_env : CSig.MapS with type key = constructor +module Indset : CSet.S with type elt = inductive +module Constrset : CSet.S with type elt = constructor +module Indset_env : CSet.S with type elt = inductive +module Constrset_env : CSet.S with type elt = constructor +module Indmap : CMap.ExtS with type key = inductive and module Set := Indset +module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset +module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env +module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 00559206ee..e846b17aa0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -302,8 +302,8 @@ let lift_constant c = let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + if Environ.mem_constant eff.seff_constant env then env + else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env in List.fold_left add_if_undefined env eff @@ -598,8 +598,8 @@ let inline_side_effects env body side_eff = (** First step: remove the constants that are still in the environment *) let filter e = let cb = (e.seff_constant, e.seff_body) in - try ignore (Environ.lookup_constant e.seff_constant env); None - with Not_found -> Some (cb, e.from_env) + if Environ.mem_constant e.seff_constant env then None + else Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -750,9 +750,7 @@ let translate_direct_opaque env kn ce = { cb with const_body = OpaqueDef c } let export_side_effects mb env (b_ctx, eff) = - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in + let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl else e :: acc, e.from_env :: sl in -- cgit v1.2.3