formalsec / smtml / 507

Committed 26 Mar 2026 05:35PM UTC coverage: 44.775% (-0.03%) from 44.802%

Build # 507

Build Type

push

github

Committed by

filipeom

Commit Message

Bump ocamlformat 0.28.1 -> 0.29.0

Coverage Stats

9 of 11 new or added lines in 2 files covered. (81.82%)

309 existing lines in 5 files now uncovered.

964 of 2153 relevant lines covered (44.77%)

9.41 hits per line

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

82.57

/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

(** 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 pp_hex fmt bv = Fmt.pf fmt "(i%d 0x%s)" bv.width (Z.format "%x" bv.value)

let pp_with ~printer fmt e =
  match printer with
  | Ty.Without_type -> pp_bv fmt e
  | With_type -> pp_wtype fmt e
  | With_type_and_hexa_float -> pp_hex fmt e

let pp fmt e = pp_with ~printer:Without_type fmt e

let pp_safe fmt e = pp_with ~printer:With_type_and_hexa_float 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)	465✔
7
8	let make v m =
9	let masked_value = Z.logand v (mask m) in	450✔
10	{ value = masked_value; width = m }	450✔
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	151✔
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	283✔
30
31	let hash a = combine (Z.hash a.value) a.width	283✔
32
33	let equal a b = Z.equal a.value b.value && a.width = b.width	246✔
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	(** Bitvector pretty printer. By default it prints signed bitvectors. *)
60	let pp_bv fmt bv =
61	let value = to_signed bv in	2✔
62	Z.pp_print fmt value	2✔
63
64	let pp_wtype fmt bv =
UNCOV 65	let value = to_signed bv in	×
UNCOV 66	Fmt.pf fmt "(i%d %a)" bv.width Z.pp_print value	×
67
UNCOV 68	let pp_hex fmt bv = Fmt.pf fmt "(i%d 0x%s)" bv.width (Z.format "%x" bv.value)	×
69
70	let pp_with ~printer fmt e =
71	match printer with	2✔
72	\| Ty.Without_type -> pp_bv fmt e	2✔
UNCOV 73	\| With_type -> pp_wtype fmt e	×
UNCOV 74	\| With_type_and_hexa_float -> pp_hex fmt e	×
75
76	let pp fmt e = pp_with ~printer:Without_type fmt e	2✔
77
UNCOV 78	let pp_safe fmt e = pp_with ~printer:With_type_and_hexa_float fmt e	×
79
80	(* Unop *)
81	let neg bv = make (Z.neg bv.value) bv.width	3✔
82
83	let lognot a = make (Z.lognot a.value) a.width	3✔
84
85	let clz bv =
86	let rec count_zeros i =	1✔
UNCOV 87	if i >= bv.width \|\| Z.testbit bv.value (bv.width - 1 - i) then i	×
88	else count_zeros (i + 1)	7✔
89	in
90	make (Z.of_int @@ count_zeros 0) bv.width	1✔
91
92	let ctz bv =
93	let rec count_zeros i =	1✔
UNCOV 94	if i >= bv.width \|\| Z.testbit bv.value i then i else count_zeros (i + 1)	×
95	in
96	make (Z.of_int @@ count_zeros 0) bv.width	1✔
97
98	let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width	1✔
99
100	(* Binop *)
101	let add a b =
102	assert (a.width = b.width);	12✔
103	make (Z.add a.value b.value) a.width	12✔
104
105	let sub a b =
106	assert (a.width = b.width);	5✔
107	make (Z.sub a.value b.value) a.width	5✔
108
109	let mul a b =
110	assert (a.width = b.width);	5✔
111	make (Z.mul a.value b.value) a.width	5✔
112
113	let div a b =
114	assert (a.width = b.width);	3✔
UNCOV 115	if Z.equal b.value Z.zero then raise Division_by_zero;	×
116	make (Z.div (to_signed a) (to_signed b)) a.width	3✔
117
118	let div_u a b =
119	assert (a.width = b.width);	1✔
UNCOV 120	if Z.equal b.value Z.zero then raise Division_by_zero;	×
121	make (Z.div a.value b.value) a.width	1✔
122
123	let logand a b =
124	assert (a.width = b.width);	3✔
125	make (Z.logand a.value b.value) a.width	3✔
126
127	let logor a b =
128	assert (a.width = b.width);	3✔
129	make (Z.logor a.value b.value) a.width	3✔
130
131	let logxor a b =
132	assert (a.width = b.width);	3✔
133	make (Z.logxor a.value b.value) a.width	3✔
134
135	let normalize_shift_amount n width =
136	(* FIXME: only works for widths that are powers of 2. *)
137	assert (width > 0 && width land (width - 1) = 0);	18✔
138	Z.to_int @@ Z.logand n (Z.of_int (width - 1))	18✔
139
140	let shl a n =
141	let n = normalize_shift_amount (view n) (numbits a) in	4✔
142	make (Z.shift_left a.value n) a.width	4✔
143
144	let ashr a n =
145	let n = normalize_shift_amount (view n) (numbits a) in	4✔
146	let signed_value = to_signed a in	4✔
147	make (Z.shift_right signed_value n) a.width	4✔
148
149	let lshr a n =
150	let n = normalize_shift_amount (view n) (numbits a) in	2✔
151	make (Z.shift_right_trunc a.value n) a.width	2✔
152
153	let rem a b =
154	assert (a.width = b.width);	3✔
UNCOV 155	if Z.equal b.value Z.zero then raise Division_by_zero;	×
156	make (Z.rem (to_signed a) (to_signed b)) a.width	3✔
157
158	let rem_u a b =
UNCOV 159	assert (a.width = b.width);	×
160	if Z.equal b.value Z.zero then raise Division_by_zero;	×
161	make (Z.rem a.value b.value) a.width	×
162
163	let rotate_left bv n =
164	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
165	let left_part = Z.shift_left bv.value n in	4✔
166	let right_part = Z.shift_right bv.value (bv.width - n) in	4✔
167	let rotated = Z.logor left_part right_part in	4✔
168	make rotated bv.width	4✔
169
170	let rotate_right bv n =
171	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
172	let right_part = Z.shift_right bv.value n in	4✔
173	let left_part = Z.shift_left bv.value (bv.width - n) in	4✔
174	let rotated = Z.logor left_part right_part in	4✔
175	make rotated bv.width	4✔
176
177	(* Relop *)
178	let lt_u a b = Z.lt a.value b.value	6✔
179
180	let gt_u a b = Z.gt a.value b.value	1✔
181
182	let le_u a b = Z.leq a.value b.value	5✔
183
UNCOV 184	let ge_u a b = Z.geq a.value b.value	×
185
186	let lt a b = Z.lt (to_signed a) (to_signed b)	7✔
187
188	let gt a b = Z.gt (to_signed a) (to_signed b)	1✔
189
190	let le a b = Z.leq (to_signed a) (to_signed b)	7✔
191
192	let ge a b = Z.geq (to_signed a) (to_signed b)	1✔
193
194	(* Extract and concat *)
195	let concat a b =
196	let new_width = a.width + b.width in	7✔
197	let shifted = Z.shift_left a.value b.width in
198	let combined = Z.logor shifted b.value in	7✔
199	make combined new_width	7✔
200
201	let extract bv ~high ~low =
202	assert (high < bv.width && low >= 0 && low <= high);	11✔
203	let width = high - low + 1 in
204	let shifted = Z.shift_right bv.value low in
205	let extracted = Z.logand shifted (mask width) in	11✔
206	make extracted width	11✔
207
208	(* Cvtop *)
209	let zero_extend width bv =
210	let new_width = bv.width + width in	5✔
211	make bv.value new_width
212
213	let sign_extend width bv =
214	let new_width = bv.width + width in	6✔
215	let msb = msb bv in
216	let sign_mask =	6✔
217	if msb then
218	let shift_amount = bv.width in	4✔
219	Z.shift_left (mask width) shift_amount	4✔
220	else Z.zero	2✔
221	in
222	let extended = Z.logor bv.value sign_mask in
223	make extended new_width	6✔
224
225	let to_string bv = Fmt.str "%a" pp bv	2✔
226
227	let to_json bv = `String (to_string bv)	2✔

formalsec / smtml / 507

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