New documentation on counterexamples feature

CHANGES.md

@@ -7,10 +7,10 @@ Session
 
 Drivers
   * the clause `syntax converter` disappeared. Any former use should
-    be replaced by `syntax literal` and/or `syntax function`
+    be replaced by `syntax literal` and/or `syntax function` :x:
 
 Language
-  * the `any` expression is now always ghost
+  * the `any` expression is now always ghost :x:
   * A syntactic sugar called "auto-dereference" is introduced, so as
     to avoid, on simple programs, the heavy use of `(!)` character on
     references. See details in Section A.1 of the manual.
@@ -19,9 +19,10 @@ Transformations
   * `split_vc` and `subst_all` now avoid substituting user symbols by
     generated ones :x:
   * `destruct_rec` applies `destruct` recursively on a goal
-  * `destruct` now simplifies away equalities on constructors
+  * `destruct` now simplifies away equalities on constructors :x:
+  * `destruct` now simplifies `if .. then .. else ..` and `match .. with ..` :x:
   * `destruct_alg` renamed to `destruct_term`. It also has a new experimental
-    keyword `using` to name newly destructed elements
+    keyword `using` to name newly destructed elements :x:
 
 Tools
   * added a command `why3 session update` to modify sessions from the
@@ -37,9 +38,12 @@ IDE
   * added support for GTK3
 
 Counterexamples
-  * Field names now use ident names instead of smt generated ones:
-    int32qtint -> int32'int
-  * Fix parsing of bitvector counterexamples orignated from Z3
+  * Changed the way counterexamples are triggered. Read Section 5.3.7
+    of the manual for details :x:
+  * various improvements on the generated counterexamples
+  * Field names now use ident names instead of smt generated ones, e.g.
+    int32qtint -> int32'int :x:
+  * Fix parsing of bitvector values from counterexamples generated by Z3
 
 Provers
   * support for Z3 4.8.1 (released Oct 16, 2018)

Makefile.in

@@ -1863,6 +1863,21 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
 	printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
 	@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
 
+test-ce.byte: examples/use_api/counterexample.ml lib/why3/why3.cma
+	$(SHOW) 'Ocaml    $<'
+	$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
+	|| (rm -f why3session.xml why3shapes why3shapes.gz;  \
+	printf "Test of Why3 API calls for counterexamples failed. Please fix it"; exit 2)
+	@rm -f why3session.xml why3shapes why3shapes.gz
+
+test-ce.opt: examples/use_api/counterexample.ml lib/why3/why3.cmxa
+	$(SHOW) 'Ocamlopt $<'
+	$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa  $< \
+	&& ./test-ce.opt > /dev/null) \
+	|| (rm -f test-ce.opt why3session.xml why3shapes why3shapes.gz; \
+	printf "Test of Why3 API calls for counterexamples failed. Please fix it"; exit 2)
+	@rm -f test-ce.opt why3session.xml why3shapes why3shapes.gz
+
 #only test the compilation of runstrat
 test-runstrat.byte: lib/why3/why3.cma lib/why3/META
 	OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean
@@ -1924,6 +1939,10 @@ doc/generated/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_cod
 doc/generated/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code
 	doc/extract_ocaml_code $* < $< > $@
 
+doc/generated/counterexample__%.ml: examples/use_api/counterexample.ml doc/extract_ocaml_code
+	doc/extract_ocaml_code $* < $< > $@
+
+
 OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
 	buildtask printtask buildtask2 \
 	getconf getanyaltergo getaltergo200 \
@@ -1941,11 +1960,15 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \
 	source1 code1 helper1 source2 code2 source3 code3 \
 	closemodule checkingvcs
 
