diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index c886ab934..2121885e2 100644 --- a/src/cmd/cmd_conc.ml +++ b/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