From aecaf298b44def262de5ca46cf1c86afb4e5272a Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 7 Feb 2025 08:44:52 +0000 Subject: [PATCH 1/2] prevent Owned and Block in WellTyped --- backend/cn/lib/wellTyped.ml | 34 ++++++++-------------------------- 1 file changed, 8 insertions(+), 26 deletions(-) diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index f2d49a33b..cb4b6c4ad 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -1061,7 +1061,14 @@ module WReq = struct Pp.debug 22 (lazy (Pp.item "WReq: checking" (Req.pp r))); let@ spec_iargs = match Req.get_name r with - | Owned (_ct, _init) -> return [] + | Owned (ct, init) -> + let@ () = WCT.is_ct loc ct in + let@ () = match ct, init with + | Void, Req.Uninit -> fail {loc; msg = Generic !^"Block is not a valid resource, please supply another C-type (using `Block`)."} + | Void, Req.Init -> fail {loc; msg = Generic !^"Owned is not a valid resource, please supply another C-type (using `Owned`)."} + | _ -> return () + in + return [] | PName name -> let@ def = get_resource_predicate_def loc name in return def.iargs @@ -1108,35 +1115,10 @@ module WReq = struct let hint = "Only constant iteration steps are allowed." in 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 _ - -> {loc; msg = Generic (!^"Iteration step" ^^^ IT.pp p.step ^^^ parens (IT.pp - step) ^^^ !^ "different to sizeof" ^^^ Sctypes.pp ct ^^^ parens (!^ (Int.to_string - sz)))}) | _ -> return () in*) let@ permission, iargs = pure (let@ () = add_l (fst p.q) (snd p.q) (loc, lazy (Pp.string "forall-var")) in let@ permission = WIT.check loc BT.Bool p.permission in - (* let@ provable = provable loc in *) - (* let here = Locations.other __LOC__ in *) - (* let only_nonnegative_indices = *) - (* (\* It is important to use `permission` here and NOT `p.permission`. *) - (* If there is a record involved, `permission` is normalised but the - `p.permission` is not *) - (* If there is a subsitution in `provable` then a type check *) - (* assertion may fail if the non-normalised form is used *\) *) - (* let sym_args = (fst p.q, snd p.q, p.q_loc) in *) - (* LC.forall_ p.q (impl_ (permission, ge_ (sym_ sym_args, int_lit_ 0 (snd p.q) - here) here) here) *) - (* in *) - (* let@ () = match provable only_nonnegative_indices with *) - (* | `True -> *) - (* return () *) - (* | `False -> *) - (* let model = Solver.model () in *) - (* let msg = "Iterated resource gives ownership to negative indices." in *) - (* fail (fun ctxt -> {loc; msg = Generic_with_model {err= !^msg; ctxt; model}}) *) - (* in *) let has_iargs, expect_iargs = (List.length p.iargs, List.length spec_iargs) in (* +1 because of pointer argument *) let@ () = From 4f0401ba4d789bd44f618d266c865b08aef706cf Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 7 Feb 2025 09:37:29 +0000 Subject: [PATCH 2/2] do this check also for to/from_bytes --- backend/cn/lib/check.ml | 2 ++ backend/cn/lib/wellTyped.ml | 25 +++++++++++++++++++------ backend/cn/lib/wellTyped_intf.ml | 2 ++ 3 files changed, 23 insertions(+), 6 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 14336d694..7da06465b 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -1904,6 +1904,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | To_from_bytes ((To | From), { name = PName _; _ }) -> fail (fun _ -> { loc; msg = Byte_conv_needs_owned }) | To_from_bytes (To, { name = Owned (ct, init); pointer; _ }) -> + let@ () = WellTyped.owned_ct_ok loc (ct, init) in let@ pointer = WellTyped.infer_term pointer in let@ (_, O value), _ = RI.Special.predicate_request @@ -1921,6 +1922,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | Uninit -> add_c loc (LC.T (IT.eq_ (byte_arr, default_ map_bt here) here)) | Init -> add_c loc (LC.T (bytes_constraints ~value ~byte_arr ct))) | To_from_bytes (From, { name = Owned (ct, init); pointer; _ }) -> + let@ () = WellTyped.owned_ct_ok loc (ct, init) in let@ pointer = WellTyped.infer_term pointer in let q_sym = Sym.fresh_named "from_bytes" in let@ (_, O byte_arr), _ = diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index cb4b6c4ad..b76023de4 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -1053,6 +1053,22 @@ let warn_when_not_quantifier_bt ^^^ !^"was provided. This will become an error in the future.") +let owned_ct_ok loc (ct, init) = + let@ () = WCT.is_ct loc ct in + let pp_resource ct = match init with + | Request.Init -> !^"Owned" ^^ Pp.angles !^ct + | Request.Uninit -> !^"Block" ^^ Pp.angles !^ct + in + match ct with + | Void -> + let msg = + pp_resource "void" ^^^ !^"is not a valid resource," + ^^^ !^"please specify another C-type" + ^^^ Pp.parens (!^"using" ^^^ pp_resource "YOURTYPE") + in + fail {loc; msg = Generic msg} + | _ -> return () + module WReq = struct module Req = Request open IndexTerms @@ -1062,12 +1078,7 @@ module WReq = struct let@ spec_iargs = match Req.get_name r with | Owned (ct, init) -> - let@ () = WCT.is_ct loc ct in - let@ () = match ct, init with - | Void, Req.Uninit -> fail {loc; msg = Generic !^"Block is not a valid resource, please supply another C-type (using `Block`)."} - | Void, Req.Init -> fail {loc; msg = Generic !^"Owned is not a valid resource, please supply another C-type (using `Owned`)."} - | _ -> return () - in + let@ () = owned_ct_ok loc (ct, init) in return [] | PName name -> let@ def = get_resource_predicate_def loc name in @@ -2594,6 +2605,8 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru let check_ct = lift2 check_ct + let owned_ct_ok = lift2 owned_ct_ok + let ensure_same_argument_number loc type_ n ~expect = let ( let@ ) = M.bind in let@ context = M.get_context () in diff --git a/backend/cn/lib/wellTyped_intf.ml b/backend/cn/lib/wellTyped_intf.ml index 2c8ed06bc..88842f4b3 100644 --- a/backend/cn/lib/wellTyped_intf.ml +++ b/backend/cn/lib/wellTyped_intf.ml @@ -14,6 +14,8 @@ module type S = sig val check_ct : Locations.t -> Sctypes.ctype -> unit t + val owned_ct_ok : Locations.t -> (Sctypes.ctype * Request.init) -> unit t + val infer_term : 'bt IndexTerms.annot -> IndexTerms.t t val check_term : Locations.t -> BaseTypes.t -> 'bt IndexTerms.annot -> IndexTerms.t t