Commit 88617ea2 authored by François Bobot's avatar François Bobot

Add the use of Expr in the manual

parent 12b304de
......@@ -1768,6 +1768,7 @@ bench-api:
$(MAKE) test-api-logic.@OCAMLBEST@
$(MAKE) test-api-transform.@OCAMLBEST@
$(MAKE) test-api-mlw-tree.@OCAMLBEST@
$(MAKE) test-api-mlw-expr.@OCAMLBEST@
# $(MAKE) test-api-mlw.@OCAMLBEST@
$(MAKE) test-session.@OCAMLBEST@
......@@ -1832,6 +1833,19 @@ test-api-mlw-tree.opt: examples/use_api/mlw_tree.ml lib/why3/why3.cmxa
|| (rm -f test-api-mlw-tree.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-tree.opt
test-api-mlw-expr.byte: examples/use_api/mlw_expr.ml lib/why3/why3.cma
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f test-api-mlw-expr.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-expr.byte;
test-api-mlw-expr.opt: examples/use_api/mlw_expr.ml lib/why3/why3.cmxa
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-mlw-expr.opt > /dev/null) \
|| (rm -f test-api-mlw-expr.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-expr.opt
test-api-mlw.byte: examples/use_api/mlw.ml lib/why3/why3.cma
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
......@@ -1936,6 +1950,9 @@ doc/generated/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_c
doc/generated/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@
doc/generated/mlw_expr__%.ml: examples/use_api/mlw_expr.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@
doc/generated/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@
......@@ -1960,6 +1977,8 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \
source1 code1 helper1 source2 code2 source3 code3 \
closemodule checkingvcs
OCAMLCODE_MLWEXPR = buildenv source2 code2_import code2 createmodule checkingvcs
OCAMLCODE_COUNTEREXAMPLES = ce_declarepropvars ce_adaptgoals \
ce_get_cvc4ce ce_callprover ce_nobuiltin
......@@ -1968,6 +1987,7 @@ OCAMLCODE = \
$(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/mlw_expr__, $(addsuffix .ml, $(OCAMLCODE_MLWEXPR))) \
$(addprefix doc/generated/counterexample__, $(addsuffix .ml, $(OCAMLCODE_COUNTEREXAMPLES))) \
doc/generated/whyconf__provertype.ml
......
......@@ -312,9 +312,16 @@ from an OCaml program.
\section{ML Programs}
The simplest way to build \whyml programs from OCaml is to build
untyped syntax trees for such programs, and then
call the \why typing procedure to build typed declarations.
One can build \whyml programs starting at different steps of the \whyml pipeline
(parsing, typing, VC generation). We present here two choices. The first is to build
an untyped syntax trees, and then
call the \why typing procedure to build typed declarations. The second choice is
to directly build the typed declaration. The first choice use concepts similar
to the \whyml language but errors in the generation are harder to debug since
they are lost inside the typing phase, the second choice use more internal
notions but it is easier to pinpoint the functions wrongly used.
\subsection{Untyped syntax tree}
The examples of this section are available in the file
\verb|examples/use_api/mlw_tree.ml| of the distribution.
......@@ -372,6 +379,36 @@ 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}
\subsection{Typed declaration}
The examples of this section are available in the file
\verb|examples/use_api/mlw_expr.ml| of the distribution.
The first step to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}.
\lstinputlisting{generated/mlw_expr__buildenv.ml}
To write our programs, we need to import some other modules from the
standard library integers and references. The only subtleties is to get logic
functions from the logical part of the modules
\verb|mod_theory.Theory.th_export| and the program functions from \verb|mod_export|.
\lstinputlisting{generated/mlw_expr__code2_import.ml}
We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_expr__source2.ml}
The OCaml code that programmatically build this Why3 function is as follows.
\lstinputlisting{generated/mlw_expr__code2.ml}
Having declared all the programs we wanted to write, we can now create the
module and generate the VCs.
\lstinputlisting{generated/mlw_expr__createmodule.ml}
We can then construct the proofs tasks for our module, and then try to
call the Alt-Ergo prover. The rest of that code is using OCaml
functions that were already introduced before.
\lstinputlisting{generated/mlw_expr__checkingvcs.ml}
\section{Generating counterexamples}
\label{sec:ce_api}
......
......@@ -118,7 +118,7 @@ let ref_fun : Expr.rsymbol =
(* the "!" function *)
let get_fun : Expr.rsymbol =
Pmodule.ns_find_rs ref_module.Pmodule.mod_export ["prefix !"]
Pmodule.ns_find_rs ref_module.Pmodule.mod_export [Ident.op_prefix "!"]
let d2 =
let id = Ident.id_fresh "f" in
......@@ -187,11 +187,12 @@ let d2 =
let d2' =
let id = Ident.id_fresh "f" in
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
in
let post =
Term.ps_app Term.ps_equ [Term.t_var result; Term.t_nat_const 0]
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
in
let post = Term.ps_app Term.ps_equ [Term.t_var result; Term.t_nat_const 0] in
Ity.create_post result post
in
let body =
(* building expression "ref 0" *)
......@@ -214,7 +215,7 @@ let d2' =
Ity.create_pvsymbol unit Ity.ity_unit
in
let def,rs = Expr.let_sym id
(Expr.c_fun [arg_unit] [post] [] Ity.Mxs.empty Ity.Mpv.empty body) in
(Expr.c_fun [arg_unit] [] [post] Ity.Mxs.empty Ity.Mpv.empty body) in
try
let def = Pdecl.create_let_decl def in
Format.eprintf "It works!@.";
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- 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 MLW modules, using parse trees instead of direct
API calls
******************)
(* BEGIN{buildenv} *)
open Why3
let config : Whyconf.config = Whyconf.read_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)
(* END{buildenv} *)
(*
declaration of
BEGIN{source2}
let f2 () : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
END{source2}
*)
(* BEGIN{code2_import} *)
let int_module : Pmodule.pmodule =
Pmodule.read_module env ["int"] "Int"
let ge_int : Term.lsymbol =
Theory.ns_find_ls int_module.Pmodule.mod_theory.Theory.th_export
[Ident.op_infix ">="]
let ref_module : Pmodule.pmodule =
Pmodule.read_module env ["ref"] "Ref"
let ref_type : Ity.itysymbol =
Pmodule.ns_find_its ref_module.Pmodule.mod_export ["ref"]
(* the "ref" function *)
let ref_fun : Expr.rsymbol =
Pmodule.ns_find_rs ref_module.Pmodule.mod_export ["ref"]
(* the "!" function *)
let get_fun : Expr.rsymbol =
Pmodule.ns_find_rs ref_module.Pmodule.mod_export [Ident.op_prefix "!"]
(* END{code2_import} *)
(* BEGIN{code2} *)
let d2 =
let id = Ident.id_fresh "f" in
let post =
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
in
let post = Term.ps_app ge_int [Term.t_var result; Term.t_nat_const 0] in
Ity.create_post result post
in
let body =
(* building expression "ref 42" *)
let e =
let c0 = Expr.e_const (Number.int_const_of_int 42) Ity.ity_int in
let refzero_type = Ity.ity_app ref_type [Ity.ity_int] [] in
Expr.e_app ref_fun [c0] [] refzero_type
in
(* building the first part of the let x = ref 42 *)
let id_x = Ident.id_fresh "x" in
let letdef, var_x = Expr.let_var id_x e in
(* building expression "!x" *)
let bang_x = Expr.e_app get_fun [Expr.e_var var_x] [] Ity.ity_int in
(* the complete body *)
Expr.e_let letdef bang_x
in
let arg_unit =
let unit = Ident.id_fresh "unit" in
Ity.create_pvsymbol unit Ity.ity_unit
in
let def,rs = Expr.let_sym id
(Expr.c_fun [arg_unit] [] [post] Ity.Mxs.empty Ity.Mpv.empty body) in
Pdecl.create_let_decl def
(* END{code2} *)
(* BEGIN{createmodule} *)
let mod2 =
let uc : Pmodule.pmodule_uc =
Pmodule.create_module env (Ident.id_fresh "MyModule")
in
let uc = Pmodule.use_export uc int_module in
let uc = Pmodule.use_export uc ref_module in
let uc = Pmodule.add_pdecl ~vc:true uc d2 in
Pmodule.close_module uc
(* END{createmodule} *)
(* Checking the VCs *)
(* BEGIN{checkingvcs} *)
let my_tasks : Task.task list =
Task.split_theory mod2.Pmodule.mod_theory None None
open Format
let () =
printf "Tasks are:@.";
let _ =
List.fold_left
(fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
1 my_tasks
in ()
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
let alt_ergo : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
(** all provers that have the name "Alt-Ergo" *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
eprintf "Prover Alt-Ergo not installed or not configured@.";
exit 0
end else
snd (Whyconf.Mprover.max_binding provers)
let alt_ergo_driver : Driver.driver =
try
Whyconf.load_driver main env alt_ergo.Whyconf.driver []
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
let () =
let _ =
List.fold_left
(fun i t ->
let r =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver t)
in
printf "@[On task %d, alt-ergo answers %a@."
i (Call_provers.print_prover_result ~json_model:false) r;
i+1
)
1 my_tasks
in ()
(* END{checkingvcs} *)
(*
Local Variables:
compile-command: "ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma -I `ocamlfind query menhirLib` menhirLib.cmo -I `ocamlfind query camlzip` zip.cma ../../lib/why3/why3.cma mlw_tree.ml"
End:
*)
......@@ -16,14 +16,12 @@ let exn_printers =
let register exn_printer = Stack.push exn_printer exn_printers
let () =
let all_exn_printer fmt exn =
Format.fprintf fmt "anomaly: %s" (Printexc.to_string exn) in
register all_exn_printer
let anomaly_exn_printer fmt exn =
Format.fprintf fmt "anomaly: %s" (Printexc.to_string exn)
exception Exit_loop
let exn_printer fmt exn =
let registered_exn_printer fmt exn =
let test f =
try
Format.fprintf fmt "@[%a@]" f exn;
......@@ -32,6 +30,24 @@ let exn_printer fmt exn =
| Exit_loop -> raise Exit_loop
| _ -> ()
in
try Stack.iter test exn_printers
Stack.iter test exn_printers
let exn_printer fmt exn =
try
registered_exn_printer fmt exn;
anomaly_exn_printer fmt exn
with Exit_loop -> ()
let () =
Printexc.register_printer (fun exn ->
let b = Buffer.create 10 in
let fmt = Format.formatter_of_buffer b in
try
registered_exn_printer fmt exn;
None
with Exit_loop ->
Format.pp_print_flush fmt ();
Some (Buffer.contents b)
)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment