Update Cerberus commit for Byte C type

Author: dc-mak

cn.opam

@@ -23,7 +23,7 @@ depends: [
   "zarith" {>= "1.13"}
 ]
 pin-depends: [
-  ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#881feae"]
+  ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#718ca6c0"]
 ]
 build: [
   ["dune" "subst"] {pinned}

lib/baseTypes.ml

@@ -137,6 +137,7 @@ let rec of_sct loc is_signed size_of = function
     Map (uintptr_bt loc is_signed size_of, of_sct loc is_signed size_of sct)
   | Pointer sct -> Loc (loc sct)
   | Struct tag -> Struct tag
+  | Byte -> MemByte
   | Function _ -> Cerb_debug.error "todo: function types"
 
 

lib/bugExplanation/replicators.ml

@@ -171,6 +171,7 @@ let compile_sct_aux (prog5 : unit Mucore.file) (sct : Sctypes.t)
   let b1, s1 =
     match sct with
     | Void -> failwith __LOC__
+    | Byte -> failwith ("TODO: Byte case for " ^ __FUNCTION__)
     | Integer _ ->
       ( [ Utils.create_binding buf_sym C.pointer_to_char ],
         A.

lib/check.ml

@@ -1762,7 +1762,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
       (* FIXME this hard codes big endianness but this should be switchable *)
       let here = Locations.other __LOC__ in
       match ct with
-      | Sctypes.Void | Array (_, _) | Struct _ | Function (_, _, _) ->
+      | Sctypes.Void | Array (_, _) | Struct _ | Function (_, _, _) | Byte ->
         fail (fun _ -> { loc; msg = Unsupported_byte_conv_ct ct })
       | Integer it ->
         let bt = IT.get_bt value in

lib/indexTerms.ml

@@ -974,7 +974,7 @@ let value_check mode (struct_layouts : Memory.struct_decls) ct about loc =
   let open Memory in
   let rec aux (ct_ : Sctypes.t) about =
     match ct_ with
-    | Void -> bool_ true loc
+    | Void | Byte -> bool_ true loc
     | Integer it ->
       in_z_range about (Memory.min_integer_type it, Memory.max_integer_type it) loc
     | Array (_, None) ->

lib/pack.ml

@@ -43,7 +43,7 @@ let packing_ft ~full loc global provable ret =
   match ret with
   | P ret ->
     (match ret.name with
-     | Owned ((Void | Integer _ | Pointer _ | Function _), _init) -> None
+     | Owned ((Void | Integer _ | Pointer _ | Function _ | Byte), _init) -> None
      | Owned ((Array (ict, olength) as ct), init) ->
        let qpred = unfolded_array loc init (ict, olength) ret.pointer in
        let o_s, o = IT.fresh_named (Memory.bt_of_sct ct) "value" loc in
@@ -104,7 +104,7 @@ let packing_ft ~full loc global provable ret =
 let unpack_owned loc global (ct, init) pointer (O o) =
   let open Sctypes in
   match ct with
-  | Void | Integer _ | Pointer _ | Function _ -> None
+  | Void | Integer _ | Pointer _ | Function _ | Byte -> None
   | Array (ict, olength) -> Some [ (unfolded_array loc init (ict, olength) pointer, O o) ]
   | Struct tag ->
     let layout = Sym.Map.find tag global.Global.struct_decls in

lib/pp_mucore_coq.ml

@@ -691,7 +691,8 @@ let rec pp_ctype (Ctype.Ctype (annots, ct)) =
          pp_constructor "Ctype.Pointer" [ pp_qualifiers quals; pp_ctype ct ]
        | Ctype.Atomic ct -> pp_constructor "Ctype.Atomic" [ pp_ctype ct ]
        | Ctype.Struct sym -> pp_constructor "Ctype.Struct" [ pp_symbol sym ]
-       | Ctype.Union sym -> pp_constructor "Ctype.Union" [ pp_symbol sym ])
+       | Ctype.Union sym -> pp_constructor "Ctype.Union" [ pp_symbol sym ]
+       | Ctype.Byte -> pp_constructor0 "Ctype.Byte")
     ]
 
 
@@ -726,6 +727,7 @@ let rec pp_sctype = function
             pp_bool variadic
           ]
       ]
+  | Sctypes.Byte -> pp_constructor0 "SCtypes.Byte"
 
 
 let rec pp_core_base_type = function

lib/sctypes.ml

@@ -80,6 +80,7 @@ type ctype =
       (qualifiers * ctype)
       * (ctype * (* is_register *) bool) list
       * (* is_variadic *) bool
+  | Byte
 [@@deriving eq, ord]
 
 type t = ctype
@@ -142,6 +143,7 @@ let rec to_ctype (ct_ : ctype) =
     | Array (t, oi) -> Array (to_ctype t, Option.map Z.of_int oi)
     | Pointer t -> Pointer (Ctype.no_qualifiers, to_ctype t)
     | Struct t -> Struct t
+    | Byte -> Byte
     | Function ((ret_q, ret_ct), args, variadic) ->
       let args =
         List.map
@@ -184,6 +186,7 @@ let rec of_ctype (Ctype.Ctype (_, ct_)) =
     return (Pointer t)
   | Ctype.Atomic _ -> None
   | Ctype.Struct s -> return (Struct s)
+  | Byte -> return Byte
   | Union _ -> fail
 
 

lib/wellTyped.ml

@@ -325,6 +325,7 @@ module WCT = struct
         let@ _struct_decl = get_struct_decl loc tag in
         return ()
       | Function ((_, rct), args, _) -> ListM.iterM aux (rct :: List.map fst args)
+      | Byte -> return ()
     in
     fun ct -> aux ct
 end