From 545a514ba51436076c736d21c9d5b4710238db55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Thu, 17 Jun 2010 16:26:52 +0200 Subject: [PATCH] Added heptcheck in heptagon/main When given a .ept file, it just check its validity. When given a .epi file, it checks it and creates the .epci compiled file. --- heptagon/analysis/interface.ml | 34 +++---- heptagon/heptagon.ml | 11 ++- heptagon/main/compiler_utils.ml | 55 +++++++++++ heptagon/main/hept_compiler.ml | 50 ++++++++++ heptagon/main/heptcheck.ml | 141 ++++++++++++++++++++++++++++ heptagon/parsing/lexer.mll | 2 - heptagon/parsing/parser.mly | 54 +++++------ heptagon/parsing/parsetree.ml | 5 + heptagon/parsing/scoping.ml | 11 ++- heptagon/transformations/present.ml | 11 +-- 10 files changed, 313 insertions(+), 61 deletions(-) create mode 100644 heptagon/main/compiler_utils.ml create mode 100644 heptagon/main/hept_compiler.ml create mode 100644 heptagon/main/heptcheck.ml diff --git a/heptagon/analysis/interface.ml b/heptagon/analysis/interface.ml index 1da5c45..184a658 100644 --- a/heptagon/analysis/interface.ml +++ b/heptagon/analysis/interface.ml @@ -14,6 +14,8 @@ open Heptagon open Signature open Modules open Typing +open Pp_tools +open Types module Type = struct @@ -49,16 +51,16 @@ struct | Tabstract -> fprintf ff "@[type %s@.@]" name | Tenum(tag_name_list) -> fprintf ff "@[type %s = " name; - print_list ff print_name " |" tag_name_list; + print_list_r print_name "" " |" "" ff tag_name_list; fprintf ff "@.@]" | Tstruct(f_ty_list) -> fprintf ff "@[type %s = " name; - fprintf ff "@[{"; - print_list ff - (fun ff (field, ty) -> print_name ff field; + fprintf ff "@["; + print_list_r + (fun ff { f_name = field; f_type = ty } -> print_name ff field; fprintf ff ": "; - print_type ff ty) ";" f_ty_list; - fprintf ff "}@]@.@]" + print_type ff ty) "{" ";" "}" ff f_ty_list; + fprintf ff "@]@.@]" let signature ff name { node_inputs = inputs; node_outputs = outputs; @@ -73,24 +75,22 @@ struct let print_node_params ff = function | [] -> () - | l -> - fprintf ff "<<"; - print_list ff print_name "," l; - fprintf ff ">>" in + | l -> print_list_r print_name "<<" "," ">>" ff l + in fprintf ff "@[val "; print_name ff name; - print_node_params ff params; - fprintf ff "(@["; - print_list ff print ";" inputs; - fprintf ff "@]) returns (@["; - print_list ff print ";" outputs; - fprintf ff "@])"; + print_node_params ff (List.map (fun p -> p.p_name) params); + fprintf ff "@["; + print_list_r print "(" ";" ")" ff inputs; + fprintf ff "@] returns @["; + print_list_r print "(" ";" ")" ff outputs; + fprintf ff "@]"; (match constr with | [] -> () | constr -> fprintf ff "\n with: @["; - print_list ff Static.print_size_constr "," constr; + print_list_r Static.print_size_constr "" "," "" ff constr; fprintf ff "@]" ); fprintf ff "@.@]" diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml index 1b7939f..0bc0b28 100644 --- a/heptagon/heptagon.ml +++ b/heptagon/heptagon.ml @@ -169,10 +169,10 @@ let mk_var_dec ?(last = Var) name ty = { v_name = name; v_type = ty; v_last = last; v_loc = Location.get_current_location () } -let mk_block defnames eqs = +let mk_block ?(statefull = true) defnames eqs = { b_local = []; b_equs = eqs; b_defnames = defnames; - b_statefull = true; b_loc = no_location } - + b_statefull = statefull; b_loc = no_location } + let dfalse = mk_exp (Econst (Cconstr Initial.pfalse)) (Tid Initial.pbool) let dtrue = mk_exp (Econst (Cconstr Initial.ptrue)) (Tid Initial.pbool) @@ -182,6 +182,11 @@ let mk_ifthenelse e1 e2 e3 = let mk_simple_equation pat e = mk_equation ~statefull:false (Eeq(pat, e)) +let mk_switch_equation ?(statefull = true) e l = + mk_equation ~statefull:statefull (Eswitch (e, l)) + + + (* let cfalse = Cconstr Initial.pfalse diff --git a/heptagon/main/compiler_utils.ml b/heptagon/main/compiler_utils.ml new file mode 100644 index 0000000..8772336 --- /dev/null +++ b/heptagon/main/compiler_utils.ml @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +open Misc +open Location + +let lexical_error err loc = + Printf.eprintf "%aIllegal character.\n" output_location loc; + raise Error + +let syntax_error loc = + Printf.eprintf "%aSyntax error.\n" output_location loc; + raise Error + +let language_error lang = + Printf.eprintf "Unknown language: %s.\n" lang + +let parse parsing_fun lexing_fun lexbuf = + try + parsing_fun lexing_fun lexbuf + with + | Lexer.Lexical_error(err, pos1, pos2) -> + lexical_error err (Loc(pos1, pos2)) + | Parsing.Parse_error -> + let pos1 = Lexing.lexeme_start lexbuf + and pos2 = Lexing.lexeme_end lexbuf in + let l = Loc(pos1,pos2) in + syntax_error l + +let comment s = Printf.printf "** %s done **\n" s; flush stdout + +let do_pass f d p pp enabled = + if enabled + then + let r = f p in + if !verbose + then begin + comment d; + pp r; + end; + r + else p + +let do_silent_pass f d p enabled = + if enabled + then begin + let r = f p in + if !verbose then comment d; r + end + else p diff --git a/heptagon/main/hept_compiler.ml b/heptagon/main/hept_compiler.ml new file mode 100644 index 0000000..f7f1de5 --- /dev/null +++ b/heptagon/main/hept_compiler.ml @@ -0,0 +1,50 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +open Misc +open Compiler_utils + +let compile_impl pp p = + (* Typing *) + let p = do_pass Typing.program "Typing" p pp true in + + if !print_types then Interface.Printer.print stdout; + + (* Causality check *) + let p = do_silent_pass Causality.program "Causality check" p true in + + (* Initialization check *) + let p = + do_silent_pass Initialization.program "Initialization check" p !init in + + (* Completion of partial definitions *) + let p = do_pass Completion.program "Completion" p pp true in + + (* Automata *) + let p = do_pass Automata.program "Automata" p pp true in + + (* Present *) + let p = do_pass Present.program "Present" p pp true in + + (* Shared variables (last) *) + let p = do_pass Last.program "Last" p pp true in + + (* Reset *) + let p = do_pass Reset.program "Reset" p pp true in + + (* Every *) + let p = do_pass Every.program "Every" p pp true in + + (* Return the transformed AST *) + p + + +let compile_interface l = + Interface.Type.main l; + if !print_types then Interface.Printer.print stdout; + l diff --git a/heptagon/main/heptcheck.ml b/heptagon/main/heptcheck.ml new file mode 100644 index 0000000..4a4b1d6 --- /dev/null +++ b/heptagon/main/heptcheck.ml @@ -0,0 +1,141 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +(* Checks the validity of a Heptagon file (interface or implementation).*) + +open Misc +open Compiler_utils +open Location + +let init_compiler modname source_name ic = + Location.initialize source_name ic; + Modules.initialize modname; + Initial.initialize () + +let pp = Printer.print stdout + +let parse_implementation lexbuf = + parse Parser.program Lexer.token lexbuf + +let parse_interface lexbuf = + parse Parser.interface Lexer.token lexbuf + +let compile_impl modname filename = + (* input and output files *) + let source_name = filename ^ ".ept" in + + let ic = open_in source_name in + let close_all_files () = + close_in ic + in + + try + init_compiler modname source_name ic; + + (* Parsing of the file *) + let lexbuf = Lexing.from_channel ic in + let p = parse_implementation lexbuf in + + (* Convert the parse tree to Heptagon AST *) + let p = Scoping.translate_program p in + if !verbose + then begin + comment "Parsing"; + pp p + end; + + (* Call the compiler*) + Hept_compiler.compile_impl pp p; + + if !verbose + then begin + comment "Check successfull" + end; + close_all_files () + + with x -> close_all_files (); raise x + +let compile_interface modname filename = + (* input and output files *) + let source_name = filename ^ ".epi" in + let obj_interf_name = filename ^ ".epci" in + + let ic = open_in source_name in + let itc = open_out_bin obj_interf_name in + let close_all_files () = + close_in ic; + close_out itc in + + try + init_compiler modname source_name ic; + + (* Parsing of the file *) + let lexbuf = Lexing.from_channel ic in + let l = parse_interface lexbuf in + + (* Convert the parse tree to Heptagon AST *) + let l = Scoping.translate_interface l in + + (* Call the compiler*) + Hept_compiler.compile_interface l; + + Modules.write itc; + + close_all_files () + with + | x -> close_all_files (); raise x + +let compile file = + if Filename.check_suffix file ".ept" + then + let filename = Filename.chop_suffix file ".ept" in + let modname = String.capitalize(Filename.basename filename) in + compile_impl modname filename + else if Filename.check_suffix file ".epi" + then + let filename = Filename.chop_suffix file ".epi" in + let modname = String.capitalize(Filename.basename filename) in + compile_interface modname filename + else + raise (Arg.Bad ("Unknow file type: " ^ file)) + +let doc_verbose = "\t\t\tSet verbose mode" +and doc_version = "\t\tThe version of the compiler" +and doc_print_types = "\t\t\tPrint types" +and doc_include = "\t\tAdd to the list of include directories" +and doc_stdlib = "\t\tDirectory for the standard library" +and doc_locate_stdlib = "\t\tLocate standard libray" +and doc_no_pervasives = "\tDo not load the pervasives module" +and doc_full_type_info = "\t\t\tPrint full type information" +and doc_noinit = "\t\tDisable initialization analysis" + +let errmsg = "Options are:" + +let main () = + try + Arg.parse + [ + "-v",Arg.Set verbose, doc_verbose; + "-version", Arg.Unit show_version, doc_version; + "-i", Arg.Set print_types, doc_print_types; + "-I", Arg.String add_include, doc_include; + "-where", Arg.Unit locate_stdlib, doc_locate_stdlib; + "-stdlib", Arg.String set_stdlib, doc_stdlib; + "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives; + "-noinit", Arg.Clear init, doc_noinit; + "-fti", Arg.Set full_type_info, doc_full_type_info; + ] + compile + errmsg; + with + | Misc.Error -> exit 2;; + +main () + + diff --git a/heptagon/parsing/lexer.mll b/heptagon/parsing/lexer.mll index 3e0251f..d367e8a 100644 --- a/heptagon/parsing/lexer.mll +++ b/heptagon/parsing/lexer.mll @@ -21,12 +21,10 @@ let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);; List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "node", NODE; "fun", FUN; - "safe", SAFE; "returns", RETURNS; "var", VAR; "val", VAL; "const", CONST; - "unsafe", UNSAFE; "let", LET; "tel", TEL; "end", END; diff --git a/heptagon/parsing/parser.mly b/heptagon/parsing/parser.mly index 4af55a9..265a54f 100644 --- a/heptagon/parsing/parser.mly +++ b/heptagon/parsing/parser.mly @@ -1,10 +1,9 @@ %{ open Misc -open Global +open Signature open Location open Names -open Linearity open Parsetree %} @@ -118,7 +117,7 @@ const_decs: const_dec: | CONST IDENT COLON ty_ident EQUAL exp - { cmake $2 $4 $6 } + { mk_const_dec $2 $4 $6 } ; type_decs: @@ -127,9 +126,9 @@ type_decs: ; type_dec: - | TYPE IDENT { tmake $2 Type_abs } - | TYPE IDENT EQUAL enum_ty_desc { tmake $2 (Type_enum ($4)) } - | TYPE IDENT EQUAL struct_ty_desc { tmake $2 (Type_struct ($4)) } + | TYPE IDENT { mk_type_dec $2 Type_abs } + | TYPE IDENT EQUAL enum_ty_desc { mk_type_dec $2 (Type_enum ($4)) } + | TYPE IDENT EQUAL struct_ty_desc { mk_type_dec $2 (Type_struct ($4)) } ; enum_ty_desc: @@ -193,7 +192,7 @@ nonmt_params: param: | ident_list COLON ty_ident - { List.map (fun id -> vmake id $3 Var) $1 } + { List.map (fun id -> mk_var_dec id $3 Var) $1 } ; out_params: @@ -252,11 +251,11 @@ loc_params: var_last: | ident_list COLON ty_ident - { List.map (fun id -> vmake id $3 Var) $1 } + { List.map (fun id -> mk_var_dec id $3 Var) $1 } | LAST IDENT COLON ty_ident EQUAL const - { [ vmake $2 $4 (Last(Some($6))) ] } + { [ mk_var_dec $2 $4 (Last(Some($6))) ] } | LAST IDENT COLON ty_ident - { [ vmake $2 $4 (Last(None)) ] } + { [ mk_var_dec $2 $4 (Last(None)) ] } ; ident_list: @@ -292,26 +291,26 @@ opt_bar: ; equ: - | pat EQUAL exp { eqmake (Eeq($1, $3)) } + | pat EQUAL exp { mk_equation (Eeq($1, $3)) } | AUTOMATON automaton_handlers END - { eqmake (Eautomaton(List.rev $2)) } + { mk_equation (Eautomaton(List.rev $2)) } | SWITCH exp opt_bar switch_handlers END - { eqmake (Eswitch($2, List.rev $4)) } + { mk_equation (Eswitch($2, List.rev $4)) } | PRESENT opt_bar present_handlers END - { eqmake (Epresent(List.rev $3, bmake [] [])) } + { mk_equation (Epresent(List.rev $3, mk_block [] [])) } | PRESENT opt_bar present_handlers DEFAULT loc_vars DO equs END - { eqmake (Epresent(List.rev $3, bmake $5 $7)) } + { mk_equation (Epresent(List.rev $3, mk_block $5 $7)) } | IF exp THEN loc_vars DO equs ELSE loc_vars DO equs END - { eqmake (Eswitch($2, - [{ w_name = Name("true"); w_block = bmake $4 $6}; - { w_name = Name("false"); w_block = bmake $8 $10 }])) } + { mk_equation (Eswitch($2, + [{ w_name = Name("true"); w_block = mk_block $4 $6}; + { w_name = Name("false"); w_block = mk_block $8 $10 }])) } | RESET equs EVERY exp - { eqmake (Ereset($2, $4)) } + { mk_equation (Ereset($2, $4)) } ; automaton_handler: | STATE Constructor loc_vars DO equs opt_until_escapes opt_unless_escapes - { { s_state = $2; s_block = bmake $3 $5; + { { s_state = $2; s_block = mk_block $3 $5; s_until = $6; s_unless = $7 } } ; @@ -350,7 +349,7 @@ escapes: switch_handler: | constructor loc_vars DO equs - { { w_name = $1; w_block = bmake $2 $4 } } + { { w_name = $1; w_block = mk_block $2 $4 } } ; switch_handlers: @@ -362,7 +361,7 @@ switch_handlers: present_handler: | exp loc_vars DO equs - { { p_cond = $1; p_block = bmake $2 $4 } } + { { p_cond = $1; p_block = mk_block $2 $4 } } ; present_handlers: @@ -444,7 +443,7 @@ exp: | SUBTRACTIVE exp %prec prec_uminus { mk_exp (mk_op_call ("~"^$1) [] [$2]) } | IF exp THEN exp ELSE exp - { mk_exp (Eapp(mk_app Eifthenelse [$2; $4; $6])) } + { mk_exp (Eapp(mk_app Eifthenelse, [$2; $4; $6])) } | simple_exp ARROW exp { mk_exp (Eapp(mk_app Earrow, [$1; $3])) } | LAST IDENT @@ -457,7 +456,7 @@ exp: | exp indexes { mk_exp (mk_array_op_call (Eselect $2) [$1]) } | exp DOT indexes DEFAULT exp - { mk_exp (mk_array_op_call Eselect_dyn [$1; $5]@$3) } + { mk_exp (mk_array_op_call Eselect_dyn ([$1; $5]@$3)) } | exp WITH indexes EQUAL exp { mk_exp (mk_array_op_call (Eupdate $3) [$1; $5]) } | exp LBRACKET exp DOUBLE_DOT exp RBRACKET @@ -562,7 +561,8 @@ interface_decl: | OPEN Constructor { mk_interface_decl (Iopen $2) } | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN - { mk_interface_decl (Isignature({ sig_name = $4; sig_inputs = $6; + { mk_interface_decl (Isignature({ sig_name = $3; + sig_inputs = $6; sig_outputs = $10; sig_params = $4; })) } ; @@ -578,8 +578,8 @@ nonmt_params_signature: ; param_signature: - | IDENT COLON ty_ident { Signature.mk_arg (Some $1) $3) } - | ty_ident { Signature.mk_arg None $1 } + | IDENT COLON ty_ident { mk_arg (Some $1) $3 } + | ty_ident { mk_arg None $1 } ; %% diff --git a/heptagon/parsing/parsetree.ml b/heptagon/parsing/parsetree.ml index 4512065..32882f5 100644 --- a/heptagon/parsing/parsetree.ml +++ b/heptagon/parsing/parsetree.ml @@ -150,6 +150,8 @@ type program = p_nodes : node_dec list; p_consts : const_dec list; } +type arg = { a_type : ty; a_name : name option } + type signature = { sig_name : name; sig_inputs : arg list; @@ -210,3 +212,6 @@ let mk_const_dec id ty e = { c_name = id; c_type = ty; c_value = e; c_loc = Location.get_current_location (); } +let mk_arg name ty = + { a_type = ty; a_name = name } + diff --git a/heptagon/parsing/scoping.ml b/heptagon/parsing/scoping.ml index 37c3379..35207fe 100644 --- a/heptagon/parsing/scoping.ml +++ b/heptagon/parsing/scoping.ml @@ -293,7 +293,7 @@ let translate_typedec const_env ty = | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list) | Type_struct(field_ty_list) -> let translate_field_type (f,ty) = - f, translate_type const_env ty + Signature.mk_field f (translate_type const_env ty) in Heptagon.Type_struct (List.map translate_field_type field_ty_list) in @@ -315,10 +315,15 @@ let translate_program p = Heptagon.p_nodes = List.map (translate_node const_env Rename.empty) p.p_nodes; Heptagon.p_consts = List.map (translate_const_dec const_env) p.p_consts; } +let translate_arg const_env a = + { Signature.a_name = a.a_name; + Signature.a_type = translate_type const_env a.a_type } + let translate_signature s = + let const_env = build_id_list no_location NamesEnv.empty s.sig_params in { Heptagon.sig_name = s.sig_name; - Heptagon.sig_inputs = s.sig_inputs; - Heptagon.sig_outputs = s.sig_outputs; + Heptagon.sig_inputs = List.map (translate_arg const_env) s.sig_inputs; + Heptagon.sig_outputs = List.map (translate_arg const_env) s.sig_outputs; Heptagon.sig_params = List.map Signature.mk_param s.sig_params; } let translate_interface_desc const_env = function diff --git a/heptagon/transformations/present.ml b/heptagon/transformations/present.ml index 0a86fa6..ddc40e1 100644 --- a/heptagon/transformations/present.ml +++ b/heptagon/transformations/present.ml @@ -13,15 +13,8 @@ open Misc open Location open Heptagon -open Global open Initial -let block defnames statefull eqs = - { b_local = []; b_equs = eqs; b_defnames = defnames; - b_statefull = statefull; b_loc = no_location } -let switch statefull e l = - { eq_desc = Eswitch(e, l); eq_statefull = statefull; eq_loc = no_location } - let rec translate_eq v eq = match eq.eq_desc with | Eswitch(e, switch_handlers) -> @@ -54,8 +47,8 @@ and translate_switch_handlers handlers = and translate_present_handlers handlers cont = let translate_present_handler { p_cond = e; p_block = b } cont = let statefull = b.b_statefull or cont.b_statefull in - block b.b_defnames statefull - [switch statefull e [{ w_name = ptrue; w_block = b }; + mk_block ~statefull:statefull b.b_defnames + [mk_switch_equation ~statefull:statefull e [{ w_name = ptrue; w_block = b }; { w_name = pfalse; w_block = cont }]] in let b = List.fold_right translate_present_handler handlers cont in List.hd (b.b_equs)