From fdd5243fce5def474ea40a5d8abcbad9823fc176 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Sun, 29 Dec 2024 18:24:29 +0000 Subject: [PATCH] CN: Reduce code dup. for Global related errs Because of the split between WellTyped and Typing, the code for handling lookups in Global was duplicated across the two. This commit adjusts the API exposed by Global to avoid duplicating the error handling logic. It also needs to move Global-specific errors out of TypeErrors and into Global to avoid a circular dependency. (TypeErrors depends on Context which depends on Global, so Global cannot reference TypeErrors types). --- backend/cn/lib/cLogicalFuns.ml | 2 +- backend/cn/lib/check.ml | 2 +- backend/cn/lib/compile.ml | 15 +++-- backend/cn/lib/global.ml | 80 +++++++++++++++-------- backend/cn/lib/typeErrors.ml | 34 ++++------ backend/cn/lib/typeErrors.mli | 16 +---- backend/cn/lib/typing.ml | 63 ++---------------- backend/cn/lib/wellTyped.ml | 113 +++++++-------------------------- backend/cn/lib/wellTyped.mli | 6 +- 9 files changed, 108 insertions(+), 223 deletions(-) diff --git a/backend/cn/lib/cLogicalFuns.ml b/backend/cn/lib/cLogicalFuns.ml index 6ff498065..a97eac804 100644 --- a/backend/cn/lib/cLogicalFuns.ml +++ b/backend/cn/lib/cLogicalFuns.ml @@ -738,7 +738,7 @@ let add_logical_funs_from_c call_funinfo funs_to_convert funs = let@ fbody = match Pmap.lookup c_fun_sym funs with | Some fbody -> return fbody - | None -> fail_n { loc; msg = Unknown_function c_fun_sym } + | None -> fail_n { loc; msg = Global (Unknown_function c_fun_sym) } in let@ it = c_fun_to_it loc global_context l_fun_sym c_fun_sym def fbody in Pp.debug diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 4be62926c..8fdb6ffd1 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -2611,7 +2611,7 @@ let record_and_check_datatypes datatypes = datatypes -(** Note: this does not check loop invariants and CN statements! *) +(** NOTE: not clear if this checks loop invariants and CN statements! *) let check_decls_lemmata_fun_specs (file : unit Mu.file) = Cerb_debug.begin_csv_timing (); (* decl, lemmata, function specification checking *) diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml index 76ddb603b..26b45c570 100644 --- a/backend/cn/lib/compile.ml +++ b/backend/cn/lib/compile.ml @@ -424,7 +424,7 @@ module EffectfulTranslation = struct let lookup_struct loc tag env = match lookup_struct_opt tag env with | Some def -> return def - | None -> fail { loc; msg = Unknown_struct tag } + | None -> fail { loc; msg = Global (Unknown_struct tag) } let lookup_member loc (_tag, def) member = @@ -437,13 +437,13 @@ module EffectfulTranslation = struct let lookup_datatype loc sym env = match Sym.Map.find_opt sym env.datatypes with | Some info -> return info - | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype sym } + | None -> fail { loc; msg = Global (Unknown_datatype sym) } let lookup_constr loc sym env = match Sym.Map.find_opt sym env.datatype_constrs with | Some info -> return info - | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype_constr sym } + | None -> fail { loc; msg = Global (Unknown_datatype_constr sym) } let cannot_tell_pointee_ctype loc e = @@ -852,7 +852,9 @@ module EffectfulTranslation = struct | Some fsig -> return fsig.return_bty | None -> fail - { loc; msg = Unknown_logical_function { id = fsym; resource = false } } + { loc; + msg = Global (Unknown_logical_function { id = fsym; resource = false }) + } in return (apply_ fsym args (BaseTypes.Surface.inj bt) loc)) | CNExpr_cons (c_nm, exprs) -> @@ -1070,7 +1072,10 @@ module EffectfulTranslation = struct let@ pred_sig = match lookup_predicate pred env with | None -> - fail { loc; msg = Unknown_resource_predicate { id = pred; logical = false } } + fail + { loc; + msg = Global (Unknown_resource_predicate { id = pred; logical = false }) + } | Some pred_sig -> return pred_sig in let output_bt = pred_sig.pred_output in diff --git a/backend/cn/lib/global.ml b/backend/cn/lib/global.ml index 85975a877..386f217b6 100644 --- a/backend/cn/lib/global.ml +++ b/backend/cn/lib/global.ml @@ -44,63 +44,89 @@ let sym_map_from_bindings xs = List.fold_left (fun m (nm, x) -> Sym.Map.add nm x m) Sym.Map.empty xs -module type Reader = sig - type global = t - +type error = + | Unknown_function of Sym.t + | Unknown_struct of Sym.t + | Unknown_datatype of Sym.t + | Unknown_datatype_constr of Sym.t + | Unknown_resource_predicate of + { id : Sym.t; + logical : bool + } + | Unknown_logical_function of + { id : Sym.t; + resource : bool + } + | Unknown_lemma of Sym.t + +type global_t_alias_do_not_use = t + +module type ErrorReader = sig type 'a t val return : 'a -> 'a t val bind : 'a t -> ('a -> 'b t) -> 'b t - type state - - val get : unit -> state t + val get_global : unit -> global_t_alias_do_not_use t - val to_global : state -> global + val fail : Locations.t -> error -> 'a t end module type Lifted = sig type 'a t - val get_resource_predicate_def : Sym.t -> Definition.Predicate.t option t + val get_resource_predicate_def : Locations.t -> Sym.t -> Definition.Predicate.t t - val get_logical_function_def : Sym.t -> Definition.Function.t option t + val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.t t val get_fun_decl - : Sym.t -> - (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) option t + : Locations.t -> + Sym.t -> + (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) t - val get_lemma : Sym.t -> (Cerb_location.t * AT.lemmat) option t + val get_lemma : Locations.t -> Sym.t -> (Cerb_location.t * AT.lemmat) t - val get_struct_decl : Sym.t -> Memory.struct_layout option t + val get_struct_decl : Locations.t -> Sym.t -> Memory.struct_layout t - val get_datatype : Sym.t -> BaseTypes.dt_info option t + val get_datatype : Locations.t -> Sym.t -> BaseTypes.dt_info t - val get_datatype_constr : Sym.t -> BaseTypes.constr_info option t + val get_datatype_constr : Locations.t -> Sym.t -> BaseTypes.constr_info t end -module Lift (M : Reader) : Lifted with type 'a t := 'a M.t = struct - let lift f sym = +module Lift (M : ErrorReader) : Lifted with type 'a t := 'a M.t = struct + let lift f loc sym msg = let ( let@ ) = M.bind in - let@ state = M.get () in - let global = M.to_global state in - M.return (f global sym) + let@ global = M.get_global () in + match f global sym with Some x -> M.return x | None -> M.fail loc (msg global) + + + let get_logical_function_def_opt id = get_logical_function_def id + + let get_logical_function_def loc id = + lift get_logical_function_def loc id (fun global -> + let res = get_resource_predicate_def global id in + Unknown_logical_function { id; resource = Option.is_some res }) + + let get_resource_predicate_def loc id = + lift get_resource_predicate_def loc id (fun global -> + let log = get_logical_function_def_opt global id in + Unknown_resource_predicate { id; logical = Option.is_some log }) - let get_resource_predicate_def = lift get_resource_predicate_def - let get_logical_function_def = lift get_logical_function_def + let get_fun_decl loc fsym = lift get_fun_decl loc fsym (fun _ -> Unknown_function fsym) - let get_fun_decl = lift get_fun_decl + let get_lemma loc lsym = lift get_lemma loc lsym (fun _ -> Unknown_lemma lsym) - let get_lemma = lift get_lemma + let get_struct_decl loc tag = lift get_struct_decl loc tag (fun _ -> Unknown_struct tag) - let get_struct_decl = lift get_struct_decl + let get_datatype loc tag = + lift get_datatype loc tag (fun _ -> Unknown_datatype_constr tag) - let get_datatype = lift get_datatype - let get_datatype_constr = lift get_datatype_constr + let get_datatype_constr loc tag = + lift get_datatype_constr loc tag (fun _ -> Unknown_datatype_constr tag) end let pp_struct_layout (tag, layout) = diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml index bcaac62f2..e423b25a0 100644 --- a/backend/cn/lib/typeErrors.ml +++ b/backend/cn/lib/typeErrors.ml @@ -112,21 +112,9 @@ module RequestChain = struct end type message = - | Unknown_variable of Sym.t - | Unknown_function of Sym.t - | Unknown_struct of Sym.t - | Unknown_datatype of Sym.t - | Unknown_datatype_constr of Sym.t - | Unknown_resource_predicate of - { id : Sym.t; - logical : bool - } - | Unknown_logical_function of - { id : Sym.t; - resource : bool - } + | Global of Global.error | Unexpected_member of Id.t list * Id.t - | Unknown_lemma of Sym.t + | Unknown_variable of Sym.t (* some from Kayvan's compilePredicates module *) | First_iarg_missing | First_iarg_not_pointer of @@ -272,19 +260,19 @@ let pp_message te = | Unknown_variable s -> let short = !^"Unknown variable" ^^^ squotes (Sym.pp s) in { short; descr = None; state = None } - | Unknown_function sym -> + | Global (Unknown_function sym) -> let short = !^"Unknown function" ^^^ squotes (Sym.pp sym) in { short; descr = None; state = None } - | Unknown_struct tag -> + | Global (Unknown_struct tag) -> let short = !^"Struct" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Unknown_datatype tag -> + | Global (Unknown_datatype tag) -> let short = !^"Datatype" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Unknown_datatype_constr tag -> + | Global (Unknown_datatype_constr tag) -> let short = !^"Datatype constructor" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Unknown_resource_predicate { id; logical } -> + | Global (Unknown_resource_predicate { id; logical }) -> let short = !^"Unknown resource predicate" ^^^ squotes (Sym.pp id) in let descr = if logical then @@ -293,7 +281,7 @@ let pp_message te = None in { short; descr; state = None } - | Unknown_logical_function { id; resource } -> + | Global (Unknown_logical_function { id; resource }) -> let short = !^"Unknown logical function" ^^^ squotes (Sym.pp id) in let descr = if resource then @@ -302,13 +290,13 @@ let pp_message te = None in { short; descr; state = None } + | Global (Unknown_lemma sym) -> + let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in + { short; descr = None; state = None } | Unexpected_member (expected, member) -> let short = !^"Unexpected member" ^^^ Id.pp member in let descr = !^"the struct only has members" ^^^ list Id.pp expected in { short; descr = Some descr; state = None } - | Unknown_lemma sym -> - let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in - { short; descr = None; state = None } | First_iarg_missing -> let short = !^"Missing pointer input argument" in let descr = !^"a predicate definition must have at least one input argument" in diff --git a/backend/cn/lib/typeErrors.mli b/backend/cn/lib/typeErrors.mli index a5c1b9a3e..ae3f2fc64 100644 --- a/backend/cn/lib/typeErrors.mli +++ b/backend/cn/lib/typeErrors.mli @@ -50,21 +50,9 @@ module RequestChain : sig end type message = - | Unknown_variable of Sym.t - | Unknown_function of Sym.t - | Unknown_struct of Sym.t - | Unknown_datatype of Sym.t - | Unknown_datatype_constr of Sym.t - | Unknown_resource_predicate of - { id : Sym.t; - logical : bool - } - | Unknown_logical_function of - { id : Sym.t; - resource : bool - } + | Global of Global.error | Unexpected_member of Id.t list * Id.t - | Unknown_lemma of Sym.t + | Unknown_variable of Sym.t | First_iarg_missing | First_iarg_not_pointer of { pname : Request.name; diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index a0334fa9c..9019a3777 100644 --- a/backend/cn/lib/typing.ml +++ b/backend/cn/lib/typing.ml @@ -210,15 +210,17 @@ module ErrorReader = struct let bind = bind - type state = s + let get_global () = + let@ s = get () in + return s.typing_context.global - type global = Global.t - let get = get + let fail loc msg = fail (fun _ -> { loc; msg = Global msg }) - let to_global (s : s) = s.typing_context.global + let get_context () = + let@ s = get () in + return s.typing_context - let to_context (s : s) = s.typing_context let lift = lift end @@ -230,63 +232,12 @@ module Global = struct let is_fun_decl global id = Option.is_some @@ Global.get_fun_decl global id - let get_logical_function_def_opt id = get_logical_function_def id - - let error_if_none opt loc msg = - let@ opt in - Option.fold - opt - ~some:return - ~none: - (let@ msg in - fail (fun _ -> { loc; msg })) - - - let get_logical_function_def loc id = - error_if_none - (get_logical_function_def id) - loc - (let@ res = get_resource_predicate_def id in - return (TypeErrors.Unknown_logical_function { id; resource = Option.is_some res })) - - - let get_struct_decl loc tag = - error_if_none (get_struct_decl tag) loc (return (TypeErrors.Unknown_struct tag)) - - - let get_datatype loc tag = - error_if_none (get_datatype tag) loc (return (TypeErrors.Unknown_datatype tag)) - - - let get_datatype_constr loc tag = - error_if_none - (get_datatype_constr tag) - loc - (return (TypeErrors.Unknown_datatype_constr tag)) - - let get_struct_member_type loc tag member = let@ decl = get_struct_decl loc tag in let@ ty = get_member_type loc member decl in return ty - let get_fun_decl loc fsym = - error_if_none (get_fun_decl fsym) loc (return (TypeErrors.Unknown_function fsym)) - - - let get_lemma loc lsym = - error_if_none (get_lemma lsym) loc (return (TypeErrors.Unknown_lemma lsym)) - - - let get_resource_predicate_def loc id = - error_if_none - (get_resource_predicate_def id) - loc - (let@ log = get_logical_function_def_opt id in - return (TypeErrors.Unknown_resource_predicate { id; logical = Option.is_some log })) - - let get_fun_decls () = let@ global = get_global () in return (Sym.Map.bindings global.fun_decls) diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index 14222bec2..bd6ef4246 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -18,33 +18,38 @@ module GlobalReader = struct let bind x f s = match x s with Ok (y, s') -> f y s' | Error err -> Error err - let get () s = Ok (s, s) + let get_global () s = Ok (s.Context.global, s) - let to_global ctxt = ctxt.Context.global - - type global = Global.t - - type state = Context.t + let fail loc msg _ = Error TypeErrors.{ loc; msg = Global msg } end module NoSolver = struct include GlobalReader include Global.Lift (GlobalReader) - type failure = TypeErrors.t + let fail err : 'a t = fun _ -> Error err - let liftFail typeErr = typeErr + let ( let@ ) = bind + + let get_member_type loc member layout : Sctypes.t t = + let member_types = Memory.member_types layout in + match List.assoc_opt Id.equal member member_types with + | Some membertyp -> return membertyp + | None -> fail { loc; msg = Unexpected_member (List.map fst member_types, member) } + + + let get_struct_member_type loc tag member = + let@ decl = get_struct_decl loc tag in + let@ ty = get_member_type loc member decl in + return ty - let pure x s = match x s with Ok (y, _) -> Ok (y, s) | Error err -> Error err - let fail (typeErr : failure) : 'a t = fun _ -> Error (liftFail typeErr) + let pure x s = match x s with Ok (y, _) -> Ok (y, s) | Error err -> Error err let update f s = Ok ((), f s) let lookup f : _ t = fun s -> Ok (f s, s) - let ( let@ ) = bind - let bound_a sym = lookup (Context.bound_a sym) let bound_l sym = lookup (Context.bound_l sym) @@ -64,70 +69,6 @@ module NoSolver = struct fail { loc; msg = Mismatch { has = BT.pp has; expect = BT.pp expect } } - let error_if_none opt loc msg = - let@ opt in - Option.fold - opt - ~some:return - ~none: - (let@ msg in - fail { loc; msg }) - - - let get_logical_function_def_opt id = get_logical_function_def id - - let get_logical_function_def loc id = - error_if_none - (get_logical_function_def id) - loc - (let@ res = get_resource_predicate_def id in - return (TypeErrors.Unknown_logical_function { id; resource = Option.is_some res })) - - - let get_struct_decl loc tag = - error_if_none (get_struct_decl tag) loc (return (TypeErrors.Unknown_struct tag)) - - - let get_datatype loc tag = - error_if_none (get_datatype tag) loc (return (TypeErrors.Unknown_datatype tag)) - - - let get_datatype_constr loc tag = - error_if_none - (get_datatype_constr tag) - loc - (return (TypeErrors.Unknown_datatype_constr tag)) - - - let get_member_type loc member layout : Sctypes.t t = - let member_types = Memory.member_types layout in - match List.assoc_opt Id.equal member member_types with - | Some membertyp -> return membertyp - | None -> fail { loc; msg = Unexpected_member (List.map fst member_types, member) } - - - let get_struct_member_type loc tag member = - let@ decl = get_struct_decl loc tag in - let@ ty = get_member_type loc member decl in - return ty - - - let get_fun_decl loc fsym = - error_if_none (get_fun_decl fsym) loc (return (TypeErrors.Unknown_function fsym)) - - - let get_lemma loc lsym = - error_if_none (get_lemma lsym) loc (return (TypeErrors.Unknown_lemma lsym)) - - - let get_resource_predicate_def loc id = - error_if_none - (get_resource_predicate_def id) - loc - (let@ log = get_logical_function_def_opt id in - return (TypeErrors.Unknown_resource_predicate { id; logical = Option.is_some log })) - - let lift = function Ok x -> return x | Error x -> fail x let run ctxt x = x ctxt @@ -137,8 +78,6 @@ let use_ity = ref true open NoSolver -let fail typeErr = fail (liftFail typeErr) - open Effectful.Make (NoSolver) let illtyped_index_term (loc : Locations.t) it has ~expected ~reason = @@ -2523,11 +2462,7 @@ module type ErrorReader = sig val bind : 'a t -> ('a -> 'b t) -> 'b t - type state - - val get : unit -> state t - - val to_context : state -> Context.t + val get_context : unit -> Context.t t val lift : 'a Or_TypeError.t -> 'a t end @@ -2535,22 +2470,19 @@ end module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = struct let lift1 f x = let ( let@ ) = M.bind in - let@ state = M.get () in - let context = M.to_context state in + let@ context = M.get_context () in M.lift (Result.map fst (run context (f x))) let lift2 f x y = let ( let@ ) = M.bind in - let@ state = M.get () in - let context = M.to_context state in + let@ context = M.get_context () in M.lift (Result.map fst (f x y context)) let lift3 f x y z = let ( let@ ) = M.bind in - let@ state = M.get () in - let context = M.to_context state in + let@ context = M.get_context () in M.lift (Result.map fst (f x y z context)) @@ -2594,8 +2526,7 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru let ensure_same_argument_number loc type_ n ~expect = let ( let@ ) = M.bind in - let@ state = M.get () in - let context = M.to_context state in + let@ context = M.get_context () in M.lift (Result.map fst (ensure_same_argument_number loc type_ n ~expect context)) diff --git a/backend/cn/lib/wellTyped.mli b/backend/cn/lib/wellTyped.mli index 762140161..22296b75e 100644 --- a/backend/cn/lib/wellTyped.mli +++ b/backend/cn/lib/wellTyped.mli @@ -9,11 +9,7 @@ module type ErrorReader = sig val bind : 'a t -> ('a -> 'b t) -> 'b t - type state - - val get : unit -> state t - - val to_context : state -> Context.t + val get_context : unit -> Context.t t val lift : 'a Or_TypeError.t -> 'a t end