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

49.38

/src/smtml/model.ml

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

type t = (Symbol.t, Value.t) Hashtbl.t

let iter f model = Hashtbl.iter (fun a b -> f (a, b)) model

let get_symbols (model : t) : Symbol.t List.t =
  Hashtbl.to_seq_keys model |> List.of_seq |> List.sort Symbol.compare

let compare_bindings (s1, v1) (s2, v2) =
  let compare_symbol = Symbol.compare s1 s2 in
  if compare_symbol = 0 then Value.compare v1 v2 else compare_symbol

let get_bindings (model : t) : (Symbol.t * Value.t) list =
  Hashtbl.to_seq model |> List.of_seq |> List.sort compare_bindings

let evaluate (model : t) (symb : Symbol.t) : Value.t option =
  Hashtbl.find_opt model symb

let pp_bindings fmt ?(no_values = false) model =
  Fmt.list
    ~sep:(fun fmt () -> Fmt.pf fmt "@\n")
    (fun fmt (key, data) ->
      let t = Symbol.type_of key in
      if not no_values then
        Fmt.pf fmt "(%a %a %a)" Symbol.pp key Ty.pp t Value.pp data
      else Fmt.pf fmt "(%a %a)" Symbol.pp key Ty.pp t )
    fmt (get_bindings model)

let pp ?(no_values = false) fmt model =
  Fmt.pf fmt "(model@\n  @[<v>%a@])" (pp_bindings ~no_values) model

let to_string (model : t) : string = Fmt.str "%a" (pp ~no_values:false) model

