why3prove: Make the output of counterexamples readable by default

bench/ce-bench

@@ -71,7 +71,7 @@ run () {
         echo "Strongest Postcondition" > "$f.out"
         printf "Strongest Postcondition  ${file_path} ($1)... "
     fi
-    $dir/../bin/why3prove.opt --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
+    $dir/../bin/why3prove.opt --json --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
         # This ad hoc sed removes any timing information from counterexamples output.
         # Counterexamples in JSON format cannot match this regexp.
         sed 's/ ([0-9]\+\.[0-9]\+s)//' | \

examples/use_api/logic.ml

@@ -136,7 +136,7 @@ let result1 : Call_provers.prover_result =
 
 (* prints Alt-Ergo answer *)
 let () = printf "@[On task 1, Alt-Ergo answers %a@."
-  Call_provers.print_prover_result result1
+  (Call_provers.print_prover_result ~json_model:false) result1
 (* END{callprover} *)
 
 (* BEGIN{calltimelimit} *)
@@ -192,7 +192,7 @@ let result3 =
     alt_ergo_driver task3)
 
 let () = printf "@[On task 3, alt-ergo answers %a@."
-  Call_provers.print_prover_result result3
+  (Call_provers.print_prover_result ~json_model:false) result3
 
 (* quantifiers: let's build "forall x:int. x*x >= 0" *)
 (* BEGIN{quantfmla1} *)
@@ -230,7 +230,7 @@ let result4 =
     alt_ergo_driver task4)
 
 let () = printf "@[On task 4, alt-ergo answers %a@."
-  Call_provers.print_prover_result result4
+  (Call_provers.print_prover_result ~json_model:false) result4
 
 (* build a theory with all these goals *)
 

examples/use_api/mlw_tree.ml

@@ -300,7 +300,7 @@ let () =
                               alt_ergo_driver t)
        in
        printf "@[On task %d, alt-ergo answers %a@."
-              i Call_provers.print_prover_result r;
+              i (Call_provers.print_prover_result ~json_model:false) r;
        i+1
       )
       1 my_tasks

src/driver/call_provers.ml

@@ -162,14 +162,17 @@ let print_prover_status fmt = function
 let print_steps fmt s =
   if s >= 0 then fprintf fmt ", %d steps" s
 
-let print_prover_result fmt {pr_answer = ans; pr_status = status;
-                             pr_output = out; pr_time   = t;
-                             pr_steps  = s;   pr_model  = m} =
+let print_prover_result ~json_model fmt {pr_answer = ans; pr_status = status;
+                                         pr_output = out; pr_time   = t;
+                                         pr_steps  = s;   pr_model  = m} =
   let print_attrs = Debug.test_flag debug_attrs in
   fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
   if not (Model_parser.is_model_empty m) then begin
     fprintf fmt "\nCounter-example model:";
-    Model_parser.print_model ~print_attrs fmt m
+    if json_model then
+      Model_parser.print_model ~print_attrs fmt m
+    else
+      Model_parser.print_model_human ?me_name_trans:None ~print_attrs fmt m
   end;
   if ans == HighFailure then
     fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."

src/driver/call_provers.mli

@@ -52,7 +52,8 @@ type prover_result = {
 val print_prover_answer : Format.formatter -> prover_answer -> unit
 (** Pretty-print a {! prover_answer} *)
 
-val print_prover_result : Format.formatter -> prover_result -> unit
+val print_prover_result :
+  json_model:bool -> Format.formatter -> prover_result -> unit
 (** Pretty-print a prover_result. The answer and the time are output.
     The output of the prover is printed if and only if the answer is
     a [HighFailure] *)

src/session/controller_itp.ml

@@ -41,7 +41,8 @@ let print_status fmt st =
   | Scheduled         -> fprintf fmt "Scheduled"
   | Running           -> fprintf fmt "Running"
   | Done r            ->
-      fprintf fmt "Done(%a)" Call_provers.print_prover_result r
+      fprintf fmt "Done(%a)"
+        (Call_provers.print_prover_result ~json_model:false) r
   | Interrupted       -> fprintf fmt "Interrupted"
   | Detached          -> fprintf fmt "Detached"
   | InternalFailure e ->
@@ -1035,8 +1036,8 @@ let print_report fmt (r: report) =
   match r with
   | Result (new_r, old_r) ->
     Format.fprintf fmt "new_result = %a, old_result = %a@."
-      Call_provers.print_prover_result new_r
-      Call_provers.print_prover_result old_r
+      (Call_provers.print_prover_result ~json_model:false) new_r
+      (Call_provers.print_prover_result ~json_model:false) old_r
   | CallFailed e ->
     Format.fprintf fmt "Callfailed %a@." Exn_printer.exn_printer e
   | Replay_interrupted ->
@@ -1047,7 +1048,7 @@ let print_report fmt (r: report) =
     Format.fprintf fmt "No edited file@."
   | No_former_result new_r ->
     Format.fprintf fmt "new_result = %a, no former result@."
-      Call_provers.print_prover_result new_r
+      (Call_provers.print_prover_result ~json_model:false) new_r
 
 (* TODO to be removed when we have a better way to print *)
 let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list) =
