Revision ca7ff3f7
Added by Lélio Brun 8 months 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