lustrec / src / backends / Horn / horn_backend.ml @ 86ae18b7
History | View | Annotate | Download (3.98 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 |
Kahsai, HCSV'14. |
14 |
|
15 |
This is a modified version that handles reset and automaton |
16 |
*) |
17 |
|
18 |
open Format |
19 |
open LustreSpec |
20 |
open Corelang |
21 |
open Machine_code |
22 |
|
23 |
open Horn_backend_common |
24 |
open Horn_backend_printers |
25 |
open Horn_backend_collecting_sem |
26 |
|
27 |
(* |
28 |
TODO: |
29 |
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows |
30 |
|
31 |
- gerer le reset --- DONE |
32 |
- reconstruire les rechable states DONE |
33 |
- reintroduire le cex/traces ... DONE |
34 |
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres ) |
35 |
*) |
36 |
|
37 |
let main_print machines fmt = |
38 |
if !Options.main_node <> "" then |
39 |
begin |
40 |
let node = !Options.main_node in |
41 |
let machine = get_machine machines node in |
42 |
if !Options.horn_cex then( |
43 |
cex_computation machines fmt node machine; |
44 |
get_cex machines fmt node machine) |
45 |
else ( |
46 |
collecting_semantics machines fmt node machine; |
47 |
check_prop machines fmt node machine; |
48 |
) |
49 |
end |
50 |
|
51 |
|
52 |
let load_file f = |
53 |
let ic = open_in f in |
54 |
let n = in_channel_length ic in |
55 |
let s = String.create n in |
56 |
really_input ic s 0 n; |
57 |
close_in ic; |
58 |
(s) |
59 |
|
60 |
let print_type_definitions fmt = |
61 |
let cpt_type = ref 0 in |
62 |
Hashtbl.iter (fun typ decl -> |
63 |
match typ with |
64 |
| Tydec_const var -> |
65 |
(match decl.top_decl_desc with |
66 |
| TypeDef tdef -> ( |
67 |
match tdef.tydef_desc with |
68 |
| Tydec_enum tl -> |
69 |
incr cpt_type; |
70 |
fprintf fmt "(declare-datatypes () ((%s %a)));@.@." |
71 |
var |
72 |
(Utils.fprintf_list ~sep:" " pp_print_string) tl |
73 |
| _ -> assert false |
74 |
) |
75 |
| _ -> assert false |
76 |
) |
77 |
| _ -> ()) type_table |
78 |
|
79 |
|
80 |
|
81 |
|
82 |
let print_dep fmt prog = |
83 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,"); |
84 |
fprintf fmt "; Statically linked libraries@"; |
85 |
let dependencies = Corelang.get_dependencies prog in |
86 |
List.iter |
87 |
(fun dep -> |
88 |
let (local, s) = Corelang.dependency_of_top dep in |
89 |
let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in |
90 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); |
91 |
let horn = load_file basename in |
92 |
fprintf fmt "@.%s@." horn; |
93 |
) |
94 |
dependencies |
95 |
|
96 |
let check_sfunction mannot = |
97 |
(*Check if its an sfunction*) |
98 |
match mannot with |
99 |
[] -> false |
100 |
| [x] -> |
101 |
begin |
102 |
match x.annots with |
103 |
[] -> false |
104 |
|[(key,va)] -> |
105 |
begin |
106 |
match key with |
107 |
[] -> false |
108 |
| [x] -> x == "c_code" || x =="matlab" |
109 |
| _ -> false |
110 |
end |
111 |
|(_,_)::_ -> false |
112 |
end |
113 |
| _::_ -> false |
114 |
|
115 |
let translate fmt basename prog machines= |
116 |
(* We print typedef *) |
117 |
print_dep fmt prog; (*print static library e.g. math*) |
118 |
print_type_definitions fmt; |
119 |
(*List.iter (print_machine machines fmt) (List.rev machines);*) |
120 |
List.iter(fun m -> |
121 |
let is_sfunction = check_sfunction m.mannot in |
122 |
if is_sfunction then( |
123 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id); |
124 |
print_sfunction machines fmt m |
125 |
) else ( |
126 |
print_machine machines fmt m) |
127 |
) |
128 |
(List.rev machines); |
129 |
main_print machines fmt |
130 |
|
131 |
(* Local Variables: *) |
132 |
(* compile-command:"make -C ../.." *) |
133 |
(* End: *) |