formalsec / smtml / 321

Committed 03 May 2025 06:14PM UTC coverage: 42.428% (-7.8%) from 50.195%

Build # 321

Build Type

push

github

Committed by

filipeom

Commit Message

Don't install z3 in deploy CI

Run Details

720 of 1697 relevant lines covered (42.43%)

7.49 hits per line

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

35.06

/src/smtml/ty.ml

(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

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

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

let discr = function
  | Ty_app -> 0
  | Ty_bool -> 1
  | Ty_int -> 2
  | Ty_list -> 3
  | Ty_none -> 4
  | Ty_real -> 5
  | Ty_str -> 6
  | Ty_unit -> 7
  | Ty_regexp -> 8
  | Ty_bitv n -> 9 + n
  | Ty_fp n -> 10 + n

let compare t1 t2 = compare (discr t1) (discr t2)

let equal t1 t2 = compare t1 t2 = 0

let pp fmt = function
  | Ty_int -> Fmt.string fmt "int"
  | Ty_real -> Fmt.string fmt "real"
  | Ty_bool -> Fmt.string fmt "bool"
  | Ty_str -> Fmt.string fmt "str"
  | Ty_bitv n -> Fmt.pf fmt "i%d" n
  | Ty_fp n -> Fmt.pf fmt "f%d" n
  | Ty_list -> Fmt.string fmt "list"
  | Ty_app -> Fmt.string fmt "app"
  | Ty_unit -> Fmt.string fmt "unit"
  | Ty_none -> Fmt.string fmt "none"
  | Ty_regexp -> Fmt.string fmt "regexp"

let string_of_type (ty : t) : string = Fmt.str "%a" pp ty

let of_string = function
  | "int" -> Ok Ty_int
  | "real" -> Ok Ty_real
  | "bool" -> Ok Ty_bool
  | "str" -> Ok Ty_str
  | "list" -> Ok Ty_list
  | "app" -> Ok Ty_app
  | "unit" -> Ok Ty_unit
  | "none" -> Ok Ty_none
  | "regexp" -> Ok Ty_regexp
  | s ->
    if String.starts_with ~prefix:"i" s then begin
      let s = String.sub s 1 (String.length s - 1) in
      match int_of_string_opt s with
      | None -> Fmt.error_msg "can not parse type %s" s
      | Some n when n < 0 ->
        Fmt.error_msg "size of bitvectors must be a positive integer"
      | Some n -> Ok (Ty_bitv n)
    end
    else if String.starts_with ~prefix:"f" s then begin
      let s = String.sub s 1 (String.length s - 1) in
      match int_of_string_opt s with
      | None -> Fmt.error_msg "can not parse type %s" s
      | Some n when n < 0 ->
        Fmt.error_msg "size of fp must be a positive integer"
      | Some n -> Ok (Ty_fp n)
    end
    else Fmt.error_msg "can not parse type %s" s

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 | Ty_none | Ty_regexp ->
    assert false

module Unop = struct
  type t =
    | Neg
    | Not
    | Clz
    | Ctz
    | Popcnt
    (* Float *)
    | Abs
    | Sqrt
    | Is_nan
    | Ceil
    | Floor
    | Trunc
    | Nearest
    | Head
    | Tail
    | Reverse
    | Length
    (* String *)
    | Trim
    (* RegExp *)
    | Regexp_star
    | Regexp_loop of (int * int)
    | Regexp_plus
    | Regexp_opt
    | Regexp_comp

  let equal o1 o2 =
    match (o1, o2) with
    | Neg, Neg
    | Not, Not
    | Clz, Clz
    | Popcnt, Popcnt
    | Ctz, Ctz
    | Abs, Abs
    | Sqrt, Sqrt
    | Is_nan, Is_nan
    | Ceil, Ceil
    | Floor, Floor
    | Trunc, Trunc
    | Nearest, Nearest
    | Head, Head
    | Tail, Tail
    | Reverse, Reverse
    | Length, Length
    | Trim, Trim
    | Regexp_star, Regexp_star
    | Regexp_loop _, Regexp_loop _
    | Regexp_plus, Regexp_plus
    | Regexp_opt, Regexp_opt
    | Regexp_comp, Regexp_comp ->
      true
    | ( ( Neg | Not | Clz | Popcnt | Ctz | Abs | Sqrt | Is_nan | Ceil | Floor
        | Trunc | Nearest | Head | Tail | Reverse | Length | Trim | Regexp_star
        | Regexp_loop _ | Regexp_plus | Regexp_opt | Regexp_comp )
      , _ ) ->
      false

  let pp fmt = function
    | Neg -> Fmt.string fmt "neg"
    | Not -> Fmt.string fmt "not"
    | Clz -> Fmt.string fmt "clz"
    | Ctz -> Fmt.string fmt "ctz"
    | Popcnt -> Fmt.string fmt "popcnt"
    | Abs -> Fmt.string fmt "abs"
    | Sqrt -> Fmt.string fmt "sqrt"
    | Is_nan -> Fmt.string fmt "is_nan"
    | Ceil -> Fmt.string fmt "ceil"
    | Floor -> Fmt.string fmt "floor"
    | Trunc -> Fmt.string fmt "trunc"
    | Nearest -> Fmt.string fmt "nearest"
    | Head -> Fmt.string fmt "head"
    | Tail -> Fmt.string fmt "tail"
    | Reverse -> Fmt.string fmt "reverse"
    | Length -> Fmt.string fmt "length"
    | Trim -> Fmt.string fmt "trim"
    | Regexp_star -> Fmt.string fmt "*"
    | Regexp_loop _ -> Fmt.string fmt "loop"
    | Regexp_plus -> Fmt.string fmt "+"
    | Regexp_opt -> Fmt.string fmt "opt"
    | Regexp_comp -> Fmt.string fmt "comp"
end

module Binop = struct
  type t =
    | Add
    | Sub
    | Mul
    | Div
    | DivU
    | Rem
    | RemU
    | Shl
    | ShrA
    | ShrL
    | And
    | Or
    | Xor
    | Pow
    | Min
    | Max
    | Copysign
    | Rotl
    | Rotr
    | At
    | List_cons
    | List_append
    (* String *)
    | String_prefix
    | String_suffix
    | String_contains
    | String_last_index
    | String_in_re
    (* Regexp *)
    | Regexp_range

  let equal o1 o2 =
    match (o1, o2) with
    | Add, Add
    | Sub, Sub
    | Mul, Mul
    | Div, Div
    | DivU, DivU
    | Rem, Rem
    | RemU, RemU
    | Shl, Shl
    | ShrA, ShrA
    | ShrL, ShrL
    | And, And
    | Or, Or
    | Xor, Xor
    | Pow, Pow
    | Min, Min
    | Max, Max
    | Copysign, Copysign
    | Rotl, Rotl
    | Rotr, Rotr
    | At, At
    | List_cons, List_cons
    | List_append, List_append
    | String_prefix, String_prefix
    | String_suffix, String_suffix
    | String_contains, String_contains
    | String_last_index, String_last_index
    | String_in_re, String_in_re
    | Regexp_range, Regexp_range ->
      true
    | ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And
        | Or | Xor | Pow | Min | Max | Copysign | Rotl | Rotr | At | List_cons
        | List_append | String_prefix | String_suffix | String_contains
        | String_last_index | String_in_re | Regexp_range )
      , _ ) ->
      false

  let pp fmt = function
    | Add -> Fmt.string fmt "add"
    | Sub -> Fmt.string fmt "sub"
    | Mul -> Fmt.string fmt "mul"
    | Div -> Fmt.string fmt "div_s"
    | DivU -> Fmt.string fmt "div_u"
    | Rem -> Fmt.string fmt "rem_s"
    | RemU -> Fmt.string fmt "rem_u"
    | Shl -> Fmt.string fmt "shl"
    | ShrA -> Fmt.string fmt "shr_s"
    | ShrL -> Fmt.string fmt "shr_u"
    | And -> Fmt.string fmt "and"
    | Or -> Fmt.string fmt "or"
    | Xor -> Fmt.string fmt "xor"
    | Pow -> Fmt.string fmt "pow"
    | Min -> Fmt.string fmt "min"
    | Max -> Fmt.string fmt "max"
    | Copysign -> Fmt.string fmt "copysign"
    | Rotl -> Fmt.string fmt "rotl"
    | Rotr -> Fmt.string fmt "rotr"
    | At -> Fmt.string fmt "at"
    | List_cons -> Fmt.string fmt "cons"
    | List_append -> Fmt.string fmt "append"
    | String_prefix -> Fmt.string fmt "prefixof"
    | String_suffix -> Fmt.string fmt "suffixof"
    | String_contains -> Fmt.string fmt "contains"
    | String_last_index -> Fmt.string fmt "last_indexof"
    | String_in_re -> Fmt.string fmt "in_re"
    | Regexp_range -> Fmt.string fmt "range"
