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.52

/src/smtml/value.ml

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

open Ty

type t =
  | True
  | False
  | Unit
  | Int of int
  | Real of float
  | Str of string
  | Num of Num.t
  | List of t list
  | App : [> `Op of string ] * t list -> t
  | Nothing

let type_of (v : t) : Ty.t =
  match v with
  | True | False -> Ty_bool
  | Unit -> Ty_unit
  | Int _ -> Ty_int
  | Real _ -> Ty_real
  | Str _ -> Ty_str
  | Num n -> Num.type_of n
  | List _ -> Ty_list
  | App _ -> Ty_app
  | Nothing -> Ty_none

let discr = function
  | True -> 0
  | False -> 1
  | Unit -> 2
  | Int _ -> 3
  | Real _ -> 4
  | Str _ -> 5
  | Num _ -> 6
  | List _ -> 7
  | App _ -> 8
  | Nothing -> 9

let rec compare (a : t) (b : t) : int =
  match (a, b) with
  | True, True | False, False | Unit, Unit | Nothing, Nothing -> 0
  | False, True -> -1
  | True, False -> 1
  | Int a, Int b -> Int.compare a b
  | Real a, Real b -> Float.compare a b
  | Str a, Str b -> String.compare a b
  | Num a, Num b -> Num.compare a b
  | List a, List b -> List.compare compare a b
  | App (`Op op1, vs1), App (`Op op2, vs2) ->
    let c = String.compare op1 op2 in
    if c = 0 then List.compare compare vs1 vs2 else c
  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | List _ | App _
      | Nothing )
    , _ ) ->
    (* TODO: I don't know if this is always semantically correct *)
    Int.compare (discr a) (discr b)

let rec equal (v1 : t) (v2 : t) : bool =
  match (v1, v2) with
  | True, True | False, False | Unit, Unit | Nothing, Nothing -> true
  | Int a, Int b -> Int.equal a b
  | Real a, Real b -> Float.equal a b
  | Str a, Str b -> String.equal a b
  | Num a, Num b -> Num.equal a b
  | List l1, List l2 -> List.equal equal l1 l2
  | App (`Op op1, vs1), App (`Op op2, vs2) ->
    String.equal op1 op2 && List.equal equal vs1 vs2
  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | List _ | App _
      | Nothing )
    , _ ) ->
    false

let map v f = match v with Nothing -> Nothing | _ -> f v

let ( let+ ) = map

let rec pp fmt = function
  | True -> Fmt.string fmt "true"
  | False -> Fmt.string fmt "false"
  | Unit -> Fmt.string fmt "unit"
  | Int x -> Fmt.int fmt x
  | Real x -> Fmt.pf fmt "%F" x
  | Num x -> Num.pp_no_type fmt x
  | Str x -> Fmt.pf fmt "%S" x
  | List l -> (Fmt.hovbox ~indent:1 (Fmt.list ~sep:Fmt.comma pp)) fmt l
  | App (`Op op, vs) ->
    Fmt.pf fmt "@[<hov 1>%s(%a)@]" op (Fmt.list ~sep:Fmt.comma pp) vs
  | Nothing -> Fmt.string fmt "none"
  | App _ -> assert false

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

let of_string (cast : Ty.t) v =
  let open Result in
  match cast with
  | Ty_bitv _ | Ty_fp _ ->
    let+ n = Num.of_string cast v in
    Num n
  | Ty_bool -> (
    match v with
    | "true" -> Ok True
    | "false" -> Ok False
    | _ -> Fmt.error_msg "invalid value %s, expected boolean" v )
  | Ty_int -> (
    match int_of_string_opt v with
    | None -> Fmt.error_msg "invalid value %s, expected integer" v
    | Some n -> Ok (Int n) )
  | Ty_real -> (
    match float_of_string_opt v with
    | None -> Fmt.error_msg "invalid value %s, expected real" v
    | Some n -> Ok (Real n) )
  | Ty_str -> Ok (Str v)
  | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp ->
    Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast

let rec to_json (v : t) : Yojson.Basic.t =
  match v with
  | True -> `Bool true
  | False -> `Bool false
  | Unit -> `String "unit"
  | Int int -> `Int int
  | Real real -> `Float real
  | Str str -> `String str
  | Num n -> Num.to_json n
  | List l -> `List (List.map to_json l)
  | Nothing -> `Null
  | App _ -> assert false

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	open Ty
6
7	type t =
8	\| True
9	\| False
10	\| Unit
11	\| Int of int
12	\| Real of float
13	\| Str of string
14	\| Num of Num.t
15	\| List of t list
16	\| App : [> `Op of string ] * t list -> t
17	\| Nothing
18
19	let type_of (v : t) : Ty.t =
20	match v with	316✔
21	\| True \| False -> Ty_bool	6✔
22	\| Unit -> Ty_unit	×
23	\| Int _ -> Ty_int	51✔
24	\| Real _ -> Ty_real	31✔
25	\| Str _ -> Ty_str	40✔
26	\| Num n -> Num.type_of n	170✔
27	\| List _ -> Ty_list	9✔
28	\| App _ -> Ty_app	×
29	\| Nothing -> Ty_none	×
30
31	let discr = function
32	\| True -> 0	×
33	\| False -> 1	×
34	\| Unit -> 2	×
35	\| Int _ -> 3	×
36	\| Real _ -> 4	×
37	\| Str _ -> 5	×
38	\| Num _ -> 6	×
39	\| List _ -> 7	×
40	\| App _ -> 8	×
41	\| Nothing -> 9	×
42
43	let rec compare (a : t) (b : t) : int =
44	match (a, b) with	×
45	\| True, True \| False, False \| Unit, Unit \| Nothing, Nothing -> 0	×
46	\| False, True -> -1	×
47	\| True, False -> 1	×
48	\| Int a, Int b -> Int.compare a b	×
49	\| Real a, Real b -> Float.compare a b	×
50	\| Str a, Str b -> String.compare a b	×
51	\| Num a, Num b -> Num.compare a b	×
52	\| List a, List b -> List.compare compare a b	×
53	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	×
54	let c = String.compare op1 op2 in
55	if c = 0 then List.compare compare vs1 vs2 else c	×
56	\| ( ( True \| False \| Unit \| Int _ \| Real _ \| Str _ \| Num _ \| List _ \| App _	×
57	\| Nothing )	×
58	, _ ) ->
59	(* TODO: I don't know if this is always semantically correct *)
60	Int.compare (discr a) (discr b)	×
61
62	let rec equal (v1 : t) (v2 : t) : bool =
63	match (v1, v2) with	582✔
64	\| True, True \| False, False \| Unit, Unit \| Nothing, Nothing -> true	×
65	\| Int a, Int b -> Int.equal a b	142✔
66	\| Real a, Real b -> Float.equal a b	61✔
67	\| Str a, Str b -> String.equal a b	49✔
68	\| Num a, Num b -> Num.equal a b	235✔
69	\| List l1, List l2 -> List.equal equal l1 l2	7✔
70	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	7✔
71	String.equal op1 op2 && List.equal equal vs1 vs2	7✔
72	\| ( ( True \| False \| Unit \| Int _ \| Real _ \| Str _ \| Num _ \| List _ \| App _	×
73	\| Nothing )	×
74	, _ ) ->
75	false
76
77	let map v f = match v with Nothing -> Nothing \| _ -> f v	×
78
79	let ( let+ ) = map
80
81	let rec pp fmt = function
82	\| True -> Fmt.string fmt "true"	×
83	\| False -> Fmt.string fmt "false"	×
84	\| Unit -> Fmt.string fmt "unit"	×
85	\| Int x -> Fmt.int fmt x	×
86	\| Real x -> Fmt.pf fmt "%F" x	×
87	\| Num x -> Num.pp_no_type fmt x	×
88	\| Str x -> Fmt.pf fmt "%S" x	×
89	\| List l -> (Fmt.hovbox ~indent:1 (Fmt.list ~sep:Fmt.comma pp)) fmt l	×
90	\| App (`Op op, vs) ->	×
91	Fmt.pf fmt "@[<hov 1>%s(%a)@]" op (Fmt.list ~sep:Fmt.comma pp) vs	×
92	\| Nothing -> Fmt.string fmt "none"	×
93	\| App _ -> assert false
94
95	let to_string (v : t) : string = Fmt.str "%a" pp v	×
96
97	let of_string (cast : Ty.t) v =
98	let open Result in	11✔
99	match cast with
100	\| Ty_bitv _ \| Ty_fp _ ->	3✔
101	let+ n = Num.of_string cast v in	7✔
102	Num n	7✔
103	\| Ty_bool -> (	2✔
104	match v with
105	\| "true" -> Ok True	2✔
106	\| "false" -> Ok False	×
107	\| _ -> Fmt.error_msg "invalid value %s, expected boolean" v )	×
108	\| Ty_int -> (	2✔
109	match int_of_string_opt v with
110	\| None -> Fmt.error_msg "invalid value %s, expected integer" v	×
111	\| Some n -> Ok (Int n) )	2✔
112	\| Ty_real -> (	×
113	match float_of_string_opt v with
114	\| None -> Fmt.error_msg "invalid value %s, expected real" v	×
115	\| Some n -> Ok (Real n) )	×
116	\| Ty_str -> Ok (Str v)	×
117	\| Ty_app \| Ty_list \| Ty_none \| Ty_unit \| Ty_regexp ->	×
118	Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast
119
120	let rec to_json (v : t) : Yojson.Basic.t =
121	match v with	7✔
122	\| True -> `Bool true	1✔
123	\| False -> `Bool false	×
124	\| Unit -> `String "unit"	×
125	\| Int int -> `Int int	1✔
126	\| Real real -> `Float real	1✔
127	\| Str str -> `String str	1✔
128	\| Num n -> Num.to_json n	3✔
129	\| List l -> `List (List.map to_json l)	×
130	\| Nothing -> `Null	×
131	\| App _ -> assert false

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