some cleaning

Author: redianthus

dune-project

@@ -73,7 +73,7 @@
   (sedlex
    (>= 3.3))
   (smtml
-   (>= 0.15.0))
+   (>= 0.16.0))
   synchronizer
   (uutf
    (>= 1.0.3))

owi.opam

@@ -38,7 +38,7 @@ depends: [
   "prelude" {>= "0.5"}
   "processor" {>= "0.2"}
   "sedlex" {>= "3.3"}
-  "smtml" {>= "0.15.0"}
+  "smtml" {>= "0.16.0"}
   "synchronizer"
   "uutf" {>= "1.0.3"}
   "xmlm" {>= "1.4.0"}

src/infra/benchmark.ml

@@ -18,7 +18,7 @@ let empty_stats () =
 let handle_time_span atomic_span f =
   if Log.is_bench_enabled () then
     let counter = Mtime_clock.counter () in
-    (* f is supposed to take a long time as it is calling the solver *)
+    (* f is supposed to take a long time! *)
     let res = f () in
     let span = Mtime_clock.count counter in
     let rec atomic_set () =
@@ -44,7 +44,8 @@ let percentage ~whole ~self =
   let self = Mtime.Span.to_float_ns self in
   self /. whole *. 100.
 
-let print_final ~bench_stats ~execution_time_a ~execution_time_b =
+let print_final ~bench_stats ~execution_time_a ~execution_time_b
+  ~wait_for_all_domains =
   let execution_time =
     (* execution time shouldn't be none in bench mode *)
     let execution_time_a =
@@ -100,14 +101,10 @@ let print_final ~bench_stats ~execution_time_a ~execution_time_b =
       solver_intermediate_model_time percentage );
 
   Log.bench (fun m ->
-    let percentage =
-      let whole = Mtime.Span.to_float_ns execution_time in
-      let interp = Mtime.Span.to_float_ns interpreter_time in
-      interp /. whole *. 100.
-    in
+    let percentage = percentage ~whole:execution_time ~self:interpreter_time in
     m "interpreter loop time         : %a (%.2G%%)" Mtime.Span.pp
       interpreter_time percentage );
   Log.bench (fun m -> m "path count: %d" (Atomic.get bench_stats.path_count));
 
-  let solver_stats = Solver.get_all_stats () in
+  let solver_stats = Solver.get_all_stats ~wait_for_all_domains in
   Log.bench (fun m -> m "solver stats: %a" Solver.pp_stats solver_stats)

src/infra/log.ml

@@ -7,6 +7,11 @@ include (val Logs.src_log main_src : Logs.LOG)
 let is_bench_enabled () =
   match Logs.Src.level bench_src with None -> false | Some _ -> true
 
+let is_info_enabled () =
+  match Logs.Src.level main_src with
+  | Some (Logs.Debug | Logs.Info) -> true
+  | None | Some _ -> false
+
 let bench_fn str fn =
   match Logs.Src.level bench_src with
   | None -> fn ()

src/infra/log.mli

@@ -2,6 +2,8 @@ include Logs.LOG
 
 val main_src : Logs.src
 
+val is_info_enabled : unit -> bool
+
 val is_bench_enabled : unit -> bool
 
 val bench_fn : string -> (unit -> 'a) -> 'a

src/intf/symbolic_choice_intf.ml

@@ -71,7 +71,7 @@ module type S = sig
     -> Smtml.Solver_type.t
     -> 'a t
     -> thread
-    -> callback:(close:(unit -> unit) -> 'a eval * thread -> unit)
+    -> callback:(close_work_queue:(unit -> unit) -> 'a eval * thread -> unit)
     -> callback_init:(unit -> unit)
     -> callback_end:(unit -> unit)
     -> unit Domain.t array

src/intf/work_ds_intf.ml

@@ -12,7 +12,7 @@ module type S = sig
   val push : 'a -> Prio.t -> 'a t -> unit
 
   (** Make a new pledge, ie indicate that new elements may be pushed to the
-      queue and that calls to pop should block waitting for them. *)
+      queue and that calls to pop should block waiting for them. *)
   val make_pledge : 'a t -> unit
 
   (** End one pledge. *)

src/symbolic/solver.ml

@@ -27,27 +27,35 @@ let check (S (solver_module, s)) pc =
   let module Solver = (val solver_module) in
   Solver.check_set s pc
 
-let model_of_partition (S (solver_module, s)) ~partition : Smtml.Model.t =
+let model_of_path_condition (S (solver_module, s)) ~path_condition :
+  Smtml.Model.t Option.t =
+  let exception Unknown in
   let module Solver = (val solver_module) in
-  let partition =
-    List.map
-      (fun pc ->
-        match Solver.get_sat_model s pc with
-        | `Model model -> model
-        | `Unknown -> assert false
-        | `Unsat -> assert false )
-      partition
-  in
-  let model = Hashtbl.create 64 in
-  List.iter
-    (fun tbl -> Hashtbl.iter (fun sym v -> Hashtbl.add model sym v) tbl)
-    partition;
-  model
+  try
+    let sub_conditions = Symbolic_path_condition.slice path_condition in
+    let models =
+      List.map
+        (fun pc ->
+          match Solver.get_sat_model s pc with
+          | `Model model -> model
+          | `Unknown ->
+            (* it can happen if the solver is interrupted, otherwise it is an error, we raise, so the function can return an option that will be handled by the called *)
+            raise Unknown
+          | `Unsat ->
+            (* it can not happen otherwise it means we reached an unreachable branch (or added garbage to the PC and did something wrong, who knows... :-) *)
+            assert false )
+        sub_conditions
+    in
+    (* We build the new complete model by merging all "sub models" *)
+    let model = Hashtbl.create 64 in
+    List.iter (Hashtbl.iter (Hashtbl.add model)) models;
+    Some model
+  with Unknown -> None
 
-let get_sat_model (S (solver_module, s)) ~symbol_scopes ~pc =
+let model_of_set (S (solver_module, s)) ~symbol_scopes ~set =
   let module Solver = (val solver_module) in
   let symbols = Symbol_scope.only_symbols symbol_scopes in
-  Solver.get_sat_model ~symbols s pc
+  Solver.get_sat_model ~symbols s set
 
 let empty_stats = Smtml.Statistics.Map.empty
 
@@ -61,9 +69,17 @@ let interrupt_all () =
       Solver.interrupt s )
     solvers
 
-let get_all_stats () =
+let get_all_stats ~wait_for_all_domains =
   if not (Log.is_bench_enabled ()) then empty_stats
   else begin
+    (* interrupt_all is unreliable but is a best effort to try to make sure we don't wait too long on really long requests.
+     The reliable alternative would be to backup the statistics before each SMT request when in benchmark mode, but this would be too costly and lead to less accurate requests than random failures... *)
+    interrupt_all ();
+    (* we wait for all domains to terminate because:
+    - some solvers can not be interrupted and usually don't like being asked for statistics while running
+    - we already got all the previous metrics, so we don't care about waiting more... *)
+    wait_for_all_domains ();
+
     let solvers = Atomic.get instances in
     List.fold_left
       (fun stats_acc (S (solver_module, s)) ->
@@ -74,7 +90,7 @@ let get_all_stats () =
             Logs.warn (fun m ->
               m
                 "could not fetch the statistics of one solver because it was \
-                 canceled" );
+                 canceled, used empty stats instead" );
             empty_stats
         in
         Smtml.Statistics.merge stats stats_acc )

src/symbolic/solver.mli

@@ -8,20 +8,20 @@ val fresh : Smtml.Solver_type.t -> unit -> t
 
 val check : t -> Smtml.Expr.Set.t -> [ `Sat | `Unknown | `Unsat ]
 
-val get_sat_model :
+val model_of_set :
      t
   -> symbol_scopes:Symbol_scope.t
-  -> pc:Smtml.Expr.Set.t
+  -> set:Smtml.Expr.Set.t
   -> [ `Unsat | `Unknown | `Model of Smtml.Model.t ]
 
-val model_of_partition : t -> partition:Smtml.Expr.Set.t list -> Smtml.Model.t
+val model_of_path_condition :
+  t -> path_condition:Symbolic_path_condition.t -> Smtml.Model.t option
 
 val empty_stats : Smtml.Statistics.t
 
 val stats_are_empty : Smtml.Statistics.t -> bool
 
 val pp_stats : Smtml.Statistics.t Fmt.t
 
-val get_all_stats : unit -> Smtml.Statistics.t
-
-val interrupt_all : unit -> unit
+val get_all_stats :
+  wait_for_all_domains:(Unit.t -> Unit.t) -> Smtml.Statistics.t

src/symbolic/symbolic_choice.ml

@@ -92,21 +92,21 @@ module CoreImpl = struct
         (fun f write_back -> handle_status (Schedulable.run f wls) write_back)
         sched.work_queue
 
-    let spawn_worker sched wls_init callback callback_init callback_close =
+    let spawn_worker sched wls_init ~callback ~callback_init ~callback_end =
       callback_init ();
       Domain.spawn (fun () ->
-        Fun.protect
-          ~finally:(fun () -> callback_close ())
-          (fun () ->
-            let wls = wls_init () in
-            try
-              work wls sched
-                (callback ~close:(fun () ->
-                   Work_datastructure.close sched.work_queue ) )
-            with e ->
-              let bt = Printexc.get_raw_backtrace () in
-              Work_datastructure.close sched.work_queue;
-              Printexc.raise_with_backtrace e bt ) )
+        let wls = wls_init () in
+        Fun.protect ~finally:callback_end (fun () ->
+          try
+            work wls sched
+              (callback ~close_work_queue:(fun () ->
+                 Work_datastructure.close sched.work_queue ) )
+          with e ->
+            let bt = Printexc.get_raw_backtrace () in
+            (* TODO: I don't understand why we are closing the work queue if one worker dies...
+                    If I remove this line, nothing seens to go wrong with the tests... *)
+            Work_datastructure.close sched.work_queue;
+            Printexc.raise_with_backtrace e bt ) )
   end
 
   module State = struct
@@ -256,7 +256,7 @@ module CoreImpl = struct
       -> Smtml.Solver_type.t
       -> 'a t
       -> thread
-      -> callback:(close:(unit -> unit) -> 'a eval * thread -> unit)
+      -> callback:(close_work_queue:(unit -> unit) -> 'a eval * thread -> unit)
       -> callback_init:(unit -> unit)
       -> callback_end:(unit -> unit)
       -> unit Domain.t array
@@ -314,19 +314,24 @@ module CoreImpl = struct
       add_init_task sched (State.run t thread);
       if workers > 1 then Logs_threaded.enable ();
       Array.init workers (fun _i ->
-        spawn_worker sched (Solver.fresh solver) callback callback_init
-          callback_end )
+        spawn_worker sched (Solver.fresh solver) ~callback ~callback_init
+          ~callback_end )
 
     let trap t =
       let* thread in
       let* solver in
-      let pc = Thread.pc thread in
+      let path_condition = Thread.pc thread in
       let symbol_scopes = Thread.symbol_scopes thread in
       let stats = Thread.bench_stats thread in
-      let model =
+      let* model =
         Benchmark.handle_time_span stats.solver_final_model_time @@ fun () ->
-        let partition = Symbolic_path_condition.explode pc in
-        Solver.model_of_partition solver ~partition
+        match Solver.model_of_path_condition solver ~path_condition with
+        | Some model -> return model
+        | None ->
+          (* It can happen when the solver is interrupted *)
+          (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged
+             if solver was interrupted then stop else assert false *)
+          stop
       in
       let labels = Thread.labels thread in
       let breadcrumbs = Thread.breadcrumbs thread in
@@ -358,7 +363,7 @@ module Make (Thread : Thread_intf.S) = struct
   let get_pc () =
     let+ thread in
     let pc = Thread.pc thread in
-    let pc = Symbolic_path_condition.explode pc in
+    let pc = Symbolic_path_condition.slice pc in
     List.fold_left Smtml.Expr.Set.union Smtml.Expr.Set.empty pc
 
   let add_breadcrumb crumb =
@@ -396,26 +401,26 @@ module Make (Thread : Thread_intf.S) = struct
     let* () = yield prio in
     let* thread in
     let* solver in
-    let pc = Thread.pc thread in
-    let sliced_pc = Symbolic_path_condition.slice pc v in
+    let pc = Thread.pc thread |> Symbolic_path_condition.slice_on_condition v in
     let stats = Thread.bench_stats thread in
     let reachability =
       Benchmark.handle_time_span stats.solver_sat_time @@ fun () ->
-      Solver.check solver sliced_pc
+      Solver.check solver pc
     in
     return reachability
 
   let get_model_or_stop symbol =
     let* () = yield Prio.default in
     let* solver in
-    let+ thread in
-    let pc = Thread.pc thread in
-    let pc = Symbolic_path_condition.slice_on_symbol pc symbol in
+    let* thread in
+    let set =
+      Thread.pc thread |> Symbolic_path_condition.slice_on_symbol symbol
+    in
     let stats = Thread.bench_stats thread in
     let symbol_scopes = Symbol_scope.of_symbol symbol in
     let sat_model =
       Benchmark.handle_time_span stats.solver_intermediate_model_time (fun () ->
-        Solver.get_sat_model solver ~symbol_scopes ~pc )
+        Solver.model_of_set solver ~symbol_scopes ~set )
     in
     match sat_model with
     | `Unsat -> stop
@@ -426,7 +431,11 @@ module Make (Thread : Thread_intf.S) = struct
         (* the model exists so the symbol should evaluate *)
         assert false
     end
-    | `Unknown -> assert false
+    | `Unknown ->
+      (* It can happen when the solver is interrupted *)
+      (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged
+               if solver was interrupted then stop else assert false *)
+      stop
 
   let select_inner ~explore_first ?(with_breadcrumbs = true)
     ~check_only_true_branch (cond : Symbolic_boolean.t) ~prio_true ~prio_false =
@@ -460,6 +469,8 @@ module Make (Thread : Thread_intf.S) = struct
             stop
           | `Unknown ->
             (* It can happen when the solver is interrupted *)
+            (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged
+                 if solver was interrupted then stop else assert false *)
             stop
           end
         end
@@ -495,25 +506,27 @@ module Make (Thread : Thread_intf.S) = struct
       (Some assign, sym)
 
   let select_i32 (i : Symbolic_i32.t) =
-    let sym_int = Smtml.Expr.simplify i in
-    match Smtml.Expr.view sym_int with
+    let i = Smtml.Expr.simplify i in
+    match Smtml.Expr.view i with
     | Val (Bitv bv) when Smtml.Bitvector.numbits bv <= 32 ->
       return (Smtml.Bitvector.to_int32 bv)
     | _ ->
-      let* assign, symbol = summary_symbol sym_int in
+      let* assign, symbol = summary_symbol i in
       let* () =
         match assign with Some assign -> add_pc assign | None -> return ()
       in
       let rec generator () =
         let* possible_value = get_model_or_stop symbol in
-        let* possible_value in
         let i =
           match possible_value with
           | Smtml.Value.Bitv bv when Smtml.Bitvector.numbits bv <= 32 ->
             Smtml.Bitvector.to_int32 bv
-          | _ -> Fmt.failwith "Unreachable: found symbol must be a value"
+          | _ ->
+            (* it should be a value! *)
+            assert false
         in
         let s = Smtml.Expr.symbol symbol in
+        (* TODO: everything which follows look like select_inner and could probably be simplified by calling it directly! *)
         let this_value_cond =
           let open Smtml.Expr in
           Bitv.I32.(s = v i)
@@ -548,13 +561,18 @@ module Make (Thread : Thread_intf.S) = struct
     else
       let* thread in
       let* solver in
-      let pc = Thread.pc thread in
+      let path_condition = Thread.pc thread in
       let symbol_scopes = Thread.symbol_scopes thread in
       let stats = Thread.bench_stats thread in
-      let model =
+      let* model =
         Benchmark.handle_time_span stats.solver_final_model_time @@ fun () ->
-        let partition = Symbolic_path_condition.explode pc in
-        Solver.model_of_partition solver ~partition
+        match Solver.model_of_path_condition solver ~path_condition with
+        | Some model -> return model
+        | None ->
+          (* It can happen when the solver is interrupted *)
+          (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged
+               if solver was interrupted then stop else assert false *)
+          stop
       in
       let breadcrumbs = Thread.breadcrumbs thread in
       let labels = Thread.labels thread in