Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/machine_code_common.ml | ||
---|---|---|
6 | 6 |
|
7 | 7 |
let print_statelocaltag = true |
8 | 8 |
|
9 |
let is_memory m id = |
|
10 |
(List.exists (fun o -> o.var_id = id.var_id) m.mmemory) |
|
9 |
let is_memory m id = List.exists (fun o -> o.var_id = id.var_id) m.mmemory |
|
11 | 10 |
|
12 |
let is_reset_flag id = |
|
13 |
id.var_id = "_reset" |
|
11 |
let is_reset_flag id = id.var_id = "_reset" |
|
14 | 12 |
|
15 |
let pp_vdecl fmt v = |
|
16 |
pp_print_string fmt v.var_id |
|
13 |
let pp_vdecl fmt v = pp_print_string fmt v.var_id |
|
17 | 14 |
|
18 | 15 |
let rec pp_val m fmt v = |
19 | 16 |
let pp_val = pp_val m in |
20 | 17 |
match v.value_desc with |
21 |
| Cst c -> Printers.pp_const fmt c |
|
22 |
| Var v -> |
|
18 |
| Cst c -> |
|
19 |
Printers.pp_const fmt c |
|
20 |
| Var v -> |
|
23 | 21 |
if is_memory m v then |
24 |
if print_statelocaltag then |
|
25 |
fprintf fmt "{%s}" v.var_id
|
|
26 |
else
|
|
27 |
pp_print_string fmt v.var_id
|
|
28 |
else
|
|
29 |
if print_statelocaltag then
|
|
30 |
fprintf fmt "%s" v.var_id
|
|
31 |
else
|
|
32 |
pp_vdecl fmt v
|
|
33 |
| Array vl -> pp_print_bracketed pp_val fmt vl
|
|
34 |
| Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
|
|
35 |
| Power (v, n) -> fprintf fmt "(%a^%a)" pp_val v pp_val n
|
|
36 |
| Fun (n, vl) -> fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
|
|
37 |
| ResetFlag -> fprintf fmt "RESET"
|
|
22 |
if print_statelocaltag then fprintf fmt "{%s}" v.var_id
|
|
23 |
else pp_print_string fmt v.var_id
|
|
24 |
else if print_statelocaltag then fprintf fmt "%s" v.var_id
|
|
25 |
else pp_vdecl fmt v
|
|
26 |
| Array vl ->
|
|
27 |
pp_print_bracketed pp_val fmt vl
|
|
28 |
| Access (t, i) ->
|
|
29 |
fprintf fmt "%a[%a]" pp_val t pp_val i
|
|
30 |
| Power (v, n) ->
|
|
31 |
fprintf fmt "(%a^%a)" pp_val v pp_val n
|
|
32 |
| Fun (n, vl) ->
|
|
33 |
fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
|
|
34 |
| ResetFlag ->
|
|
35 |
fprintf fmt "RESET"
|
|
38 | 36 |
|
39 | 37 |
module PrintSpec = struct |
40 |
|
|
41 | 38 |
let pp_reg fmt = function |
42 |
| ResetFlag -> pp_print_string fmt "{RESET}" |
|
43 |
| StateVar v -> fprintf fmt "{OUT:%a}" pp_vdecl v |
|
44 |
|
|
45 |
let pp_expr: type a. machine_t -> formatter -> (value_t, a) expression_t -> unit = |
|
46 |
fun m fmt -> function |
|
47 |
| Val v -> pp_val m fmt v |
|
48 |
| Tag t -> pp_print_string fmt t |
|
49 |
| Var v -> pp_vdecl fmt v |
|
50 |
| Memory r -> pp_reg fmt r |
|
39 |
| ResetFlag -> |
|
40 |
pp_print_string fmt "{RESET}" |
|
41 |
| StateVar v -> |
|
42 |
fprintf fmt "{OUT:%a}" pp_vdecl v |
|
43 |
|
|
44 |
let pp_expr : |
|
45 |
type a. machine_t -> formatter -> (value_t, a) expression_t -> unit = |
|
46 |
fun m fmt -> function |
|
47 |
| Val v -> |
|
48 |
pp_val m fmt v |
|
49 |
| Tag t -> |
|
50 |
pp_print_string fmt t |
|
51 |
| Var v -> |
|
52 |
pp_vdecl fmt v |
|
53 |
| Memory r -> |
|
54 |
pp_reg fmt r |
|
51 | 55 |
|
52 | 56 |
let pp_predicate m fmt p = |
53 |
let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit = |
|
54 |
fun fmt e -> pp_expr m fmt e
|
|
57 |
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
|
58 |
fun fmt e -> pp_expr m fmt e |
|
55 | 59 |
in |
56 | 60 |
match p with |
57 | 61 |
| Transition (f, inst, i, inputs, locals, outputs, _r, _mems) -> |
58 |
fprintf fmt "Transition_%a<%a>%a%a" |
|
59 |
pp_print_string f |
|
60 |
(pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF") |
|
61 |
pp_print_string) inst |
|
62 |
(pp_print_option pp_print_int) i |
|
63 |
(pp_print_parenthesized pp_expr) (inputs @ locals @ outputs) |
|
62 |
fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f |
|
63 |
(pp_print_option |
|
64 |
~none:(fun fmt () -> pp_print_string fmt "SELF") |
|
65 |
pp_print_string) |
|
66 |
inst |
|
67 |
(pp_print_option pp_print_int) |
|
68 |
i |
|
69 |
(pp_print_parenthesized pp_expr) |
|
70 |
(inputs @ locals @ outputs) |
|
64 | 71 |
| Reset (f, inst, r) -> |
65 |
fprintf fmt "Reset_%a<%a> on %a" |
|
66 |
pp_print_string f |
|
67 |
pp_print_string inst |
|
72 |
fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst |
|
68 | 73 |
(pp_val m) r |
69 | 74 |
| MemoryPack (f, inst, i) -> |
70 |
fprintf fmt "MemoryPack_%a<%a>%a" |
|
71 |
pp_print_string f |
|
72 |
(pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF") |
|
73 |
pp_print_string) inst |
|
74 |
(pp_print_option pp_print_int) i |
|
75 |
fprintf fmt "MemoryPack_%a<%a>%a" pp_print_string f |
|
76 |
(pp_print_option |
|
77 |
~none:(fun fmt () -> pp_print_string fmt "SELF") |
|
78 |
pp_print_string) |
|
79 |
inst |
|
80 |
(pp_print_option pp_print_int) |
|
81 |
i |
|
75 | 82 |
| ResetCleared f -> |
76 | 83 |
fprintf fmt "ResetCleared_%a" pp_print_string f |
77 |
| Initialization -> () |
|
84 |
| Initialization -> |
|
85 |
() |
|
78 | 86 |
|
79 | 87 |
let pp_spec m = |
80 |
let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit = |
|
81 |
fun fmt e -> pp_expr m fmt e
|
|
88 |
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
|
89 |
fun fmt e -> pp_expr m fmt e |
|
82 | 90 |
in |
83 | 91 |
let rec pp_spec fmt f = |
84 | 92 |
match f with |
85 |
| True -> pp_print_string fmt "true" |
|
86 |
| False -> pp_print_string fmt "false" |
|
93 |
| True -> |
|
94 |
pp_print_string fmt "true" |
|
95 |
| False -> |
|
96 |
pp_print_string fmt "false" |
|
87 | 97 |
| Equal (a, b) -> |
88 | 98 |
fprintf fmt "%a == %a" pp_expr a pp_expr b |
89 | 99 |
| And fs -> |
90 |
pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ") |
|
91 |
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs |
|
100 |
pp_print_list |
|
101 |
~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ") |
|
102 |
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) |
|
103 |
fmt fs |
|
92 | 104 |
| Or fs -> |
93 |
pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ") |
|
94 |
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs |
|
105 |
pp_print_list |
|
106 |
~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ") |
|
107 |
(fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) |
|
108 |
fmt fs |
|
95 | 109 |
| Imply (a, b) -> |
96 | 110 |
fprintf fmt "%a@ -> %a" pp_spec a pp_spec b |
97 | 111 |
| Exists (xs, a) -> |
98 | 112 |
fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]" |
99 |
(pp_comma_list Printers.pp_var) xs pp_spec a |
|
113 |
(pp_comma_list Printers.pp_var) |
|
114 |
xs pp_spec a |
|
100 | 115 |
| Forall (xs, a) -> |
101 | 116 |
fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]" |
102 |
(pp_comma_list Printers.pp_var) xs pp_spec a |
|
117 |
(pp_comma_list Printers.pp_var) |
|
118 |
xs pp_spec a |
|
103 | 119 |
| Ternary (e, a, b) -> |
104 |
fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])" |
|
105 |
pp_expr e pp_spec a pp_spec b
|
|
120 |
fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])" pp_expr e
|
|
121 |
pp_spec a pp_spec b |
|
106 | 122 |
| Predicate p -> |
107 | 123 |
pp_predicate m fmt p |
108 | 124 |
| StateVarPack r -> |
109 | 125 |
fprintf fmt "StateVarPack<%a>" pp_reg r |
110 | 126 |
| ExistsMem (_f, a, b) -> |
111 |
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [a; b])
|
|
127 |
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
|
|
112 | 128 |
in |
113 | 129 |
pp_spec |
114 |
|
|
115 | 130 |
end |
116 | 131 |
|
117 | 132 |
let pp_spec m = |
118 | 133 |
if !Options.spec <> "no" then |
119 |
pp_print_list |
|
120 |
~pp_open_box:pp_open_vbox0 |
|
121 |
~pp_prologue:pp_print_cut |
|
134 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut |
|
122 | 135 |
(fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m)) |
123 |
else |
|
124 |
pp_print_nothing |
|
136 |
else pp_print_nothing |
|
125 | 137 |
|
126 | 138 |
let rec pp_instr m fmt i = |
127 | 139 |
let pp_val = pp_val m in |
128 | 140 |
let pp_branch = pp_branch m in |
129 |
begin match i.instr_desc with |
|
130 |
| MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v |
|
131 |
| MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v |
|
132 |
| MResetAssign b -> fprintf fmt "RESET := %a" pp_print_bool b |
|
133 |
| MSetReset i -> fprintf fmt "set_reset %s" i |
|
134 |
| MClearReset -> fprintf fmt "clear_reset %s" m.mname.node_id |
|
135 |
| MNoReset i -> fprintf fmt "noreset %s" i |
|
136 |
| MStep (il, i, vl) -> |
|
137 |
fprintf fmt "%a := %s%a" |
|
138 |
(pp_comma_list pp_vdecl) il |
|
139 |
i |
|
140 |
(pp_print_parenthesized pp_val) vl |
|
141 |
| MBranch (g,hl) -> |
|
142 |
fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}" |
|
143 |
pp_val g |
|
144 |
(pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) hl |
|
145 |
| MComment s -> pp_print_string fmt s |
|
146 |
| MSpec s -> pp_print_string fmt ("@" ^ s) |
|
147 |
|
|
148 |
end; |
|
141 |
(match i.instr_desc with |
|
142 |
| MLocalAssign (i, v) -> |
|
143 |
fprintf fmt "%s := %a" i.var_id pp_val v |
|
144 |
| MStateAssign (i, v) -> |
|
145 |
fprintf fmt "{%s} := %a" i.var_id pp_val v |
|
146 |
| MResetAssign b -> |
|
147 |
fprintf fmt "RESET := %a" pp_print_bool b |
|
148 |
| MSetReset i -> |
|
149 |
fprintf fmt "set_reset %s" i |
|
150 |
| MClearReset -> |
|
151 |
fprintf fmt "clear_reset %s" m.mname.node_id |
|
152 |
| MNoReset i -> |
|
153 |
fprintf fmt "noreset %s" i |
|
154 |
| MStep (il, i, vl) -> |
|
155 |
fprintf fmt "%a := %s%a" (pp_comma_list pp_vdecl) il i |
|
156 |
(pp_print_parenthesized pp_val) |
|
157 |
vl |
|
158 |
| MBranch (g, hl) -> |
|
159 |
fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}" pp_val g |
|
160 |
(pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) |
|
161 |
hl |
|
162 |
| MComment s -> |
|
163 |
pp_print_string fmt s |
|
164 |
| MSpec s -> |
|
165 |
pp_print_string fmt ("@" ^ s)); |
|
149 | 166 |
(* Annotation *) |
150 | 167 |
(* let _ = *) |
151 |
(* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *) |
|
168 |
(* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original |
|
169 |
expr: %a" Printers.pp_expr e *) |
|
152 | 170 |
(* in *) |
153 |
begin match i.lustre_eq with |
|
154 |
| None -> () |
|
155 |
| Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq |
|
156 |
end; |
|
171 |
(match i.lustre_eq with |
|
172 |
| None -> |
|
173 |
() |
|
174 |
| Some eq -> |
|
175 |
fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq); |
|
157 | 176 |
pp_spec m fmt i.instr_spec |
158 | 177 |
|
159 |
|
|
160 | 178 |
and pp_branch m fmt (t, h) = |
161 | 179 |
fprintf fmt "@[<v 2>%s:@,%a@]" t |
162 |
(pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h |
|
163 |
|
|
164 |
let pp_instrs m = |
|
165 |
pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m) |
|
180 |
(pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) |
|
181 |
h |
|
166 | 182 |
|
183 |
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m) |
|
167 | 184 |
|
168 | 185 |
(* merge log: get_node_def was in c0f8 *) |
169 | 186 |
(* Returns the node/machine associated to id in m calls *) |
170 | 187 |
let get_node_def id m = |
171 | 188 |
try |
172 |
let (decl, _) = List.assoc id m.mcalls in
|
|
189 |
let decl, _ = List.assoc id m.mcalls in
|
|
173 | 190 |
Corelang.node_of_top decl |
174 |
with Not_found -> (
|
|
191 |
with Not_found -> |
|
175 | 192 |
(* eprintf "Unable to find node %s in list [%a]@.@?" *) |
176 | 193 |
(* id *) |
177 |
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *) |
|
194 |
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) |
|
195 |
m.mcalls *) |
|
178 | 196 |
(* ; *) |
179 | 197 |
raise Not_found |
180 |
) |
|
181 |
|
|
198 |
|
|
182 | 199 |
(* merge log: machine_vars was in 44686 *) |
183 |
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory |
|
200 |
let machine_vars m = |
|
201 |
m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory |
|
184 | 202 |
|
185 | 203 |
let pp_step m fmt s = |
186 | 204 |
fprintf fmt |
187 |
"@[<v>\ |
|
188 |
inputs : %a@ \ |
|
189 |
outputs: %a@ \ |
|
190 |
locals : %a@ \ |
|
191 |
checks : %a@ \ |
|
192 |
instrs : @[%a@]@ \ |
|
205 |
"@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ \ |
|
193 | 206 |
asserts : @[%a@]@]@ " |
194 |
(pp_comma_list Printers.pp_var) s.step_inputs |
|
195 |
(pp_comma_list Printers.pp_var) s.step_outputs |
|
196 |
(pp_comma_list Printers.pp_var) s.step_locals |
|
207 |
(pp_comma_list Printers.pp_var) |
|
208 |
s.step_inputs |
|
209 |
(pp_comma_list Printers.pp_var) |
|
210 |
s.step_outputs |
|
211 |
(pp_comma_list Printers.pp_var) |
|
212 |
s.step_locals |
|
197 | 213 |
(pp_comma_list (fun fmt (_, c) -> pp_val m fmt c)) |
198 |
s.step_checks |
|
199 |
(pp_instrs m) s.step_instrs
|
|
200 |
(pp_comma_list (pp_val m)) s.step_asserts
|
|
214 |
s.step_checks (pp_instrs m) s.step_instrs
|
|
215 |
(pp_comma_list (pp_val m))
|
|
216 |
s.step_asserts |
|
201 | 217 |
|
202 | 218 |
let pp_static_call fmt (node, args) = |
203 |
fprintf fmt "%s<%a>" |
|
204 |
(node_name node)
|
|
205 |
(pp_comma_list Dimension.pp_dimension) args
|
|
219 |
fprintf fmt "%s<%a>" (node_name node)
|
|
220 |
(pp_comma_list Dimension.pp_dimension)
|
|
221 |
args |
|
206 | 222 |
|
207 |
let pp_instance fmt (o1, o2) = |
|
208 |
fprintf fmt "(%s, %a)" |
|
209 |
o1 |
|
210 |
pp_static_call o2 |
|
223 |
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2 |
|
211 | 224 |
|
212 | 225 |
let pp_memory_pack m fmt mp = |
213 |
fprintf fmt |
|
214 |
"@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]" |
|
215 |
pp_print_string mp.mpname.node_id |
|
216 |
(pp_print_option pp_print_int) mp.mpindex |
|
217 |
(PrintSpec.pp_spec m) mp.mpformula |
|
226 |
fprintf fmt "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]" pp_print_string |
|
227 |
mp.mpname.node_id |
|
228 |
(pp_print_option pp_print_int) |
|
229 |
mp.mpindex (PrintSpec.pp_spec m) mp.mpformula |
|
218 | 230 |
|
219 | 231 |
let pp_memory_packs m fmt = |
220 | 232 |
if !Options.spec <> "no" then |
221 |
fprintf fmt |
|
222 |
"@[<v 2>memory_packs:@ %a@]" |
|
223 |
(pp_print_list (pp_memory_pack m)) |
|
224 |
else |
|
225 |
pp_print_nothing fmt |
|
233 |
fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m)) |
|
234 |
else pp_print_nothing fmt |
|
226 | 235 |
|
227 | 236 |
let pp_transition m fmt t = |
228 |
fprintf fmt |
|
229 |
"@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" |
|
230 |
pp_print_string t.tname.node_id |
|
231 |
(pp_print_option pp_print_int) t.tindex |
|
232 |
(pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs) |
|
237 |
fprintf fmt "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" pp_print_string |
|
238 |
t.tname.node_id |
|
239 |
(pp_print_option pp_print_int) |
|
240 |
t.tindex |
|
241 |
(pp_print_parenthesized pp_vdecl) |
|
242 |
(t.tinputs @ t.tlocals @ t.toutputs) |
|
233 | 243 |
(PrintSpec.pp_spec m) t.tformula |
234 | 244 |
|
235 | 245 |
let pp_transitions m fmt = |
236 | 246 |
if !Options.spec <> "no" then |
237 |
fprintf fmt |
|
238 |
"@[<v 2>transitions:@ %a@]" |
|
239 |
(pp_print_list (pp_transition m)) |
|
240 |
else |
|
241 |
pp_print_nothing fmt |
|
247 |
fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m)) |
|
248 |
else pp_print_nothing fmt |
|
242 | 249 |
|
243 | 250 |
let pp_machine fmt m = |
244 | 251 |
fprintf fmt |
245 |
"@[<v 2>machine %s@ \ |
|
246 |
mem : %a@ \ |
|
247 |
instances: %a@ \ |
|
248 |
init : %a@ \ |
|
249 |
const : %a@ \ |
|
250 |
step :@ \ |
|
251 |
@[<v 2>%a@]@ \ |
|
252 |
spec : @[<v>%t@ %a@ @ %a@]@ \ |
|
253 |
annot : @[%a@]@]@ " |
|
252 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const \ |
|
253 |
: %a@ step :@ @[<v 2>%a@]@ spec : @[<v>%t@ %a@ @ %a@]@ annot \ |
|
254 |
: @[%a@]@]@ " |
|
254 | 255 |
m.mname.node_id |
255 |
(pp_comma_list Printers.pp_var) m.mmemory |
|
256 |
(pp_comma_list pp_instance) m.minstances |
|
257 |
(pp_instrs m) m.minit |
|
258 |
(pp_instrs m) m.mconst |
|
259 |
(pp_step m) m.mstep |
|
260 |
(fun fmt -> match m.mspec.mnode_spec with |
|
261 |
| None -> () |
|
262 |
| Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id |
|
263 |
| Some (Contract spec) -> Printers.pp_spec fmt spec) |
|
264 |
(pp_memory_packs m) m.mspec.mmemory_packs |
|
265 |
(pp_transitions m) m.mspec.mtransitions |
|
266 |
(pp_print_list Printers.pp_expr_annot) m.mannot |
|
267 |
|
|
268 |
let pp_machines = |
|
269 |
pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine |
|
256 |
(pp_comma_list Printers.pp_var) |
|
257 |
m.mmemory |
|
258 |
(pp_comma_list pp_instance) |
|
259 |
m.minstances (pp_instrs m) m.minit (pp_instrs m) m.mconst (pp_step m) |
|
260 |
m.mstep |
|
261 |
(fun fmt -> |
|
262 |
match m.mspec.mnode_spec with |
|
263 |
| None -> |
|
264 |
() |
|
265 |
| Some (NodeSpec id) -> |
|
266 |
fprintf fmt "cocospec: %s" id |
|
267 |
| Some (Contract spec) -> |
|
268 |
Printers.pp_spec fmt spec) |
|
269 |
(pp_memory_packs m) m.mspec.mmemory_packs (pp_transitions m) |
|
270 |
m.mspec.mtransitions |
|
271 |
(pp_print_list Printers.pp_expr_annot) |
|
272 |
m.mannot |
|
273 |
|
|
274 |
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine |
|
270 | 275 |
|
271 | 276 |
let rec is_const_value v = |
272 | 277 |
match v.value_desc with |
273 |
| Cst _ -> true |
|
274 |
| Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args |
|
275 |
| _ -> false |
|
278 |
| Cst _ -> |
|
279 |
true |
|
280 |
| Fun (_, args) -> |
|
281 |
Basic_library.is_value_internal_fun v && List.for_all is_const_value args |
|
282 |
| _ -> |
|
283 |
false |
|
276 | 284 |
|
277 | 285 |
(* Returns the declared stateless status and the computed one. *) |
278 | 286 |
let get_stateless_status_node n = |
279 |
(n.node_dec_stateless, |
|
280 |
try |
|
281 |
Utils.desome n.node_stateless |
|
282 |
with _ -> failwith ("stateless status of machine " ^ n.node_id ^ " not computed")) |
|
283 |
|
|
284 |
let get_stateless_status_top_decl td = match td.top_decl_desc with |
|
285 |
| Node n -> get_stateless_status_node n |
|
286 |
| ImportedNode n -> n.nodei_stateless, false |
|
287 |
| _ -> true, false |
|
288 |
|
|
289 |
let get_stateless_status m = |
|
290 |
get_stateless_status_node m.mname |
|
287 |
( n.node_dec_stateless, |
|
288 |
try Utils.desome n.node_stateless |
|
289 |
with _ -> |
|
290 |
failwith ("stateless status of machine " ^ n.node_id ^ " not computed") ) |
|
291 |
|
|
292 |
let get_stateless_status_top_decl td = |
|
293 |
match td.top_decl_desc with |
|
294 |
| Node n -> |
|
295 |
get_stateless_status_node n |
|
296 |
| ImportedNode n -> |
|
297 |
n.nodei_stateless, false |
|
298 |
| _ -> |
|
299 |
true, false |
|
300 |
|
|
301 |
let get_stateless_status m = get_stateless_status_node m.mname |
|
291 | 302 |
|
292 | 303 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
293 | 304 |
|
... | ... | |
299 | 310 |
|
300 | 311 |
let get_instr_spec i = i.instr_spec |
301 | 312 |
|
302 |
let mk_val v t = |
|
303 |
{ value_desc = v; |
|
304 |
value_type = t; |
|
305 |
value_annot = None } |
|
313 |
let mk_val v t = { value_desc = v; value_type = t; value_annot = None } |
|
306 | 314 |
|
307 |
let vdecl_to_val vd = |
|
308 |
mk_val (Var vd) vd.var_type |
|
315 |
let vdecl_to_val vd = mk_val (Var vd) vd.var_type |
|
309 | 316 |
|
310 |
let vdecls_to_vals = |
|
311 |
List.map vdecl_to_val |
|
317 |
let vdecls_to_vals = List.map vdecl_to_val |
|
312 | 318 |
|
313 | 319 |
let id_to_tag id = |
314 | 320 |
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in |
... | ... | |
319 | 325 |
(* (Ternary (Val c, |
320 | 326 |
* And (List.map get_instr_spec t), |
321 | 327 |
* And (List.map get_instr_spec e))) *) |
322 |
(MBranch(c, [ |
|
323 |
(tag_true, t); |
|
324 |
(tag_false, e) ])) |
|
328 |
(MBranch (c, [ tag_true, t; tag_false, e ])) |
|
325 | 329 |
|
326 | 330 |
let mk_branch ?lustre_eq c br = |
327 | 331 |
mkinstr ?lustre_eq |
... | ... | |
330 | 334 |
* br)) *) |
331 | 335 |
(MBranch (c, br)) |
332 | 336 |
|
333 |
let mk_branch' ?lustre_eq v = |
|
334 |
mk_branch ?lustre_eq (vdecl_to_val v) |
|
337 |
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v) |
|
335 | 338 |
|
336 | 339 |
let mk_assign ?lustre_eq x v = |
337 |
mkinstr ?lustre_eq |
|
338 |
(* (Equal (Var x, Val v)) *) |
|
339 |
(MLocalAssign (x, v)) |
|
340 |
mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v)) |
|
340 | 341 |
|
341 | 342 |
let arrow_machine = |
342 | 343 |
let state = "_first" in |
343 |
let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in |
|
344 |
let var_state = |
|
345 |
dummy_var_decl state Type_predef.type_bool |
|
346 |
(* (Types.new_ty Types.Tbool) *) |
|
347 |
in |
|
344 | 348 |
let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in |
345 | 349 |
let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in |
346 | 350 |
let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in |
347 | 351 |
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |
348 |
assert(var_input1.var_type = var_input2.var_type); |
|
349 |
let t_arg = var_input1.var_type in (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de reprendre le type des variables non ? *) |
|
352 |
assert (var_input1.var_type = var_input2.var_type); |
|
353 |
let t_arg = var_input1.var_type in |
|
354 |
(* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de |
|
355 |
reprendre le type des variables non ? *) |
|
350 | 356 |
{ |
351 | 357 |
mname = Arrow.arrow_desc; |
352 |
mmemory = [var_state];
|
|
358 |
mmemory = [ var_state ];
|
|
353 | 359 |
mcalls = []; |
354 | 360 |
minstances = []; |
355 |
minit = [mkinstr (MStateAssign(var_state, cst true))];
|
|
361 |
minit = [ mkinstr (MStateAssign (var_state, cst true)) ];
|
|
356 | 362 |
mstatic = []; |
357 | 363 |
mconst = []; |
358 |
mstep = { |
|
359 |
step_inputs = Arrow.arrow_desc.node_inputs; |
|
360 |
step_outputs = Arrow.arrow_desc.node_outputs; |
|
361 |
step_locals = []; |
|
362 |
step_checks = []; |
|
363 |
step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool) |
|
364 |
(List.map mkinstr |
|
365 |
[MStateAssign(var_state, cst false); |
|
366 |
MLocalAssign(var_output, mk_val (Var var_input1) t_arg)]) |
|
367 |
(List.map mkinstr |
|
368 |
[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ]; |
|
369 |
step_asserts = []; |
|
370 |
}; |
|
364 |
mstep = |
|
365 |
{ |
|
366 |
step_inputs = Arrow.arrow_desc.node_inputs; |
|
367 |
step_outputs = Arrow.arrow_desc.node_outputs; |
|
368 |
step_locals = []; |
|
369 |
step_checks = []; |
|
370 |
step_instrs = |
|
371 |
[ |
|
372 |
mk_conditional |
|
373 |
(mk_val (Var var_state) Type_predef.type_bool) |
|
374 |
(List.map mkinstr |
|
375 |
[ |
|
376 |
MStateAssign (var_state, cst false); |
|
377 |
MLocalAssign (var_output, mk_val (Var var_input1) t_arg); |
|
378 |
]) |
|
379 |
(List.map mkinstr |
|
380 |
[ MLocalAssign (var_output, mk_val (Var var_input2) t_arg) ]); |
|
381 |
]; |
|
382 |
step_asserts = []; |
|
383 |
}; |
|
371 | 384 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] }; |
372 | 385 |
mannot = []; |
373 |
msch = None |
|
386 |
msch = None;
|
|
374 | 387 |
} |
375 | 388 |
|
376 | 389 |
let empty_desc = |
... | ... | |
378 | 391 |
node_id = Arrow.arrow_id; |
379 | 392 |
node_type = Types.bottom; |
380 | 393 |
node_clock = Clocks.bottom; |
381 |
node_inputs= []; |
|
382 |
node_outputs= []; |
|
383 |
node_locals= []; |
|
394 |
node_inputs = [];
|
|
395 |
node_outputs = [];
|
|
396 |
node_locals = [];
|
|
384 | 397 |
node_gencalls = []; |
385 | 398 |
node_checks = []; |
386 | 399 |
node_asserts = []; |
387 |
node_stmts= []; |
|
400 |
node_stmts = [];
|
|
388 | 401 |
node_dec_stateless = true; |
389 | 402 |
node_stateless = Some true; |
390 | 403 |
node_spec = None; |
391 | 404 |
node_annot = []; |
392 | 405 |
node_iscontract = false; |
393 |
} |
|
406 |
}
|
|
394 | 407 |
|
395 | 408 |
let empty_machine = |
396 | 409 |
{ |
... | ... | |
401 | 414 |
minit = []; |
402 | 415 |
mstatic = []; |
403 | 416 |
mconst = []; |
404 |
mstep = { |
|
405 |
step_inputs = []; |
|
406 |
step_outputs = []; |
|
407 |
step_locals = []; |
|
408 |
step_checks = []; |
|
409 |
step_instrs = []; |
|
410 |
step_asserts = []; |
|
411 |
}; |
|
417 |
mstep = |
|
418 |
{ |
|
419 |
step_inputs = []; |
|
420 |
step_outputs = []; |
|
421 |
step_locals = []; |
|
422 |
step_checks = []; |
|
423 |
step_instrs = []; |
|
424 |
step_asserts = []; |
|
425 |
}; |
|
412 | 426 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] }; |
413 | 427 |
mannot = []; |
414 |
msch = None |
|
428 |
msch = None;
|
|
415 | 429 |
} |
416 | 430 |
|
417 | 431 |
let new_instance = |
418 | 432 |
let cpt = ref (-1) in |
419 | 433 |
fun callee tag -> |
420 |
begin
|
|
421 |
let o =
|
|
422 |
if Stateless.check_node callee then
|
|
423 |
node_name callee
|
|
424 |
else
|
|
425 |
Printf.sprintf "ni_%d" (incr cpt; !cpt) in
|
|
426 |
let o =
|
|
427 |
if !Options.ansi && is_generic_node callee
|
|
428 |
then Printf.sprintf "%s_inst_%d"
|
|
429 |
o
|
|
430 |
(incr cpt; !cpt)
|
|
431 |
else o in
|
|
432 |
o |
|
433 |
end
|
|
434 |
|
|
434 |
let o =
|
|
435 |
if Stateless.check_node callee then node_name callee
|
|
436 |
else
|
|
437 |
Printf.sprintf "ni_%d"
|
|
438 |
(incr cpt;
|
|
439 |
!cpt)
|
|
440 |
in
|
|
441 |
let o =
|
|
442 |
if !Options.ansi && is_generic_node callee then
|
|
443 |
Printf.sprintf "%s_inst_%d" o
|
|
444 |
(incr cpt;
|
|
445 |
!cpt)
|
|
446 |
else o
|
|
447 |
in
|
|
448 |
o |
|
435 | 449 |
|
436 | 450 |
let get_machine_opt machines name = |
437 | 451 |
List.fold_left |
438 | 452 |
(fun res m -> |
439 | 453 |
match res with |
440 |
| Some _ -> res |
|
441 |
| None -> if m.mname.node_id = name then Some m else None) |
|
454 |
| Some _ -> |
|
455 |
res |
|
456 |
| None -> |
|
457 |
if m.mname.node_id = name then Some m else None) |
|
442 | 458 |
None machines |
443 | 459 |
|
444 | 460 |
let get_machine machines node_name = |
445 |
try
|
|
446 |
Utils.desome (get_machine_opt machines node_name)
|
|
447 |
with Utils.DeSome ->
|
|
448 |
eprintf "Unable to find machine %s in machines %a@.@?"
|
|
449 |
node_name
|
|
450 |
(Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
|
|
451 |
; assert false
|
|
452 |
|
|
461 |
try Utils.desome (get_machine_opt machines node_name)
|
|
462 |
with Utils.DeSome ->
|
|
463 |
eprintf "Unable to find machine %s in machines %a@.@?" node_name
|
|
464 |
(Utils.fprintf_list ~sep:", " (fun fmt m ->
|
|
465 |
pp_print_string fmt m.mname.node_id))
|
|
466 |
machines;
|
|
467 |
assert false |
|
468 |
|
|
453 | 469 |
let get_const_assign m id = |
454 | 470 |
try |
455 |
match get_instr_desc (List.find |
|
456 |
(fun instr -> match get_instr_desc instr with |
|
457 |
| MLocalAssign (v, _) -> v == id |
|
458 |
| _ -> false) |
|
459 |
m.mconst |
|
460 |
) with |
|
461 |
| MLocalAssign (_, e) -> e |
|
462 |
| _ -> assert false |
|
471 |
match |
|
472 |
get_instr_desc |
|
473 |
(List.find |
|
474 |
(fun instr -> |
|
475 |
match get_instr_desc instr with |
|
476 |
| MLocalAssign (v, _) -> |
|
477 |
v == id |
|
478 |
| _ -> |
|
479 |
false) |
|
480 |
m.mconst) |
|
481 |
with |
|
482 |
| MLocalAssign (_, e) -> |
|
483 |
e |
|
484 |
| _ -> |
|
485 |
assert false |
|
463 | 486 |
with Not_found -> assert false |
464 | 487 |
|
465 |
|
|
466 | 488 |
let value_of_ident loc m id = |
467 | 489 |
(* is is a state var *) |
468 | 490 |
try |
469 |
let v = List.find (fun v -> v.var_id = id) m.mmemory |
|
470 |
in mk_val (Var v) v.var_type |
|
471 |
with Not_found -> |
|
472 |
try (* id is a node var *) |
|
473 |
let v = get_node_var id m.mname |
|
474 |
in mk_val (Var v) v.var_type |
|
475 |
with Not_found -> |
|
476 |
try (* id is a constant *) |
|
477 |
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |
|
478 |
in mk_val (Var c) c.var_type |
|
479 |
with Not_found -> |
|
480 |
(* id is a tag *) |
|
481 |
let t = Const_tag id |
|
482 |
in mk_val (Cst t) (Typing.type_const loc t) |
|
491 |
let v = List.find (fun v -> v.var_id = id) m.mmemory in |
|
492 |
mk_val (Var v) v.var_type |
|
493 |
with Not_found -> ( |
|
494 |
try |
|
495 |
(* id is a node var *) |
|
496 |
let v = get_node_var id m.mname in |
|
497 |
mk_val (Var v) v.var_type |
|
498 |
with Not_found -> ( |
|
499 |
try |
|
500 |
(* id is a constant *) |
|
501 |
let c = |
|
502 |
Corelang.var_decl_of_const |
|
503 |
(const_of_top (Hashtbl.find Corelang.consts_table id)) |
|
504 |
in |
|
505 |
mk_val (Var c) c.var_type |
|
506 |
with Not_found -> |
|
507 |
(* id is a tag *) |
|
508 |
let t = Const_tag id in |
|
509 |
mk_val (Cst t) (Typing.type_const loc t))) |
|
483 | 510 |
|
484 | 511 |
(* type of internal fun used in dimension expression *) |
485 | 512 |
let type_of_value_appl f args = |
486 |
if List.mem f Basic_library.arith_funs |
|
487 |
then (List.hd args).value_type |
|
513 |
if List.mem f Basic_library.arith_funs then (List.hd args).value_type |
|
488 | 514 |
else Type_predef.type_bool |
489 | 515 |
|
490 | 516 |
let rec value_of_dimension m dim = |
491 | 517 |
match dim.Dimension.dim_desc with |
492 |
| Dimension.Dbool b -> |
|
493 |
mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool |
|
494 |
| Dimension.Dint i -> |
|
495 |
mk_val (Cst (Const_int i)) Type_predef.type_int |
|
496 |
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v |
|
518 |
| Dimension.Dbool b -> |
|
519 |
mk_val |
|
520 |
(Cst (Const_tag (if b then tag_true else tag_false))) |
|
521 |
Type_predef.type_bool |
|
522 |
| Dimension.Dint i -> |
|
523 |
mk_val (Cst (Const_int i)) Type_predef.type_int |
|
524 |
| Dimension.Dident v -> |
|
525 |
value_of_ident dim.Dimension.dim_loc m v |
|
497 | 526 |
| Dimension.Dappl (f, args) -> |
498 |
let vargs = List.map (value_of_dimension m) args |
|
499 |
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
|
500 |
| Dimension.Dite (i, t, e) -> |
|
501 |
(match List.map (value_of_dimension m) [i; t; e] with |
|
502 |
| [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type |
|
503 |
| _ -> assert false) |
|
504 |
| Dimension.Dlink dim' -> value_of_dimension m dim' |
|
505 |
| _ -> assert false |
|
527 |
let vargs = List.map (value_of_dimension m) args in |
|
528 |
mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
|
529 |
| Dimension.Dite (i, t, e) -> ( |
|
530 |
match List.map (value_of_dimension m) [ i; t; e ] with |
|
531 |
| [ vi; vt; ve ] -> |
|
532 |
mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type |
|
533 |
| _ -> |
|
534 |
assert false) |
|
535 |
| Dimension.Dlink dim' -> |
|
536 |
value_of_dimension m dim' |
|
537 |
| _ -> |
|
538 |
assert false |
|
506 | 539 |
|
507 | 540 |
let rec dimension_of_value value = |
508 | 541 |
match value.value_desc with |
509 |
| Cst (Const_tag t) when t = tag_true -> Dimension.mkdim_bool Location.dummy_loc true |
|
510 |
| Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool Location.dummy_loc false |
|
511 |
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i |
|
512 |
| Var v -> Dimension.mkdim_ident Location.dummy_loc v.var_id |
|
513 |
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) |
|
514 |
| _ -> assert false |
|
515 |
|
|
542 |
| Cst (Const_tag t) when t = tag_true -> |
|
543 |
Dimension.mkdim_bool Location.dummy_loc true |
|
544 |
| Cst (Const_tag t) when t = tag_false -> |
|
545 |
Dimension.mkdim_bool Location.dummy_loc false |
|
546 |
| Cst (Const_int i) -> |
|
547 |
Dimension.mkdim_int Location.dummy_loc i |
|
548 |
| Var v -> |
|
549 |
Dimension.mkdim_ident Location.dummy_loc v.var_id |
|
550 |
| Fun (f, args) -> |
|
551 |
Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) |
|
552 |
| _ -> |
|
553 |
assert false |
|
516 | 554 |
|
517 | 555 |
let rec join_branches hl1 hl2 = |
518 |
match hl1, hl2 with |
|
519 |
| [] , _ -> hl2 |
|
520 |
| _ , [] -> hl1 |
|
521 |
| (t1, h1)::q1, (t2, h2)::q2 -> |
|
522 |
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else |
|
523 |
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
|
524 |
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
|
556 |
match hl1, hl2 with |
|
557 |
| [], _ -> |
|
558 |
hl2 |
|
559 |
| _, [] -> |
|
560 |
hl1 |
|
561 |
| (t1, h1) :: q1, (t2, h2) :: q2 -> |
|
562 |
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 |
|
563 |
else if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
|
564 |
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
|
525 | 565 |
|
526 | 566 |
and join_guards inst1 insts2 = |
527 |
match get_instr_desc inst1, insts2 with |
|
528 |
| MBranch (x1, hl1), |
|
529 |
({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 |
|
530 |
when x1 = x2 -> |
|
531 |
mkinstr |
|
532 |
~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2) |
|
533 |
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) |
|
534 |
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) |
|
535 |
:: insts2 |
|
536 |
| _ -> inst1 :: insts2 |
|
537 |
|
|
538 |
let join_guards_list insts = |
|
539 |
List.fold_right join_guards insts [] |
|
567 |
match get_instr_desc inst1, insts2 with |
|
568 |
| ( MBranch (x1, hl1), |
|
569 |
({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 ) |
|
570 |
when x1 = x2 -> |
|
571 |
mkinstr |
|
572 |
~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2) |
|
573 |
(* TODO on pourrait uniquement concatener les lustres de inst1 et |
|
574 |
hd(inst2) *) |
|
575 |
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) |
|
576 |
:: insts2 |
|
577 |
| _ -> |
|
578 |
inst1 :: insts2 |
|
579 |
|
|
580 |
let join_guards_list insts = List.fold_right join_guards insts [] |
Also available in: Unified diff
reformatting