From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: 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 --- backend/Mach.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'backend/Mach.v') 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 -- cgit