Unify non-void C-type checks

array_shift, RW/W (Owned) and sizeof now use the exact same check and
error message in wellTyped.ml.

Curiously, whilst this does fix the test case in
rems-project/cerberus#716, the error message is wholly unsatisfactory
because of how steps for quantified resources are defined.

Author: dc-mak

lib/check.ml

@@ -1927,7 +1927,8 @@ 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 ctxt = match init with Init -> `RW | Uninit -> `W in
+           let@ () = WellTyped.err_if_ct_void loc ctxt ct in
            let@ pointer = WellTyped.infer_term pointer in
            let@ (_, O value), _ =
              RI.Special.predicate_request
@@ -1947,7 +1948,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               let@ constr = bytes_constraints ~value ~byte_arr ct in
               add_c loc (LC.T constr))
          | To_from_bytes (From, { name = Owned (ct, init); pointer; _ }) ->
-           let@ () = WellTyped.owned_ct_ok loc (ct, init) in
+           let ctxt = match init with Init -> `RW | Uninit -> `W in
+           let@ () = WellTyped.err_if_ct_void loc ctxt ct in
            let@ pointer = WellTyped.infer_term pointer in
            let q_sym = Sym.fresh_named "from_bytes" in
            let@ (_, O byte_arr), _ =

lib/typeErrors.ml

@@ -315,8 +315,15 @@ let pp_welltyped = function
   | Missing_member m ->
     let short = !^"Missing member" ^^^ Id.pp m in
     { short; descr = None; state = None }
-  | Size_of_void ->
-    let short = !^"Cannot take the sizeof of a void expression" in
+  | Void_ctype ctxt ->
+    let ctxt =
+      match ctxt with
+      | `RW -> "RW"
+      | `W -> "W"
+      | `Array_shift -> "array_shift"
+      | `Sizeof -> "sizeof"
+    in
+    let short = !^"C-type must not be void in a" ^^^ !^ctxt ^^ angles underscore in
     { short; descr = None; state = None }
 
 

lib/wellTyped.ml

@@ -36,7 +36,7 @@ type message =
   | Empty_pattern
   | Redundant_pattern of Pp.document
   | Unknown_variable of Sym.t
-  | Size_of_void
+  | Void_ctype of [ `Array_shift | `Sizeof | `RW | `W ]
 
 type error =
   { loc : Locations.t;
@@ -232,6 +232,10 @@ let correct_members_sorted_annotated loc spec have =
   return have_annotated
 
 
+let err_if_ct_void loc context ct =
+  match ct with Sctypes.Void -> fail { loc; msg = Void_ctype context } | _ -> return ()
+
+
 module WBT = struct
   open BT
 
@@ -837,6 +841,7 @@ module WIT = struct
         (* looking at solver mapping *)
         return (IT (MemberShift (t, tag, member), BT.Loc (), loc))
       | ArrayShift { base; ct; index } ->
+        let@ () = err_if_ct_void loc `Array_shift ct in
         let@ () = WCT.is_ct loc ct in
         let@ base = check loc (Loc ()) base in
         let@ index = infer index in
@@ -850,11 +855,7 @@ module WIT = struct
         let@ ptr = check loc (Loc ()) ptr in
         return (IT (HasAllocId ptr, BT.Bool, loc))
       | SizeOf ct ->
-        let@ () =
-          match ct with
-          | Sctypes.Void -> fail { loc; msg = Size_of_void }
-          | _ -> return ()
-        in
+        let@ () = err_if_ct_void loc `Sizeof ct in
         let@ () = WCT.is_ct loc ct in
         let sz = Memory.size_of_ctype ct in
         let rs = Option.get (BT.is_bits_bt Memory.size_bt) in
@@ -1069,25 +1070,6 @@ let warn_when_not_quantifier_bt
        ^^ dot)
 
 
-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 [@alert "-deprecated"] }
-  | _ -> return ()
-
-
 module WReq = struct
   module Req = Request
   open IndexTerms
@@ -1097,7 +1079,9 @@ module WReq = struct
     let@ spec_iargs =
       match Req.get_name r with
       | Owned (ct, init) ->
-        let@ () = owned_ct_ok loc (ct, init) in
+        let tag = match init with Req.Init -> `RW | Uninit -> `W in
+        let@ () = err_if_ct_void loc tag ct in
+        let@ () = WCT.is_ct loc ct in
         return []
       | PName name ->
         let@ def = get_resource_predicate_def loc name in
@@ -2642,7 +2626,7 @@ 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 err_if_ct_void = lift3 err_if_ct_void
 
   let ensure_same_argument_number loc type_ n ~expect =
     let ( let@ ) = M.bind in

lib/wellTyped.mli

