Revised Stacking and Asmgen passes and Mach semantics:

- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
  fill this hole with the return address in the Asmgen proof.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 33 insertions, 0 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index a78c8bf..87d9dc9 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -68,6 +68,10 @@ Coercion IR: ireg >-> preg.
 Coercion FR: freg >-> preg.
 Coercion CR: crbit >-> preg.
 
+(** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
+
+Notation "'SP'" := ESP (only parsing).
+
 (** ** Instruction set. *)
 
 Definition label := positive.
@@ -197,6 +201,8 @@ with annot_param : Type :=
   | APstack: memory_chunk -> Z -> annot_param.
 
 Definition code := list instruction.
+Definition function := code.
+Definition fn_code (f: function) : code := f.
 Definition fundef := AST.fundef code.
 Definition program := AST.program fundef unit.
 
@@ -863,3 +869,30 @@ Ltac Equalities :=
 (* final states *)
   inv H; inv H0. congruence.
 Qed.
+
+(** Classification functions for processor registers (used in Asmgenproof). *)
+
+Definition data_preg (r: preg) : bool :=
+  match r with
+  | PC => false
+  | IR _ => true
+  | FR _ => true
+  | ST0 => true
+  | CR _ => false
+  | RA => false
+  end.
+
+Definition nontemp_preg (r: preg) : bool :=
+  match r with
+  | PC => false
+  | IR ECX => false
+  | IR EDX => false
+  | IR _ => true
+  | FR XMM6 => false
+  | FR XMM7 => false
+  | FR _ => true
+  | ST0 => false
+  | CR _ => false
+  | RA => false
+  end.
+