formalsec / smtml / 405

Committed 24 Oct 2025 04:27PM UTC coverage: 53.755% (-0.3%) from 54.096%

Build # 405

Build Type

push

github

Committed by

filipeom

Commit Message

Use the the hex format to print and parse floats

Run Details

0 of 13 new or added lines in 2 files covered. (0.0%)

111 existing lines in 3 files now uncovered.

952 of 1771 relevant lines covered (53.75%)

11.32 hits per line

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

84.47

/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

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

formalsec / smtml / 405

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