Revision 7ecfca04 src/main_lustre_compiler.ml
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 22 | 22 |
|
| 23 | 23 |
let extensions = [".ec"; ".lus"; ".lusi"] |
| 24 | 24 |
|
| 25 |
let check_stateless_decls decls = |
|
| 26 |
report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@,@?"); |
|
| 27 |
try |
|
| 28 |
Stateless.check_prog decls |
|
| 29 |
with (Stateless.Error (loc, err)) as exc -> |
|
| 30 |
Format.eprintf "Stateless status error at loc %a: %a@]@." |
|
| 31 |
Location.pp_loc loc |
|
| 32 |
Stateless.pp_error err; |
|
| 33 |
raise exc |
|
| 25 |
(* print a .lusi header file from a source prog *) |
|
| 26 |
let print_lusi prog dirname basename extension = |
|
| 27 |
let header = Lusic.extract_header dirname basename prog in |
|
| 28 |
let header_name = dirname ^ "/" ^ basename ^ extension in |
|
| 29 |
let h_out = open_out header_name in |
|
| 30 |
let h_fmt = formatter_of_out_channel h_out in |
|
| 31 |
begin |
|
| 32 |
Typing.uneval_prog_generics header; |
|
| 33 |
Clock_calculus.uneval_prog_generics header; |
|
| 34 |
Printers.pp_lusi_header h_fmt basename header; |
|
| 35 |
close_out h_out |
|
| 36 |
end |
|
| 37 |
|
|
| 38 |
(* compile a .lusi header file *) |
|
| 39 |
let compile_header dirname basename extension = |
|
| 40 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
| 41 |
let header_name = basename ^ extension in |
|
| 42 |
let lusic_ext = extension ^ "c" in |
|
| 43 |
begin |
|
| 44 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
|
| 45 |
let header = parse_header true (dirname ^ "/" ^ header_name) in |
|
| 46 |
ignore (Modules.load_header ISet.empty header); |
|
| 47 |
ignore (check_top_decls header); |
|
| 48 |
create_dest_dir (); |
|
| 49 |
Log.report ~level:1 |
|
| 50 |
(fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension)); |
|
| 51 |
Lusic.write_lusic true header destname lusic_ext; |
|
| 52 |
Lusic.print_lusic_to_h destname lusic_ext; |
|
| 53 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.") |
|
| 54 |
end |
|
| 55 |
|
|
| 56 |
(* check whether a source file has a compiled header, |
|
| 57 |
if not, generate the compiled header *) |
|
| 58 |
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension = |
|
| 59 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
| 60 |
let lusic_ext = extension ^ "c" in |
|
| 61 |
let header_name = destname ^ lusic_ext in |
|
| 62 |
begin |
|
| 63 |
if not (Sys.file_exists header_name) then |
|
| 64 |
begin |
|
| 65 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
|
| 66 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
|
| 67 |
Lusic.print_lusic_to_h destname lusic_ext |
|
| 68 |
end |
|
| 69 |
else |
|
| 70 |
let lusic = Lusic.read_lusic destname lusic_ext in |
|
| 71 |
if not lusic.Lusic.from_lusi then |
|
| 72 |
begin |
|
| 73 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
|
| 74 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
|
| 75 |
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*) |
|
| 76 |
Lusic.print_lusic_to_h destname lusic_ext |
|
| 77 |
end |
|
| 78 |
else |
|
| 79 |
begin |
|
| 80 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); |
|
| 81 |
Modules.check_dependency lusic destname; |
|
| 82 |
let header = lusic.Lusic.contents in |
|
| 83 |
let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in |
|
| 84 |
check_compatibility |
|
| 85 |
(prog, computed_types_env, computed_clocks_env) |
|
| 86 |
(header, declared_types_env, declared_clocks_env) |
|
| 87 |
end |
|
| 88 |
end |
|
| 89 |
|
|
| 90 |
|
|
| 91 |
let functional_backend () = |
|
| 92 |
match !Options.output with |
|
| 93 |
| "horn" | "lustre" | "acsl" -> true |
|
| 94 |
| _ -> false |
|
| 95 |
|
|
| 96 |
(* From prog to prog *) |
|
| 97 |
let stage1 prog dirname basename = |
|
| 98 |
(* Removing automata *) |
|
| 99 |
let prog = expand_automata prog in |
|
| 100 |
|
|
| 101 |
Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog); |
|
| 102 |
|
|
| 103 |
(* Importing source *) |
|
| 104 |
let _ = Modules.load_program ISet.empty prog in |
|
| 34 | 105 |
|
| 35 |
let type_decls env decls = |
|
| 36 |
report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?"); |
|
| 37 |
let new_env = |
|
| 38 |
begin |
|
| 39 |
try |
|
| 40 |
Typing.type_prog env decls |
|
| 41 |
with (Types.Error (loc,err)) as exc -> |
|
| 42 |
Format.eprintf "Typing error at loc %a: %a@]@." |
|
| 43 |
Location.pp_loc loc |
|
| 44 |
Types.pp_error err; |
|
| 45 |
raise exc |
|
| 46 |
end |
|
| 47 |
in |
|
| 48 |
if !Options.print_types then |
|
| 49 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_type decls); |
|
| 50 |
new_env |
|
| 51 |
|
|
| 52 |
let clock_decls env decls = |
|
| 53 |
report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@,@?"); |
|
| 54 |
let new_env = |
|
| 55 |
begin |
|
| 56 |
try |
|
| 57 |
Clock_calculus.clock_prog env decls |
|
| 58 |
with (Clocks.Error (loc,err)) as exc -> |
|
| 59 |
Location.print loc; |
|
| 60 |
eprintf "Clock calculus error at loc %a: %a@]@." Location.pp_loc loc Clocks.pp_error err; |
|
| 61 |
raise exc |
|
| 62 |
end |
|
| 63 |
in |
|
| 64 |
if !Options.print_clocks then |
|
| 65 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_clock decls); |
|
| 66 |
new_env |
|
| 67 |
|
|
| 68 |
(* Loading Lusi file and filling type tables with parsed |
|
| 69 |
functions/nodes *) |
|
| 70 |
let load_lusi own filename = |
|
| 71 |
Location.input_name := filename; |
|
| 72 |
let lexbuf = Lexing.from_channel (open_in filename) in |
|
| 73 |
Location.init lexbuf filename; |
|
| 74 |
(* Parsing *) |
|
| 75 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename); |
|
| 76 |
try |
|
| 77 |
Parse.header own Parser_lustre.header Lexer_lustre.token lexbuf |
|
| 78 |
with |
|
| 79 |
| (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> |
|
| 80 |
Parse.report_error err; |
|
| 81 |
raise exc |
|
| 82 |
| Corelang.Error (loc, err) as exc -> |
|
| 83 |
Format.eprintf "Parsing error at loc %a: %a@]@." |
|
| 84 |
Location.pp_loc loc |
|
| 85 |
Corelang.pp_error err; |
|
| 86 |
raise exc |
|
| 87 |
|
|
| 88 |
let check_lusi header = |
|
| 89 |
let new_tenv = type_decls Basic_library.type_env header in (* Typing *) |
|
| 90 |
let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *) |
|
| 91 |
header, new_tenv, new_cenv |
|
| 92 |
|
|
| 93 |
let rec compile basename extension = |
|
| 94 |
(* Loading the input file *) |
|
| 95 |
let source_name = basename^extension in |
|
| 96 |
Location.input_name := source_name; |
|
| 97 |
let lexbuf = Lexing.from_channel (open_in source_name) in |
|
| 98 |
Location.init lexbuf source_name; |
|
| 99 |
(* Parsing *) |
|
| 100 |
report ~level:1 |
|
| 101 |
(fun fmt -> fprintf fmt "@[<v>.. parsing file %s@,@?" source_name); |
|
| 102 |
let prog = |
|
| 103 |
try |
|
| 104 |
Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf |
|
| 105 |
with |
|
| 106 |
| (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> |
|
| 107 |
Parse.report_error err; |
|
| 108 |
raise exc |
|
| 109 |
| Corelang.Error (loc, err) as exc -> |
|
| 110 |
Format.eprintf "Parsing error at loc %a: %a@]@." |
|
| 111 |
Location.pp_loc loc |
|
| 112 |
Corelang.pp_error err; |
|
| 113 |
raise exc |
|
| 114 |
in |
|
| 115 | 106 |
(* Extracting dependencies *) |
| 116 | 107 |
let dependencies, type_env, clock_env = import_dependencies prog in |
| 117 | 108 |
|
Also available in: Unified diff