Skip to content

Commit 22a233b

Browse files
alastairreidalastairreid
committed
C23 runtime: fix integer promotion issues
Part of the fun of C's integer promotion rules is that, if you add 2 8-bit unsigned values, the operation could produce a different size of result because of the context that the operation is performed in. For example, if a and b are 8 bits, then uint64_t x = (uint64_t)(a + b); could result in a 64-bit addition and, therefore, x[63:16] may not be zero. (In particular, x[16] could be 1) The way to guard against this context-dependent promotion is to explicitly cast the result of every arithmetic operation to the expected size. For example, we calculate x like this uint64_t x = (uint64_t)(uint8_t)(x + y); This commit inserts additional casts in every place that we think an unintended promotion could occur.
1 parent d97ab74 commit 22a233b

File tree

1 file changed

+46
-21
lines changed

1 file changed

+46
-21
lines changed

Diff for: ‎libASL/runtime_c23.ml

+46-21
Original file line numberDiff line numberDiff line change
@@ -108,22 +108,54 @@ module Runtime : RT.RuntimeLib = struct
108108
op
109109
RT.pp_expr y
110110

111+
(* Binary operation that returns bits(N).
112+
* The result is explicitly cast to bits(N) to prevent the C integer promotion
113+
* rules from changing the width or sign of the operation.
114+
*)
115+
let binop_bits (fmt : PP.formatter) (n : int) (op : string) (x : RT.rt_expr) (y : RT.rt_expr) : unit =
116+
PP.fprintf fmt "((%a)(%a %s %a))"
117+
ty_bits n
118+
RT.pp_expr x
119+
op
120+
RT.pp_expr y
121+
122+
(* Unary operation that returns __sint(N).
123+
* The result is explicitly cast to __sint(N) to prevent the C integer promotion
124+
* rules from changing the width or sign of the operation.
125+
*)
126+
let unop_sintN (fmt : PP.formatter) (n : int) (op : string) (x : RT.rt_expr) : unit =
127+
PP.fprintf fmt "((%a)(%s %a))"
128+
ty_sint n
129+
op
130+
RT.pp_expr x
131+
132+
(* Binary operation that returns __sint(N).
133+
* The result is explicitly cast to __sint(N) to prevent the C integer promotion
134+
* rules from changing the width or sign of the operation.
135+
*)
136+
let binop_sintN (fmt : PP.formatter) (n : int) (op : string) (x : RT.rt_expr) (y : RT.rt_expr) : unit =
137+
PP.fprintf fmt "((%a)(%a %s %a))"
138+
ty_sint n
139+
RT.pp_expr x
140+
op
141+
RT.pp_expr y
142+
111143
(* signed sized integer functions *)
112144
let eq_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "==" x y
113145
let ne_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "!=" x y
114146
let ge_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt ">=" x y
115147
let gt_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt ">" x y
116148
let le_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "<=" x y
117149
let lt_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "<" x y
118-
let add_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "+" x y
119-
let neg_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = unop fmt "-" x
120-
let sub_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "-" x y
121-
let mul_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "*" x y
122-
let shr_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt ">>" x y
123-
let shl_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "<<" x y
124-
let exact_div_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "/" x y
125-
let zdiv_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "/" x y
126-
let zrem_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "%" x y
150+
let add_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "+" x y
151+
let neg_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = unop_sintN fmt n "-" x
152+
let sub_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "-" x y
153+
let mul_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "*" x y
154+
let shr_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n ">>" x y
155+
let shl_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "<<" x y
156+
let exact_div_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "/" x y
157+
let zdiv_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "/" x y
158+
let zrem_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_sintN fmt n "%" x y
127159

128160
let fdiv_sintN (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit =
129161
PP.fprintf fmt "({ %a __tmp1 = %a; "
@@ -398,16 +430,9 @@ module Runtime : RT.RuntimeLib = struct
398430

399431
let eq_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "==" x y
400432
let ne_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "!=" x y
401-
let add_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "+" x y
402-
let sub_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit =
403-
(* Subtraction is awkward because even though the inputs are unsigned, the result seems to be signed
404-
* and so we explicitly cast the result back to unsigned.
405-
*)
406-
PP.fprintf fmt "((%a)(%a - %a))"
407-
ty_bits n
408-
RT.pp_expr x
409-
RT.pp_expr y
410-
let mul_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "*" x y
433+
let add_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_bits fmt n "+" x y
434+
let sub_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_bits fmt n "-" x y
435+
let mul_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_bits fmt n "*" x y
411436
let and_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "&" x y
412437
let or_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "|" x y
413438
let eor_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "^" x y
@@ -419,8 +444,8 @@ module Runtime : RT.RuntimeLib = struct
419444
else
420445
unop fmt "~" x
421446

422-
let lsl_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt "<<" x y
423-
let lsr_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop fmt ">>" x y
447+
let lsl_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_bits fmt n "<<" x y
448+
let lsr_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit = binop_bits fmt n ">>" x y
424449

425450
let asr_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) (y : RT.rt_expr) : unit =
426451
PP.fprintf fmt "((%a)(((%a)%a) >> %a))"

0 commit comments

Comments
 (0)