end

module Relop = struct
  type t =
    | Eq
    | Ne
    | Lt
    | LtU
    | Gt
    | GtU
    | Le
    | LeU
    | Ge
    | GeU

  let equal op1 op2 =
    match (op1, op2) with
    | Eq, Eq
    | Ne, Ne
    | Lt, Lt
    | LtU, LtU
    | Gt, Gt
    | GtU, GtU
    | Le, Le
    | LeU, LeU
    | Ge, Ge
    | GeU, GeU ->
      true
    | (Eq | Ne | Lt | LtU | Gt | GtU | Le | LeU | Ge | GeU), _ -> false

  let pp fmt = function
    | Eq -> Fmt.string fmt "eq"
    | Ne -> Fmt.string fmt "ne"
    | Lt -> Fmt.string fmt "lt_s"
    | LtU -> Fmt.string fmt "lt_u"
    | Gt -> Fmt.string fmt "gt_s"
    | GtU -> Fmt.string fmt "gt_u"
    | Le -> Fmt.string fmt "le_s"
    | LeU -> Fmt.string fmt "le_u"
    | Ge -> Fmt.string fmt "ge_s"
    | GeU -> Fmt.string fmt "ge_u"
end

module Triop = struct
  type t =
    | Ite
    | List_set
    (* String *)
    | String_extract
    | String_replace
    | String_index

  let equal op1 op2 =
    match (op1, op2) with
    | Ite, Ite
    | List_set, List_set
    | String_extract, String_extract
    | String_replace, String_replace
    | String_index, String_index ->
      true
    | (Ite | List_set | String_extract | String_replace | String_index), _ ->
      false

  let pp fmt = function
    | Ite -> Fmt.string fmt "ite"
    | String_extract -> Fmt.string fmt "substr"
    | String_replace -> Fmt.string fmt "replace"
    | String_index -> Fmt.string fmt "indexof"
    | List_set -> Fmt.string fmt "set"
