formalsec / smtml / 479

Committed 04 Feb 2026 05:12PM UTC coverage: 45.274% (-0.07%) from 45.345%

Build # 479

Build Type

push

github

Committed by

filipeom

Commit Message

fix: Add i32.{to_bool, of_bool} cvtop evaluation functions (#531)

Closes #531

Run Details

0 of 6 new or added lines in 1 file covered. (0.0%)

283 existing lines in 4 files now uncovered.

958 of 2116 relevant lines covered (45.27%)

9.57 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

83.81

/src/smtml/bitvector.ml

type t =
  { value : Z.t
  ; width : int
  }

let mask width = Z.pred (Z.shift_left Z.one width)

let make v m =
  let masked_value = Z.logand v (mask m) in
  { value = masked_value; width = m }

let view { value; _ } = value

let numbits { width; _ } = width

let of_int8 v =
  (* TODO: add a check on v to make sure it is not too big ? *)
  make (Z.of_int v) 8

let of_int16 v =
  (* TODO: add a check on v to make sure it is not too big ? *)
  make (Z.of_int v) 16

let of_int32 v = make (Z.of_int32 v) 32

let of_int64 v = make (Z.of_int64 v) 64

(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
let[@inline] combine h v = (h * 33) + v

let hash a = combine (Z.hash a.value) a.width

let equal a b = Z.equal a.value b.value && a.width = b.width

let eqz v = Z.equal Z.zero v.value

let eq_one v = Z.equal Z.one v.value

let compare a b = Z.compare a.value b.value

let msb bv = Z.testbit bv.value (bv.width - 1)

let to_signed bv =
  let msb = msb bv in
  if msb then Z.sub bv.value (Z.shift_left Z.one bv.width) else bv.value

let to_int32 v =
  if numbits v <= 32 then Z.to_int32 (to_signed v)
  else
    Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"
      v.width

let to_int64 v =
  if numbits v <= 64 then Z.to_int64 (to_signed v)
  else
    Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"
      v.width

type printer =
  [ `Pretty  (** Human-readable format. *)
  | `WithType  (** Print with type info. *)
  ]

(** Bitvector pretty printer. By default it prints signed bitvectors. *)
let pp_bv fmt bv =
  let value = to_signed bv in
  Z.pp_print fmt value

let pp_wtype fmt bv =
  let value = to_signed bv in
  Fmt.pf fmt "(i%d %a)" bv.width Z.pp_print value

let printer = ref pp_bv

let set_default_printer = function
  | `Pretty -> printer := pp_bv
  | `WithType -> printer := pp_wtype

let pp fmt e = !printer fmt e

(* Unop *)
let neg bv = make (Z.neg bv.value) bv.width

let lognot a = make (Z.lognot a.value) a.width

let clz bv =
  let rec count_zeros i =
    if i >= bv.width || Z.testbit bv.value (bv.width - 1 - i) then i
    else count_zeros (i + 1)
  in
  make (Z.of_int @@ count_zeros 0) bv.width

let ctz bv =
  let rec count_zeros i =
    if i >= bv.width || Z.testbit bv.value i then i else count_zeros (i + 1)
  in
  make (Z.of_int @@ count_zeros 0) bv.width

let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width

(* Binop *)
let add a b =
  assert (a.width = b.width);
  make (Z.add a.value b.value) a.width

let sub a b =
  assert (a.width = b.width);
  make (Z.sub a.value b.value) a.width

let mul a b =
  assert (a.width = b.width);
  make (Z.mul a.value b.value) a.width

let div a b =
  assert (a.width = b.width);
  if Z.equal b.value Z.zero then raise Division_by_zero;
  make (Z.div (to_signed a) (to_signed b)) a.width

let div_u a b =
  assert (a.width = b.width);
  if Z.equal b.value Z.zero then raise Division_by_zero;
  make (Z.div a.value b.value) a.width

let logand a b =
  assert (a.width = b.width);
  make (Z.logand a.value b.value) a.width

let logor a b =
  assert (a.width = b.width);
  make (Z.logor a.value b.value) a.width

let logxor a b =
  assert (a.width = b.width);
  make (Z.logxor a.value b.value) a.width

let normalize_shift_amount n width =
  (* FIXME: only works for widths that are powers of 2. *)
  assert (width > 0 && width land (width - 1) = 0);
  Z.to_int @@ Z.logand n (Z.of_int (width - 1))

let shl a n =
  let n = normalize_shift_amount (view n) (numbits a) in
  make (Z.shift_left a.value n) a.width

let ashr a n =
  let n = normalize_shift_amount (view n) (numbits a) in
  let signed_value = to_signed a in
  make (Z.shift_right signed_value n) a.width

let lshr a n =
  let n = normalize_shift_amount (view n) (numbits a) in
  make (Z.shift_right_trunc a.value n) a.width

let rem a b =
  assert (a.width = b.width);
  if Z.equal b.value Z.zero then raise Division_by_zero;
  make (Z.rem (to_signed a) (to_signed b)) a.width

let rem_u a b =
  assert (a.width = b.width);
  if Z.equal b.value Z.zero then raise Division_by_zero;
  make (Z.rem a.value b.value) a.width

let rotate_left bv n =
  let n = normalize_shift_amount (view n) (numbits bv) in
  let left_part = Z.shift_left bv.value n in
  let right_part = Z.shift_right bv.value (bv.width - n) in
  let rotated = Z.logor left_part right_part in
  make rotated bv.width

let rotate_right bv n =
  let n = normalize_shift_amount (view n) (numbits bv) in
  let right_part = Z.shift_right bv.value n in
  let left_part = Z.shift_left bv.value (bv.width - n) in
  let rotated = Z.logor left_part right_part in
  make rotated bv.width

(* Relop *)
let lt_u a b = Z.lt a.value b.value

let gt_u a b = Z.gt a.value b.value

let le_u a b = Z.leq a.value b.value

let ge_u a b = Z.geq a.value b.value

let lt a b = Z.lt (to_signed a) (to_signed b)

let gt a b = Z.gt (to_signed a) (to_signed b)

let le a b = Z.leq (to_signed a) (to_signed b)

let ge a b = Z.geq (to_signed a) (to_signed b)

(* Extract and concat *)
let concat a b =
  let new_width = a.width + b.width in
  let shifted = Z.shift_left a.value b.width in
  let combined = Z.logor shifted b.value in
  make combined new_width

let extract bv ~high ~low =
  assert (high < bv.width && low >= 0 && low <= high);
  let width = high - low + 1 in
  let shifted = Z.shift_right bv.value low in
  let extracted = Z.logand shifted (mask width) in
  make extracted width

(* Cvtop *)
let zero_extend width bv =
  let new_width = bv.width + width in
  make bv.value new_width

let sign_extend width bv =
  let new_width = bv.width + width in
  let msb = msb bv in
  let sign_mask =
    if msb then
      let shift_amount = bv.width in
      Z.shift_left (mask width) shift_amount
    else Z.zero
  in
  let extended = Z.logor bv.value sign_mask in
  make extended new_width

let to_string bv = Fmt.str "%a" pp bv

let to_json bv = `String (to_string bv)

1	type t =
2	{ value : Z.t
3	; width : int
4	}
5
6	let mask width = Z.pred (Z.shift_left Z.one width)	464✔
7
8	let make v m =
9	let masked_value = Z.logand v (mask m) in	449✔
10	{ value = masked_value; width = m }	449✔
11
12	let view { value; _ } = value	19✔
13
14	let numbits { width; _ } = width	47✔
15
16	let of_int8 v =
17	(* TODO: add a check on v to make sure it is not too big ? *)
18	make (Z.of_int v) 8	7✔
19
20	let of_int16 v =
21	(* TODO: add a check on v to make sure it is not too big ? *)
22	make (Z.of_int v) 16	×
23
24	let of_int32 v = make (Z.of_int32 v) 32	150✔
25
26	let of_int64 v = make (Z.of_int64 v) 64	105✔
27
28	(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
29	let[@inline] combine h v = (h * 33) + v	302✔
30
31	let hash a = combine (Z.hash a.value) a.width	302✔
32
33	let equal a b = Z.equal a.value b.value && a.width = b.width	221✔
34
35	let eqz v = Z.equal Z.zero v.value	14✔
36
37	let eq_one v = Z.equal Z.one v.value	8✔
38
39	let compare a b = Z.compare a.value b.value	×
40
41	let msb bv = Z.testbit bv.value (bv.width - 1)	77✔
42
43	let to_signed bv =
44	let msb = msb bv in	71✔
45	if msb then Z.sub bv.value (Z.shift_left Z.one bv.width) else bv.value	8✔
46
47	let to_int32 v =
48	if numbits v <= 32 then Z.to_int32 (to_signed v)	9✔
49	else
50	Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"	×
51	v.width
52
53	let to_int64 v =
54	if numbits v <= 64 then Z.to_int64 (to_signed v)	12✔
55	else
56	Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"	×
57	v.width
58
59	type printer =
60	[ `Pretty (** Human-readable format. *)
61	\| `WithType (** Print with type info. *)
62	]
63
64	(** Bitvector pretty printer. By default it prints signed bitvectors. *)
65	let pp_bv fmt bv =
66	let value = to_signed bv in	2✔
67	Z.pp_print fmt value	2✔
68
69	let pp_wtype fmt bv =
70	let value = to_signed bv in	×
71	Fmt.pf fmt "(i%d %a)" bv.width Z.pp_print value	×
72
73	let printer = ref pp_bv
74
75	let set_default_printer = function
76	\| `Pretty -> printer := pp_bv	×
77	\| `WithType -> printer := pp_wtype	×
78
79	let pp fmt e = !printer fmt e	2✔
80
81	(* Unop *)
82	let neg bv = make (Z.neg bv.value) bv.width	3✔
83
84	let lognot a = make (Z.lognot a.value) a.width	3✔
85
86	let clz bv =
87	let rec count_zeros i =	1✔
88	if i >= bv.width \|\| Z.testbit bv.value (bv.width - 1 - i) then i	×
89	else count_zeros (i + 1)	7✔
90	in
91	make (Z.of_int @@ count_zeros 0) bv.width	1✔
92
93	let ctz bv =
94	let rec count_zeros i =	1✔
95	if i >= bv.width \|\| Z.testbit bv.value i then i else count_zeros (i + 1)	×
96	in
97	make (Z.of_int @@ count_zeros 0) bv.width	1✔
98
99	let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width	1✔
100
101	(* Binop *)
102	let add a b =
103	assert (a.width = b.width);	12✔
104	make (Z.add a.value b.value) a.width	12✔
105
106	let sub a b =
107	assert (a.width = b.width);	5✔
108	make (Z.sub a.value b.value) a.width	5✔
109
110	let mul a b =
111	assert (a.width = b.width);	5✔
112	make (Z.mul a.value b.value) a.width	5✔
113
114	let div a b =
115	assert (a.width = b.width);	3✔
116	if Z.equal b.value Z.zero then raise Division_by_zero;	×
117	make (Z.div (to_signed a) (to_signed b)) a.width	3✔
118
119	let div_u a b =
120	assert (a.width = b.width);	1✔
121	if Z.equal b.value Z.zero then raise Division_by_zero;	×
122	make (Z.div a.value b.value) a.width	1✔
123
124	let logand a b =
125	assert (a.width = b.width);	3✔
126	make (Z.logand a.value b.value) a.width	3✔
127
128	let logor a b =
129	assert (a.width = b.width);	3✔
130	make (Z.logor a.value b.value) a.width	3✔
131
132	let logxor a b =
133	assert (a.width = b.width);	3✔
134	make (Z.logxor a.value b.value) a.width	3✔
135
136	let normalize_shift_amount n width =
137	(* FIXME: only works for widths that are powers of 2. *)
138	assert (width > 0 && width land (width - 1) = 0);	18✔
139	Z.to_int @@ Z.logand n (Z.of_int (width - 1))	18✔
140
141	let shl a n =
142	let n = normalize_shift_amount (view n) (numbits a) in	4✔
143	make (Z.shift_left a.value n) a.width	4✔
144
145	let ashr a n =
146	let n = normalize_shift_amount (view n) (numbits a) in	4✔
147	let signed_value = to_signed a in	4✔
148	make (Z.shift_right signed_value n) a.width	4✔
149
150	let lshr a n =
151	let n = normalize_shift_amount (view n) (numbits a) in	2✔
152	make (Z.shift_right_trunc a.value n) a.width	2✔
153
154	let rem a b =
155	assert (a.width = b.width);	3✔
156	if Z.equal b.value Z.zero then raise Division_by_zero;	×
157	make (Z.rem (to_signed a) (to_signed b)) a.width	3✔
158
159	let rem_u a b =
160	assert (a.width = b.width);	×
161	if Z.equal b.value Z.zero then raise Division_by_zero;	×
162	make (Z.rem a.value b.value) a.width	×
163
164	let rotate_left bv n =
165	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
166	let left_part = Z.shift_left bv.value n in	4✔
167	let right_part = Z.shift_right bv.value (bv.width - n) in	4✔
168	let rotated = Z.logor left_part right_part in	4✔
169	make rotated bv.width	4✔
170
171	let rotate_right bv n =
172	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
173	let right_part = Z.shift_right bv.value n in	4✔
174	let left_part = Z.shift_left bv.value (bv.width - n) in	4✔
175	let rotated = Z.logor left_part right_part in	4✔
176	make rotated bv.width	4✔
177
178	(* Relop *)
179	let lt_u a b = Z.lt a.value b.value	6✔
180
181	let gt_u a b = Z.gt a.value b.value	1✔
182
183	let le_u a b = Z.leq a.value b.value	5✔
184
UNCOV 185	let ge_u a b = Z.geq a.value b.value	×
186
187	let lt a b = Z.lt (to_signed a) (to_signed b)	7✔
188
189	let gt a b = Z.gt (to_signed a) (to_signed b)	1✔
190
191	let le a b = Z.leq (to_signed a) (to_signed b)	7✔
192
193	let ge a b = Z.geq (to_signed a) (to_signed b)	1✔
194
195	(* Extract and concat *)
196	let concat a b =
197	let new_width = a.width + b.width in	7✔
198	let shifted = Z.shift_left a.value b.width in
199	let combined = Z.logor shifted b.value in	7✔
200	make combined new_width	7✔
201
202	let extract bv ~high ~low =
203	assert (high < bv.width && low >= 0 && low <= high);	11✔
204	let width = high - low + 1 in
205	let shifted = Z.shift_right bv.value low in
206	let extracted = Z.logand shifted (mask width) in	11✔
207	make extracted width	11✔
208
209	(* Cvtop *)
210	let zero_extend width bv =
211	let new_width = bv.width + width in	5✔
212	make bv.value new_width
213
214	let sign_extend width bv =
215	let new_width = bv.width + width in	6✔
216	let msb = msb bv in
217	let sign_mask =	6✔
218	if msb then
219	let shift_amount = bv.width in	4✔
220	Z.shift_left (mask width) shift_amount	4✔
221	else Z.zero	2✔
222	in
223	let extended = Z.logor bv.value sign_mask in
224	make extended new_width	6✔
225
226	let to_string bv = Fmt.str "%a" pp bv	2✔
227
228	let to_json bv = `String (to_string bv)	2✔

formalsec / smtml / 479

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous