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

34.92

/src/smtml/num.ml

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

type t =
  | I8 of int
  | I32 of int32
  | I64 of int64
  | F32 of int32
  | F64 of int64

type printer =
  [ `Pretty
  | `Hexadecimal
  ]

let type_of (n : t) =
  match n with
  | I8 _ -> Ty.(Ty_bitv 8)
  | I32 _ -> Ty.(Ty_bitv 32)
  | I64 _ -> Ty.(Ty_bitv 64)
  | F32 _ -> Ty.(Ty_fp 32)
  | F64 _ -> Ty.(Ty_fp 64)

let compare n1 n2 =
  match (n1, n2) with
  | I8 i1, I8 i2 -> Int.compare i1 i2
  | I32 i1, I32 i2 -> Int32.compare i1 i2
  | I64 i1, I64 i2 -> Int64.compare i1 i2
  | F32 i1, F32 i2 ->
    Float.compare (Int32.float_of_bits i1) (Int32.float_of_bits i2)
  | F64 i1, F64 i2 ->
    Float.compare (Int64.float_of_bits i1) (Int64.float_of_bits i2)
  | I8 _, _ -> -1
  | I32 _, I8 _ -> 1
  | I32 _, _ -> -1
  | I64 _, (I8 _ | I32 _) -> 1
  | I64 _, _ -> -1
  | F32 _, (I8 _ | I32 _ | I64 _) -> 1
  | F32 _, F64 _ -> -1
  | F64 _, _ -> 1

let equal (n1 : t) (n2 : t) : bool = compare n1 n2 = 0

let num_of_bool (b : bool) : t = I32 (if b then 1l else 0l)

let pp_num fmt (n : t) =
  match n with
  | I8 i -> Fmt.pf fmt "(i8 %d)" i
  | I32 i -> Fmt.pf fmt "(i32 %ld)" i
  | I64 i -> Fmt.pf fmt "(i64 %Ld)" i
  | F32 f -> Fmt.pf fmt "(f32 %F)" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "(f64 %F)" (Int64.float_of_bits f)

let pp_hex fmt (n : t) =
  match n with
  | I8 i -> Fmt.pf fmt "0x%02x" (i land 0xff)
  | I32 i -> Fmt.pf fmt "0x%08lx" i
  | I64 i -> Fmt.pf fmt "0x%016Lx" i
  | F32 f -> Fmt.pf fmt "(fp 0x%08lx)" f
  | F64 f -> Fmt.pf fmt "(fp 0x%016Lx)" f

let pp_no_type fmt = function
  | I8 i -> Fmt.pf fmt "%d" i
  | I32 i -> Fmt.pf fmt "%ld" i
  | I64 i -> Fmt.pf fmt "%Ld" i
  | F32 f -> Fmt.pf fmt "%F" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "%F" (Int64.float_of_bits f)

let printer = ref pp_num

let set_default_printer = function
  | `Pretty -> printer := pp_num
  | `Hexadecimal -> printer := pp_hex

let pp fmt v = !printer fmt v

let to_string (n : t) : string = Fmt.str "%a" pp n

let of_string (cast : Ty.t) value =
  match cast with
  | Ty_bitv 1 -> (
    match value with
    | "true" -> Ok (I32 1l)
    | "false" -> Ok (I32 0l)
    | _ -> Fmt.error_msg "invalid value %s, expected 1-bit bitv" value )
  | Ty_bitv 8 -> (
    match int_of_string_opt value with
    | None -> Fmt.error_msg "invalid value %s, expected 8-bit bitv" value
    | Some n -> Ok (I8 n) )
  | Ty_bitv 32 -> Ok (I32 (Int32.of_string value))
  | Ty_bitv 64 -> Ok (I64 (Int64.of_string value))
  | Ty_fp 32 -> (
    match float_of_string_opt value with
    | None -> Fmt.error_msg "invalid value %s, expected float" value
    | Some n -> Ok (F32 (Int32.bits_of_float n)) )
  | Ty_fp 64 -> (
    match float_of_string_opt value with
    | None -> Fmt.error_msg "invalid value %s, expected float" value
    | Some n -> Ok (F64 (Int64.bits_of_float n)) )
  | _ -> Fmt.error_msg "invalid value, expected num"