@@ -26,7 +26,7 @@ type message =
   | Empty_pattern
   | Redundant_pattern of Pp.document
   | Unknown_variable of Sym.t
-  | Size_of_void
+  | Void_ctype of [ `Sizeof | `Array_shift | `RW | `W ]
 
 type error =
   { loc : Locations.t;

lib/wellTyped_intf.ml

@@ -14,7 +14,11 @@ 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 err_if_ct_void
+    :  Locations.t ->
+    [ `Sizeof | `Array_shift | `RW | `W ] ->
+    Sctypes.ctype ->
+    unit t
 
   val infer_term : 'bt IndexTerms.annot -> IndexTerms.t t
 

tests/cn/array_shift_mismatch.error.c.verify

@@ -1,28 +1,7 @@
-return code: 125
+return code: 1
 tests/cn/array_shift_mismatch.error.c:8:19: warning: annotation on array_shift suggests p has type void* but it has type signed int*.
     ptr_eq(return,array_shift<void>(p, 1u64));
                   ^~~~~~~~~~~~~~~~~~~~~~~~~~ 
-internal error: size_of_ctype applied to void
-cn: internal error, uncaught exception:
-    Failure("internal error: size_of_ctype applied to void")
-    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
-    Called from Cn__Solver.translate_term in file "lib/solver.ml", line 947, characters 32-57
-    Called from Cn__Solver.translate_term in file "lib/solver.ml", line 753, characters 13-32
-    Called from Cn__Solver.add_assumption in file "lib/solver.ml", line 1105, characters 46-68
-    Called from Cn__Typing.add_c_internal in file "lib/typing.ml", line 409, characters 11-51
-    Called from Cn__Typing.bind.(fun) in file "lib/typing.ml", line 49, characters 17-20
-    Called from Cn__Typing.bind.(fun) in file "lib/typing.ml", line 49, characters 17-20
-    Called from Cn__Typing.pure.(fun) in file "lib/typing.ml", line 76, characters 22-25
-    Called from Cn__Typing.pure.(fun) in file "lib/typing.ml", line 76, characters 22-25
-    Called from Cn__Typing.pure.(fun) in file "lib/typing.ml", line 76, characters 22-25
-    Called from Cn__Typing.pure.(fun) in file "lib/typing.ml", line 76, characters 22-25
-    Called from Cn__Typing.pure.(fun) in file "lib/typing.ml", line 76, characters 22-25
-    Called from Cn__Typing.bind.(fun) in file "lib/typing.ml", line 49, characters 17-20
-    Called from Cn__Typing.bind.(fun) in file "lib/typing.ml", line 49, characters 17-20
-    Called from Cn__Typing.bind.(fun) in file "lib/typing.ml", line 49, characters 17-20
-    Called from Cn__Typing.run_from_pause in file "lib/typing.ml", line 68, characters 50-55
-    Called from Dune__exe__Main.with_well_formedness_check in file "bin/main.ml", line 187, characters 15-69
-    Called from Dune__exe__Main.with_well_formedness_check in file "bin/main.ml", lines 176-204, characters 6-15
-    Re-raised at Dune__exe__Main.with_well_formedness_check in file "bin/main.ml", line 212, characters 4-69
-    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
-    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
+tests/cn/array_shift_mismatch.error.c:8:19: error: C-type must not be void in a array_shift<_>
+    ptr_eq(return,array_shift<void>(p, 1u64));
+                  ^~~~~~~~~~~~~~~~~~~~~~~~~~ 

tests/cn/array_shift_void.error.c.verify

@@ -1,3 +1,3 @@
 return code: 1
-other location (File "lib/compile.ml", line 1144, characters 33-40)  error: Cannot take the sizeof of a void expression
+other location (File "lib/compile.ml", line 1145, characters 33-40)  error: C-type must not be void in a sizeof<_>
 

tests/cn/tree16/as_mutual_dt/tree16.c.verify

@@ -11,8 +11,8 @@ tests/cn/tree16/as_mutual_dt/tree16.c:111:19: warning: 'each' prefers a 'u64', b
 tests/cn/tree16/as_mutual_dt/tree16.c:121:18: warning: 'each' prefers a 'u64', but 'j' has type 'i32'.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i1' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i1' has type 'i32'.
 
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
 
 [1/1]: lookup_rec -- pass

tests/cn/tree16/as_partial_map/tree16.c.verify

@@ -17,9 +17,9 @@ tests/cn/tree16/as_partial_map/tree16.c:137:19: warning: 'each' prefers a 'u64',
 tests/cn/tree16/as_partial_map/tree16.c:146:18: warning: 'each' prefers a 'u64', but 'j' has type 'i32'.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i2' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i2' has type 'i32'.
 
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
 
 [1/2]: cn_get_num_nodes -- pass
 [2/2]: lookup_rec -- pass