Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Horn/horn_backend.ml | ||
---|---|---|
12 | 12 |
(* The compilation presented here was first defined in Garoche, Gurfinkel, |
13 | 13 |
Kahsai, HCSV'14. |
14 | 14 |
|
15 |
This is a modified version that handles reset and automaton |
|
16 |
*) |
|
15 |
This is a modified version that handles reset and automaton *) |
|
17 | 16 |
|
18 | 17 |
open Format |
19 | 18 |
open Lustre_types |
20 | 19 |
open Corelang |
21 | 20 |
open Machine_code_types |
22 |
|
|
23 | 21 |
open Horn_backend_common |
24 | 22 |
open Horn_backend_printers |
25 | 23 |
open Horn_backend_collecting_sem |
26 | 24 |
|
27 |
(* |
|
28 |
TODO: |
|
29 |
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows |
|
30 |
- gerer le reset --- DONE |
|
31 |
- reconstruire les rechable states DONE |
|
32 |
- reintroduire le cex/traces ... DONE |
|
33 |
- 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 ) |
|
34 |
*) |
|
25 |
(* TODO: - gerer les traces. Ca merde pour l'instant dans le calcul des memoires |
|
26 |
sur les arrows - gerer le reset --- DONE - reconstruire les rechable states |
|
27 |
DONE - reintroduire le cex/traces ... DONE - traiter les types enum et les |
|
28 |
branchements sur ces types enum (en particulier les traitements des resets |
|
29 |
qui ont lieu dans certaines branches et pas dans d'autres ) *) |
|
35 | 30 |
|
36 | 31 |
let main_print machines fmt = |
37 |
if !Options.main_node <> "" then |
|
38 |
begin |
|
32 |
if !Options.main_node <> "" then |
|
39 | 33 |
let node = !Options.main_node in |
40 | 34 |
let machine = get_machine machines node in |
41 |
if !Options.horn_cex then( |
|
35 |
if !Options.horn_cex then (
|
|
42 | 36 |
cex_computation machines fmt node machine; |
43 | 37 |
get_cex machines fmt machine) |
44 | 38 |
else ( |
45 | 39 |
collecting_semantics machines fmt node machine; |
46 |
check_prop machines fmt machine; |
|
47 |
) |
|
48 |
end |
|
49 |
|
|
40 |
check_prop machines fmt machine) |
|
50 | 41 |
|
51 | 42 |
let load_file f = |
52 | 43 |
let ic = open_in f in |
... | ... | |
58 | 49 |
|
59 | 50 |
let print_type_definitions fmt = |
60 | 51 |
let cpt_type = ref 0 in |
61 |
Hashtbl.iter (fun typ decl ->
|
|
62 |
match typ with
|
|
63 |
| Tydec_const var ->
|
|
64 |
(match decl.top_decl_desc with
|
|
65 |
| TypeDef tdef -> (
|
|
66 |
match tdef.tydef_desc with
|
|
67 |
| Tydec_enum tl ->
|
|
68 |
incr cpt_type;
|
|
69 |
fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
|
|
70 |
var
|
|
71 |
(Utils.fprintf_list ~sep:" " pp_print_string) tl
|
|
72 |
| _ -> assert false
|
|
73 |
)
|
|
74 |
| _ -> assert false
|
|
75 |
)
|
|
76 |
| _ -> ()) type_table
|
|
77 |
|
|
78 |
|
|
79 |
|
|
52 |
Hashtbl.iter |
|
53 |
(fun typ decl ->
|
|
54 |
match typ with
|
|
55 |
| Tydec_const var -> (
|
|
56 |
match decl.top_decl_desc with
|
|
57 |
| TypeDef tdef -> (
|
|
58 |
match tdef.tydef_desc with
|
|
59 |
| Tydec_enum tl ->
|
|
60 |
incr cpt_type;
|
|
61 |
fprintf fmt "(declare-datatypes () ((%s %a)));@.@." var
|
|
62 |
(Utils.fprintf_list ~sep:" " pp_print_string)
|
|
63 |
tl
|
|
64 |
| _ ->
|
|
65 |
assert false)
|
|
66 |
| _ ->
|
|
67 |
assert false)
|
|
68 |
| _ -> |
|
69 |
()) |
|
70 |
type_table |
|
80 | 71 |
|
81 | 72 |
let print_dep fmt prog = |
82 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,"); |
|
73 |
Log.report ~level:1 (fun fmt -> |
|
74 |
fprintf fmt "@[<v 2>.. extracting Horn libraries@,"); |
|
83 | 75 |
fprintf fmt "; Statically linked libraries@,"; |
84 | 76 |
let dependencies = Corelang.get_dependencies prog in |
85 | 77 |
List.iter |
86 | 78 |
(fun dep -> |
87 |
let (local, s) = Corelang.dependency_of_top dep in |
|
88 |
let basename = (Options_management.name_dependency (local, s) ".lusic") ^ ".smt2" in |
|
89 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); |
|
79 |
let local, s = Corelang.dependency_of_top dep in |
|
80 |
let basename = |
|
81 |
Options_management.name_dependency (local, s) ".lusic" ^ ".smt2" |
|
82 |
in |
|
83 |
Log.report ~level:1 (fun fmt -> |
|
84 |
Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); |
|
90 | 85 |
let horn = load_file basename in |
91 |
fprintf fmt "@.%s@." (horn); |
|
92 |
) |
|
86 |
fprintf fmt "@.%s@." horn) |
|
93 | 87 |
dependencies |
94 | 88 |
|
95 | 89 |
let check_sfunction mannot = |
96 |
(*Check if its an sfunction*) |
|
90 |
(*Check if its an sfunction*)
|
|
97 | 91 |
match mannot with |
98 |
[] -> false |
|
99 |
| [x] -> |
|
100 |
begin |
|
101 |
match x.annots with |
|
102 |
[] -> false |
|
103 |
|[(key, _)] -> |
|
104 |
begin |
|
105 |
match key with |
|
106 |
[] -> false |
|
107 |
| [x] -> x == "c_code" || x =="matlab" |
|
108 |
| _ -> false |
|
109 |
end |
|
110 |
|(_,_)::_ -> false |
|
111 |
end |
|
112 |
| _::_ -> false |
|
92 |
| [] -> |
|
93 |
false |
|
94 |
| [ x ] -> ( |
|
95 |
match x.annots with |
|
96 |
| [] -> |
|
97 |
false |
|
98 |
| [ (key, _) ] -> ( |
|
99 |
match key with |
|
100 |
| [] -> |
|
101 |
false |
|
102 |
| [ x ] -> |
|
103 |
x == "c_code" || x == "matlab" |
|
104 |
| _ -> |
|
105 |
false) |
|
106 |
| (_, _) :: _ -> |
|
107 |
false) |
|
108 |
| _ :: _ -> |
|
109 |
false |
|
113 | 110 |
|
114 | 111 |
let preprocess machines = |
115 |
List.fold_right (fun m res -> |
|
116 |
if List.mem m.mname.node_id registered_keywords then |
|
117 |
{ m with mname = { m.mname with node_id = protect_kwd m.mname.node_id }}::res |
|
118 |
else |
|
119 |
m :: res |
|
120 |
) machines [] |
|
121 |
|
|
122 |
let translate fmt prog machines= |
|
112 |
List.fold_right |
|
113 |
(fun m res -> |
|
114 |
if List.mem m.mname.node_id registered_keywords then |
|
115 |
{ |
|
116 |
m with |
|
117 |
mname = { m.mname with node_id = protect_kwd m.mname.node_id }; |
|
118 |
} |
|
119 |
:: res |
|
120 |
else m :: res) |
|
121 |
machines [] |
|
122 |
|
|
123 |
let translate fmt prog machines = |
|
123 | 124 |
let machines = preprocess machines in |
124 | 125 |
(* We print typedef *) |
125 |
print_dep fmt prog; (*print static library e.g. math*) |
|
126 |
print_dep fmt prog; |
|
127 |
(*print static library e.g. math*) |
|
126 | 128 |
print_type_definitions fmt; |
127 | 129 |
(*List.iter (print_machine machines fmt) (List.rev machines);*) |
128 |
List.iter(fun m -> |
|
130 |
List.iter |
|
131 |
(fun m -> |
|
129 | 132 |
let is_sfunction = check_sfunction m.mannot in |
130 |
if is_sfunction then( |
|
131 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id); |
|
132 |
print_sfunction machines fmt m |
|
133 |
) else ( |
|
134 |
print_machine machines fmt m) |
|
135 |
) |
|
136 |
(List.rev machines); |
|
133 |
if is_sfunction then ( |
|
134 |
Log.report ~level:1 (fun fmt -> |
|
135 |
fprintf fmt ".. detected sfunction: %s@," m.mname.node_id); |
|
136 |
print_sfunction machines fmt m) |
|
137 |
else print_machine machines fmt m) |
|
138 |
(List.rev machines); |
|
137 | 139 |
main_print machines fmt |
138 | 140 |
|
139 | 141 |
(* Local Variables: *) |
Also available in: Unified diff
reformatting