formalsec / smtml / 175

Committed 12 Jul 2024 09:10AM UTC coverage: 50.585% (+1.4%) from 49.176%

Build # 175

Build Type

push

github

Committed by

filipeom

Commit Message

Test relop simplification

Run Details

1125 of 2224 relevant lines covered (50.58%)

22.03 hits per line

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

6.02

/lib/ty.ml

(***************************************************************************)
(* This file is part of the third-party OCaml library `smtml`.             *)
(* Copyright (C) 2023-2024 formalsec                                       *)
(*                                                                         *)
(* This program is free software: you can redistribute it and/or modify    *)
(* it under the terms of the GNU General Public License as published by    *)
(* the Free Software Foundation, either version 3 of the License, or       *)
(* (at your option) any later version.                                     *)
(*                                                                         *)
(* This program is distributed in the hope that it will be useful,         *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           *)
(* GNU General Public License for more details.                            *)
(*                                                                         *)
(* You should have received a copy of the GNU General Public License       *)
(* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
(***************************************************************************)

let pp_string = Format.pp_print_string

let fprintf = Format.fprintf

type _ cast =
  | C8 : int cast
  | C32 : int32 cast
  | C64 : int64 cast

type t =
  | Ty_int
  | Ty_real
  | Ty_bool
  | Ty_str
  | Ty_bitv of int
  | Ty_fp of int
  | Ty_list
  | Ty_app
  | Ty_unit

type unop =
  | Neg
  | Not
  | Clz
  | Ctz
  (* Float *)
  | Abs
  | Sqrt
  | Is_nan
  | Ceil
  | Floor
  | Trunc
  | Nearest
  | Head
  | Tail
  | Reverse
  | Length
  (* String *)
  | Trim

type binop =
  | Add
  | Sub
  | Mul
  | Div
  | DivU
  | Rem
  | RemU
  | Shl
  | ShrA
  | ShrL
  | And
  | Or
  | Xor
  | Pow
  | Min
  | Max
  | Rotl
  | Rotr
  | At
  | List_append_last
  | List_append
  (* String *)
  | String_prefix
  | String_suffix
  | String_contains
  | String_last_index

type relop =
  | Eq
  | Ne
  | Lt
  | LtU
  | Gt
  | GtU
  | Le
  | LeU
  | Ge
  | GeU

type triop =
  | Ite
  | List_set
  (* String *)
  | String_extract
  | String_replace
  | String_index

type cvtop =
  | ToString
  | OfString
  | ToBool
  | OfBool
  | Reinterpret_int
  | Reinterpret_float
  | DemoteF64
  | PromoteF32
  | ConvertSI32
  | ConvertUI32
  | ConvertSI64
  | ConvertUI64
  | TruncSF32
  | TruncUF32
  | TruncSF64
  | TruncUF64
  | WrapI64
  | Sign_extend of int
  | Zero_extend of int
  (* String *)
  | String_to_code
  | String_from_code
  | String_to_int
  | String_from_int
  | String_to_float

type naryop =
  | Logand
  | Logor
  | Concat

type logic =
  | AUFLIA
  | AUFLIRA
  | AUFNIRA
  | LIA
  | LRA
  | QF_ABV
  | QF_AUFBV
  | QF_AUFLIA
  | QF_AX
  | QF_BV
  | QF_BVFP
  | QF_IDL
  | QF_LIA
  | QF_LRA
  | QF_NIA
  | QF_NRA
  | QF_RDL
  | QF_S
  | QF_UF
  | QF_UFBV
  | QF_UFIDL
  | QF_UFLIA
  | QF_UFLRA
  | QF_UFNRA
  | UFLRA
  | UFNIA

let pp_unop fmt (op : unop) =
  match op with
  | Neg -> pp_string fmt "neg"
  | Not -> pp_string fmt "not"
  | Clz -> pp_string fmt "clz"
  | Ctz -> pp_string fmt "ctz"
  | Abs -> pp_string fmt "abs"
  | Sqrt -> pp_string fmt "sqrt"
  | Is_nan -> pp_string fmt "is_nan"
  | Ceil -> pp_string fmt "ceil"
  | Floor -> pp_string fmt "floor"
  | Trunc -> pp_string fmt "trunc"
  | Nearest -> pp_string fmt "nearest"
  | Head -> pp_string fmt "head"
  | Tail -> pp_string fmt "tail"
  | Reverse -> pp_string fmt "reverse"
  | Length -> pp_string fmt "length"
  | Trim -> pp_string fmt "trim"

let pp_binop fmt (op : binop) =
  match op with
  | Add -> pp_string fmt "add"
  | Sub -> pp_string fmt "sub"
  | Mul -> pp_string fmt "mul"
  | Div -> pp_string fmt "div"
  | DivU -> pp_string fmt "div_u"
  | Rem -> pp_string fmt "rem"
  | RemU -> pp_string fmt "rem_u"
  | Shl -> pp_string fmt "shl"
  | ShrA -> pp_string fmt "shr"
  | ShrL -> pp_string fmt "shr_u"
  | And -> pp_string fmt "and"
  | Or -> pp_string fmt "or"
  | Xor -> pp_string fmt "xor"
  | Pow -> pp_string fmt "pow"
  | Min -> pp_string fmt "min"
  | Max -> pp_string fmt "max"
  | Rotl -> pp_string fmt "rotl"
  | Rotr -> pp_string fmt "rotr"
  | At -> pp_string fmt "at"
  | List_append_last -> pp_string fmt "append_last"
  | List_append -> pp_string fmt "append"
  | String_prefix -> pp_string fmt "prefixof"
  | String_suffix -> pp_string fmt "suffixof"
  | String_contains -> pp_string fmt "contains"
  | String_last_index -> pp_string fmt "last_indexof"

let pp_triop fmt (op : triop) =
  match op with
  | Ite -> pp_string fmt "ite"
  | String_extract -> pp_string fmt "substr"
  | String_replace -> pp_string fmt "replace"
  | String_index -> pp_string fmt "indexof"
  | List_set -> pp_string fmt "set"

let pp_relop fmt (op : relop) =
  match op with
  | Eq -> pp_string fmt "eq"
  | Ne -> pp_string fmt "ne"
  | Lt -> pp_string fmt "lt"
  | LtU -> pp_string fmt "lt_u"
  | Gt -> pp_string fmt "gt"
  | GtU -> pp_string fmt "gt_u"
  | Le -> pp_string fmt "le"
  | LeU -> pp_string fmt "le_u"
  | Ge -> pp_string fmt "ge"
  | GeU -> pp_string fmt "ge_u"

let pp_cvtop fmt (op : cvtop) =
  match op with
  | ToString -> pp_string fmt "to_string"
  | OfString -> pp_string fmt "of_string"
  | ToBool -> pp_string fmt "to_bool"
  | OfBool -> pp_string fmt "of_bool"
  | Reinterpret_int -> pp_string fmt "reinterpret_int"
  | Reinterpret_float -> pp_string fmt "reinterpret_float"
  | DemoteF64 -> pp_string fmt "demote_f64"
  | PromoteF32 -> pp_string fmt "promote_f32"
  | ConvertSI32 -> pp_string fmt "convert_i32_s"
  | ConvertUI32 -> pp_string fmt "convert_i32_u"
  | ConvertSI64 -> pp_string fmt "convert_i64_s"
  | ConvertUI64 -> pp_string fmt "convert_i64_u"
  | TruncSF32 -> pp_string fmt "trunc_f32_s"
  | TruncUF32 -> pp_string fmt "trunc_f32_u"
  | TruncSF64 -> pp_string fmt "trunc_f64_s"
  | TruncUF64 -> pp_string fmt "trunc_f64_u"
  | WrapI64 -> pp_string fmt "wrap_i64"
  | Sign_extend sz -> fprintf fmt "extend_i%d_s" sz
  | Zero_extend sz -> fprintf fmt "extend_i%d_u" sz
  | String_to_code -> pp_string fmt "to_code"
  | String_from_code -> pp_string fmt "from_code"
  | String_to_int -> pp_string fmt "to_int"
  | String_from_int -> pp_string fmt "from_int"
  | String_to_float -> pp_string fmt "to_float"

let pp_naryop fmt (op : naryop) =
  match op with
  | Logand -> pp_string fmt "and"
  | Logor -> pp_string fmt "or"
  | Concat -> pp_string fmt "++"

let pp fmt = function
  | Ty_int -> pp_string fmt "int"
  | Ty_real -> pp_string fmt "real"
  | Ty_bool -> pp_string fmt "bool"
  | Ty_str -> pp_string fmt "str"
  | Ty_bitv n -> fprintf fmt "i%d" n
  | Ty_fp n -> fprintf fmt "f%d" n
  | Ty_list -> pp_string fmt "list"
  | Ty_app -> pp_string fmt "app"
  | Ty_unit -> pp_string fmt "unit"

let pp_logic fmt : logic -> unit = function
  | AUFLIA -> pp_string fmt "AUFLIA"
  | AUFLIRA -> pp_string fmt "AUFLIRA"
  | AUFNIRA -> pp_string fmt "AUFNIRA"
  | LIA -> pp_string fmt "LIA"
  | LRA -> pp_string fmt "LRA"
  | QF_ABV -> pp_string fmt "QF_ABV"
  | QF_AUFBV -> pp_string fmt "QF_AUFBV"
  | QF_AUFLIA -> pp_string fmt "QF_AUFLIA"
  | QF_AX -> pp_string fmt "QF_AX"
  | QF_BV -> pp_string fmt "QF_BV"
  | QF_BVFP -> pp_string fmt "QF_BVFP"
  | QF_IDL -> pp_string fmt "QF_IDL"
  | QF_LIA -> pp_string fmt "QF_LIA"
  | QF_LRA -> pp_string fmt "QF_LRA"
  | QF_NIA -> pp_string fmt "QF_NIA"
  | QF_NRA -> pp_string fmt "QF_NRA"
  | QF_RDL -> pp_string fmt "QF_RDL"
  | QF_S -> pp_string fmt "QF_S"
  | QF_UF -> pp_string fmt "QF_UF"
  | QF_UFBV -> pp_string fmt "QF_UFBV"
  | QF_UFIDL -> pp_string fmt "QF_UFIDL"
  | QF_UFLIA -> pp_string fmt "QF_UFLIA"
  | QF_UFLRA -> pp_string fmt "QF_UFLRA"
  | QF_UFNRA -> pp_string fmt "QF_UFNRA"
  | UFLRA -> pp_string fmt "UFLRA"
  | UFNIA -> pp_string fmt "UFNIA"

let equal t1 t2 =
  match (t1, t2) with
  | Ty_int, Ty_int | Ty_real, Ty_real | Ty_bool, Ty_bool | Ty_str, Ty_str ->
    true
  | Ty_bitv n1, Ty_bitv n2 | Ty_fp n1, Ty_fp n2 -> n1 = n2
  | _ -> false

let string_of_type (ty : t) : string = Format.asprintf "%a" pp ty

let size (ty : t) : int =
  match ty with
  | Ty_bitv n | Ty_fp n -> n / 8
  | Ty_int | Ty_bool -> 4
  | Ty_real | Ty_str | Ty_list | Ty_app | Ty_unit -> assert false

1	(***************************************************************************)
2	(* This file is part of the third-party OCaml library `smtml`. *)
3	(* Copyright (C) 2023-2024 formalsec *)
4	(* *)
5	(* This program is free software: you can redistribute it and/or modify *)
6	(* it under the terms of the GNU General Public License as published by *)
7	(* the Free Software Foundation, either version 3 of the License, or *)
8	(* (at your option) any later version. *)
9	(* *)
10	(* This program is distributed in the hope that it will be useful, *)
11	(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
12	(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
13	(* GNU General Public License for more details. *)
14	(* *)
15	(* You should have received a copy of the GNU General Public License *)
16	(* along with this program. If not, see <https://www.gnu.org/licenses/>. *)
17	(***************************************************************************)
18
19	let pp_string = Format.pp_print_string
20
21	let fprintf = Format.fprintf
22
23	type _ cast =
24	\| C8 : int cast
25	\| C32 : int32 cast
26	\| C64 : int64 cast
27
28	type t =
29	\| Ty_int
30	\| Ty_real
31	\| Ty_bool
32	\| Ty_str
33	\| Ty_bitv of int
34	\| Ty_fp of int
35	\| Ty_list
36	\| Ty_app
37	\| Ty_unit
38
39	type unop =
40	\| Neg
41	\| Not
42	\| Clz
43	\| Ctz
44	(* Float *)
45	\| Abs
46	\| Sqrt
47	\| Is_nan
48	\| Ceil
49	\| Floor
50	\| Trunc
51	\| Nearest
52	\| Head
53	\| Tail
54	\| Reverse
55	\| Length
56	(* String *)
57	\| Trim
58
59	type binop =
60	\| Add
61	\| Sub
62	\| Mul
63	\| Div
64	\| DivU
65	\| Rem
66	\| RemU
67	\| Shl
68	\| ShrA
69	\| ShrL
70	\| And
71	\| Or
72	\| Xor
73	\| Pow
74	\| Min
75	\| Max
76	\| Rotl
77	\| Rotr
78	\| At
79	\| List_append_last
80	\| List_append
81	(* String *)
82	\| String_prefix
83	\| String_suffix
84	\| String_contains
85	\| String_last_index
86
87	type relop =
88	\| Eq
89	\| Ne
90	\| Lt
91	\| LtU
92	\| Gt
93	\| GtU
94	\| Le
95	\| LeU
96	\| Ge
97	\| GeU
98
99	type triop =
100	\| Ite
101	\| List_set
102	(* String *)
103	\| String_extract
104	\| String_replace
105	\| String_index
106
107	type cvtop =
108	\| ToString
109	\| OfString
110	\| ToBool
111	\| OfBool
112	\| Reinterpret_int
113	\| Reinterpret_float
114	\| DemoteF64
115	\| PromoteF32
116	\| ConvertSI32
117	\| ConvertUI32
118	\| ConvertSI64
119	\| ConvertUI64
120	\| TruncSF32
121	\| TruncUF32
122	\| TruncSF64
123	\| TruncUF64
124	\| WrapI64
125	\| Sign_extend of int
126	\| Zero_extend of int
127	(* String *)
128	\| String_to_code
129	\| String_from_code
130	\| String_to_int
131	\| String_from_int
132	\| String_to_float
133
134	type naryop =
135	\| Logand
136	\| Logor
137	\| Concat
138
139	type logic =
140	\| AUFLIA
141	\| AUFLIRA
142	\| AUFNIRA
143	\| LIA
144	\| LRA
145	\| QF_ABV
146	\| QF_AUFBV
147	\| QF_AUFLIA
148	\| QF_AX
149	\| QF_BV
150	\| QF_BVFP
151	\| QF_IDL
152	\| QF_LIA
153	\| QF_LRA
154	\| QF_NIA
155	\| QF_NRA
156	\| QF_RDL
157	\| QF_S
158	\| QF_UF
159	\| QF_UFBV
160	\| QF_UFIDL
161	\| QF_UFLIA
162	\| QF_UFLRA
163	\| QF_UFNRA
164	\| UFLRA
165	\| UFNIA
166
167	let pp_unop fmt (op : unop) =
168	match op with	×
169	\| Neg -> pp_string fmt "neg"	×
170	\| Not -> pp_string fmt "not"	×
171	\| Clz -> pp_string fmt "clz"	×
172	\| Ctz -> pp_string fmt "ctz"	×
173	\| Abs -> pp_string fmt "abs"	×
174	\| Sqrt -> pp_string fmt "sqrt"	×
175	\| Is_nan -> pp_string fmt "is_nan"	×
176	\| Ceil -> pp_string fmt "ceil"	×
177	\| Floor -> pp_string fmt "floor"	×
178	\| Trunc -> pp_string fmt "trunc"	×
179	\| Nearest -> pp_string fmt "nearest"	×
180	\| Head -> pp_string fmt "head"	×
181	\| Tail -> pp_string fmt "tail"	×
182	\| Reverse -> pp_string fmt "reverse"	×
183	\| Length -> pp_string fmt "length"	×
184	\| Trim -> pp_string fmt "trim"	×
185
186	let pp_binop fmt (op : binop) =
187	match op with	×
188	\| Add -> pp_string fmt "add"	×
189	\| Sub -> pp_string fmt "sub"	×
190	\| Mul -> pp_string fmt "mul"	×
191	\| Div -> pp_string fmt "div"	×
192	\| DivU -> pp_string fmt "div_u"	×
193	\| Rem -> pp_string fmt "rem"	×
194	\| RemU -> pp_string fmt "rem_u"	×
195	\| Shl -> pp_string fmt "shl"	×
196	\| ShrA -> pp_string fmt "shr"	×
197	\| ShrL -> pp_string fmt "shr_u"	×
198	\| And -> pp_string fmt "and"	×
199	\| Or -> pp_string fmt "or"	×
200	\| Xor -> pp_string fmt "xor"	×
201	\| Pow -> pp_string fmt "pow"	×
202	\| Min -> pp_string fmt "min"	×
203	\| Max -> pp_string fmt "max"	×
204	\| Rotl -> pp_string fmt "rotl"	×
205	\| Rotr -> pp_string fmt "rotr"	×
206	\| At -> pp_string fmt "at"	×
207	\| List_append_last -> pp_string fmt "append_last"	×
208	\| List_append -> pp_string fmt "append"	×
209	\| String_prefix -> pp_string fmt "prefixof"	×
210	\| String_suffix -> pp_string fmt "suffixof"	×
211	\| String_contains -> pp_string fmt "contains"	×
212	\| String_last_index -> pp_string fmt "last_indexof"	×
213
214	let pp_triop fmt (op : triop) =
215	match op with	×
216	\| Ite -> pp_string fmt "ite"	×
217	\| String_extract -> pp_string fmt "substr"	×
218	\| String_replace -> pp_string fmt "replace"	×
219	\| String_index -> pp_string fmt "indexof"	×
220	\| List_set -> pp_string fmt "set"	×
221
222	let pp_relop fmt (op : relop) =
223	match op with	×
224	\| Eq -> pp_string fmt "eq"	×
225	\| Ne -> pp_string fmt "ne"	×
226	\| Lt -> pp_string fmt "lt"	×
227	\| LtU -> pp_string fmt "lt_u"	×
228	\| Gt -> pp_string fmt "gt"	×
229	\| GtU -> pp_string fmt "gt_u"	×
230	\| Le -> pp_string fmt "le"	×
231	\| LeU -> pp_string fmt "le_u"	×
232	\| Ge -> pp_string fmt "ge"	×
233	\| GeU -> pp_string fmt "ge_u"	×
234
235	let pp_cvtop fmt (op : cvtop) =
236	match op with	×
237	\| ToString -> pp_string fmt "to_string"	×
238	\| OfString -> pp_string fmt "of_string"	×
239	\| ToBool -> pp_string fmt "to_bool"	×
240	\| OfBool -> pp_string fmt "of_bool"	×
241	\| Reinterpret_int -> pp_string fmt "reinterpret_int"	×
242	\| Reinterpret_float -> pp_string fmt "reinterpret_float"	×
243	\| DemoteF64 -> pp_string fmt "demote_f64"	×
244	\| PromoteF32 -> pp_string fmt "promote_f32"	×
245	\| ConvertSI32 -> pp_string fmt "convert_i32_s"	×
246	\| ConvertUI32 -> pp_string fmt "convert_i32_u"	×
247	\| ConvertSI64 -> pp_string fmt "convert_i64_s"	×
248	\| ConvertUI64 -> pp_string fmt "convert_i64_u"	×
249	\| TruncSF32 -> pp_string fmt "trunc_f32_s"	×
250	\| TruncUF32 -> pp_string fmt "trunc_f32_u"	×
251	\| TruncSF64 -> pp_string fmt "trunc_f64_s"	×
252	\| TruncUF64 -> pp_string fmt "trunc_f64_u"	×
253	\| WrapI64 -> pp_string fmt "wrap_i64"	×
254	\| Sign_extend sz -> fprintf fmt "extend_i%d_s" sz	×
255	\| Zero_extend sz -> fprintf fmt "extend_i%d_u" sz	×
256	\| String_to_code -> pp_string fmt "to_code"	×
257	\| String_from_code -> pp_string fmt "from_code"	×
258	\| String_to_int -> pp_string fmt "to_int"	×
259	\| String_from_int -> pp_string fmt "from_int"	×
260	\| String_to_float -> pp_string fmt "to_float"	×
261
262	let pp_naryop fmt (op : naryop) =
263	match op with	×
264	\| Logand -> pp_string fmt "and"	×
265	\| Logor -> pp_string fmt "or"	×
266	\| Concat -> pp_string fmt "++"	×
267
268	let pp fmt = function
269	\| Ty_int -> pp_string fmt "int"	×
270	\| Ty_real -> pp_string fmt "real"	×
271	\| Ty_bool -> pp_string fmt "bool"	×
272	\| Ty_str -> pp_string fmt "str"	×
273	\| Ty_bitv n -> fprintf fmt "i%d" n	×
274	\| Ty_fp n -> fprintf fmt "f%d" n	×
275	\| Ty_list -> pp_string fmt "list"	×
276	\| Ty_app -> pp_string fmt "app"	×
277	\| Ty_unit -> pp_string fmt "unit"	×
278
279	let pp_logic fmt : logic -> unit = function	8✔
280	\| AUFLIA -> pp_string fmt "AUFLIA"	×
281	\| AUFLIRA -> pp_string fmt "AUFLIRA"	×
282	\| AUFNIRA -> pp_string fmt "AUFNIRA"	×
283	\| LIA -> pp_string fmt "LIA"	2✔
284	\| LRA -> pp_string fmt "LRA"	×
285	\| QF_ABV -> pp_string fmt "QF_ABV"	×
286	\| QF_AUFBV -> pp_string fmt "QF_AUFBV"	×
287	\| QF_AUFLIA -> pp_string fmt "QF_AUFLIA"	×
288	\| QF_AX -> pp_string fmt "QF_AX"	×
289	\| QF_BV -> pp_string fmt "QF_BV"	×
290	\| QF_BVFP -> pp_string fmt "QF_BVFP"	5✔
291	\| QF_IDL -> pp_string fmt "QF_IDL"	×
292	\| QF_LIA -> pp_string fmt "QF_LIA"	1✔
293	\| QF_LRA -> pp_string fmt "QF_LRA"	×
294	\| QF_NIA -> pp_string fmt "QF_NIA"	×
295	\| QF_NRA -> pp_string fmt "QF_NRA"	×
296	\| QF_RDL -> pp_string fmt "QF_RDL"	×
297	\| QF_S -> pp_string fmt "QF_S"	×
298	\| QF_UF -> pp_string fmt "QF_UF"	×
299	\| QF_UFBV -> pp_string fmt "QF_UFBV"	×
300	\| QF_UFIDL -> pp_string fmt "QF_UFIDL"	×
301	\| QF_UFLIA -> pp_string fmt "QF_UFLIA"	×
302	\| QF_UFLRA -> pp_string fmt "QF_UFLRA"	×
303	\| QF_UFNRA -> pp_string fmt "QF_UFNRA"	×
304	\| UFLRA -> pp_string fmt "UFLRA"	×
305	\| UFNIA -> pp_string fmt "UFNIA"	×
306
307	let equal t1 t2 =
308	match (t1, t2) with	163✔
309	\| Ty_int, Ty_int \| Ty_real, Ty_real \| Ty_bool, Ty_bool \| Ty_str, Ty_str ->	4✔
310	true
311	\| Ty_bitv n1, Ty_bitv n2 \| Ty_fp n1, Ty_fp n2 -> n1 = n2	20✔
312	\| _ -> false	×
313
314	let string_of_type (ty : t) : string = Format.asprintf "%a" pp ty	×
315
316	let size (ty : t) : int =
317	match ty with	1✔
318	\| Ty_bitv n \| Ty_fp n -> n / 8	×
319	\| Ty_int \| Ty_bool -> 4	×
320	\| Ty_real \| Ty_str \| Ty_list \| Ty_app \| Ty_unit -> assert false

formalsec / smtml / 175

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