Revision 1b721bfd
Added by Pierre-Loïc Garoche almost 6 years ago
| src/backends/EMF/EMF_backend.ml | ||
|---|---|---|
| 154 | 154 |
|
| 155 | 155 |
let rec branch_block_vars il = |
| 156 | 156 |
List.fold_left |
| 157 |
(fun (accu_def, accu_read) i -> |
|
| 158 |
let defined_vars, read_vars = branch_instr_vars i in |
|
| 159 |
ISet.union accu_def defined_vars, VSet.union accu_read read_vars) |
|
| 160 |
(ISet.empty, VSet.empty) il |
|
| 157 |
(fun (accu_all_def, accu_def, accu_read) i -> |
|
| 158 |
let all_defined_vars, common_def_vars, read_vars = branch_instr_vars i in |
|
| 159 |
ISet.union accu_all_def all_defined_vars, |
|
| 160 |
ISet.union accu_def common_def_vars, |
|
| 161 |
VSet.union accu_read read_vars) |
|
| 162 |
(ISet.empty, ISet.empty, VSet.empty) il |
|
| 161 | 163 |
and branch_instr_vars i = |
| 162 | 164 |
match Corelang.get_instr_desc i with |
| 163 | 165 |
| MLocalAssign (var,expr) |
| 164 |
| MStateAssign (var,expr) -> ISet.singleton var.var_id, get_expr_vars expr |
|
| 166 |
| MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
|
|
| 165 | 167 |
| MStep (vars, _, args) -> |
| 166 |
ISet.of_list (List.map (fun v -> v.var_id) vars), |
|
| 167 |
List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args |
|
| 168 |
let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in |
|
| 169 |
lhs, lhs, |
|
| 170 |
List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args |
|
| 168 | 171 |
| MBranch (g,(_,hd_il)::tl) -> (* We focus on variables defined in all branches *) |
| 169 | 172 |
let read_guard = get_expr_vars g in |
| 170 |
let def_vars_hd, read_vars_hd = branch_block_vars hd_il in |
|
| 171 |
let def_vars, read_vars = |
|
| 173 |
let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars hd_il in
|
|
| 174 |
let all_def_vars, def_vars, read_vars =
|
|
| 172 | 175 |
List.fold_left |
| 173 |
(fun (def_vars, read_vars) (_, il) -> |
|
| 176 |
(fun (all_def_vars, def_vars, read_vars) (_, il) ->
|
|
| 174 | 177 |
(* We accumulate reads but intersect writes *) |
| 175 |
let writes_il, reads_il = branch_block_vars il in |
|
| 178 |
let all_writes_il, writes_il, reads_il = branch_block_vars il in |
|
| 179 |
ISet.union all_def_vars all_writes_il, |
|
| 176 | 180 |
ISet.inter def_vars writes_il, |
| 177 |
VSet.union read_vars reads_il |
|
| 181 |
VSet.union read_vars reads_il
|
|
| 178 | 182 |
) |
| 179 |
(def_vars_hd, read_vars_hd) |
|
| 183 |
(all_def_vars_hd, def_vars_hd, read_vars_hd)
|
|
| 180 | 184 |
tl |
| 181 | 185 |
in |
| 182 |
def_vars, VSet.union read_guard read_vars |
|
| 186 |
all_def_vars, def_vars, VSet.union read_guard read_vars
|
|
| 183 | 187 |
| MBranch _ -> assert false (* branch instruction should admit at least one case *) |
| 184 | 188 |
| MReset ni |
| 185 |
| MNoReset ni -> ISet.singleton (reset_name ni), VSet.empty |
|
| 189 |
| MNoReset ni -> |
|
| 190 |
let write = ISet.singleton (reset_name ni) in |
|
| 191 |
write, write, VSet.empty |
|
| 186 | 192 |
| MComment _ -> assert false (* not available for EMF output *) |
| 187 | 193 |
|
| 188 | 194 |
|
| ... | ... | |
| 231 | 237 |
) |
| 232 | 238 |
|
| 233 | 239 |
| MBranch (g, hl) -> ( |
| 234 |
let outputs, inputs = branch_instr_vars i in |
|
| 240 |
let all_outputs, outputs, inputs = branch_instr_vars i in |
|
| 241 |
Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." |
|
| 242 |
Machine_code.pp_instr i |
|
| 243 |
(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) |
|
| 244 |
(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) |
|
| 245 |
pp_emf_vars_decl |
|
| 246 |
(VSet.elements inputs) |
|
| 247 |
|
|
| 248 |
; |
|
| 249 |
let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in |
|
| 250 |
Format.eprintf "Filtering in: %a@.@." |
|
| 251 |
pp_emf_vars_decl |
|
| 252 |
(VSet.elements inputs) |
|
| 253 |
|
|
| 254 |
; |
|
| 235 | 255 |
fprintf fmt "\"kind\": \"branch\",@ "; |
| 236 | 256 |
fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *) |
| 237 | 257 |
fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs); |
| ... | ... | |
| 244 | 264 |
fprintf fmt "@[<v 2>\"branches\": {@ %a@]}@ "
|
| 245 | 265 |
(fprintf_list ~sep:",@ " |
| 246 | 266 |
(fun fmt (tag, instrs_tag) -> |
| 247 |
let (*branch_outputs*) _, branch_inputs = branch_block_vars instrs_tag in |
|
| 267 |
let branch_all_lhs, _, branch_inputs = branch_block_vars instrs_tag in |
|
| 268 |
let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in |
|
| 248 | 269 |
fprintf fmt "@[<v 2>\"%s\": {@ " tag;
|
| 249 | 270 |
fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; |
| 250 | 271 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); |
Also available in: Unified diff
bug fixed: Inputs for branches solved