diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-10 09:40:04 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-10 09:40:04 +0000 |
commit | 3b24f0e0404de0c2c5b1cf64d5a5d6059cd604b6 (patch) | |
tree | 72b1df72ecb879939bd963dc6077cea92792e0d4 | |
parent | 538f7ad4feabf9eafe00788ef3a2b65a379d3ee1 (diff) | |
download | compcert-3b24f0e0404de0c2c5b1cf64d5a5d6059cd604b6.tar.gz compcert-3b24f0e0404de0c2c5b1cf64d5a5d6059cd604b6.zip |
Define useful functions instr_defs and instr_uses
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | backend/RTL.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index 9b27a172..838cf0a8 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -387,6 +387,41 @@ Definition successors_instr (i: instruction) : list node := Definition successors (f: function) : PTree.t (list node) := PTree.map1 successors_instr f.(fn_code). +(** The registers used by an instruction *) + +Definition instr_uses (i: instruction) : list reg := + match i with + | Inop s => nil + | Iop op args res s => args + | Iload chunk addr args dst s => args + | Istore chunk addr args src s => src :: args + | Icall sig (inl r) args res s => r :: args + | Icall sig (inr id) args res s => args + | Itailcall sig (inl r) args => r :: args + | Itailcall sig (inr id) args => args + | Ibuiltin ef args res s => args + | Icond cond args ifso ifnot => args + | Ijumptable arg tbl => arg :: nil + | Ireturn None => nil + | Ireturn (Some arg) => arg :: nil + end. + +(** The register defined by an instruction, if any *) + +Definition instr_defs (i: instruction) : option reg := + match i with + | Inop s => None + | Iop op args res s => Some res + | Iload chunk addr args dst s => Some dst + | Istore chunk addr args src s => None + | Icall sig ros args res s => Some res + | Itailcall sig ros args => None + | Ibuiltin ef args res s => Some res + | Icond cond args ifso ifnot => None + | Ijumptable arg tbl => None + | Ireturn optarg => None + end. + (** Transformation of a RTL function instruction by instruction. This applies a given transformation function to all instructions of a function and constructs a transformed function from that. *) |