Add Byte variant to Ctype

dc-mak · dc-mak · commit 41430e298dd6 · 2025-07-16T13:00:38.000+01:00
Needs to be extended with a ternary argument (signed, unsigned, neither)
to reflect how to treat it in certain places, but assuming (Integer
Char) and signed for now.
diff --git a/frontend/model/ail/ailTypesAux.lem b/frontend/model/ail/ailTypesAux.lem
@@ -257,6 +257,8 @@ let rec is_complete sigm ty =
         | Nothing ->
             false
       end
+  | Byte ->
+      true
 end
 
 (* STD §6.2.5#1, sentence 4 *)
@@ -1263,6 +1265,8 @@ match ty with
       false
   | Union _ ->
       false
+  | Byte ->
+      false
 end
 
 
diff --git a/frontend/model/ail/ailWf.lem b/frontend/model/ail/ailWf.lem
@@ -114,6 +114,8 @@ let rec wf_type sigm (Ctype _ ty) =
       return ()
   | Union _ ->
       return ()
+  | Byte ->
+      return ()
 (*
   | Builtin _ ->
       return () *)
diff --git a/frontend/model/ail/genTypes.lem b/frontend/model/ail/genTypes.lem
@@ -26,6 +26,7 @@ type genType =
  | GenStruct of ail_identifier
  | GenUnion of ail_identifier
  | GenAtomic of genType
+ | GenByte
 
 val signedInt_gty: genType
 let signedInt_gty =
@@ -126,6 +127,8 @@ let rec eq_genType gty1 gty2 =
         7
     | GenAtomic _ ->
         8
+    | GenByte ->
+        9
   end in
   match (gty1, gty2) with
     | (GenBasic gbty1, GenBasic gbty2 ) ->
@@ -209,6 +212,8 @@ match ty with
       GenStruct tag
   | Union  tag ->
       GenUnion tag
+  | Byte ->
+      GenByte
 end
 
 val inject_typeCategory: typeCategory -> genTypeCategory
diff --git a/frontend/model/ail/genTypesAux.lem b/frontend/model/ail/genTypesAux.lem
@@ -318,6 +318,8 @@ let rec interpret_genType loc impl gty =
     | GenAtomic gty ->
         interpret_genType loc impl gty >>= fun ty ->
         ret (Atomic ty)
+    | GenByte ->
+        ret Byte
   end
 
 val interpret_genTypeCategory: Loc.t -> IntegerImpl.implementation -> genTypeCategory -> errorM typeCategory
@@ -401,6 +403,8 @@ let is_complete sigm gty =
           | _ ->
               false
         end
+    | GenByte ->
+        true
 end
 
 val is_incomplete: forall 'a. sigma 'a -> genType -> bool
diff --git a/frontend/model/cabs_to_ail.lem b/frontend/model/cabs_to_ail.lem
@@ -173,6 +173,8 @@ let rec wip tagDefs acc path_prefix (outer_path, outer_ty) (Ctype.Ctype _ cty) =
           | _ ->
               error "elemPathFromCtype_aux3, Union"
         end
+    | Ctype.Byte ->
+        (path_prefix, outer_path, outer_ty) :: acc
   end
 
 val elemPathFromCtype3: bool -> map ail_identifier tag_definition -> Ctype.ctype -> list (init_path * init_path * Ctype.ctype)
@@ -422,6 +424,8 @@ let rec innerCtype tagDefs (Ctype.Ctype _ ty as cty) =
           | _ ->
               error "innerCtype: Union"
         end
+   | Ctype.Byte ->
+        error "innerCtype: Byte"
   end
 
 
diff --git a/frontend/model/cabs_to_ail_aux.lem b/frontend/model/cabs_to_ail_aux.lem
@@ -151,6 +151,9 @@ let rec mk_zeroInit_aux tagDefs (Ctype.Ctype _ ty) =
           | _ ->
               error "[Cabs_to_ail.mk_zeroInit_aux] - internal ERROR: Union"
         end
+    | Ctype.Byte ->
+        (* TODO: check *)
+        A.ConstantInteger (A.IConstant 0 A.Octal Nothing)
   end
 let mk_zeroInit tagDefs ty =
   A.AnnotatedExpression () [] Loc.unknown
@@ -253,6 +256,8 @@ let rec export_ctype (Ctype.Ctype annot ty_ as ty) =
         ty
     | Ctype.Union _ ->
         ty
+    | Ctype.Byte ->
+        ty
   end
 
 val     has_continue: cabs_statement -> bool
diff --git a/frontend/model/core_aux.lem b/frontend/model/core_aux.lem
@@ -47,6 +47,9 @@ let rec core_object_type_of_ctype (Ctype _ ty) =
        Just (OTy_struct tag_sym)
    | Union tag_sym ->
        Just (OTy_union tag_sym)
+   | Byte ->
+       (* TODO add an OTy_byte? *)
+       Just OTy_integer
   end
 
 val oTy_of_bTy: core_base_type -> maybe core_object_type
diff --git a/frontend/model/ctype.lem b/frontend/model/ctype.lem
@@ -58,6 +58,7 @@ type ctype_ (*[name = "^\\([a-z A-Z]*_\\)?ty[0-9]*'?$"]*) =
   | Atomic of ctype
   | Struct of Symbol.sym
   | Union of Symbol.sym
+  | Byte
 and ctype =
   Ctype of list Annot.annot * ctype_
 
@@ -150,6 +151,8 @@ let rec ctypeEqual (Ctype _ ty1) (Ctype _ ty2) =
         7
     | Union _ ->
         8
+    | Byte ->
+        9
   end in
   let paramsEqual (qs1, ty1, b1) (qs2, ty2, b2) =
     qs1 = qs2 && ctypeEqual ty1 ty2 && b1 = b2 in
diff --git a/frontend/model/defacto_memory.lem b/frontend/model/defacto_memory.lem
@@ -434,6 +434,8 @@ let rec mkUnspec (Ctype _ ty) =
     | (Union tag_sym) ->
         let ((memb_ident, (_, _, _, ty)), _) = Ctype_aux.get_unionDef tag_sym in
         MVunion tag_sym memb_ident (mkUnspec ty)
+    | Byte ->
+        MVinteger Char (IV Prov_none IVunspecified)
   end
 
 
@@ -1065,6 +1067,8 @@ let rec impl_sizeof_ival_aux (Ctype _ ty as cty) =
     | Union tag_sym ->
         (* TODO: move the code from mem_simplify *)
         IVsizeof (Ctype [] (Union tag_sym))
+    | Byte ->
+       IVconcrete 1
 end
 
 
diff --git a/frontend/model/defacto_memory_aux.lem b/frontend/model/defacto_memory_aux.lem
@@ -347,6 +347,8 @@ let rec simplify_integer_value_base ival_ =
             (* TOOD: move the code from mem_simplify here *)
             | Union tag_sym ->
                 Right ival_ (* error "TODO simplify_integer_value: IVsizeof Union" *)
+            | Byte ->
+                Left 1
           end
       | IValignof (Ctype _ ty) ->
           match ty with
@@ -384,6 +386,8 @@ let rec simplify_integer_value_base ival_ =
                 Right ival_
             | Union tag_sym ->
                 error "TODO simplify_integer_value: IValignof Union"
+            | Byte ->
+                Left 1
           end
       | IVoffsetof _ _ ->
           Right ival_
diff --git a/frontend/model/implementation.lem b/frontend/model/implementation.lem
@@ -676,6 +676,8 @@ let rec normalise_ctype (Ctype annots ty_) =
         ty_
     | Union _ ->
         ty_
+    | Byte ->
+        ty_
   end
 
 
diff --git a/memory/concrete/impl_mem.ml b/memory/concrete/impl_mem.ml
@@ -23,7 +23,8 @@ let ctype_mem_compatible ty1 ty2 =
       | Void
       | Basic _
       | Struct _
-      | Union _ ->
+      | Union _
+      | Byte ->
           ty
       | Function ((_, ret_ty), xs, b) ->
           Function (
@@ -187,6 +188,8 @@ and sizeof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) : N.num =
               let x = modulus max_size max_align in
               if equal x zero then max_size else add max_size (sub max_align x)
         end
+    | Byte ->
+      of_int 1
 
 and alignof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) =
   match ty with
