diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-29 23:01:15 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-29 23:01:15 +0200 |
commit | 4aad20a92dc926d8c537e65946ca03bf2b6b02b9 (patch) | |
tree | 5e6e2efa225fba853468bde1f7213de4a5861a3b /backend | |
parent | 07f2bfbd62568e2e0d983ccb33d020bf6985e874 (diff) | |
download | compcert-kvx-4aad20a92dc926d8c537e65946ca03bf2b6b02b9.tar.gz compcert-kvx-4aad20a92dc926d8c537e65946ca03bf2b6b02b9.zip |
begin coding dead code injector
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Inject.v | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/backend/Inject.v b/backend/Inject.v new file mode 100644 index 00000000..dd70556a --- /dev/null +++ b/backend/Inject.v @@ -0,0 +1,60 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Inductive inj_instr : Type := + | INJop: operation -> list reg -> reg -> inj_instr + | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. + +Definition inject_instr (i : inj_instr) (pc' : node) : instruction := + match i with + | INJop op args dst => Iop op args dst pc' + | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc' + end. + +Fixpoint inject_list (prog : code) (pc : node) (dst : node) + (l : list inj_instr) : node * code := + let pc' := Pos.succ pc in + match l with + | nil => (pc', PTree.set pc (Inop dst) prog) + | h::t => + inject_list (PTree.set pc (inject_instr h pc') prog) + pc' dst t + end. + +Definition successor (i : instruction) : node := + match i with + | Inop pc' => pc' + | Iop _ _ _ pc' => pc' + | Iload _ _ _ _ _ pc' => pc' + | Istore _ _ _ _ pc' => pc' + | Icall _ _ _ _ pc' => pc' + | Ibuiltin _ _ _ pc' => pc' + | Icond _ _ pc' _ => pc' + | Itailcall _ _ _ + | Ijumptable _ _ + | Ireturn _ => 1%positive + end. + +Definition alter_successor (i : instruction) (pc' : node) : instruction := + match i with + | Inop _ => Inop pc' + | Iop op args dst _ => Iop op args dst pc' + | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc' + | Istore chunk addr args src _ => Istore chunk addr args src pc' + | Icall sig ri args dst _ => Icall sig ri args dst pc' + | Ibuiltin ef args res _ => Ibuiltin ef args res pc' + | Icond cond args _ pc2 => Icond cond args pc' pc2 + | Itailcall _ _ _ + | Ijumptable _ _ + | Ireturn _ => i + end. + +Definition inject_at (prog : code) (pc extra_pc : node) + (l : list inj_instr) : node * code := + match PTree.get pc prog with + | Some i => + inject_list (PTree.set pc (alter_successor i extra_pc) prog) + extra_pc (successor i) l + | None => inject_list prog extra_pc 1%positive l (* does not happen *) + end. |