let to_json (n : t) : Yojson.Basic.t = `String (Fmt.str "%a" pp_no_type n)

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	type t =
6	\| I8 of int
7	\| I32 of int32
8	\| I64 of int64
9	\| F32 of int32
10	\| F64 of int64
11
12	type printer =
13	[ `Pretty
14	\| `Hexadecimal
15	]
16
17	let type_of (n : t) =
18	match n with	170✔
19	\| I8 _ -> Ty.(Ty_bitv 8)	×
20	\| I32 _ -> Ty.(Ty_bitv 32)	86✔
21	\| I64 _ -> Ty.(Ty_bitv 64)	44✔
22	\| F32 _ -> Ty.(Ty_fp 32)	21✔
23	\| F64 _ -> Ty.(Ty_fp 64)	19✔
24
25	let compare n1 n2 =
26	match (n1, n2) with	235✔
27	\| I8 i1, I8 i2 -> Int.compare i1 i2	×
28	\| I32 i1, I32 i2 -> Int32.compare i1 i2	108✔
29	\| I64 i1, I64 i2 -> Int64.compare i1 i2	77✔
30	\| F32 i1, F32 i2 ->	26✔
31	Float.compare (Int32.float_of_bits i1) (Int32.float_of_bits i2)	26✔
32	\| F64 i1, F64 i2 ->	24✔
33	Float.compare (Int64.float_of_bits i1) (Int64.float_of_bits i2)	24✔
34	\| I8 _, _ -> -1	×
35	\| I32 _, I8 _ -> 1	×
36	\| I32 _, _ -> -1	×
37	\| I64 _, (I8 _ \| I32 _) -> 1	×
38	\| I64 _, _ -> -1	×
39	\| F32 _, (I8 _ \| I32 _ \| I64 _) -> 1	×
40	\| F32 _, F64 _ -> -1	×
41	\| F64 _, _ -> 1	×
42
43	let equal (n1 : t) (n2 : t) : bool = compare n1 n2 = 0	235✔
44
45	let num_of_bool (b : bool) : t = I32 (if b then 1l else 0l)	×
46
47	let pp_num fmt (n : t) =
48	match n with	×
49	\| I8 i -> Fmt.pf fmt "(i8 %d)" i	×
50	\| I32 i -> Fmt.pf fmt "(i32 %ld)" i	×
51	\| I64 i -> Fmt.pf fmt "(i64 %Ld)" i	×
52	\| F32 f -> Fmt.pf fmt "(f32 %F)" (Int32.float_of_bits f)	×
53	\| F64 f -> Fmt.pf fmt "(f64 %F)" (Int64.float_of_bits f)	×
54
55	let pp_hex fmt (n : t) =
56	match n with	×
57	\| I8 i -> Fmt.pf fmt "0x%02x" (i land 0xff)	×
58	\| I32 i -> Fmt.pf fmt "0x%08lx" i	×
59	\| I64 i -> Fmt.pf fmt "0x%016Lx" i	×
60	\| F32 f -> Fmt.pf fmt "(fp 0x%08lx)" f	×
61	\| F64 f -> Fmt.pf fmt "(fp 0x%016Lx)" f	×
62
63	let pp_no_type fmt = function
64	\| I8 i -> Fmt.pf fmt "%d" i	×
65	\| I32 i -> Fmt.pf fmt "%ld" i	1✔
66	\| I64 i -> Fmt.pf fmt "%Ld" i	1✔
67	\| F32 f -> Fmt.pf fmt "%F" (Int32.float_of_bits f)	1✔
68	\| F64 f -> Fmt.pf fmt "%F" (Int64.float_of_bits f)	×
69
70	let printer = ref pp_num
71
72	let set_default_printer = function
73	\| `Pretty -> printer := pp_num	×
74	\| `Hexadecimal -> printer := pp_hex	×
75
76	let pp fmt v = !printer fmt v	×
77
78	let to_string (n : t) : string = Fmt.str "%a" pp n	×
79
80	let of_string (cast : Ty.t) value =
81	match cast with	7✔
82	\| Ty_bitv 1 -> (	×
83	match value with
84	\| "true" -> Ok (I32 1l)	×
85	\| "false" -> Ok (I32 0l)	×
86	\| _ -> Fmt.error_msg "invalid value %s, expected 1-bit bitv" value )	×
87	\| Ty_bitv 8 -> (	×
88	match int_of_string_opt value with
89	\| None -> Fmt.error_msg "invalid value %s, expected 8-bit bitv" value	×
90	\| Some n -> Ok (I8 n) )	×
91	\| Ty_bitv 32 -> Ok (I32 (Int32.of_string value))	1✔
92	\| Ty_bitv 64 -> Ok (I64 (Int64.of_string value))	3✔
93	\| Ty_fp 32 -> (	3✔
94	match float_of_string_opt value with
95	\| None -> Fmt.error_msg "invalid value %s, expected float" value	×
96	\| Some n -> Ok (F32 (Int32.bits_of_float n)) )	3✔
97	\| Ty_fp 64 -> (	×
98	match float_of_string_opt value with
99	\| None -> Fmt.error_msg "invalid value %s, expected float" value	×
100	\| Some n -> Ok (F64 (Int64.bits_of_float n)) )	×
101	\| _ -> Fmt.error_msg "invalid value, expected num"	×
102
103	let to_json (n : t) : Yojson.Basic.t = `String (Fmt.str "%a" pp_no_type n)	3✔

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