Hide debug messages

src/cmd/cmd_conc.ml

@@ -240,6 +240,7 @@ let try_initialize pc node head =
   match node.node with Not_explored -> node.node <- new_node pc head | _ -> ()
 
 let check = true
+let print_debug = true
 
 let rec add_trace pc node (trace : trace) =
   match trace.remaining_pc with
@@ -295,8 +296,13 @@ let add_trace tree trace = add_trace [] tree trace
 let run_once tree link_state modules_to_run forced_values =
   let result = run_modules_to_run link_state modules_to_run in
   let ( ( result
-        , Choice.{ pc; symbols = _; symbols_value; shared = _; preallocated_values = _ } )
-        as r ) =
+        , Choice.
+            { pc
+            ; symbols = _
+            ; symbols_value
+            ; shared = _
+            ; preallocated_values = _
+            } ) as r ) =
     let forced_values =
       match forced_values with None -> Hashtbl.create 0 | Some v -> v
     in
@@ -314,8 +320,10 @@ let run_once tree link_state modules_to_run forced_values =
     { assignments = symbols_value; remaining_pc = List.rev pc; end_of_trace }
   in
   let () =
-    Format.pp_std "Add trace:@\n";
-    Format.pp_std "%a@\n" Concolic_choice.pp_pc trace.remaining_pc
+    if print_debug then begin
+      Format.pp_std "Add trace:@\n";
+      Format.pp_std "%a@\n" Concolic_choice.pp_pc trace.remaining_pc
+    end
   in
   add_trace tree trace;
   r
@@ -324,11 +332,12 @@ let run_once tree link_state modules_to_run forced_values =
 let rec find_node_to_run tree =
   match tree.node with
   | Not_explored ->
-    Format.pp_std "Try unexplored@.%a@.@." Concolic_choice.pp_pc tree.pc;
+    if print_debug then
+      Format.pp_std "Try unexplored@.%a@.@." Concolic_choice.pp_pc tree.pc;
     Some tree.pc
   | Select { cond = _; if_true; if_false } ->
     let b = Random.bool () in
-    Format.pp_std "Select bool %b@." b;
+    if print_debug then Format.pp_std "Select bool %b@." b;
     let tree = if b then if_true else if_false in
     find_node_to_run tree
   | Select_i32 { value = _; branches } ->
@@ -338,17 +347,19 @@ let rec find_node_to_run tree =
     if n = 0 then None
     else
       let i = Random.int n in
-      let () = Format.pp_std "Select_i32 %i@." i in
+      if print_debug then Format.pp_std "Select_i32 %i@." i;
       let _, branch = List.nth branches i in
       find_node_to_run branch
   | Assume { cond = _; cont } -> find_node_to_run cont
   | Assert { cond; cont = _; disproved = None } ->
     let pc : Concolic_choice.pc = Select (cond, false) :: tree.pc in
-    Format.pp_std "Try Assert@.%a@.@." Concolic_choice.pp_pc pc;
+    if print_debug then
+      Format.pp_std "Try Assert@.%a@.@." Concolic_choice.pp_pc pc;
     Some pc
   | Assert { cond = _; cont; disproved = Some _ } -> find_node_to_run cont
   | Unreachable ->
-    Format.pp_std "Unreachable (Retry)@.%a@." Concolic_choice.pp_pc tree.pc;
+    if print_debug then
+      Format.pp_std "Unreachable (Retry)@.%a@." Concolic_choice.pp_pc tree.pc;
     None
 
 let pc_model solver pc =
@@ -368,16 +379,19 @@ let find_model_to_run solver tree =
 let launch solver tree link_state modules_to_run =
   let rec find_model n =
     if n = 0 then
-      let () = Format.pp_std "Failed to find something to run@." in
+      let () =
+        if print_debug then Format.pp_std "Failed to find something to run@."
+      in
       None
     else
       match find_model_to_run solver tree with
       | None -> find_model (n - 1)
       | Some m ->
         let () =
-          Format.pp_std "Found something to run %a@."
-            (fun ppf v -> Smtml.Model.pp ppf v)
-            m
+          if print_debug then
+            Format.pp_std "Found something to run %a@."
+              (fun ppf v -> Smtml.Model.pp ppf v)
+              m
         in
         Some m
   in
@@ -392,13 +406,15 @@ let launch solver tree link_state modules_to_run =
     | Ok (Ok ()) -> loop (count - 1)
     | Ok (Error e) -> Result.failwith e
     | Error (Assume_fail c) -> begin
-      Format.pp_std "Assume_fail: %a@\n" Smtml.Expr.pp c;
-      Format.pp_std "Assignments:@\n%a@\n" Concolic_choice.pp_assignments
-        thread.symbols_value;
-      Format.pp_std "Retry !@\n";
+      if print_debug then begin
+        Format.pp_std "Assume_fail: %a@\n" Smtml.Expr.pp c;
+        Format.pp_std "Assignments:@\n%a@\n" Concolic_choice.pp_assignments
+          thread.symbols_value;
+        Format.pp_std "Retry !@\n"
+      end;
       match pc_model solver thread.pc with
       | None ->
-        Format.pp_err "Can't satisfy assume !@\n";
+        if print_debug then Format.pp_err "Can't satisfy assume !@\n";
         loop (count - 1)
       | Some model -> run_model (Some model) (count - 1)
     end