Skip to content

GitLab

why3
why3
Commit 8c49b08e authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

programs: parsing of annotations done later (ocamlyacc is not reentrant at all); typing exceptions

parent 87fa1632
Hide whitespace changes
Inline Side-by-side
Showing with 345 additions and 87 deletions
Makefile.in
View file @ 8c49b08e
......@@ -511,6 +511,9 @@ test: bin/why.byte $(TOOLS)
testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte -I theories/ tests/test-pgm-jcf.mlw
bench/programs/good/%: bin/whyml.byte
bin/whyml.byte -I theories bench/programs/good/$*.mlw
examples/programs/%: bin/whyml.byte
bin/whyml.byte -I theories examples/programs/$*.mlw
......
bench/bench
View file @ 8c49b08e
......@@ -111,6 +111,7 @@ echo ""
echo "=== Type-checking good programs ==="
pgml_options=--type-only
programs bench/programs/good
programs examples/programs
echo ""
bench/programs/good/exns.mlw 0 → 100644
View file @ 8c49b08e
(* exception without argument *)
exception E
let p1 () = {} (raise E : unit) { false } | E -> { true }
(* exception with an argument *)
exception F of int
let p2 () = {} raise (F 1) : unit { false } | F -> { result = 1 }
let p2a () =
{} raise (F (raise E : int)) : unit { false } | E -> { true } | F -> { false }
(* composition of exceptions with other constructs *)
let p3 () =
{} begin raise (F 1); raise (F 2) : unit end { false } | F -> { result = 1 }
let p4 () =
{}
(if True then raise (F 1) else raise (F 2)) : unit
{ false } | F -> { result = 1 }
let p5 () =
{}
begin
if True then raise (F 1);
raise E : unit
end
{ false } | E -> { false } | F -> { result = 1 }
let p6 () =
{}
begin
if False then raise (F 1);
raise E : unit
end
{ false } | E -> { true } | F -> { false }
(* composition of exceptions with side-effect on a reference *)
parameter x : int ref
let p7 () =
{} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
let p8 () =
{}
begin x := 1; raise (F !x); x := 2 end
{ false } | F -> { !x = 1 and result = 1 }
let p9 () =
{}
(raise (F begin x := 1; !x end) : unit)
{ false } | F -> { !x = 1 and result = 1 }
(* try / with *)
let p10 () = {} (try raise E : int with E -> 0 end) { result = 0 }
let p11 () = {} (try raise (F 1) : int with F x -> x end) { result = 1 }
let p12 () =
{}
try
begin raise E; raise (F 1); 1 end
with E -> 2
| F x -> 3
end
{ result = 2 }
let p13 () =
{}
try
begin raise E; raise (F 1); x := 1 end
with E -> x := 2
| F _ -> x := 3
end
{ !x = 2 }
let p13a () =
{}
try
(if !x = 1 then raise E)
(*{ true | E => x = 1 }*)
with E ->
x := 0
end
{ !x <> 1 }
exception E1
exception E2
exception E3
let p14 () =
{}
begin
if !x = 1 then raise E1;
if !x = 2 then raise E2;
if !x = 3 then raise E3;
raise E : unit
end
{ false } | E1 -> { !x = 1 } | E2 -> { !x = 2 } | E3 -> { !x = 3 }
| E -> { !x <> 1 and !x <> 2 and !x <> 3 }
let p15 () =
{}
if !x = 0 then raise E else (x := 0; raise (F !x)) : unit
{ false } | E -> { !x=0 } | F -> { result=0 }
let p16 () = {} if !x = 0 then (x:=1; raise E) { !x<>0 } | E -> { !x=1 }
let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { !x=0 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exns"
End:
*)
examples/programs/dijkstra.mlw
View file @ 8c49b08e
{
use set.Fset as S
use array.Array as M
......@@ -205,7 +204,6 @@ let shortest_path_code (src:vertex) (dst:vertex) =
(forall v:vertex.
not S.mem(v, !visited) -> forall dv:int. not path(src, v, dv)) }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/dijkstra"
......
src/programs/pgm_lexer.mll
View file @ 8c49b08e
......@@ -39,6 +39,7 @@
(fun (x,y) -> Hashtbl.add keywords x y)
[ "absurd", ABSURD;
"and", AND;
"any", ANY;
"as", AS;
"assert", ASSERT;
"assume", ASSUME;
......@@ -146,8 +147,6 @@ rule token = parse
{ LEFTPAR }
| ")"
{ RIGHTPAR }
| "()"
{ UIDENT "Unit" }
| ":"
{ COLON }
| ";"
......
src/programs/pgm_parser.mly
View file @ 8c49b08e
......@@ -68,31 +68,24 @@
let id = { id = prefix op; id_loc = loc_i 1 } in
mk_expr (mk_apply_id id [e1])
let id_unit () = { id = "Unit"; id_loc = loc () }
let id_unit () = { id = "unit"; id_loc = loc () }
let id_result () = { id = "result"; id_loc = loc () }
let id_anonymous () = { id = "_"; id_loc = loc () }
let lexpr_true () = { Ptree.pp_loc = loc (); Ptree.pp_desc = PPtrue }
let lexpr_false () = { Ptree.pp_loc = loc (); Ptree.pp_desc = PPfalse }
let ty_unit () = Tpure (PPTtyapp ([], Qident (id_unit ())))
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
let reloc loc lb =
lb.lex_curr_p <- loc;
lb.lex_abs_pos <- loc.pos_cnum
let parse_string f loc s =
let lb = Lexing.from_string s in
reloc loc lb;
f lb
let logic_list0_decl (loc, s) = parse_string Lexer.parse_list0_decl loc s
let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
let lexpr_true () = symbol_start_pos (), "true"
let lexpr_false () = symbol_start_pos (), "false"
let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
let type_c p ty ef q =
{ pc_result_name = id_result ();
pc_result_type = ty;
pc_effect = ef;
pc_pre = p;
pc_post = q; }
%}
/* Tokens */
......@@ -106,7 +99,7 @@
/* keywords */
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT OF PARAMETER
%token RAISE RAISES READS REC
......@@ -121,6 +114,9 @@
/* Precedences */
%nonassoc prec_post
%nonassoc BAR
%nonassoc prec_recfun
%nonassoc prec_triple
%left LEFTBLEFTB
......@@ -154,6 +150,8 @@
%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE
/* Entry points */
%type <Pgm_ptree.file> file
......@@ -181,7 +179,7 @@ list1_decl:
decl:
| LOGIC
{ Dlogic (logic_list0_decl $1) }
{ Dlogic $1 (*(logic_list0_decl $1)*) }
| LET lident EQUAL expr
{ Dlet ($2, $4) }
| LET lident list1_type_v_binder EQUAL triple
......@@ -268,7 +266,7 @@ expr:
| expr SEMICOLON expr
{ mk_expr (Esequence ($1, $3)) }
| assertion_kind LOGIC
{ mk_expr (Eassert ($1, lexpr $2)) }
{ mk_expr (Eassert ($1, $2)) }
| expr AMPAMP expr
{ mk_expr (Elazy (LazyAnd, $1, $3)) }
| expr BARBAR expr
......@@ -297,13 +295,17 @@ expr:
{ mk_expr (Eraise ($2, None)) }
| RAISE LEFTPAR uident expr RIGHTPAR
{ mk_expr (Eraise ($3, Some $4)) }
| TRY expr WITH option_bar list1_handler_sep_bar END
{ mk_expr (Etry ($2, $5)) }
| ANY simple_type_c
{ mk_expr (Eany $2) }
;
triple:
| LOGIC expr LOGIC
{ lexpr $1, $2, lexpr $3 }
| pre expr post
{ $1, $2, $3 }
| expr %prec prec_triple
{ lexpr_true (), $1, lexpr_true () }
{ lexpr_true (), $1, (lexpr_true (), []) }
;
simple_expr:
......@@ -338,6 +340,17 @@ option_bar:
| BAR { () }
;
list1_handler_sep_bar:
| handler { [$1] }
| handler BAR list1_handler_sep_bar { $1 :: $3 }
;
handler:
| ident ARROW expr { ($1, None, $3) }
| ident ident ARROW expr { ($1, Some $2, $4) }
| ident UNDERSCORE ARROW expr { ($1, Some (id_anonymous ()), $4) }
;
match_cases:
| match_case { [$1] }
| match_case BAR match_cases { $1::$3 }
......@@ -371,13 +384,13 @@ loop_annotation:
;
loop_invariant:
| INVARIANT LOGIC { Some (lexpr $2) }
| /* epsilon */ { None }
| INVARIANT LOGIC { Some $2 }
| /* epsilon */ { None }
;
loop_variant:
| VARIANT LOGIC { Some (lexpr $2) }
| /* epsilon */ { None }
| VARIANT LOGIC { Some $2 }
| /* epsilon */ { None }
;
constant:
......@@ -414,14 +427,10 @@ list1_type_v_binder:
type_v_binder:
| lident { $1, None }
| LEFTPAR RIGHTPAR { id_anonymous (), Some (ty_unit ()) }
| LEFTPAR lident COLON type_v RIGHTPAR { $2, Some $4 }
;
opt_colon_spec:
| /* epsilon */ { None }
| COLON type_c { Some $2 }
;
type_v:
| simple_type_v
{ $1 }
......@@ -440,17 +449,38 @@ simple_type_v:
type_c:
| type_v
{ { pc_result_name = id_result ();
pc_result_type = $1;
pc_effect = empty_effect;
pc_pre = lexpr_true ();
pc_post = lexpr_true (); } }
| LOGIC type_v effects LOGIC
{ { pc_result_name = id_result ();
pc_result_type = $2;
pc_effect = $3;
pc_pre = lexpr $1;
pc_post = lexpr $4; } }
{ type_c (lexpr_true ()) $1 empty_effect (lexpr_true (), []) }
| pre type_v effects post
{ type_c $1 $2 $3 $4 }
;
simple_type_c:
| simple_type_v
{ type_c (lexpr_true ()) $1 empty_effect (lexpr_true (), []) }
| pre type_v effects post
{ type_c $1 $2 $3 $4 }
;
pre:
| LOGIC { $1 }
;
post:
| LOGIC list0_post_exn { $1, $2 }
;
list0_post_exn:
| /* epsilon */ %prec prec_post { [] }
| list1_post_exn { $1 }
;
list1_post_exn:
| post_exn %prec prec_post { [$1] }
| post_exn list1_post_exn { $1 :: $2 }
;
post_exn:
| BAR uident ARROW LOGIC { $2, $4 }
;
effects:
......@@ -475,7 +505,7 @@ opt_raises:
opt_variant:
| /* epsilon */ { None }
| VARIANT LOGIC { Some (lexpr $2) }
| VARIANT LOGIC { Some $2 }
;
list0_lident_sep_comma:
......
src/programs/pgm_ptree.ml
View file @ 8c49b08e
......@@ -29,10 +29,12 @@ type constant = Term.constant
type assertion_kind = Aassert | Aassume | Acheck
type lexpr = Ptree.lexpr
type lazy_op = LazyAnd | LazyOr
type logic = Lexing.position * string
type lexpr = logic
type loop_annotation = {
loop_invariant : lexpr option;
loop_variant : lexpr option;
......@@ -44,6 +46,10 @@ type effect = {
pe_raises : ident list;
}
type pre = lexpr
type post = lexpr * (ident * lexpr) list
type type_v =
| Tpure of Ptree.pty
| Tarrow of binder list * type_c
......@@ -52,8 +58,8 @@ and type_c =
{ pc_result_name : ident;
pc_result_type : type_v;
pc_effect : effect;
pc_pre : lexpr;
pc_post : lexpr; }
pc_pre : pre;
pc_post : post; }
and binder = ident * type_v option
......@@ -81,20 +87,22 @@ and expr_desc =
| Eskip
| Eabsurd
| Eraise of ident * expr option
| Etry of expr * (ident * ident option * expr) list
(* annotations *)
| Eassert of assertion_kind * lexpr
| Eghost of expr
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
| Eany of type_c
(* TODO: try, any, post?, ghost *)
(* TODO: post?, ghost *)
and triple = lexpr * expr * lexpr
and triple = pre * expr * post
type decl =
| Dlet of ident * expr
| Dletrec of (ident * binder list * variant option * triple) list
| Dlogic of Ptree.decl list
| Dlogic of logic
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
......
src/programs/pgm_ttree.ml
View file @ 8c49b08e
......@@ -41,6 +41,10 @@ type deffect = {
type dlexpr = Typing.denv * Ptree.lexpr
type dpre = dlexpr
type dpost = dlexpr * (Term.lsymbol * dlexpr) list
type dtype_v =
| DTpure of Denv.dty
| DTarrow of dbinder list * dtype_c
......@@ -49,12 +53,17 @@ and dtype_c =
{ dc_result_name : string;
dc_result_type : dtype_v;
dc_effect : deffect;
dc_pre : dlexpr;
dc_post : dlexpr; }
dc_pre : dpre;
dc_post : dpost; }
and dbinder = string * dtype_v
type dvariant = Pgm_ptree.lexpr
type dloop_annotation = {
dloop_invariant : Ptree.lexpr option;
dloop_variant : Ptree.lexpr option;
}
type dvariant = Ptree.lexpr
type dexpr = {
dexpr_desc : dexpr_desc;
......@@ -76,18 +85,19 @@ and dexpr_desc =
| DEsequence of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEwhile of dexpr * Pgm_ptree.loop_annotation * dexpr
| DEwhile of dexpr * dloop_annotation * dexpr
| DElazy of lazy_op * dexpr * dexpr
| DEmatch of dexpr list * (Typing.dpattern list * dexpr) list
| DEskip
| DEabsurd
| DEraise of Term.lsymbol * dexpr option
| DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
| DEassert of assertion_kind * Ptree.lexpr
| DEghost of dexpr
| DElabel of string * dexpr
and dtriple = dlexpr * dexpr * dlexpr
and dtriple = dpre * dexpr * dpost
(* phase 2: typing annotations *)
......@@ -103,6 +113,10 @@ type effect = {
e_raises : Term.lsymbol list;
}
type pre = Term.fmla
type post = Term.fmla * (Term.lsymbol * Term.fmla) list
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
......@@ -111,8 +125,8 @@ and type_c =
{ c_result_name : Term.vsymbol;
c_result_type : type_v;
c_effect : effect;
c_pre : Term.fmla;
c_post : Term.fmla; }
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
......@@ -144,6 +158,7 @@ and expr_desc =
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
......@@ -151,7 +166,7 @@ and expr_desc =
and recfun = Term.vsymbol * binder list * variant option * triple
and triple = Term.fmla * expr * Term.fmla
and triple = pre * expr * post
type decl =
| Dlet of Term.lsymbol * expr
......
src/programs/pgm_typing.ml
View file @ 8c49b08e
......@@ -54,6 +54,22 @@ let report fmt = function
let id_result = "result"
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
let reloc loc lb =
lb.Lexing.lex_curr_p <- loc;
lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum
let parse_string f loc s =
let lb = Lexing.from_string s in
reloc loc lb;
f lb
let logic_list0_decl (loc, s) = parse_string Lexer.parse_list0_decl loc s
let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
(* environments *)
let ts_unit uc = ns_find_ts (get_namespace uc) ["unit"]
......@@ -144,6 +160,19 @@ let deffect env e =
List.map (fun id -> let ls,_,_ = dexception env id in ls)
e.Pgm_ptree.pe_raises; }
let dpost env ty (q, ql) =
let dexn (id, l) =
let s, tyl, _ = dexception env id in
let denv = match tyl with
| [] -> env.denv
| [ty] -> Typing.add_var id_result ty env.denv
| _ -> assert false
in
s, (denv, lexpr l)
in
let denv = Typing.add_var id_result ty env.denv in
(denv, lexpr q), List.map dexn ql
let rec dtype_v env = function
| Pgm_ptree.Tpure pt ->
DTpure (pure_type env pt)
......@@ -157,10 +186,8 @@ and dtype_c env c =
{ dc_result_name = c.Pgm_ptree.pc_result_name.id;
dc_result_type = ty;
dc_effect = deffect env c.Pgm_ptree.pc_effect;
dc_pre = env.denv, c.Pgm_ptree.pc_pre;
dc_post =
let denv = Typing.add_var id_result (dpurify env ty) env.denv in
denv, c.Pgm_ptree.pc_post;
dc_pre = env.denv, lexpr c.Pgm_ptree.pc_pre;
dc_post = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
}
and dbinder env ({id=x; id_loc=loc}, v) =
......@@ -172,6 +199,10 @@ and dbinder env ({id=x; id_loc=loc}, v) =
let env = { env with denv = Typing.add_var x ty env.denv } in
env, (x, v)
let dloop_annotation a =
{ dloop_invariant = option_map lexpr a.Pgm_ptree.loop_invariant;
dloop_variant = option_map lexpr a.Pgm_ptree.loop_variant; }
let rec dexpr env e =
let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
{ dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
......@@ -232,7 +263,7 @@ and dexpr_desc env loc = function
expected_type e1 (dty_bool env.uc);
let e2 = dexpr env e2 in
expected_type e2 (dty_unit env.uc);
DEwhile (e1, a, e2), (dty_unit env.uc)
DEwhile (e1, dloop_annotation a, e2), (dty_unit env.uc)
| Pgm_ptree.Elazy (op, e1, e2) ->
let e1 = dexpr env e1 in
expected_type e1 (dty_bool env.uc);
......@@ -274,9 +305,31 @@ and dexpr_desc env loc = function
assert false
in
DEraise (ls, e), create_type_var loc
| Pgm_ptree.Etry (e1, hl) ->
let e1 = dexpr env e1 in
let handler (id, x, h) =
let ls, tyl, _ = dexception env id in
let x, env = match x, tyl with
| Some _, [] ->
errorm ~loc "expection %s has no argument" id.id
| None, [] ->
None, env
| None, [ty] ->
errorm ~loc "exception %s is expecting an argument of type %a"
id.id print_dty ty;
| Some x, [ty] ->
Some x.id, { env with denv = Typing.add_var x.id ty env.denv }
| _ ->
assert false
in
let h = dexpr env h in
expected_type h e1.dexpr_type;
(ls, x, h)
in
DEtry (e1, List.map handler hl), e1.dexpr_type
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, le), (dty_unit env.uc)
DEassert (k, lexpr le), (dty_unit env.uc)
| Pgm_ptree.Eghost e1 ->
let e1 = dexpr env e1 in
DEghost e1, e1.dexpr_type
......@@ -290,13 +343,16 @@ and dexpr_desc env loc = function
let ty = pure_type env ty in
expected_type e1 ty;
e1.dexpr_desc, ty
| Pgm_ptree.Eany _c ->
(* let c = dtype_c env c in *)
(* DEany c, c.dc_result_type *)assert false (*TODO*)
and dletrec env dl =
(* add all functions into environment *)
let add_one env (id, bl, var, t) =
let ty = create_type_var id.id_loc in
let env = { env with denv = Typing.add_var id.id ty env.denv } in
env, ((id, ty), bl, var, t)
env, ((id, ty), bl, option_map lexpr var, t)
in
let env, dl = map_fold_left add_one env dl in
(* then type-check all of them and unify *)
......@@ -314,11 +370,10 @@ and dletrec env dl =
env, List.map type_one dl
and dtriple env (p, e, q) =
let p = env.denv, p in
let p = env.denv, lexpr p in
let e = dexpr env e in
let ty = e.dexpr_type in
let denvq = Typing.add_var id_result ty env.denv in
let q = denvq, q in
let q = dpost env ty q in
(p, e, q)
(* phase 2: typing annotations *)
......@@ -342,6 +397,26 @@ let effect uc env e =
e_writes = List.map (reference uc env) e.de_writes;
e_raises = e.de_raises; }
let pre env (denv, l) = Typing.type_fmla denv env l
let post env ty (q, ql) =
let exn (ls, (denv, l)) =
let env = match ls.ls_args with
| [] ->
env
| [ty] ->
let v_result = create_vsymbol (id_fresh id_result) ty in
Mstr.add id_result v_result env