diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /backend/Mach.v | |
parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) | |
download | compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.tar.gz compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.zip |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Mach.v')
-rw-r--r-- | backend/Mach.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/backend/Mach.v b/backend/Mach.v index 2ec312e4..c6a692a1 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -27,6 +27,7 @@ Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. +Require Import Conventions. (** * Abstract syntax *) @@ -101,6 +102,21 @@ Definition regset := Regmap.t val. Notation "a ## b" := (List.map a b) (at level 1). Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level). +Fixpoint undef_regs (rl: list mreg) (rs: regset) {struct rl} : regset := + match rl with + | nil => rs + | r1 :: rl' => undef_regs rl' (Regmap.set r1 Vundef rs) + end. + +Definition undef_temps (rs: regset) := + undef_regs (int_temporaries ++ float_temporaries) rs. + +Definition undef_op (op: operation) (rs: regset) := + match op with + | Omove => rs + | _ => undef_temps rs + end. + Definition is_label (lbl: label) (instr: instruction) : bool := match instr with | Mlabel lbl' => if peq lbl lbl' then true else false |