formalsec / smtml / 175

Committed 12 Jul 2024 09:10AM UTC coverage: 50.585% (+1.4%) from 49.176%

Build # 175

Build Type

push

github

Committed by

filipeom

Commit Message

Test relop simplification

Run Details

1125 of 2224 relevant lines covered (50.58%)

22.03 hits per line

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

37.5

/lib/model.ml

(***************************************************************************)
(* This file is part of the third-party OCaml library `smtml`.             *)
(* Copyright (C) 2023-2024 formalsec                                       *)
(*                                                                         *)
(* This program is free software: you can redistribute it and/or modify    *)
(* it under the terms of the GNU General Public License as published by    *)
(* the Free Software Foundation, either version 3 of the License, or       *)
(* (at your option) any later version.                                     *)
(*                                                                         *)
(* This program is distributed in the hope that it will be useful,         *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           *)
(* GNU General Public License for more details.                            *)
(*                                                                         *)
(* You should have received a copy of the GNU General Public License       *)
(* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
(***************************************************************************)

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 =
  Format.pp_print_list
    ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
    (fun fmt (key, data) ->
      if not no_values then
        Format.fprintf fmt "(%a %a)" Symbol.pp key Value.pp data
      else
        let t = Symbol.type_of key in
        Format.fprintf fmt "(%a %a)" Symbol.pp key Ty.pp t )
    fmt (get_bindings model)

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

let to_string (model : t) : string =
  Format.asprintf "%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) ]
      | _ -> 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) ]

1	(***************************************************************************)
2	(* This file is part of the third-party OCaml library `smtml`. *)
3	(* Copyright (C) 2023-2024 formalsec *)
4	(* *)
5	(* This program is free software: you can redistribute it and/or modify *)
6	(* it under the terms of the GNU General Public License as published by *)
7	(* the Free Software Foundation, either version 3 of the License, or *)
8	(* (at your option) any later version. *)
9	(* *)
10	(* This program is distributed in the hope that it will be useful, *)
11	(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
12	(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
13	(* GNU General Public License for more details. *)
14	(* *)
15	(* You should have received a copy of the GNU General Public License *)
16	(* along with this program. If not, see <https://www.gnu.org/licenses/>. *)
17	(***************************************************************************)
18
19	type t = (Symbol.t, Value.t) Hashtbl.t
20
21	let iter f model = Hashtbl.iter (fun a b -> f (a, b)) model	×
22
23	let get_symbols (model : t) : Symbol.t List.t =
24	Hashtbl.to_seq_keys model \|> List.of_seq \|> List.sort Symbol.compare	×
25
26	let compare_bindings (s1, v1) (s2, v2) =
27	let compare_symbol = Symbol.compare s1 s2 in	21✔
28	if compare_symbol = 0 then Value.compare v1 v2 else compare_symbol	×
29
30	let get_bindings (model : t) : (Symbol.t * Value.t) list =
31	Hashtbl.to_seq model \|> List.of_seq \|> List.sort compare_bindings	7✔
32
33	let evaluate (model : t) (symb : Symbol.t) : Value.t option =
34	Hashtbl.find_opt model symb	2✔
35
36	let pp_bindings fmt ?(no_values = false) model =	×
37	Format.pp_print_list	7✔
38	~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")	15✔
39	(fun fmt (key, data) ->
40	if not no_values then	22✔
41	Format.fprintf fmt "(%a %a)" Symbol.pp key Value.pp data	22✔
42	else
43	let t = Symbol.type_of key in	×
44	Format.fprintf fmt "(%a %a)" Symbol.pp key Ty.pp t )	×
45	fmt (get_bindings model)	7✔
46
47	let pp fmt ?(no_values = false) model =	×
48	Format.fprintf fmt "(model@\n @[<v>%a@])" (pp_bindings ~no_values) model	7✔
49
50	let to_string (model : t) : string =
51	Format.asprintf "%a" (pp ~no_values:false) model	×
52
53	let to_json (model : t) : Yojson.t =
54	let combine = Yojson.Basic.Util.combine in	×
55	let add_assignment sym value assignments =
56	let assignment =	×
57	match Symbol.to_json sym with
58	\| `Assoc [ (name, props) ] ->	×
59	let value = `Assoc [ ("value", Value.to_json value) ] in	×
60	`Assoc [ (name, combine props value) ]	×
61	\| _ -> failwith "Model: Symbol.to_json returned something impossible"	×
62	in
63	combine assignments assignment
64	in
65	let model :> Yojson.t = Hashtbl.fold add_assignment model (`Assoc []) in	×
66	`Assoc [ ("model", model) ]

formalsec / smtml / 175

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