1
|
open Format
|
2
|
open LustreSpec
|
3
|
open Corelang
|
4
|
open Machine_code
|
5
|
|
6
|
|
7
|
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
|
8
|
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
|
9
|
|
10
|
let pp_type fmt t =
|
11
|
match (Types.repr t).Types.tdesc with
|
12
|
| Types.Tbool -> Format.fprintf fmt "Bool"
|
13
|
| Types.Tint -> Format.fprintf fmt "Int"
|
14
|
| Types.Tclock _
|
15
|
| Types.Tarray _
|
16
|
| Types.Tstatic _
|
17
|
| Types.Tconst _
|
18
|
| Types.Tarrow _
|
19
|
| _ -> Format.eprintf "internal error: pp_type %a@."
|
20
|
Types.print_ty t; assert false
|
21
|
|
22
|
|
23
|
let pp_decl_var fmt id =
|
24
|
Format.fprintf fmt "(declare_var %s %a)"
|
25
|
id.var_id
|
26
|
pp_type id.var_type
|
27
|
|
28
|
let pp_var fmt id = Format.pp_print_string fmt id.var_id
|
29
|
|
30
|
let pp_instr machine_name fmt i =
|
31
|
Format.fprintf fmt "(xxx)"
|
32
|
|
33
|
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
34
|
let rename_current machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_c")
|
35
|
let rename_current_list machine_name = List.map (rename_current machine_name)
|
36
|
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
|
37
|
let rename_next_list machine_name = List.map (rename_next machine_name)
|
38
|
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
|
39
|
let rename_machine_list machine_name = List.map (rename_machine machine_name)
|
40
|
|
41
|
let full_memory_vars machine instance =
|
42
|
(rename_current_list machine.mname.node_id machine.mmemory) @
|
43
|
(rename_next_list machine.mname.node_id machine.mmemory)
|
44
|
|
45
|
let machine_vars m =
|
46
|
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
|
47
|
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@
|
48
|
full_memory_vars m ()
|
49
|
|
50
|
|
51
|
(********************************************************************************************)
|
52
|
(* Instruction Printing functions *)
|
53
|
(********************************************************************************************)
|
54
|
|
55
|
let pp_horn_var m fmt id =
|
56
|
if Types.is_array_type id.var_type
|
57
|
then
|
58
|
assert false (* no arrays in Horn output *)
|
59
|
else
|
60
|
Format.fprintf fmt "%s" id.var_id
|
61
|
|
62
|
|
63
|
(* Used to print boolean constants *)
|
64
|
let pp_horn_tag fmt t =
|
65
|
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
|
66
|
|
67
|
(* Prints a constant value *)
|
68
|
let rec pp_horn_const fmt c =
|
69
|
match c with
|
70
|
| Const_int i -> pp_print_int fmt i
|
71
|
| Const_real r -> pp_print_string fmt r
|
72
|
| Const_float r -> pp_print_float fmt r
|
73
|
| Const_tag t -> pp_horn_tag fmt t
|
74
|
| Const_array ca -> assert false
|
75
|
|
76
|
(* Prints a value expression [v], with internal function calls only.
|
77
|
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
78
|
but an offset suffix may be added for array variables
|
79
|
*)
|
80
|
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
|
81
|
match v with
|
82
|
| Cst c -> pp_horn_const fmt c
|
83
|
| Array _
|
84
|
| Access _ -> assert false (* no arrays *)
|
85
|
| Power (v, n) -> assert false
|
86
|
| LocalVar v -> pp_var fmt (rename_machine self v)
|
87
|
| StateVar v ->
|
88
|
if Types.is_array_type v.var_type
|
89
|
then assert false
|
90
|
else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
|
91
|
| Fun (n, vl) -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
92
|
|
93
|
(* Prints a [value] indexed by the suffix list [loop_vars] *)
|
94
|
let rec pp_value_suffix self pp_value fmt value =
|
95
|
match value with
|
96
|
| Fun (n, vl) ->
|
97
|
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
|
98
|
| _ ->
|
99
|
pp_horn_val self pp_value fmt value
|
100
|
|
101
|
(* type_directed assignment: array vs. statically sized type
|
102
|
- [var_type]: type of variable to be assigned
|
103
|
- [var_name]: name of variable to be assigned
|
104
|
- [value]: assigned value
|
105
|
- [pp_var]: printer for variables
|
106
|
*)
|
107
|
let pp_assign m self pp_var fmt var_type var_name value =
|
108
|
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
|
109
|
|
110
|
let pp_instance_call
|
111
|
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
|
112
|
try (* stateful node instance *)
|
113
|
begin
|
114
|
let (n,_) = List.assoc i m.minstances in
|
115
|
match node_name n, inputs, outputs with
|
116
|
| "_arrow", [i1; i2], [o] -> begin
|
117
|
if init then
|
118
|
pp_assign
|
119
|
m
|
120
|
self
|
121
|
(pp_horn_var m)
|
122
|
(* (pp_horn_val self (pp_horn_var m) fmt o) *) fmt
|
123
|
o.var_type (LocalVar o) i1
|
124
|
else
|
125
|
pp_assign
|
126
|
m self (pp_horn_var m) fmt
|
127
|
o.var_type (LocalVar o) i2
|
128
|
|
129
|
end
|
130
|
| name, _, _ ->
|
131
|
begin
|
132
|
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
|
133
|
Format.fprintf fmt "(%s_%s %a%t%a%t%a)"
|
134
|
(node_name n)
|
135
|
(if init then "init" else "step")
|
136
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
|
137
|
(Utils.pp_final_char_if_non_empty " " inputs)
|
138
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
|
139
|
(Utils.pp_final_char_if_non_empty " " outputs)
|
140
|
(Utils.fprintf_list ~sep:" " pp_var) (full_memory_vars target_machine i)
|
141
|
|
142
|
end
|
143
|
end
|
144
|
with Not_found -> ( (* stateless node instance *)
|
145
|
let (n,_) = List.assoc i m.mcalls in
|
146
|
Format.fprintf fmt "(%s %a%t%a)"
|
147
|
(node_name n)
|
148
|
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
|
149
|
(Utils.pp_final_char_if_non_empty " " inputs)
|
150
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs
|
151
|
)
|
152
|
|
153
|
let pp_machine_reset (m: machine_t) self fmt inst =
|
154
|
let (node, static) = List.assoc inst m.minstances in
|
155
|
fprintf fmt "(%a %a%t%s->%s)"
|
156
|
pp_machine_reset_name (node_name node)
|
157
|
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
|
158
|
(Utils.pp_final_char_if_non_empty " " static)
|
159
|
self inst
|
160
|
|
161
|
(* TODO *)
|
162
|
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el =
|
163
|
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
|
164
|
(pp_horn_val self (pp_horn_var m)) c
|
165
|
(Utils.pp_newline_if_non_empty tl)
|
166
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl
|
167
|
(Utils.pp_newline_if_non_empty el)
|
168
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el
|
169
|
|
170
|
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
|
171
|
match instr with
|
172
|
| MReset i ->
|
173
|
pp_machine_reset m self fmt i
|
174
|
| MLocalAssign (i,v) ->
|
175
|
pp_assign
|
176
|
m self (pp_horn_var m) fmt
|
177
|
i.var_type (LocalVar i) v
|
178
|
| MStateAssign (i,v) ->
|
179
|
pp_assign
|
180
|
m self (pp_horn_var m) fmt
|
181
|
i.var_type (StateVar i) v
|
182
|
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
|
183
|
pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
|
184
|
| MStep (il, i, vl) ->
|
185
|
pp_instance_call machines ~init:init m self fmt i vl il
|
186
|
| MBranch (g,hl) ->
|
187
|
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
|
188
|
then (* boolean case, needs special treatment in C because truth value is not unique *)
|
189
|
(* may disappear if we optimize code by replacing last branch test with default *)
|
190
|
let tl = try List.assoc tag_true hl with Not_found -> [] in
|
191
|
let el = try List.assoc tag_false hl with Not_found -> [] in
|
192
|
pp_conditional machines ~init:init m self fmt g tl el
|
193
|
else assert false (* enum type case *)
|
194
|
|
195
|
|
196
|
(**************************************************************)
|
197
|
|
198
|
(* Print the machine m:
|
199
|
two functions: m_init and m_step
|
200
|
- m_init is a predicate over m memories
|
201
|
- m_step is a predicate over old_memories, inputs, new_memories, outputs
|
202
|
We first declare all variables then the two /rules/.
|
203
|
*)
|
204
|
let print_machine machines fmt m =
|
205
|
let pp_instr init = pp_machine_instr machines ~init:init m in
|
206
|
if m.mname.node_id = arrow_id then ()
|
207
|
else
|
208
|
( (* We don't print arrow function *)
|
209
|
Format.fprintf fmt "; %s@." m.mname.node_id;
|
210
|
(* Printing variables *)
|
211
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
212
|
((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
|
213
|
Format.pp_print_newline fmt ();
|
214
|
(* Declaring predicate *)
|
215
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
216
|
pp_machine_reset_name m.mname.node_id
|
217
|
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
|
218
|
|
219
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
220
|
pp_machine_step_name m.mname.node_id
|
221
|
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
|
222
|
Format.pp_print_newline fmt ();
|
223
|
|
224
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
|
225
|
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
226
|
m.mname.node_id
|
227
|
(Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
|
228
|
|
229
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
|
230
|
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
231
|
m.mname.node_id
|
232
|
(Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
|
233
|
|
234
|
()
|
235
|
)
|
236
|
|
237
|
let main_print fmt = ()
|
238
|
|
239
|
let translate fmt basename prog machines =
|
240
|
List.iter (print_machine machines fmt) (List.rev machines);
|
241
|
main_print fmt
|
242
|
|
243
|
|
244
|
(* Local Variables: *)
|
245
|
(* compile-command:"make -C .." *)
|
246
|
(* End: *)
|