end

module Cvtop = struct
  type t =
    | ToString
    | OfString
    | ToBool
    | OfBool
    | Reinterpret_int
    | Reinterpret_float
    | DemoteF64
    | PromoteF32
    | ConvertSI32
    | ConvertUI32
    | ConvertSI64
    | ConvertUI64
    | TruncSF32
    | TruncUF32
    | TruncSF64
    | TruncUF64
    | Trunc_sat_f32_s
    | Trunc_sat_f32_u
    | Trunc_sat_f64_s
    | Trunc_sat_f64_u
    | 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
    | String_to_re

  let equal op1 op2 =
    match (op1, op2) with
    | ToString, ToString
    | OfString, OfString
    | ToBool, ToBool
    | OfBool, OfBool
    | Reinterpret_int, Reinterpret_int
    | Reinterpret_float, Reinterpret_float
    | DemoteF64, DemoteF64
    | PromoteF32, PromoteF32
    | ConvertSI32, ConvertSI32
    | ConvertUI32, ConvertUI32
    | ConvertSI64, ConvertSI64
    | ConvertUI64, ConvertUI64
    | TruncSF32, TruncSF32
    | TruncUF32, TruncUF32
    | TruncSF64, TruncSF64
    | TruncUF64, TruncUF64
    | Trunc_sat_f32_s, Trunc_sat_f32_s
    | Trunc_sat_f32_u, Trunc_sat_f32_u
    | Trunc_sat_f64_s, Trunc_sat_f64_s
    | Trunc_sat_f64_u, Trunc_sat_f64_u
    | WrapI64, WrapI64
    | String_to_code, String_to_code
    | String_from_code, String_from_code
    | String_to_int, String_to_int
    | String_from_int, String_from_int
    | String_to_float, String_to_float
    | String_to_re, String_to_re ->
      true
    | Sign_extend x1, Sign_extend x2 | Zero_extend x1, Zero_extend x2 -> x1 = x2
    | ( ( ToString | OfString | ToBool | OfBool | Reinterpret_int
        | Reinterpret_float | DemoteF64 | PromoteF32 | ConvertSI32 | ConvertUI32
        | ConvertSI64 | ConvertUI64 | TruncSF32 | TruncUF32 | TruncSF64
        | TruncUF64 | Trunc_sat_f32_s | Trunc_sat_f32_u | Trunc_sat_f64_s
        | Trunc_sat_f64_u | WrapI64 | Sign_extend _ | Zero_extend _
        | String_to_code | String_from_code | String_to_int | String_from_int
        | String_to_float | String_to_re )
      , _ ) ->
      false

  let pp fmt = function
    | ToString -> Fmt.string fmt "to_string"
    | OfString -> Fmt.string fmt "of_string"
    | ToBool -> Fmt.string fmt "to_bool"
    | OfBool -> Fmt.string fmt "of_bool"
    | Reinterpret_int -> Fmt.string fmt "reinterpret_int"
    | Reinterpret_float -> Fmt.string fmt "reinterpret_float"
    | DemoteF64 -> Fmt.string fmt "demote_f64"
    | PromoteF32 -> Fmt.string fmt "promote_f32"
    | ConvertSI32 -> Fmt.string fmt "convert_i32_s"
    | ConvertUI32 -> Fmt.string fmt "convert_i32_u"
    | ConvertSI64 -> Fmt.string fmt "convert_i64_s"
    | ConvertUI64 -> Fmt.string fmt "convert_i64_u"
    | TruncSF32 -> Fmt.string fmt "trunc_f32_s"
    | TruncUF32 -> Fmt.string fmt "trunc_f32_u"
    | TruncSF64 -> Fmt.string fmt "trunc_f64_s"
    | TruncUF64 -> Fmt.string fmt "trunc_f64_u"
    | Trunc_sat_f32_s -> Fmt.string fmt "trunc_sat_f32_s"
    | Trunc_sat_f32_u -> Fmt.string fmt "trunc_sat_f32_u"
    | Trunc_sat_f64_s -> Fmt.string fmt "trunc_sat_f64_s"
    | Trunc_sat_f64_u -> Fmt.string fmt "trunc_sat_f64_u"
    | WrapI64 -> Fmt.string fmt "wrap_i64"
    | Sign_extend sz -> Fmt.pf fmt "extend_i%d_s" sz
    | Zero_extend sz -> Fmt.pf fmt "extend_i%d_u" sz
    | String_to_code -> Fmt.string fmt "to_code"
    | String_from_code -> Fmt.string fmt "from_code"
    | String_to_int -> Fmt.string fmt "to_int"
    | String_from_int -> Fmt.string fmt "from_int"
    | String_to_float -> Fmt.string fmt "to_float"
    | String_to_re -> Fmt.string fmt "to_re"
