formalsec / smtml / 444

Committed 15 Dec 2025 12:17PM UTC coverage: 45.031% (-0.3%) from 45.286%

Build # 444

Build Type

push

github

Committed by

filipeom

Commit Message

Add function `Value.default_of_type` (#483)

Closes #483

Run Details

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

879 of 1952 relevant lines covered (45.03%)

7.41 hits per line

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

26.61

/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
  | Bitv of Bitvector.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
  | Bitv bv -> Ty_bitv (Bitvector.numbits bv)
  | 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
  | Bitv _ -> 7
  | List _ -> 8
  | App _ -> 9
  | Nothing -> 10

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
  | Bitv a, Bitv b -> Bitvector.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 _ | Bitv _ | 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
  | Bitv a, Bitv b -> Bitvector.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 _ | Bitv _ | List _
      | App _ | Nothing )
    , _ ) ->
    false

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

let ( let+ ) = map

let default_of_type = function
  | Ty.Ty_bool -> False
  | Ty_int -> Int 0
  | Ty_real -> Real 0.0
  | Ty_str -> Str ""
  | Ty_bitv m -> Bitv (Bitvector.make Z.zero m)
  | Ty_fp 32 -> Num (F32 0l)
  | Ty_fp 64 -> Num (F64 0L)
  | Ty_list -> List []
  | Ty_unit -> Unit
  | Ty_none -> Nothing
  | (Ty_fp _ | Ty_app | Ty_regexp | Ty_roundingMode) as ty ->
    Fmt.failwith "No default value for type %a" Ty.pp ty

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 fmt x
  | Bitv bv -> Bitvector.pp fmt bv
  | 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 m -> Ok (Bitv (Bitvector.make (Z.of_string v) m))
  | 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 | Ty_roundingMode ->
    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
  | Bitv bv -> Bitvector.to_json bv
  | List l -> `List (List.map to_json l)
  | Nothing -> `Null
  | App _ -> assert false

module Smtlib = struct
  let pp fmt = function
    | True -> Fmt.string fmt "true"
    | False -> Fmt.string fmt "false"
    | Int x -> Fmt.int fmt x
    | Real x -> Fmt.pf fmt "%F" x
    | Num x -> Num.pp fmt x
    | Bitv bv -> Bitvector.pp fmt bv
    | Str x -> Fmt.pf fmt "%S" x
    | Unit -> assert false
    | List _ -> assert false
    | App _ -> assert false
    | Nothing -> assert false