+OCAMLCODE_COUNTEREXAMPLES =  ce_declarepropvars ce_adaptgoals \
+	ce_get_cvc4ce ce_callprover ce_nobuiltin
+
 OCAMLCODE = \
 	$(addprefix doc/generated/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
 	$(addprefix doc/generated/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \
 	$(addprefix doc/generated/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \
 	$(addprefix doc/generated/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \
+	$(addprefix doc/generated/counterexample__, $(addsuffix .ml, $(OCAMLCODE_COUNTEREXAMPLES))) \
 	doc/generated/whyconf__provertype.ml
 
 DOC = api glossary ide intro exec macros manpages install \

doc/api.tex

@@ -19,6 +19,7 @@ with a few other examples.
 \lstset{language={[Objective]Caml}}
 
 \section{Building Propositional Formulas}
+\label{sec:prop_form}
 
 The first step is to know how to build propositional formulas. The
 module \texttt{Term} gives a few functions for building these. Here is
@@ -371,6 +372,75 @@ call the Alt-Ergo prover. The rest of that code is using OCaml
 functions that were already introduced before.
 \lstinputlisting{generated/mlw_tree__checkingvcs.ml}
 
+\section{Generating counterexamples}
+\label{sec:ce_api}
+
+That feature is presented in details in Section~\ref{sec:idece}, that
+should be read first.  The counterexamples can also be generated using
+the API. The following explains how to change the source code (mainly
+adding attributes) in order to display counterexamples and how to
+parse the result given by Why3.  To illustrate this, we will adapt the
+examples from Section~\ref{sec:prop_form} to display counterexamples.
+
+\subsection{Attributes and locations on identifiers}
+
+For variables to be used for counterexamples they need to contain an attribute
+called \verb|model_trace| and a location. The \verb|model_trace| states the
+name the user wants the variable to be named in the output of the
+counterexamples pass. Usually, people put a reference to their program AST node
+in this attribute: this helps them to parse and display the results given by
+Why3.
+The locations are also necessary as every counterexamples values with no
+location won't be displayed. For example, an assignment of the source language
+such as the following will probably trigger the creation of an ident (for the
+left value) in a user subsequent tasks:
+\begin{lstlisting}
+x := !y + 1
+\end{lstlisting}
+This means that the ident generated for $x$ will hold both a \verb|model_trace|
+and a location.
+
+The example becomes the following:
+\lstinputlisting{generated/counterexample__ce_declarepropvars.ml}
+In the above, we defined a proposition ident with a location and a
+\verb|model_trace|.
+
+\subsection{Attributes in formulas}
+
+Now that variables are tagged, we can define formulas. To define a goal formula
+for counterexamples, we need to tag it with the \verb|vc:annotation|
+attribute. This attribute is automatically added when using the VC generation
+of Why3, but on a user-built task, this needs to be added. We also need to add
+a location for this goal.
+The following is obtained for the simple formula linking $A$ and $B$:
+\lstinputlisting{generated/counterexample__ce_adaptgoals.ml}
+
+Note: the transformations used for counterexamples will create new variables
+for each variable occuring inside the formula tagged by
+\verb|vc:annotation|. These variables are duplicates located at the VC
+line. They allow giving all counterexample values located at that VC line.
+
+
+% \paragraph{Tasks without the builtin modules}
+% TODO Solve the problem and remove this section
+
+% In the context of this example, we made an example that does not even load the
+% builtin theory. Counterexamples drivers are made to add a meta inside the
+% builtin theory of the task so that the printer knows that the task is for
+% counterexamples. So, we need to add the meta ourselves in this examples but in
+% practice users should never need to do this in any real applications:
+% \lstinputlisting{generated/counterexample__ce_nobuiltin.ml}
+
+
+\subsection{Counterexamples output formats}
+
+Several output formats are available for counterexamples. For users who want to
+pretty-print their counterexamples values, we recommend to use the JSON output
+as follows:
+\lstinputlisting{generated/counterexample__ce_callprover.ml}
+
+% TODO Details on the way the JSON is printed can be found in the code.
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-PDF-mode: t

doc/manpages.tex

@@ -239,6 +239,19 @@ The provers can give the following output:
   several prefixes.
 \end{description}
 
+\subsection{Getting Potential Counterexamples}
+
+That feature is presented in details in Section~\ref{sec:idece}, that should be read first.
+
+Counterexamples are also displayed by the \texttt{why3 prove} command
+when one selects a prover with the \texttt{counterexamples}
+alternative. The output is currently done in a JSON syntax (this may change in the future).
+
+% TODO: see issue #270
+% should be better given in human readable syntax by default, and
+% turned into JSON syntax only when using a option
+
+
 \section{The \texttt{ide} Command}
 \label{sec:ideref}
 
@@ -546,38 +559,118 @@ make them permanent.
 \end{description}
 
 \subsection{Displaying Counterexamples}
+\label{sec:idece}
 
 Why3 provides some support for extracting a potential counterexample
-from failing proof attempts. It is possible to display parts of this
-model in the terms of the original Why3 input.  Currently, this is
-supported for CVC4 prover version 1.5 and Z3.
+from failing proof attempts, for provers that are able to produce a
+\emph{counter-model} of the proof task. Why3 attempts to turn this
+counter-model into values for the free variables of the original Why3
+input. Currently, this is supported for CVC4 prover version at least
+1.5, and Z3 prover version at least 4.4.0.
+
+The generation of counterexamples is fully integrated in Why3 IDE. The
+recommended usage is to first start a prover normally, as shown in
+Figure~\ref{fig:ce_example0_p1}) and then click on the status icon for
+the corresponding proof attempt in the tree. Alternatively, one can
+use the key shortcut ``G'' or type \texttt{get-ce} in the command
+entry. The result can be seen on Figure \ref{fig:ce_example0_p2}: the
+same prover but with the alternative \emph{counterexamples} is
+run. The resulting counterexample is displayed in two different
+ways. First, it is displayed in the \textsf{Task} tab of the top-right
+window, at the end of the text of the task, under the form of a list
+of pairs ``variable = value'', ordered by the line number of the
+source code in which that variable takes that value. Second, it is
+displayed in the \textsf{Counterexample} tab of the bottom right
+window, this time interleaved with the code, as shown in Figure~\ref{fig:ce_example0_p2}.
+
+%%Generation of the screenshots:
+%%Those commands follow the style of starting.tex. To execute them one needs to
+%%do make update-doc-png.
+%EXECUTE rm -rf doc/cedoc/
+%EXECUTE cp bench/ce/cedoc.mlw doc/
+
+%EXECUTE bin/why3 ide -C doc/why3ide-doc.conf --batch "down;down;type cvc4;wait 2;down;snap -crop 1024x600+0+0 doc/images/ce_example0_p1.png" doc/cedoc.mlw
+
+%EXECUTE bin/why3 ide -C doc/why3ide-doc.conf --batch "down;down;type cvc4;wait 2;down;type get-ce;wait 2;down;faketype get-ce;snap -crop 1024x600+0+0 doc/images/ce_example0_p2.png" doc/cedoc.mlw
+
+%%Cleaning of the environment
+%EXECUTE rm -r doc/cedoc.mlw
+
+\begin{figure}[tbp]
+  \includegraphics[width=\textwidth]{images/ce_example0_p1.png}
+  \caption{Failing execution of CVC4} %TODO style
+  \label{fig:ce_example0_p1}
+\end{figure}
 
-The counterexamples are enable when using a prover under the
-alternative form called ``coutnerexamples''. After running the prover
-and clicking on the prover result in, the counterexample can be
-displayed in the tab Counter-example.  The counterexample is displayed
-with the original Why3 code in comments.  Counterexample values for
-Why3 source code elements at given line are displayed in a comment at
-the line below.
+\begin{figure}[tbp]
+  \includegraphics[width=\textwidth]{images/ce_example0_p2.png}
+  \caption{Counterexamples display for CVC4} %TODO style
+  \label{fig:ce_example0_p2}
+\end{figure}
 
-More information how counterexamples in Why3 works can be found
-in~\cite{hauzar16sefm} and in~\cite{dailler18jlamp}.
 
+\subsubsection{Notes on format of displayed values}
 
-%
-% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
-%
-% problem with set logic and counterexamples
-%
-% which provers
-%
-% where it is displayed
-%
-% how to interpret the display
-%
-% example
+The counterexamples can contain values of various types.
+\begin{itemize}
+\item Integer or real variables are displayed in decimal.
+\item Bitvectors are displayed in hexadecimal
+\item Integer range types are displayed in a specific notation showing their projection to integers
+\item Floating-point numbers are displayed both under a decimal approximation and an exact hexadecimal value. The special values \texttt{+oo}, \texttt{-oo} and \texttt{NaN} may occur too.
+\item Values from algebraic types and record types are displayed as in the Why3 syntax
+\item Map values are displayed in a specific syntax detailed below
+\end{itemize}
 
+To detail the display of map values, consider the following code with
+a trivially false postcondition:
+\begin{whycode}
+  use int.Int
+  use ref.Ref
+  use map.Map
+
+  let ghost test_map (ghost x : ref (map int int)) : unit
+    ensures { !x[0] <> !x[1] }
+  =
+    x := Map.set !x 0 3
+\end{whycode}
+Executing CVC4 with the ``counterexamples'' alternative on goal will trigger
+counterexamples:
+\begin{whycode}
+  use int.Int
+  use ref.Ref
+  use map.Map
+
+  let ghost test_map (ghost x : ref (map int int)) : unit
+  (* x = (1 => 3,others => 0) *)
+    ensures { !x[0] <> !x[1] }
+    (* x = (0 => 3,1 => 3,others => 0) *)
+  =
+    x := Map.set !x 0 3
+    (* x = (0 => 3,1 => 3,others => 0) *)
+\end{whycode}
+
+The notation for map is to be understood with indices on left of the arrows and
+values on the right ``(index => value)''. The meaning of the keyword \texttt{others} is
+the value for all indices that were not mentioned yet. This shows that setting
+the parameter \texttt{x} to a map that has value 3 for index 1 and zero for all other
+indices is a counterexample. We can check that this negates the
+\why{ensures} clause.
+
+\subsubsection{Known limitations}
+
+The counterexamples are known not to work on the following non-exhaustive list
+(which is undergoing active development):
+\begin{itemize}
+\item Code containing type polymorphism is often a problem due to the bad
+  interaction between monomorphisation techniques and counterexamples. This is
+  current an issue in particular for the Array module of the standard library.
+\item\relax [TODO: complete this list]
+\end{itemize}
 
+More information on the implementation of counterexamples in Why3 can
+be found in~\cite{hauzar16sefm} and in~\cite{dailler18jlamp}.  For the
+producing counterexamples using the Why3 API, see
+Section~\ref{sec:ce_api}.
 
 \section{The \texttt{replay} Command}
 \label{sec:why3replayer}
@@ -1068,6 +1161,8 @@ realize the given theories. See also Section~\ref{sec:realizations}.
 
 %%% Local Variables:
 %%% mode: latex
+%%% mode: flyspell
 %%% TeX-PDF-mode: t
 %%% TeX-master: "manual"
+%%% ispell-local-dictionary: "american"
 %%% End:

doc/why3ide-doc.conf

@@ -21,14 +21,14 @@ print_locs = false
 print_time_limit = false
 saving_policy = 2
 show_full_context = false
-task_height = 480
+task_height = 220
 tree_width = 384
 verbose = 0
 window_height = 768
 window_width = 1024
 
 [main]
-cntexample = false
+loadpath = "/home/cmarche/why3.master/share/stdlib"
 magic = 14
 memlimit = 1000
 running_provers_max = 2
@@ -46,10 +46,33 @@ version = "8.7.2"
 
 [prover]
 command = "alt-ergo -timelimit %t %f"
-command_steps = "alt-ergo -steps-bound %S %f"
+command_steps = "alt-ergo-2.2.0 -steps-bound %S %f"
 driver = "alt_ergo"
 in_place = false
 interactive = false
 name = "Alt-Ergo"
 shortcut = "alt-ergo"
-version = "2.0.0"
+version = "2.2.0"
+
+[prover]
+alternative = "counterexamples"
+command = "cvc4-1.6 --tlimit-per=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16_counterexample"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+shortcut = "cvc4-ce"
+version = "1.6"
+
+[prover]
+command = "cvc4-1.6 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+shortcut = "cvc4"
+version = "1.6"

examples/use_api/counterexample.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(*******************
+
+This file builds some goals based on logic.ml using the API and calls
+the cvc4 to query counterexamples for them
+
+Note: the comments of the form BEGIN{id} and END{id} are there for automatic extraction
+of the chapter "The Why3 API" of the manual
+******************)
+
+(* opening the Why3 library *)
+open Why3
+
+(* a ground propositional goal: true or false *)
+let fmla_true : Term.term = Term.t_true
+let fmla_false : Term.term = Term.t_false
+
+(* printing it *)
+open Format
+
+(* a propositional goal: A implies (A and B) *)
+
+(* BEGIN{ce_declarepropvars} *)
+let make_attribute (name: string) : Ident.attribute =
+  Ident.create_attribute ("model_trace:" ^ name)
+let prop_var_A : Term.lsymbol =
+  (* [user_position file line left_col right_col] *)
+  let loc = Loc.user_position "myfile.my_ext" 28 0 0  in
+  let attrs = Ident.Sattr.singleton (make_attribute "my_A") in
+  Term.create_psymbol (Ident.id_fresh ~attrs ~loc "A") []
+(* END{ce_declarepropvars} *)
+let prop_var_B : Term.lsymbol =
+  let loc = Loc.user_position "myfile.my_ext2" 101 0 0  in
+  let attrs = Ident.Sattr.singleton (make_attribute "my_B") in
+  Term.create_psymbol (Ident.id_fresh ~attrs ~loc "B") []
+
+(* BEGIN{ce_adaptgoals} *)
+let atom_A : Term.term = Term.ps_app prop_var_A []
+let atom_B : Term.term = Term.ps_app prop_var_B []
+(* Voluntarily wrong verification condition *)
+let fmla2 : Term.term =
+  Term.t_implies atom_A (Term.t_and atom_A atom_B)
+(* We add a location and attribute to indicate the start of a goal *)
+let fmla2 : Term.term =
+  let loc = Loc.user_position "myfile.my_ext" 42 28 91  in
+  let attrs = Ident.Sattr.singleton Ity.annot_attr in
+  (* Note that this remove any existing attribute/locations on fmla2 *)
+  Term.t_attr_set ~loc attrs fmla2
+(* END{ce_adaptgoals} *)
+
+let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
+
+let task2 = None
+let task2 = Task.add_param_decl task2 prop_var_A
+let task2 = Task.add_param_decl task2 prop_var_B
+(* BEGIN{ce_nobuiltin} *)
+let meta_ce = Theory.register_meta_excl "get_counterexmp" [Theory.MTstring]
+  ~desc:"Set@ when@ counter-example@ should@ be@ get."
+let task2 = Task.add_meta task2 meta_ce [Theory.MAstr ""]
+(* END{ce_nobuiltin} *)
+let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
+let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
+let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
+
+
+(* To call a prover, we need to access the Why configuration *)
+
+(* reads the config file *)
+let config : Whyconf.config = Whyconf.read_config None
+(* the [main] section of the config file *)
+let main : Whyconf.main = Whyconf.get_main config
+(* all the provers detected, from the config file *)
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers config
+
+(* BEGIN{ce_get_cvc4ce} *)
+(* One alternative for Cvc4 with counterexamples in the config file *)
+let cvc4 : Whyconf.config_prover =
+  let fp = Whyconf.parse_filter_prover "CVC4,,counterexamples" in
+  (* All provers alternative counterexamples that have the name CVC4 *)
+  let provers = Whyconf.filter_provers config fp in
+  if Whyconf.Mprover.is_empty provers then begin
+    eprintf "Prover Cvc4 not installed or not configured@.";
+    exit 0
+  end else
+    (* Most recent version found *)
+    snd (Whyconf.Mprover.max_binding provers)
+(* END{ce_get_cvc4ce} *)
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
+
+(* loading the Cvc4 driver *)
+let cvc4_driver : Driver.driver =
+  try
+    Whyconf.load_driver main env cvc4.Whyconf.driver []
+  with e ->
+    eprintf "Failed to load driver for Cvc4: %a@."
+      Exn_printer.exn_printer e;
+    exit 1
+
+(* calls Cvc4 *)
+let result1 : Call_provers.prover_result =
+  Call_provers.wait_on_call
+    (Driver.prove_task ~limit:Call_provers.empty_limit
+                       ~command:(Whyconf.get_complete_command cvc4 ~with_steps:false)
+    cvc4_driver task2)
+
+(* BEGIN{ce_callprover} *)
+(* prints Cvc4 answer *)
+let () = printf "@[On task 1, Cvc4 answers %a@."
+  Call_provers.print_prover_result result1
+
+let () = printf "Model is %a@."
+    (Model_parser.print_model_json ?me_name_trans:None ?vc_line_trans:None)
+    result1.Call_provers.pr_model
+(* END{ce_callprover} *)