end

module Naryop = struct
  type t =
    | Logand
    | Logor
    | Concat
    | Regexp_union

  let equal op1 op2 =
    match (op1, op2) with
    | Logand, Logand
    | Logor, Logor
    | Concat, Concat
    | Regexp_union, Regexp_union ->
      true
    | (Logand | Logor | Concat | Regexp_union), _ -> false

  let pp fmt = function
    | Logand -> Fmt.string fmt "and"
    | Logor -> Fmt.string fmt "or"
    | Concat -> Fmt.string fmt "++"
    | Regexp_union -> Fmt.string fmt "union"
end

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	type _ cast =
6	\| C8 : int cast
7	\| C32 : int32 cast
8	\| C64 : int64 cast
9
10	type t =
11	\| Ty_app
12	\| Ty_bitv of int
13	\| Ty_bool
14	\| Ty_fp of int
15	\| Ty_int
16	\| Ty_list
17	\| Ty_none
18	\| Ty_real
19	\| Ty_str
20	\| Ty_unit
21	\| Ty_regexp
22
23	let discr = function
24	\| Ty_app -> 0	×
25	\| Ty_bool -> 1	2✔
26	\| Ty_int -> 2	18✔
27	\| Ty_list -> 3	×
28	\| Ty_none -> 4	×
29	\| Ty_real -> 5	×
30	\| Ty_str -> 6	×
31	\| Ty_unit -> 7	×
32	\| Ty_regexp -> 8	×
33	\| Ty_bitv n -> 9 + n	32✔
34	\| Ty_fp n -> 10 + n	×
35
36	let compare t1 t2 = compare (discr t1) (discr t2)	26✔
37
38	let equal t1 t2 = compare t1 t2 = 0	15✔
39
40	let pp fmt = function
41	\| Ty_int -> Fmt.string fmt "int"	103✔
42	\| Ty_real -> Fmt.string fmt "real"	63✔
43	\| Ty_bool -> Fmt.string fmt "bool"	31✔
44	\| Ty_str -> Fmt.string fmt "str"	81✔
45	\| Ty_bitv n -> Fmt.pf fmt "i%d" n	262✔
46	\| Ty_fp n -> Fmt.pf fmt "f%d" n	81✔
47	\| Ty_list -> Fmt.string fmt "list"	18✔
48	\| Ty_app -> Fmt.string fmt "app"	×
49	\| Ty_unit -> Fmt.string fmt "unit"	×
50	\| Ty_none -> Fmt.string fmt "none"	×
51	\| Ty_regexp -> Fmt.string fmt "regexp"	×
52
53	let string_of_type (ty : t) : string = Fmt.str "%a" pp ty	×
54
55	let of_string = function
56	\| "int" -> Ok Ty_int	2✔
57	\| "real" -> Ok Ty_real	×
58	\| "bool" -> Ok Ty_bool	2✔
59	\| "str" -> Ok Ty_str	×
60	\| "list" -> Ok Ty_list	×
61	\| "app" -> Ok Ty_app	×
62	\| "unit" -> Ok Ty_unit	×
63	\| "none" -> Ok Ty_none	×
64	\| "regexp" -> Ok Ty_regexp	×
65	\| s ->	7✔
66	if String.starts_with ~prefix:"i" s then begin	4✔
67	let s = String.sub s 1 (String.length s - 1) in	4✔
68	match int_of_string_opt s with	4✔
69	\| None -> Fmt.error_msg "can not parse type %s" s	×
70	\| Some n when n < 0 ->	4✔
71	Fmt.error_msg "size of bitvectors must be a positive integer"	×
72	\| Some n -> Ok (Ty_bitv n)	4✔
73	end
74	else if String.starts_with ~prefix:"f" s then begin	3✔
75	let s = String.sub s 1 (String.length s - 1) in	3✔
76	match int_of_string_opt s with	3✔
77	\| None -> Fmt.error_msg "can not parse type %s" s	×
78	\| Some n when n < 0 ->	3✔
79	Fmt.error_msg "size of fp must be a positive integer"	×
80	\| Some n -> Ok (Ty_fp n)	3✔
81	end
82	else Fmt.error_msg "can not parse type %s" s	×
83
84	let size (ty : t) : int =
85	match ty with	2✔
86	\| Ty_bitv n \| Ty_fp n -> n / 8	×
87	\| Ty_int \| Ty_bool -> 4	×
88	\| Ty_real \| Ty_str \| Ty_list \| Ty_app \| Ty_unit \| Ty_none \| Ty_regexp ->
89	assert false
90
91	module Unop = struct
92	type t =
93	\| Neg
94	\| Not
95	\| Clz
96	\| Ctz
97	\| Popcnt
98	(* Float *)
99	\| Abs
100	\| Sqrt
101	\| Is_nan
102	\| Ceil
103	\| Floor
104	\| Trunc
105	\| Nearest
106	\| Head
107	\| Tail
108	\| Reverse
109	\| Length
110	(* String *)
111	\| Trim
112	(* RegExp *)
113	\| Regexp_star
114	\| Regexp_loop of (int * int)
115	\| Regexp_plus
116	\| Regexp_opt
117	\| Regexp_comp
118
119	let equal o1 o2 =
120	match (o1, o2) with	×
121	\| Neg, Neg	×
122	\| Not, Not	×
123	\| Clz, Clz	×
124	\| Popcnt, Popcnt	×
125	\| Ctz, Ctz	×
126	\| Abs, Abs	×
127	\| Sqrt, Sqrt	×
128	\| Is_nan, Is_nan	×
129	\| Ceil, Ceil	×
130	\| Floor, Floor	×
131	\| Trunc, Trunc	×
132	\| Nearest, Nearest	×
133	\| Head, Head	×
134	\| Tail, Tail	×
135	\| Reverse, Reverse	×
136	\| Length, Length	×
137	\| Trim, Trim	×
138	\| Regexp_star, Regexp_star	×
139	\| Regexp_loop _, Regexp_loop _	×
140	\| Regexp_plus, Regexp_plus	×
141	\| Regexp_opt, Regexp_opt	×
142	\| Regexp_comp, Regexp_comp ->	×
143	true
144	\| ( ( Neg \| Not \| Clz \| Popcnt \| Ctz \| Abs \| Sqrt \| Is_nan \| Ceil \| Floor	×
145	\| Trunc \| Nearest \| Head \| Tail \| Reverse \| Length \| Trim \| Regexp_star	×
146	\| Regexp_loop _ \| Regexp_plus \| Regexp_opt \| Regexp_comp )	×
147	, _ ) ->
148	false
149
150	let pp fmt = function
151	\| Neg -> Fmt.string fmt "neg"	4✔
152	\| Not -> Fmt.string fmt "not"	3✔
153	\| Clz -> Fmt.string fmt "clz"	×
154	\| Ctz -> Fmt.string fmt "ctz"	×
155	\| Popcnt -> Fmt.string fmt "popcnt"	×
156	\| Abs -> Fmt.string fmt "abs"	2✔
157	\| Sqrt -> Fmt.string fmt "sqrt"	1✔
158	\| Is_nan -> Fmt.string fmt "is_nan"	1✔
159	\| Ceil -> Fmt.string fmt "ceil"	1✔
160	\| Floor -> Fmt.string fmt "floor"	1✔
161	\| Trunc -> Fmt.string fmt "trunc"	3✔
162	\| Nearest -> Fmt.string fmt "nearest"	1✔
163	\| Head -> Fmt.string fmt "head"	1✔
164	\| Tail -> Fmt.string fmt "tail"	1✔
165	\| Reverse -> Fmt.string fmt "reverse"	1✔
166	\| Length -> Fmt.string fmt "length"	2✔
167	\| Trim -> Fmt.string fmt "trim"	1✔
168	\| Regexp_star -> Fmt.string fmt "*"	×
169	\| Regexp_loop _ -> Fmt.string fmt "loop"	×
170	\| Regexp_plus -> Fmt.string fmt "+"	×
171	\| Regexp_opt -> Fmt.string fmt "opt"	×
172	\| Regexp_comp -> Fmt.string fmt "comp"	×
173	end
174
175	module Binop = struct
176	type t =
177	\| Add
178	\| Sub
179	\| Mul
180	\| Div
181	\| DivU
182	\| Rem
183	\| RemU
184	\| Shl
185	\| ShrA
186	\| ShrL
187	\| And
188	\| Or
189	\| Xor
190	\| Pow
191	\| Min
192	\| Max
193	\| Copysign
194	\| Rotl
195	\| Rotr
196	\| At
197	\| List_cons
198	\| List_append
199	(* String *)
200	\| String_prefix
201	\| String_suffix
202	\| String_contains
203	\| String_last_index
204	\| String_in_re
205	(* Regexp *)
206	\| Regexp_range
207
208	let equal o1 o2 =
209	match (o1, o2) with	12✔
210	\| Add, Add	8✔
211	\| Sub, Sub	1✔
212	\| Mul, Mul	3✔
213	\| Div, Div	×
214	\| DivU, DivU	×
215	\| Rem, Rem	×
216	\| RemU, RemU	×
217	\| Shl, Shl	×
218	\| ShrA, ShrA	×
219	\| ShrL, ShrL	×
220	\| And, And	×
221	\| Or, Or	×
222	\| Xor, Xor	×
223	\| Pow, Pow	×
224	\| Min, Min	×
225	\| Max, Max	×
226	\| Copysign, Copysign	×
227	\| Rotl, Rotl	×
228	\| Rotr, Rotr	×
229	\| At, At	×
230	\| List_cons, List_cons	×
231	\| List_append, List_append	×
232	\| String_prefix, String_prefix	×
233	\| String_suffix, String_suffix	×
234	\| String_contains, String_contains	×
235	\| String_last_index, String_last_index	×
236	\| String_in_re, String_in_re	×
237	\| Regexp_range, Regexp_range ->	×
238	true
239	\| ( ( Add \| Sub \| Mul \| Div \| DivU \| Rem \| RemU \| Shl \| ShrA \| ShrL \| And	×
240	\| Or \| Xor \| Pow \| Min \| Max \| Copysign \| Rotl \| Rotr \| At \| List_cons	×
241	\| List_append \| String_prefix \| String_suffix \| String_contains	×
242	\| String_last_index \| String_in_re \| Regexp_range )	×
243	, _ ) ->
244	false
245
246	let pp fmt = function
247	\| Add -> Fmt.string fmt "add"	28✔
248	\| Sub -> Fmt.string fmt "sub"	12✔
249	\| Mul -> Fmt.string fmt "mul"	12✔
250	\| Div -> Fmt.string fmt "div_s"	8✔
251	\| DivU -> Fmt.string fmt "div_u"	×
252	\| Rem -> Fmt.string fmt "rem_s"	10✔
253	\| RemU -> Fmt.string fmt "rem_u"	×
254	\| Shl -> Fmt.string fmt "shl"	6✔
255	\| ShrA -> Fmt.string fmt "shr_s"	8✔
256	\| ShrL -> Fmt.string fmt "shr_u"	×
257	\| And -> Fmt.string fmt "and"	8✔
258	\| Or -> Fmt.string fmt "or"	6✔
259	\| Xor -> Fmt.string fmt "xor"	6✔
260	\| Pow -> Fmt.string fmt "pow"	2✔
261	\| Min -> Fmt.string fmt "min"	4✔
262	\| Max -> Fmt.string fmt "max"	4✔
263	\| Copysign -> Fmt.string fmt "copysign"	16✔
264	\| Rotl -> Fmt.string fmt "rotl"	4✔
265	\| Rotr -> Fmt.string fmt "rotr"	4✔
266	\| At -> Fmt.string fmt "at"	4✔
267	\| List_cons -> Fmt.string fmt "cons"	1✔
268	\| List_append -> Fmt.string fmt "append"	2✔
269	\| String_prefix -> Fmt.string fmt "prefixof"	2✔
270	\| String_suffix -> Fmt.string fmt "suffixof"	2✔
271	\| String_contains -> Fmt.string fmt "contains"	2✔
272	\| String_last_index -> Fmt.string fmt "last_indexof"	×
273	\| String_in_re -> Fmt.string fmt "in_re"	×
274	\| Regexp_range -> Fmt.string fmt "range"	×
275	end
276
277	module Relop = struct
278	type t =
279	\| Eq
280	\| Ne
281	\| Lt
282	\| LtU
283	\| Gt
284	\| GtU
285	\| Le
286	\| LeU
287	\| Ge
288	\| GeU
289
290	let equal op1 op2 =
291	match (op1, op2) with	1✔
292	\| Eq, Eq	1✔
293	\| Ne, Ne	×
294	\| Lt, Lt	×
295	\| LtU, LtU	×
296	\| Gt, Gt	×
297	\| GtU, GtU	×
298	\| Le, Le	×
299	\| LeU, LeU	×
300	\| Ge, Ge	×
301	\| GeU, GeU ->	×
302	true
303	\| (Eq \| Ne \| Lt \| LtU \| Gt \| GtU \| Le \| LeU \| Ge \| GeU), _ -> false	×
304
305	let pp fmt = function
306	\| Eq -> Fmt.string fmt "eq"	6✔
307	\| Ne -> Fmt.string fmt "ne"	4✔
308	\| Lt -> Fmt.string fmt "lt_s"	16✔
309	\| LtU -> Fmt.string fmt "lt_u"	6✔
310	\| Gt -> Fmt.string fmt "gt_s"	16✔
311	\| GtU -> Fmt.string fmt "gt_u"	6✔
312	\| Le -> Fmt.string fmt "le_s"	16✔
313	\| LeU -> Fmt.string fmt "le_u"	6✔
314	\| Ge -> Fmt.string fmt "ge_s"	16✔
315	\| GeU -> Fmt.string fmt "ge_u"	6✔
316	end
317
318	module Triop = struct
319	type t =
320	\| Ite
321	\| List_set
322	(* String *)
323	\| String_extract
324	\| String_replace
325	\| String_index
326
327	let equal op1 op2 =
328	match (op1, op2) with	×
329	\| Ite, Ite	×
330	\| List_set, List_set	×
331	\| String_extract, String_extract	×
332	\| String_replace, String_replace	×
333	\| String_index, String_index ->	×
334	true
335	\| (Ite \| List_set \| String_extract \| String_replace \| String_index), _ ->	×
336	false
337
338	let pp fmt = function
339	\| Ite -> Fmt.string fmt "ite"	×
340	\| String_extract -> Fmt.string fmt "substr"	3✔
341	\| String_replace -> Fmt.string fmt "replace"	3✔
342	\| String_index -> Fmt.string fmt "indexof"	3✔
343	\| List_set -> Fmt.string fmt "set"	2✔
344	end
345
346	module Cvtop = struct
347	type t =
348	\| ToString
349	\| OfString
350	\| ToBool
351	\| OfBool
352	\| Reinterpret_int
353	\| Reinterpret_float
354	\| DemoteF64
355	\| PromoteF32
356	\| ConvertSI32
357	\| ConvertUI32
358	\| ConvertSI64
359	\| ConvertUI64
360	\| TruncSF32
361	\| TruncUF32
362	\| TruncSF64
363	\| TruncUF64
364	\| Trunc_sat_f32_s
365	\| Trunc_sat_f32_u
366	\| Trunc_sat_f64_s
367	\| Trunc_sat_f64_u
368	\| WrapI64
369	\| Sign_extend of int
370	\| Zero_extend of int
371	(* String *)
372	\| String_to_code
373	\| String_from_code
374	\| String_to_int
375	\| String_from_int
376	\| String_to_float
377	\| String_to_re
378
379	let equal op1 op2 =
380	match (op1, op2) with	×
381	\| ToString, ToString	×
382	\| OfString, OfString	×
383	\| ToBool, ToBool	×
384	\| OfBool, OfBool	×
385	\| Reinterpret_int, Reinterpret_int	×
386	\| Reinterpret_float, Reinterpret_float	×
387	\| DemoteF64, DemoteF64	×
388	\| PromoteF32, PromoteF32	×
389	\| ConvertSI32, ConvertSI32	×
390	\| ConvertUI32, ConvertUI32	×
391	\| ConvertSI64, ConvertSI64	×
392	\| ConvertUI64, ConvertUI64	×
393	\| TruncSF32, TruncSF32	×
394	\| TruncUF32, TruncUF32	×
395	\| TruncSF64, TruncSF64	×
396	\| TruncUF64, TruncUF64	×
397	\| Trunc_sat_f32_s, Trunc_sat_f32_s	×
398	\| Trunc_sat_f32_u, Trunc_sat_f32_u	×
399	\| Trunc_sat_f64_s, Trunc_sat_f64_s	×
400	\| Trunc_sat_f64_u, Trunc_sat_f64_u	×
401	\| WrapI64, WrapI64	×
402	\| String_to_code, String_to_code	×
403	\| String_from_code, String_from_code	×
404	\| String_to_int, String_to_int	×
405	\| String_from_int, String_from_int	×
406	\| String_to_float, String_to_float	×
407	\| String_to_re, String_to_re ->	×
408	true
409	\| Sign_extend x1, Sign_extend x2 \| Zero_extend x1, Zero_extend x2 -> x1 = x2	×
410	\| ( ( ToString \| OfString \| ToBool \| OfBool \| Reinterpret_int	×
411	\| Reinterpret_float \| DemoteF64 \| PromoteF32 \| ConvertSI32 \| ConvertUI32	×
412	\| ConvertSI64 \| ConvertUI64 \| TruncSF32 \| TruncUF32 \| TruncSF64	×
413	\| TruncUF64 \| Trunc_sat_f32_s \| Trunc_sat_f32_u \| Trunc_sat_f64_s	×
414	\| Trunc_sat_f64_u \| WrapI64 \| Sign_extend _ \| Zero_extend _	×
415	\| String_to_code \| String_from_code \| String_to_int \| String_from_int	×
416	\| String_to_float \| String_to_re )	×
417	, _ ) ->
418	false
419
420	let pp fmt = function
421	\| ToString -> Fmt.string fmt "to_string"	2✔
422	\| OfString -> Fmt.string fmt "of_string"	×
423	\| ToBool -> Fmt.string fmt "to_bool"	×
424	\| OfBool -> Fmt.string fmt "of_bool"	×
425	\| Reinterpret_int -> Fmt.string fmt "reinterpret_int"	×
426	\| Reinterpret_float -> Fmt.string fmt "reinterpret_float"	×
427	\| DemoteF64 -> Fmt.string fmt "demote_f64"	×
428	\| PromoteF32 -> Fmt.string fmt "promote_f32"	×
429	\| ConvertSI32 -> Fmt.string fmt "convert_i32_s"	2✔
430	\| ConvertUI32 -> Fmt.string fmt "convert_i32_u"	×
431	\| ConvertSI64 -> Fmt.string fmt "convert_i64_s"	2✔
432	\| ConvertUI64 -> Fmt.string fmt "convert_i64_u"	×
433	\| TruncSF32 -> Fmt.string fmt "trunc_f32_s"	2✔
434	\| TruncUF32 -> Fmt.string fmt "trunc_f32_u"	×
435	\| TruncSF64 -> Fmt.string fmt "trunc_f64_s"	2✔
436	\| TruncUF64 -> Fmt.string fmt "trunc_f64_u"	×
437	\| Trunc_sat_f32_s -> Fmt.string fmt "trunc_sat_f32_s"	×
438	\| Trunc_sat_f32_u -> Fmt.string fmt "trunc_sat_f32_u"	×
439	\| Trunc_sat_f64_s -> Fmt.string fmt "trunc_sat_f64_s"	×
440	\| Trunc_sat_f64_u -> Fmt.string fmt "trunc_sat_f64_u"	×
441	\| WrapI64 -> Fmt.string fmt "wrap_i64"	×
442	\| Sign_extend sz -> Fmt.pf fmt "extend_i%d_s" sz	×
443	\| Zero_extend sz -> Fmt.pf fmt "extend_i%d_u" sz	×
444	\| String_to_code -> Fmt.string fmt "to_code"	1✔
445	\| String_from_code -> Fmt.string fmt "from_code"	1✔
446	\| String_to_int -> Fmt.string fmt "to_int"	1✔
447	\| String_from_int -> Fmt.string fmt "from_int"	1✔
448	\| String_to_float -> Fmt.string fmt "to_float"	1✔
449	\| String_to_re -> Fmt.string fmt "to_re"	×
450	end
451
452	module Naryop = struct
453	type t =
454	\| Logand
455	\| Logor
456	\| Concat
457	\| Regexp_union
458
459	let equal op1 op2 =
460	match (op1, op2) with	×
461	\| Logand, Logand	×
462	\| Logor, Logor	×
463	\| Concat, Concat	×
464	\| Regexp_union, Regexp_union ->	×
465	true
466	\| (Logand \| Logor \| Concat \| Regexp_union), _ -> false	×
467
468	let pp fmt = function
469	\| Logand -> Fmt.string fmt "and"	6✔
470	\| Logor -> Fmt.string fmt "or"	6✔
471	\| Concat -> Fmt.string fmt "++"	6✔
472	\| Regexp_union -> Fmt.string fmt "union"	×
473	end

formalsec / smtml / 321

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