end

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	\| Bitv of Bitvector.t
16	\| List of t list
17	\| App : [> `Op of string ] * t list -> t
18	\| Nothing
19
20	let type_of (v : t) : Ty.t =
21	match v with	6✔
22	\| True \| False -> Ty_bool	×
23	\| Unit -> Ty_unit	×
24	\| Int _ -> Ty_int	1✔
25	\| Real _ -> Ty_real	×
26	\| Str _ -> Ty_str	5✔
27	\| Num n -> Num.type_of n	×
28	\| Bitv bv -> Ty_bitv (Bitvector.numbits bv)	×
29	\| List _ -> Ty_list	×
30	\| App _ -> Ty_app	×
31	\| Nothing -> Ty_none	×
32
33	let discr = function
34	\| True -> 0	×
35	\| False -> 1	×
36	\| Unit -> 2	×
37	\| Int _ -> 3	×
38	\| Real _ -> 4	×
39	\| Str _ -> 5	×
40	\| Num _ -> 6	×
41	\| Bitv _ -> 7	×
42	\| List _ -> 8	×
43	\| App _ -> 9	×
44	\| Nothing -> 10	×
45
46	let rec compare (a : t) (b : t) : int =
47	match (a, b) with	×
48	\| True, True \| False, False \| Unit, Unit \| Nothing, Nothing -> 0	×
49	\| False, True -> -1	×
50	\| True, False -> 1	×
51	\| Int a, Int b -> Int.compare a b	×
52	\| Real a, Real b -> Float.compare a b	×
53	\| Str a, Str b -> String.compare a b	×
54	\| Num a, Num b -> Num.compare a b	×
55	\| Bitv a, Bitv b -> Bitvector.compare a b	×
56	\| List a, List b -> List.compare compare a b	×
57	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	×
58	let c = String.compare op1 op2 in
59	if c = 0 then List.compare compare vs1 vs2 else c	×
60	\| ( ( True \| False \| Unit \| Int _ \| Real _ \| Str _ \| Num _ \| Bitv _ \| List _	×
61	\| App _ \| Nothing )	×
62	, _ ) ->
63	(* TODO: I don't know if this is always semantically correct *)
64	Int.compare (discr a) (discr b)	×
65
66	let rec equal (v1 : t) (v2 : t) : bool =
67	match (v1, v2) with	654✔
68	\| True, True \| False, False \| Unit, Unit \| Nothing, Nothing -> true	×
69	\| Int a, Int b -> Int.equal a b	140✔
70	\| Real a, Real b -> Float.equal a b	67✔
71	\| Str a, Str b -> String.equal a b	49✔
72	\| Num a, Num b -> Num.equal a b	98✔
73	\| Bitv a, Bitv b -> Bitvector.equal a b	179✔
74	\| List l1, List l2 -> List.equal equal l1 l2	6✔
75	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	5✔
76	String.equal op1 op2 && List.equal equal vs1 vs2	5✔
77	\| ( ( True \| False \| Unit \| Int _ \| Real _ \| Str _ \| Num _ \| Bitv _ \| List _	×
78	\| App _ \| Nothing )	×
79	, _ ) ->
80	false
81
82	let map v f = match v with Nothing -> Nothing \| _ -> f v	×
83
84	let ( let+ ) = map
85
86	let default_of_type = function
NEW 87	\| Ty.Ty_bool -> False	×
NEW 88	\| Ty_int -> Int 0	×
NEW 89	\| Ty_real -> Real 0.0	×
NEW 90	\| Ty_str -> Str ""	×
NEW 91	\| Ty_bitv m -> Bitv (Bitvector.make Z.zero m)	×
NEW 92	\| Ty_fp 32 -> Num (F32 0l)	×
NEW 93	\| Ty_fp 64 -> Num (F64 0L)	×
NEW 94	\| Ty_list -> List []	×
NEW 95	\| Ty_unit -> Unit	×
NEW 96	\| Ty_none -> Nothing	×
NEW 97	\| (Ty_fp _ \| Ty_app \| Ty_regexp \| Ty_roundingMode) as ty ->	×
98	Fmt.failwith "No default value for type %a" Ty.pp ty
99
100	let rec pp fmt = function
101	\| True -> Fmt.string fmt "true"	×
102	\| False -> Fmt.string fmt "false"	×
103	\| Unit -> Fmt.string fmt "unit"	×
104	\| Int x -> Fmt.int fmt x	×
105	\| Real x -> Fmt.pf fmt "%F" x	×
106	\| Num x -> Num.pp fmt x	×
107	\| Bitv bv -> Bitvector.pp fmt bv	×
108	\| Str x -> Fmt.pf fmt "%S" x	×
109	\| List l -> (Fmt.hovbox ~indent:1 (Fmt.list ~sep:Fmt.comma pp)) fmt l	×
110	\| App (`Op op, vs) ->	×
111	Fmt.pf fmt "@[<hov 1>%s(%a)@]" op (Fmt.list ~sep:Fmt.comma pp) vs	×
112	\| Nothing -> Fmt.string fmt "none"	×
113	\| App _ -> assert false
114
115	let to_string (v : t) : string = Fmt.str "%a" pp v	×
116
117	let of_string (cast : Ty.t) v =
118	let open Result in	11✔
119	match cast with
120	\| Ty_bitv m -> Ok (Bitv (Bitvector.make (Z.of_string v) m))	4✔
121	\| Ty_fp _ ->	3✔
122	let+ n = Num.of_string cast v in	3✔
123	Num n	3✔
124	\| Ty_bool -> (	2✔
125	match v with
126	\| "true" -> Ok True	2✔
127	\| "false" -> Ok False	×
128	\| _ -> Fmt.error_msg "invalid value %s, expected boolean" v )	×
129	\| Ty_int -> (	2✔
130	match int_of_string_opt v with
131	\| None -> Fmt.error_msg "invalid value %s, expected integer" v	×
132	\| Some n -> Ok (Int n) )	2✔
133	\| Ty_real -> (	×
134	match float_of_string_opt v with
135	\| None -> Fmt.error_msg "invalid value %s, expected real" v	×
136	\| Some n -> Ok (Real n) )	×
137	\| Ty_str -> Ok (Str v)	×
138	\| Ty_app \| Ty_list \| Ty_none \| Ty_unit \| Ty_regexp \| Ty_roundingMode ->	×
139	Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast
140
141	let rec to_json (v : t) : Yojson.Basic.t =
142	match v with	7✔
143	\| True -> `Bool true	1✔
144	\| False -> `Bool false	×
145	\| Unit -> `String "unit"	×
146	\| Int int -> `Int int	1✔
147	\| Real real -> `Float real	1✔
148	\| Str str -> `String str	1✔
149	\| Num n -> Num.to_json n	1✔
150	\| Bitv bv -> Bitvector.to_json bv	2✔
151	\| List l -> `List (List.map to_json l)	×
152	\| Nothing -> `Null	×
153	\| App _ -> assert false
154
155	module Smtlib = struct
156	let pp fmt = function
157	\| True -> Fmt.string fmt "true"	×
158	\| False -> Fmt.string fmt "false"	×
159	\| Int x -> Fmt.int fmt x	3✔
160	\| Real x -> Fmt.pf fmt "%F" x	×
161	\| Num x -> Num.pp fmt x	×
162	\| Bitv bv -> Bitvector.pp fmt bv	×
163	\| Str x -> Fmt.pf fmt "%S" x	×
164	\| Unit -> assert false
165	\| List _ -> assert false
166	\| App _ -> assert false
167	\| Nothing -> assert false
168	end

formalsec / smtml / 444

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