From e55d9964ce9ce0d2310724a1a8f16daf60a0c7b6 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Thu, 4 Sep 2025 20:23:09 +0100 Subject: [PATCH 01/22] more doc Signed-off-by: Sacha Ayoun --- soteria/lib/logs/logs.mli | 3 +++ 1 file changed, 3 insertions(+) diff --git a/soteria/lib/logs/logs.mli b/soteria/lib/logs/logs.mli index cd7d0a896..602a9a109 100644 --- a/soteria/lib/logs/logs.mli +++ b/soteria/lib/logs/logs.mli @@ -49,6 +49,9 @@ module Cli : sig val term : (Config.t, string) result Cmdliner.Term.t end +(** [L] is the module that contains all the fonctions to actually log stuff. One + can access it using [Soteria.Logs.L] or by [open Soteria.Logs.Import] and + then using [L] directly. *) module L : sig (** [with_section ~is_branch name f] runs [f] and aggregates its log messages within a collapsible section of the log file (when logs are in HTML mode). From 0862a8a858387959a92ef4e917bcd2bfe85f07a1 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Fri, 5 Sep 2025 18:19:54 +0100 Subject: [PATCH 02/22] doc --- soteria/lib/sym_states/sym_states.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 soteria/lib/sym_states/sym_states.ml diff --git a/soteria/lib/sym_states/sym_states.ml b/soteria/lib/sym_states/sym_states.ml new file mode 100644 index 000000000..84aa3b30e --- /dev/null +++ b/soteria/lib/sym_states/sym_states.ml @@ -0,0 +1,11 @@ +(** A collection of state monad transformers for building compositional symbolic + execution states. *) + +module Bi_abd = Bi_abd +module Excl = Excl +module Freeable = Freeable +module Plist = Plist +module Pmap = Pmap +module Pure_fun = Pure_fun +module Tree_block = Tree_block +module With_info = With_info From 31b8647b1f4e1644ccb181143808fd69315cb438 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 6 Sep 2025 00:19:02 +0100 Subject: [PATCH 03/22] In progress --- soteria/lib/soteria_std/printable.ml | 6 +++++ soteria/lib/sym_data/s_elt.ml | 25 +++++++++++++++++++ soteria/lib/sym_data/s_eq.ml | 37 ++++++++++++++++++++++++++++ soteria/lib/sym_data/s_map.ml | 26 +++++++++++++++++++ soteria/lib/sym_data/sym_data.ml | 5 ++++ 5 files changed, 99 insertions(+) create mode 100644 soteria/lib/soteria_std/printable.ml create mode 100644 soteria/lib/sym_data/s_elt.ml create mode 100644 soteria/lib/sym_data/s_eq.ml create mode 100644 soteria/lib/sym_data/s_map.ml create mode 100644 soteria/lib/sym_data/sym_data.ml diff --git a/soteria/lib/soteria_std/printable.ml b/soteria/lib/soteria_std/printable.ml new file mode 100644 index 000000000..0329558c1 --- /dev/null +++ b/soteria/lib/soteria_std/printable.ml @@ -0,0 +1,6 @@ +(** Describes a type that can be pretty-printed. *) +module type S = sig + type t + + val pp : Format.formatter -> t -> unit +end diff --git a/soteria/lib/sym_data/s_elt.ml b/soteria/lib/sym_data/s_elt.ml new file mode 100644 index 000000000..bfcc82989 --- /dev/null +++ b/soteria/lib/sym_data/s_elt.ml @@ -0,0 +1,25 @@ +open Symex + +module type S = sig + (** Describes something symbolic, i.e. that contains symbolic variables. *) + + type t + + module Symex : Symex.S + + val subst : (Var.t -> Var.t) -> t -> t + val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars +end + +module Of_concrete + (Symex : Symex.S) + (C : sig + type t + end) = +struct + module Symex = Symex + include C + + let subst _ x = x + let iter_vars _ = fun _ -> () +end diff --git a/soteria/lib/sym_data/s_eq.ml b/soteria/lib/sym_data/s_eq.ml new file mode 100644 index 000000000..d93345cc8 --- /dev/null +++ b/soteria/lib/sym_data/s_eq.ml @@ -0,0 +1,37 @@ +module type S = sig + (** Defines a type that supports symbolic semantic equality. For performance + reasons, such a type most also support {e syntactic} equality, such that + syntactic equality ([equal]) implies semantic equality ([sem_eq]) *) + + (** The symex world in which the type lives. *) + module Symex : Symex.S + + type t + + (** Syntactic equality, should be fast. *) + val equal : t -> t -> bool + + (** Symbolic semantic equality *) + val sem_eq : t -> t -> Symex.Value.sbool Symex.Value.t + + (** Receives a list of {e syntactically different} values and returns a + symbolic boolean corresponding to the fact that these values are also + {e semantically} distinct. *) + val distinct : t list -> Symex.Value.sbool Symex.Value.t +end + +module Of_concrete + (Symex : Symex.S) + (C : sig + type t + + val equal : t -> t -> bool + end) : S with module Symex = Symex and type t = C.t = struct + module Symex = Symex + include C + + let sem_eq x y = Symex.Value.bool (C.equal x y) + + (* Always returns true as the input list should always be syntactically distinct *) + let distinct _ = Symex.Value.bool true +end diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml new file mode 100644 index 000000000..03c5ffa2a --- /dev/null +++ b/soteria/lib/sym_data/s_map.ml @@ -0,0 +1,26 @@ +module Key = struct + module type S = sig + include Stdlib.Map.OrderedType + include S_elt.S with type t := t + include S_eq.S with type t := t and module Symex := Symex + include Soteria_std.Printable.S with type t := t + end + + module Of_concrete + (Symex : Symex.S) + (K : sig + include Soteria_std.Ordered_type.S + + val equal : t -> t -> bool + end) = + struct + include K + include S_elt.Of_concrete (Symex) (K) + include S_eq.Of_concrete (Symex) (K) + end +end + +(* module Make (Symex : Symex.S) (Key : Key.S with module Symex = Symex) = struct + open Symex.Syntax + module Raw_map = Stdlib.Map.Make (Key) +end *) diff --git a/soteria/lib/sym_data/sym_data.ml b/soteria/lib/sym_data/sym_data.ml new file mode 100644 index 000000000..5e031243f --- /dev/null +++ b/soteria/lib/sym_data/sym_data.ml @@ -0,0 +1,5 @@ +(** A collection of symbolic data structures and usefule signatures. *) + +module S_elt = S_elt +module S_eq = S_eq +module S_map = S_map From aa8c50acc28e988f2de61acd49cdb63e4879dfc9 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 7 Sep 2025 10:52:41 +0100 Subject: [PATCH 04/22] Implement symbolic maps --- soteria/lib/sym_data/s_map.ml | 108 +++++++++++++++++++++++++++++---- soteria/lib/sym_states/pmap.ml | 1 - 2 files changed, 97 insertions(+), 12 deletions(-) diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml index 03c5ffa2a..eca1a6bb8 100644 --- a/soteria/lib/sym_data/s_map.ml +++ b/soteria/lib/sym_data/s_map.ml @@ -6,21 +6,107 @@ module Key = struct include Soteria_std.Printable.S with type t := t end - module Of_concrete - (Symex : Symex.S) - (K : sig - include Soteria_std.Ordered_type.S - - val equal : t -> t -> bool - end) = - struct + module Of_concrete (Symex : Symex.S) (K : Soteria_std.Ordered_type.S) = struct include K include S_elt.Of_concrete (Symex) (K) - include S_eq.Of_concrete (Symex) (K) + + include + S_eq.Of_concrete + (Symex) + (struct + include K + + let equal x y = compare x y = 0 + end) end end -(* module Make (Symex : Symex.S) (Key : Key.S with module Symex = Symex) = struct +module type S = sig + module Symex : Symex.S + + type key + + module Raw_map : Stdlib.Map.S with type key = key + + type 'a t = 'a Raw_map.t + + val find_opt : key -> 'a t -> (key * 'a option) Symex.t +end + +module Make (Symex : Symex.S) (Key : Key.S with module Symex = Symex) : + S with type key = Key.t and module Symex = Symex = struct + module Symex = Symex + open Symex.Syntax + module Raw_map = Stdlib.Map.Make (Key) + + type key = Key.t + type 'a t = 'a Raw_map.t + + let find_opt (key : Key.t) (m : 'a t) : (Key.t * 'a option) Symex.t = + let rec find_sym s = + match s () with + | Seq.Nil -> Symex.return (key, None) + | Seq.Cons ((k, v), tl) -> + if%sat Key.sem_eq key k then Symex.return (k, Some v) else find_sym tl + (* TODO: Investigate: if this can be somehow made a tail-call? *) + in + match Raw_map.find_opt key m with + | Some v -> + (* We found it syntactically *) + Symex.return (key, Some v) + | None -> find_sym (Raw_map.to_seq m) +end + +module Make_failfast (Symex : Symex.S) (Key : Key.S with module Symex = Symex) : + S with type key = Key.t and module Symex = Symex = struct + module Symex = Symex open Symex.Syntax module Raw_map = Stdlib.Map.Make (Key) -end *) + + type key = Key.t + type 'a t = 'a Raw_map.t + + let find_opt (key : Key.t) (m : 'a t) : (Key.t * 'a option) Symex.t = + let rec find_sym (fkey, fval) tl = + (* At this point, we know that the element is in the map, so if tl is empty, it has to be first. *) + match tl () with + | Seq.Nil -> Symex.return (fkey, Some fval) + | Seq.Cons ((skey, sval), ttl) -> + if%sat Key.sem_eq key fkey then Symex.return (fkey, Some fval) + else find_sym (skey, sval) ttl + (* TODO: Investigate: if this can be somehow made a tail-call? *) + in + match Raw_map.find_opt key m with + | Some v -> Symex.return (key, Some v) + | None -> ( + let s = Raw_map.to_seq m in + match s () with + | Seq.Nil -> + (* If the map is empty, we know for sure that the key is not in it *) + Symex.return (key, None) + | Seq.Cons (first, tl) -> + let not_in_map = + let all_keys_plus_key = + let all_keys = s |> Seq.map fst |> List.of_seq in + key :: all_keys + in + all_keys_plus_key |> Key.distinct + in + if%sat1 not_in_map then + (* In the case we know all keys are different from [key], we can return immediately *) + Symex.return (key, None) + else find_sym first tl) +end + +module Make_concrete (Symex : Symex.S) (K : Soteria_std.Ordered_type.S) : + S with type key = K.t and module Symex = Symex = struct + module Symex = Symex + module Key = Key.Of_concrete (Symex) (K) + module Raw_map = Stdlib.Map.Make (Key) + + type key = Key.t + type 'a t = 'a Raw_map.t + + let find_opt (key : Key.t) (m : 'a t) = + Symex.return (key, Raw_map.find_opt key m) +end diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml index f833ce34e..ae924e5ad 100644 --- a/soteria/lib/sym_states/pmap.ml +++ b/soteria/lib/sym_states/pmap.ml @@ -160,7 +160,6 @@ module Make (Symex : Symex.S) (Key : KeyS with module Symex = Symex) = struct | (k, v) :: tl -> if%sat Key.sem_eq key k then Symex.return (k, Some v) else find_bindings tl - (* TODO: Investigate: this is not a tailcall, because if%sat is not an if. *) in match M'.find_opt key st with | Some v -> Symex.return (key, Some v) From face434477174cd7545828847a6d4264eac14f06 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Mon, 8 Sep 2025 18:56:20 +0100 Subject: [PATCH 05/22] tinsy bit of doc Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_map.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml index eca1a6bb8..18f39f589 100644 --- a/soteria/lib/sym_data/s_map.ml +++ b/soteria/lib/sym_data/s_map.ml @@ -30,6 +30,13 @@ module type S = sig type 'a t = 'a Raw_map.t + (** [find_opt key map] returns a symbolic computation that yields + - [(key, None)] if there is no key in the map that is semantically equal + to [key] + - [(key', Some v)] if there is a binding in the map for [(key', v)] and + [key'] is semantically equal to [key]. In both cases, the resulting + [key'] can be used to insert or update the map directly without needing + to search for it again. *) val find_opt : key -> 'a t -> (key * 'a option) Symex.t end From 8a3348507d90ef5b5e03efe3c87085ead1b4e027 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Mon, 8 Sep 2025 22:12:45 +0100 Subject: [PATCH 06/22] kill channels.ml Signed-off-by: Sacha Ayoun --- soteria-c/lib/driver.ml | 2 +- soteria/lib/soteria_std/channels.ml | 7 ------- soteria/lib/terminal/diagnostic.ml | 2 +- 3 files changed, 2 insertions(+), 9 deletions(-) delete mode 100644 soteria/lib/soteria_std/channels.ml diff --git a/soteria-c/lib/driver.ml b/soteria-c/lib/driver.ml index 4f6e9fe83..d331ea9d4 100644 --- a/soteria-c/lib/driver.ml +++ b/soteria-c/lib/driver.ml @@ -315,7 +315,7 @@ let dump_summaries results = let pp_summary ~fid ft summary = Fmt.pf ft "@[%a@]" Summary.pp (Summary.analyse ~fid summary) in - let@ oc = Channels.with_out_file file in + let@ oc = Out_channel.with_open_text file in let ft = Format.formatter_of_out_channel oc in List.iter (fun (fid, summaries) -> diff --git a/soteria/lib/soteria_std/channels.ml b/soteria/lib/soteria_std/channels.ml deleted file mode 100644 index b31b16955..000000000 --- a/soteria/lib/soteria_std/channels.ml +++ /dev/null @@ -1,7 +0,0 @@ -let with_out_file file f = - let oc = open_out file in - Fun.protect ~finally:(fun () -> close_out oc) (fun () -> f oc) - -let with_in_file file f = - let ic = open_in file in - Fun.protect ~finally:(fun () -> close_in ic) (fun () -> f ic) diff --git a/soteria/lib/terminal/diagnostic.ml b/soteria/lib/terminal/diagnostic.ml index 01f00baea..caf28628f 100644 --- a/soteria/lib/terminal/diagnostic.ml +++ b/soteria/lib/terminal/diagnostic.ml @@ -35,7 +35,7 @@ let utf8_to_byte_offset str idx = let real_index (file : string) ((line, col) : pos) = let open Syntaxes.FunctionWrap in - let@ ic = Channels.with_in_file file in + let@ ic = In_channel.with_open_text file in let current_index = ref 0 in let current_line = ref 0 in while !current_line <= line do From 587668a5afe1b2b726720aa85f4918aa11282d9e Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 9 Sep 2025 09:38:21 +0100 Subject: [PATCH 07/22] more doc Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_map.ml | 7 ++++--- soteria/tutorial/index.mld | 1 + 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml index 18f39f589..75ce7b46d 100644 --- a/soteria/lib/sym_data/s_map.ml +++ b/soteria/lib/sym_data/s_map.ml @@ -34,9 +34,10 @@ module type S = sig - [(key, None)] if there is no key in the map that is semantically equal to [key] - [(key', Some v)] if there is a binding in the map for [(key', v)] and - [key'] is semantically equal to [key]. In both cases, the resulting - [key'] can be used to insert or update the map directly without needing - to search for it again. *) + [key'] is semantically equal to [key]. + + In both cases, the resulting [key'] can be used to insert or update the + map directly without needing to search for it again. *) val find_opt : key -> 'a t -> (key * 'a option) Symex.t end diff --git a/soteria/tutorial/index.mld b/soteria/tutorial/index.mld index 416c09bca..0d6ddb61d 100644 --- a/soteria/tutorial/index.mld +++ b/soteria/tutorial/index.mld @@ -11,6 +11,7 @@ {!modules: Soteria} {!modules: Soteria.Symex + Soteria.Sym_data Soteria.Sym_states Soteria.Logs Soteria.C_values From 20a8a91aea6c1c62ffe9ba3ec553ec915f29c3ea Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 9 Sep 2025 09:58:31 +0100 Subject: [PATCH 08/22] bits of doc Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_elt.ml | 2 ++ soteria/lib/sym_data/s_eq.ml | 2 ++ soteria/lib/sym_data/s_map.ml | 4 ++++ 3 files changed, 8 insertions(+) diff --git a/soteria/lib/sym_data/s_elt.ml b/soteria/lib/sym_data/s_elt.ml index bfcc82989..c2e338702 100644 --- a/soteria/lib/sym_data/s_elt.ml +++ b/soteria/lib/sym_data/s_elt.ml @@ -1,3 +1,5 @@ +(** Basic operations of symbolic abstractions *) + open Symex module type S = sig diff --git a/soteria/lib/sym_data/s_eq.ml b/soteria/lib/sym_data/s_eq.ml index d93345cc8..26f583481 100644 --- a/soteria/lib/sym_data/s_eq.ml +++ b/soteria/lib/sym_data/s_eq.ml @@ -1,3 +1,5 @@ +(** Symbolic abstractions that support equality *) + module type S = sig (** Defines a type that supports symbolic semantic equality. For performance reasons, such a type most also support {e syntactic} equality, such that diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml index 75ce7b46d..c1ce5cac9 100644 --- a/soteria/lib/sym_data/s_map.ml +++ b/soteria/lib/sym_data/s_map.ml @@ -1,3 +1,5 @@ +(** Symbolic key-value maps. *) + module Key = struct module type S = sig include Stdlib.Map.OrderedType @@ -22,6 +24,8 @@ module Key = struct end module type S = sig + (** Defines a type that is a symbolic map from [key] to value. *) + module Symex : Symex.S type key From d5f1bec94e8378ca7d6032134efef42b2847bb3a Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 9 Sep 2025 09:58:59 +0100 Subject: [PATCH 09/22] symbolic integers Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_int.ml | 20 ++++++++++++++++++++ soteria/lib/sym_data/sym_data.ml | 1 + 2 files changed, 21 insertions(+) create mode 100644 soteria/lib/sym_data/s_int.ml diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml new file mode 100644 index 000000000..8f42fe8dc --- /dev/null +++ b/soteria/lib/sym_data/s_int.ml @@ -0,0 +1,20 @@ +(** Symbolic abstractions over integers. *) + +module type S = sig + include S_elt.S + include S_eq.S with module Symex := Symex and type t := t + + (** Takes an integer and creates an abstraction over it *) + val of_z : Z.t -> t + + (** Takes a symbolic integer and returns [Some z] if this abstraction + describes exactly a single integer, and [None] otherwise *) + val to_z : t -> Z.t option + + (** {3 Arithmetic operations} *) + + val ( +@ ) : t -> t -> t + val ( -@ ) : t -> t -> t + val ( <@ ) : t -> t -> t + val ( <=@ ) : t -> t -> t +end diff --git a/soteria/lib/sym_data/sym_data.ml b/soteria/lib/sym_data/sym_data.ml index 5e031243f..89261cc8f 100644 --- a/soteria/lib/sym_data/sym_data.ml +++ b/soteria/lib/sym_data/sym_data.ml @@ -2,4 +2,5 @@ module S_elt = S_elt module S_eq = S_eq +module S_int = S_int module S_map = S_map From ac53dd390eb13cb968bd3e7a8f5f6c3fe303b808 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 18:28:11 +0100 Subject: [PATCH 10/22] Explicit S_bool module Signed-off-by: Sacha Ayoun --- soteria-c/lib/globs.ml | 6 +- soteria-c/lib/interp.ml | 8 +- soteria-c/lib/state.ml | 4 +- soteria-rust/lib/interp.ml | 2 +- soteria-rust/lib/rustsymex.ml | 2 +- soteria/lib/bv_values/analyses.ml | 4 +- soteria/lib/bv_values/bv_solver.ml | 34 +++--- soteria/lib/bv_values/encoding.ml | 2 +- soteria/lib/bv_values/eval.ml | 16 +-- soteria/lib/bv_values/svalue.ml | 128 +++++++++++----------- soteria/lib/bv_values/typed.ml | 9 +- soteria/lib/bv_values/typed.mli | 18 +++- soteria/lib/c_values/analyses.ml | 15 +-- soteria/lib/c_values/c_solver.ml | 28 ++--- soteria/lib/c_values/eval.ml | 6 +- soteria/lib/c_values/svalue.ml | 156 ++++++++++++++------------- soteria/lib/c_values/typed.ml | 7 +- soteria/lib/c_values/typed.mli | 24 +++-- soteria/lib/sym_data/s_eq.ml | 8 +- soteria/lib/sym_states/plist.ml | 5 +- soteria/lib/sym_states/pmap.ml | 6 +- soteria/lib/sym_states/pure_fun.ml | 2 +- soteria/lib/sym_states/tree_block.ml | 2 +- soteria/lib/symex/solver.ml | 6 +- soteria/lib/symex/symex.ml | 30 +++--- soteria/lib/symex/value.ml | 17 ++- soteria/tests/symex/run_twice.ml | 2 +- soteria/tutorial/core_symex.mld | 16 +-- 28 files changed, 309 insertions(+), 254 deletions(-) diff --git a/soteria-c/lib/globs.ml b/soteria-c/lib/globs.ml index 7590c4814..eeffee7ab 100644 --- a/soteria-c/lib/globs.ml +++ b/soteria-c/lib/globs.ml @@ -15,7 +15,7 @@ module Loc = struct let fresh () = let open Typed.Infix in let* loc = Csymex.nondet Typed.t_loc in - let+ () = Symex.assume [ Typed.not (loc ==@ Typed.Ptr.null_loc) ] in + let+ () = Symex.assume [ Typed.S_bool.not (loc ==@ Typed.Ptr.null_loc) ] in loc let sem_eq = Typed.sem_eq @@ -58,7 +58,7 @@ let get sym st = let open Typed.Infix in if Cerb_frontend.Symbol.equal_sym k sym then None else - let neq = Typed.not (v ==@ loc) in + let neq = Typed.S_bool.not (v ==@ loc) in Some neq) |> List.of_seq in @@ -76,7 +76,7 @@ let produce serialized st = |> Seq.self_cross_product |> Seq.map (fun ((_, loca), (_, locb)) -> let open Typed.Infix in - Typed.not (loca ==@ locb)) + Typed.S_bool.not (loca ==@ locb)) |> List.of_seq in assume to_assume diff --git a/soteria-c/lib/interp.ml b/soteria-c/lib/interp.ml index eb2aab8c5..5c5a687f3 100644 --- a/soteria-c/lib/interp.ml +++ b/soteria-c/lib/interp.ml @@ -173,7 +173,7 @@ module Make (State : State_intf.S) = struct let open Typed in match get_ty x with | TInt -> Csymex.return (bool_of_int (cast x)) - | TPointer -> Csymex.return (not (Ptr.is_null (cast x))) + | TPointer -> Csymex.return (S_bool.not (Ptr.is_null (cast x))) | _ -> Csymex.not_impl "Cannot cast to bool" let cast_aggregate_to_bool (x : Agv.t) : [> T.sbool ] Typed.t Csymex.t = @@ -588,7 +588,7 @@ module Make (State : State_intf.S) = struct L.trace (fun m -> m "Function pointer is value: %a" Agv.pp fptr); let^ fptr = cast_aggregate_to_ptr fptr in if%sat - Typed.not (Typed.Ptr.ofs fptr ==@ 0s) + Typed.S_bool.not (Typed.Ptr.ofs fptr ==@ 0s) ||@ Typed.Ptr.is_at_null_loc fptr then error `InvalidFunctionPtr else @@ -1072,7 +1072,7 @@ module Make (State : State_intf.S) = struct let rec loop () = let* cond_v = eval_expr cond in let^ cond_v = cast_aggregate_to_bool cond_v in - let neg_cond = Typed.not cond_v in + let neg_cond = Typed.S_bool.not cond_v in if%sat neg_cond then ok Normal else let () = L.trace (fun m -> m "Condition is SAT!") in @@ -1093,7 +1093,7 @@ module Make (State : State_intf.S) = struct | Normal | Continue -> let* cond_v = eval_expr cond in let^ cond_v = cast_aggregate_to_bool cond_v in - if%sat Typed.not cond_v then ok Normal else loop () + if%sat Typed.S_bool.not cond_v then ok Normal else loop () | Case _ -> failwith "SOTERIA BUG: Case in do body" in loop () diff --git a/soteria-c/lib/state.ml b/soteria-c/lib/state.ml index dc7c76d20..fbce30bbc 100644 --- a/soteria-c/lib/state.ml +++ b/soteria-c/lib/state.ml @@ -172,7 +172,7 @@ let alloc ?(zeroed = false) size st = let** loc, st = SPmap.alloc ~new_codom:block heap in let ptr = Typed.Ptr.mk loc 0s in (* The pointer is necessarily not null *) - let+ () = Typed.(assume [ not (loc ==@ Ptr.null_loc) ]) in + let+ () = Typed.(assume [ S_bool.not (loc ==@ Ptr.null_loc) ]) in Soteria.Symex.Compo_res.ok (ptr, st) let alloc_ty ty st = @@ -200,7 +200,7 @@ let produce (serialized : serialized) (st : t) : t Csymex.t = let globs_locs = List.to_seq serialized.globs |> Seq.map snd in Seq.append heap_locs globs_locs in - Seq.map (fun loc -> Typed.not (Typed.Ptr.null_loc ==@ loc)) locs + Seq.map (fun loc -> Typed.S_bool.not (Typed.Ptr.null_loc ==@ loc)) locs |> List.of_seq in let* () = Csymex.assume non_null_locs in diff --git a/soteria-rust/lib/interp.ml b/soteria-rust/lib/interp.ml index 326fd58ca..e785450ea 100644 --- a/soteria-rust/lib/interp.ml +++ b/soteria-rust/lib/interp.ml @@ -108,7 +108,7 @@ module Make (State : State_intf.S) = struct let resolve_constant (const : Expressions.constant_expr) = match const.value with | CLiteral (VScalar scalar) -> ok (Base (BV.of_scalar scalar)) - | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.bool b))) + | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.S_bool.of_bool b))) | CLiteral (VChar c) -> ok (Base (BV.u32i (Uchar.to_int c))) | CLiteral (VFloat { float_value; float_ty }) -> ok (Base (Typed.Float.mk float_ty float_value)) diff --git a/soteria-rust/lib/rustsymex.ml b/soteria-rust/lib/rustsymex.ml index b65cc310f..293398c4c 100644 --- a/soteria-rust/lib/rustsymex.ml +++ b/soteria-rust/lib/rustsymex.ml @@ -13,7 +13,7 @@ module SYMEX = include SYMEX include Syntaxes.FunctionWrap -let match_on (elements : 'a list) ~(constr : 'a -> Typed.sbool Typed.t) : +let match_on (elements : 'a list) ~(constr : 'a -> Typed.S_bool.t Typed.t) : 'a option t = let open Syntax in let rec aux = function diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index a8bf67e08..e60421c23 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -8,7 +8,7 @@ module type S = sig val simplify : t -> Svalue.t -> Svalue.t val add_constraint : t -> Svalue.t -> Svalue.t * Var.Set.t - val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t + val encode : ?vars:Var.Hashset.t -> t -> Typed.S_bool.t Typed.t Iter.t end module Merge (A1 : S) (A2 : S) : S = struct @@ -35,7 +35,7 @@ module Merge (A1 : S) (A2 : S) : S = struct let v'', vars2 = A2.add_constraint a2 v' in (v'', Var.Set.union vars1 vars2) - let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t = + let encode ?vars (a1, a2) : Typed.S_bool.t Typed.t Iter.t = Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2) end diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml index 34518241f..f151e2a67 100644 --- a/soteria/lib/bv_values/bv_solver.ml +++ b/soteria/lib/bv_values/bv_solver.ml @@ -8,34 +8,34 @@ let rec simplify ~trivial_truthiness ~fallback (v : Svalue.t) = | Bool _ | BitVec _ | Float _ -> v | _ -> ( match trivial_truthiness (Typed.type_ v) with - | Some true -> Svalue.Bool.v_true - | Some false -> Svalue.Bool.v_false + | Some true -> Svalue.S_bool.v_true + | Some false -> Svalue.S_bool.v_false | None -> ( match v.node.kind with | Unop (Not, e) -> let e' = simplify e in - if Svalue.equal e e' then v else Svalue.Bool.not e' + if Svalue.equal e e' then v else Svalue.S_bool.not e' | Binop (Eq, e1, e2) -> - if Svalue.equal e1 e2 then Svalue.Bool.v_true - else if Svalue.sure_neq e1 e2 then Svalue.Bool.v_false + if Svalue.equal e1 e2 then Svalue.S_bool.v_true + else if Svalue.sure_neq e1 e2 then Svalue.S_bool.v_false else v | Binop (And, e1, e2) -> let se1 = simplify e1 in let se2 = simplify e2 in if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.Bool.and_ se1 se2 + else Svalue.S_bool.and_ se1 se2 | Binop (Or, e1, e2) -> let se1 = simplify e1 in let se2 = simplify e2 in if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.Bool.or_ se1 se2 + else Svalue.S_bool.or_ se1 se2 | Ite (g, e1, e2) -> let sg = simplify g in let se1 = simplify e1 in let se2 = simplify e2 in if Svalue.equal sg g && Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.Bool.ite sg se1 se2 + else Svalue.S_bool.ite sg se1 se2 | _ -> fallback v)) module Make_incremental @@ -52,7 +52,7 @@ struct end) module Solver_state = struct - type t = Typed.sbool Typed.t Dynarray.t Dynarray.t + type t = Typed.S_bool.t Typed.t Dynarray.t Dynarray.t let init () = let t = Dynarray.create () in @@ -93,7 +93,7 @@ struct let iter (t : t) f = Dynarray.iter (fun t -> Dynarray.iter f t) t - let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) = + let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) = let neg_v = Typed.not v in Dynarray.find_map (Dynarray.find_map (fun value -> @@ -213,7 +213,7 @@ struct instance because an auxiliary analysis has new information about it that is not directly in the PC. *) type slot_content = - | Asrt of Typed.sbool Typed.t [@printer Typed.ppa] + | Asrt of Typed.S_bool.t Typed.t [@printer Typed.ppa] | Dirty of Var.Set.t [@printer Fmt.(iter ~sep:comma) Var.Set.iter Var.pp] [@@deriving show] @@ -276,7 +276,7 @@ struct | _ -> None (* We check if the thing contains the value itself, or its negation. *) - let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) = + let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) = let neg_v = Typed.not v in Dynarray.find_map (Dynarray.find_map (function @@ -475,7 +475,7 @@ struct [|n| == v] exists, in which case we replace it with the value [v]. If the constraint evaluates to true, then it is satisfiable. *) let v_eqs = Var.Hashtbl.create 8 in - Svalue.Bool.split_ands to_check (fun v -> + Svalue.S_bool.split_ands to_check (fun v -> match v.node.kind with | Binop ( Eq, @@ -496,7 +496,7 @@ struct | _ -> Svalue.mk_var v ty in let res = Eval.eval ~eval_var to_check in - Svalue.equal res Svalue.Bool.v_true + Svalue.equal res Svalue.S_bool.v_true let check_sat_raw solver relevant_vars to_check = (* TODO: we shouldn't wait for ack for each command individually... *) @@ -534,9 +534,11 @@ struct Solver_state.unchecked_constraints solver.state in (* This will put the check in a somewhat-normal form, to increase cache hits. *) - let to_check = Dynarray.fold_left Typed.and_ Typed.v_true to_check in let to_check = - Iter.fold Typed.and_ to_check + Dynarray.fold_left Typed.S_bool.and_ Typed.v_true to_check + in + let to_check = + Iter.fold Typed.S_bool.and_ to_check (Analysis.encode ~vars:relevant_vars solver.analysis) in let answer = check_sat_raw_memo solver relevant_vars to_check in diff --git a/soteria/lib/bv_values/encoding.ml b/soteria/lib/bv_values/encoding.ml index e8c9b44a5..cb1ba18da 100644 --- a/soteria/lib/bv_values/encoding.ml +++ b/soteria/lib/bv_values/encoding.ml @@ -127,7 +127,7 @@ and encode_value_memo v = k let encode_value (v : Svalue.t) = - Svalue.Bool.split_ands v + Svalue.S_bool.split_ands v |> Iter.map encode_value_memo |> Iter.to_list |> bool_ands diff --git a/soteria/lib/bv_values/eval.ml b/soteria/lib/bv_values/eval.ml index dd98547ba..c2f3595ea 100644 --- a/soteria/lib/bv_values/eval.ml +++ b/soteria/lib/bv_values/eval.ml @@ -2,9 +2,9 @@ open Svalue open Soteria_std let eval_binop : Binop.t -> t -> t -> t = function - | And -> Bool.and_ - | Or -> Bool.or_ - | Eq -> Bool.sem_eq + | And -> S_bool.and_ + | Or -> S_bool.or_ + | Eq -> S_bool.sem_eq | FEq -> Float.eq | FLeq -> Float.leq | FLt -> Float.lt @@ -32,7 +32,7 @@ let eval_binop : Binop.t -> t -> t -> t = function | AShr -> BitVec.ashr let eval_unop : Unop.t -> t -> t = function - | Not -> Bool.not + | Not -> S_bool.not | FAbs -> Float.abs | GetPtrLoc -> Ptr.loc | GetPtrOfs -> Ptr.ofs @@ -69,12 +69,12 @@ let rec eval ~eval_var (x : t) : t = | Nop (nop, l) -> ( let l, changed = List.map_changed eval l in if Stdlib.not changed then x - else match nop with Distinct -> Bool.distinct l) + else match nop with Distinct -> S_bool.distinct l) | Ite (guard, then_, else_) -> let guard = eval guard in - if equal guard Bool.v_true then eval then_ - else if equal guard Bool.v_false then eval else_ - else Bool.ite guard (eval then_) (eval else_) + if equal guard S_bool.v_true then eval then_ + else if equal guard S_bool.v_false then eval else_ + else S_bool.ite guard (eval then_) (eval else_) | Seq l -> let l, changed = List.map_changed eval l in if Stdlib.not changed then x else Svalue.SSeq.mk ~seq_ty:x.node.ty l diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 46d77d3da..409562356 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -112,7 +112,7 @@ end module Binop = struct type t = - (* Bool *) + (* S_bool *) | And | Or (* Comparison *) @@ -349,11 +349,11 @@ let rec subst subst_var sv = (** {2 Operator declarations} *) -module type Bool = sig +module type S_bool = sig val v_true : t val v_false : t - val as_bool : t -> bool option - val bool : bool -> t + val to_bool : t -> bool option + val of_bool : bool -> t val and_ : t -> t -> t val or_ : t -> t -> t val conj : t list -> t @@ -457,16 +457,16 @@ end (** {2 Booleans} *) -module rec Bool : Bool = struct +module rec S_bool : S_bool = struct let v_true = Bool true <| TBool let v_false = Bool false <| TBool - let as_bool t = + let to_bool t = if equal t v_true then Some true else if equal t v_false then Some false else None - let bool b = + let of_bool b = (* avoid re-alloc and re-hashconsing *) if b then v_true else v_false @@ -541,9 +541,9 @@ module rec Bool : Bool = struct let rec sem_eq v1 v2 = match (v1.node.kind, v2.node.kind) with | _ when equal v1 v2 -> v_true - | Bool b1, Bool b2 -> bool (b1 = b2) + | Bool b1, Bool b2 -> of_bool (b1 = b2) | Ptr (l1, o1), Ptr (l2, o2) -> and_ (sem_eq l1 l2) (sem_eq o1 o2) - | BitVec b1, BitVec b2 -> bool (Z.equal b1 b2) + | BitVec b1, BitVec b2 -> of_bool (Z.equal b1 b2) (* Arithmetics *) | BitVec _, Unop (Neg, v2) -> sem_eq (BitVec.neg v1) v2 | Unop (Neg, v1), BitVec _ -> sem_eq v1 (BitVec.neg v2) @@ -671,22 +671,22 @@ and BitVec : BitVec = struct let is_pow2 z = Z.(gt z zero && popcount z = 1) let of_bool n b = - if equal Bool.v_true b then one n - else if equal Bool.v_false b then zero n + if equal S_bool.v_true b then one n + else if equal S_bool.v_false b then zero n else Unop (BvOfBool n, b) <| TBitVector n let to_bool v = match v.node.kind with - | BitVec z -> Bool.bool (Stdlib.not (Z.equal z Z.zero)) + | BitVec z -> S_bool.of_bool (Stdlib.not (Z.equal z Z.zero)) | Unop (BvOfBool _, sv') -> sv' - | _ -> Bool.not (Bool.sem_eq v (zero (size_of v.node.ty))) + | _ -> S_bool.not (S_bool.sem_eq v (zero (size_of v.node.ty))) let not_bool v = let n = size_of v.node.ty in match v.node.kind with | BitVec z -> if Z.equal z Z.zero then one n else zero n - | Unop (BvOfBool n, g) -> of_bool n (Bool.not g) - | _ -> of_bool n (Bool.sem_eq v (zero n)) + | Unop (BvOfBool n, g) -> of_bool n (S_bool.not g) + | _ -> of_bool n (S_bool.sem_eq v (zero n)) let rec add v1 v2 = match (v1.node.kind, v2.node.kind) with @@ -705,7 +705,7 @@ and BitVec : BitVec = struct | Ite (b, l, r), BitVec x | BitVec x, Ite (b, l, r) -> let n = size_of v1.node.ty in let x = mk n x in - Bool.ite b (add l x) (add r x) + S_bool.ite b (add l x) (add r x) | _ -> mk_commut_binop Add v1 v2 <| v1.node.ty and sub v1 v2 = @@ -720,10 +720,10 @@ and BitVec : BitVec = struct | Binop (Sub, s, ({ node = { kind = BitVec _; _ }; _ } as c1)), BitVec _ -> sub s (add c1 v2) (* only propagate down ites if we know it's concrete *) - | Ite (b, l, r), BitVec _ -> Bool.ite b (sub l v2) (sub r v2) - | BitVec _, Ite (b, l, r) -> Bool.ite b (sub v1 l) (sub v1 r) - | Unop (BvOfBool n, b), BitVec _ -> Bool.ite b (sub (one n) v2) (neg v2) - | BitVec _, Unop (BvOfBool n, b) -> Bool.ite b (sub v1 (one n)) v1 + | Ite (b, l, r), BitVec _ -> S_bool.ite b (sub l v2) (sub r v2) + | BitVec _, Ite (b, l, r) -> S_bool.ite b (sub v1 l) (sub v1 r) + | Unop (BvOfBool n, b), BitVec _ -> S_bool.ite b (sub (one n) v2) (neg v2) + | BitVec _, Unop (BvOfBool n, b) -> S_bool.ite b (sub v1 (one n)) v1 | _ -> Binop (Sub, v1, v2) <| v1.node.ty and neg v = @@ -735,8 +735,8 @@ and BitVec : BitVec = struct match v.node.kind with | BitVec bv -> mk_masked n Z.(neg bv) | Unop (Neg, v) -> v - | Ite (b, l, r) -> Bool.ite b (neg l) (neg r) - | Unop (BvOfBool n, b) -> Bool.ite b (neg (one n)) (zero n) + | Ite (b, l, r) -> S_bool.ite b (neg l) (neg r) + | Unop (BvOfBool n, b) -> S_bool.ite b (neg (one n)) (zero n) | _ -> Unop (Neg, v) <| v.node.ty let rec mul v1 v2 = @@ -750,7 +750,7 @@ and BitVec : BitVec = struct | Ite (b, l, r), BitVec x | BitVec x, Ite (b, l, r) -> let n = size_of v1.node.ty in let x = mk n x in - Bool.ite b (mul l x) (mul r x) + S_bool.ite b (mul l x) (mul r x) | _ -> mk_commut_binop Mul v1 v2 <| v1.node.ty let div ~signed v1 v2 = @@ -811,7 +811,7 @@ and BitVec : BitVec = struct | BitVec bv -> let n = size_of v.node.ty in mk_masked n Z.(lognot bv) - | Ite (b, l, r) -> Bool.ite b (not l) (not r) + | Ite (b, l, r) -> S_bool.ite b (not l) (not r) | _ -> Unop (BvNot, v) <| v.node.ty and and_ v1 v2 = @@ -834,8 +834,8 @@ and BitVec : BitVec = struct let low_mask = Z.(pred (one lsl bitwidth)) in Z.(equal (mask land low_mask) low_mask) -> base <| t_bv n - | BitVec _, Ite (b, l, r) -> Bool.ite b (and_ v1 l) (and_ v1 r) - | Ite (b, l, r), BitVec _ -> Bool.ite b (and_ l v2) (and_ r v2) + | BitVec _, Ite (b, l, r) -> S_bool.ite b (and_ v1 l) (and_ v1 r) + | Ite (b, l, r), BitVec _ -> S_bool.ite b (and_ l v2) (and_ r v2) (* if it's a right mask, it's usually beneficial to propagate it *) | (BitVec mask, Binop (BitAnd, l, r) | Binop (BitAnd, l, r), BitVec mask) when is_right_mask mask -> @@ -845,12 +845,12 @@ and BitVec : BitVec = struct | BitVec o, Unop (BvOfBool _, _) when Z.equal o Z.one -> v2 | Unop (BvOfBool _, _), BitVec o when Z.equal o Z.one -> v1 | Unop (BvOfBool _, b1), Unop (BvOfBool _, b2) -> - of_bool n (Bool.and_ b1 b2) + of_bool n (S_bool.and_ b1 b2) | ( Ite (b1, l1, { node = { kind = BitVec r1; _ }; _ }), Ite (b2, l2, { node = { kind = BitVec r2; _ }; _ }) ) when Z.(equal r1 zero) && Z.(equal r2 zero) -> let n = size_of v1.node.ty in - Bool.ite (Bool.and_ b1 b2) (and_ l1 l2) (zero n) + S_bool.ite (S_bool.and_ b1 b2) (and_ l1 l2) (zero n) | _, _ -> mk_commut_binop BitAnd v1 v2 <| t_bv n and or_ v1 v2 = @@ -877,7 +877,8 @@ and BitVec : BitVec = struct else let new_tail = extract 0 (nx - 1) tail in concat new_tail base - | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) -> of_bool n (Bool.or_ b1 b2) + | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) -> + of_bool n (S_bool.or_ b1 b2) | _ -> mk_commut_binop BitOr v1 v2 <| v1.node.ty and xor v1 v2 = @@ -888,7 +889,7 @@ and BitVec : BitVec = struct | BitVec z, _ when Z.equal z Z.zero -> v2 | _, BitVec z when Z.equal z Z.zero -> v1 | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) -> - of_bool n (Bool.not (Bool.sem_eq b1 b2)) + of_bool n (S_bool.not (S_bool.sem_eq b1 b2)) | _ -> mk_commut_binop BitXor v1 v2 <| v1.node.ty (** [extract from_ to_ v] returns a bitvector covering bits from index @@ -924,7 +925,7 @@ and BitVec : BitVec = struct | Ite (b, l, r) -> let l = extract from_ to_ l in let r = extract from_ to_ r in - Bool.ite b l r + S_bool.ite b l r | Unop (BvExtend (false, by), _) when from_ >= prev_size - by -> (* zero extension, and we're extracting only the extended bits *) zero size @@ -971,7 +972,7 @@ and BitVec : BitVec = struct | Ite (b, l, r) -> let l = extend ~signed extend_by l in let r = extend ~signed extend_by r in - Bool.ite b l r + S_bool.ite b l r (* can't extend if signed && n == 1, as it should be all 1s *) | Unop (BvOfBool n, b) when Stdlib.not signed || n > 1 -> of_bool to_ b (* unlike with extract, we don't want to propagate extend within the expression for &, |, ^, @@ -1001,7 +1002,7 @@ and BitVec : BitVec = struct right ) ) -> concat (concat v1 left) right | Ite (b1, l1, r1), Ite (b2, l2, r2) when equal b1 b2 -> - Bool.ite b1 (concat l1 l2) (concat r1 r2) + S_bool.ite b1 (concat l1 l2) (concat r1 r2) | _, _ -> Binop (BvConcat, v1, v2) <| t_bv (n1 + n2) let rec shl v1 v2 = @@ -1039,42 +1040,42 @@ and BitVec : BitVec = struct let bits = size_of v1.node.ty in match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> - Bool.bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r) + S_bool.of_bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r) | _, BitVec x when Stdlib.not signed && Z.(equal x one) -> (* unsigned x < 1 is x == 0 *) - Bool.sem_eq v1 (zero bits) + S_bool.sem_eq v1 (zero bits) | _, BitVec x when signed && Z.(equal x zero) -> (* signed x < 0 is checking the sign bit *) let sign_bit = extract (bits - 1) (bits - 1) v1 in - Bool.sem_eq sign_bit (one 1) + S_bool.sem_eq sign_bit (one 1) | BitVec x, _ when signed && Z.equal x Z.zero -> (* signed 0 < x is checking the sign bit of x is not set *) let sign_bit = extract (bits - 1) (bits - 1) v2 in - Bool.sem_eq sign_bit (zero 1) + S_bool.sem_eq sign_bit (zero 1) | BitVec x, _ when Z.equal (bv_to_z signed bits x) (max_for signed bits) -> - Bool.v_false + S_bool.v_false | _, BitVec x when Z.equal (bv_to_z signed bits x) (min_for signed bits) -> - Bool.v_false + S_bool.v_false | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits) -> - Bool.not (Bool.sem_eq v1 v2) + S_bool.not (S_bool.sem_eq v1 v2) | _, BitVec x when Z.equal (bv_to_z signed bits x) (max_for signed bits) -> - Bool.not (Bool.sem_eq v1 v2) + S_bool.not (S_bool.sem_eq v1 v2) (* x < ite(b, 1, 0) => ite(b, x < 1, x < 0) => ite(b, x = 0, false) => b && x = 0 *) | _, Unop (BvOfBool n, b) when Stdlib.not signed -> - Bool.and_ b (Bool.sem_eq v1 (zero n)) - | Ite (b, l, r), _ -> Bool.ite b (lt ~signed l v2) (lt ~signed r v2) - | _, Ite (b, l, r) -> Bool.ite b (lt ~signed v1 l) (lt ~signed v1 r) + S_bool.and_ b (S_bool.sem_eq v1 (zero n)) + | Ite (b, l, r), _ -> S_bool.ite b (lt ~signed l v2) (lt ~signed r v2) + | _, Ite (b, l, r) -> S_bool.ite b (lt ~signed v1 l) (lt ~signed v1 r) | _ -> Binop (Lt signed, v1, v2) <| TBool let leq ~signed v1 v2 = let bits = size_of v1.node.ty in match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> - Bool.bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r) + S_bool.of_bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r) | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits) -> - Bool.v_true + S_bool.v_true | _, BitVec x when Z.equal (bv_to_z signed bits x) (max_for signed bits) -> - Bool.v_true + S_bool.v_true | _ -> Binop (Leq signed, v1, v2) <| TBool let gt ~signed v1 v2 = lt ~signed v2 v1 @@ -1086,27 +1087,27 @@ and BitVec : BitVec = struct let l = bv_to_z signed n l in let r = bv_to_z signed n r in let res = op l r in - Bool.bool Z.Compare.(res < minz || res > maxz) + S_bool.of_bool Z.Compare.(res < minz || res > maxz) let add_overflows ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> ovf_check ~signed (size_of v1.node.ty) l r Z.( + ) - | BitVec z, _ when Z.equal z Z.zero -> Bool.v_false - | _, BitVec z when Z.equal z Z.zero -> Bool.v_false + | BitVec z, _ when Z.equal z Z.zero -> S_bool.v_false + | _, BitVec z when Z.equal z Z.zero -> S_bool.v_false | _ -> Binop (AddOvf signed, v1, v2) <| TBool let mul_overflows ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> ovf_check ~signed (size_of v1.node.ty) l r Z.( * ) - | BitVec z, _ when Z.equal z Z.zero || Z.equal z Z.one -> Bool.v_false - | _, BitVec z when Z.equal z Z.zero || Z.equal z Z.one -> Bool.v_false + | BitVec z, _ when Z.equal z Z.zero || Z.equal z Z.one -> S_bool.v_false + | _, BitVec z when Z.equal z Z.zero || Z.equal z Z.one -> S_bool.v_false | _ -> Binop (MulOvf signed, v1, v2) <| TBool let neg_overflows v = match v.node.kind with | BitVec bv -> let n = size_of v.node.ty in - Bool.bool (Z.equal (bv_to_z true n bv) (min_for true n)) + S_bool.of_bool (Z.equal (bv_to_z true n bv) (min_for true n)) | _ -> Unop (NegOvf, v) <| TBool let sub_overflows ~signed v1 v2 = @@ -1115,7 +1116,7 @@ and BitVec : BitVec = struct let neg_ovf = neg_overflows v2 in let neg_v2 = neg v2 in let add_ovf = add_overflows ~signed v1 neg_v2 in - Bool.or_ neg_ovf add_ovf + S_bool.or_ neg_ovf add_ovf let of_float ~signed ~size v = let p = precision_of_f v.node.ty in @@ -1150,12 +1151,12 @@ and Float : Float = struct let lt v1 v2 = match (v1.node.kind, v2.node.kind) with - | Float f1, Float f2 -> Bool.bool (str2f f1 < str2f f2) + | Float f1, Float f2 -> S_bool.of_bool (str2f f1 < str2f f2) | _ -> Binop (FLt, v1, v2) <| TBool let leq v1 v2 = match (v1.node.kind, v2.node.kind) with - | Float f1, Float f2 -> Bool.bool (str2f f1 <= str2f f2) + | Float f1, Float f2 -> S_bool.of_bool (str2f f1 <= str2f f2) | _ -> Binop (FLeq, v1, v2) <| TBool let gt v1 v2 = lt v2 v1 @@ -1178,7 +1179,8 @@ and Float : Float = struct let[@inline] is_floatclass fc = fun sv -> match sv.node.kind with - | Float f -> Bool.bool (FloatClass.as_fpclass fc = classify_float (str2f f)) + | Float f -> + S_bool.of_bool (FloatClass.as_fpclass fc = classify_float (str2f f)) | _ -> Unop (FIs fc, sv) <| TBool let is_normal = is_floatclass Normal @@ -1200,7 +1202,7 @@ module Ptr = struct | _ -> Unop (GetPtrLoc, p) <| TLoc (size_of p.node.ty) let null_loc n = BitVec Z.zero <| TLoc n - let is_null_loc l = Bool.sem_eq l (null_loc (size_of l.node.ty)) + let is_null_loc l = S_bool.sem_eq l (null_loc (size_of l.node.ty)) let loc_of_z n z = BitVec z <| TLoc n let loc_of_int n i = loc_of_z n (Z.of_int i) @@ -1219,7 +1221,7 @@ module Ptr = struct mk loc (BitVec.add ofs o) let null n = mk (null_loc n) (BitVec.zero n) - let is_null p = Bool.sem_eq p (null (size_of p.node.ty)) + let is_null p = S_bool.sem_eq p (null (size_of p.node.ty)) let is_at_null_loc p = is_null_loc (loc p) end @@ -1238,10 +1240,10 @@ module Infix = struct let bv_z = BitVec.mk let ptr = Ptr.mk let seq = SSeq.mk - let ( ==@ ) = Bool.sem_eq - let ( ==?@ ) = Bool.sem_eq_untyped - let ( &&@ ) = Bool.and_ - let ( ||@ ) = Bool.or_ + let ( ==@ ) = S_bool.sem_eq + let ( ==?@ ) = S_bool.sem_eq_untyped + let ( &&@ ) = S_bool.and_ + let ( ||@ ) = S_bool.or_ let ( >@ ) = BitVec.gt ~signed:false let ( >=@ ) = BitVec.geq ~signed:false let ( <@ ) = BitVec.lt ~signed:false diff --git a/soteria/lib/bv_values/typed.ml b/soteria/lib/bv_values/typed.ml index c0cd27610..bbcd831b5 100644 --- a/soteria/lib/bv_values/typed.ml +++ b/soteria/lib/bv_values/typed.ml @@ -29,11 +29,16 @@ end type nonrec +'a t = t type nonrec +'a ty = ty -type sbool = T.sbool let t_int = t_bv -include Bool +include S_bool + +module S_bool = struct + type t = T.sbool + + include S_bool +end let[@inline] get_ty x = x.node.ty let[@inline] type_type x = x diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli index 5e99d53fa..d235d0a41 100644 --- a/soteria/lib/bv_values/typed.mli +++ b/soteria/lib/bv_values/typed.mli @@ -62,7 +62,19 @@ val t_f : Svalue.FloatPrecision.t -> [> sfloat ] ty (** {2 Typed svalues} *) type +'a t -type sbool = T.sbool + +module S_bool : sig + type +'a v := 'a t + type t = sbool + + val of_bool : bool -> [> sbool ] v + val to_bool : [< sbool ] v -> bool option + val and_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v + val or_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v + val not : [< sbool ] v -> [> sbool ] v +end + +type sbool := T.sbool (** Basic value operations *) @@ -96,12 +108,8 @@ val sem_eq : 'a t -> 'a t -> sbool t val sem_eq_untyped : 'a t -> 'a t -> [> sbool ] t val v_true : [> sbool ] t val v_false : [> sbool ] t -val bool : bool -> [> sbool ] t -val as_bool : 'a t -> bool option -val and_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t val conj : [< sbool ] t list -> [> sbool ] t val split_ands : [< sbool ] t -> ([> sbool ] t -> unit) -> unit -val or_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t val not : sbool t -> sbool t val distinct : 'a t list -> [> sbool ] t val ite : [< sbool ] t -> 'a t -> 'a t -> 'a t diff --git a/soteria/lib/c_values/analyses.ml b/soteria/lib/c_values/analyses.ml index b95e13447..250cf90e8 100644 --- a/soteria/lib/c_values/analyses.ml +++ b/soteria/lib/c_values/analyses.ml @@ -10,7 +10,7 @@ module type S = sig val simplify : t -> Svalue.t -> Svalue.t val add_constraint : t -> Svalue.t -> Svalue.t * Var.Set.t - val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t + val encode : ?vars:Var.Hashset.t -> t -> Typed.S_bool.t Typed.t Iter.t end module Merge (A1 : S) (A2 : S) : S = struct @@ -37,7 +37,7 @@ module Merge (A1 : S) (A2 : S) : S = struct let v'', vars2 = A2.add_constraint a2 v' in (v'', Var.Set.union vars1 vars2) - let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t = + let encode ?vars (a1, a2) : Typed.S_bool.t Typed.t Iter.t = Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2) end @@ -208,7 +208,7 @@ module Interval : S = struct (if neg then "/" else "∩") Range.pp range' Range.pp new_range); let is_ok = not (Range.is_empty range) in - ((Svalue.bool (is_ok <> neg), Var.Set.empty), st) + ((Svalue.S_bool.of_bool (is_ok <> neg), Var.Set.empty), st) | Some new_range -> ( let st' = Var.Map.add var new_range st in log (fun m -> @@ -221,7 +221,7 @@ module Interval : S = struct let eq = Svalue.int_z m ==@ mk_var var in (* this is hacky; we found the exact value, but we can't return the equality if we're negating, since that equality will otherwise be negated. *) - (((if neg then Svalue.not eq else eq), Var.Set.empty), st') + (((if neg then Svalue.S_bool.not eq else eq), Var.Set.empty), st') (* The range is empty, so this cannot be true *) | _ when Range.is_empty new_range -> ((Svalue.v_false, Var.Set.empty), st') @@ -233,7 +233,8 @@ module Interval : S = struct (* We could cleanly absorb the range, so the PC doesn't need to store it -- however we must mark this variable as dirty, as maybe the modified range still renders the branch infeasible, e.g. because of some additional PC assertions. *) - | _ -> ((Svalue.bool (not neg), Var.Set.singleton var), st')) + | _ -> ((Svalue.S_bool.of_bool (not neg), Var.Set.singleton var), st') + ) in match v.node.kind with | Binop @@ -260,7 +261,7 @@ module Interval : S = struct (* We conservatively explore negations; we're only interested in simple (in)equalities *) | Unop (Not, nv) -> let (nv', vars), st' = add_constraint ~absorb ~neg:(not neg) nv st in - ((Svalue.not nv', vars), st') + ((Svalue.S_bool.not nv', vars), st') (* We don't explore && and || within negations, because that becomes messy. *) | Binop (And, v1, v2) when not neg -> let (v1', vars1), st' = add_constraint ~absorb v1 st in @@ -289,7 +290,7 @@ module Interval : S = struct (** Encode all the information relevant to the given variables and conjuncts them with the given accumulator. *) - let encode ?vars st : Typed.sbool Typed.t Iter.t = + let encode ?vars st : Typed.S_bool.t Typed.t Iter.t = let to_check = Option.fold ~none:(fun _ -> true) ~some:Var.Hashset.mem vars in diff --git a/soteria/lib/c_values/c_solver.ml b/soteria/lib/c_values/c_solver.ml index 98033a3d1..40267a9c2 100644 --- a/soteria/lib/c_values/c_solver.ml +++ b/soteria/lib/c_values/c_solver.ml @@ -16,7 +16,7 @@ struct end) module Solver_state = struct - type t = Typed.sbool Typed.t Dynarray.t Dynarray.t + type t = Typed.S_bool.t Typed.t Dynarray.t Dynarray.t let init () = let t = Dynarray.create () in @@ -57,8 +57,8 @@ struct let iter (t : t) f = Dynarray.iter (fun t -> Dynarray.iter f t) t - let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) = - let neg_v = Typed.not v in + let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) = + let neg_v = Typed.S_bool.not v in Dynarray.find_map (Dynarray.find_map (fun value -> if Typed.equal value v then Some true @@ -134,7 +134,7 @@ struct match v.node.kind with | Unop (Not, e) -> let e' = simplify' solver e in - if Svalue.equal e e' then v else Svalue.not e' + if Svalue.equal e e' then v else Svalue.S_bool.not e' | Binop (Eq, e1, e2) -> if Svalue.equal e1 e2 && (not @@ Svalue.is_float e1.node.ty) then Svalue.v_true @@ -144,7 +144,7 @@ struct let se1 = simplify' solver e1 in let se2 = simplify' solver e2 in if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.or_ se1 se2 + else Svalue.S_bool.or_ se1 se2 | _ -> Analysis.simplify solver.analysis v)) and simplify solver (v : 'a Typed.t) : 'a Typed.t = @@ -199,7 +199,7 @@ struct instance because an auxiliary analysis has new information about it that is not directly in the PC. *) type slot_content = - | Asrt of Typed.sbool Typed.t [@printer Typed.ppa] + | Asrt of Typed.S_bool.t Typed.t [@printer Typed.ppa] | Dirty of Var.Set.t [@printer Fmt.(iter ~sep:comma) Var.Set.iter Var.pp] [@@deriving show] @@ -262,8 +262,8 @@ struct | _ -> None (* We check if the thing contains the value itself, or its negation. *) - let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) = - let neg_v = Typed.not v in + let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) = + let neg_v = Typed.S_bool.not v in Dynarray.find_map (Dynarray.find_map (function | { value = Asrt value; _ } -> @@ -450,7 +450,7 @@ struct match v.node.kind with | Unop (Not, e) -> let e' = simplify' solver e in - if Svalue.equal e e' then v else Svalue.not e' + if Svalue.equal e e' then v else Svalue.S_bool.not e' | Binop (Eq, e1, e2) -> if Svalue.equal e1 e2 && (not @@ Svalue.is_float e1.node.ty) then Svalue.v_true @@ -460,12 +460,12 @@ struct let se1 = simplify' solver e1 in let se2 = simplify' solver e2 in if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.and_ se1 se2 + else Svalue.S_bool.and_ se1 se2 | Binop (Or, e1, e2) -> let se1 = simplify' solver e1 in let se2 = simplify' solver e2 in if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v - else Svalue.or_ se1 se2 + else Svalue.S_bool.or_ se1 se2 | Ite (g, e1, e2) -> let sg = simplify' solver g in let se1 = simplify' solver e1 in @@ -557,9 +557,11 @@ struct Solver_state.unchecked_constraints solver.state in (* This will put the check in a somewhat-normal form, to increase cache hits. *) - let to_check = Dynarray.fold_left Typed.and_ Typed.v_true to_check in let to_check = - Iter.fold Typed.and_ to_check + Dynarray.fold_left Typed.S_bool.and_ Typed.v_true to_check + in + let to_check = + Iter.fold Typed.S_bool.and_ to_check (Analysis.encode ~vars:relevant_vars solver.analysis) in let answer = check_sat_raw_memo solver relevant_vars to_check in diff --git a/soteria/lib/c_values/eval.ml b/soteria/lib/c_values/eval.ml index 39ee438cc..3bc55fb59 100644 --- a/soteria/lib/c_values/eval.ml +++ b/soteria/lib/c_values/eval.ml @@ -7,8 +7,8 @@ let eval_var (v : Var.t) (ty : Svalue.ty) : t = Effect.perform (Eval_var (v, ty)) let eval_binop : Binop.t -> t -> t -> t = function - | And -> and_ - | Or -> or_ + | And -> S_bool.and_ + | Or -> S_bool.or_ | Eq -> sem_eq | Leq -> leq | Lt -> lt @@ -45,7 +45,7 @@ let eval_binop : Binop.t -> t -> t -> t = function | BitAShr -> BitVec.Raw.ashr let eval_unop : Unop.t -> t -> t = function - | Not -> not + | Not -> S_bool.not | FAbs -> Float.abs | GetPtrLoc -> Ptr.loc | GetPtrOfs -> Ptr.ofs diff --git a/soteria/lib/c_values/svalue.ml b/soteria/lib/c_values/svalue.ml index 153d6400d..f8e3b5cd7 100644 --- a/soteria/lib/c_values/svalue.ml +++ b/soteria/lib/c_values/svalue.ml @@ -367,45 +367,47 @@ let rec subst subst_var sv = let v_true = Bool true <| TBool let v_false = Bool false <| TBool -let as_bool t = - if equal t v_true then Some true - else if equal t v_false then Some false - else None +module S_bool = struct + let to_bool t = + if equal t v_true then Some true + else if equal t v_false then Some false + else None -let bool b = - (* avoid re-alloc and re-hashconsing *) - if b then v_true else v_false + let of_bool b = + (* avoid re-alloc and re-hashconsing *) + if b then v_true else v_false -let and_ v1 v2 = - match (v1.node.kind, v2.node.kind) with - | _, _ when equal v1 v2 -> v1 - | Bool false, _ | _, Bool false -> v_false - | Bool true, _ -> v2 - | _, Bool true -> v1 - | _ -> mk_commut_binop And v1 v2 <| TBool - -let or_ v1 v2 = - match (v1.node.kind, v2.node.kind) with - | Bool true, _ | _, Bool true -> v_true - | Bool false, _ -> v2 - | _, Bool false -> v1 - | _ -> mk_commut_binop Or v1 v2 <| TBool + let and_ v1 v2 = + match (v1.node.kind, v2.node.kind) with + | _, _ when equal v1 v2 -> v1 + | Bool false, _ | _, Bool false -> v_false + | Bool true, _ -> v2 + | _, Bool true -> v1 + | _ -> mk_commut_binop And v1 v2 <| TBool -let conj l = List.fold_left and_ v_true l + let or_ v1 v2 = + match (v1.node.kind, v2.node.kind) with + | Bool true, _ | _, Bool true -> v_true + | Bool false, _ -> v2 + | _, Bool false -> v1 + | _ -> mk_commut_binop Or v1 v2 <| TBool + + let rec not sv = + if equal sv v_true then v_false + else if equal sv v_false then v_true + else + match sv.node.kind with + | Unop (Not, sv) -> sv + | Binop (Lt, v1, v2) -> Binop (Leq, v2, v1) <| TBool + | Binop (Leq, v1, v2) -> Binop (Lt, v2, v1) <| TBool + | Binop (BvLt s, v1, v2) -> Binop (BvLeq s, v2, v1) <| TBool + | Binop (BvLeq s, v1, v2) -> Binop (BvLt s, v2, v1) <| TBool + | Binop (Or, v1, v2) -> mk_commut_binop And (not v1) (not v2) <| TBool + | Binop (And, v1, v2) -> mk_commut_binop Or (not v1) (not v2) <| TBool + | _ -> Unop (Not, sv) <| TBool +end -let rec not sv = - if equal sv v_true then v_false - else if equal sv v_false then v_true - else - match sv.node.kind with - | Unop (Not, sv) -> sv - | Binop (Lt, v1, v2) -> Binop (Leq, v2, v1) <| TBool - | Binop (Leq, v1, v2) -> Binop (Lt, v2, v1) <| TBool - | Binop (BvLt s, v1, v2) -> Binop (BvLeq s, v2, v1) <| TBool - | Binop (BvLeq s, v1, v2) -> Binop (BvLt s, v2, v1) <| TBool - | Binop (Or, v1, v2) -> mk_commut_binop And (not v1) (not v2) <| TBool - | Binop (And, v1, v2) -> mk_commut_binop Or (not v1) (not v2) <| TBool - | _ -> Unop (Not, sv) <| TBool +let conj l = List.fold_left S_bool.and_ v_true l let rec split_ands (sv : t) (f : t -> unit) : unit = match sv.node.kind with @@ -430,11 +432,11 @@ let ite guard if_ else_ = | Bool true, _, _ -> if_ | Bool false, _, _ -> else_ | _, Bool true, Bool false -> guard - | _, Bool false, Bool true -> not guard - | _, Bool false, _ -> and_ (not guard) else_ - | _, Bool true, _ -> or_ guard else_ - | _, _, Bool false -> and_ guard if_ - | _, _, Bool true -> or_ (not guard) if_ + | _, Bool false, Bool true -> S_bool.not guard + | _, Bool false, _ -> S_bool.and_ (S_bool.not guard) else_ + | _, Bool true, _ -> S_bool.or_ guard else_ + | _, _, Bool false -> S_bool.and_ guard if_ + | _, _, Bool true -> S_bool.or_ (S_bool.not guard) if_ | _, Int o, Int z when Z.equal o Z.one && Z.equal z Z.zero -> Unop (IntOfBool, guard) <| TInt | _ when equal if_ else_ -> if_ @@ -567,9 +569,8 @@ let neg v = to be seamlessly used on [TInt], without worrying about the underlying representation.*) module BitVec = struct - let bool_or = or_ - let bool_and = and_ - let bool_not = not + let bool_or = S_bool.or_ + let bool_and = S_bool.and_ (** Raw operations for values of type [TBitVector]; be careful when using these, so as to provide properly typed values. Prefer using [BitVec] @@ -770,7 +771,7 @@ module BitVec = struct && Z.(equal r1 zero) && Z.(equal r2 zero) -> ite - (bool_not (mk_commut_binop Eq b1 b2 <| TBool)) + (S_bool.not (mk_commut_binop Eq b1 b2 <| TBool)) (mk_like v1 Z.one) (mk_like v1 Z.zero) | _ -> mk_commut_binop BitXor v1 v2 <| v1.node.ty @@ -896,7 +897,7 @@ module BitVec = struct let bits = size_of_bv v1.node.ty in match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> - bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r) + S_bool.of_bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r) | _, BitVec x when Stdlib.not signed && Z.(equal x one) -> (* unsigned x < 1 is x == 0 *) mk_commut_binop Eq v1 (mk_like v1 Z.zero) <| TBool @@ -914,7 +915,8 @@ module BitVec = struct let bits = size_of_bv v1.node.ty in match (v1.node.kind, v2.node.kind) with | BitVec l, BitVec r -> - bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r) + S_bool.of_bool + @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r) | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits) -> v_true @@ -1045,7 +1047,7 @@ module BitVec = struct { node = { kind = BitVec l; _ }; _ }, { node = { kind = BitVec r; _ }; _ } ) when Z.equal l Z.zero && Z.equal r Z.one -> - int_of_bool (not b) + int_of_bool (S_bool.not b) | Ite (b, t, e) -> ite b (to_int signed t) (to_int signed e) | _ -> Unop (IntOfBv signed, v) <| t_int @@ -1060,7 +1062,7 @@ module BitVec = struct let and_ ~size ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with | Int i1, Int i2 -> int_z (Z.( land ) i1 i2) - | Bool b1, Bool b2 -> bool (b1 && b2) + | Bool b1, Bool b2 -> S_bool.of_bool (b1 && b2) | _ -> let v1_bv = of_int signed size v1 in let v2_bv = of_int signed size v2 in @@ -1070,7 +1072,7 @@ module BitVec = struct let or_ ~size ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with | Int i1, Int i2 -> int_z (Z.( lor ) i1 i2) - | Bool b1, Bool b2 -> bool (b1 || b2) + | Bool b1, Bool b2 -> S_bool.of_bool (b1 || b2) | _ -> let v1_bv = of_int signed size v1 in let v2_bv = of_int signed size v2 in @@ -1080,7 +1082,7 @@ module BitVec = struct let xor ~size ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with | Int i1, Int i2 -> int_z (Z.( lxor ) i1 i2) - | Bool b1, Bool b2 -> bool (b1 <> b2) + | Bool b1, Bool b2 -> S_bool.of_bool (b1 <> b2) | _ -> let v1_bv = of_int signed size v1 in let v2_bv = of_int signed size v2 in @@ -1142,12 +1144,14 @@ module Float = struct let lt v1 v2 = match (v1.node.kind, v2.node.kind) with - | Float f1, Float f2 -> bool (float_of_string f1 < float_of_string f2) + | Float f1, Float f2 -> + S_bool.of_bool (float_of_string f1 < float_of_string f2) | _ -> Binop (FLt, v1, v2) <| TBool let leq v1 v2 = match (v1.node.kind, v2.node.kind) with - | Float f1, Float f2 -> bool (float_of_string f1 <= float_of_string f2) + | Float f1, Float f2 -> + S_bool.of_bool (float_of_string f1 <= float_of_string f2) | _ -> Binop (FLeq, v1, v2) <| TBool let gt v1 v2 = lt v2 v1 @@ -1171,7 +1175,8 @@ module Float = struct fun sv -> match sv.node.kind with | Float f -> - bool (FloatClass.as_fpclass fc = classify_float (float_of_string f)) + S_bool.of_bool + (FloatClass.as_fpclass fc = classify_float (float_of_string f)) | _ -> Unop (FIs fc, sv) <| TBool let is_normal = is_floatclass Normal @@ -1204,7 +1209,7 @@ end let rec lt v1 v2 = match (v1.node.kind, v2.node.kind) with - | Int i1, Int i2 -> bool (Z.lt i1 i2) + | Int i1, Int i2 -> S_bool.of_bool (Z.lt i1 i2) | _, _ when equal v1 v2 -> v_false | _, Binop (Plus, v2, v3) when equal v1 v2 -> lt zero v3 | _, Binop (Plus, v2, v3) when equal v1 v3 -> lt zero v2 @@ -1230,14 +1235,14 @@ let rec lt v1 v2 = lt v1 (int_z @@ Z.sub x y) | Int y, Binop (Times, { node = { kind = Int x; _ }; _ }, v1') | Int y, Binop (Times, v1', { node = { kind = Int x; _ }; _ }) -> - if Z.equal Z.zero x then bool (Z.lt y Z.zero) + if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero) else let op = if Z.divisible y x || Z.(y > zero) then lt else leq in if Z.(zero < x) then op (int_z Z.(y / x)) v1' else op v1' (int_z Z.(y / x)) | Binop (Times, v1', { node = { kind = Int x; _ }; _ }), Int y | Binop (Times, { node = { kind = Int x; _ }; _ }, v1'), Int y -> - if Z.equal Z.zero x then bool (Z.lt Z.zero y) + if Z.equal Z.zero x then S_bool.of_bool (Z.lt Z.zero y) else let op = if Z.divisible y x || Z.(y < zero) then lt else leq in if Z.(zero < x) then op v1' (int_z Z.(y / x)) @@ -1251,7 +1256,10 @@ let rec lt v1 v2 = | Int z, Unop (IntOfBool, b) -> ( match Z.(compare z zero) with 0 -> b | 1 -> v_false | _ -> v_true) | Unop (IntOfBool, b), Int z -> ( - match Z.(compare z one) with 0 -> not b | 1 -> v_true | _ -> v_false) + match Z.(compare z one) with + | 0 -> S_bool.not b + | 1 -> v_true + | _ -> v_false) | Int _, Ite (b, t, e) -> ite b (lt v1 t) (lt v1 e) | Ite (b, t, e), Int _ -> ite b (lt t v2) (lt e v2) | _ -> ( @@ -1261,7 +1269,7 @@ let rec lt v1 v2 = and leq v1 v2 = match (v1.node.kind, v2.node.kind) with - | Int i1, Int i2 -> bool (Z.leq i1 i2) + | Int i1, Int i2 -> S_bool.of_bool (Z.leq i1 i2) | _, _ when equal v1 v2 -> v_true | _, Binop (Plus, v2, v3) when equal v1 v2 -> leq zero v3 | _, Binop (Plus, v2, v3) when equal v1 v3 -> leq zero v2 @@ -1285,14 +1293,14 @@ and leq v1 v2 = leq v1 (int_z @@ Z.sub x y) | Int y, Binop (Times, { node = { kind = Int x; _ }; _ }, v1') | Int y, Binop (Times, v1', { node = { kind = Int x; _ }; _ }) -> - if Z.equal Z.zero x then bool (Z.lt y Z.zero) + if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero) else let op = if Z.divisible y x || Z.(y < zero) then leq else lt in if Z.(zero < x) then op (int_z Z.(y / x)) v1' else op v1' (int_z Z.(y / x)) | Binop (Times, v1', { node = { kind = Int x; _ }; _ }), Int y | Binop (Times, { node = { kind = Int x; _ }; _ }, v1'), Int y -> - if Z.equal Z.zero x then bool (Z.lt y Z.zero) + if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero) else let op = if Z.divisible y x || Z.(y > zero) then leq else lt in if Z.(zero < x) then op v1' (int_z Z.(y / x)) @@ -1314,7 +1322,10 @@ and leq v1 v2 = | Int z, Unop (IntOfBool, b) -> ( match Z.(compare z one) with 0 -> b | 1 -> v_false | _ -> v_true) | Unop (IntOfBool, b), Int z -> ( - match Z.(compare z zero) with 0 -> not b | 1 -> v_true | _ -> v_false) + match Z.(compare z zero) with + | 0 -> S_bool.not b + | 1 -> v_true + | _ -> v_false) | Int _, Ite (b, t, e) -> ite b (leq v1 t) (leq v1 e) | Ite (b, t, e), Int _ -> ite b (leq t v2) (leq e v2) | _ -> ( @@ -1329,10 +1340,10 @@ let rec sem_eq v1 v2 = if equal v1 v2 && Stdlib.not (is_float v1.node.ty) then v_true else match (v1.node.kind, v2.node.kind) with - | Int z1, Int z2 -> bool (Z.equal z1 z2) - | Bool b1, Bool b2 -> bool (b1 = b2) - | Ptr (l1, o1), Ptr (l2, o2) -> and_ (sem_eq l1 l2) (sem_eq o1 o2) - | BitVec b1, BitVec b2 -> bool (Z.equal b1 b2) + | Int z1, Int z2 -> S_bool.of_bool (Z.equal z1 z2) + | Bool b1, Bool b2 -> S_bool.of_bool (b1 = b2) + | Ptr (l1, o1), Ptr (l2, o2) -> S_bool.and_ (sem_eq l1 l2) (sem_eq o1 o2) + | BitVec b1, BitVec b2 -> S_bool.of_bool (Z.equal b1 b2) | _, Binop (Plus, v2, v3) when equal v1 v2 -> sem_eq v3 zero | _, Binop (Plus, v2, v3) when equal v1 v3 -> sem_eq v2 zero | Binop (Plus, v1, v3), _ when equal v1 v2 -> sem_eq v3 zero @@ -1357,10 +1368,11 @@ let rec sem_eq v1 v2 = | Int y, Binop (Times, v1, { node = { kind = Int x; _ }; _ }) | Binop (Times, v1, { node = { kind = Int x; _ }; _ }), Int y | Binop (Times, { node = { kind = Int x; _ }; _ }, v1), Int y -> - if Z.equal Z.zero x then bool (Z.equal Z.zero y) + if Z.equal Z.zero x then S_bool.of_bool (Z.equal Z.zero y) else if Z.(equal zero (rem y x)) then sem_eq v1 (int_z Z.(y / x)) else v_false - | Unop (IntOfBool, v1), Int z -> if Z.equal Z.zero z then not v1 else v1 + | Unop (IntOfBool, v1), Int z -> + if Z.equal Z.zero z then S_bool.not v1 else v1 | Unop (IntOfBool, b1), Unop (IntOfBool, b2) -> sem_eq b1 b2 (* Reduce (X & #x...N) = #x...M to (X & #xN) = #xM *) | Binop (BitAnd, _, _), _ | _, Binop (BitAnd, _, _) -> ( @@ -1417,14 +1429,14 @@ let sem_eq_untyped v1 v2 = let not_int_bool sv = match sv.node.kind with | Int z -> if Z.equal z Z.zero then one else zero - | Unop (IntOfBool, sv') -> int_of_bool (not sv') + | Unop (IntOfBool, sv') -> int_of_bool (S_bool.not sv') | _ -> int_of_bool (sem_eq sv zero) let bool_of_int sv = match sv.node.kind with - | Int z -> bool (Stdlib.not (Z.equal z Z.zero)) + | Int z -> S_bool.of_bool (Stdlib.not (Z.equal z Z.zero)) | Unop (IntOfBool, sv') -> sv' - | _ -> not (sem_eq sv zero) + | _ -> S_bool.not (sem_eq sv zero) (** {2 Pointers} *) @@ -1476,8 +1488,8 @@ module Infix = struct let ( >=@ ) = geq let ( <@ ) = lt let ( <=@ ) = leq - let ( &&@ ) = and_ - let ( ||@ ) = or_ + let ( &&@ ) = S_bool.and_ + let ( ||@ ) = S_bool.or_ let ( +@ ) = plus let ( -@ ) = minus let ( ~- ) = neg diff --git a/soteria/lib/c_values/typed.ml b/soteria/lib/c_values/typed.ml index f3cf11c27..5ca5dd3f0 100644 --- a/soteria/lib/c_values/typed.ml +++ b/soteria/lib/c_values/typed.ml @@ -26,7 +26,12 @@ end type nonrec +'a t = t type nonrec +'a ty = ty -type sbool = T.sbool + +module S_bool = struct + type t = T.sbool + + include S_bool +end let[@inline] get_ty x = x.node.ty let[@inline] untype_type x = x diff --git a/soteria/lib/c_values/typed.mli b/soteria/lib/c_values/typed.mli index 48d54d351..8f3a9b6ba 100644 --- a/soteria/lib/c_values/typed.mli +++ b/soteria/lib/c_values/typed.mli @@ -49,9 +49,9 @@ val t_f128 : [> sfloat ] ty (** {2 Typed svalues} *) type +'a t -type sbool = T.sbool +type sbool := T.sbool -(** Basic value operations *) +(** {3 Basic value operations} *) val get_ty : 'a t -> Svalue.ty val untype_type : 'a ty -> Svalue.ty @@ -74,19 +74,25 @@ val equal : ([< any ] as 'a) t -> 'a t -> bool val compare : ([< any ] as 'a) t -> 'a t -> int val hash : [< any ] t -> int -(** Typed constructors *) +(** {3 Typed constructors} *) + +module S_bool : sig + type +'a v := 'a t + type t = sbool + + val of_bool : bool -> [> sbool ] v + val to_bool : [< sbool ] v -> bool option + val and_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v + val or_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v + val not : [< sbool ] v -> [> sbool ] v +end val sem_eq : 'a t -> 'a t -> sbool t val sem_eq_untyped : 'a t -> 'a t -> [> sbool ] t val v_true : [> sbool ] t val v_false : [> sbool ] t -val bool : bool -> [> sbool ] t -val as_bool : 'a t -> bool option -val and_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t val conj : [< sbool ] t list -> [> sbool ] t val split_ands : [< sbool ] t -> ([> sbool ] t -> unit) -> unit -val or_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t -val not : sbool t -> sbool t val not_int_bool : [< sint ] t -> [> sint ] t val distinct : 'a t list -> [> sbool ] t val ite : [< sbool ] t -> 'a t -> 'a t -> 'a t @@ -99,7 +105,7 @@ val bool_of_int : [< sint ] t -> [> sbool ] t val zero : [> sint ] t val one : [> nonzero ] t -(** Integer operations *) +(** {3 Integer operations} *) val geq : [< sint ] t -> [< sint ] t -> [> sbool ] t val gt : [< sint ] t -> [< sint ] t -> [> sbool ] t diff --git a/soteria/lib/sym_data/s_eq.ml b/soteria/lib/sym_data/s_eq.ml index 26f583481..8bcb14cac 100644 --- a/soteria/lib/sym_data/s_eq.ml +++ b/soteria/lib/sym_data/s_eq.ml @@ -14,12 +14,12 @@ module type S = sig val equal : t -> t -> bool (** Symbolic semantic equality *) - val sem_eq : t -> t -> Symex.Value.sbool Symex.Value.t + val sem_eq : t -> t -> Symex.Value.S_bool.t Symex.Value.t (** Receives a list of {e syntactically different} values and returns a symbolic boolean corresponding to the fact that these values are also {e semantically} distinct. *) - val distinct : t list -> Symex.Value.sbool Symex.Value.t + val distinct : t list -> Symex.Value.S_bool.t Symex.Value.t end module Of_concrete @@ -32,8 +32,8 @@ module Of_concrete module Symex = Symex include C - let sem_eq x y = Symex.Value.bool (C.equal x y) + let sem_eq x y = Symex.Value.S_bool.of_bool (C.equal x y) (* Always returns true as the input list should always be syntactically distinct *) - let distinct _ = Symex.Value.bool true + let distinct _ = Symex.Value.S_bool.of_bool true end diff --git a/soteria/lib/sym_states/plist.ml b/soteria/lib/sym_states/plist.ml index d10296312..2fa66ecf9 100644 --- a/soteria/lib/sym_states/plist.ml +++ b/soteria/lib/sym_states/plist.ml @@ -11,7 +11,7 @@ module type SInt_sig = sig include Stdlib.Map.OrderedType with type t := t - type sbool_v := Value.sbool Value.t + type sbool_v := Value.S_bool.t Value.t val pp : Format.formatter -> t -> unit val sem_eq : t -> t -> sbool_v @@ -78,7 +78,8 @@ struct | None -> SInt.greater_or_equal ofs (SInt.of_int 0) | Some b -> SInt.in_range ofs (SInt.of_int 0, b) in - if%sat Symex.Value.not cond then Result.error `OutOfBounds else Result.ok () + if%sat Symex.Value.S_bool.not cond then Result.error `OutOfBounds + else Result.ok () let create (size : int) ~(new_codom : 'a) : 'a t = if size <= 0 then diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml index ae924e5ad..718efcb98 100644 --- a/soteria/lib/sym_states/pmap.ml +++ b/soteria/lib/sym_states/pmap.ml @@ -6,7 +6,7 @@ module type KeyS = sig module Symex : Symex.S include Stdlib.Map.OrderedType with type t := t - type sbool_v := Symex.Value.sbool Symex.Value.t + type sbool_v := Symex.Value.S_bool.t Symex.Value.t val pp : Format.formatter -> t -> unit val sem_eq : t -> t -> sbool_v @@ -21,9 +21,9 @@ module Mk_concrete_key (Symex : Symex.S) (Key : Soteria_std.Ordered_type.S) : module Symex = Symex include Key - let sem_eq x y = Symex.Value.bool (Key.compare x y = 0) + let sem_eq x y = Symex.Value.S_bool.of_bool (Key.compare x y = 0) let fresh () = failwith "Fresh not implemented for concrete keys" - let distinct _ = Symex.Value.bool true + let distinct _ = Symex.Value.S_bool.of_bool true let subst _ x = x let iter_vars _ = fun _ -> () end diff --git a/soteria/lib/sym_states/pure_fun.ml b/soteria/lib/sym_states/pure_fun.ml index 3cfe8a477..a52434edd 100644 --- a/soteria/lib/sym_states/pure_fun.ml +++ b/soteria/lib/sym_states/pure_fun.ml @@ -13,7 +13,7 @@ module type Codom = sig val pp : Format.formatter -> t -> unit val fresh : unit -> t Symex.t - val sem_eq : t -> t -> Symex.Value.sbool Symex.Value.t + val sem_eq : t -> t -> Symex.Value.S_bool.t Symex.Value.t val subst : (Var.t -> Var.t) -> t -> t val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars end diff --git a/soteria/lib/sym_states/tree_block.ml b/soteria/lib/sym_states/tree_block.ml index 85f2aab59..d01b24410 100644 --- a/soteria/lib/sym_states/tree_block.ml +++ b/soteria/lib/sym_states/tree_block.ml @@ -123,7 +123,7 @@ module Make MemVal with module Symex = Symex and type 'a SInt.t = 'a Symex.Value.t - and type SInt.sbool = Symex.Value.sbool) = + and type SInt.sbool = Symex.Value.S_bool.t) = struct open Compo_res open Symex.Syntax diff --git a/soteria/lib/symex/solver.ml b/soteria/lib/symex/solver.ml index 1c77a367b..95da98169 100644 --- a/soteria/lib/symex/solver.ml +++ b/soteria/lib/symex/solver.ml @@ -6,7 +6,7 @@ module type Mutable_incremental = sig include Reversible.Mutable module Value : Value.S - type sbool_v := Value.sbool Value.t + type sbool_v := Value.S_bool.t Value.t (** Adds constraints to the solver state. The [simplified] flag indicates if {!simplify} was already applied to the constraints, and is [false] by @@ -24,8 +24,10 @@ module type In_place_incremental = sig include Reversible.In_place module Value : Value.S + type sbool_v := Value.S_bool.t Value.t + (** simplified indicates if constraits were already simplified *) - val add_constraints : ?simplified:bool -> Value.sbool Value.t list -> unit + val add_constraints : ?simplified:bool -> sbool_v list -> unit val sat : unit -> bool diff --git a/soteria/lib/symex/symex.ml b/soteria/lib/symex/symex.ml index 64bab15ef..1e090642f 100644 --- a/soteria/lib/symex/symex.ml +++ b/soteria/lib/symex/symex.ml @@ -57,11 +57,11 @@ module type S = sig Use this instead of [`Lfail] directly in type signatures to avoid potential typos such as [`LFail] which will take precious time to debug... trust me. *) - type lfail = [ `Lfail of Value.sbool Value.t ] + type lfail = [ `Lfail of Value.S_bool.t Value.t ] type 'a v := 'a Value.t type 'a vt := 'a Value.ty - type sbool := Value.sbool + type sbool := Value.S_bool.t val assume : sbool v list -> unit t val vanish : unit -> 'a t @@ -205,14 +205,14 @@ module type S = sig ?fuel:Fuel_gauge.t -> mode:Approx.t -> ('ok, 'err, 'fix) t -> - (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list) + (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list) list val run_with_stats : ?fuel:Fuel_gauge.t -> mode:Approx.t -> ('ok, 'err, 'fix) t -> - (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list) + (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list) list Stats.with_stats @@ -220,7 +220,7 @@ module type S = sig ?fuel:Fuel_gauge.t -> mode:Approx.t -> ('ok, 'err, 'fix) t -> - (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list) + (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list) list val ok : 'ok -> ('ok, 'err, 'fix) t @@ -269,7 +269,7 @@ module type S = sig val ( let+? ) : ('a, 'b, 'c) Result.t -> ('c -> 'd) -> ('a, 'b, 'd) Result.t module Symex_syntax : sig - type sbool_v := Value.sbool Value.t + type sbool_v := Value.S_bool.t Value.t val branch_on : ?left_branch_name:string -> @@ -336,7 +336,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : end type 'a t = 'a Iter.t - type lfail = [ `Lfail of Value.sbool Value.t ] + type lfail = [ `Lfail of Value.S_bool.t Value.t ] module Symex_state : Reversible.In_place = struct let backtrack_n n = @@ -367,7 +367,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : f () | l :: ls -> ( let l = Solver.simplify l in - match Value.as_bool l with + match Value.S_bool.to_bool l with | Some true -> aux acc ls | Some false -> L.trace (fun m -> m "Assuming false, stopping this branch") @@ -380,7 +380,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : side-effects at the wrong time. *) let assert_raw value : bool = let value = Solver.simplify value in - match Value.as_bool value with + match Value.S_bool.to_bool value with | Some true -> true | Some false -> false | None -> @@ -388,7 +388,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : L.with_section (Fmt.str "Checking entailment for %a" Value.ppa value) in Symex_state.save (); - Solver.add_constraints [ Value.(not value) ]; + Solver.add_constraints [ Value.S_bool.not value ]; let sat_result = Solver.sat () in Symex_state.backtrack_n 1; if Approx.As_ctx.is_ux () then not (Solver_result.is_sat sat_result) @@ -408,7 +408,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : let consume_false () f = if Approx.As_ctx.is_ux () then () - else f (Compo_res.Error (`Lfail (Value.bool false))) + else f (Compo_res.Error (`Lfail (Value.S_bool.of_bool false))) let nondet ty f = let v = Solver.fresh_var ty in @@ -422,7 +422,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : ~(else_ : unit -> 'a Iter.t) : 'a Iter.t = fun f -> let guard = Solver.simplify guard in - match Value.as_bool guard with + match Value.S_bool.to_bool guard with (* [then_] and [else_] could be ['a t] instead of [unit -> 'a t], if we remove the Some true and Some false optimisation. *) | Some true -> then_ () f @@ -438,7 +438,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : else L.trace (fun m -> m "Branch is not feasible")); Symex_state.backtrack_n 1; L.with_section ~is_branch:true right_branch_name (fun () -> - Solver.add_constraints [ Value.(not guard) ]; + Solver.add_constraints [ Value.S_bool.not guard ]; if !left_unsat then (* Right must be sat since left was not! We didn't branch so we don't consume the counter *) else_ () f @@ -478,7 +478,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : ~then_ ~else_ : 'a Iter.t = fun f -> let guard = Solver.simplify guard in - match Value.as_bool guard with + match Value.S_bool.to_bool guard with | Some true -> then_ () f | Some false -> else_ () f | None -> @@ -488,7 +488,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : if left_sat then then_ () f; Symex_state.backtrack_n 1; if not left_sat then ( - Solver.add_constraints [ Value.(not guard) ]; + Solver.add_constraints [ Value.S_bool.not guard ]; else_ () f) let branch_on_take_one ?left_branch_name ?right_branch_name guard ~then_ diff --git a/soteria/lib/symex/value.ml b/soteria/lib/symex/value.ml index f63dd8123..d09c7d84c 100644 --- a/soteria/lib/symex/value.ml +++ b/soteria/lib/symex/value.ml @@ -1,14 +1,21 @@ module type S = sig type +'a t type +'a ty - type sbool - val not : sbool t -> sbool t - val sem_eq : 'a t -> 'a t -> sbool t + module S_bool : sig + type +'a v := 'a t + type t + + val not : t v -> t v + val and_ : t v -> t v -> t v + val or_ : t v -> t v -> t v + val to_bool : t v -> bool option + val of_bool : bool -> t v + end + + val sem_eq : 'a t -> 'a t -> S_bool.t t val ppa : Format.formatter -> 'a t -> unit val iter_vars : 'a t -> 'b ty Var.iter_vars val subst : (Var.t -> Var.t) -> 'a t -> 'a t val mk_var : Var.t -> 'a ty -> 'a t - val as_bool : 'a t -> bool option - val bool : bool -> sbool t end diff --git a/soteria/tests/symex/run_twice.ml b/soteria/tests/symex/run_twice.ml index 59329a87e..74df4fb80 100644 --- a/soteria/tests/symex/run_twice.ml +++ b/soteria/tests/symex/run_twice.ml @@ -21,7 +21,7 @@ let fn () = let open Typed.Infix in let* v = nondet Typed.t_int in let* () = assume [ v ==@ Typed.zero ] in - if%sat Typed.not (v ==@ Typed.one) then return true else return false + if%sat Typed.S_bool.not (v ==@ Typed.one) then return true else return false let do_test () = let pp = diff --git a/soteria/tutorial/core_symex.mld b/soteria/tutorial/core_symex.mld index 316c2301d..1c17c0d5a 100644 --- a/soteria/tutorial/core_symex.mld +++ b/soteria/tutorial/core_symex.mld @@ -37,7 +37,7 @@ Executing a symbolic process is done using the {{!Soteria.Symex.S.run}run} funct # Symex.run - : ?fuel:Symex.Fuel_gauge.t -> mode:Symex.Approx.t -> - 'a Symex.t -> ('a * Symex.Value.sbool Typed.t list) list + 'a Symex.t -> ('a * Symex.Value.S_bool.t Typed.t list) list = ]} @@ -47,7 +47,7 @@ For instance, let's execute the symbolic process we just created, using the {{!S {@ocaml[ # Symex.return 0 |> Symex.run ~mode:OX;; -- : (int * Symex.Value.sbool Typed.t list) list = [(0, [])]]} +- : (int * Symex.Value.S_bool.t Typed.t list) list = [(0, [])]]} ]} As expected the result of the symbolic process is a single branch with the value [0] and an empty path condition [[]], which means that there is no condition for taking this branch, i.e., it is always taken. @@ -67,7 +67,7 @@ Let's run this process: {@ocaml[ # Symex.nondet Typed.t_int |> Symex.run ~mode:OX;; -- : ([> Typed.T.sint ] Typed.t * Symex.Value.sbool Typed.t list) list = +- : ([> Typed.T.sint ] Typed.t * Symex.Value.S_bool.t Typed.t list) list = [(V|1|, [])] ]} @@ -108,7 +108,8 @@ Running this symbolic process yields a single branch with no path condition: {@ocaml[ # Symex.run ~mode:OX process;; -- : (([> Typed.T.sint ] as '_weak1) Typed.t * Symex.Value.sbool Typed.t list) +- : (([> Typed.T.sint ] as '_weak1) Typed.t * + Symex.Value.S_bool.t Typed.t list) list = [((V|1| + 2), [])] ]} @@ -124,7 +125,7 @@ For instance, we can create a symbolic process that introduces a nondeterministi val process : bool Symex.t = # Symex.run ~mode:OX process;; -- : (bool * Symex.Value.sbool Typed.t list) list = [(false, [])] +- : (bool * Symex.Value.S_bool.t Typed.t list) list = [(false, [])] ]} This process returns a single branch with the value [false], as it is not *always* guaranteed that the symbolic integer [x] is positive. Now, if we add an assumption that, say, [x] is greater than 10, we get a different result: @@ -137,7 +138,8 @@ This process returns a single branch with the value [false], as it is not *alway val process : bool Symex.t = # Symex.run ~mode:OX process;; -- : (bool * Symex.Value.sbool Typed.t list) list = [(true, [(11 <= V|1|)])] +- : (bool * Symex.Value.S_bool.t Typed.t list) list = +[(true, [(11 <= V|1|)])] ]} This time, the assertion is satisfied, and the symbolic process returns a single branch with value [true], and a path condition that corresponds to the assumption we made, i.e. that [V|1|] (the symbolic integer) is greater than or equal to 11 (which is equivalent to the assumption we wrote). @@ -156,7 +158,7 @@ A more interesting symbolic process is one that introduces conditional branching val process : string Symex.t = # Symex.run ~mode:OX process;; -- : (string * Symex.Value.sbool Typed.t list) list = +- : (string * Symex.Value.S_bool.t Typed.t list) list = [("V|1| is even", [(0 == (V|1| mod 2))]); ("V|1| is odd", [(0 != (V|1| mod 2))])] ]} From a14070fe9af5d1ce121c8a786491d3d443815543 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 18:28:21 +0100 Subject: [PATCH 11/22] S_elt is printable Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_elt.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/soteria/lib/sym_data/s_elt.ml b/soteria/lib/sym_data/s_elt.ml index c2e338702..e673e02b8 100644 --- a/soteria/lib/sym_data/s_elt.ml +++ b/soteria/lib/sym_data/s_elt.ml @@ -7,6 +7,7 @@ module type S = sig type t + include Soteria_std.Printable.S with type t := t module Symex : Symex.S val subst : (Var.t -> Var.t) -> t -> t From 7e9c4602daabe7c835cd8e41a833f914ca6e749c Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 18:37:58 +0100 Subject: [PATCH 12/22] Symbolic ranges Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_int.ml | 6 +++-- soteria/lib/sym_data/s_range.ml | 45 ++++++++++++++++++++++++++++++++ soteria/lib/sym_data/sym_data.ml | 1 + 3 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 soteria/lib/sym_data/s_range.ml diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml index 8f42fe8dc..2d81479a0 100644 --- a/soteria/lib/sym_data/s_int.ml +++ b/soteria/lib/sym_data/s_int.ml @@ -13,8 +13,10 @@ module type S = sig (** {3 Arithmetic operations} *) + type sbool_v := Symex.Value.S_bool.t Symex.Value.t + val ( +@ ) : t -> t -> t val ( -@ ) : t -> t -> t - val ( <@ ) : t -> t -> t - val ( <=@ ) : t -> t -> t + val ( <@ ) : t -> t -> sbool_v + val ( <=@ ) : t -> t -> sbool_v end diff --git a/soteria/lib/sym_data/s_range.ml b/soteria/lib/sym_data/s_range.ml new file mode 100644 index 000000000..eddab0359 --- /dev/null +++ b/soteria/lib/sym_data/s_range.ml @@ -0,0 +1,45 @@ +(** Symbolic abstractions over ranges. *) + +module Make (S_int : S_int.S) = struct + module Symex = S_int.Symex + + type sbool = Symex.Value.S_bool.t Symex.Value.t + + (** Type of value representing the bounds of the interval *) + type v = S_int.t + + (** A value [(a, b)] of type [t] represents the interval starting at [a] + {e included} and ending at [b] {e excluded}. Often denoted {m [a, b)} or + {m [a, b[}*) + type t = v * v + + open S_int + + let sem_eq (a1, b1) (a2, b2) = + Symex.Value.S_bool.and_ (S_int.sem_eq a1 a2) (S_int.sem_eq b1 b2) + + (** [size (a, b)] is [b - a] *) + let size (a, b) = b -@ a + + (** [split_at (a, b) x] is [(a, x), (x, b)] *) + let split_at (l, h) x = ((l, x), (x, h)) + + (** [offset (a, b) x] is [(a + x, b + x)] *) + let offset (l, h) x = (l +@ x, h +@ x) + + (** [subseteq r1 r2] is a symbolic boolean characterising whether [r1] is a + subset of [r2] *) + let subset_eq (a1, b1) (a2, b2) = + Symex.Value.S_bool.and_ (a2 <=@ a1) (b1 <=@ b2) + + (** [subset_strict r1 r2] is a symbolic boolean characterising whether [r1] is + a strict subset of [r2] (i.e. it is equivalent to + [(subseteq r1 r2) && not (sem_eq r1 r2)]) *) + let subset_strict (a1, b1) (a2, b2) = + Symex.Value.S_bool.and_ (a2 <@ a1) (b1 <@ b2) + + (** [of_low_and_size a b] is [(a, a + b)]*) + let of_low_and_size low size = (low, low +@ size) + + let pp fmt (a, b) = Format.fprintf fmt "[%a, %a[" S_int.pp a S_int.pp b +end diff --git a/soteria/lib/sym_data/sym_data.ml b/soteria/lib/sym_data/sym_data.ml index 89261cc8f..0e64766db 100644 --- a/soteria/lib/sym_data/sym_data.ml +++ b/soteria/lib/sym_data/sym_data.ml @@ -3,4 +3,5 @@ module S_elt = S_elt module S_eq = S_eq module S_int = S_int +module S_range = S_range module S_map = S_map From cd9426321b8398b5809842cca178e9b84c4bbb1e Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 18:44:53 +0100 Subject: [PATCH 13/22] S_int doesn't use infix Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_int.ml | 11 +++++++---- soteria/lib/sym_data/s_range.ml | 10 +++++----- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml index 2d81479a0..099b6bf41 100644 --- a/soteria/lib/sym_data/s_int.ml +++ b/soteria/lib/sym_data/s_int.ml @@ -11,12 +11,15 @@ module type S = sig describes exactly a single integer, and [None] otherwise *) val to_z : t -> Z.t option + val zero : t + val one : t + (** {3 Arithmetic operations} *) type sbool_v := Symex.Value.S_bool.t Symex.Value.t - val ( +@ ) : t -> t -> t - val ( -@ ) : t -> t -> t - val ( <@ ) : t -> t -> sbool_v - val ( <=@ ) : t -> t -> sbool_v + val add : t -> t -> t + val minus : t -> t -> t + val lt : t -> t -> sbool_v + val leq : t -> t -> sbool_v end diff --git a/soteria/lib/sym_data/s_range.ml b/soteria/lib/sym_data/s_range.ml index eddab0359..53de28c96 100644 --- a/soteria/lib/sym_data/s_range.ml +++ b/soteria/lib/sym_data/s_range.ml @@ -19,27 +19,27 @@ module Make (S_int : S_int.S) = struct Symex.Value.S_bool.and_ (S_int.sem_eq a1 a2) (S_int.sem_eq b1 b2) (** [size (a, b)] is [b - a] *) - let size (a, b) = b -@ a + let size (a, b) = minus b a (** [split_at (a, b) x] is [(a, x), (x, b)] *) let split_at (l, h) x = ((l, x), (x, h)) (** [offset (a, b) x] is [(a + x, b + x)] *) - let offset (l, h) x = (l +@ x, h +@ x) + let offset (l, h) x = (add l x, add h x) (** [subseteq r1 r2] is a symbolic boolean characterising whether [r1] is a subset of [r2] *) let subset_eq (a1, b1) (a2, b2) = - Symex.Value.S_bool.and_ (a2 <=@ a1) (b1 <=@ b2) + Symex.Value.S_bool.and_ (leq a2 a1) (leq b1 b2) (** [subset_strict r1 r2] is a symbolic boolean characterising whether [r1] is a strict subset of [r2] (i.e. it is equivalent to [(subseteq r1 r2) && not (sem_eq r1 r2)]) *) let subset_strict (a1, b1) (a2, b2) = - Symex.Value.S_bool.and_ (a2 <@ a1) (b1 <@ b2) + Symex.Value.S_bool.and_ (lt a2 a1) (lt b1 b2) (** [of_low_and_size a b] is [(a, a + b)]*) - let of_low_and_size low size = (low, low +@ size) + let of_low_and_size low size = (low, add low size) let pp fmt (a, b) = Format.fprintf fmt "[%a, %a[" S_int.pp a S_int.pp b end From 6b3244d761f3152aa7e106e666496b1e2133e21d Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 18:47:29 +0100 Subject: [PATCH 14/22] Make_syntax for S_int Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_int.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml index 099b6bf41..4619c81ae 100644 --- a/soteria/lib/sym_data/s_int.ml +++ b/soteria/lib/sym_data/s_int.ml @@ -23,3 +23,16 @@ module type S = sig val lt : t -> t -> sbool_v val leq : t -> t -> sbool_v end + +module Make_syntax (S_int : S) = struct + let ( +@ ) = S_int.add + let ( -@ ) = S_int.minus + let ( <@ ) = S_int.lt + let ( <=@ ) = S_int.leq + + module Sym_int_syntax = struct + let mk_nonzero x = S_int.of_z (Z.of_int x) + let zero = S_int.zero + let one = S_int.one + end +end From 6a4556cbd17b5c7c349976a76ad18da3cecacb83 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 21:18:46 +0100 Subject: [PATCH 15/22] syntaxes Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_eq.ml | 4 ++++ soteria/lib/sym_data/s_int.ml | 15 +++++++++------ soteria/lib/symex/value.ml | 22 ++++++++++++++++------ 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/soteria/lib/sym_data/s_eq.ml b/soteria/lib/sym_data/s_eq.ml index 8bcb14cac..7c6d9fa37 100644 --- a/soteria/lib/sym_data/s_eq.ml +++ b/soteria/lib/sym_data/s_eq.ml @@ -22,6 +22,10 @@ module type S = sig val distinct : t list -> Symex.Value.S_bool.t Symex.Value.t end +module Make_syntax (S : S) = struct + let ( ==@ ) = S.sem_eq +end + module Of_concrete (Symex : Symex.S) (C : sig diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml index 4619c81ae..a1882845d 100644 --- a/soteria/lib/sym_data/s_int.ml +++ b/soteria/lib/sym_data/s_int.ml @@ -3,6 +3,7 @@ module type S = sig include S_elt.S include S_eq.S with module Symex := Symex and type t := t + include Soteria_std.Printable.S with type t := t (** Takes an integer and creates an abstraction over it *) val of_z : Z.t -> t @@ -11,8 +12,8 @@ module type S = sig describes exactly a single integer, and [None] otherwise *) val to_z : t -> Z.t option - val zero : t - val one : t + val zero : unit -> t + val one : unit -> t (** {3 Arithmetic operations} *) @@ -25,10 +26,12 @@ module type S = sig end module Make_syntax (S_int : S) = struct - let ( +@ ) = S_int.add - let ( -@ ) = S_int.minus - let ( <@ ) = S_int.lt - let ( <=@ ) = S_int.leq + include S_eq.Make_syntax (S_int) + + let[@inline] ( +@ ) = S_int.add + let[@inline] ( -@ ) = S_int.minus + let[@inline] ( <@ ) = S_int.lt + let[@inline] ( <=@ ) = S_int.leq module Sym_int_syntax = struct let mk_nonzero x = S_int.of_z (Z.of_int x) diff --git a/soteria/lib/symex/value.ml b/soteria/lib/symex/value.ml index d09c7d84c..3edd065c2 100644 --- a/soteria/lib/symex/value.ml +++ b/soteria/lib/symex/value.ml @@ -1,9 +1,6 @@ -module type S = sig - type +'a t - type +'a ty - - module S_bool : sig - type +'a v := 'a t +module S_bool = struct + module type S = sig + type +'a v type t val not : t v -> t v @@ -13,6 +10,19 @@ module type S = sig val of_bool : bool -> t v end + module Make_syntax (S_bool : S) = struct + let[@inline] ( &&@ ) = S_bool.and_ + let[@inline] ( ||@ ) = S_bool.or_ + let[@inline] not = S_bool.not + end +end + +module type S = sig + type +'a t + type +'a ty + + module S_bool : S_bool.S with type +'a v := 'a t + val sem_eq : 'a t -> 'a t -> S_bool.t t val ppa : Format.formatter -> 'a t -> unit val iter_vars : 'a t -> 'b ty Var.iter_vars From 4445595e8e6fb343ac650695e4bc1933b06f1eb6 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 21:18:51 +0100 Subject: [PATCH 16/22] this is actually what I need Signed-off-by: Sacha Ayoun --- soteria/lib/sym_data/s_range.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/soteria/lib/sym_data/s_range.ml b/soteria/lib/sym_data/s_range.ml index 53de28c96..a253daff4 100644 --- a/soteria/lib/sym_data/s_range.ml +++ b/soteria/lib/sym_data/s_range.ml @@ -32,11 +32,8 @@ module Make (S_int : S_int.S) = struct let subset_eq (a1, b1) (a2, b2) = Symex.Value.S_bool.and_ (leq a2 a1) (leq b1 b2) - (** [subset_strict r1 r2] is a symbolic boolean characterising whether [r1] is - a strict subset of [r2] (i.e. it is equivalent to - [(subseteq r1 r2) && not (sem_eq r1 r2)]) *) - let subset_strict (a1, b1) (a2, b2) = - Symex.Value.S_bool.and_ (lt a2 a1) (lt b1 b2) + (** [strictly_inside (a, b) r] is [a < r < b] *) + let strictly_inside x (a, b) = Symex.Value.S_bool.and_ (lt a x) (lt x b) (** [of_low_and_size a b] is [(a, a + b)]*) let of_low_and_size low size = (low, add low size) From 614464845daa50ab6cea93bdd5ba8f828fe1de75 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 21:48:31 +0100 Subject: [PATCH 17/22] more juggling around Signed-off-by: Sacha Ayoun --- soteria/lib/bv_values/typed.ml | 1 + soteria/lib/bv_values/typed.mli | 11 +---------- soteria/lib/c_values/svalue.ml | 1 + soteria/lib/c_values/typed.ml | 1 + soteria/lib/c_values/typed.mli | 12 ++---------- soteria/lib/sym_data/s_int.ml | 8 ++++---- soteria/lib/symex/value.ml | 8 ++++---- 7 files changed, 14 insertions(+), 28 deletions(-) diff --git a/soteria/lib/bv_values/typed.ml b/soteria/lib/bv_values/typed.ml index bbcd831b5..810dffc3b 100644 --- a/soteria/lib/bv_values/typed.ml +++ b/soteria/lib/bv_values/typed.ml @@ -35,6 +35,7 @@ let t_int = t_bv include S_bool module S_bool = struct + type +'a v = 'a t type t = T.sbool include S_bool diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli index d235d0a41..62af1bcee 100644 --- a/soteria/lib/bv_values/typed.mli +++ b/soteria/lib/bv_values/typed.mli @@ -63,16 +63,7 @@ val t_f : Svalue.FloatPrecision.t -> [> sfloat ] ty type +'a t -module S_bool : sig - type +'a v := 'a t - type t = sbool - - val of_bool : bool -> [> sbool ] v - val to_bool : [< sbool ] v -> bool option - val and_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v - val or_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v - val not : [< sbool ] v -> [> sbool ] v -end +module S_bool : Symex.Value.S_bool.S with type 'a v = 'a t and type t = sbool type sbool := T.sbool diff --git a/soteria/lib/c_values/svalue.ml b/soteria/lib/c_values/svalue.ml index f8e3b5cd7..04a256d49 100644 --- a/soteria/lib/c_values/svalue.ml +++ b/soteria/lib/c_values/svalue.ml @@ -445,6 +445,7 @@ let ite guard if_ else_ = (** {2 Integers} *) let int_z z = Int z <| TInt +let to_z v = match v.node.kind with Int z -> Some z | _ -> None let int i = int_z (Z.of_int i) let nonzero_z z = diff --git a/soteria/lib/c_values/typed.ml b/soteria/lib/c_values/typed.ml index 5ca5dd3f0..f78aa7cd3 100644 --- a/soteria/lib/c_values/typed.ml +++ b/soteria/lib/c_values/typed.ml @@ -28,6 +28,7 @@ type nonrec +'a t = t type nonrec +'a ty = ty module S_bool = struct + type +'a v = 'a t type t = T.sbool include S_bool diff --git a/soteria/lib/c_values/typed.mli b/soteria/lib/c_values/typed.mli index 8f3a9b6ba..7f6fe5fc9 100644 --- a/soteria/lib/c_values/typed.mli +++ b/soteria/lib/c_values/typed.mli @@ -76,16 +76,7 @@ val hash : [< any ] t -> int (** {3 Typed constructors} *) -module S_bool : sig - type +'a v := 'a t - type t = sbool - - val of_bool : bool -> [> sbool ] v - val to_bool : [< sbool ] v -> bool option - val and_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v - val or_ : [< sbool ] v -> [< sbool ] v -> [> sbool ] v - val not : [< sbool ] v -> [> sbool ] v -end +module S_bool : Symex.Value.S_bool.S with type 'a v = 'a t and type t = sbool val sem_eq : 'a t -> 'a t -> sbool t val sem_eq_untyped : 'a t -> 'a t -> [> sbool ] t @@ -98,6 +89,7 @@ val distinct : 'a t list -> [> sbool ] t val ite : [< sbool ] t -> 'a t -> 'a t -> 'a t val int_z : Z.t -> [> sint ] t val int : int -> [> sint ] t +val to_z : [< sint ] t -> Z.t option val nonzero_z : Z.t -> [> nonzero ] t val nonzero : int -> [> nonzero ] t val int_of_bool : [< sbool ] t -> [> sint ] t diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml index a1882845d..8c4936a96 100644 --- a/soteria/lib/sym_data/s_int.ml +++ b/soteria/lib/sym_data/s_int.ml @@ -28,10 +28,10 @@ end module Make_syntax (S_int : S) = struct include S_eq.Make_syntax (S_int) - let[@inline] ( +@ ) = S_int.add - let[@inline] ( -@ ) = S_int.minus - let[@inline] ( <@ ) = S_int.lt - let[@inline] ( <=@ ) = S_int.leq + let ( +@ ) = S_int.add + let ( -@ ) = S_int.minus + let ( <@ ) = S_int.lt + let ( <=@ ) = S_int.leq module Sym_int_syntax = struct let mk_nonzero x = S_int.of_z (Z.of_int x) diff --git a/soteria/lib/symex/value.ml b/soteria/lib/symex/value.ml index 3edd065c2..340d5bfb1 100644 --- a/soteria/lib/symex/value.ml +++ b/soteria/lib/symex/value.ml @@ -11,9 +11,9 @@ module S_bool = struct end module Make_syntax (S_bool : S) = struct - let[@inline] ( &&@ ) = S_bool.and_ - let[@inline] ( ||@ ) = S_bool.or_ - let[@inline] not = S_bool.not + let ( &&@ ) = S_bool.and_ + let ( ||@ ) = S_bool.or_ + let not = S_bool.not end end @@ -21,7 +21,7 @@ module type S = sig type +'a t type +'a ty - module S_bool : S_bool.S with type +'a v := 'a t + module S_bool : S_bool.S with type +'a v = 'a t val sem_eq : 'a t -> 'a t -> S_bool.t t val ppa : Format.formatter -> 'a t -> unit From 186ce51033e59292972d58af8665dc4b28e9858e Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 10 Sep 2025 21:49:03 +0100 Subject: [PATCH 18/22] let's go! Tree_block now uses proper S_int Signed-off-by: Sacha Ayoun --- soteria-c/lib/ctree_block.ml | 12 +++-- soteria-rust/lib/rtree_block.ml | 18 ++++--- soteria/lib/sym_states/tree_block.ml | 70 +++++++--------------------- 3 files changed, 38 insertions(+), 62 deletions(-) diff --git a/soteria-c/lib/ctree_block.ml b/soteria-c/lib/ctree_block.ml index bcdae9464..b6fd590b1 100644 --- a/soteria-c/lib/ctree_block.ml +++ b/soteria-c/lib/ctree_block.ml @@ -11,14 +11,20 @@ module MemVal = struct module TB = Soteria.Sym_states.Tree_block module Symex = Csymex - module SInt = struct + module S_int = struct + module Symex = Csymex include Typed include Typed.Infix - type sint = T.sint - type sbool = T.sbool + type t = T.sint Typed.t let[@inline] zero () = zero + let[@inline] one () = one + let of_z = Typed.int_z + let to_z = Typed.to_z + let pp = Typed.ppa + let add = Typed.plus + let sub = Typed.minus end let pp_init ft (v, ty) = diff --git a/soteria-rust/lib/rtree_block.ml b/soteria-rust/lib/rtree_block.ml index 8bb7d8d19..629f3e699 100644 --- a/soteria-rust/lib/rtree_block.ml +++ b/soteria-rust/lib/rtree_block.ml @@ -17,18 +17,22 @@ module Make (Sptr : Sptr.S) = struct module TB = Soteria.Sym_states.Tree_block module Symex = Rustsymex - module SInt = struct + module S_int = struct + module Symex = Rustsymex include Typed include Typed.Infix - type sint = T.sint - type sbool = T.sbool + type t = T.sint Typed.t + let pp = ppa let zero () = Typed.BitVec.usize Z.zero - let ( <@ ) = Typed.Infix.( <$@ ) - let ( <=@ ) = Typed.Infix.( <=$@ ) - let ( +@ ) = Typed.Infix.( +!@ ) - let ( -@ ) = Typed.Infix.( -!@ ) + let one () = Typed.BitVec.usize Z.one + let of_z = Typed.BitVec.usize + let to_z _ = None (* Can be improved, but sound. *) + let add = Typed.BitVec.add + let minus = Typed.BitVec.sub + let lt = Typed.BitVec.lt ~signed:false + let leq = Typed.BitVec.leq ~signed:false end let pp_init ft (v, ty) = diff --git a/soteria/lib/sym_states/tree_block.ml b/soteria/lib/sym_states/tree_block.ml index d01b24410..9f07ef186 100644 --- a/soteria/lib/sym_states/tree_block.ml +++ b/soteria/lib/sym_states/tree_block.ml @@ -1,4 +1,5 @@ open Symex +module Make_bool_syntax = Symex.Value.S_bool.Make_syntax open Soteria_std.Syntaxes.FunctionWrap (** A [Split_tree] is a simplified representation of a tree, that has no offset. @@ -45,24 +46,10 @@ and node_qty = Partially | Totally *) module type MemVal = sig module Symex : Symex.S - - module SInt : sig - type +'a t = 'a Symex.Value.t - type sbool - type sint - - val v_false : sbool t - val zero : unit -> sint t - val ( +@ ) : sint t -> sint t -> sint t - val ( -@ ) : sint t -> sint t -> sint t - val ( <@ ) : sint t -> sint t -> sbool t - val ( <=@ ) : sint t -> sint t -> sbool t - val ( ==@ ) : sint t -> sint t -> sbool t - val ( &&@ ) : sbool t -> sbool t -> sbool t - end + module S_int : Sym_data.S_int.S with module Symex = Symex type t - type sint := SInt.sint SInt.t + type sint := S_int.t val pp : Format.formatter -> t -> unit @@ -117,24 +104,20 @@ module type MemVal = sig val assert_exclusively_owned : t -> (unit, 'err, serialized) Symex.Result.t end -module Make - (Symex : Symex.S) - (MemVal : - MemVal - with module Symex = Symex - and type 'a SInt.t = 'a Symex.Value.t - and type SInt.sbool = Symex.Value.S_bool.t) = +module Make (Symex : Symex.S) (MemVal : MemVal with module Symex = Symex) = struct open Compo_res open Symex.Syntax open Symex - open MemVal.SInt + open Sym_data.S_int.Make_syntax (MemVal.S_int) + open Make_bool_syntax (Symex.Value.S_bool) + module Range = Sym_data.S_range.Make (MemVal.S_int) module Sym_int_syntax = struct let zero = MemVal.SInt.zero end - type nonrec sint = sint Symex.Value.t + type sint = MemVal.S_int.t [@@deriving show { with_path = false }] (* re-export the types to be able to use them easily *) type nonrec ('a, 'sint) tree = ('a, 'sint) tree = { @@ -143,19 +126,6 @@ struct children : (('a, 'sint) tree * ('a, 'sint) tree) option; } - module Range = struct - type t = sint * sint - - let pp ft (l, u) = Fmt.pf ft "[%a, %a[" Symex.Value.ppa l Symex.Value.ppa u - let sem_eq (a, c) (b, d) = a ==@ b &&@ (c ==@ d) - let is_inside (l1, u1) (l2, u2) = l2 <=@ l1 &&@ (u1 <=@ u2) - let strictly_inside x (l, u) = l <@ x &&@ (x <@ u) - let size (l, u) = u -@ l - let split_at (l, h) x = ((l, x), (x, h)) - let offset (l, u) off = (l +@ off, u +@ off) - let of_low_and_size low size = (low, low +@ size) - end - module Split_tree = Split_tree module Node = struct @@ -332,7 +302,7 @@ struct else if Option.is_none t.children then return (t, None) else let left, right = Option.get t.children in - if%sat Range.is_inside range left.range then + if%sat Range.subset_eq range left.range then let* extracted, new_left = extract left range in let+ new_self = match new_left with @@ -449,7 +419,7 @@ struct in frame_inside ~replace_node ~rebuild_parent new_self range else - if%sat Range.is_inside range left.range then + if%sat Range.subset_eq range left.range then let** node, left = frame_inside ~replace_node ~rebuild_parent left range in @@ -508,7 +478,7 @@ struct type t = { root : Tree.t; - bound : sint option; [@printer Fmt.(option ~none:(any "⊥") Symex.Value.ppa)] + bound : sint option; [@printer Fmt.(option ~none:(any "⊥") MemVal.S_int.pp)] } [@@deriving show { with_path = false }] @@ -520,7 +490,7 @@ struct let () = Option.iter (fun b -> - let range_str = Fmt.str "[%a; ∞[" Symex.Value.ppa b in + let range_str = Fmt.str "[%a; ∞[" MemVal.S_int.pp b in r := [ (range_str, text "OOB") ]) t.bound in @@ -535,12 +505,8 @@ struct (** Logic *) type serialized_atom = - | MemVal of { - offset : sint; [@printer Symex.Value.ppa] - len : sint; [@printer Symex.Value.ppa] - v : MemVal.serialized; - } - | Bound of sint [@printer fun f v -> Fmt.pf f "Bound(%a)" Symex.Value.ppa v] + | MemVal of { offset : sint; len : sint; v : MemVal.serialized } + | Bound of sint [@printer fun f v -> Fmt.pf f "Bound(%a)" MemVal.S_int.pp v] [@@deriving show { with_path = false }] type serialized = serialized_atom list @@ -614,7 +580,7 @@ struct (** Logic *) let subst_serialized subst_var (serialized : serialized) = - let v_subst v = Symex.Value.subst subst_var v in + let v_subst v = MemVal.S_int.subst subst_var v in let subst_atom = function | MemVal { offset; len; v } -> let v = MemVal.subst_serialized subst_var v in @@ -627,10 +593,10 @@ struct List.iter (function | MemVal { offset; len; v } -> - Symex.Value.iter_vars offset f; - Symex.Value.iter_vars len f; + MemVal.S_int.iter_vars offset f; + MemVal.S_int.iter_vars len f; MemVal.iter_vars_serialized v f - | Bound v -> Symex.Value.iter_vars v f) + | Bound v -> MemVal.S_int.iter_vars v f) serialized let pp_serialized = Fmt.Dump.list pp_serialized_atom From 0c4413c1c850db2255720d6985ed9fe89605d516 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Mon, 15 Sep 2025 17:00:06 +0100 Subject: [PATCH 19/22] Update soteria/lib/sym_data/sym_data.ml Co-authored-by: N1ark --- soteria/lib/sym_data/sym_data.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/soteria/lib/sym_data/sym_data.ml b/soteria/lib/sym_data/sym_data.ml index 0e64766db..b7709bbf6 100644 --- a/soteria/lib/sym_data/sym_data.ml +++ b/soteria/lib/sym_data/sym_data.ml @@ -1,4 +1,4 @@ -(** A collection of symbolic data structures and usefule signatures. *) +(** A collection of symbolic data structures and useful signatures. *) module S_elt = S_elt module S_eq = S_eq From c34fa4fb18dfc065704cbc4b34a8c92ad7bec4a4 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 16 Sep 2025 12:46:58 +0100 Subject: [PATCH 20/22] post-rebase fixups Signed-off-by: Sacha Ayoun --- soteria-rust/lib/rtree_block.ml | 4 ++-- soteria/lib/bv_values/typed.ml | 2 ++ soteria/lib/bv_values/typed.mli | 1 + soteria/lib/sym_states/tree_block.ml | 2 +- soteria/lib/symex/symex.ml | 7 +++---- 5 files changed, 9 insertions(+), 7 deletions(-) diff --git a/soteria-rust/lib/rtree_block.ml b/soteria-rust/lib/rtree_block.ml index 629f3e699..2ae2aef4c 100644 --- a/soteria-rust/lib/rtree_block.ml +++ b/soteria-rust/lib/rtree_block.ml @@ -29,8 +29,8 @@ module Make (Sptr : Sptr.S) = struct let one () = Typed.BitVec.usize Z.one let of_z = Typed.BitVec.usize let to_z _ = None (* Can be improved, but sound. *) - let add = Typed.BitVec.add - let minus = Typed.BitVec.sub + let add = Typed.Infix.( +!@ ) + let minus = Typed.Infix.( -!@ ) let lt = Typed.BitVec.lt ~signed:false let leq = Typed.BitVec.leq ~signed:false end diff --git a/soteria/lib/bv_values/typed.ml b/soteria/lib/bv_values/typed.ml index 810dffc3b..86b75241c 100644 --- a/soteria/lib/bv_values/typed.ml +++ b/soteria/lib/bv_values/typed.ml @@ -71,6 +71,8 @@ module BitVec = struct let mki_nz n i = if i = 0 then failwith "Zero value in mki_nonzero" else mki_masked n i + + let assume_not_overflowed v = v end module Infix = struct diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli index 62af1bcee..d84069ec9 100644 --- a/soteria/lib/bv_values/typed.mli +++ b/soteria/lib/bv_values/typed.mli @@ -133,6 +133,7 @@ module BitVec : sig val sub_overflows : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t val mul_overflows : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t val neg_overflows : [< sint ] t -> [> sbool ] t + val assume_not_overflowed : [< sint_ovf ] t -> [> sint ] t (* inequalities *) val lt : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t diff --git a/soteria/lib/sym_states/tree_block.ml b/soteria/lib/sym_states/tree_block.ml index 9f07ef186..656df26e8 100644 --- a/soteria/lib/sym_states/tree_block.ml +++ b/soteria/lib/sym_states/tree_block.ml @@ -114,7 +114,7 @@ struct module Range = Sym_data.S_range.Make (MemVal.S_int) module Sym_int_syntax = struct - let zero = MemVal.SInt.zero + let zero = MemVal.S_int.zero end type sint = MemVal.S_int.t [@@deriving show { with_path = false }] diff --git a/soteria/lib/symex/symex.ml b/soteria/lib/symex/symex.ml index 1e090642f..affdbb542 100644 --- a/soteria/lib/symex/symex.ml +++ b/soteria/lib/symex/symex.ml @@ -457,14 +457,14 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : ~(then_ : unit -> 'a Iter.t) ~(else_ : unit -> 'a Iter.t) : 'a Iter.t = fun f -> let guard = Solver.simplify guard in - match Value.as_bool guard with + match Value.S_bool.to_bool guard with (* [then_] and [else_] could be ['a t] instead of [unit -> 'a t], if we remove the Some true and Some false optimisation. *) | Some true -> then_ () f | Some false -> else_ () f | None -> Symex_state.save (); - Solver.add_constraints ~simplified:true [ Value.(not guard) ]; + Solver.add_constraints ~simplified:true [ Value.S_bool.not guard ]; let neg_unsat = Solver_result.is_unsat (Solver.sat ()) in if neg_unsat then then_ () f; Symex_state.backtrack_n 1; @@ -499,8 +499,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) : else branch_on ?left_branch_name ?right_branch_name guard ~then_ ~else_ f let assert_or_error guard err = - branch_on - Value.(not guard) + branch_on (Value.S_bool.not guard) ~then_:(fun () -> return (Compo_res.Error err)) ~else_:(fun () -> return (Compo_res.Ok ())) From 0bac1ecf3cbd435ae7ad4a6edd48dfbdd890f652 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Thu, 20 Nov 2025 23:08:27 +0000 Subject: [PATCH 21/22] promote test Signed-off-by: Sacha Ayoun --- soteria-c/test/cram/simple_bi.t/run.t | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/soteria-c/test/cram/simple_bi.t/run.t b/soteria-c/test/cram/simple_bi.t/run.t index 900a4f1c3..8e2a8ef53 100644 --- a/soteria-c/test/cram/simple_bi.t/run.t +++ b/soteria-c/test/cram/simple_bi.t/run.t @@ -23,7 +23,7 @@ info = None })]; globs = [] } ]; - pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)]; + pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)]; post = { heap = [(V|1|, @@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason, info = None })]; globs = [] } ]; - pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)]; + pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)]; post = { heap = [(V|1|, @@ -255,7 +255,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack. ]; pc = [(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|); - (V|1| <=u 0x7fffffff); (0xfffffffffffffffc <=u V|3|)]; + (V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)]; post = { heap = [(V|2|, @@ -309,7 +309,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack. ]; pc = [(0x0000000000000000 != V|1|); (V|3| == 0x00000001); - (0xfffffffffffffffc <=u V|2|); (V|3| == 0x00000001)]; + (V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)]; post = { heap = [(V|1|, @@ -341,9 +341,12 @@ if%sat1 had the wrong semantics and would not correctly backtrack. ]; pc = [(0x0000000000000000 != V|1|); + ((V|2| Date: Fri, 21 Nov 2025 15:16:53 +0000 Subject: [PATCH 22/22] woops Signed-off-by: Sacha Ayoun --- soteria/lib/bv_values/bv_solver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml index 74d3d0331..8b265efdb 100644 --- a/soteria/lib/bv_values/bv_solver.ml +++ b/soteria/lib/bv_values/bv_solver.ml @@ -14,7 +14,7 @@ let rec simplify ~trivial_truthiness ~fallback (v : Svalue.t) = match v.node.kind with | Unop (Not, e) -> let e' = simplify e in - if Svalue.equal e e' then v else Svalue.S_bool.not e' + if Svalue.equal e e' then fallback v else Svalue.S_bool.not e' | Binop (Eq, e1, e2) -> if Svalue.equal e1 e2 then Svalue.S_bool.v_true else if Svalue.sure_neq e1 e2 then Svalue.S_bool.v_false