let to_json (model : t) : Yojson.t =
  let combine = Yojson.Basic.Util.combine in
  let add_assignment sym value assignments =
    let assignment =
      match Symbol.to_json sym with
      | `Assoc [ (name, props) ] ->
        let value = `Assoc [ ("value", Value.to_json value) ] in
        `Assoc [ (name, combine props value) ]
      | _ -> Fmt.failwith "Model: Symbol.to_json returned something impossible"
    in
    combine assignments assignment
  in
  let model :> Yojson.t = Hashtbl.fold add_assignment model (`Assoc []) in
  `Assoc [ ("model", model) ]

(** {b Example}: Model in the json format:

    {@json[
      {
        "model" : {
          "x_0" : { "ty" : "int", "value" : 42 },
          "x_1" : { "ty" : "bool", "value" : true },
          "x_2" : { "ty" : "f32", "value" : 42.42 }
        }
      }
    ]} *)
let to_json_string model =
  let model = to_json model in
  Fmt.str "%a" (Yojson.pretty_print ~std:true) model

let to_scfg ~no_value model =
  let open Scfg.Types in
  let children =
    let bindings = get_bindings model in
    List.map
      (fun (symbol, value) ->
        let p0 = Symbol.to_string symbol in
        let p1 = Symbol.type_of symbol |> Ty.string_of_type in
        let params =
          if no_value then [ p0; p1 ]
          else
            let p2 = Value.to_string value in
            [ p0; p1; p2 ]
        in
        { name = "symbol"; params; children = [] } )
      bindings
  in
  [ { name = "model"; params = []; children } ]

(** {b Example}: Model in the scfg format:

    {@scfg[
      model {
        symbol x_0 int 42
        symbol x_1 bool true
        symbol x_2 f32 42.42
      }
    ]} *)
let to_scfg_string ~no_value model =
  let model = to_scfg ~no_value model in
  Fmt.str "%a" Scfg.Pp.config model

let to_smtlib _model = assert false

(** {b Example}: TODO *)
let to_smtlib_string model =
  let _model = to_smtlib model in
  assert false

module Parse = struct
  module Json = struct
    open Result
    module Json = Yojson.Basic

    let from_json json =
      let symbols = Json.Util.member "model" json |> Json.Util.to_assoc in
      let tbl = Hashtbl.create 16 in
      let* () =
        Result.list_iter
          (fun (symbol, json) ->
            let ty = Json.Util.member "ty" json |> Json.Util.to_string in
            let* ty = Ty.of_string ty in
            let value =
              (* FIXME: this is a bit hackish in order to reuse the previous code *)
              match Json.Util.member "value" json with
              | `Bool x -> Bool.to_string x
              | `Float x -> Float.to_string x
              | `Int x -> Int.to_string x
              | `String x -> x
              | _ -> assert false
            in
            let+ value = Value.of_string ty value in
            let key = Symbol.make ty symbol in
            Hashtbl.add tbl key value )
          symbols
      in
      Ok tbl

    let from_string s = Json.from_string s |> from_json

    let from_channel chan = Json.from_channel chan |> from_json

    let from_file file =
      let file = Fpath.to_string file in
      Json.from_file ~fname:file file |> from_json
  end

  module Scfg = struct
    open Result

    let from_scfg v =
      match Scfg.Query.get_dir "model" v with
      | None ->
        Fmt.error_msg
          "can not find the directive `model` while parsing the scfg config"
      | Some model ->
        let symbols = Scfg.Query.get_dirs "symbol" model.children in
        let tbl = Hashtbl.create 16 in
        let* () =
          Result.list_iter
            (fun symbol ->
              let* name = Scfg.Query.get_param 0 symbol in
              let* ty = Scfg.Query.get_param 1 symbol in
              let* ty = Ty.of_string ty in
              let* value = Scfg.Query.get_param 2 symbol in
              let+ value = Value.of_string ty value in
              let key = Symbol.make ty name in
              Hashtbl.add tbl key value )
            symbols
        in
        Ok tbl

    let from_string s =
      let* model = Scfg.Parse.from_string s in
      from_scfg model

    let from_channel chan =
      let* model = Scfg.Parse.from_channel chan in
      from_scfg model

    let from_file file =
      let* model = Scfg.Parse.from_file file in
      from_scfg model
  end

  module Smtlib = struct
    let from_string _s = assert false

    let from_channel _chan = assert false

    let from_file _file = assert false
  end
end

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	type t = (Symbol.t, Value.t) Hashtbl.t
6
7	let iter f model = Hashtbl.iter (fun a b -> f (a, b)) model	×
8
9	let get_symbols (model : t) : Symbol.t List.t =
10	Hashtbl.to_seq_keys model \|> List.of_seq \|> List.sort Symbol.compare	×
11
12	let compare_bindings (s1, v1) (s2, v2) =
13	let compare_symbol = Symbol.compare s1 s2 in	×
14	if compare_symbol = 0 then Value.compare v1 v2 else compare_symbol	×
15
16	let get_bindings (model : t) : (Symbol.t * Value.t) list =
17	Hashtbl.to_seq model \|> List.of_seq \|> List.sort compare_bindings	×
18
19	let evaluate (model : t) (symb : Symbol.t) : Value.t option =
20	Hashtbl.find_opt model symb	3✔
21
22	let pp_bindings fmt ?(no_values = false) model =	×
23	Fmt.list	×
24	~sep:(fun fmt () -> Fmt.pf fmt "@\n")	×
25	(fun fmt (key, data) ->
26	let t = Symbol.type_of key in	×
27	if not no_values then	×
28	Fmt.pf fmt "(%a %a %a)" Symbol.pp key Ty.pp t Value.pp data	×
29	else Fmt.pf fmt "(%a %a)" Symbol.pp key Ty.pp t )	×
30	fmt (get_bindings model)	×
31
32	let pp ?(no_values = false) fmt model =	×
33	Fmt.pf fmt "(model@\n @[<v>%a@])" (pp_bindings ~no_values) model	×
34
35	let to_string (model : t) : string = Fmt.str "%a" (pp ~no_values:false) model	×
36
37	let to_json (model : t) : Yojson.t =
38	let combine = Yojson.Basic.Util.combine in	2✔
39	let add_assignment sym value assignments =
40	let assignment =	7✔
41	match Symbol.to_json sym with
42	\| `Assoc [ (name, props) ] ->	7✔
43	let value = `Assoc [ ("value", Value.to_json value) ] in	7✔
44	`Assoc [ (name, combine props value) ]	7✔
45	\| _ -> Fmt.failwith "Model: Symbol.to_json returned something impossible"	×
46	in
47	combine assignments assignment
48	in
49	let model :> Yojson.t = Hashtbl.fold add_assignment model (`Assoc []) in	2✔
50	`Assoc [ ("model", model) ]
51
52	(** {b Example}: Model in the json format:
53
54	{@json[
55	{
56	"model" : {
57	"x_0" : { "ty" : "int", "value" : 42 },
58	"x_1" : { "ty" : "bool", "value" : true },
59	"x_2" : { "ty" : "f32", "value" : 42.42 }
60	}
61	}
62	]} *)
63	let to_json_string model =
64	let model = to_json model in	1✔
65	Fmt.str "%a" (Yojson.pretty_print ~std:true) model	1✔
66
67	let to_scfg ~no_value model =
68	let open Scfg.Types in	×
69	let children =
70	let bindings = get_bindings model in
71	List.map	×
72	(fun (symbol, value) ->
73	let p0 = Symbol.to_string symbol in	×
74	let p1 = Symbol.type_of symbol \|> Ty.string_of_type in	×
75	let params =	×
76	if no_value then [ p0; p1 ]	×
77	else
78	let p2 = Value.to_string value in	×
79	[ p0; p1; p2 ]	×
80	in
81	{ name = "symbol"; params; children = [] } )
82	bindings
83	in
84	[ { name = "model"; params = []; children } ]
85
86	(** {b Example}: Model in the scfg format:
87
88	{@scfg[
89	model {
90	symbol x_0 int 42
91	symbol x_1 bool true
92	symbol x_2 f32 42.42
93	}
94	]} *)
95	let to_scfg_string ~no_value model =
96	let model = to_scfg ~no_value model in	×
97	Fmt.str "%a" Scfg.Pp.config model	×
98
99	let to_smtlib _model = assert false	×
100
101	(** {b Example}: TODO *)
102	let to_smtlib_string model =
103	let _model = to_smtlib model in	×
104	assert false	×
105
106	module Parse = struct
107	module Json = struct
108	open Result
109	module Json = Yojson.Basic
110
111	let from_json json =
112	let symbols = Json.Util.member "model" json \|> Json.Util.to_assoc in	2✔
113	let tbl = Hashtbl.create 16 in	2✔
114	let* () =	2✔
115	Result.list_iter	2✔
116	(fun (symbol, json) ->
117	let ty = Json.Util.member "ty" json \|> Json.Util.to_string in	7✔
118	let* ty = Ty.of_string ty in	7✔
119	let value =	7✔
120	(* FIXME: this is a bit hackish in order to reuse the previous code *)
121	match Json.Util.member "value" json with
122	\| `Bool x -> Bool.to_string x	1✔
123	\| `Float x -> Float.to_string x	1✔
124	\| `Int x -> Int.to_string x	2✔
125	\| `String x -> x	3✔
126	\| _ -> assert false
127	in
128	let+ value = Value.of_string ty value in	7✔
129	let key = Symbol.make ty symbol in	7✔
130	Hashtbl.add tbl key value )	7✔
131	symbols
132	in
133	Ok tbl	2✔
134
135	let from_string s = Json.from_string s \|> from_json	2✔
136
137	let from_channel chan = Json.from_channel chan \|> from_json	×
138
139	let from_file file =
140	let file = Fpath.to_string file in	×
141	Json.from_file ~fname:file file \|> from_json	×
142	end
143
144	module Scfg = struct
145	open Result
146
147	let from_scfg v =
148	match Scfg.Query.get_dir "model" v with	1✔
149	\| None ->	×
150	Fmt.error_msg
151	"can not find the directive `model` while parsing the scfg config"
152	\| Some model ->	1✔
153	let symbols = Scfg.Query.get_dirs "symbol" model.children in
154	let tbl = Hashtbl.create 16 in	1✔
155	let* () =	1✔
156	Result.list_iter	1✔
157	(fun symbol ->
158	let* name = Scfg.Query.get_param 0 symbol in	4✔
159	let* ty = Scfg.Query.get_param 1 symbol in	4✔
160	let* ty = Ty.of_string ty in	4✔
161	let* value = Scfg.Query.get_param 2 symbol in	4✔
162	let+ value = Value.of_string ty value in	4✔
163	let key = Symbol.make ty name in	4✔
164	Hashtbl.add tbl key value )	4✔
165	symbols
166	in
167	Ok tbl	1✔
168
169	let from_string s =
170	let* model = Scfg.Parse.from_string s in	1✔
171	from_scfg model	1✔
172
173	let from_channel chan =
174	let* model = Scfg.Parse.from_channel chan in	×
175	from_scfg model	×
176
177	let from_file file =
178	let* model = Scfg.Parse.from_file file in	×
179	from_scfg model	×
180	end
181
182	module Smtlib = struct
183	let from_string _s = assert false	×
184
185	let from_channel _chan = assert false	×
186
187	let from_file _file = assert false	×
188	end
189	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