diff --git a/backend/cn/lib/builtins.ml b/backend/cn/lib/builtins.ml index 0ccf6ca3e..2d826a69d 100644 --- a/backend/cn/lib/builtins.ml +++ b/backend/cn/lib/builtins.ml @@ -2,24 +2,27 @@ module SBT = BaseTypes.Surface open Or_TypeError open IndexTerms +let fail_number_args loc ~has ~expect = + fail { loc; msg = WellTyped (Number_arguments { type_ = `Other; has; expect }) } + + (* builtin function symbols *) let mk_arg0 mk args loc = match args with | [] -> return (mk loc) - | _ :: _ as xs -> - fail { loc; msg = Number_arguments { has = List.length xs; expect = 0 } } + | _ :: _ as xs -> fail_number_args loc ~has:(List.length xs) ~expect:0 let mk_arg1 mk args loc = match args with | [ x ] -> return (mk x loc) - | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 1 } } + | xs -> fail_number_args loc ~has:(List.length xs) ~expect:1 let mk_arg2_err mk args loc = match args with | [ x; y ] -> mk (x, y) loc - | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 2 } } + | xs -> fail_number_args loc ~has:(List.length xs) ~expect:2 let mk_arg2 mk = mk_arg2_err (fun tup loc -> return (mk tup loc)) @@ -27,7 +30,7 @@ let mk_arg2 mk = mk_arg2_err (fun tup loc -> return (mk tup loc)) let mk_arg3_err mk args loc = match args with | [ x; y; z ] -> mk (x, y, z) loc - | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 3 } } + | xs -> fail_number_args loc ~has:(List.length xs) ~expect:3 let mk_arg3 mk = mk_arg3_err (fun tup loc -> return (mk tup loc)) @@ -35,7 +38,7 @@ let mk_arg3 mk = mk_arg3_err (fun tup loc -> return (mk tup loc)) let mk_arg5 mk args loc = match args with | [ a; b; c; d; e ] -> return (mk (a, b, c, d, e) loc) - | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 5 } } + | xs -> fail_number_args loc ~has:(List.length xs) ~expect:5 let min_bits_def (sign, n) = @@ -124,7 +127,9 @@ let array_to_list_def = let expected = "map/array" in fail { loc; - msg = Illtyped_it { it = pp arr; has = SBT.pp (get_bt arr); expected; reason } + msg = + WellTyped + (Illtyped_it { it = pp arr; has = SBT.pp (get_bt arr); expected; reason }) } | Some (_, bt) -> return (array_to_list_ (arr, i, len) bt loc)) ) diff --git a/backend/cn/lib/cLogicalFuns.ml b/backend/cn/lib/cLogicalFuns.ml index a97eac804..6769ff8b3 100644 --- a/backend/cn/lib/cLogicalFuns.ml +++ b/backend/cn/lib/cLogicalFuns.ml @@ -1,15 +1,14 @@ -open TypeErrors -open Typing - -open Effectful.Make (Typing) - module StringMap = Map.Make (String) module IntMap = Map.Make (Int) module CF = Cerb_frontend module BT = BaseTypes -open Cerb_pp_prelude module Mu = Mucore module IT = IndexTerms +open Cerb_pp_prelude +open TypeErrors +open Typing + +open Effectful.Make (Typing) let fail_n m = fail (fun _ctxt -> m) @@ -245,7 +244,7 @@ let rec symb_exec_pexpr ctxt var_map pexpr = | PEsym sym -> (match Sym.Map.find_opt sym var_map with | Some r -> return r - | _ -> fail_n { loc; msg = Unknown_variable sym }) + | _ -> fail_n { loc; msg = WellTyped (Unknown_variable sym) }) | PEval v -> (match val_to_it loc v with | Some r -> return r diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 8fdb6ffd1..bfa0383c9 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -42,13 +42,16 @@ let rec check_and_match_pattern (Mu.Pattern (loc, _, bty, pattern)) it = match bty with | BT.List item_bt -> return item_bt | _ -> - fail (fun _ -> { loc; msg = Mismatch { has = !^"list"; expect = BT.pp bty } }) + fail (fun _ -> + { loc; msg = WellTyped (Mismatch { has = !^"list"; expect = BT.pp bty }) }) in let@ () = add_c loc (LC.T (eq__ it (nil_ ~item_bt loc) loc)) in return [] | Ccons, [ p1; p2 ] -> - let@ () = ensure_base_type loc ~expect:bty (List (Mu.bt_of_pattern p1)) in - let@ () = ensure_base_type loc ~expect:bty (Mu.bt_of_pattern p2) in + let@ () = + WellTyped.ensure_base_type loc ~expect:bty (List (Mu.bt_of_pattern p1)) + in + let@ () = WellTyped.ensure_base_type loc ~expect:bty (Mu.bt_of_pattern p2) in let item_bt = Mu.bt_of_pattern p1 in let@ a1 = check_and_match_pattern p1 (head_ ~item_bt it loc) in let@ a2 = check_and_match_pattern p2 (tail_ it loc) in @@ -56,7 +59,10 @@ let rec check_and_match_pattern (Mu.Pattern (loc, _, bty, pattern)) it = return (a1 @ a2) | Ctuple, pats -> let@ () = - ensure_base_type loc ~expect:bty (Tuple (List.map Mu.bt_of_pattern pats)) + WellTyped.ensure_base_type + loc + ~expect:bty + (Tuple (List.map Mu.bt_of_pattern pats)) in let@ all_as = ListM.mapiM @@ -77,7 +83,7 @@ let check_computational_bound loc s = if is_bound then return () else - fail (fun _ -> { loc; msg = Unknown_variable s }) + fail (fun _ -> { loc; msg = WellTyped (Unknown_variable s) }) let unsupported loc doc = @@ -85,7 +91,7 @@ let unsupported loc doc = let check_ptrval (loc : Locations.t) ~(expect : BT.t) (ptrval : pointer_value) : IT.t m = - let@ () = ensure_base_type loc ~expect BT.(Loc ()) in + let@ () = WellTyped.ensure_base_type loc ~expect BT.(Loc ()) in CF.Impl_mem.case_ptrval ptrval (fun ct -> @@ -116,7 +122,7 @@ let expect_must_be_map_bt loc ~expect = match expect with | BT.Map (index_bt, item_bt) -> return (index_bt, item_bt) | _ -> - let msg = Mismatch { has = !^"array"; expect = BT.pp expect } in + let msg = WellTyped (Mismatch { has = !^"array"; expect = BT.pp expect }) in fail (fun _ -> { loc; msg }) @@ -130,7 +136,7 @@ let rec check_mem_value (loc : Locations.t) ~(expect : BT.t) (mem : mem_value) : (fun ity iv -> let@ () = WellTyped.check_ct loc (Integer ity) in let bt = Memory.bt_of_sct (Integer ity) in - let@ () = ensure_base_type loc ~expect bt in + let@ () = WellTyped.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 +150,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.check_ct loc (Struct tag) in - let@ () = ensure_base_type loc ~expect (Struct tag) in + let@ () = WellTyped.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 @@ -187,7 +193,9 @@ let ensure_bitvector_type (loc : Locations.t) ~(expect : BT.t) : (BT.sign * int) | None -> fail (fun _ -> { loc; - msg = Mismatch { has = !^"(unspecified) bitvector type"; expect = BT.pp expect } + msg = + WellTyped + (Mismatch { has = !^"(unspecified) bitvector type"; expect = BT.pp expect }) }) @@ -214,13 +222,14 @@ let rec check_object_value (loc : Locations.t) (Mu.OV (expect, ov)) : IT.t m = assert (Option.is_some (BT.is_bits_bt index_bt)); let@ () = ListM.iterM - (fun i -> ensure_base_type loc ~expect:item_bt (Mu.bt_of_object_value i)) + (fun i -> + WellTyped.ensure_base_type loc ~expect:item_bt (Mu.bt_of_object_value i)) items in let@ values = ListM.mapM (check_object_value loc) items in return (make_array_ ~index_bt ~item_bt values loc) | OVstruct (tag, fields) -> - let@ () = ensure_base_type loc ~expect (Struct tag) in + let@ () = WellTyped.ensure_base_type loc ~expect (Struct tag) in check_struct loc tag fields | OVunion (tag, id, mv) -> check_union loc tag id mv | OVfloating _iv -> unsupported loc !^"floats" @@ -229,38 +238,40 @@ let rec check_object_value (loc : Locations.t) (Mu.OV (expect, ov)) : IT.t m = let rec check_value (loc : Locations.t) (Mu.V (expect, v)) : IT.t m = match v with | Vobject ov -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_object_value ov) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_object_value ov) in check_object_value loc ov | Vctype ct -> - let@ () = ensure_base_type loc ~expect CType in + let@ () = WellTyped.ensure_base_type loc ~expect CType in let ct = Sctypes.of_ctype_unsafe loc ct in let@ () = WellTyped.check_ct loc ct in return (IT.const_ctype_ ct loc) | Vunit -> - let@ () = ensure_base_type loc ~expect Unit in + let@ () = WellTyped.ensure_base_type loc ~expect Unit in return (IT.unit_ loc) | Vtrue -> - let@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in return (IT.bool_ true loc) | Vfalse -> - let@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in return (IT.bool_ false loc) | Vfunction_addr sym -> - let@ () = ensure_base_type loc ~expect (Loc ()) in + let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in (* check it is a valid function address *) let@ _ = Global.get_fun_decl loc sym in return (IT.sym_ (sym, BT.(Loc ()), loc)) | Vlist (_item_cbt, vals) -> let item_bt = Mu.bt_of_value (List.hd vals) in - let@ () = ensure_base_type loc ~expect (List item_bt) in + let@ () = WellTyped.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 + ListM.iterM + (fun i -> WellTyped.ensure_base_type loc ~expect:item_bt (Mu.bt_of_value i)) + vals in let@ values = ListM.mapM (check_value loc) vals in return (list_ ~item_bt values ~nil_loc:loc) | Vtuple vals -> let item_bts = List.map Mu.bt_of_value vals in - let@ () = ensure_base_type loc ~expect (Tuple item_bts) in + let@ () = WellTyped.ensure_base_type loc ~expect (Tuple item_bts) in let@ values = ListM.mapM (check_value loc) vals in return (tuple_ values loc) @@ -412,11 +423,9 @@ let check_conv_int loc ~expect ct arg = let check_against_core_bt loc msg2 cbt bt = - Typing.lift - (CoreTypeChecks.check_against_core_bt - (fun msg -> Or_TypeError.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) }) - cbt - bt) + CoreTypeChecks.check_against_core_bt cbt bt + |> Result.map_error (fun msg -> { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) }) + |> Typing.lift let check_has_alloc_id loc ptr ub_unspec = @@ -511,27 +520,29 @@ 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@ () = ensure_base_type loc ~expect bt in + let@ () = WellTyped.ensure_base_type loc ~expect bt in k (sym_ (sym, bt, loc)) | Value lvt -> - let@ () = ensure_base_type loc ~expect (IT.get_bt lvt) in + let@ () = WellTyped.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 + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_value v) in let@ vt = check_value loc v in k vt | PEconstrained _ -> Cerb_debug.error "todo: PEconstrained" | PEctor (ctor, pes) -> (match (ctor, pes) with | Ctuple, _ -> - let@ () = ensure_base_type loc ~expect (Tuple (List.map Mu.bt_of_pexpr pes)) in + let@ () = + WellTyped.ensure_base_type loc ~expect (Tuple (List.map Mu.bt_of_pexpr pes)) + in check_pexprs pes (fun values -> k (tuple_ values loc)) | Carray, _ -> let@ index_bt, item_bt = expect_must_be_map_bt loc ~expect in assert (Option.is_some (BT.is_bits_bt index_bt)); let@ () = ListM.iterM - (fun i -> ensure_base_type loc ~expect:item_bt (Mu.bt_of_pexpr i)) + (fun i -> WellTyped.ensure_base_type loc ~expect:item_bt (Mu.bt_of_pexpr i)) pes in check_pexprs pes (fun values -> k (make_array_ ~index_bt ~item_bt values loc)) @@ -540,25 +551,33 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = match expect with | List item_bt -> return item_bt | _ -> - let msg = Mismatch { has = !^"list"; expect = BT.pp expect } in + let msg = WellTyped (Mismatch { has = !^"list"; expect = BT.pp expect }) in fail (fun _ -> { loc; msg }) in let@ () = check_against_core_bt loc !^"checking Cnil" item_cbt item_bt in k (nil_ ~item_bt loc) | Cnil _item_bt, _ -> fail (fun _ -> - { loc; msg = Number_arguments { has = List.length pes; expect = 0 } }) + { loc; + msg = + WellTyped + (Number_arguments { type_ = `Other; has = List.length pes; expect = 0 }) + }) | Ccons, [ pe1; pe2 ] -> - let@ () = ensure_base_type loc ~expect (List (Mu.bt_of_pexpr pe1)) in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in + let@ () = WellTyped.ensure_base_type loc ~expect (List (Mu.bt_of_pexpr pe1)) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun vt1 -> check_pexpr pe2 (fun vt2 -> k (cons_ (vt1, vt2) loc))) | Ccons, _ -> fail (fun _ -> - { loc; msg = Number_arguments { has = List.length pes; expect = 2 } })) + { loc; + msg = + WellTyped + (Number_arguments { type_ = `Other; has = List.length pes; expect = 2 }) + })) | PEbitwise_unop (unop, pe1) -> let@ _ = ensure_bitvector_type loc ~expect in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in check_pexpr pe1 (fun vt1 -> let unop = match unop with @@ -570,8 +589,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = k value) | PEbitwise_binop (binop, pe1, pe2) -> let@ _ = ensure_bitvector_type loc ~expect in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in let binop = match binop with BW_AND -> BW_And | BW_OR -> BW_Or | BW_XOR -> BW_Xor in @@ -582,9 +601,9 @@ 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@ () = ensure_base_type loc ~expect (Loc ()) in + let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in let@ () = WellTyped.check_ct loc ct in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun vt1 -> check_pexpr pe2 (fun vt2 -> @@ -608,8 +627,8 @@ 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@ () = ensure_base_type loc ~expect (Loc ()) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun vt -> let@ ct = Global.get_struct_member_type loc tag member in let result = memberShift_ (vt, tag, member) loc in @@ -627,15 +646,17 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in k result) | PEnot pe -> - let@ () = ensure_base_type loc ~expect Bool in - let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = WellTyped.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) -> let check_cmp_ty = function | BT.Integer | Bits _ | Real -> return () | ty -> fail (fun _ -> - { loc; msg = Mismatch { has = BT.pp ty; expect = !^"comparable type" } }) + { loc; + msg = WellTyped (Mismatch { has = BT.pp ty; expect = !^"comparable type" }) + }) in let not_yet x = Pp.debug 1 (lazy (Pp.item "not yet restored" (Pp_mucore_ast.pp_pexpr orig_pe))); @@ -643,7 +664,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in (match op with | OpDiv -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.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 +679,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@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.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,48 +694,63 @@ 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@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = - ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) + WellTyped.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@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) + WellTyped.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@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) + WellTyped.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@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) + WellTyped.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@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in let@ () = - ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2) + WellTyped.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@ () = 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 + 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 check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (and_ [ v1; v2 ] loc))) | OpOr -> - 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 + 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 check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (or_ [ v1; v2 ] loc))) | OpAdd -> not_yet "OpAdd" | OpSub -> @@ -728,7 +764,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = | PEapply_fun (fun_id, args) -> let@ () = match Mu.fun_return_type fun_id args with - | Some (`Returns_BT bt) -> ensure_base_type loc ~expect bt + | Some (`Returns_BT bt) -> WellTyped.ensure_base_type loc ~expect bt | Some `Returns_Integer -> WellTyped.ensure_bits_type loc expect | None -> fail (fun _ -> @@ -742,14 +778,11 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = let@ () = let has = List.length args in let expect = List.length expect_args in - if expect = has then - return () - else - fail (fun _ -> { loc; msg = Number_arguments { has; expect } }) + WellTyped.ensure_same_argument_number loc `Other has ~expect in let@ _ = ListM.map2M - (fun pe expect -> ensure_base_type loc ~expect (Mu.bt_of_pexpr pe)) + (fun pe expect -> WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe)) args expect_args in @@ -758,14 +791,17 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = k res) | PEstruct (tag, xs) -> let@ () = WellTyped.check_ct loc (Struct tag) in - let@ () = ensure_base_type loc ~expect (Struct tag) in + let@ () = WellTyped.ensure_base_type loc ~expect (Struct tag) in let@ layout = Global.get_struct_decl loc tag in let member_types = Memory.member_types layout in let@ _ = ListM.map2M (fun (id, ct) (id', pe') -> assert (Id.equal id id'); - ensure_base_type loc ~expect:(Memory.bt_of_sct ct) (Mu.bt_of_pexpr pe')) + WellTyped.ensure_base_type + loc + ~expect:(Memory.bt_of_sct ct) + (Mu.bt_of_pexpr pe')) member_types xs in @@ -774,8 +810,10 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = k (struct_ (tag, members) loc)) | PEunion _ -> Cerb_debug.error "todo: PEunion" | PEcfunction pe2 -> - let@ () = ensure_base_type loc ~expect (Tuple [ CType; List CType; Bool; Bool ]) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in + let@ () = + WellTyped.ensure_base_type loc ~expect (Tuple [ CType; List CType; Bool; Bool ]) + in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in check_pexpr pe2 (fun ptr -> let@ _global = get_global () in (* function vals are just symbols the same as the names of functions *) @@ -790,7 +828,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = | PEmemberof _ -> Cerb_debug.error "todo: PEmemberof" | PEbool_to_integer pe -> let@ _ = ensure_bitvector_type loc ~expect in - let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> k (ite_ (arg, int_lit_ 1 expect loc, int_lit_ 0 expect loc) loc)) | PEbounded_binop (Bound_Wrap act, iop, pe1, pe2) -> @@ -801,14 +839,14 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = match act.ct with | Integer ity when Sctypes.is_unsigned_integer_type ity -> true | _ -> false); - let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in + let@ () = WellTyped.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 let@ () = match iop with | IOpShl | IOpShr -> return () - | _ -> ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) + | _ -> WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun arg1 -> check_pexpr pe2 (fun arg2 -> @@ -843,14 +881,14 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = | PEbounded_binop (Bound_Except act, iop, pe1, pe2) -> let@ () = WellTyped.check_ct act.loc act.ct in let ity = match act.ct with Integer ity -> ity | _ -> assert false in - let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in + let@ () = WellTyped.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 let@ () = match iop with | IOpShl | IOpShr -> return () - | _ -> ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) + | _ -> WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe2) in let _, bits = Option.get (BT.is_bits_bt expect) in check_pexpr pe1 (fun arg1 -> @@ -889,12 +927,12 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = in k direct_x)) | PEconv_int (ct_expr, pe) | PEconv_loaded_int (ct_expr, pe) -> - let@ () = ensure_base_type loc ~expect:CType (Mu.bt_of_pexpr ct_expr) in + let@ () = WellTyped.ensure_base_type loc ~expect:CType (Mu.bt_of_pexpr ct_expr) in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe) in check_pexpr ct_expr (fun ct_it -> let@ ct = check_single_ct loc ct_it in let@ () = WellTyped.check_ct loc ct in - let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct ct) in + let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct ct) in check_pexpr pe (fun lvt -> let@ vt = check_conv_int loc ~expect ct lvt in k vt)) @@ -921,14 +959,14 @@ 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.check_ct act.loc act.ct in - let@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.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)) | PEif (pe, e1, e2) -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr e1) in - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr e2) in - let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr e1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr e2) in + let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in check_pexpr pe (fun c -> let aux e cond name = let@ () = add_c loc (LC.T cond) in @@ -950,8 +988,10 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m = let@ () = pure (aux e2 (not_ c here) "else") in return ()) | PElet (p, e1, e2) -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr e2) in - let@ () = ensure_base_type loc ~expect:(Mu.bt_of_pexpr e1) (Mu.bt_of_pattern p) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr e2) in + let@ () = + WellTyped.ensure_base_type loc ~expect:(Mu.bt_of_pexpr e1) (Mu.bt_of_pattern p) + in check_pexpr e1 (fun v1 -> let@ bound_a = check_and_match_pattern p v1 in check_pexpr e2 (fun lvt -> @@ -1064,7 +1104,7 @@ end = struct | _ -> let expect = count_computational original_ftyp in let has = List.length original_args in - fail (fun _ -> { loc; msg = Number_arguments { expect; has } }) + WellTyped.ensure_same_argument_number loc `Other has ~expect in fun args ftyp k -> aux [] args ftyp k in @@ -1072,7 +1112,9 @@ end = struct let check_arg_pexpr (pe : BT.t Mu.pexpr) ~expect k = - let@ () = ensure_base_type (Mu.loc_of_pexpr pe) ~expect (Mu.bt_of_pexpr pe) in + let@ () = + WellTyped.ensure_base_type (Mu.loc_of_pexpr pe) ~expect (Mu.bt_of_pexpr pe) + in check_pexpr pe k @@ -1318,12 +1360,12 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in (match e_ with | Epure pe -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe) in check_pexpr pe (fun lvt -> k lvt) | Ememop memop -> let here = Locations.other __LOC__ in let pointer_eq ?(negate = false) pe1 pe2 = - let@ () = ensure_base_type loc ~expect Bool in + let@ () = WellTyped.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 @@ -1394,9 +1436,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in let pointer_op op pe1 pe2 = let ub = CF.Undefined.UB053_distinct_aggregate_union_pointer_comparison in - let@ () = ensure_base_type loc ~expect Bool in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun arg1 -> check_pexpr pe2 (fun arg2 -> let@ () = check_both_eq_alloc loc arg1 arg2 ub in @@ -1412,9 +1454,15 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | PtrGe (pe1, pe2) -> pointer_op (Fun.flip gePointer_ loc) pe1 pe2 | Ptrdiff (act, pe1, pe2) -> let@ () = WellTyped.check_ct act.loc act.ct in - let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct (Integer Ptrdiff_t)) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in + let@ () = + WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct (Integer Ptrdiff_t)) + in + let@ () = + WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) + in + let@ () = + WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) + in check_pexpr pe1 (fun arg1 -> check_pexpr pe2 (fun arg2 -> (* copying and adapting from memory/concrete/impl_mem.ml *) @@ -1443,8 +1491,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ () = WellTyped.check_ct act_from.loc act_from.ct in let@ () = WellTyped.check_ct act_to.loc act_to.ct in assert (match act_to.ct with Integer _ -> true | _ -> false); - let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act_to.ct) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct act_to.ct) in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> let actual_value = cast_ (Memory.bt_of_sct act_to.ct) arg loc in (* NOTE: After discussing with Kavyan @@ -1469,9 +1517,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.check_ct act_from.loc act_from.ct in let@ () = WellTyped.check_ct act_to.loc act_to.ct in - let@ () = ensure_base_type loc ~expect (Loc ()) in + let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in let@ () = - ensure_base_type + WellTyped.ensure_base_type loc ~expect:(Memory.bt_of_sct act_from.ct) (Mu.bt_of_pexpr pe) @@ -1496,8 +1544,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.check_ct act.loc act.ct in - let@ () = ensure_base_type loc ~expect Bool in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = WellTyped.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 -> @@ -1511,8 +1559,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.check_ct act.loc act.ct in - let@ () = ensure_base_type loc ~expect Bool in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect Bool in + let@ () = WellTyped.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 *) @@ -1520,8 +1568,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let result = aligned_ (arg, act.ct) loc in k result) | PtrArrayShift (pe1, act, pe2) -> - let@ () = ensure_base_type loc ~expect (Loc ()) in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in + let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in + let@ () = + WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) + in let@ () = WellTyped.check_ct act.loc act.ct in let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in check_pexpr pe1 (fun vt1 -> @@ -1545,8 +1595,12 @@ 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@ () = 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 + 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 check_pexpr pe1 (fun vt1 -> check_pexpr pe2 (fun vt2 -> let unspec = CF.Undefined.UB_unspec_copy_alloc_id in @@ -1571,7 +1625,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.check_ct act.loc act.ct in - let@ () = ensure_base_type loc ~expect (Loc ()) in + let@ () = WellTyped.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 = @@ -1622,8 +1676,8 @@ 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.check_ct loc ct in - let@ () = ensure_base_type loc ~expect Unit in - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in + let@ () = WellTyped.ensure_base_type loc ~expect Unit in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> let@ _ = RI.Special.predicate_request @@ -1638,10 +1692,15 @@ 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.check_ct act.loc act.ct 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 Unit 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) (Mu.bt_of_pexpr v_pe) + WellTyped.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 -> @@ -1680,8 +1739,10 @@ 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.check_ct act.loc act.ct 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 + 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 check_pexpr p_pe (fun pointer -> let@ value = load loc pointer act.ct in k value) @@ -1696,7 +1757,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@ () = ensure_base_type loc ~expect Unit in + let@ () = WellTyped.ensure_base_type loc ~expect Unit in k (unit_ loc) | Eccall (act, f_pe, pes) -> let@ () = WellTyped.check_ct act.loc act.ct in @@ -1708,7 +1769,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = (* | _ -> fail (fun _ -> {loc; msg = Generic (Pp.item "not a function pointer at call-site" *) (* (Sctypes.pp act.ct))}) *) (* in *) - let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr f_pe) in + let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr f_pe) in check_pexpr f_pe (fun f_it -> let@ _global = get_global () in let@ fsym = known_function_pointer loc f_it in @@ -1722,7 +1783,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@ () = ensure_base_type loc ~expect bt in + let@ () = WellTyped.ensure_base_type loc ~expect bt in let@ _, members = make_return_record loc @@ -1732,10 +1793,17 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ lvt = bind_return loc members rt in k lvt)) | Eif (c_pe, e1, e2) -> - let@ () = ensure_base_type (Mu.loc_of_expr e1) ~expect (Mu.bt_of_expr e1) in - let@ () = ensure_base_type (Mu.loc_of_expr e2) ~expect (Mu.bt_of_expr e2) in let@ () = - ensure_base_type (Mu.loc_of_pexpr c_pe) ~expect:Bool (Mu.bt_of_pexpr c_pe) + WellTyped.ensure_base_type (Mu.loc_of_expr e1) ~expect (Mu.bt_of_expr e1) + in + let@ () = + WellTyped.ensure_base_type (Mu.loc_of_expr e2) ~expect (Mu.bt_of_expr e2) + in + let@ () = + WellTyped.ensure_base_type + (Mu.loc_of_pexpr c_pe) + ~expect:Bool + (Mu.bt_of_pexpr c_pe) in check_pexpr c_pe (fun carg -> let aux lc _nm e = @@ -1750,13 +1818,17 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ () = pure (aux (not_ carg loc) "false" e2) in return ()) | Ebound e -> - let@ () = ensure_base_type (Mu.loc_of_expr e) ~expect (Mu.bt_of_expr e) in + let@ () = + WellTyped.ensure_base_type (Mu.loc_of_expr e) ~expect (Mu.bt_of_expr e) + in check_expr labels e k | End _ -> Cerb_debug.error "todo: End" | Elet (p, e1, e2) -> - let@ () = ensure_base_type (Mu.loc_of_expr e2) ~expect (Mu.bt_of_expr e2) in let@ () = - ensure_base_type + WellTyped.ensure_base_type (Mu.loc_of_expr e2) ~expect (Mu.bt_of_expr e2) + in + let@ () = + WellTyped.ensure_base_type (Mu.loc_of_pattern p) ~expect:(Mu.bt_of_pexpr e1) (Mu.bt_of_pattern p) @@ -1767,7 +1839,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ () = remove_as bound_a in k rt)) | Eunseq es -> - let@ () = ensure_base_type loc ~expect (Tuple (List.map Mu.bt_of_expr es)) in + let@ () = + WellTyped.ensure_base_type loc ~expect (Tuple (List.map Mu.bt_of_expr es)) + in let rec aux es vs prev_used = match es with | e :: es' -> @@ -1820,7 +1894,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@ () = ensure_base_type loc ~expect Unit in + let@ () = WellTyped.ensure_base_type loc ~expect Unit in let aux loc stmt = (* copying bits of code from elsewhere in check.ml *) match stmt with @@ -1925,11 +1999,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ def = Global.get_logical_function_def loc f in let has_args, expect_args = (List.length args, List.length def.args) in let@ () = - WellTyped.ensure_same_argument_number - loc - `General - has_args - ~expect:expect_args + WellTyped.ensure_same_argument_number loc `Other has_args ~expect:expect_args in let@ args = ListM.map2M @@ -2024,9 +2094,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in loop cn_progs | Ewseq (p, e1, e2) | Esseq (p, e1, e2) -> - let@ () = ensure_base_type loc ~expect (Mu.bt_of_expr e2) in + let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_expr e2) in let@ () = - ensure_base_type + WellTyped.ensure_base_type (Mu.loc_of_pattern p) ~expect:(Mu.bt_of_expr e1) (Mu.bt_of_pattern p) @@ -2037,7 +2107,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ () = remove_as bound_a in k it2)) | Erun (label_sym, pes) -> - let@ () = ensure_base_type loc ~expect Unit in + let@ () = WellTyped.ensure_base_type loc ~expect Unit in let@ lt, lkind = match Sym.Map.find_opt label_sym labels with | None -> @@ -2052,7 +2122,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@ () = ensure_base_type loc ~expect:Unit (Mu.bt_of_expr e) in + let@ () = WellTyped.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 diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml index 26b45c570..cfad7854c 100644 --- a/backend/cn/lib/compile.ml +++ b/backend/cn/lib/compile.ml @@ -431,7 +431,8 @@ module EffectfulTranslation = struct let member_types = Memory.member_types def in match List.assoc_opt Id.equal member member_types with | Some ty -> return ty - | None -> fail { loc; msg = Unexpected_member (List.map fst member_types, member) } + | None -> + fail { loc; msg = Global (Unexpected_member (List.map fst member_types, member)) } let lookup_datatype loc sym env = @@ -530,7 +531,9 @@ module EffectfulTranslation = struct let reason = "map/array index" in fail { loc; - msg = Illtyped_it { it = Terms.pp e1; has = SBT.pp has; expected; reason } + msg = + WellTyped + (Illtyped_it { it = Terms.pp e1; has = SBT.pp has; expected; reason }) } in return (IT (MapGet (e1, e2), rbt, loc)) @@ -547,7 +550,8 @@ module EffectfulTranslation = struct let@ member_bt = match List.assoc_opt Id.equal member members with | Some member_bt -> return member_bt - | None -> fail { loc; msg = Unexpected_member (List.map fst members, member) } + | None -> + fail { loc; msg = Global (Unexpected_member (List.map fst members, member)) } in return (IT.recordMember_ ~member_bt (t, member) loc) | Struct tag -> @@ -572,8 +576,9 @@ module EffectfulTranslation = struct fail { loc; msg = - Illtyped_it - { it = Terms.pp t; has = BaseTypes.Surface.pp has; expected; reason } + WellTyped + (Illtyped_it + { it = Terms.pp t; has = BaseTypes.Surface.pp has; expected; reason }) } @@ -591,7 +596,10 @@ module EffectfulTranslation = struct (fun (env, locally_bound, acc) (m, pat') -> match List.assoc_opt Id.equal m cons_info.params with | None -> - fail { loc; msg = Unexpected_member (List.map fst cons_info.params, m) } + fail + { loc; + msg = Global (Unexpected_member (List.map fst cons_info.params, m)) + } | Some mbt -> let@ env', locally_bound', pat' = translate_cn_pat env locally_bound (pat', SBT.inj mbt) @@ -650,7 +658,7 @@ module EffectfulTranslation = struct (Pp.list (fun (nm, _) -> Sym.pp nm) (Sym.Map.bindings env.computationals)))); - fail { loc; msg = Unknown_variable sym } + fail { loc; msg = WellTyped (Unknown_variable sym) } | Some (bt, None) -> return (sym, bt) | Some (bt, Some renamed_sym) -> return (renamed_sym, bt) in @@ -708,14 +716,15 @@ module EffectfulTranslation = struct fail { loc = IT.get_loc e; msg = - Illtyped_it - { it = Terms.pp e; - has = SBT.pp bt; - expected = "struct"; - reason = - (let head, pos = Locations.head_pos_of_location loc in - head ^ "\n" ^ pos) - } + WellTyped + (Illtyped_it + { it = Terms.pp e; + has = SBT.pp bt; + expected = "struct"; + reason = + (let head, pos = Locations.head_pos_of_location loc in + head ^ "\n" ^ pos) + }) }) | CNExpr_arrayindexupdates (e, updates) -> let@ e = self e in @@ -791,8 +800,9 @@ module EffectfulTranslation = struct fail { loc; msg = - Illtyped_it - { it = Terms.pp index; has = SBT.pp has; expected; reason } + WellTyped + (Illtyped_it + { it = Terms.pp index; has = SBT.pp has; expected; reason }) }) | has -> let expected = "pointer" in @@ -800,7 +810,8 @@ module EffectfulTranslation = struct fail { loc; msg = - Illtyped_it { it = Terms.pp base; has = SBT.pp has; expected; reason } + WellTyped + (Illtyped_it { it = Terms.pp base; has = SBT.pp has; expected; reason }) }) | CNExpr_membershift (e, opt_tag, member) -> let@ e = self e in @@ -824,8 +835,9 @@ module EffectfulTranslation = struct fail { loc; msg = - Illtyped_it - { it = Terms.pp e; has = SBT.pp (Struct tag'); expected; reason } + WellTyped + (Illtyped_it + { it = Terms.pp e; has = SBT.pp (Struct tag'); expected; reason }) }) | Some tag, Loc None | None, Loc (Some (Struct tag)) -> with_tag tag | None, Loc None -> cannot_tell_pointee_ctype loc e @@ -834,7 +846,9 @@ module EffectfulTranslation = struct let reason = "struct member offset" in fail { loc; - msg = Illtyped_it { it = Terms.pp e; has = SBT.pp has; expected; reason } + msg = + WellTyped + (Illtyped_it { it = Terms.pp e; has = SBT.pp has; expected; reason }) }) | CNExpr_addr nm -> return (sym_ (nm, BT.Loc None, loc)) | CNExpr_cast (bt, expr) -> @@ -1053,8 +1067,9 @@ module EffectfulTranslation = struct fail { loc; msg = - Illtyped_it - { it = Terms.pp ptr_expr; has = SBT.pp has; expected; reason } + WellTyped + (Illtyped_it + { it = Terms.pp ptr_expr; has = SBT.pp has; expected; reason }) }) in match res with @@ -1537,7 +1552,9 @@ module UsingLoads = struct | has -> let expected = "pointer" in let reason = "dereferencing" in - let msg = Illtyped_it { it = IT.pp it; has = SBT.pp has; expected; reason } in + let msg = + WellTyped (Illtyped_it { it = IT.pp it; has = SBT.pp has; expected; reason }) + in fail { loc; msg } diff --git a/backend/cn/lib/coreTypeChecks.ml b/backend/cn/lib/coreTypeChecks.ml index 5e8666e09..fc5bf7894 100644 --- a/backend/cn/lib/coreTypeChecks.ml +++ b/backend/cn/lib/coreTypeChecks.ml @@ -1,12 +1,20 @@ (* comparisons between CN base types and Core base types *) -open Effectful.Make (Or_TypeError) - module BT = BaseTypes open Cerb_frontend.Core -let check_against_core_bt fail_op core_bt cn_bt = - let fail cbt bt = +let check_against_core_bt core_bt cn_bt = + let fail msg = Result.Error msg in + let module M = struct + include Result + + type 'a t = ('a, Pp.document) Result.t + + let return = ok + end + in + let open Effectful.Make (M) in + let mismatch cbt bt = let msg1 = Pp.typ (Pp.string "mismatching core/CN types") @@ -22,7 +30,7 @@ let check_against_core_bt fail_op core_bt cn_bt = (Pp.string "inner mismatch") (Pp.ineq (Pp_mucore.pp_core_base_type cbt) (BT.pp bt))) in - fail_op msg2 + fail msg2 in let rec check_object_type = function | OTy_integer, BT.Integer -> return () @@ -32,9 +40,9 @@ let check_against_core_bt fail_op core_bt cn_bt = let@ () = check_object_type (OTy_integer, param_t) in check_object_type (t, t2) | OTy_struct tag, BT.Struct tag2 when Sym.equal tag tag2 -> return () - | OTy_union _tag, _ -> fail_op (Pp.string "unsupported: union types") - | OTy_floating, _ -> fail_op (Pp.string "unsupported: floats") - | core_obj_ty, bt -> fail (BTy_object core_obj_ty) bt + | OTy_union _tag, _ -> fail (Pp.string "unsupported: union types") + | OTy_floating, _ -> fail (Pp.string "unsupported: floats") + | core_obj_ty, bt -> mismatch (BTy_object core_obj_ty) bt in let rec check_core_base_type = function | BTy_unit, BT.Unit -> return () @@ -45,8 +53,8 @@ let check_against_core_bt fail_op core_bt cn_bt = | BTy_tuple cbts, BT.Tuple bts when List.length bts == List.length bts -> let@ _ = ListM.map2M (Tools.curry check_core_base_type) cbts bts in return () - | BTy_storable, _ -> fail_op (Pp.string "unsupported: BTy_storable") + | BTy_storable, _ -> fail (Pp.string "unsupported: BTy_storable") | BTy_ctype, BT.CType -> return () - | cbt, bt -> fail cbt bt + | cbt, bt -> mismatch cbt bt in check_core_base_type (core_bt, cn_bt) diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 87b622f6f..312d644f9 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/backend/cn/lib/core_to_mucore.ml @@ -927,8 +927,9 @@ let rec make_largs_with_accesses f_i env st (accesses, conditions) = let is_pass_by_pointer = function By_pointer -> true | By_value -> false -let check_against_core_bt loc = - CoreTypeChecks.check_against_core_bt (fun msg -> fail { loc; msg = Generic msg }) +let check_against_core_bt loc cbt bt = + CoreTypeChecks.check_against_core_bt cbt bt + |> Result.map_error (fun msg -> TypeErrors.{ loc; msg = Generic msg }) let make_label_args f_i loc env st args (accesses, inv) = diff --git a/backend/cn/lib/diagnostics.ml b/backend/cn/lib/diagnostics.ml index b22277552..1c7edc76c 100644 --- a/backend/cn/lib/diagnostics.ml +++ b/backend/cn/lib/diagnostics.ml @@ -103,8 +103,9 @@ let split_eq x y = | IT.Apply (nm, xs), IT.Apply (nm2, ys) when Sym.equal nm nm2 -> Some (List.map2 (fun x y -> (x, y)) xs ys) | IT.Constructor (nm, xs), IT.Constructor (nm2, ys) when Sym.equal nm nm2 -> - let xs = List.sort WellTyped.compare_by_fst_id xs in - let ys = List.sort WellTyped.compare_by_fst_id ys in + let compare_fst_id (x, _) (y, _) = Id.compare x y in + let xs = List.sort compare_fst_id xs in + let ys = List.sort compare_fst_id ys in Some (List.map2 (fun (_, x) (_, y) -> (x, y)) xs ys) | _ -> None diff --git a/backend/cn/lib/global.ml b/backend/cn/lib/global.ml index 386f217b6..3b18160c2 100644 --- a/backend/cn/lib/global.ml +++ b/backend/cn/lib/global.ml @@ -58,6 +58,7 @@ type error = resource : bool } | Unknown_lemma of Sym.t + | Unexpected_member of Id.t list * Id.t (** TODO replace with actual terms *) type global_t_alias_do_not_use = t @@ -89,6 +90,8 @@ module type Lifted = sig val get_struct_decl : Locations.t -> Sym.t -> Memory.struct_layout t + val get_member_type : Locations.t -> Id.t -> Memory.struct_piece list -> Sctypes.ctype t + val get_datatype : Locations.t -> Sym.t -> BaseTypes.dt_info t val get_datatype_constr : Locations.t -> Sym.t -> BaseTypes.constr_info t @@ -121,6 +124,13 @@ module Lift (M : ErrorReader) : Lifted with type 'a t := 'a M.t = struct let get_struct_decl loc tag = lift get_struct_decl loc tag (fun _ -> Unknown_struct tag) + let get_member_type loc member layout = + let member_types = Memory.member_types layout in + match List.assoc_opt Id.equal member member_types with + | Some membertyp -> M.return membertyp + | None -> M.fail loc (Unexpected_member (List.map fst member_types, member)) + + let get_datatype loc tag = lift get_datatype loc tag (fun _ -> Unknown_datatype_constr tag) diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml index e423b25a0..6013e2af7 100644 --- a/backend/cn/lib/typeErrors.ml +++ b/backend/cn/lib/typeErrors.ml @@ -113,15 +113,13 @@ end type message = | Global of Global.error - | Unexpected_member of Id.t list * Id.t - | Unknown_variable of Sym.t + | WellTyped of WellTyped.message (* some from Kayvan's compilePredicates module *) | First_iarg_missing | First_iarg_not_pointer of { pname : Request.name; found_bty : BaseTypes.t } - | Missing_member of Id.t | Missing_resource of { requests : RequestChain.t; situation : situation; @@ -139,41 +137,11 @@ type message = ctxt : Context.t * Explain.log; model : Solver.model_with_q } - | Number_members of - { has : int; - expect : int - } - | Number_arguments of - { has : int; - expect : int - } - | Number_input_arguments of - { has : int; - expect : int - } - | Number_output_arguments of - { has : int; - expect : int - } - | Mismatch of - { has : document; - expect : document - } - | Illtyped_it of - { it : document; - has : document; (* 'expected' and 'has' as in Kayvan's Core type checker *) - expected : string; - reason : string - } | Illtyped_binary_it of { left : IT.Surface.t; right : IT.Surface.t; binop : CF.Cn.cn_binop } - | NIA of - { it : IT.t; - hint : string - } | TooBigExponent : { it : IT.t } -> message | NegativeExponent : { it : IT.t } -> message | Write_value_unrepresentable of @@ -228,7 +196,7 @@ type message = ctxt : Context.t * Explain.log; model : Solver.model_with_q } - | Generic of document + | Generic of Pp.document (** TODO delete this *) | Generic_with_model of { err : document; model : Solver.model_with_q; @@ -236,10 +204,6 @@ type message = } | Unsupported of document | Parser of Cerb_frontend.Errors.cparser_cause - | Empty_pattern - | Missing_pattern of document - | Redundant_pattern of document - | Duplicate_pattern | Empty_provenance | Inconsistent_assumptions of string * (Context.t * Explain.log) | Byte_conv_needs_owned @@ -255,24 +219,20 @@ type report = state : Report.report option } -let pp_message te = - match te with - | Unknown_variable s -> - let short = !^"Unknown variable" ^^^ squotes (Sym.pp s) in - { short; descr = None; state = None } - | Global (Unknown_function sym) -> +let pp_global = function + | Global.Unknown_function sym -> let short = !^"Unknown function" ^^^ squotes (Sym.pp sym) in { short; descr = None; state = None } - | Global (Unknown_struct tag) -> + | Unknown_struct tag -> let short = !^"Struct" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Global (Unknown_datatype tag) -> + | Unknown_datatype tag -> let short = !^"Datatype" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Global (Unknown_datatype_constr tag) -> + | Unknown_datatype_constr tag -> let short = !^"Datatype constructor" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in { short; descr = None; state = None } - | Global (Unknown_resource_predicate { id; logical }) -> + | Unknown_resource_predicate { id; logical } -> let short = !^"Unknown resource predicate" ^^^ squotes (Sym.pp id) in let descr = if logical then @@ -281,7 +241,7 @@ let pp_message te = None in { short; descr; state = None } - | Global (Unknown_logical_function { id; resource }) -> + | Unknown_logical_function { id; resource } -> let short = !^"Unknown logical function" ^^^ squotes (Sym.pp id) in let descr = if resource then @@ -290,91 +250,25 @@ let pp_message te = None in { short; descr; state = None } - | Global (Unknown_lemma sym) -> + | 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 } - | First_iarg_missing -> - let short = !^"Missing pointer input argument" in - let descr = !^"a predicate definition must have at least one input argument" in - { short; descr = Some descr; state = None } - | First_iarg_not_pointer { pname; found_bty } -> - let short = !^"Non-pointer first input argument" in - let descr = - !^"the first input argument of predicate" - ^^^ squotes (Request.pp_name pname) - ^^^ !^"must have type" - ^^^ squotes BaseTypes.(pp (Loc ())) - ^^^ !^"but was found with type" - ^^^ squotes BaseTypes.(pp found_bty) - in - { short; descr = Some descr; state = None } - | Missing_member m -> - let short = !^"Missing member" ^^^ Id.pp m in + + +let pp_welltyped = function + | WellTyped.Global msg -> pp_global msg + | Unknown_variable s -> + let short = !^"Unknown variable" ^^^ squotes (Sym.pp s) in { short; descr = None; state = None } - | Missing_resource { requests; situation; ctxt; model } -> - let short = !^"Missing resource" ^^^ for_situation situation in - let descr = RequestChain.pp requests in - let orequest = - Option.map - (fun (r : RequestChain.elem) -> r.RequestChain.resource) - (List.nth_opt (List.rev requests) 0) - in - let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in - { short; descr; state = Some state } - | Merging_multiple_arrays { requests; situation; ctxt; model } -> - let short = - !^"Cannot satisfy request for resource" - ^^^ for_situation situation - ^^ dot - ^^^ !^"It requires merging multiple arrays." + | Number_arguments { type_; has; expect } -> + let type_ = + match type_ with `Other -> "" | `Input -> "input" | `Output -> "output" in - let descr = RequestChain.pp requests in - let orequest = - Option.map (fun r -> r.RequestChain.resource) (List.nth_opt (List.rev requests) 0) - in - let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in - { short; descr; state = Some state } - | Unused_resource { resource; ctxt; model } -> - let resource = Res.pp resource in - let short = !^"Left-over unused resource" ^^^ squotes resource in - let state = Explain.trace ctxt model Explain.no_ex in - { short; descr = None; state = Some state } - | Number_members { has; expect } -> - let short = !^"Wrong number of struct members" in - let descr = - !^"Expected" - ^^^ !^(string_of_int expect) - ^^ comma - ^^^ !^"has" - ^^^ !^(string_of_int has) - in - { short; descr = Some descr; state = None } - | Number_arguments { has; expect } -> - let short = !^"Wrong number of arguments" in - let descr = - !^"Expected" - ^^^ !^(string_of_int expect) - ^^ comma - ^^^ !^"has" - ^^^ !^(string_of_int has) - in - { short; descr = Some descr; state = None } - | Number_input_arguments { has; expect } -> - let short = !^"Wrong number of input arguments" in - let descr = - !^"Expected" - ^^^ !^(string_of_int expect) - ^^ comma - ^^^ !^"has" - ^^^ !^(string_of_int has) - in - { short; descr = Some descr; state = None } - | Number_output_arguments { has; expect } -> - let short = !^"Wrong number of output arguments" in + let short = !^"Wrong number" ^^^ !^type_ ^^^ !^"of arguments" in let descr = !^"Expected" ^^^ !^(string_of_int expect) @@ -419,6 +313,66 @@ let pp_message te = ^^^ !^hint in { short; descr = Some descr; state = None } + | Empty_pattern -> + let short = !^"Empty match expression." in + { short; descr = None; state = None } + | Generic err -> + let short = err in + { short; descr = None; state = None } + | Redundant_pattern p' -> + let short = !^"Redundant pattern" in + { short; descr = Some p'; state = None } + | Missing_member m -> + let short = !^"Missing member" ^^^ Id.pp m in + { short; descr = None; state = None } + + +let pp_message = function + | Global msg -> pp_global msg + | WellTyped msg -> pp_welltyped msg + | First_iarg_missing -> + let short = !^"Missing pointer input argument" in + let descr = !^"a predicate definition must have at least one input argument" in + { short; descr = Some descr; state = None } + | First_iarg_not_pointer { pname; found_bty } -> + let short = !^"Non-pointer first input argument" in + let descr = + !^"the first input argument of predicate" + ^^^ squotes (Request.pp_name pname) + ^^^ !^"must have type" + ^^^ squotes BaseTypes.(pp (Loc ())) + ^^^ !^"but was found with type" + ^^^ squotes BaseTypes.(pp found_bty) + in + { short; descr = Some descr; state = None } + | Missing_resource { requests; situation; ctxt; model } -> + let short = !^"Missing resource" ^^^ for_situation situation in + let descr = RequestChain.pp requests in + let orequest = + Option.map + (fun (r : RequestChain.elem) -> r.RequestChain.resource) + (List.nth_opt (List.rev requests) 0) + in + let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + { short; descr; state = Some state } + | Merging_multiple_arrays { requests; situation; ctxt; model } -> + let short = + !^"Cannot satisfy request for resource" + ^^^ for_situation situation + ^^ dot + ^^^ !^"It requires merging multiple arrays." + in + let descr = RequestChain.pp requests in + let orequest = + Option.map (fun r -> r.RequestChain.resource) (List.nth_opt (List.rev requests) 0) + in + let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + { short; descr; state = Some state } + | Unused_resource { resource; ctxt; model } -> + let resource = Res.pp resource in + let short = !^"Left-over unused resource" ^^^ squotes resource in + let state = Explain.trace ctxt model Explain.no_ex in + { short; descr = None; state = Some state } | TooBigExponent { it } -> let it = IT.pp it in let short = !^"Exponent too big" in @@ -564,18 +518,6 @@ let pp_message te = | Parser err -> let short = !^(Cerb_frontend.Pp_errors.string_of_cparser_cause err) in { short; descr = None; state = None } - | Empty_pattern -> - let short = !^"Empty match expression." in - { short; descr = None; state = None } - | Missing_pattern p' -> - let short = !^"Missing pattern" ^^^ squotes p' ^^ dot in - { short; descr = None; state = None } - | Redundant_pattern p' -> - let short = !^"Redundant pattern" in - { short; descr = Some p'; state = None } - | Duplicate_pattern -> - let short = !^"Duplicate pattern" in - { short; descr = None; state = None } | Empty_provenance -> let short = !^"Empty provenance" in { short; descr = None; state = None } diff --git a/backend/cn/lib/typeErrors.mli b/backend/cn/lib/typeErrors.mli index ae3f2fc64..087276d4b 100644 --- a/backend/cn/lib/typeErrors.mli +++ b/backend/cn/lib/typeErrors.mli @@ -51,14 +51,12 @@ end type message = | Global of Global.error - | Unexpected_member of Id.t list * Id.t - | Unknown_variable of Sym.t + | WellTyped of WellTyped.message | First_iarg_missing | First_iarg_not_pointer of { pname : Request.name; found_bty : BaseTypes.t } - | Missing_member of Id.t | Missing_resource of { requests : RequestChain.t; situation : situation; @@ -76,41 +74,11 @@ type message = ctxt : Context.t * Explain.log; model : Solver.model_with_q } - | Number_members of - { has : int; - expect : int - } - | Number_arguments of - { has : int; - expect : int - } - | Number_input_arguments of - { has : int; - expect : int - } - | Number_output_arguments of - { has : int; - expect : int - } - | Mismatch of - { has : Pp.document; (** TODO replace with an actual type *) - expect : Pp.document (** TODO replace with an acutal type *) - } - | Illtyped_it of - { it : Pp.document; (** TODO replace with an actual type *) - has : Pp.document; (* TODO replace with an actual type *) - expected : string; (** TODO replace with an actual type *) - reason : string (** TODO replace with an actual type *) - } | Illtyped_binary_it of { left : IndexTerms.Surface.t; right : IndexTerms.Surface.t; binop : Cerb_frontend.Cn.cn_binop } - | NIA of - { it : IndexTerms.t; - hint : string (** TODO replace with an actual type *) - } | TooBigExponent : { it : IndexTerms.t } -> message | NegativeExponent : { it : IndexTerms.t } -> message | Write_value_unrepresentable of @@ -172,10 +140,6 @@ type message = } | Unsupported of Pp.document (** TODO add source location *) | Parser of Cerb_frontend.Errors.cparser_cause - | Empty_pattern - | Missing_pattern of Pp.document (** TODO delete this *) - | Redundant_pattern of Pp.document (** TODO delete this *) - | Duplicate_pattern | Empty_provenance | Inconsistent_assumptions of string * (Context.t * Explain.log) (** TODO replace string with an actual type *) diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index 9019a3777..74e58a84b 100644 --- a/backend/cn/lib/typing.ml +++ b/backend/cn/lib/typing.ml @@ -195,14 +195,6 @@ let modify_where (f : Where.t -> Where.t) : unit t = { s with log; typing_context }) -let get_member_type loc member layout : Sctypes.t m = - let member_types = Memory.member_types layout in - match List.assoc_opt Id.equal member member_types with - | Some membertyp -> return membertyp - | None -> - fail (fun _ -> { loc; msg = Unexpected_member (List.map fst member_types, member) }) - - module ErrorReader = struct type nonrec 'a t = 'a t @@ -215,14 +207,16 @@ module ErrorReader = struct return s.typing_context.global + let lift = function + | Ok x -> return x + | Error WellTyped.{ loc; msg } -> fail (fun _ -> { loc; msg = WellTyped msg }) + + let fail loc msg = fail (fun _ -> { loc; msg = Global msg }) let get_context () = let@ s = get () in return s.typing_context - - - let lift = lift end module Global = struct @@ -296,6 +290,8 @@ end (* end: convenient functions for global typing context *) +module WellTyped = WellTyped.Lift (ErrorReader) + let add_sym_eqs sym_eqs = modify (fun s -> let sym_eqs = @@ -525,13 +521,6 @@ let model_with_internal loc prop = (* functions for binding return types and associated auxiliary functions *) -let ensure_base_type (loc : Loc.t) ~(expect : BT.t) (has : BT.t) : unit m = - if BT.equal has expect then - return () - else - fail (fun _ -> { loc; msg = Mismatch { has = BT.pp has; expect = BT.pp expect } }) - - let make_return_record loc (record_name : string) record_members = let record_s = Sym.fresh_make_uniq record_name in (* let record_s = Sym.fresh_make_uniq (TypeErrors.call_prefix call_situation) in *) @@ -552,11 +541,13 @@ let bind_logical_return_internal loc = let rec aux members lrt = match (members, lrt) with | member :: members, LogicalReturnTypes.Define ((s, it), _, lrt) -> - let@ () = ensure_base_type loc ~expect:(IT.get_bt it) (IT.get_bt member) in + let@ () = + WellTyped.ensure_base_type loc ~expect:(IT.get_bt it) (IT.get_bt member) + in let@ () = add_c_internal (LC.T (IT.eq__ member it loc)) in aux members (LogicalReturnTypes.subst (IT.make_subst [ (s, member) ]) lrt) | member :: members, Resource ((s, (re, bt)), _, lrt) -> - let@ () = ensure_base_type loc ~expect:bt (IT.get_bt member) in + let@ () = WellTyped.ensure_base_type loc ~expect:bt (IT.get_bt member) in let@ () = add_r_internal loc (re, Res.O member) in aux members (LogicalReturnTypes.subst (IT.make_subst [ (s, member) ]) lrt) | members, Constraint (lc, _, lrt) -> @@ -577,7 +568,7 @@ let bind_logical_return loc members lrt = let bind_return loc members (rt : ReturnTypes.t) = match (members, rt) with | member :: members, Computational ((s, bt), _, lrt) -> - let@ () = ensure_base_type loc ~expect:bt (IT.get_bt member) in + let@ () = WellTyped.ensure_base_type loc ~expect:bt (IT.get_bt member) in let@ () = bind_logical_return loc @@ -783,10 +774,3 @@ let test_value_eqs loc guard x ys = let@ group = value_eq_group guard x in let@ ms = prev_models_with loc guard_it in loop group ms ys - - -module WellTyped = struct - type nonrec 'a t = 'a t - - include WellTyped.Lift (ErrorReader) -end diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli index e1e70e213..881e89b9a 100644 --- a/backend/cn/lib/typing.mli +++ b/backend/cn/lib/typing.mli @@ -156,8 +156,6 @@ val test_value_eqs val lift : 'a Or_TypeError.t -> 'a m -val ensure_base_type : Locations.t -> expect:BaseTypes.t -> BaseTypes.t -> unit m - val make_return_record : Locations.t -> string -> @@ -189,4 +187,4 @@ val modify_where : (Where.t -> Where.t) -> unit m val init_solver : unit -> unit m -module WellTyped : WellTyped_intf.S with type 'a t = 'a t +module WellTyped : WellTyped_intf.S with type 'a t := 'a t diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index bd6ef4246..da7ad671f 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -9,7 +9,39 @@ let squotes, warn, dot, string, debug, item, colon, comma = Pp.(squotes, warn, dot, string, debug, item, colon, comma) -type 'a t = Context.t -> ('a * Context.t) Or_TypeError.t +type message = + | Global of Global.error + | Mismatch of + { has : Pp.document; + expect : Pp.document + } + | Generic of Pp.document (** TODO remove *) + | Illtyped_it of + { it : Pp.document; (** TODO replace with terms *) + has : Pp.document; (* 'expected' and 'has' as in Kayvan's Core type checker *) + expected : string; + reason : string + } + | Number_arguments of + { type_ : [ `Other | `Input | `Output ]; + has : int; + expect : int + } + | Missing_member of Id.t + | NIA of + { it : IT.t; + hint : string + } + | Empty_pattern + | Redundant_pattern of Pp.document + | Unknown_variable of Sym.t + +type error = + { loc : Locations.t; + msg : message + } + +type 'a t = Context.t -> ('a * Context.t, error) Result.t module GlobalReader = struct type nonrec 'a t = 'a t @@ -20,7 +52,7 @@ module GlobalReader = struct let get_global () s = Ok (s.Context.global, s) - let fail loc msg _ = Error TypeErrors.{ loc; msg = Global msg } + let fail loc msg _ = Error { loc; msg = Global msg } end module NoSolver = struct @@ -31,13 +63,6 @@ module NoSolver = struct 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 @@ -62,13 +87,6 @@ module NoSolver = struct let add_l sym bt info = update (Context.add_l sym bt info) - let ensure_base_type loc ~expect has : unit t = - if BT.equal has expect then - return () - else - fail { loc; msg = Mismatch { has = BT.pp has; expect = BT.pp expect } } - - let lift = function Ok x -> return x | Error x -> fail x let run ctxt x = x ctxt @@ -80,6 +98,13 @@ open NoSolver open Effectful.Make (NoSolver) +let ensure_base_type loc ~expect has : unit t = + if BT.equal has expect then + return () + else + fail { loc; msg = Mismatch { has = BT.pp has; expect = BT.pp expect } } + + let illtyped_index_term (loc : Locations.t) it has ~expected ~reason = let reason = match reason with @@ -88,8 +113,7 @@ let illtyped_index_term (loc : Locations.t) it has ~expected ~reason = head ^ "\n" ^ pos | Either.Right reason -> reason in - TypeErrors. - { loc; msg = Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason } } + { loc; msg = Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason } } let ensure_bits_type (loc : Loc.t) (has : BT.t) = @@ -166,14 +190,11 @@ let ensure_map_type ~reason it = ~reason:(Either.Left reason)) -let ensure_same_argument_number loc input_output has ~expect = +let ensure_same_argument_number loc type_ has ~expect = if has = expect then return () - else ( - match input_output with - | `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 } }) + else + fail { loc; msg = Number_arguments { type_; has; expect } } let compare_by_fst_id (x, _) (y, _) = Id.compare x y @@ -186,7 +207,7 @@ 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 { loc; msg = Unexpected_member (List.map fst spec, id) }) + fail { loc; msg = Global (Global.Unexpected_member (List.map fst spec, id)) }) needed have in @@ -443,7 +464,7 @@ module WIT = struct match () with | () when is_a -> get_a s | () when is_l -> get_l s - | () -> fail { loc; msg = TypeErrors.Unknown_variable s } + | () -> fail { loc; msg = Unknown_variable s } in (match binding with | BaseType bt -> return (IT (Sym s, bt, loc)) @@ -537,9 +558,7 @@ module WIT = struct in warn loc msg; return (IT (Binop (DivNoSMT, t, t'), IT.get_bt t, loc)) - | _ -> - (* TODO: check for a zero divisor *) - return (IT (Binop (Div, t, t'), IT.get_bt t, loc))) + | _ -> return (IT (Binop (Div, t, t'), IT.get_bt t, loc))) | DivNoSMT -> let@ t = infer t in let@ () = ensure_arith_type ~reason:loc t in @@ -942,7 +961,7 @@ module WIT = struct | Apply (name, args) -> 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@ () = ensure_same_argument_number loc `Other has_args ~expect:expect_args in let@ args = ListM.map2M (fun has_arg (_, def_arg_bt) -> @@ -1374,7 +1393,6 @@ module WArgs = struct end module BaseTyping = struct - open TypeErrors module BT = BaseTypes module AT = ArgumentTypes open BT @@ -1382,12 +1400,9 @@ module BaseTyping = struct type label_context = (AT.lt * Where.label * Locations.t) Sym.Map.t let check_against_core_bt loc msg2 cbt bt = - lift - (CoreTypeChecks.check_against_core_bt - (fun msg -> - Or_TypeError.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) }) - cbt - bt) + CoreTypeChecks.check_against_core_bt cbt bt + |> Result.map_error (fun msg -> { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) }) + |> lift module Mu = Mucore @@ -1425,14 +1440,18 @@ module BaseTyping = struct let@ _item_bt = get_item_bt bt in return (Mu.Cnil cbt, []) | Cnil _, _ -> - fail { loc; msg = Number_arguments { has = List.length pats; expect = 0 } } + let type_ = `Other in + let has = List.length pats in + fail { loc; msg = Number_arguments { type_; has; 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 { loc; msg = Number_arguments { has = List.length pats; expect = 2 } } + let type_ = `Other in + let has = List.length pats in + fail { loc; msg = Number_arguments { type_; has; expect = 2 } } | Ctuple, pats -> let@ bts = match BT.is_tuple_bt bt with @@ -1703,8 +1722,9 @@ module BaseTyping = struct let@ () = ensure_base_type loc ~expect:(List ibt) (bt_of_pexpr xs) in return (bt_of_pexpr xs) | _ -> - fail - { loc; msg = Number_arguments { has = List.length pes; expect = 2 } }) + let type_ = `Other in + let has = List.length pes in + fail { loc; msg = Number_arguments { type_; has; expect = 2 } }) | Ctuple -> return (BT.Tuple (List.map bt_of_pexpr pes)) | Carray -> let ibt = bt_of_pexpr (List.hd pes) in @@ -1871,7 +1891,7 @@ module BaseTyping = struct let@ () = ensure_same_argument_number loc - `General + `Other (List.length its) ~expect:(List.length def.args) in @@ -1883,7 +1903,7 @@ module BaseTyping = struct let wrong_number_arguments () = let has = List.length its in let expect = AT.count_computational lemma_typ in - fail { loc; msg = Number_arguments { has; expect } } + fail { loc; msg = Number_arguments { type_ = `Other; has; expect } } in let rec check_args lemma_typ its = match (lemma_typ, its) with @@ -2118,7 +2138,7 @@ module BaseTyping = struct let wrong_number_arguments () = let has = List.length pes in let expect = AT.count_computational lt in - fail { loc; msg = Number_arguments { has; expect } } + fail { loc; msg = Number_arguments { type_ = `Other; has; expect } } in let rec check_args lt pes = match (lt, pes) with @@ -2449,8 +2469,6 @@ let check_term = WIT.check let check_ct = WCT.is_ct -let compare_by_fst_id = compare_by_fst_id - let ensure_same_argument_number = ensure_same_argument_number let ensure_bits_type = ensure_bits_type @@ -2464,7 +2482,7 @@ module type ErrorReader = sig val get_context : unit -> Context.t t - val lift : 'a Or_TypeError.t -> 'a t + val lift : ('a, error) Result.t -> 'a t end module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = struct @@ -2522,13 +2540,28 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru let check_ct = lift2 check_ct - let compare_by_fst_id = compare_by_fst_id - let ensure_same_argument_number loc type_ n ~expect = let ( let@ ) = M.bind in let@ context = M.get_context () in - M.lift (Result.map fst (ensure_same_argument_number loc type_ n ~expect context)) + M.lift + (Result.map fst (run context (ensure_same_argument_number loc type_ n ~expect))) + + + (** TODO This should be removed, but there is a discrepancy between WellTyped + and Check for base typing for bounded_binops. *) + let ensure_base_type loc ~expect has = + (* if not (BT.equal expect has) then *) + (* failwith ("has: " ^ Pp.plain (BT.pp has) ^ ", expect: " ^ Pp.plain (BT.pp expect)); *) + (* M.return () *) + let ( let@ ) = M.bind in + let@ context = M.get_context () in + M.lift (Result.map fst (run context (ensure_base_type loc has ~expect))) - let ensure_bits_type = lift2 ensure_bits_type + (** TODO If this crashes, figure out why WellTyped did not catch it earlier. + If it doesn't, then just delete it *) + let ensure_bits_type = + (* assert (match bt with BT.Bits _ -> true | _ -> false); *) + (* M.return () *) + lift2 ensure_bits_type end diff --git a/backend/cn/lib/wellTyped.mli b/backend/cn/lib/wellTyped.mli index 22296b75e..d2e5ac199 100644 --- a/backend/cn/lib/wellTyped.mli +++ b/backend/cn/lib/wellTyped.mli @@ -1,5 +1,37 @@ val use_ity : bool ref +type message = + | Global of Global.error + | Mismatch of + { has : Pp.document; + expect : Pp.document + } + | Generic of Pp.document + | Illtyped_it of + { it : Pp.document; + has : Pp.document; + expected : string; + reason : string + } + | Number_arguments of + { type_ : [ `Other | `Input | `Output ]; + has : int; + expect : int + } + | Missing_member of Id.t + | NIA of + { it : IndexTerms.t; + hint : string + } + | Empty_pattern + | Redundant_pattern of Pp.document + | Unknown_variable of Sym.t + +type error = + { loc : Locations.t; + msg : message + } + include WellTyped_intf.S module type ErrorReader = sig @@ -11,7 +43,7 @@ module type ErrorReader = sig val get_context : unit -> Context.t t - val lift : 'a Or_TypeError.t -> 'a t + val lift : ('a, error) Result.t -> 'a t end module Lift : functor (M : ErrorReader) -> WellTyped_intf.S with type 'a t := 'a M.t diff --git a/backend/cn/lib/wellTyped_intf.ml b/backend/cn/lib/wellTyped_intf.ml index f16432e1a..d3e179f32 100644 --- a/backend/cn/lib/wellTyped_intf.ml +++ b/backend/cn/lib/wellTyped_intf.ml @@ -3,15 +3,15 @@ module type S = sig val ensure_bits_type : Locations.t -> BaseTypes.t -> unit t + val ensure_base_type : Locations.t -> expect:BaseTypes.t -> BaseTypes.t -> unit t + val ensure_same_argument_number : Locations.t -> - [< `General | `Input | `Output ] -> + [ `Other | `Input | `Output ] -> int -> expect:int -> unit t - val compare_by_fst_id : Id.t * 'a -> Id.t * 'b -> int - val check_ct : Locations.t -> Sctypes.ctype -> unit t val infer_term : 'bt IndexTerms.annot -> IndexTerms.t t diff --git a/tests/cn/tree16/as_mutual_dt/tree16.c.verify b/tests/cn/tree16/as_mutual_dt/tree16.c.verify index 37b1eeaf0..bcb3d7581 100644 --- a/tests/cn/tree16/as_mutual_dt/tree16.c.verify +++ b/tests/cn/tree16/as_mutual_dt/tree16.c.verify @@ -8,8 +8,8 @@ tests/cn/tree16/as_mutual_dt/tree16.c:111:19: warning: 'each' expects a 'u64', b tests/cn/tree16/as_mutual_dt/tree16.c:121:18: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future. take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len)) ^ -other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&i1' with type 'i32' was provided. This will become an error in the future. +other location (File "backend/cn/lib/compile.ml", line 1593, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&i1' with type 'i32' was provided. This will become an error in the future. -other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future. +other location (File "backend/cn/lib/compile.ml", line 1593, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future. [1/1]: lookup_rec -- pass diff --git a/tests/cn/tree16/as_partial_map/tree16.c.verify b/tests/cn/tree16/as_partial_map/tree16.c.verify index 0132fc840..80b65218d 100644 --- a/tests/cn/tree16/as_partial_map/tree16.c.verify +++ b/tests/cn/tree16/as_partial_map/tree16.c.verify @@ -14,9 +14,9 @@ tests/cn/tree16/as_partial_map/tree16.c:137:19: warning: 'each' expects a 'u64', tests/cn/tree16/as_partial_map/tree16.c:146:18: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future. take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len)) ^ -other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&i2' with type 'i32' was provided. This will become an error in the future. +other location (File "backend/cn/lib/compile.ml", line 1593, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&i2' with type 'i32' was provided. This will become an error in the future. -other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future. +other location (File "backend/cn/lib/compile.ml", line 1593, characters 38-45) warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future. [1/2]: cn_get_num_nodes -- pass [2/2]: lookup_rec -- pass