Commit 5a3ff59f authored by MARCHE Claude's avatar MARCHE Claude

in progress

parent e0218337
......@@ -501,6 +501,7 @@ PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/python/py_parser.ml plugins/python/py_parser.mli \
plugins/microc/mc_lexer.ml \
plugins/microc/mc_parser.ml plugins/microc/mc_parser.mli \
plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli \
plugins/parser/dimacs.ml
PLUG_PARSER = genequlin dimacs
......@@ -509,7 +510,7 @@ PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUG_MICROC = mc_ast mc_parser mc_lexer mc_printer mc_main
PLUG_CFG = cfg_ast cfg_parser cfg_lexer cfg_main
PLUG_CFG = cfg_ast cfg_parser cfg_main
PLUGINS = genequlin dimacs tptp python microc cfg
......@@ -543,7 +544,7 @@ PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES) \
$(addprefix plugins/cfg/, $(CFGMODULES)) \
$(CFGMODULES)
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
......@@ -2136,6 +2137,12 @@ clean::
$(SHOW) 'Menhir $<'
$(HIDE)$(MENHIR) --table --explain --strict $<
plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli: plugins/cfg/cfg_parser.mly
$(SHOW) 'Menhir $<'
$(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser \
--external-tokens Why3.Parser \
src/parser/parser.mly $<
%.dep: %.ml %.mli
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $<i $(TOTARGET)
......
......@@ -11,68 +11,38 @@
open Why3
type ident = Ptree.ident
type unop =
| Uneg (* -e *)
| Unot (* !e *)
type pty = Ptree.pty
type binop =
| Badd | Bsub | Bmul | Bdiv | Bmod (* + - * / % *)
| Beq | Bneq | Blt | Ble | Bgt | Bge (* == != < <= > >= *)
| Band | Bor (* && || *)
type ident = Ptree.ident
type ty =
| Tvoid
| Tint
| Tarray
type binder = Ptree.binder
type loop_annotation =
Ptree.invariant * Ptree.variant
type pattern = Ptree.pattern
type expr = {
expr_desc: expr_desc;
expr_loc : Loc.position;
}
type spec = Ptree.spec
and expr_desc =
| Eunit
| Eint of string
| Estring of string
| Eaddr of ident
| Eident of ident
| Ebinop of binop * expr * expr
| Eunop of unop * expr
| Ecall of ident * expr list
| Eget of expr * expr (* e1[e2] *)
type cfg_expr = {
cfg_expr_desc : cfg_expr_desc;
cfg_expr_loc : Loc.position;
}
and stmt = {
stmt_desc: stmt_desc;
stmt_loc : Loc.position;
}
and cfg_expr_desc =
| CFGtrue
(** Boolean literal [True] *)
| CFGfalse
(** Boolean literal [False] *)
| CFGconst of Constant.constant
(** Constant literals *)
(* TODO: expand *)
and stmt_desc =
| Sskip
| Sif of expr * stmt * stmt
| Sreturn of expr
| Svar of ty * ident * expr
| Sassign of ident * expr
| Swhile of expr * loop_annotation * stmt
(* | Sfor of stmt * expr * stmt * loop_annotation * block *)
| Seval of expr
| Sset of expr * expr * expr (* e1[e2] = e3 *)
| Sassert of Expr.assertion_kind * Ptree.term
| Sbreak
| Slabel of ident
| Sblock of stmt list
type param =
ty * ident
type cfg_fundef =
ident * binder list * pty * pattern * spec * binder list * cfg_expr
(** function name, argument, return type, ?, contract, local variables, body *)
type decl =
| Dinclude of ident
| Dfun of ty * ident * param list * Ptree.spec * stmt
| Dlogic of ty option * ident * param list * Ptree.term option
| Dprop of Decl.prop_kind * ident * Ptree.term
type cfg_decl =
| Dmlw_decl of Ptree.decl
| Dletcfg of cfg_fundef list
type file = decl list
type cfg_file = (ident * cfg_decl list) list
(** a list of modules containing lists of declarations *)
......@@ -11,24 +11,44 @@
%{
open Cfg_ast
let mk_cfgexpr d s e = { cfgexpr_desc = d; cfgexpr_loc = floc s e }
%}
(* extra token *)
%token CFG
%start cfgfile
%type <Cfg_ast.cfg> cfgfile
%%
cfgfile:
| dl=decl* EOF { dl }
| ml=cfgmodule* EOF { ml }
;
decl:
| LET attrs(lident_rich) binders EQUAL seq { $1 }
cfgmodule:
| MODULE id=attrs(uident_nq) dl=cfgdecl* END
{ (id,dl) }
cfgdecl:
| module_decl_parsing_only { Dmlw_decl $1 }
| LET CFG with_list1(recdefn) { Dletcfg $2 }
;
seq:
recdefn:
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL b=body
{ let pat, ty, _mask = ret in
let spec = apply_return pat sp in
(id, args, ret, ty, pat, spec, b) }
;
body:
| cfgexpr { $1 }
;
cfgexpr:
| TRUE { mk_cfgexpr CFGtrue $startpos $endpos }
;
......@@ -362,7 +362,7 @@ module_decl:
}
| use_clone { () }
module_decl_parsing_only:
%public module_decl_parsing_only:
| scope_head_parsing_only module_decl_parsing_only* END
{ let loc,import,qid = $1 in (Dscope(loc,import,qid,$2))}
| IMPORT uqualid { (Dimport $2) }
......@@ -653,7 +653,7 @@ params: param* { List.concat $1 }
params1: param+ { List.concat $1 }
binders: binder+ { List.concat $1 }
%public binders: binder+ { List.concat $1 }
param:
| special_binder
......@@ -1296,7 +1296,7 @@ for_dir:
(* Specification *)
spec:
%public spec:
| (* epsilon *) %prec prec_no_spec { empty_spec }
| single_spec spec { spec_union $1 $2 }
......@@ -1354,7 +1354,7 @@ return_opt:
| (* epsilon *) { mk_pat Pwild $startpos $endpos, None, Ity.MaskVisible }
| COLON return_named { let pat, ty, mask = $2 in pat, Some ty, mask }
return_named:
%public return_named:
| LEFTPAR ret_cast RIGHTPAR
{ $2 }
| LEFTPAR comma_list2(ret_cast) RIGHTPAR
......@@ -1496,12 +1496,12 @@ ident:
| lident { $1 }
| lident_op { $1 }
ident_nq:
%public ident_nq:
| uident_nq { $1 }
| lident_nq { $1 }
| lident_op_nq { $1 }
lident_rich:
%public lident_rich:
| lident_nq { $1 }
| lident_op_nq { $1 }
......@@ -1509,7 +1509,7 @@ uident:
| UIDENT { mk_id $1 $startpos $endpos }
| CORE_UIDENT { mk_id $1 $startpos $endpos }
uident_nq:
%public uident_nq:
| UIDENT { mk_id $1 $startpos $endpos }
| CORE_UIDENT { let loc = floc $startpos($1) $endpos($1) in
Loc.errorm ~loc core_ident_error $1 }
......@@ -1609,7 +1609,7 @@ prefix_op:
(* Attributes and position markers *)
attrs(X): X attr* { add_attr $1 $2 }
%public attrs(X): X attr* { add_attr $1 $2 }
attr:
| ATTRIBUTE { ATstr (Ident.create_attribute $1) }
......@@ -1620,7 +1620,7 @@ attr:
bar_list1(X):
| ioption(BAR) ; xl = separated_nonempty_list(BAR, X) { xl }
with_list1(X):
%public with_list1(X):
| separated_nonempty_list(WITH, X) { $1 }
comma_list2(X):
......
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