@@ -1227,7 +1228,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
                   | Done res ->
                      assert (res.Call_provers.pr_answer = Call_provers.Valid);
                      Debug.dprintf debug "Bisecting: %a.@."
-                                   Call_provers.print_prover_result res
+                       (Call_provers.print_prover_result ~json_model:false) res
                   end
                 in
                 schedule_proof_attempt ?save_to:None c pn prover ~limit ~callback ~notification

src/session/session_itp.ml

@@ -484,7 +484,8 @@ let print_proof_attempt fmt pa =
   fprintf fmt "%a tl=%d %a"
           Whyconf.print_prover pa.prover
           pa.limit.Call_provers.limit_time
-          (Pp.print_option Call_provers.print_prover_result) pa.proof_state
+          (Pp.print_option (Call_provers.print_prover_result ~json_model:false))
+          pa.proof_state
 
 let rec print_proof_node s (fmt: Format.formatter) p =
   let pn = get_proofNode s p in

src/tools/why3prove.ml

@@ -26,6 +26,8 @@ let opt_input = ref None
 let opt_theory = ref None
 let opt_trans = ref []
 let opt_metas = ref []
+(* Option for printing counterexamples with JSON formatting *)
+let opt_json = ref false
 
 let add_opt_file x =
   let tlist = Queue.create () in
@@ -137,6 +139,8 @@ let option_list = [
       "<dir> print the selected goals to separate files in <dir>";
   "--output", Arg.String (fun s -> opt_output := Some s),
       " same as -o";
+  "--json", Arg.Set opt_json,
+      " print counterexamples in JSON format";
   "--print-theory", Arg.Set opt_print_theory,
       " print selected theories";
   "--print-namespace", Arg.Set opt_print_namespace,
@@ -254,7 +258,7 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
         let res = Call_provers.wait_on_call call in
         printf "%s %s %s: %a@." fname tname
           (task_goal task).Decl.pr_name.Ident.id_string
-          Call_provers.print_prover_result res;
+          (Call_provers.print_prover_result ~json_model:!opt_json) res;
         if res.Call_provers.pr_answer <> Call_provers.Valid then unproved := true
     | None, None ->
         Driver.print_task drv std_formatter task

src/tools/why3replay.ml

@@ -118,7 +118,7 @@ let () =
       if Debug.test_flag debug then
         Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r)
 
-let print_result = Call_provers.print_prover_result
+let print_result = Call_provers.print_prover_result ~json_model:false
 
 module S = Session_itp
 

src/tools/why3shell.ml

@@ -283,7 +283,9 @@ let print_proof_attempt fmt pa_id =
   | None -> fprintf fmt "%s" pa.node_name
   | Some _pr ->
     fprintf fmt "%s %a"
-      pa.node_name (Pp.print_option Call_provers.print_prover_result) (get_result pa.node_proof)
+      pa.node_name
+      (Pp.print_option (Call_provers.print_prover_result ~json_model:false))
+      (get_result pa.node_proof)
 
 let rec print_proof_node (fmt: Format.formatter) goal_id =
   let goal = Hnode.find nodes goal_id in

src/why3session/why3session_html.ml

@@ -239,7 +239,8 @@ struct
 
   let print_proof_status fmt = function
     | None -> fprintf fmt "No result"
-    | Some res -> fprintf fmt "Done: %a" Call_provers.print_prover_result res
+    | Some res -> fprintf fmt "Done: %a"
+                    (Call_provers.print_prover_result ~json_model:true) res
 
   let print_proof_attempt s fmt pa =
     let pa = get_proof_attempt_node s pa in

[François Bobot]

@sdailler Added as an optional argument, it would have not broken the backward compatibility.

[MARCHE Claude]

I asked Sylvain to add this option parameter. I believe it is better to have non optional parameter to enforce the caller to think about which parameter to pass.

Yet, this example shows another doom of API design: the name for that parameter is very badly chosen.

[DAILLER Sylvain]

Yes, regarding counterexamples, I was not very careful at being backward compatible. You will surely find other places where the .mli functions changed.

I am not sure that it is possible to use an optional argument in this case in the code. I am not a specialist but I don't think fprintf "%a" print_prover_result pr works without putting explicitly the optional label ? argument.

[François Bobot]

I am not sure that it is possible to use an optional argument in this case in the code

We need to use the label in this case. So that's true, it is not completely backward compatible just a little more. I opened https://github.com/ocaml/ocaml/issues/8661 to have a better understanding of the limitations.

[DAILLER Sylvain]

I think people will say that this is normal behaviour of labels in case of partial applications. My personal rule of thumbs is to avoid using them in such cases.

I am not sure they expected to use the optional labels for backward compatibility.