Commit 019647ce authored by MARCHE Claude's avatar MARCHE Claude

fix syntax of var decl, allow ghost var

parent 31d776b9
......@@ -309,7 +309,6 @@ WhyML declaration is allowed, plus an additional declaration of
program function with following form, introduced by keywords `let cfg`:
..
`let` `cfg` :math:`f (x_1:t_1) ... (x_n:t_n) : t`
`requires` { :math:`Pre` }
`ensures` { :math:`Post` }
......@@ -318,7 +317,7 @@ program function with following form, introduced by keywords `let cfg`:
...
`var` :math:`y_k : u_k`;
`{`
instructions
instructions
`}`
L_1
`{`
......@@ -338,20 +337,19 @@ block being denoted by a label L1 .. Lj above. The instructions are
semi-colon separated sequence of either regular WhyML expressions of
type `unit`, or CFG-specific instructions below:
. a `goto` statement: `goto L` where L is one of the label of the
- a `goto` statement: `goto L` where L is one of the label of the
other blocks. It naturally instructs to continue execution at the
given block.
. a code invariant: `invariant I { t }` where `I` is a name and `t`
- a code invariant: `invariant I { t }` where `I` is a name and `t`
a predicate. It is similar as an assert expression, telling that `t`
must hold when execution reaches this statement. Additionally, it
acts as a cut in the generation of VC, similarly as a loop
invariant. See example below.
. a switch statement, of the form
- a switch statement, of the form
..
`switch` (e)
| pat_1 -> instructions_1
...
......@@ -369,7 +367,7 @@ The extension of syntax is formally described by the following rules.
module: "module" `ident` `decl`* "end"
decl: "let" "cfg" `cfg_fundef` ("with" `cfg_fundef`)*
cfg_fundef: `ident` `binders` : `type` `spec` "=" `vardecl`* "{" `block` "}" `labelblock`*
vardecl: "var" `binder` ";"
vardecl: "var" `ident`* ":" `type` ";" | "ghost" "var" `ident`* ":" `type` ";"
block: `instruction` (";" `instruction`)*
labelblock: `ident` "{" `block` "}"
instruction:
......@@ -383,14 +381,78 @@ The extension of syntax is formally described by the following rules.
An example
~~~~~~~~~~
The following example comes from the documentation of the ANSI C Specification Language
\cite{baudinXXacsl, section 2.4.2 Loop invariants).
::
/*@ requires n >= 0 && \valid(a,0,n);
@ ensures \forall integer j ; 0 <= j < n ==> \result >= a[j])
@*/
int max_array(int a[], int n) {
int m, i = 0;
goto L;
do {
if (a[i] > m) { L: m = a[i]; }
/*@ invariant
@ 0 <= i < n && \forall integer j ; 0 <= j <= i ==> m >= a[j]);
@*/
i++;
}
while (i < n);
return m;
}
The code can be viewed as a control-flow graph as follows.
.. figure:: images/cfg.mps
Here is a version in the Why3-CFG language, where label L corresponds
to node X, label L1 to node 'inv', label L2 to node YY.
::
let cfg max_array (a:array int) : (max: int, ghost ind:int)
requires { a.length > 0 }
ensures { forall j. 0 <= j < a.length -> a[ind] >= a[j] }
=
var i m:int;
ghost var ind:int;
{
i <- 0;
goto L
}
L {
m <- a[i];
ind <- i;
goto L1
}
L1 {
invariant I { 0 <= i < a.length /\
0 <= ind < a.length /\
m = a[ind] /\
forall j. 0 <= j <= i -> a[ind] >= a[j] };
i <- i+1;
switch (i < a.length)
| True -> goto L2
| False -> (m,ind)
end
}
L2 {
switch (a[i] > m)
| True -> goto L
| False -> goto L1
end
}
Limitations
~~~~~~~~~~~
Termination is never checked
- Termination is never checked
local variables cannot be declared ghost
- New keywords "cfg", "goto", "switch" and "var" cannot be used as regular identifiers anymore
New keywords `cfg`, `goto`, `switch` and `var` cannot be used as regular identifiers anymore
- consecutive invariants are not seen as a conjunction of invariants
......@@ -1492,6 +1492,12 @@ WhyML Attributes
.. why3:attribute:: vc:sp
.. why3:attribute:: vc:wp
.. why3:attribute:: vc:white_box
.. why3:attribute:: vc:keep_precondition
.. _sec.meta:
Why3 Metas
......
......@@ -11,34 +11,10 @@
open Why3
type pty = Ptree.pty
type ident = Ptree.ident
type binder = Ptree.binder
type pattern = Ptree.pattern
type spec = Ptree.spec
type label = Ptree.ident
(*
type cfg_expr = {
cfg_expr_desc : cfg_expr_desc;
cfg_expr_loc : Loc.position;
}
and cfg_expr_desc =
| CFGtrue
(** Boolean literal [True] *)
| CFGfalse
(** Boolean literal [False] *)
| CFGconst of Constant.constant
(** Constant literals *)
(* TODO: expand -> variables, bin op, function call... or any Ptree.expr ! *)
*)
type cfg_instr = {
cfg_instr_desc : cfg_instr_desc;
cfg_instr_loc : Loc.position;
......@@ -52,7 +28,7 @@ and cfg_instr_desc =
| CFGinvariant of ident * Ptree.term
(** named invariant *)
| CFGexpr of Ptree.expr
(** any other regular WhyML expressions *)
(** any other regular WhyML expressions *)
and switch_branch = Ptree.pattern * block
(** pattern -> regular WhyML expression ; goto ident *)
......@@ -61,9 +37,10 @@ and block = cfg_instr list
type cfg_fundef =
ident * binder list * pty * pattern * spec * binder list * block * (label * block) list
ident * Ptree.binder list * Ptree.pty * Ptree.pattern * Ity.mask * Ptree.spec *
(bool * ident * Ptree.pty) list * block * (label * block) list
(** function name, argument, return type, ?, contract,
local variables, first block, other blocks *)
(ghost) local variables, first block, other blocks *)
type cfg_decl =
| Dmlw_decl of Ptree.decl
......
......@@ -108,6 +108,7 @@ let translate_cfg preconds block blocks =
in
traverse_block bl
| CFGinvariant(id,t) ->
(* TODO: if next instruction is also an invariant, groupe them together *)
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ id.id_str)) in
(* TODO : add also an "expl:" *)
let t = { t with term_desc = Tattr(attr,t) } in
......@@ -145,18 +146,16 @@ let translate_cfg preconds block blocks =
let e_ref = mk_expr ~loc:Loc.dummy_position Eref
let declare_local (loc,idopt,ghost,tyopt) body =
match idopt, tyopt with
| Some id, Some ty ->
Debug.dprintf debug "declaring local variable %a of type %a@." pp_id id pp_pty ty ;
let e = Eany([],Expr.RKnone,tyopt,pat_wild ~loc,Ity.MaskVisible,empty_spec) in
let e = mk_expr ~loc (Eapply(e_ref,mk_expr ~loc e)) in
let id = { id with id_ats = (ATstr Pmodule.ref_attr) :: id.id_ats } in
mk_expr ~loc:id.id_loc (Elet(id,ghost,Expr.RKnone,e,body))
| _ -> failwith "invalid variable declaration"
let declare_local (ghost,id,ty) body =
let loc = id.id_loc in
Debug.dprintf debug "declaring local variable %a of type %a@." pp_id id pp_pty ty ;
let e = Eany([],Expr.RKnone,Some ty,pat_wild ~loc,Ity.MaskVisible,empty_spec) in
let e = mk_expr ~loc (Eapply(e_ref,mk_expr ~loc e)) in
let id = { id with id_ats = (ATstr Pmodule.ref_attr) :: id.id_ats } in
mk_expr ~loc:id.id_loc (Elet(id,ghost,Expr.RKnone,e,body))
let build_path_function retty postconds (startlabel, preconds, body) : Ptree.fundef =
let build_path_function retty pat mask postconds (startlabel, preconds, body) : Ptree.fundef =
let body =
List.fold_left
(fun acc t ->
......@@ -169,10 +168,10 @@ let build_path_function retty postconds (startlabel, preconds, body) : Ptree.fun
let spec = { empty_spec with sp_post = postconds} in
let id = mk_id ~loc ("_from_" ^ startlabel) in
let arg = (loc,None,false,Some unit_type) in
(id,false,Expr.RKnone, [arg], Some retty, pat_wild ~loc, Ity.MaskVisible, spec, body)
(id,false,Expr.RKnone, [arg], Some retty, pat, mask, spec, body)
let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
let translate_letcfg (id,args,retty,pat,mask,spec,locals,block,blocks) =
Debug.dprintf debug "translating cfg function `%s`@." id.id_str;
Debug.dprintf debug "return type is `%a`@." pp_pty retty;
let funs = translate_cfg spec.sp_pre block blocks in
......@@ -181,7 +180,7 @@ let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
mk_expr ~loc (Eidapp(Qident (mk_id ~loc "_from_start"),[mk_unit ~loc]))
in
let defs =
List.map (build_path_function retty spec.sp_post) funs
List.map (build_path_function retty pat mask spec.sp_post) funs
in
let body =
mk_expr ~loc (Erec(defs,body))
......@@ -194,7 +193,7 @@ let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
mk_expr ~loc (Eattr(divergent_attr,body))
in
let f =
Efun(args, Some retty, pat, Ity.MaskVisible, spec, body)
Efun(args, Some retty, pat, mask, spec, body)
in
Dlet (id,false,Expr.RKnone,mk_expr ~loc:id.id_loc f)
......
......@@ -25,7 +25,6 @@
%start cfgfile
%type <Cfg_ast.cfg_file> cfgfile
%type <Cfg_ast.binder list> vardecl
%type <Cfg_ast.cfg_instr list> sequence
%type <(Ptree.pattern * Cfg_ast.cfg_instr list) list> cases
......@@ -47,9 +46,9 @@ cfgdecl:
recdefn:
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL
v=vardecls b=block bl=labelblock*
{ let pat, ty, _mask = ret in
{ let pat, ty, mask = ret in
let spec = apply_return pat sp in
(id, args, ty, pat, spec, v, b, bl) }
(id, args, ty, pat, mask, spec, v, b, bl) }
;
vardecls:
......@@ -58,9 +57,14 @@ vardecls:
;
vardecl:
| VAR b=binder SEMICOLON { b }
| g=ghost VAR vl=attrs(lident_nq)* COLON t=ty SEMICOLON
{ List.map (fun id -> (g,id,t)) vl }
;
ghost:
| /* epsilon */ { false }
| GHOST { true }
labelblock:
| id = attrs(uident) b=block { (id,b) }
;
......
......@@ -17,7 +17,7 @@ let cfg cfggoto (x:int) : int
requires { x >= 0 }
ensures { result = x + 2 }
=
var (y : int);
var y : int;
{
y <- x+1;
goto L
......@@ -31,7 +31,7 @@ let cfg cfg_inv (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
var y:int;
{
y <- x;
invariant I { y >= 0} ;
......@@ -46,7 +46,7 @@ let cfg cfg_infinite_loop (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
var y:int;
{
y <- 0;
goto L;
......@@ -63,7 +63,7 @@ let cfg cfg_finite_loop (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
var y:int;
{
y <- 0;
goto L;
......
......@@ -5,7 +5,7 @@ module MaxArray
use array.Array
let cfg compute_max (a:array int) : (max: int, ind:int)
let cfg compute_max (a:array int) : (max: int, ghost ind:int)
requires { a.length > 0 }
ensures { forall i. 0 <= i < a.length -> a[ind] >= a[i] }
=
......@@ -25,8 +25,8 @@ module MaxArray
*)
var (i m:int);
var (ind:int); (* should be ghost *)
var i m:int;
ghost var ind:int;
{
i <- 0;
goto L
......
......@@ -610,7 +610,7 @@ ind_case:
(* Type expressions *)
ty:
%public ty:
| ty_arg { $1 }
| lqualid ty_arg+ { PTtyapp ($1, $2) }
| ty ARROW ty { PTarrow ($1, $3) }
......@@ -1512,7 +1512,7 @@ squalid:
want it in lident_nq, not even with an error message.
This avoids a conflict in "let ref x = ...". *)
lident_nq:
%public lident_nq:
| LIDENT { mk_id $1 $startpos $endpos }
| lident_keyword { mk_id $1 $startpos $endpos }
| CORE_LIDENT { let loc = floc $startpos($1) $endpos($1) in
......
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