Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
| src/backends/Horn/horn_backend_common.ml | ||
|---|---|---|
| 17 | 17 |
let get_machine = Machine_code_common.get_machine |
| 18 | 18 |
|
| 19 | 19 |
let machine_reset_name id = id ^ "_reset" |
| 20 |
let machine_step_name id = id ^ "_step" |
|
| 21 |
let machine_stateless_name id = id ^ "_fun" |
|
| 20 |
|
|
| 21 |
let machine_step_name id = id ^ "_step" |
|
| 22 |
|
|
| 23 |
let machine_stateless_name id = id ^ "_fun" |
|
| 24 |
|
|
| 22 | 25 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id |
| 26 |
|
|
| 23 | 27 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
| 28 |
|
|
| 24 | 29 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id |
| 25 | 30 |
|
| 26 | 31 |
let rec pp_type fmt t = |
| 27 |
if Types.is_bool_type t then fprintf fmt "Bool" else |
|
| 28 |
if Types.is_int_type t then fprintf fmt "Int" else |
|
| 29 |
if Types.is_real_type t then fprintf fmt "Real" else |
|
| 30 |
match (Types.repr t).Types.tdesc with |
|
| 31 |
| Types.Tconst ty -> pp_print_string fmt ty |
|
| 32 |
| Types.Tclock t -> pp_type fmt t |
|
| 33 |
| Types.Tarray(_,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")" |
|
| 34 |
| Types.Tstatic(_, ty) -> pp_type fmt ty |
|
| 35 |
| Types.Tarrow _ |
|
| 36 |
| _ -> eprintf "internal error: pp_type %a@." |
|
| 37 |
Types.print_ty t; assert false |
|
| 32 |
if Types.is_bool_type t then fprintf fmt "Bool" |
|
| 33 |
else if Types.is_int_type t then fprintf fmt "Int" |
|
| 34 |
else if Types.is_real_type t then fprintf fmt "Real" |
|
| 35 |
else |
|
| 36 |
match (Types.repr t).Types.tdesc with |
|
| 37 |
| Types.Tconst ty -> |
|
| 38 |
pp_print_string fmt ty |
|
| 39 |
| Types.Tclock t -> |
|
| 40 |
pp_type fmt t |
|
| 41 |
| Types.Tarray (_, ty) -> |
|
| 42 |
fprintf fmt "(Array Int "; |
|
| 43 |
pp_type fmt ty; |
|
| 44 |
fprintf fmt ")" |
|
| 45 |
| Types.Tstatic (_, ty) -> |
|
| 46 |
pp_type fmt ty |
|
| 47 |
| Types.Tarrow _ | _ -> |
|
| 48 |
eprintf "internal error: pp_type %a@." Types.print_ty t; |
|
| 49 |
assert false |
|
| 38 | 50 |
|
| 39 | 51 |
let pp_decl_var fmt id = |
| 40 |
fprintf fmt "(declare-var %s %a)" |
|
| 41 |
id.var_id |
|
| 42 |
pp_type id.var_type |
|
| 43 |
|
|
| 44 |
(* let pp_var fmt id = pp_print_string fmt id.var_id *) |
|
| 52 |
fprintf fmt "(declare-var %s %a)" id.var_id pp_type id.var_type |
|
| 45 | 53 |
|
| 54 |
(* let pp_var fmt id = pp_print_string fmt id.var_id *) |
|
| 46 | 55 |
|
| 47 | 56 |
let pp_conj pp fmt l = |
| 48 | 57 |
match l with |
| 49 |
[] -> assert false |
|
| 50 |
| [x] -> pp fmt x |
|
| 51 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l |
|
| 52 |
|
|
| 53 |
|
|
| 58 |
| [] -> |
|
| 59 |
assert false |
|
| 60 |
| [ x ] -> |
|
| 61 |
pp fmt x |
|
| 62 |
| _ -> |
|
| 63 |
fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l |
|
| 54 | 64 |
|
| 55 | 65 |
(********************************************************************************************) |
| 56 |
(* Workaround to prevent the use of declared keywords as node name *)
|
|
| 66 |
(* Workaround to prevent the use of declared keywords as node name *)
|
|
| 57 | 67 |
(********************************************************************************************) |
| 58 |
let registered_keywords = ["implies"]
|
|
| 68 |
let registered_keywords = [ "implies" ]
|
|
| 59 | 69 |
|
| 60 |
let protect_kwd s = |
|
| 61 |
if List.mem s registered_keywords then |
|
| 62 |
"__" ^ s |
|
| 63 |
else |
|
| 64 |
s |
|
| 70 |
let protect_kwd s = if List.mem s registered_keywords then "__" ^ s else s |
|
| 65 | 71 |
|
| 66 | 72 |
let node_name n = |
| 67 | 73 |
let name = node_name n in |
| 68 | 74 |
protect_kwd name |
| 69 | 75 |
|
| 70 |
|
|
| 71 | 76 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
| 72 |
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
|
| 77 |
|
|
| 78 |
let rename f v = { v with var_id = f v.var_id }
|
|
| 79 |
|
|
| 73 | 80 |
let rename_machine p = rename (fun n -> concat p n) |
| 81 |
|
|
| 74 | 82 |
let rename_machine_list p = List.map (rename_machine p) |
| 75 | 83 |
|
| 76 |
let rename_current = rename (fun n -> n ^ "_c") |
|
| 84 |
let rename_current = rename (fun n -> n ^ "_c") |
|
| 85 |
|
|
| 77 | 86 |
let rename_current_list = List.map rename_current |
| 78 |
let rename_mid = rename (fun n -> n ^ "_m") |
|
| 87 |
|
|
| 88 |
let rename_mid = rename (fun n -> n ^ "_m") |
|
| 89 |
|
|
| 79 | 90 |
let rename_mid_list = List.map rename_mid |
| 91 |
|
|
| 80 | 92 |
let rename_next = rename (fun n -> n ^ "_x") |
| 81 |
let rename_next_list = List.map rename_next |
|
| 82 | 93 |
|
| 94 |
let rename_next_list = List.map rename_next |
|
| 83 | 95 |
|
| 84 | 96 |
let local_memory_vars machine = |
| 85 | 97 |
rename_machine_list machine.mname.node_id machine.mmemory |
| 86 |
|
|
| 87 |
let instances_memory_vars ?(without_arrow=false) machines machine =
|
|
| 98 |
|
|
| 99 |
let instances_memory_vars ?(without_arrow = false) machines machine =
|
|
| 88 | 100 |
let rec aux fst prefix m = |
| 89 |
( |
|
| 90 |
if not fst then ( |
|
| 91 |
(rename_machine_list (concat prefix m.mname.node_id) m.mmemory) |
|
| 92 |
) |
|
| 93 |
else [] |
|
| 94 |
) @ |
|
| 95 |
List.fold_left (fun accu (id, (n, _)) -> |
|
| 96 |
let name = node_name n in |
|
| 97 |
if without_arrow && name = "_arrow" then |
|
| 98 |
accu |
|
| 99 |
else |
|
| 100 |
let machine_n = get_machine machines name in |
|
| 101 |
( aux false (concat prefix |
|
| 102 |
(if fst then id else concat m.mname.node_id id)) |
|
| 103 |
machine_n ) @ accu |
|
| 104 |
) [] (m.minstances) |
|
| 101 |
(if not fst then |
|
| 102 |
rename_machine_list (concat prefix m.mname.node_id) m.mmemory |
|
| 103 |
else []) |
|
| 104 |
@ List.fold_left |
|
| 105 |
(fun accu (id, (n, _)) -> |
|
| 106 |
let name = node_name n in |
|
| 107 |
if without_arrow && name = "_arrow" then accu |
|
| 108 |
else |
|
| 109 |
let machine_n = get_machine machines name in |
|
| 110 |
aux false |
|
| 111 |
(concat prefix (if fst then id else concat m.mname.node_id id)) |
|
| 112 |
machine_n |
|
| 113 |
@ accu) |
|
| 114 |
[] m.minstances |
|
| 105 | 115 |
in |
| 106 | 116 |
aux true machine.mname.node_id machine |
| 107 | 117 |
|
| 108 | 118 |
(* Extract the arrows of a given node/machine *) |
| 109 | 119 |
let arrow_vars machines machine : Lustre_types.var_decl list = |
| 110 | 120 |
let rec aux fst prefix m = |
| 111 |
List.fold_left (fun accu (id, (n, _)) -> |
|
| 112 |
let name = node_name n in |
|
| 113 |
if name = "_arrow" then |
|
| 114 |
let arrow_machine = Machine_code_common.arrow_machine in |
|
| 115 |
(rename_machine_list |
|
| 116 |
(concat prefix (concat (if fst then id else concat m.mname.node_id id) "_arrow")) |
|
| 117 |
arrow_machine.mmemory |
|
| 118 |
) @ accu |
|
| 119 |
else |
|
| 120 |
let machine_n = get_machine machines name in |
|
| 121 |
( aux false (concat prefix |
|
| 122 |
(if fst then id else concat m.mname.node_id id)) |
|
| 123 |
machine_n ) @ accu |
|
| 124 |
) [] (m.minstances) |
|
| 121 |
List.fold_left |
|
| 122 |
(fun accu (id, (n, _)) -> |
|
| 123 |
let name = node_name n in |
|
| 124 |
if name = "_arrow" then |
|
| 125 |
let arrow_machine = Machine_code_common.arrow_machine in |
|
| 126 |
rename_machine_list |
|
| 127 |
(concat prefix |
|
| 128 |
(concat (if fst then id else concat m.mname.node_id id) "_arrow")) |
|
| 129 |
arrow_machine.mmemory |
|
| 130 |
@ accu |
|
| 131 |
else |
|
| 132 |
let machine_n = get_machine machines name in |
|
| 133 |
aux false |
|
| 134 |
(concat prefix (if fst then id else concat m.mname.node_id id)) |
|
| 135 |
machine_n |
|
| 136 |
@ accu) |
|
| 137 |
[] m.minstances |
|
| 125 | 138 |
in |
| 126 | 139 |
aux true machine.mname.node_id machine |
| 127 | 140 |
|
| 128 |
let full_memory_vars ?(without_arrow=false) machines machine =
|
|
| 129 |
(local_memory_vars machine)
|
|
| 130 |
@ (instances_memory_vars ~without_arrow machines machine)
|
|
| 141 |
let full_memory_vars ?(without_arrow = false) machines machine =
|
|
| 142 |
local_memory_vars machine
|
|
| 143 |
@ instances_memory_vars ~without_arrow machines machine
|
|
| 131 | 144 |
|
| 132 | 145 |
let inout_vars m = |
| 133 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)
|
|
| 134 |
@ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
|
|
| 146 |
rename_machine_list m.mname.node_id m.mstep.step_inputs
|
|
| 147 |
@ rename_machine_list m.mname.node_id m.mstep.step_outputs
|
|
| 135 | 148 |
|
| 136 | 149 |
let step_vars machines m = |
| 137 |
(inout_vars m)
|
|
| 138 |
@ (rename_current_list (full_memory_vars machines m))
|
|
| 139 |
@ (rename_next_list (full_memory_vars machines m))
|
|
| 150 |
inout_vars m
|
|
| 151 |
@ rename_current_list (full_memory_vars machines m)
|
|
| 152 |
@ rename_next_list (full_memory_vars machines m)
|
|
| 140 | 153 |
|
| 141 | 154 |
let step_vars_m_x machines m = |
| 142 |
(inout_vars m)
|
|
| 143 |
@ (rename_mid_list (full_memory_vars machines m))
|
|
| 144 |
@ (rename_next_list (full_memory_vars machines m))
|
|
| 155 |
inout_vars m
|
|
| 156 |
@ rename_mid_list (full_memory_vars machines m)
|
|
| 157 |
@ rename_next_list (full_memory_vars machines m)
|
|
| 145 | 158 |
|
| 146 | 159 |
let reset_vars machines m = |
| 147 |
(rename_current_list (full_memory_vars machines m))
|
|
| 148 |
@ (rename_mid_list (full_memory_vars machines m))
|
|
| 160 |
rename_current_list (full_memory_vars machines m)
|
|
| 161 |
@ rename_mid_list (full_memory_vars machines m)
|
|
| 149 | 162 |
|
| 150 | 163 |
let step_vars_c_m_x machines m = |
| 151 |
(inout_vars m) |
|
| 152 |
@ (rename_current_list (full_memory_vars machines m)) |
|
| 153 |
@ (rename_mid_list (full_memory_vars machines m)) |
|
| 154 |
@ (rename_next_list (full_memory_vars machines m)) |
|
| 155 |
|
|
| 164 |
inout_vars m |
|
| 165 |
@ rename_current_list (full_memory_vars machines m) |
|
| 166 |
@ rename_mid_list (full_memory_vars machines m) |
|
| 167 |
@ rename_next_list (full_memory_vars machines m) |
|
| 156 | 168 |
|
| 157 | 169 |
(* Local Variables: *) |
| 158 | 170 |
(* compile-command:"make -C ../.." *) |
Also available in: Unified diff
reformatting