From 40a016404fb00d7d9b8e202e079178aa060daf73 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 27 Dec 2024 02:31:48 +0000 Subject: [PATCH] CN: Separate well-typed and consistency checks WellTyped/well-formedness checks were intertwined with the typing monad because they also performed consistency checks. This made running just the well-formedness checks slower, and did not allow users to opt-out of running the consistency check. This commit adds variants `consistent` functions, which are variants on the `welltyped` functions. The latter add variables to scope and check basetypes; the former add variables to scope, constraints and resources. It also tidies up the wellTyped.ml module to clarify and restrict which of the typing monad functions it was using. This will be the first step of many to factor out the logging and the error reporting for different phases. This commit also required an update to the `pure` function in the typing monad, so that it can work without a solver (functionality with a solver initialised should be unaffected). Slightly awkwardly, the reshuffle also required gathering and delaying adding the range constraints for global variables, since adding constraints and resources both require the solver to be initialised. This can and should be tidied up, which will come in subsequent commits, but for now this should pass all tests. --- backend/cn/bin/main.ml | 4 +- backend/cn/lib/check.ml | 197 +++++----- backend/cn/lib/resourceInference.ml | 4 +- backend/cn/lib/typing.ml | 4 +- backend/cn/lib/typing.mli | 2 - backend/cn/lib/wellTyped.ml | 546 ++++++++++++++++++-------- tests/cn/implies3.error.c.verify | 2 +- tests/cn/inconsistent.error.c.verify | 2 +- tests/cn/inconsistent2.error.c.verify | 3 + 9 files changed, 501 insertions(+), 263 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index a80720458..0ffdb0d56 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -322,9 +322,9 @@ let verify ~magic_comment_char_dollar (* Callbacks *) ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace) ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused -> - let check (functions, lemmas) = + let check (functions, global_var_constraints, lemmas) = let open Typing in - let@ errors = Check.time_check_c_functions functions in + let@ errors = Check.time_check_c_functions (global_var_constraints, functions) in if not quiet then List.iter (fun (fn, err) -> diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index e1a561f63..6ad4c8778 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -130,7 +130,7 @@ let rec check_mem_value (loc : Locations.t) ~(expect : BT.t) (mem : mem_value) : (fun ity iv -> let@ () = WellTyped.WCT.is_ct loc (Integer ity) in let bt = Memory.bt_of_sct (Integer ity) in - let@ () = WellTyped.ensure_base_type loc ~expect bt in + let@ () = ensure_base_type loc ~expect bt in return (int_lit_ (Memory.int_of_ival iv) bt loc)) (fun _ft _fv -> unsupported loc !^"floats") (fun ct ptrval -> @@ -144,7 +144,7 @@ let rec check_mem_value (loc : Locations.t) ~(expect : BT.t) (mem : mem_value) : return (make_array_ ~index_bt ~item_bt values loc)) (fun tag mvals -> let@ () = WellTyped.WCT.is_ct loc (Struct tag) in - let@ () = WellTyped.ensure_base_type loc ~expect (Struct tag) in + let@ () = ensure_base_type loc ~expect (Struct tag) in let mvals = List.map (fun (id, ct, mv) -> (id, Sctypes.of_ctype_unsafe loc ct, mv)) mvals in @@ -232,18 +232,18 @@ let rec check_value (loc : Locations.t) (Mu.V (expect, v)) : IT.t m = let@ () = ensure_base_type loc ~expect (Mu.bt_of_object_value ov) in check_object_value loc ov | Vctype ct -> - let@ () = WellTyped.ensure_base_type loc ~expect CType in + let@ () = ensure_base_type loc ~expect CType in let ct = Sctypes.of_ctype_unsafe loc ct in let@ () = WellTyped.WCT.is_ct loc ct in return (IT.const_ctype_ ct loc) | Vunit -> - let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect Unit in return (IT.unit_ loc) | Vtrue -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in return (IT.bool_ true loc) | Vfalse -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in return (IT.bool_ false loc) | Vfunction_addr sym -> let@ () = ensure_base_type loc ~expect (Loc ()) in @@ -252,7 +252,7 @@ let rec check_value (loc : Locations.t) (Mu.V (expect, v)) : IT.t m = return (IT.sym_ (sym, BT.(Loc ()), loc)) | Vlist (_item_cbt, vals) -> let item_bt = Mu.bt_of_value (List.hd vals) in - let@ () = WellTyped.ensure_base_type loc ~expect (List item_bt) in + let@ () = ensure_base_type loc ~expect (List item_bt) in let@ () = ListM.iterM (fun i -> ensure_base_type loc ~expect:item_bt (Mu.bt_of_value i)) vals in @@ -511,10 +511,10 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = let@ binding = get_a sym in (match binding with | BaseType bt -> - let@ () = WellTyped.ensure_base_type loc ~expect bt in + let@ () = ensure_base_type loc ~expect bt in k (sym_ (sym, bt, loc)) | Value lvt -> - let@ () = WellTyped.ensure_base_type loc ~expect (IT.get_bt lvt) in + let@ () = ensure_base_type loc ~expect (IT.get_bt lvt) in k lvt) | PEval v -> let@ () = ensure_base_type loc ~expect (Mu.bt_of_value v) in @@ -582,7 +582,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = | Cfvfromint _ -> unsupported loc !^"floats" | Civfromfloat _ -> unsupported loc !^"floats" | PEarray_shift (pe1, ct, pe2) -> - let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = ensure_base_type loc ~expect (Loc ()) in let@ () = WellTyped.WCT.is_ct loc ct in let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in @@ -608,7 +608,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in k result)) | PEmember_shift (pe, tag, member) -> - let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = ensure_base_type loc ~expect (Loc ()) in let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun vt -> let@ ct = get_struct_member_type loc tag member in @@ -627,7 +627,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in k result) | PEnot pe -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in check_pexpr pe (fun vt -> k (not_ vt loc)) | PEop (op, pe1, pe2) -> @@ -643,7 +643,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in (match op with | OpDiv -> - let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc expect in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> @@ -658,7 +658,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = let ub = CF.Undefined.UB045a_division_by_zero in fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))) | OpRem_t -> - let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc expect in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> @@ -673,63 +673,48 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = let ub = CF.Undefined.UB045b_modulo_by_zero in fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))) | OpEq -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Mu.bt_of_pexpr pe1) - (Mu.bt_of_pexpr pe2) + ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (eq_ (v1, v2) loc))) | OpGt -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Mu.bt_of_pexpr pe1) - (Mu.bt_of_pexpr pe2) + ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (gt_ (v1, v2) loc))) | OpLt -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Mu.bt_of_pexpr pe1) - (Mu.bt_of_pexpr pe2) + ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (lt_ (v1, v2) loc))) | OpGe -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Mu.bt_of_pexpr pe1) - (Mu.bt_of_pexpr pe2) + ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (ge_ (v1, v2) loc))) | OpLe -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Mu.bt_of_pexpr pe1) - (Mu.bt_of_pexpr pe2) + ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (le_ (v1, v2) loc))) | OpAnd -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in - let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in - let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in + let@ () = ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in + let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (and_ [ v1; v2 ] loc))) | OpOr -> - let@ () = WellTyped.ensure_base_type loc ~expect Bool in - let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in - let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in + let@ () = ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in + let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (or_ [ v1; v2 ] loc))) | OpAdd -> not_yet "OpAdd" | OpSub -> @@ -936,7 +921,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })) | PEis_representable_integer (pe, act) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe) in let ity = Option.get (Sctypes.is_integer_type act.ct) in check_pexpr pe (fun arg -> k (is_representable_integer arg ity)) @@ -1338,7 +1323,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | Ememop memop -> let here = Locations.other __LOC__ in let pointer_eq ?(negate = false) pe1 pe2 = - let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect Bool in let k, case, res = if negate then ((fun x -> k (not_ x loc)), "in", "ptrNeq") else (k, "", "ptrEq") in @@ -1484,9 +1469,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | PtrFromInt (act_from, act_to, pe) -> let@ () = WellTyped.WCT.is_ct act_from.loc act_from.ct in let@ () = WellTyped.WCT.is_ct act_to.loc act_to.ct in - let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = ensure_base_type loc ~expect (Loc ()) in let@ () = - WellTyped.ensure_base_type + ensure_base_type loc ~expect:(Memory.bt_of_sct act_from.ct) (Mu.bt_of_pexpr pe) @@ -1511,8 +1496,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | PtrValidForDeref (act, pe) -> (* TODO (DCM, VIP) *) let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect Bool in - let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in (* TODO (DCM, VIP): error if called on Void or Function Ctype. return false if resource missing *) check_pexpr pe (fun arg -> @@ -1526,8 +1511,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = k result) | PtrWellAligned (act, pe) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect Bool in - let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = ensure_base_type loc ~expect Bool in + let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in (* TODO (DCM, VIP): error if called on Void or Function Ctype *) check_pexpr pe (fun arg -> (* let unspec = CF.Undefined.UB_unspec_pointer_add in *) @@ -1560,12 +1545,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = (Loc.other __LOC__) !^"PtrMemberShift should be a CHERI only construct" | CopyAllocId (pe1, pe2) -> - let@ () = - WellTyped.ensure_base_type loc ~expect:Memory.uintptr_bt (Mu.bt_of_pexpr pe1) - in - let@ () = - WellTyped.ensure_base_type loc ~expect:BT.(Loc ()) (Mu.bt_of_pexpr pe2) - in + let@ () = ensure_base_type loc ~expect:Memory.uintptr_bt (Mu.bt_of_pexpr pe1) in + let@ () = ensure_base_type loc ~expect:BT.(Loc ()) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun vt1 -> check_pexpr pe2 (fun vt2 -> let unspec = CF.Undefined.UB_unspec_copy_alloc_id in @@ -1590,7 +1571,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = (match action_ with | Create (pe, act, prefix) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = ensure_base_type loc ~expect (Loc ()) in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> let ret_s, ret = @@ -1641,7 +1622,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = Cerb_debug.error "todo: Free" | Kill (Static ct, pe) -> let@ () = WellTyped.WCT.is_ct loc ct in - let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect Unit in let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> let@ _ = @@ -1657,15 +1638,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = k (unit_ loc)) | Store (_is_locking, act, p_pe, v_pe, _mo) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) in let@ () = - WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) - in - let@ () = - WellTyped.ensure_base_type - loc - ~expect:(Memory.bt_of_sct act.ct) - (Mu.bt_of_pexpr v_pe) + ensure_base_type loc ~expect:(Memory.bt_of_sct act.ct) (Mu.bt_of_pexpr v_pe) in check_pexpr p_pe (fun parg -> check_pexpr v_pe (fun varg -> @@ -1704,10 +1680,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = k (unit_ loc))) | Load (act, p_pe, _mo) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in - let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in - let@ () = - WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) - in + let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in + let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) in check_pexpr p_pe (fun pointer -> let@ value = load loc pointer act.ct in k value) @@ -1722,7 +1696,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | LinuxStore (_ct, _sym1, _sym2, _mo) -> Cerb_debug.error "todo: LinuxStore" | LinuxRMW (_ct, _sym1, _sym2, _mo) -> Cerb_debug.error "todo: LinuxRMW") | Eskip -> - let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect Unit in k (unit_ loc) | Eccall (act, f_pe, pes) -> let@ () = WellTyped.WCT.is_ct act.loc act.ct in @@ -1748,7 +1722,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in (* checks pes against their annotations, and that they match ft's argument types *) Spine.calltype_ft loc ~fsym pes ft (fun (Computational ((_, bt), _, _) as rt) -> - let@ () = WellTyped.ensure_base_type loc ~expect bt in + let@ () = ensure_base_type loc ~expect bt in let@ _, members = make_return_record loc @@ -1846,7 +1820,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in eq_ (lhs, rhs) here in - let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = ensure_base_type loc ~expect Unit in let aux loc stmt = (* copying bits of code from elsewhere in check.ml *) match stmt with @@ -2077,7 +2051,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let check_expr_top loc labels rt e = - let@ () = WellTyped.ensure_base_type loc ~expect:Unit (Mu.bt_of_expr e) in + let@ () = ensure_base_type loc ~expect:Unit (Mu.bt_of_expr e) in check_expr labels e (fun lvt -> let (RT.Computational ((return_s, return_bt), _info, lrt)) = rt in match return_bt with @@ -2280,11 +2254,10 @@ let record_and_check_resource_predicates preds = preds -let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m = +let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> LC.t list m = fun globs -> - (* TODO: check the expressions *) - ListM.iterM - (fun (sym, def) -> + ListM.fold_leftM + (fun acc (sym, def) -> match def with | Mu.GlobalDef (ct, _) | GlobalDecl ct -> let@ () = WellTyped.WCT.is_ct (Loc.other __LOC__) ct in @@ -2292,12 +2265,10 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m = let info = (Loc.other __LOC__, lazy (Pp.item "global" (Sym.pp sym))) in let@ () = add_a sym bt info in let here = Locations.other __LOC__ in - let@ () = - add_c here (LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here)) - in + let good = LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here) in let ptr = sym_ (sym, bt, here) in - let@ () = add_c here (LC.T (IT.hasAllocId_ ptr here)) in - let@ () = + let hasAllocId = LC.T (IT.hasAllocId_ ptr here) in + let range = if !IT.use_vip then let module H = Alloc.History in let H.{ base; size } = H.(split (lookup_ptr ptr here) here) in @@ -2311,11 +2282,13 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m = ] here in - add_c here (LC.T bounds) + [ LC.T bounds ] else - return () + [] in - return ()) + (* TODO: check the expressions *) + return (good :: hasAllocId :: (range @ acc))) + [] globs @@ -2645,8 +2618,7 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) = let@ () = record_tagdefs file.tagDefs in let@ () = check_tagdefs file.tagDefs in let@ () = record_and_check_datatypes file.datatypes in - let@ () = init_solver () in - let@ () = record_globals file.globs in + let@ global_var_constraints = record_globals file.globs in let@ () = register_fun_syms file in let@ () = ListM.iterM (add_stdlib_spec file.call_funinfo) (Sym.Set.elements file.stdlib_syms) @@ -2662,14 +2634,41 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) = let@ _trusted, checked = wf_check_and_record_functions file.funs file.call_funinfo in Pp.debug 3 (lazy (Pp.headline "type-checked C functions and specifications.")); Cerb_debug.end_csv_timing "decl, lemmata, function specification checking"; - return (List.rev checked, lemmata) + return (List.rev checked, global_var_constraints, lemmata) (** With CSV timing enabled, check the provided functions with [check_c_functions]. See that function for more information on the semantics of checking. *) -let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t) list m = +let time_check_c_functions (global_var_constraints, (checked : c_function list)) + : (string * TypeErrors.t) list m + = Cerb_debug.begin_csv_timing () (*type checking functions*); + let@ () = init_solver () in + let here = Locations.other __LOC__ in + let@ () = add_cs here global_var_constraints in + let@ global = get_global () in + let@ () = + Sym.Map.fold + (fun _ def acc -> + (* I think this avoids a left-recursion in the monad bind *) + let@ () = WellTyped.WRPD.consistent def in + acc) + global.resource_predicates + (return ()) + in + let@ () = + Sym.Map.fold + (fun _ (loc, def, _) acc -> + match def with + | None -> acc + | Some def -> + (* I think this avoids a left-recursion in the monad bind *) + let@ () = WellTyped.WFT.consistent "proc/fun" loc def in + acc) + global.fun_decls + (return ()) + in let@ errors = check_c_functions checked in Cerb_debug.end_csv_timing "type checking functions"; return errors @@ -2678,7 +2677,17 @@ let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t) let generate_lemmas lemmata o_lemma_mode = let@ global = get_global () in match o_lemma_mode with - | Some mode -> lift (Lemmata.generate global mode lemmata) + | Some mode -> + let@ () = + Sym.Map.fold + (fun sym (loc, lemma_typ) acc -> + (* I think this avoids a left-recursion in the monad bind *) + let@ () = WellTyped.WLemma.consistent loc sym lemma_typ in + acc) + global.lemmata + (return ()) + in + lift (Lemmata.generate global mode lemmata) | None -> return () (* TODO: diff --git a/backend/cn/lib/resourceInference.ml b/backend/cn/lib/resourceInference.ml index 07e11f63a..285f1dfb6 100644 --- a/backend/cn/lib/resourceInference.ml +++ b/backend/cn/lib/resourceInference.ml @@ -160,7 +160,7 @@ module General = struct = Pp.(debug 7 (lazy (item __LOC__ (Req.pp (P requested))))); let start_timing = Pp.time_log_start __LOC__ "" in - let@ oarg_bt = WellTyped.oarg_bt_of_pred loc requested.name in + let@ oarg_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in let@ provable = provable loc in let@ global = get_global () in let@ simp_ctxt = simp_ctxt () in @@ -384,7 +384,7 @@ module General = struct and qpredicate_request loc uiinfo (requested : Req.QPredicate.t) = let@ o_oarg = qpredicate_request_aux loc uiinfo requested in - let@ oarg_item_bt = WellTyped.oarg_bt_of_pred loc requested.name in + let@ oarg_item_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in match o_oarg with | None -> return None | Some (oarg, rw_time) -> diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index bf1f01786..72d392b29 100644 --- a/backend/cn/lib/typing.ml +++ b/backend/cn/lib/typing.ml @@ -72,9 +72,9 @@ let pause_to_result (pause : 'a pause) : 'a Or_TypeError.t = Result.map fst paus let pure (m : 'a t) : 'a t = fun s -> - Solver.push (Option.get s.solver); + Option.iter Solver.push s.solver; let outcome = match m s with Ok (a, _) -> Ok (a, s) | Error e -> Error e in - Solver.pop (Option.get s.solver) 1; + Option.iter (fun s -> Solver.pop s 1) s.solver; outcome diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli index 8d7d646c0..2c0b95fda 100644 --- a/backend/cn/lib/typing.mli +++ b/backend/cn/lib/typing.mli @@ -1,5 +1,3 @@ -type solver - type 'a t type 'a m = 'a t diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index 31312c47f..981ade6b8 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -2,29 +2,69 @@ module CF = Cerb_frontend module BT = BaseTypes module IT = IndexTerms module Loc = Locations -module LC = LogicalConstraints -module TE = TypeErrors -module Res = Resource -module Req = Request -module Def = Definition -module LRT = LogicalReturnTypes -module AT = ArgumentTypes -module LAT = LogicalArgumentTypes -module Mu = Mucore module IdSet = Set.Make (Id) -open Context -open Global -open TE -open Pp -open Typing +open Pp.Infix + +let squotes, warn, dot, string, debug, item, colon, comma = + Pp.(squotes, warn, dot, string, debug, item, colon, comma) + + +module type NoSolver = sig + (** TODO make this abstract, and one-way lifting functions? *) + type 'a m = 'a Typing.t + + (* TODO: different error types for type errors, consistency errors, proof errors *) + type failure = Context.t * Explain.log -> TypeErrors.t + + val pure : 'a m -> 'a m + + val fail : failure -> 'a m + + val bound_a : Sym.t -> bool m + + val bound_l : Sym.t -> bool m + + val get_a : Sym.t -> Context.basetype_or_value m + + val get_l : Sym.t -> Context.basetype_or_value m + + val add_a : Sym.t -> BT.t -> Context.l_info -> unit m + + val add_l : Sym.t -> BT.t -> Context.l_info -> unit m + + val get_struct_decl : Loc.t -> Sym.t -> Memory.struct_layout m + + val get_struct_member_type : Loc.t -> Sym.t -> Id.t -> Sctypes.ctype m + + val get_datatype : Loc.t -> Sym.t -> BT.dt_info m + + val get_datatype_constr : Loc.t -> Sym.t -> BT.constr_info m + + val get_resource_predicate_def : Loc.t -> Sym.t -> Definition.Predicate.t m + + val get_logical_function_def : Loc.t -> Sym.t -> Definition.Function.t m + + val get_lemma : Loc.t -> Sym.t -> (Cerb_location.t * ArgumentTypes.lemmat) m + + val get_fun_decl + : Loc.t -> + Sym.t -> + (Loc.t * ArgumentTypes.ft option * Sctypes.c_concrete_sig) m + + val ensure_base_type : Loc.t -> expect:BT.t -> BT.t -> unit m + + val lift : 'a Or_TypeError.t -> 'a m +end + +open (Typing : NoSolver) + +let fail typeErr = fail (fun _ -> typeErr) open Effectful.Make (Typing) let use_ity = ref true -let ensure_base_type = Typing.ensure_base_type - -let illtyped_index_term (loc : Locations.t) it has ~expected ~reason (_ctxt, _log) = +let illtyped_index_term (loc : Locations.t) it has ~expected ~reason = let reason = match reason with | Either.Left reason -> @@ -32,16 +72,14 @@ let illtyped_index_term (loc : Locations.t) it has ~expected ~reason (_ctxt, _lo head ^ "\n" ^ pos | Either.Right reason -> reason in - { loc; - msg = TypeErrors.Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason } - } + TypeErrors. + { loc; msg = Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason } } let ensure_bits_type (loc : Loc.t) (has : BT.t) = match has with | BT.Bits (_sign, _n) -> return () - | has -> - fail (fun _ -> { loc; msg = Mismatch { has = BT.pp has; expect = !^"bitvector" } }) + | has -> fail { loc; msg = Mismatch { has = BT.pp has; expect = !^"bitvector" } } let ensure_z_fits_bits_type loc (sign, n) v = @@ -49,7 +87,7 @@ let ensure_z_fits_bits_type loc (sign, n) v = return () else ( let err = !^"Value" ^^^ Pp.z v ^^^ !^"does not fit" ^^^ BT.pp (Bits (sign, n)) in - fail (fun _ -> { loc; msg = Generic err })) + fail { loc; msg = Generic err }) let ensure_arith_type ~reason it = @@ -117,9 +155,9 @@ let ensure_same_argument_number loc input_output has ~expect = return () else ( match input_output with - | `General -> fail (fun _ -> { loc; msg = Number_arguments { has; expect } }) - | `Input -> fail (fun _ -> { loc; msg = Number_input_arguments { has; expect } }) - | `Output -> fail (fun _ -> { loc; msg = Number_output_arguments { has; expect } })) + | `General -> fail { loc; msg = Number_arguments { has; expect } } + | `Input -> fail { loc; msg = Number_input_arguments { has; expect } } + | `Output -> fail { loc; msg = Number_output_arguments { has; expect } }) let compare_by_fst_id (x, _) (y, _) = Id.compare x y @@ -132,13 +170,13 @@ let correct_members loc (spec : (Id.t * 'a) list) (have : (Id.t * 'b) list) = if IdSet.mem id needed then return (IdSet.remove id needed) else - fail (fun _ -> { loc; msg = Unexpected_member (List.map fst spec, id) })) + fail { loc; msg = Unexpected_member (List.map fst spec, id) }) needed have in match IdSet.elements needed with | [] -> return () - | missing :: _ -> fail (fun _ -> { loc; msg = Missing_member missing }) + | missing :: _ -> fail { loc; msg = Missing_member missing } let correct_members_sorted_annotated loc spec have = @@ -206,8 +244,8 @@ module WBT = struct match BT.pick_integer_encoding_type z with | Some bt -> return bt | None -> - fail (fun _ -> - { loc; msg = Generic (Pp.item "no standard encoding type for constant" (Pp.z z)) }) + fail + { loc; msg = Generic (Pp.item "no standard encoding type for constant" (Pp.z z)) } end module WCT = struct @@ -228,6 +266,7 @@ module WCT = struct end module WIT = struct + module LC = LogicalConstraints open BaseTypes open IndexTerms @@ -280,7 +319,7 @@ module WIT = struct | [] -> assert (List.for_all (function [] -> true | _ -> false) cases); (match cases with - | [] -> fail (fun _ -> { loc; msg = Generic !^"Incomplete pattern" }) + | [] -> fail { loc; msg = Generic !^"Incomplete pattern" } | _ -> return ()) (* | [_(\*[]*\)] -> return () *) (* | _::_::_ -> fail (fun _ -> {loc; msg = Generic !^"Duplicate pattern"}) *) @@ -358,7 +397,7 @@ module WIT = struct ^/^ !^prev_pos ^^ !^suggestion in - fail (fun _ -> { loc = pat_loc; msg = Redundant_pattern err })) + fail { loc = pat_loc; msg = Redundant_pattern err }) [] pats in @@ -367,7 +406,7 @@ module WIT = struct let rec get_location_for_type = function | IT (Apply (name, _args), _, loc) -> - let@ def = Typing.get_logical_function_def loc name in + let@ def = get_logical_function_def loc name in return def.loc | IT ((MapSet (t, _, _) | Let (_, t)), _, _) -> get_location_for_type t | IT (Cons (it, _), _, _) | it -> return @@ IT.get_loc it @@ -389,7 +428,7 @@ module WIT = struct match () with | () when is_a -> get_a s | () when is_l -> get_l s - | () -> fail (fun _ -> { loc; msg = TE.Unknown_variable s }) + | () -> fail { loc; msg = TypeErrors.Unknown_variable s } in (match binding with | BaseType bt -> return (IT (Sym s, bt, loc)) @@ -718,10 +757,10 @@ module WIT = struct let@ () = match (IT.get_bt t, cbt) with | Integer, Loc () -> - fail (fun _ -> + fail { loc; msg = Generic !^"cast from integer not allowed in bitvector version" - }) + } | Loc (), Alloc_id -> return () | Integer, Real -> return () | Real, Integer -> return () @@ -741,7 +780,7 @@ module WIT = struct ^^^ BT.pp target ^^ dot in - fail (fun _ -> { loc; msg = Generic msg }) + fail { loc; msg = Generic msg } in return (IT (Cast (cbt, t), cbt, loc)) | MemberShift (t, tag, member) -> @@ -853,14 +892,14 @@ module WIT = struct if BT.equal ix_bt (IT.get_bt i) then return () else - fail (fun _ -> + fail { loc; msg = Generic (Pp.item "array_to_list: index type disagreement" (Pp.list IT.pp_with_typ [ i; arr ])) - }) + } in return (IT (ArrayToList (arr, i, len), BT.List bt, loc)) | MapConst (index_bt, t) -> @@ -886,7 +925,7 @@ module WIT = struct let@ body = infer body in return (IT (MapDef ((s, abt), body), Map (abt, IT.get_bt body), loc))) | Apply (name, args) -> - let@ def = Typing.get_logical_function_def loc name in + let@ def = get_logical_function_def loc name in let has_args, expect_args = (List.length args, List.length def.args) in let@ () = ensure_same_argument_number loc `General has_args ~expect:expect_args in let@ args = @@ -902,7 +941,7 @@ module WIT = struct let@ t1 = infer t1 in pure (let@ () = add_l name (IT.get_bt t1) (loc, lazy (Pp.string "let-var")) in - let@ () = add_c loc (LC.T (IT.def_ name t1 loc)) in + (* let@ () = add_c loc (LC.T (IT.def_ name t1 loc)) in *) let@ t2 = infer t2 in return (IT (Let ((name, t1), t2), IT.get_bt t2, loc))) | Constructor (s, args) -> @@ -937,7 +976,7 @@ module WIT = struct let@ () = cases_necessary (List.map (fun (pat, _) -> pat) cases) in let@ rbt = match rbt with - | None -> fail (fun _ -> { loc; msg = Empty_pattern }) + | None -> fail { loc; msg = Empty_pattern } | Some rbt -> return rbt in return (IT (Match (e, cases), rbt, loc)) @@ -965,7 +1004,7 @@ let warn_when_not_quantifier_bt (ident : string) (loc : Locations.t) (bt : BaseTypes.t) - (sym : document option) + (sym : Pp.document option) : unit = if not (BT.equal bt quantifier_bt) then @@ -981,6 +1020,7 @@ let warn_when_not_quantifier_bt module WReq = struct + module Req = Request open IndexTerms let welltyped loc r = @@ -989,7 +1029,7 @@ module WReq = struct match Req.get_name r with | Owned (_ct, _init) -> return [] | PName name -> - let@ def = Typing.get_resource_predicate_def loc name in + let@ def = get_resource_predicate_def loc name in return def.iargs in match r with @@ -1023,16 +1063,16 @@ module WReq = struct if Z.lt Z.zero z then return step else - fail (fun _ -> + fail { loc; msg = Generic (!^"Iteration step" ^^^ IT.pp p.step ^^^ !^"must be positive") - }) + } | IT (SizeOf _, _, _) -> return step | IT (Cast (_, IT (SizeOf _, _, _)), _, _) -> return step | _ -> let hint = "Only constant iteration steps are allowed." in - fail (fun _ -> { loc; msg = NIA { it = p.step; hint } }) + fail { loc; msg = NIA { it = p.step; hint } } in (*let@ () = match p.name with | (Owned (ct, _init)) -> let sz = Memory.size_of_ctype ct in if IT.equal step (IT.int_lit_ sz (snd p.q)) then return () else fail (fun _ @@ -1085,23 +1125,22 @@ module WReq = struct { name = p.name; pointer; q = p.q; q_loc = p.q_loc; step; permission; iargs }) end -let oarg_bt_of_pred loc = function - | Req.Owned (ct, _init) -> return (Memory.bt_of_sct ct) - | Req.PName pn -> - let@ def = Typing.get_resource_predicate_def loc pn in - return def.oarg_bt +module WRS = struct + let oarg_bt_of_pred loc = function + | Request.Owned (ct, _init) -> return (Memory.bt_of_sct ct) + | Request.PName pn -> + let@ def = get_resource_predicate_def loc pn in + return def.oarg_bt -let oarg_bt loc = function - | Req.P pred -> oarg_bt_of_pred loc pred.name - | Req.Q pred -> - let@ item_bt = oarg_bt_of_pred loc pred.name in - return (BT.make_map_bt (snd pred.q) item_bt) + let oarg_bt loc = function + | Request.P pred -> oarg_bt_of_pred loc pred.name + | Request.Q pred -> + let@ item_bt = oarg_bt_of_pred loc pred.name in + return (BT.make_map_bt (snd pred.q) item_bt) -module WRS = struct let welltyped loc (resource, bt) = - Pp.(debug 6 (lazy !^__LOC__)); let@ resource = WReq.welltyped loc resource in let@ bt = WBT.is_bt loc bt in let@ oarg_bt = oarg_bt loc resource in @@ -1110,7 +1149,7 @@ module WRS = struct end module WLC = struct - type t = LogicalConstraints.t + module LC = LogicalConstraints let welltyped loc lc = match lc with @@ -1127,66 +1166,87 @@ module WLC = struct end module WLRT = struct + module LC = LogicalConstraints module LRT = LogicalReturnTypes - open LRT - type t = LogicalReturnTypes.t - - let welltyped loc lrt = + let consistent loc lrt = + let open Typing in let rec aux = let here = Locations.other __LOC__ in function - | Define ((s, it), ((loc, _) as info), lrt) -> + | LRT.Define ((s, it), ((loc, _) as info), lrt) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) - let@ it = WIT.infer it in let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in + aux lrt + | Resource ((s, (re, re_oa_spec)), (loc, _), lrt) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in + let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in + aux lrt + | Constraint (lc, info, lrt) -> + (* TODO abort early if one of the constraints is the literal fase, + so that users are allowed to write such specs *) + let@ () = add_c (fst info) lc in + aux lrt + | I -> + let@ provable = provable loc in + let here = Locations.other __LOC__ in + (match provable (LC.T (IT.bool_ false here)) with + | `True -> + fail (fun ctxt_log -> + { loc; msg = Inconsistent_assumptions ("return type", ctxt_log) }) + | `False -> return ()) + in + pure (aux lrt) + + + let welltyped _loc lrt = + let rec aux = function + | LRT.Define ((s, it), ((loc, _) as info), lrt) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ it = WIT.infer it in + let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in let@ lrt = aux lrt in - return (Define ((s, it), info, lrt)) + return (LRT.Define ((s, it), info, lrt)) | Resource ((s, (re, re_oa_spec)), ((loc, _) as info), lrt) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) let@ re, re_oa_spec = WRS.welltyped loc (re, re_oa_spec) in let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in - let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in let@ lrt = aux lrt in - return (Resource ((s, (re, re_oa_spec)), info, lrt)) + return (LRT.Resource ((s, (re, re_oa_spec)), info, lrt)) | Constraint (lc, info, lrt) -> let@ lc = WLC.welltyped (fst info) lc in - let@ () = add_c (fst info) lc in let@ lrt = aux lrt in - return (Constraint (lc, info, lrt)) - | I -> - let@ provable = provable loc in - let here = Locations.other __LOC__ in - let@ () = - match provable (LC.T (IT.bool_ false here)) with - | `True -> - fail (fun ctxt_log -> - { loc; msg = Inconsistent_assumptions ("return type", ctxt_log) }) - | `False -> return () - in - return I + return (LRT.Constraint (lc, info, lrt)) + | I -> return LRT.I in pure (aux lrt) end module WRT = struct - type t = ReturnTypes.t - let subst = ReturnTypes.subst let pp = ReturnTypes.pp + let consistent loc rt = + pure + (match rt with + | ReturnTypes.Computational ((name, bt), info, lrt) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in + WLRT.consistent loc lrt) + + let welltyped loc rt = - Pp.(debug 6 (lazy !^__LOC__)); pure (match rt with - | RT.Computational ((name, bt), info, lrt) -> + | ReturnTypes.Computational ((name, bt), info, lrt) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) let@ bt = WBT.is_bt (fst info) bt in let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in let@ lrt = WLRT.welltyped loc lrt in - return (RT.Computational ((name, bt), info, lrt))) + return (ReturnTypes.Computational ((name, bt), info, lrt))) end (* module WFalse = struct *) @@ -1200,13 +1260,18 @@ end (* end *) let pure_and_no_initial_resources loc m = + let open Typing in pure (let@ (), _ = map_and_fold_resources loc (fun _re () -> (Deleted, ())) () in m) module WLAT = struct - let welltyped i_welltyped i_pp kind loc (at : 'i LAT.t) : 'i LAT.t m = + module LC = LogicalConstraints + module LAT = LogicalArgumentTypes + + let consistent i_welltyped i_pp kind loc (at : 'i LAT.t) : unit m = + let open Typing in debug 12 (lazy @@ -1216,23 +1281,17 @@ module WLAT = struct function | LAT.Define ((s, it), info, at) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) - let@ it = WIT.infer it in let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in - let@ at = aux at in - return (LAT.Define ((s, it), info, at)) - | LAT.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) -> + aux at + | LAT.Resource ((s, (re, re_oa_spec)), (loc, _), at) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) - let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in - let@ at = aux at in - return (LAT.Resource ((s, (re, re_oa_spec)), info, at)) + aux at | LAT.Constraint (lc, info, at) -> - let@ lc = WLC.welltyped (fst info) lc in let@ () = add_c (fst info) lc in - let@ at = aux at in - return (LAT.Constraint (lc, info, at)) + aux at | LAT.I i -> let@ provable = provable loc in let here = Locations.other __LOC__ in @@ -1243,6 +1302,34 @@ module WLAT = struct { loc; msg = Inconsistent_assumptions (kind, ctxt_log) }) | `False -> return () in + i_welltyped loc i + in + pure (aux at) + + + let welltyped i_welltyped i_pp kind loc (at : 'i LAT.t) : 'i LAT.t m = + debug + 12 + (lazy + (item ("checking wf of " ^ kind ^ " at " ^ Loc.to_string loc) (LAT.pp i_pp at))); + let rec aux = function + | LAT.Define ((s, it), info, at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ it = WIT.infer it in + let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in + let@ at = aux at in + return (LAT.Define ((s, it), info, at)) + | LAT.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in + let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in + let@ at = aux at in + return (LAT.Resource ((s, (re, re_oa_spec)), info, at)) + | LAT.Constraint (lc, info, at) -> + let@ lc = WLC.welltyped (fst info) lc in + let@ at = aux at in + return (LAT.Constraint (lc, info, at)) + | LAT.I i -> let@ i = i_welltyped loc i in return (LAT.I i) in @@ -1250,6 +1337,23 @@ module WLAT = struct end module WAT = struct + module AT = ArgumentTypes + + let consistent i_welltyped i_pp kind loc (at : 'i AT.t) : unit m = + debug + 12 + (lazy + (item ("checking wf of " ^ kind ^ " at " ^ Loc.to_string loc) (AT.pp i_pp at))); + let rec aux = function + | AT.Computational ((name, bt), info, at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in + aux at + | AT.L at -> WLAT.consistent i_welltyped i_pp kind loc at + in + pure (aux at) + + let welltyped i_welltyped i_pp kind loc (at : 'i AT.t) : 'i AT.t m = debug 12 @@ -1270,6 +1374,12 @@ module WAT = struct end module WFT = struct + let consistent = + WAT.consistent + (fun loc rt -> pure_and_no_initial_resources loc (WRT.consistent loc rt)) + WRT.pp + + let welltyped = WAT.welltyped (fun loc rt -> pure_and_no_initial_resources loc (WRT.welltyped loc rt)) @@ -1286,6 +1396,10 @@ end (pd.oargs)) *) module WLArgs = struct + module LC = LogicalConstraints + module LAT = LogicalArgumentTypes + module Mu = Mucore + let rec typ ityp = function | Mu.Define (bound, info, lat) -> LAT.Define (bound, info, typ ityp lat) | Mu.Resource (bound, info, lat) -> LAT.Resource (bound, info, typ ityp lat) @@ -1293,32 +1407,26 @@ module WLArgs = struct | Mu.I i -> LAT.I (ityp i) - let welltyped (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments_l) - : 'j Mu.arguments_l m + let consistent (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments_l) + : unit m = + let open Typing in let rec aux = let here = Locations.other __LOC__ in - Pp.(debug 6 (lazy !^__LOC__)); function | Mu.Define ((s, it), ((loc, _) as info), at) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) - let@ it = WIT.infer it in let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in - let@ at = aux at in - return (Mu.Define ((s, it), info, at)) - | Mu.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) -> + aux at + | Mu.Resource ((s, (re, re_oa_spec)), (loc, _), at) -> (* no need to alpha-rename, because context.ml ensures there's no name clashes *) - let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in - let@ at = aux at in - return (Mu.Resource ((s, (re, re_oa_spec)), info, at)) + aux at | Mu.Constraint (lc, info, at) -> - let@ lc = WLC.welltyped (fst info) lc in let@ () = add_c (fst info) lc in - let@ at = aux at in - return (Mu.Constraint (lc, info, at)) + aux at | Mu.I i -> let@ provable = provable loc in let here = Locations.other __LOC__ in @@ -1329,6 +1437,32 @@ module WLArgs = struct { loc; msg = Inconsistent_assumptions (kind, ctxt_log) }) | `False -> return () in + i_welltyped loc i + in + pure (aux at) + + + let welltyped (i_welltyped : Loc.t -> 'i -> 'j m) _kind loc (at : 'i Mu.arguments_l) + : 'j Mu.arguments_l m + = + let rec aux = function + | Mu.Define ((s, it), ((loc, _) as info), at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ it = WIT.infer it in + let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in + let@ at = aux at in + return (Mu.Define ((s, it), info, at)) + | Mu.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in + let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in + let@ at = aux at in + return (Mu.Resource ((s, (re, re_oa_spec)), info, at)) + | Mu.Constraint (lc, info, at) -> + let@ lc = WLC.welltyped (fst info) lc in + let@ at = aux at in + return (Mu.Constraint (lc, info, at)) + | Mu.I i -> let@ i = i_welltyped loc i in return (Mu.I i) in @@ -1336,11 +1470,34 @@ module WLArgs = struct end module WArgs = struct + module AT = ArgumentTypes + module Mu = Mucore + let rec typ ityp = function | Mu.Computational (bound, info, at) -> AT.Computational (bound, info, typ ityp at) | Mu.L lat -> AT.L (WLArgs.typ ityp lat) + let consistent : (Loc.t -> 'i -> 'j m) -> string -> Loc.t -> 'i Mu.arguments -> unit m = + fun (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments) -> + debug 6 (lazy !^__LOC__); + debug + 12 + (lazy + (item + ("checking consistency of " ^ kind ^ " at " ^ Loc.to_string loc) + (CF.Pp_ast.pp_doc_tree + (Mucore.dtree_of_arguments (fun _i -> Dleaf !^"...") at)))); + let rec aux = function + | Mu.Computational ((name, bt), info, at) -> + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in + aux at + | Mu.L at -> WLArgs.consistent i_welltyped kind loc at + in + pure (aux at) + + let welltyped : 'i 'j. (Loc.t -> 'i -> 'j m) -> string -> Loc.t -> 'i Mu.arguments -> 'j Mu.arguments m @@ -1369,7 +1526,6 @@ module WArgs = struct end module BaseTyping = struct - open Typing open TypeErrors module BT = BaseTypes module RT = ReturnTypes @@ -1379,7 +1535,7 @@ module BaseTyping = struct type label_context = (AT.lt * Where.label * Locations.t) Sym.Map.t let check_against_core_bt loc msg2 cbt bt = - Typing.lift + lift (CoreTypeChecks.check_against_core_bt (fun msg -> Or_TypeError.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) }) @@ -1387,6 +1543,8 @@ module BaseTyping = struct bt) + module Mu = Mucore + let rec check_and_bind_pattern bt = function | Mu.Pattern (loc, anns, _, p_) -> let@ p_ = check_and_bind_pattern_ bt loc p_ in @@ -1412,8 +1570,7 @@ module BaseTyping = struct match BT.is_list_bt bt with | Some bt -> return bt | None -> - fail (fun _ -> - { loc; msg = Generic (Pp.item "list pattern match against" (BT.pp bt)) }) + fail { loc; msg = Generic (Pp.item "list pattern match against" (BT.pp bt)) } in let@ ctor, pats = match (ctor, pats) with @@ -1421,22 +1578,20 @@ module BaseTyping = struct let@ _item_bt = get_item_bt bt in return (Mu.Cnil cbt, []) | Cnil _, _ -> - fail (fun _ -> - { loc; msg = Number_arguments { has = List.length pats; expect = 0 } }) + fail { loc; msg = Number_arguments { has = List.length pats; expect = 0 } } | Ccons, [ p1; p2 ] -> let@ item_bt = get_item_bt bt in let@ p1 = check_and_bind_pattern item_bt p1 in let@ p2 = check_and_bind_pattern bt p2 in return (Mu.Ccons, [ p1; p2 ]) | Ccons, _ -> - fail (fun _ -> - { loc; msg = Number_arguments { has = List.length pats; expect = 2 } }) + fail { loc; msg = Number_arguments { has = List.length pats; expect = 2 } } | Ctuple, pats -> let@ bts = match BT.is_tuple_bt bt with | Some bts when List.length bts == List.length pats -> return bts | _ -> - fail (fun _ -> + fail { loc; msg = Generic @@ -1444,7 +1599,7 @@ module BaseTyping = struct (Int.to_string (List.length pats) ^ "-length tuple pattern match against") (BT.pp bt)) - }) + } in let@ pats = ListM.map2M check_and_bind_pattern bts pats in return (Mu.Ctuple, pats) @@ -1499,12 +1654,12 @@ module BaseTyping = struct if BT.fits_range (Option.get (BT.is_bits_bt bt)) z then return (Mu.OV (bt, OVinteger iv)) else - fail (fun _ -> + fail { loc; msg = Generic (!^"Value " ^^^ Pp.z z ^^^ !^"does not fit in expected type" ^^^ BT.pp bt) - }) + } | _ -> let@ ov = infer_object_value loc ov_original in let@ () = ensure_base_type loc ~expect:bt (Mu.bt_of_object_value ov) in @@ -1575,9 +1730,7 @@ module BaseTyping = struct let rec infer_pexpr : 'TY. 'TY Mu.pexpr -> BT.t Mu.pexpr m = fun pe -> let open Mu in - Pp.debug - 22 - (lazy (Pp.item "WellTyped.BaseTyping.infer_pexpr" (Pp_mucore_ast.pp_pexpr pe))); + Pp.debug 22 (lazy (Pp.item __FUNCTION__ (Pp_mucore_ast.pp_pexpr pe))); let (Pexpr (loc, annots, _, pe_)) = pe in match integer_annot annots with | Some ity when !use_ity -> @@ -1703,8 +1856,8 @@ module BaseTyping = struct let@ () = ensure_base_type loc ~expect:(List ibt) (bt_of_pexpr xs) in return (bt_of_pexpr xs) | _ -> - fail (fun _ -> - { loc; msg = Number_arguments { has = List.length pes; expect = 2 } })) + fail + { loc; msg = Number_arguments { has = List.length pes; expect = 2 } }) | Ctuple -> return (BT.Tuple (List.map bt_of_pexpr pes)) | Carray -> let ibt = bt_of_pexpr (List.hd pes) in @@ -1796,21 +1949,21 @@ module BaseTyping = struct let@ () = ensure_bits_type loc bt in return bt | None, _ -> - fail (fun _ -> + fail { loc; msg = Generic (Pp.item "untypeable mucore function" (Pp_mucore_ast.pp_pexpr orig_pe)) - }) + } | Some `Returns_Integer, None -> - fail (fun _ -> + fail { loc; msg = Generic (Pp.item "mucore function requires type-annotation" (Pp_mucore_ast.pp_pexpr orig_pe)) - }) + } in return (bt, pexps) @@ -1819,10 +1972,7 @@ module BaseTyping = struct let open Cnprog in Pp.debug 22 - (lazy - (Pp.item - "WellTyped.check_cn_statement" - (CF.Pp_ast.pp_doc_tree (dtree_of_statement stmt)))); + (lazy (Pp.item __FUNCTION__ (CF.Pp_ast.pp_doc_tree (dtree_of_statement stmt)))); match stmt with | Pack_unpack (pack_unpack, pt) -> let@ p_pt = WReq.welltyped loc (P pt) in @@ -1886,7 +2036,7 @@ module BaseTyping = struct let wrong_number_arguments () = let has = List.length its in let expect = AT.count_computational lemma_typ in - fail (fun _ -> { loc; msg = Number_arguments { has; expect } }) + fail { loc; msg = Number_arguments { has; expect } } in let rec check_args lemma_typ its = match (lemma_typ, its) with @@ -1935,9 +2085,7 @@ module BaseTyping = struct let rec infer_expr : 'TY. label_context -> 'TY Mu.expr -> BT.t Mu.expr m = fun label_context e -> let open Mu in - Pp.debug - 22 - (lazy (Pp.item "WellTyped.BaseTyping.infer_expr" (Pp_mucore_ast.pp_expr e))); + Pp.debug 22 (lazy (Pp.item __FUNCTION__ (Pp_mucore_ast.pp_expr e))); let (Expr (loc, annots, _, e_)) = e in match integer_annot annots with | Some ity when !use_ity -> @@ -2062,12 +2210,12 @@ module BaseTyping = struct assert (not is_variadic); return (snd ret_v_ct, List.map fst arg_r_cts) | _ -> - fail (fun _ -> + fail { loc; msg = Generic (Pp.item "not a function pointer at call-site" (Sctypes.pp act.ct)) - }) + } in let@ f_pe = check_pexpr (Loc ()) f_pe in (* TODO: we'd have to check the arguments against the function type, but we @@ -2116,16 +2264,14 @@ module BaseTyping = struct (* copying from check.ml *) let@ lt, _lkind = match Sym.Map.find_opt l label_context with - | None -> - fail (fun _ -> - { loc; msg = Generic (!^"undefined code label" ^/^ Sym.pp l) }) + | None -> fail { loc; msg = Generic (!^"undefined code label" ^/^ Sym.pp l) } | Some (lt, lkind, _) -> return (lt, lkind) in let@ pes = let wrong_number_arguments () = let has = List.length pes in let expect = AT.count_computational lt in - fail (fun _ -> { loc; msg = Number_arguments { has; expect } }) + fail { loc; msg = Number_arguments { has; expect } } in let rec check_args lt pes = match (lt, pes) with @@ -2173,16 +2319,23 @@ module BaseTyping = struct end module WLabel = struct - open Mu + open Mucore let typ l = WArgs.typ (fun _body -> False.False) l + let consistent (loc : Loc.t) (lt : _ expr arguments) : unit m = + WArgs.consistent (fun _loc _body -> return ()) "loop/label" loc lt + + let welltyped (loc : Loc.t) (lt : _ expr arguments) : _ expr arguments m = WArgs.welltyped (fun _loc body -> return body) "loop/label" loc lt end module WProc = struct - open Mu + module AT = ArgumentTypes + module LAT = LogicalArgumentTypes + module Mu = Mucore + open Mucore let label_context function_rt label_defs = Pmap.fold @@ -2205,9 +2358,42 @@ module WProc = struct let typ p = WArgs.typ (fun (_body, _labels, rt) -> rt) p + let consistent : Loc.t -> _ Mu.args_and_body -> unit m = + fun (loc : Loc.t) (at : 'TY1 Mu.args_and_body) -> + WArgs.consistent + (fun loc (_body, labels, rt) -> + let@ () = pure_and_no_initial_resources loc (WRT.consistent loc rt) in + let@ () = + PmapM.iterM + (fun _sym def -> + match def with + | Return _ -> return () + | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) -> + pure_and_no_initial_resources + loc + (WLabel.consistent loc label_args_and_body)) + labels + in + PmapM.iterM + (fun _sym def -> + match def with + | Return _ -> return () + | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) -> + pure_and_no_initial_resources + loc + (WArgs.consistent + (fun _loc _label_body -> return ()) + "label" + loc + label_args_and_body)) + labels) + "function" + loc + at + + let welltyped : Loc.t -> _ Mu.args_and_body -> _ Mu.args_and_body m = fun (loc : Loc.t) (at : 'TY1 Mu.args_and_body) -> - Pp.(debug 6 (lazy !^__LOC__)); WArgs.welltyped (fun loc (body, labels, rt) -> let@ rt = pure_and_no_initial_resources loc (WRT.welltyped loc rt) in @@ -2255,6 +2441,45 @@ module WProc = struct end module WRPD = struct + module Def = Definition + module LC = LogicalConstraints + + let consistent Def.Predicate.{ loc; pointer; iargs; oarg_bt = _; clauses } = + let open Typing in + (* no need to alpha-rename, because context.ml ensures there's no name clashes *) + pure + (let@ () = add_l pointer BT.(Loc ()) (loc, lazy (Pp.string "ptr-var")) in + let@ () = + ListM.iterM (fun (s, bt) -> add_l s bt (loc, lazy (Pp.string "input-var"))) iargs + in + match clauses with + | None -> return () + | Some clauses -> + let@ _ = + ListM.fold_leftM + (fun acc Def.Clause.{ loc; guard; packing_ft } -> + let here = Locations.other __LOC__ in + let negated_guards = + List.map (fun clause -> IT.not_ clause.Def.Clause.guard here) acc + in + pure + (let@ () = add_c loc (LC.T guard) in + let@ () = add_c loc (LC.T (IT.and_ negated_guards here)) in + let@ () = + WLAT.consistent + (fun _loc _it -> return ()) + IT.pp + "clause" + loc + packing_ft + in + return (acc @ [ Def.Clause.{ loc; guard; packing_ft } ]))) + [] + clauses + in + return ()) + + let welltyped Def.Predicate.{ loc; pointer; iargs; oarg_bt; clauses } = (* no need to alpha-rename, because context.ml ensures there's no name clashes *) pure @@ -2276,14 +2501,8 @@ module WRPD = struct ListM.fold_leftM (fun acc Def.Clause.{ loc; guard; packing_ft } -> let@ guard = WIT.check loc BT.Bool guard in - let here = Locations.other __LOC__ in - let negated_guards = - List.map (fun clause -> IT.not_ clause.Def.Clause.guard here) acc - in pure - (let@ () = add_c loc (LC.T guard) in - let@ () = add_c loc (LC.T (IT.and_ negated_guards here)) in - let@ packing_ft = + (let@ packing_ft = WLAT.welltyped (fun loc it -> WIT.check loc oarg_bt it) IT.pp @@ -2329,17 +2548,26 @@ module WLFD = struct end module WLemma = struct + let consistent loc _lemma_s lemma_typ = + WAT.consistent + (fun loc lrt -> pure_and_no_initial_resources loc (WLRT.consistent loc lrt)) + LogicalReturnTypes.pp + "lemma" + loc + lemma_typ + + let welltyped loc _lemma_s lemma_typ = WAT.welltyped (fun loc lrt -> pure_and_no_initial_resources loc (WLRT.welltyped loc lrt)) - LRT.pp + LogicalReturnTypes.pp "lemma" loc lemma_typ end module WDT = struct - open Mu + open Mucore let welltyped (dt_name, { loc; cases }) = let@ _ = @@ -2434,7 +2662,7 @@ module WDT = struct ^/^ !^"Indirect recursion via map, set, record," ^^^ !^"or tuple types is not permitted." in - fail (fun _ -> { loc; msg = Generic err })) + fail { loc; msg = Generic err }) args) cases) scc) diff --git a/tests/cn/implies3.error.c.verify b/tests/cn/implies3.error.c.verify index 6958a7939..2d7b1bede 100644 --- a/tests/cn/implies3.error.c.verify +++ b/tests/cn/implies3.error.c.verify @@ -1,5 +1,5 @@ return code: 1 -tests/cn/implies3.error.c:1:1: error: function makes inconsistent assumptions +tests/cn/implies3.error.c:1:1: error: proc/fun makes inconsistent assumptions int foo () ~~~~^~~~~~ State file: file:///tmp/state__implies3.error.c.html diff --git a/tests/cn/inconsistent.error.c.verify b/tests/cn/inconsistent.error.c.verify index 29136eb38..d0a2acb96 100644 --- a/tests/cn/inconsistent.error.c.verify +++ b/tests/cn/inconsistent.error.c.verify @@ -1,5 +1,5 @@ return code: 1 -tests/cn/inconsistent.error.c:1:1: error: function makes inconsistent assumptions +tests/cn/inconsistent.error.c:1:1: error: proc/fun makes inconsistent assumptions void f() ~~~~~^~~ State file: file:///tmp/state__inconsistent.error.c.html diff --git a/tests/cn/inconsistent2.error.c.verify b/tests/cn/inconsistent2.error.c.verify index 125c67455..845303060 100644 --- a/tests/cn/inconsistent2.error.c.verify +++ b/tests/cn/inconsistent2.error.c.verify @@ -2,6 +2,9 @@ return code: 1 tests/cn/inconsistent2.error.c:9:19: warning: 'each' expects a 'u64', but 'i' with type 'i32' was provided. This will become an error in the future. /*@ requires take f1 = each(i32 i; 0i32 <= i && i <= 0i32) { False(p + i, i) }; ^ +tests/cn/inconsistent2.error.c:12:22: warning: 'extract' expects a 'u64', but '0'i32' with type 'i32' was provided. This will become an error in the future. + /*@ extract False, 0i32; @*/ + ^ tests/cn/inconsistent2.error.c:8:1: error: return type makes inconsistent assumptions void f (int *p) ~~~~~^~~~~~~~~~