Commit d18e38a3 authored by MARCHE Claude's avatar MARCHE Claude

more general ASTs for instructions

parent 29a9d10f
......@@ -21,6 +21,7 @@ type pattern = Ptree.pattern
type spec = Ptree.spec
(*
type cfg_expr = {
cfg_expr_desc : cfg_expr_desc;
cfg_expr_loc : Loc.position;
......@@ -33,17 +34,35 @@ and cfg_expr_desc =
(** Boolean literal [False] *)
| CFGconst of Constant.constant
(** Constant literals *)
| CFGlabel of ident * cfg_expr
(** declare a label *)
(* 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;
}
and cfg_instr_desc =
| CFGgoto of ident
(** goto a label *)
(** goto a label "goto L" *)
| CFGexpr of Ptree.expr
(*
| CFGassign of ident * cfg_expr
(** assignment "x <- e" *)
| CFGassert of Expr.assertion_kind * Ptree.term
(* TODO: expand *)
(** assert or assume or check *)
(* TODO: expand -> branching, procedure call... or any Ptree.expr ! *)
*)
type block = cfg_instr list
type label = Ptree.ident
type cfg_fundef =
ident * binder list * pty * pattern * spec * binder list * cfg_expr
(** function name, argument, return type, ?, contract, local variables, body *)
ident * binder list * pty * pattern * spec * binder list * block * (label * block) list
(** function name, argument, return type, ?, contract,
local variables, first block, other blocks *)
type cfg_decl =
| Dmlw_decl of Ptree.decl
......
......@@ -41,6 +41,7 @@
[
"cfg", CFG;
"goto", GOTO;
"var", VAR;
"abstract", ABSTRACT;
"absurd", ABSURD;
"alias", ALIAS;
......@@ -297,6 +298,6 @@ rule token = parse
try
Cfg_parser.cfgfile token lb
with
Cfg_parser.Error as e -> raise (Loc.Located (Loc.extract (lb.lex_start_p,lb.lex_curr_p),e))
Cfg_parser.Error as e -> raise (Loc.Located (Loc.extract (lb.Lexing.lex_start_p,lb.Lexing.lex_curr_p),e))
}
......@@ -330,20 +330,31 @@ let rec pp_pty fmt t =
| _ ->
Format.fprintf fmt "@[<pp_pty>@]"
let rec translate_cfg e =
(*
let translate_expr e =
let loc = e.cfg_expr_loc in
match e.cfg_expr_desc with
| CFGtrue -> mk_expr loc Etrue
| CFGfalse -> mk_expr loc Efalse
| CFGconst c -> mk_expr loc (Econst c)
*)
let translate_instr e =
let loc = e.cfg_instr_loc in
match e.cfg_instr_desc with
(*
| CFGassert(k,t) -> mk_expr loc (Eassert(k,t))
| CFGlabel(_id,e) -> translate_cfg e
| CFGassign(id,e) -> mk_expr loc (Etuple [])
*)
| CFGgoto _id -> mk_expr loc (Etuple [])
| CFGexpr e -> e
let translate_cfg block blocks = mk_expr Loc.dummy_position (Etuple [])
let translate_cfg (id,args,retty,pat,spec,_locals,body) =
let translate_letcfg (id,args,retty,pat,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 body = translate_cfg body in
let body = translate_cfg block blocks in
let f =
Efun(args, Some retty, pat, Ity.MaskVisible, spec, body)
in
......@@ -352,7 +363,7 @@ let translate_cfg (id,args,retty,pat,spec,_locals,body) =
let translate_decl d acc =
match d with
| Dmlw_decl d -> d :: acc
| Dletcfg l -> List.fold_right (fun d acc -> (translate_cfg d)::acc) l acc
| Dletcfg l -> List.fold_right (fun d acc -> (translate_letcfg d)::acc) l acc
let translate (m,dl) =
(m,List.fold_right translate_decl dl [])
......@@ -367,16 +378,19 @@ let read_channel env _path file c =
in
Debug.dprintf debug "%s parsed successfully.@." file;
let ptree = Modules (List.map translate f) in
try
Typing.type_mlw_file env [] (file ^ ".mlw") ptree
with
Loc.Located(loc,e) ->
let msg = Format.asprintf "%a" Exn_printer.exn_printer e in
Format.eprintf "%a%s@." Loc.report_position loc msg;
Debug.dprintf debug "%a@."
(Mlw_printer.with_marker ~msg loc Mlw_printer.pp_mlw_file)
ptree;
exit 1
let mm = try
Typing.type_mlw_file env [] (file ^ ".mlw") ptree
with
Loc.Located(loc,e) ->
let msg = Format.asprintf "%a" Exn_printer.exn_printer e in
Format.eprintf "%a%s@." Loc.report_position loc msg;
Debug.dprintf debug "%a@."
(Mlw_printer.with_marker ~msg loc Mlw_printer.pp_mlw_file)
ptree;
exit 1
in
Debug.dprintf debug "%a@." Mlw_printer.pp_mlw_file ptree;
mm
let () =
Env.register_format mlw_language "mlcfg" ["mlcfg"] read_channel
......
......@@ -16,15 +16,19 @@
let floc s e = Loc.extract (s,e)
(*
let mk_cfgexpr d s e = { cfg_expr_desc = d; cfg_expr_loc = floc s e }
*)
let mk_cfginstr d s e = { cfg_instr_desc = d; cfg_instr_loc = floc s e }
%}
(* extra tokens *)
%token CFG GOTO
%token CFG GOTO VAR
%start cfgfile
%type <Cfg_ast.cfg_file> cfgfile
%type <Cfg_ast.binder list> vardecl
%%
......@@ -42,26 +46,51 @@ cfgdecl:
;
recdefn:
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL b=body
| 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 spec = apply_return pat sp in
(id, args, ty, pat, spec, [], b) }
(id, args, ty, pat, spec, v, b, bl) }
;
body:
| cfgexpr { $1 }
vardecls:
| /* epsilon */ { [] }
| vardecl vardecls { $1 @ $2 }
;
vardecl:
| VAR b=binder SEMICOLON { b }
;
labelblock:
| id = attrs(uident) b=block { (id,b) }
;
block:
| LEFTBRC semicolon_list1(instr) RIGHTBRC { $2 }
;
instr:
| GOTO uident
{ mk_cfginstr (CFGgoto $2) $startpos $endpos }
| contract_expr
{ mk_cfginstr (CFGexpr $1) $startpos $endpos }
(*
| lident LARROW cfgexpr
{ mk_cfginstr (CFGassign ($1,$3)) $startpos $endpos }
| k=assertion_kind id=option(ident_nq) LEFTBRC t=term RIGHTBRC
{ let (n,k)=k in
mk_cfginstr (CFGassert(k, name_term id n t)) $startpos $endpos }
*)
;
(*
cfgexpr:
| TRUE
{ mk_cfgexpr CFGtrue $startpos $endpos }
| FALSE
{ mk_cfgexpr CFGfalse $startpos $endpos }
| GOTO uident
{ mk_cfgexpr (CFGgoto $2) $startpos $endpos }
| LABEL id = attrs(uident) IN e = cfgexpr
{ mk_cfgexpr (CFGlabel(id,e)) $startpos $endpos }
| k=assertion_kind id=option(ident_nq) LEFTBRC t=term RIGHTBRC
{ let (n,k)=k in
mk_cfgexpr (CFGassert(k, name_term id n t)) $startpos $endpos }
| numeral
{ mk_cfgexpr (CFGconst $1) $startpos $endpos }
;
*)
......@@ -4,6 +4,7 @@
open Why3
type token =
| VAR
| CFG
| GOTO
| WRITES
......
......@@ -8,13 +8,23 @@ val test (x:int) : unit
let cfg cfgassert (x:int) : unit
requires { x >= 0 }
=
assert { 3 }
{
assert { 3 = 4 }
}
let cfg cfggoto (x:int) : unit
let cfg cfggoto (x:int) : int
requires { x >= 0 }
ensures { result = x + 2 }
=
label L in
var (y : int);
{
y <- x+1;
goto L
}
L {
y <- y+1;
y
}
let main () = cfgassert 42; cfggoto 43
......
......@@ -666,7 +666,7 @@ param:
{ let r = fst $3 in let ty = if r then PTref [$4] else $4 in
List.map (fun (l,i) -> l, set_ref_opt l r i, true, ty) (snd $3) }
binder:
%public binder:
| special_binder
{ let l,i = $1 in [l, i, false, None] }
| lident_nq attr+
......@@ -888,7 +888,7 @@ minus_numeral:
| MINUS INTEGER { Constant.(ConstInt (Number.neg_int $2)) }
| MINUS REAL { Constant.(ConstReal (Number.neg_real $2))}
numeral:
%public numeral:
| INTEGER { Constant.ConstInt $1 }
| REAL { Constant.ConstReal $1 }
......@@ -975,7 +975,7 @@ seq_expr:
| contract_expr SEMICOLON seq_expr
{ mk_expr (Esequence ($1, $3)) $startpos $endpos }
contract_expr:
%public contract_expr:
| assign_expr %prec prec_no_spec { $1 }
| assign_expr single_spec spec
{ let p = mk_pat Pwild $startpos $endpos in
......@@ -1503,7 +1503,7 @@ squalid:
| CORE_UIDENT { let loc = floc $startpos($1) $endpos($1) in
Loc.errorm ~loc core_ident_error $1 }
lident:
%public lident:
| LIDENT { mk_id $1 $startpos $endpos }
| lident_keyword { mk_id $1 $startpos $endpos }
| CORE_LIDENT { mk_id $1 $startpos $endpos }
......@@ -1621,7 +1621,7 @@ comma_list2(X):
comma_list0(X):
| xl = separated_list(COMMA, X) { xl }
semicolon_list1(X):
%public semicolon_list1(X):
| x = X ; ioption(SEMICOLON) { [x] }
| x = X ; SEMICOLON ; xl = semicolon_list1(X) { x :: xl }
......
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