diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-10 19:25:47 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-10 19:25:47 +0200 |
| commit | b44d87ef03279cb479101d7b02031cf78136062d (patch) | |
| tree | 04efb96fa7176398f25654c1cd029f51d7f84087 /kvx | |
| parent | fe7e30495c1690068e1df8aded85404299aaf329 (diff) | |
| download | compcert-kvx-b44d87ef03279cb479101d7b02031cf78136062d.tar.gz compcert-kvx-b44d87ef03279cb479101d7b02031cf78136062d.zip | |
oracle super restrictif
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/PrepassSchedulingOracle.ml | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/kvx/lib/PrepassSchedulingOracle.ml b/kvx/lib/PrepassSchedulingOracle.ml index b83078f8..322dff85 100644 --- a/kvx/lib/PrepassSchedulingOracle.ml +++ b/kvx/lib/PrepassSchedulingOracle.ml @@ -132,11 +132,13 @@ let get_simple_dependencies (seqa : (instruction*Regset.t) array) = match insn with | Inop _ -> () | Iop(op, inputs, output, _) -> - (if Op.is_trapping_op op then set_branch i); + (* (if Op.is_trapping_op op then set_branch i); *) + set_branch i; add_input_regs i inputs; add_output_reg i (latency_of_op op (List.length inputs)) output | Iload(trap, chunk, addressing, addr_regs, output, _) -> - (if trap=TRAP then set_branch i); + set_branch i; + (* (if trap=TRAP then set_branch i); *) add_input_mem i; add_input_regs i addr_regs; add_output_reg i (latency_of_load trap chunk addressing (List.length addr_regs)) output @@ -154,7 +156,8 @@ let get_simple_dependencies (seqa : (instruction*Regset.t) array) = add_input_mem i; add_input_regs i inputs; add_output_reg i (latency_of_call signature ef) output; - add_output_mem i + add_output_mem i; + failwith "Icall" | Itailcall(signature, ef, inputs) -> set_branch i; (match ef with @@ -162,24 +165,29 @@ let get_simple_dependencies (seqa : (instruction*Regset.t) array) = | Datatypes.Coq_inr symbol -> () ); add_input_mem i; - add_input_regs i inputs + add_input_regs i inputs; + failwith "Itailcall" | Ibuiltin(ef, builtin_inputs, builtin_output, _) -> set_branch i; add_input_mem i; List.iter (add_builtin_arg i) builtin_inputs; add_builtin_res i builtin_output; - add_output_mem i + add_output_mem i; + failwith "Ibuiltin" | Icond(cond, inputs, _, _, _) -> set_branch i; add_input_regs i inputs | Ijumptable(input, _) -> set_branch i; - add_input_reg i input + add_input_reg i input; + failwith "Ijumptable" | Ireturn(Some input) -> set_branch i; - add_input_reg i input + add_input_reg i input; + failwith "Ireturn" | Ireturn(None) -> - set_branch i + set_branch i; + failwith "Ireturn none" end seqa; !latency_constraints;; |