Skip to content

GitLab

why3
why3
Commit 3d86e1c5 authored by Rehan MALAK's avatar Rehan MALAK
3 Browse files
Options

extends Ptree/Typing API to the entire mlw file

parent b88f3d74
Hide whitespace changes
Inline Side-by-side
Showing with 334 additions and 220 deletions
Makefile.in
View file @ 3d86e1c5
......@@ -1925,9 +1925,9 @@ OCAMLCODE_CALLPROVERS = proveranswer proverresult resourcelimit
OCAMLCODE_TRANSFORM = negate register
OCAMLCODE_MLWTREE = buildenv openmodule useimport \
source1 code1 helper1 source2 code2 source3 code3 \
closemodule checkingvcs
OCAMLCODE_MLWTREE = buildenv \
source1 code1 helper1 source2 code2 source3 code3 source4 code4 \
getmodules checkingvcs
OCAMLCODE_MLWEXPR = buildenv source2 code2_import code2 createmodule checkingvcs
......
doc/api.tex
View file @ 3d86e1c5
......@@ -328,51 +328,50 @@ The examples of this section are available in the file
The first step is to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}, and open the OCaml module
\verb|Ptree| which contains most of the OCaml functions we need in
\verb|Ptree| (``parse tree'') which contains most of the OCaml functions we need in
this section.
\lstinputlisting{generated/mlw_tree__buildenv.ml}
To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following
declarations, that first introduces a pseudo ``file'' to hold the
module, then the module itself called \verb|Program|.
\lstinputlisting{generated/mlw_tree__openmodule.ml}
Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without
any attributes nor any location.
To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally
imports \verb|int.Int|.
\lstinputlisting{generated/mlw_tree__useimport.ml}
We want now to build a program equivalent to the following code in concrete Why3 syntax.
Each of our example programs will build a module.
Let's consider the Why3 code.
\lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}
The OCaml code that programmatically build this Why3 function is as follows.
The Ocaml code that programmatically builds it is as follows.
\lstinputlisting{generated/mlw_tree__code1.ml}
This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}.
Most of the code is not using directly the \verb|Ptree| constructors
but instead makes uses of the helper
functions that are given in Figure~\ref{fig:helpers}.
Notice \verb|mk_ident| which builds an identifier (\verb|Ptree.ident|) without
any attributes nor any location and \verb|use_import| which lets us to import
some other modules and in particular the ones from the standard library. At the end,
our module is no more than the identifier and a list of two declarations (\verb|Ptree.decl list|)
\begin{figure}[t]
\lstinputlisting{generated/mlw_tree__helper1.ml}
\caption{Helper functions for building WhyML programs}
\label{fig:helpers}
\end{figure}
We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
The OCaml code that programmatically build this Why3 function is as follows.
\lstinputlisting{generated/mlw_tree__code2.ml}
The next example makes use of arrays.
We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}
The corresponding OCaml code is as follows
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
\lstinputlisting{generated/mlw_tree__code3.ml}
Having declared all the programs we wanted to write, we can now close
the module and the file, and get as a result the set of modules of our
The next example makes use of arrays.
\lstinputlisting[language=why3]{generated/mlw_tree__source4.ml}
The corresponding OCaml code is as follows
\lstinputlisting{generated/mlw_tree__code4.ml}
Having declared all the modules we wanted to write, we can now call the \why typing procedure
and get as a result the set of modules of our
file, under the form of a map of module names to modules.
\lstinputlisting{generated/mlw_tree__closemodule.ml}
\lstinputlisting{generated/mlw_tree__getmodules.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
......
examples/use_api/mlw_tree.ml
View file @ 3d86e1c5
......@@ -24,19 +24,10 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
(* END{buildenv} *)
(* start a module *)
(* BEGIN{openmodule} *)
let () = Typing.open_file env [] (* empty pathname *)
(* BEGIN{helper1} *)
let mk_ident s = { id_str = s; id_ats = []; id_loc = Loc.dummy_position }
let () = Typing.open_module (mk_ident "Program")
(* END{openmodule} *)
(* use int.Int *)
(* BEGIN{useimport} *)
let mk_qid l =
let mk_qualid l =
let rec aux l =
match l with
| [] -> assert false
......@@ -45,17 +36,10 @@ let mk_qid l =
in
aux (List.rev l)
let use_import (f, m) =
let m = mk_ident m in
let loc = Loc.dummy_position in
Typing.open_scope loc m;
Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_ident f), m)));
Typing.close_scope loc ~import:true
let use_int_Int = use_import ("int","Int")
(* END{useimport} *)
let use_import l =
let qid_id_opt = (mk_qualid l, None) in
Duseimport(Loc.dummy_position,false,[qid_id_opt])
(* BEGIN{helper1} *)
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
let mk_term t = { term_desc = t; term_loc = Loc.dummy_position }
......@@ -84,162 +68,236 @@ let mk_evar x = mk_expr(Eident(Qident x))
(* declaration of
BEGIN{source1}
let f1 (x:int) : unit
requires { x=6 }
ensures { result=42 }
= x*7
module M1
use int.Int
goal g : 2 + 2 = 4
end
END{source1}
*)
(* BEGIN{code1} *)
let eq_symb = mk_qid [Ident.op_infix "="]
let int_type_id = mk_qid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = mk_qid ["Int";Ident.op_infix "*"]
let d1 : decl =
let id_x = mk_ident "x" in
let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst 6] in
let result = mk_ident "result" in
let post = mk_tapp eq_symb [mk_var result; mk_tconst 42] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst 7] in
let f1 =
Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body)
let mod_M1 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* goal g : 2 + 2 = 4 *)
let g =
let two = mk_tconst 2 in
let four = mk_tconst 4 in
let add_int = mk_qualid ["Int";Ident.op_infix "+"] in
let two_plus_two = mk_tapp add_int [two ; two] in
let eq_int = mk_qualid ["Int";Ident.op_infix "="] in
let goal_term = mk_tapp eq_int [four ; two_plus_two] in
Dprop(Pgoal,mk_ident "g",goal_term)
in
Dlet(mk_ident "f1",false,Expr.RKnone, mk_expr f1)
let () =
try Typing.add_decl Loc.dummy_position d1
with e ->
Format.printf "Exception raised during typing of d:@ %a@."
Exn_printer.exn_printer e
(mk_ident "M1",[use_int_Int ; g])
(* END{code1} *)
(*
declaration of
BEGIN{source2}
let f2 () : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
END{source2}
*)
(* declaration of
BEGIN{source2}
module M2
let f (x:int) : int
requires { x=6 }
ensures { result=42 }
= x*7
end
END{source2}
*)
(* BEGIN{code2} *)
let ge_int = mk_qid ["Int";Ident.op_infix ">="]
let use_ref_Ref = use_import ("ref","Ref")
let d2 =
let result = mk_ident "result" in
let post = mk_term(Tidapp(ge_int,[mk_var result;mk_tconst 0])) in
let spec = {
sp_pre = [];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
let e1 = mk_eapp (mk_qid ["Ref";"ref"]) [mk_econst 42] in
let eq_symb = mk_qualid [Ident.op_infix "="]
let int_type_id = mk_qualid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = mk_qualid ["Int";Ident.op_infix "*"]
let mod_M2 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* f *)
let f =
let id_x = mk_ident "x" in
let e2 = mk_eapp (mk_qid ["Ref";Ident.op_prefix "!"]) [mk_evar id_x] in
mk_expr(Elet(id_x,false,Expr.RKlocal,e1,e2))
let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst 6] in
let result = mk_ident "result" in
let post = mk_tapp eq_symb [mk_var result; mk_tconst 42] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst 7] in
let f =
Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body)
in
Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
in
let f = Efun(param0,None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f2",false,Expr.RKnone, mk_expr f)
let () =
try Typing.add_decl Loc.dummy_position d2
with e ->
Format.printf "Exception raised during typing of d2:@ %a@."
Exn_printer.exn_printer e
(mk_ident "M2",[use_int_Int ; f])
(* END{code2} *)
(*
BEGIN{source3}
let f (a:array int) : unit
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
END{source3}
*)
(* BEGIN{code3} *)
let () = use_import ("array","Array")
let array_int_type = PTtyapp(mk_qid ["Array";"array"],[int_type])
let length = mk_qid ["Array";"length"]
(* declaration of
BEGIN{source3}
module M3
let f() : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
end
END{source3}
*)
let array_get = mk_qid ["Array"; Ident.op_get ""]
(* BEGIN{code3} *)
let ge_int = mk_qualid ["Int";Ident.op_infix ">="]
let mod_M3 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* use ref.Ref *)
let use_ref_Ref = use_import (["ref";"Ref"]) in
(* f *)
let f =
let result = mk_ident "result" in
let post = mk_term(Tidapp(ge_int,[mk_var result;mk_tconst 0])) in
let spec = {
sp_pre = [];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
let e1 = mk_eapp (mk_qualid ["Ref";"ref"]) [mk_econst 42] in
let id_x = mk_ident "x" in
let qid = mk_qualid ["Ref";Ident.op_prefix "!"] in
let e2 = mk_eapp qid [mk_evar id_x] in
mk_expr(Elet(id_x,false,Expr.RKnone,e1,e2))
in
let f = Efun(param0,None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
in
(mk_ident "M3",[use_int_Int ; use_ref_Ref ; f])
(* END{code3} *)
let array_set = mk_qid ["Array"; Ident.op_set ""]
(* declaration of
BEGIN{source4}
module M4
let f (a:array int) : unit
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
end
END{source4}
*)
let d3 =
let id_a = mk_ident "a" in
let pre =
mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst 1]
(* BEGIN{code4} *)
let array_int_type = PTtyapp(mk_qualid ["Array";"array"],[int_type])
let length = mk_qualid ["Array";"length"]
let array_get = mk_qualid ["Array"; Ident.op_get ""]
let array_set = mk_qualid ["Array"; Ident.op_set ""]
let mod_M4 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* use array.Array *)
let use_array_Array = use_import (["array";"Array"]) in
(* use f *)
let f =
let id_a = mk_ident "a" in
let pre =
mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst 1]
in
let post =
mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst 0];
mk_tconst 42]
in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[mk_pat Pwild,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
mk_eapp array_set [mk_evar id_a; mk_econst 0; mk_econst 42]
in
let f = Efun(param1 id_a array_int_type,
None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f", false, Expr.RKnone, mk_expr f)
in
let post =
mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst 0];
mk_tconst 42]
in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[mk_pat Pwild,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
mk_eapp array_set [mk_evar id_a; mk_econst 0; mk_econst 42]
(mk_ident "M4",[use_int_Int ; use_array_Array ; f])
(* END{code4} *)
(* The following example is not in the manual
* it shows how to use Ptree API for scope/import declarations
module M5
scope S
function f (x : int) : int = x
end
import S
goal g : f 2 = 2
end
*)
let mod_M5 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* scope S *)
let scope_S =
(* f *)
let f =
let logic = {
ld_loc = Loc.dummy_position;
ld_ident = mk_ident "f";
ld_params = [(Loc.dummy_position,Some (mk_ident "x"),false,int_type)] ;
ld_type = Some int_type;
ld_def = Some (mk_var (mk_ident "x")) ;
} in
Dlogic([logic])
in
Dscope(Loc.dummy_position,false,mk_ident "S",[f])
in
let f = Efun(param1 id_a array_int_type,
None,Ity.MaskVisible,spec,body)
(* import S *)
let import_S = Dimport (mk_qualid ["S"]) in
(* goal g : f 2 = 2 *)
let g =
let two = mk_tconst 2 in
let eq_int = mk_qualid ["Int";Ident.op_infix "="] in
let f_of_two = mk_tapp (mk_qualid ["f"]) [two] in
let goal_term = mk_tapp eq_int [f_of_two ; two] in
Dprop(Pgoal,mk_ident "g",goal_term)
in
Dlet(mk_ident "f3", false, Expr.RKnone, mk_expr f)
let () =
try Typing.add_decl Loc.dummy_position d3
with e ->
Format.printf "Exception raised during typing of d3:@ %a@."
Exn_printer.exn_printer e
(* END{code3} *)
(mk_ident "M5",[use_int_Int ; scope_S ; import_S ; g])
(* BEGIN{closemodule} *)
let () = Typing.close_module Loc.dummy_position
let mods : Pmodule.pmodule Wstdlib.Mstr.t = Typing.close_file ()
(* END{closemodule} *)
(* BEGIN{getmodules} *)
let mods =
let mlw_file = Modules [mod_M1 ; mod_M2 ; mod_M3 ; mod_M4] in
Typing.type_mlw_file env [] "myfile.mlw" mlw_file
(* END{getmodules} *)
(* Checking the VCs *)
......
plugins/python/py_main.ml
View file @ 3d86e1c5
......@@ -309,7 +309,7 @@ and block env ~loc = function
let e = Efun (params, None, Ity.MaskVisible, sp, body) in
Elet (id, false, Expr.RKnone, mk_expr ~loc e, s) in
mk_expr ~loc e
| (Dimport _ | Py_ast.Dlogic _) :: sl ->
| (Py_ast.Dimport _ | Py_ast.Dlogic _) :: sl ->
block env ~loc sl
let fresh_type_var =
......@@ -350,7 +350,8 @@ let read_channel env path file c =
let use_import (f, m) =
let m = mk_id ~loc m in
Typing.open_scope loc m;
Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_id ~loc f), m)));
let decl = Ptree.Duseimport(loc,false,[((Qdot (Qident (mk_id ~loc f), m)),None)]) in
Typing.add_decl loc decl ;
Typing.close_scope loc ~import:true in
List.iter use_import
["int", "Int"; "ref", "Refint"; "python", "Python"];
......
src/parser/parser.mly
View file @ 3d86e1c5
......@@ -12,10 +12,6 @@
%{
open Ptree
let qualid_last = function Qident x | Qdot (_, x) -> x
let use_as q = function Some x -> x | None -> qualid_last q
let floc s e = Loc.extract (s,e)
let add_attr id l = (* id.id_ats is usually nil *)
......@@ -322,7 +318,7 @@ module_decl:
| scope_head module_decl* END
{ Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
| IMPORT uqualid
{ Typing.import_scope (floc $startpos $endpos) $2 }
{ Typing.add_decl (floc $startpos $endpos) (Dimport($2)) }
| d = pure_decl | d = prog_decl | d = meta_decl
{ Typing.add_decl (floc $startpos $endpos) d;
add_record_projections d
......@@ -347,27 +343,33 @@ module_decl_no_head:
use_clone:
| USE EXPORT tqualid
{ Typing.add_decl (floc $startpos $endpos) (Duse $3) }
{ let loc = floc $startpos $endpos in
let decl = Ptree.Duseexport $3 in
Typing.add_decl loc decl
}
| CLONE EXPORT tqualid clone_subst
{ Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
{ let loc = floc $startpos $endpos in
let decl = Ptree.Dcloneexport($3,$4) in
Typing.add_decl loc decl
}
| USE boption(IMPORT) m_as_list = comma_list1(use_as)
{ let loc = floc $startpos $endpos in
let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
if $2 && not exists_as then Warning.emit ~loc
let import = $2 in
if import && not exists_as then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
let add_import (m, q) = let import = $2 || q = None in
Typing.open_scope loc (use_as m q);
Typing.add_decl loc (Duse m);
Typing.close_scope loc ~import in
List.iter add_import m_as_list }
let decl = Ptree.Duseimport(loc,import,m_as_list) in
Typing.add_decl loc decl
}
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
{ let loc = floc $startpos $endpos in
if $2 && $4 = None then Warning.emit ~loc
let import = $2 in
let as_opt = $4 in
if import && as_opt = None then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
let import = $2 || $4 = None in
Typing.open_scope loc (use_as $3 $4);
Typing.add_decl loc (Dclone ($3, $5));
Typing.close_scope loc ~import }
let decl = Ptree.Dcloneimport(loc,import,$3,as_opt,$5) in
Typing.add_decl loc decl
}
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }
......
src/parser/ptree.ml
View file @ 3d86e1c5
......@@ -263,7 +263,19 @@ type decl =
(** declaration of global exceptions *)
| Dmeta of ident * metarg list
(** `meta` *)
| Dclone of qualid * clone_subst list
| Dcloneexport of qualid * clone_subst list
(** `clone` *)
| Duse of qualid
| Duseexport of qualid
(** `use` *)
| Dcloneimport of Loc.position * bool * qualid * ident option * clone_subst list
(** `clone import ... as ...` *)
| Duseimport of Loc.position * bool * (qualid * ident option) list
(** `use import ... as ...` *)
| Dimport of qualid
(** `import` *)
| Dscope of Loc.position * bool * ident * decl list
(** `scope` *)
type mlw_file =