Skip to content

Commit 9eb2ce2

Browse files
dc-makkmemarian
dc-mak
authored and
kmemarian
committed
Make Byte casts have no UB
As per offline review feedback, this commit makes the casts use wrapping conversions instead of having them be UB. This also fixes the incorrect (and ad-hoc) behaviour of the IntFromByte. Both operations now use conv_int to wrap appropriately.
1 parent 20681df commit 9eb2ce2

10 files changed

Lines changed: 28 additions & 56 deletions

File tree

‎frontend/model/core_eval.lem‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -782,8 +782,8 @@ let rec step_eval_pexpr n loc parent_call_loc_opt core_extern env mem_st_opt fil
782782
, Just [ Core.Vobject (Core.OVinteger ival) ] ) ->
783783
EU.return (PEval (Vobject (OVinteger (Mem.bytefromint loc ival))))
784784
| ( Mem_common.IntFromByte
785-
, Just [ Core.Vctype (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity))); Core.Vobject (Core.OVinteger ival) ] ) ->
786-
EU.return (PEval (Vobject (OVinteger (Mem.intfrombyte loc ity ival))))
785+
, Just [ Core.Vobject (Core.OVinteger ival) ] ) ->
786+
EU.return (PEval (Vobject (OVinteger (Mem.intfrombyte loc ival))))
787787
| (_, Just _) ->
788788
EU.fail $ Illformed_program "PEmemop"
789789
| (_, Nothing) ->

‎frontend/model/core_typing.lem‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -606,10 +606,9 @@ let rec infer_pexpr tagDefs env ((Pexpr annot _ pexpr_ as pexpr) : generic_pexpr
606606
| PEmemop Mem_common.ByteFromInt [pe] ->
607607
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe >>= fun pe' ->
608608
E.return (Pexpr annot (InferredType_object OTy_integer) (PEmemop Mem_common.ByteFromInt [pe']))
609-
| PEmemop Mem_common.IntFromByte [pe1; pe2] ->
610-
typecheck_pexpr tagDefs env BTy_ctype pe1 >>= fun pe1' ->
611-
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe2 >>= fun pe2' ->
612-
E.return (Pexpr annot (InferredType_object OTy_integer) (PEmemop Mem_common.IntFromByte [pe1'; pe2']))
609+
| PEmemop Mem_common.IntFromByte [pe] ->
610+
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe >>= fun pe' ->
611+
E.return (Pexpr annot (InferredType_object OTy_integer) (PEmemop Mem_common.IntFromByte [pe']))
613612
| PEmemop _ _ ->
614613
E.fail loc (CoreTyping_TODO (Pp.stringFromCore_pexpr pexpr))
615614
| PEnot pe ->
@@ -1003,11 +1002,10 @@ and typecheck_pexpr tagDefs (env: typing_env) (bTy: core_base_type) (Pexpr annot
10031002
guard_match loc "memop(bytefromtint)" bTy (BTy_object OTy_integer) >>
10041003
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe >>= fun pe' ->
10051004
E.return (PEmemop Mem_common.ByteFromInt [pe'])
1006-
| PEmemop Mem_common.IntFromByte [pe1; pe2] ->
1005+
| PEmemop Mem_common.IntFromByte [pe] ->
10071006
guard_match loc "memop(intfrombyte)" bTy (BTy_object OTy_integer) >>
1008-
typecheck_pexpr tagDefs env BTy_ctype pe1 >>= fun pe1' ->
1009-
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe2 >>= fun pe2' ->
1010-
E.return (PEmemop Mem_common.IntFromByte [pe1'; pe2'])
1007+
typecheck_pexpr tagDefs env (BTy_object OTy_integer) pe >>= fun pe' ->
1008+
E.return (PEmemop Mem_common.IntFromByte [pe'])
10111009
| PEmemop _ _ ->
10121010
E.fail loc (CoreTyping_TODO (Pp.stringFromCore_pexpr pexpr))
10131011
| PEnot pe ->

‎frontend/model/mem.lem‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ declare ocaml target_rep function copy_alloc_id = `Impl_mem.copy_alloc_id`
176176

177177
(* Byte casting operations *)
178178
val bytefromint: Loc.t -> integer_value -> integer_value
179-
val intfrombyte: Loc.t -> Ctype.integerType -> integer_value -> integer_value
179+
val intfrombyte: Loc.t -> integer_value -> integer_value
180180
declare ocaml target_rep function bytefromint = `Impl_mem.bytefromint`
181181
declare ocaml target_rep function intfrombyte = `Impl_mem.intfrombyte`
182182

‎frontend/model/mem_common.lem‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -366,7 +366,7 @@ type pure_memop =
366366
| Ptr_tIntValue
367367
(* Bytes *)
368368
| ByteFromInt (* integer -> byte *)
369-
| IntFromByte (* (integerType, byte) -> integer *)
369+
| IntFromByte (* byte -> integer *)
370370

371371
type generic_memop 'sym =
372372
| PtrEq

‎frontend/model/translation.lem‎

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1944,14 +1944,10 @@ else if AilTypesAux.is_byte cast_ty && AilTypesAux.is_integer e_ty then
19441944
Caux.mk_pure_e (
19451945
Caux.mk_case_pe e_wrp.E.sym_pe
19461946
[ ( Caux.mk_specified_pat obj_wrp.E.sym_pat
1947-
, Caux.mk_if_pe
1948-
(Caux.mk_op_pe C.OpOr
1949-
(Caux.mk_op_pe C.OpLt obj_wrp.E.sym_pe (Caux.mk_integer_pe (~128)))
1950-
(Caux.mk_op_pe C.OpLt (Caux.mk_integer_pe 255) obj_wrp.E.sym_pe))
1951-
(Caux.mk_undef_pe loc Undefined.UB_Byte_invalid_byte_value)
1952-
(Caux.mk_let_pe (Caux.mk_sym_pat let_sym (C.BTy_object C.OTy_integer (* byte *)))
1953-
(Caux.mk_memop_pe Mem_common.ByteFromInt [obj_wrp.E.sym_pe])
1954-
((Caux.mk_specified_pe (Caux.mk_sym_pe let_sym)))) )
1947+
, Caux.mk_let_pe (Caux.mk_sym_pat let_sym (C.BTy_object C.OTy_integer (* byte *)))
1948+
(* only integer values valid for a Ctype.unsigned_char can be cast to a byte *)
1949+
(Caux.mk_memop_pe Mem_common.ByteFromInt [stdlib.mkcall_conv_int Ctype.unsigned_char obj_wrp.E.sym_pe])
1950+
((Caux.mk_specified_pe (Caux.mk_sym_pe let_sym))) )
19551951
; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype)
19561952
, (* Casting an unspecified integer to a byte type gives an unspecified byte *)
19571953
Caux.mk_unspecified_pe cast_ty ) ]
@@ -1964,7 +1960,7 @@ else if AilTypesAux.is_integer cast_ty && AilTypesAux.is_byte e_ty then
19641960
Caux.mk_case_pe e_wrp.E.sym_pe
19651961
[ ( Caux.mk_specified_pat obj_wrp.E.sym_pat
19661962
, Caux.mk_let_pe (Caux.mk_sym_pat let_sym (C.BTy_object C.OTy_integer))
1967-
(Caux.mk_memop_pe Mem_common.IntFromByte [Caux.mk_ail_ctype_pe cast_ty; obj_wrp.E.sym_pe])
1963+
(stdlib.mkcall_conv_int cast_ty (Caux.mk_memop_pe Mem_common.IntFromByte [obj_wrp.E.sym_pe]))
19681964
(Caux.mk_specified_pe (Caux.mk_sym_pe let_sym)) )
19691965
; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype)
19701966
, (* Casting an unspecified byte to an integer type gives an unspecified integer *)

‎frontend/model/undefined.lem‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -731,9 +731,6 @@ type undefined_behaviour =
731731
(* free() is called on a NULL pointer (used in switch stricter than ISO) *)
732732
| UB_CERB005_free_nullptr
733733

734-
(* bytes *)
735-
| UB_Byte_invalid_byte_value
736-
737734
val std_of_undefined_behaviour: undefined_behaviour -> maybe string
738735
let std_of_undefined_behaviour = function
739736
| UB004a_incorrect_main_return_type ->
@@ -1089,7 +1086,6 @@ let ub_str_bimap =
10891086
; (UB_CHERI_BoundsViolation,"UB_CHERI_BoundsViolation")
10901087
; (UB_CHERI_UndefinedTag,"UB_CHERI_UndefinedTag")
10911088
; (UB_CHERI_ZeroLength,"UB_CHERI_ZeroLength")
1092-
; (UB_Byte_invalid_byte_value,"UB_Byte_invalid_byte_value")
10931089
]
10941090

10951091

@@ -1250,8 +1246,6 @@ let ub_short_string = function
12501246
"out of bounds pointer in realloc()"
12511247
| UB_CERB003_invalid_function_pointer ->
12521248
"invalid function pointer"
1253-
| UB_Byte_invalid_byte_value ->
1254-
"invalid byte value"
12551249
| ub ->
12561250
"(UB missing short message): " ^ show ub
12571251
end
@@ -1421,8 +1415,6 @@ let pretty_string_of_undefined_behaviour = function
14211415
"a call to 'free()' is given a 'NULL' pointer"
14221416
| Invalid_format str ->
14231417
"Invalid_format \"" ^ str ^ "\""
1424-
| UB_Byte_invalid_byte_value ->
1425-
"conversion to byte given unrepresentable value"
14261418
| ub ->
14271419
"(UB missing short message): " ^ show ub
14281420
end

‎memory/concrete/impl_mem.ml‎

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2769,18 +2769,13 @@ VIP:type pointer_value =
27692769
(* Bytes are always typedef'd to unsigned chars, and I'm assuming unsigned
27702770
chars are always 8 bits. This function flips the interpretation of the
27712771
leading bit if it is 1. *)
2772-
let bytefromint loc (IV (prov, intval) as ival) =
2773-
assert (N.(less_equal (of_int (-128)) intval && less_equal intval (of_int 255)));
2774-
if N.(less_equal zero intval) then
2775-
ival
2776-
else
2777-
(IV (prov, N.(add intval (of_int 256))))
2778-
2779-
let intfrombyte _loc ity (IV (prov, intval) as ival) =
2780-
if (AilTypesAux.is_signed_ity ity && N.(greater_equal intval (of_int 128))) then
2781-
IV (prov, N.(sub intval (of_int 256)))
2782-
else
2783-
ival
2772+
let bytefromint loc (IV (_, intval) as ival) =
2773+
assert (N.(less_equal (of_int 0) intval && less_equal intval (of_int 255)));
2774+
ival
2775+
2776+
let intfrombyte _loc (IV (_, intval) as ival) =
2777+
assert (N.(less_equal (of_int 0) intval && less_equal intval (of_int 255)));
2778+
ival
27842779

27852780
(* JSON serialisation: Memory layout for UI *)
27862781

‎memory/vip/impl_mem.ml‎

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -980,18 +980,13 @@ let update_ival ival x =
980980
leading bit if it is 1. *)
981981
let bytefromint _loc ival : integer_value =
982982
let intval = match ival with IVloc (_, i) | IVint i -> i in
983-
assert (N.(less_equal (of_int (-128)) intval && less_equal intval (of_int 255)));
984-
if N.(less_equal zero intval) then
985-
ival
986-
else
987-
update_ival ival (N.(add intval (of_int 256)))
983+
assert (N.(less_equal (of_int 0) intval && less_equal intval (of_int 255)));
984+
ival
988985

989-
let intfrombyte _loc ity ival : integer_value =
986+
let intfrombyte _loc ival : integer_value =
990987
let intval = match ival with IVloc (_, i) | IVint i -> i in
991-
if (AilTypesAux.is_signed_ity ity && N.(greater_equal intval (of_int 128))) then
992-
update_ival ival N.(sub intval (of_int 256))
993-
else
994-
ival
988+
assert (N.(less_equal (of_int 0) intval && less_equal intval (of_int 255)));
989+
ival
995990

996991

997992
(* Integer value constructors *)

‎ocaml_frontend/memory_model.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@ module type Memory = sig
126126

127127
(* Byte casting operations *)
128128
val bytefromint: Cerb_location.t -> integer_value -> integer_value
129-
val intfrombyte: Cerb_location.t -> Ctype.integerType -> integer_value -> integer_value
129+
val intfrombyte: Cerb_location.t -> integer_value -> integer_value
130130

131131

132132
(* Integer value constructors *)

‎tests/bytes/cast_256_byte.exec.c.exec‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1 @@
11
return code: 0
2-
bytes/cast_256_byte.exec.c:7:5: error: undefined behaviour: invalid byte value
3-
(byte)256;
4-
^~~~~~~~~
5-
no C11 reference

0 commit comments

Comments
 (0)