formalsec / smtml / 349

Committed 11 Jun 2025 07:46PM UTC coverage: 55.168%. First build

Build # 349

Build Type

push

github

Committed by

filipeom

Commit Message

add support for Bv of size 16

Run Details

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

950 of 1722 relevant lines covered (55.17%)

11.51 hits per line

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

87.76

/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

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

(* 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)	454✔
7
8	let make v m =
9	let masked_value = Z.logand v (mask m) in	440✔
10	{ value = masked_value; width = m }	440✔
11
12	let view { value; _ } = value	19✔
13
14	let numbits { width; _ } = width	195✔
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 ? *)
NEW 22	make (Z.of_int v) 16	×
23
24	let of_int32 v = make (Z.of_int32 v) 32	147✔
25
26	let of_int64 v = make (Z.of_int64 v) 64	104✔
27
28	let equal a b = Z.equal a.value b.value && a.width = b.width	221✔
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)	76✔
37
38	let to_signed bv =
39	let msb = msb bv in	70✔
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)	11✔
50	else
51	Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"	×
52	v.width
53
54	(** Bitvector pretty printer. By default it prints signed bitvectors. *)
55	let pp fmt bv =
56	let value = to_signed bv in	2✔
57	Z.pp_print fmt value	2✔
58
59	(* Unop *)
60	let neg bv = make (Z.neg bv.value) bv.width	3✔
61
62	let lognot a = make (Z.lognot a.value) a.width	2✔
63
64	let clz bv =
65	let rec count_zeros i =	1✔
66	if i >= bv.width \|\| Z.testbit bv.value (bv.width - 1 - i) then i	×
67	else count_zeros (i + 1)	7✔
68	in
69	make (Z.of_int @@ count_zeros 0) bv.width	1✔
70
71	let ctz bv =
72	let rec count_zeros i =	1✔
73	if i >= bv.width \|\| Z.testbit bv.value i then i else count_zeros (i + 1)	×
74	in
75	make (Z.of_int @@ count_zeros 0) bv.width	1✔
76
77	let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width	1✔
78
79	(* Binop *)
80	let add a b =
81	assert (a.width = b.width);	11✔
82	make (Z.add a.value b.value) a.width	11✔
83
84	let sub a b =
85	assert (a.width = b.width);	5✔
86	make (Z.sub a.value b.value) a.width	5✔
87
88	let mul a b =
89	assert (a.width = b.width);	5✔
90	make (Z.mul a.value b.value) a.width	5✔
91
92	let div a b =
93	assert (a.width = b.width);	3✔
94	if Z.equal b.value Z.zero then raise Division_by_zero;	×
95	make (Z.div (to_signed a) (to_signed b)) a.width	3✔
96
97	let div_u a b =
98	assert (a.width = b.width);	1✔
99	if Z.equal b.value Z.zero then raise Division_by_zero;	×
100	make (Z.div a.value b.value) a.width	1✔
101
102	let logand a b =
103	assert (a.width = b.width);	3✔
104	make (Z.logand a.value b.value) a.width	3✔
105
106	let logor a b =
107	assert (a.width = b.width);	3✔
108	make (Z.logor a.value b.value) a.width	3✔
109
110	let logxor a b =
111	assert (a.width = b.width);	3✔
112	make (Z.logxor a.value b.value) a.width	3✔
113
114	let normalize_shift_amount n width =
115	(* FIXME: only works for widths that are powers of 2. *)
116	assert (width > 0 && width land (width - 1) = 0);	18✔
117	Z.to_int @@ Z.logand n (Z.of_int (width - 1))	18✔
118
119	let shl a n =
120	let n = normalize_shift_amount (view n) (numbits a) in	4✔
121	make (Z.shift_left a.value n) a.width	4✔
122
123	let ashr a n =
124	let n = normalize_shift_amount (view n) (numbits a) in	4✔
125	let signed_value = to_signed a in	4✔
126	make (Z.shift_right signed_value n) a.width	4✔
127
128	let lshr a n =
129	let n = normalize_shift_amount (view n) (numbits a) in	2✔
130	make (Z.shift_right_trunc a.value n) a.width	2✔
131
132	let rem a b =
133	assert (a.width = b.width);	3✔
134	if Z.equal b.value Z.zero then raise Division_by_zero;	×
135	make (Z.rem (to_signed a) (to_signed b)) a.width	3✔
136
137	let rem_u a b =
138	assert (a.width = b.width);	×
139	if Z.equal b.value Z.zero then raise Division_by_zero;	×
140	make (Z.rem a.value b.value) a.width	×
141
142	let rotate_left bv n =
143	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
144	let left_part = Z.shift_left bv.value n in	4✔
145	let right_part = Z.shift_right bv.value (bv.width - n) in	4✔
146	let rotated = Z.logor left_part right_part in	4✔
147	make rotated bv.width	4✔
148
149	let rotate_right bv n =
150	let n = normalize_shift_amount (view n) (numbits bv) in	4✔
151	let right_part = Z.shift_right bv.value n in	4✔
152	let left_part = Z.shift_left bv.value (bv.width - n) in	4✔
153	let rotated = Z.logor left_part right_part in	4✔
154	make rotated bv.width	4✔
155
156	(* Relop *)
157	let lt_u a b = Z.lt a.value b.value	5✔
158
159	let gt_u a b = Z.gt a.value b.value	3✔
160
161	let le_u a b = Z.leq a.value b.value	4✔
162
163	let ge_u a b = Z.geq a.value b.value	2✔
164
165	let lt a b = Z.lt (to_signed a) (to_signed b)	4✔
166
167	let gt a b = Z.gt (to_signed a) (to_signed b)	4✔
168
169	let le a b = Z.leq (to_signed a) (to_signed b)	4✔
170
171	let ge a b = Z.geq (to_signed a) (to_signed b)	4✔
172
173	(* Extract and concat *)
174	let concat a b =
175	let new_width = a.width + b.width in	7✔
176	let shifted = Z.shift_left a.value b.width in
177	let combined = Z.logor shifted b.value in	7✔
178	make combined new_width	7✔
179
180	let extract bv ~high ~low =
181	assert (high < bv.width && low >= 0 && low <= high);	10✔
182	let width = high - low + 1 in
183	let shifted = Z.shift_right bv.value low in
184	let extracted = Z.logand shifted (mask width) in	10✔
185	make extracted width	10✔
186
187	(* Cvtop *)
188	let zero_extend width bv =
189	let new_width = bv.width + width in	3✔
190	make bv.value new_width
191
192	let sign_extend width bv =
193	let new_width = bv.width + width in	6✔
194	let msb = msb bv in
195	let sign_mask =	6✔
196	if msb then
197	let shift_amount = bv.width in	4✔
198	Z.shift_left (mask width) shift_amount	4✔
199	else Z.zero	2✔
200	in
201	let extended = Z.logor bv.value sign_mask in
202	make extended new_width	6✔
203
204	let to_string bv = Fmt.str "%a" pp bv	2✔
205
206	let to_json bv = `String (to_string bv)	2✔

formalsec / smtml / 349

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