Revision 75c459f4
Added by Lélio Brun about 2 years ago
| src/machine_code_common.ml | ||
|---|---|---|
| 1 | 1 |
open Lustre_types |
| 2 | 2 |
open Machine_code_types |
| 3 |
open Spec_types |
|
| 4 |
open Spec_common |
|
| 3 | 5 |
open Corelang |
| 4 | 6 |
|
| 5 | 7 |
let print_statelocaltag = true |
| ... | ... | |
| 153 | 155 |
let is_output m id = |
| 154 | 156 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs |
| 155 | 157 |
|
| 158 |
let get_instr_spec i = i.instr_spec |
|
| 156 | 159 |
|
| 157 | 160 |
let mk_conditional ?lustre_eq c t e = |
| 158 |
mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ])) |
|
| 159 |
|
|
| 160 |
|
|
| 161 |
mkinstr ?lustre_eq |
|
| 162 |
(Ternary (Val c, |
|
| 163 |
And (List.map get_instr_spec t), |
|
| 164 |
And (List.map get_instr_spec e))) |
|
| 165 |
(MBranch(c, [ |
|
| 166 |
(tag_true, t); |
|
| 167 |
(tag_false, e) ])) |
|
| 168 |
|
|
| 169 |
let mk_branch ?lustre_eq c br = |
|
| 170 |
mkinstr ?lustre_eq |
|
| 171 |
(And (List.map (fun (l, instrs) -> |
|
| 172 |
Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs))) |
|
| 173 |
br)) |
|
| 174 |
(MBranch (c, br)) |
|
| 175 |
|
|
| 176 |
let mk_assign ?lustre_eq x v = |
|
| 177 |
mkinstr ?lustre_eq |
|
| 178 |
(Equal (Var x, Val v)) |
|
| 179 |
(MLocalAssign (x, v)) |
|
| 161 | 180 |
|
| 162 | 181 |
let mk_val v t = |
| 163 | 182 |
{ value_desc = v;
|
| ... | ... | |
| 178 | 197 |
mmemory = [var_state]; |
| 179 | 198 |
mcalls = []; |
| 180 | 199 |
minstances = []; |
| 181 |
minit = [mkinstr (MStateAssign(var_state, cst true))]; |
|
| 200 |
minit = [mkinstr True (MStateAssign(var_state, cst true))];
|
|
| 182 | 201 |
mstatic = []; |
| 183 | 202 |
mconst = []; |
| 184 | 203 |
mstep = {
|
| ... | ... | |
| 187 | 206 |
step_locals = []; |
| 188 | 207 |
step_checks = []; |
| 189 | 208 |
step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool) |
| 190 |
(List.map mkinstr
|
|
| 209 |
(List.map (mkinstr True)
|
|
| 191 | 210 |
[MStateAssign(var_state, cst false); |
| 192 | 211 |
MLocalAssign(var_output, mk_val (Var var_input1) t_arg)]) |
| 193 |
(List.map mkinstr
|
|
| 212 |
(List.map (mkinstr True)
|
|
| 194 | 213 |
[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ]; |
| 195 | 214 |
step_asserts = []; |
| 196 | 215 |
}; |
| ... | ... | |
| 354 | 373 |
| _ , [] -> |
| 355 | 374 |
[inst1] |
| 356 | 375 |
| MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 -> |
| 357 |
mkinstr |
|
| 376 |
mkinstr True
|
|
| 358 | 377 |
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) |
| 359 | 378 |
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) |
| 360 | 379 |
:: (List.tl insts2) |
Also available in: Unified diff
start with Spec AST generation