@@ -265,6 +268,8 @@ and alignof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) =
                 max memb_align acc
               ) 0 membrs
         end
+    | Byte ->
+      1
 
 
 module Concrete : Memory = struct
@@ -951,6 +956,20 @@ module Concrete : Memory = struct
               | None ->
                   MVunspecified cty
             end , bs2)
+      | Byte ->
+          (* should be handled similarly to integers *)
+          let (bs1, bs2) = L.split_at 1 bs in
+          let (prov, bs1') = AbsByte.pvi_split_bytes bs1 in
+            (* PNVI-ae-udi *)
+          ( AbsByte.provs_of_bytes bs1
+          , begin match extract_unspec bs1' with
+              | Some cs ->
+                  let char_signed = (Ocaml_implementation.get ()).is_signed_ity Char  in
+                  MVinteger ( Char
+                            , mk_ival prov (int_of_bytes char_signed cs))
+              | None ->
+                  MVunspecified cty
+            end , bs2)
       | Basic (Floating fty) ->
           let (bs1, bs2) = L.split_at (N.to_int (sizeof cty)) bs in
           (* we don't care about provenances for floats *)
@@ -1055,7 +1074,7 @@ module Concrete : Memory = struct
           if is_zap then
             (* TODO: hack to prevent pointer zap from crashing if a union is in the memory *)
             ( `NoTaint, MVunspecified cty, bs2)
-          else match Pmap.find tag_sym (Tags.tagDefs ()) with
+          else (match Pmap.find tag_sym (Tags.tagDefs ()) with
             | _, UnionDef ((first_membr_def :: _) as membrs) ->
                 let (membr_ident, (_, _, _, membr_ty)) =
                   match IntMap.find_opt addr unionmap with
@@ -1070,7 +1089,7 @@ module Concrete : Memory = struct
                 let (taint, mval, _ ) = self membr_ty bs1 in
                 (taint, MVunion (tag_sym, membr_ident, mval), bs2)
             | _ ->
-                assert false
+                assert false)
 
   (* INTERNAL bytes_of_int *)
   let bytes_of_int is_signed size i : (char option) list =
@@ -1351,7 +1370,8 @@ module Concrete : Memory = struct
           None
       | Some (Ctype (_, Basic _))
       | Some (Ctype (_, Union _))
-      | Some (Ctype (_, Pointer _)) ->
+      | Some (Ctype (_, Pointer _))
+      | Some (Ctype (_, Byte)) ->
           let offset = N.sub addr alloc.base in
           Some (string_of_prefix alloc.prefix ^ " + " ^ N.to_string offset)
       | Some (Ctype (_, Struct tag_sym)) -> (* TODO: nested structs *)
diff --git a/memory/vip/common.ml b/memory/vip/common.ml
@@ -98,6 +98,8 @@ and sizeof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) =
               let x = max_size mod max_align in
               if x = 0 then max_size else max_size + (max_align - x)
         end
+    | Byte ->
+        1
 
 and alignof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) =
   match ty with
@@ -176,6 +178,8 @@ and alignof ?(tagDefs= Tags.tagDefs ()) (Ctype (_, ty) as cty) =
                 max memb_align acc
               ) 0 membrs
         end
+    | Byte ->
+        1
 
 let ity_max ity =
   let open Nat_big_num in
diff --git a/memory/vip/impl_mem.ml b/memory/vip/impl_mem.ml
@@ -448,6 +448,24 @@ match ty with
          | `UNSPECIFIED ->
              MVunspecified cty
        end , bs2)
+ | Byte ->
+     let (bs1, bs2) = L.split_at (Common.sizeof cty) bs in
+     ( begin match interp_bytes bs1 with
+         | `SPECIFIED (prov_status, _, cs, _) ->
+             let char_signed = (Ocaml_implementation.get ()).is_signed_ity Char in
+             let n = int_of_bytes char_signed cs in
+             MVinteger ( Char
+                       , match prov_status with
+                           | `NOPROV ->
+                               IVint n
+                           | `PROV alloc_id ->
+                               (* Printf.printf "IN abst() ==> cs: %s ==> IVloc n: %s\n"
+                                 (String.concat ", " (List.map (fun c -> string_of_int (int_of_char c)) cs))
+                                 (N.to_string n); *)
+                               IVloc (Prov_some alloc_id, n))
+         | `UNSPECIFIED ->
+             MVunspecified cty
+       end , bs2)
  | Basic (Floating fty) ->
      let (bs1, bs2) = L.split_at (Common.sizeof cty) bs in
      (* let (_, _, bs1') = AbsByte.split_bytes bs1 in *)
diff --git a/ocaml_frontend/core_remove_unused_functions.ml b/ocaml_frontend/core_remove_unused_functions.ml
@@ -232,6 +232,7 @@ let deps_of fn_or_impl : ('a,'bty,'sym) name_collector =
     | Atomic ct -> names_in_ctype ct
     | Struct sym -> record_dep (Sym sym)
     | Union sym -> record_dep (Sym sym)
+    | Byte -> return ()
   in
 
   let rec names_in_core_object_type = function
diff --git a/ocaml_frontend/ocaml_implementation.ml b/ocaml_frontend/ocaml_implementation.ml
@@ -507,6 +507,8 @@ let rec alignof ?(tagDefs= alignof_tagDefs_aux ()) (Ctype (_, ty)) =
             | _ ->
                 None
         ) (Some 1) (Pmap.find tag_sym tagDefs)
+    | Byte ->
+      Some 1
 
 let alignof_proxy tagDefs =
   alignof ~tagDefs
diff --git a/ocaml_frontend/pprinters/pp_ail.ml b/ocaml_frontend/pprinters/pp_ail.ml
@@ -250,6 +250,8 @@ let pp_ctype_aux ~is_human pp_ident_opt qs (Ctype (_, ty) as cty) =
         2
     | Pointer _ ->
         3
+    | Byte ->
+        4
   in
   let rec aux p qs (Ctype (annots, ty)) : P.document -> P.document =
     let annot_doc = if !executable_spec then
@@ -304,7 +306,10 @@ let pp_ctype_aux ~is_human pp_ident_opt qs (Ctype (_, ty) as cty) =
           | Union sym ->
               fun k ->
                 pp_qualifiers qs ^^ pp_keyword "union" ^^^ pp_id_type ~is_human sym ^^ k
-        end) 
+          | Byte ->
+              fun k ->
+                pp_qualifiers qs ^^ pp_keyword "byte" ^^ k
+        end)
     in
   let pp_spaced_ident =
     match pp_ident_opt with Some pp_ident -> P.space ^^ pp_ident | None -> P.empty in
@@ -359,6 +364,8 @@ let rec pp_ctype_human qs (Ctype (_, ty)) =
         prefix_pp_qs ^^ !^ "struct" ^^^ pp_id tag_sym
     | Union tag_sym ->
         prefix_pp_qs ^^ !^ "union" ^^^ pp_id tag_sym
+    | Byte ->
+        prefix_pp_qs ^^ !^ "byte"
 
 (* -- EXPRESSIONS -- *)
 let pp_arithmeticOperator = function
@@ -1010,6 +1017,8 @@ let rec pp_genType = function
       !^ "union" ^^^ pp_id ~is_human:true tag_sym
   | GenAtomic gty ->
       !^ "atomic" ^^^ pp_genType gty
+  | GenByte ->
+      !^ "byte"
 
 let pp_genTypeCategory = function
  | GenLValueType (qs, ty, isRegister) ->
diff --git a/ocaml_frontend/pprinters/pp_ail_ast.ml b/ocaml_frontend/pprinters/pp_ail_ast.ml
@@ -66,6 +66,8 @@ let rec pp_ctype_human_aux qs (Ctype (_, ty)) =
         prefix_pp_qs ^^ !^ "struct" ^^^ Pp_ail.pp_id ~is_human:true tag_sym
     | Union tag_sym ->
         prefix_pp_qs ^^ !^ "union" ^^^ Pp_ail.pp_id ~is_human:true tag_sym
+    | Byte ->
+        prefix_pp_qs ^^ !^ "byte"
 
 and pp_ctype_human qs (Ctype (xs, _) as ty) =
   let typedef_opt = List.fold_left (fun acc_opt x ->
@@ -135,6 +137,8 @@ let rec pp_genType = function
       !^ "GenUnion" ^^ Pp_ail.pp_id ~is_human:true sym
   | GenAtomic gty ->
       !^ "GenAtomic" ^^ pp_genType gty
+  | GenByte ->
+      !^"GenByte"
 
 
 let pp_ctype qs ty =
diff --git a/ocaml_frontend/pprinters/pp_ail_raw.ml b/ocaml_frontend/pprinters/pp_ail_raw.ml
@@ -119,4 +119,6 @@ let rec pp_ctype_raw (Ctype (_,cty)) =
         pp_ctor "Struct" ^^^ pp_id sym
     | Union sym ->
         pp_ctor "Union" ^^^ pp_id sym
+    | Byte ->
+        pp_ctor "Byte"
 
diff --git a/ocaml_frontend/pprinters/pp_core_ctype.ml b/ocaml_frontend/pprinters/pp_core_ctype.ml
@@ -86,6 +86,8 @@ let rec pp_ctype (Ctype (_, ty)) =
       !^ "struct" ^^^ pp_symbol sym (*!^(Pp_symbol.to_string sym)*)
   | Union sym ->
       !^ "union" ^^^ pp_symbol sym (*!^(Pp_symbol.to_string sym)*)
+  | Byte ->
+      !^ "cn_byte"
 
 
 (*
diff --git a/parsers/core/core_parser.mly b/parsers/core/core_parser.mly
@@ -285,6 +285,8 @@ let rec symbolify_ctype (Ctype (annots, ty)) =
   | Union tag ->
       symbolify_symbol tag >>= fun tag' ->
       Eff.return (Union tag')
+  | Byte ->
+      Eff.return Byte
 
 let symbolify_value _cval =
   match _cval with

Original file line number	Diff line number	Diff line change
`@@ -58,6 +58,7 @@ type ctype_ ([name = "^\\([a-z A-Z]_\\)?ty[0-9]'?$"]) =`
`58`	`58`	`\| Atomic of ctype`
`59`	`59`	`\| Struct of Symbol.sym`
`60`	`60`	`\| Union of Symbol.sym`
	`61`	`+ \| Byte`
`61`	`62`	`and ctype =`
`62`	`63`	`Ctype of list Annot.annot * ctype_`
`63`	`64`
`@@ -150,6 +151,8 @@ let rec ctypeEqual (Ctype _ ty1) (Ctype _ ty2) =`
`150`	`151`	`7`
`151`	`152`	`\| Union _ ->`
`152`	`153`	`8`
	`154`	`+ \| Byte ->`
	`155`	`+ 9`
`153`	`156`	`end in`
`154`	`157`	`let paramsEqual (qs1, ty1, b1) (qs2, ty2, b2) =`
`155`	`158`	`qs1 = qs2 && ctypeEqual ty1 ty2 && b1 = b2 in`