Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64

Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.

This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true).  Unlike previous approaches, no other file is duplicated between these two variants of x86.

While we are at it, I renamed "ia32" into "x86" everywhere.  "ia32" is Intel speak for the 32-bit architecture.  It is not a good name to describe both the 32 and 64 bit architectures.

Finally, .depend is no longer under version control and is regenerated when the target architecture changes.  That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).

1 files changed, 367 insertions, 0 deletions

diff --git a/x86/Machregs.v b/x86/Machregs.v
new file mode 100644
index 00000000..741081a6
--- /dev/null
+++ b/x86/Machregs.v
@@ -0,0 +1,367 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import String.
+Require Import Coqlib.
+Require Import Decidableplus.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Op.
+
+(** ** Machine registers *)
+
+(** The following type defines the machine registers that can be referenced
+  as locations.  These include:
+- Integer registers that can be allocated to RTL pseudo-registers.
+- Floating-point registers that can be allocated to RTL pseudo-registers.
+- The special [FP0] register denoting the top of the X87 float stack.
+
+  The type [mreg] does not include special-purpose or reserved
+  machine registers such as the stack pointer and the condition codes. *)
+
+Inductive mreg: Type :=
+  (** Allocatable integer regs *)
+  | AX | BX | CX | DX | SI | DI | BP
+  | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15  (**r only in 64-bit mode *)
+  (** Allocatable float regs *)
+  | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7
+  | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15  (**r only in 64-bit mode *)
+  (** Special float reg *)
+  | FP0.
+
+Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
+Proof. decide equality. Defined.
+Global Opaque mreg_eq.
+
+Definition all_mregs :=
+     AX :: BX :: CX :: DX :: SI :: DI :: BP
+  :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15
+  :: X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7
+  :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15
+  :: FP0 :: nil.
+
+Lemma all_mregs_complete:
+  forall (r: mreg), In r all_mregs.
+Proof.
+  assert (forall r, proj_sumbool (In_dec mreg_eq r all_mregs) = true) by (destruct r; reflexivity).
+  intros. specialize (H r). InvBooleans. auto.
+Qed.
+
+Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+  
+Instance Finite_mreg : Finite mreg := {
+  Finite_elements := all_mregs;
+  Finite_elements_spec := all_mregs_complete
+}.
+
+Definition mreg_type (r: mreg): typ :=
+  match r with
+  | AX | BX | CX | DX | SI | DI | BP => if Archi.ptr64 then Tany64 else Tany32
+  | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => Tany64
+  | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => Tany64
+  | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Tany64
+  | FP0 => Tany64
+  end.
+
+Local Open Scope positive_scope.
+
+Module IndexedMreg <: INDEXED_TYPE.
+  Definition t := mreg.
+  Definition eq := mreg_eq.
+  Definition index (r: mreg): positive :=
+    match r with
+    | AX => 1 | BX => 2 | CX => 3 | DX => 4 | SI => 5 | DI => 6 | BP => 7
+    | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11 | R12 => 12 | R13 => 13 | R14 => 14 | R15 => 15
+    | X0 => 16 | X1 => 17 | X2 => 18 | X3 => 19 | X4 => 20 | X5 => 21 | X6 => 22 | X7 => 23
+    | X8 => 24 | X9 => 25 | X10 => 26 | X11 => 27 | X12 => 28 | X13 => 29 | X14 => 30 | X15 => 31
+    | FP0 => 32
+    end.
+  Lemma index_inj:
+    forall r1 r2, index r1 = index r2 -> r1 = r2.
+  Proof.
+    decide_goal.
+  Qed.
+End IndexedMreg.
+
+Definition is_stack_reg (r: mreg) : bool :=
+  match r with FP0 => true | _ => false end.
+
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("RAX", AX) :: ("RBX", BX) :: ("RCX", CX) :: ("RDX", DX) ::
+  ("RSI", SI) :: ("RDI", DI) :: ("RBP", BP) ::
+  ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) ::
+  ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) ::
+  ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: ("R11", R11) ::
+  ("R12", R12) :: ("R13", R13) :: ("R14", R14) :: ("R15", R15) ::
+  ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) ::
+  ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) ::
+  ("XMM8", X8) :: ("XMM9", X9) :: ("XMM10", X10) :: ("XMM11", X11) ::
+  ("XMM12", X12) :: ("XMM13", X13) :: ("XMM14", X14) :: ("XMM15", X15) ::
+  ("ST0", FP0) :: nil.
+
+Definition register_by_name (s: string) : option mreg :=
+  let fix assoc (l: list (string * mreg)) : option mreg :=
+    match l with
+    | nil => None
+    | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l'
+    end
+  in assoc register_names.
+
+(** ** Destroyed registers, preferred registers *)
+
+Definition destroyed_by_op (op: operation): list mreg :=
+  match op with
+  | Ocast8signed | Ocast8unsigned => AX :: nil
+  | Omulhs => AX :: DX :: nil
+  | Omulhu => AX :: DX :: nil
+  | Odiv => AX :: DX :: nil
+  | Odivu => AX :: DX :: nil
+  | Omod => AX :: DX :: nil
+  | Omodu => AX :: DX :: nil
+  | Oshrximm _ => CX :: nil
+  | Omullhs => AX :: DX :: nil
+  | Omullhu => AX :: DX :: nil
+  | Odivl => AX :: DX :: nil
+  | Odivlu => AX :: DX :: nil
+  | Omodl => AX :: DX :: nil
+  | Omodlu => AX :: DX :: nil
+  | Oshrxlimm _ => DX :: nil
+  | Ocmp _ => AX :: CX :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg :=
+  nil.
+
+Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
+  match chunk with
+  | Mint8signed | Mint8unsigned => if Archi.ptr64 then nil else AX :: CX :: nil
+  | _ => nil
+  end. 
+
+Definition destroyed_by_cond (cond: condition): list mreg :=
+  nil.
+
+Definition destroyed_by_jumptable: list mreg :=
+  AX :: DX :: nil.
+
+Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
+  match cl with
+  | nil => nil
+  | c1 :: cl =>
+      match register_by_name c1 with
+      | Some r => r :: destroyed_by_clobber cl
+      | None   => destroyed_by_clobber cl
+      end
+  end.
+
+Definition destroyed_by_builtin (ef: external_function): list mreg :=
+  match ef with
+  | EF_memcpy sz al =>
+      if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil
+  | EF_vstore (Mint8unsigned|Mint8signed) =>
+      if Archi.ptr64 then nil else AX :: CX :: nil
+  | EF_builtin name sg =>
+      if string_dec name "__builtin_va_start" then AX :: nil
+      else if string_dec name "__builtin_write16_reversed"
+           || string_dec name "__builtin_write32_reversed"
+      then CX :: DX :: nil
+      else nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
+  | _ => nil
+  end.
+
+Definition destroyed_at_function_entry: list mreg :=
+  (* must include [destroyed_by_setstack ty] *)
+  AX :: FP0 :: nil.
+
+Definition destroyed_by_setstack (ty: typ): list mreg :=
+  match ty with
+  | Tfloat | Tsingle => FP0 :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_at_indirect_call: list mreg :=
+  nil.
+
+Definition temp_for_parent_frame: mreg :=
+  AX.
+
+Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
+  match op with
+  | Omulhs => (Some AX :: None :: nil, Some DX)
+  | Omulhu => (Some AX :: None :: nil, Some DX)
+  | Odiv => (Some AX :: Some CX :: nil, Some AX)
+  | Odivu => (Some AX :: Some CX :: nil, Some AX)
+  | Omod => (Some AX :: Some CX :: nil, Some DX)
+  | Omodu => (Some AX :: Some CX :: nil, Some DX)
+  | Oshl => (None :: Some CX :: nil, None)
+  | Oshr => (None :: Some CX :: nil, None)
+  | Oshru => (None :: Some CX :: nil, None)
+  | Oshrximm _ => (Some AX :: nil, Some AX)
+  | Omullhs => (Some AX :: None :: nil, Some DX)
+  | Omullhu => (Some AX :: None :: nil, Some DX)
+  | Odivl => (Some AX :: Some CX :: nil, Some AX)
+  | Odivlu => (Some AX :: Some CX :: nil, Some AX)
+  | Omodl => (Some AX :: Some CX :: nil, Some DX)
+  | Omodlu => (Some AX :: Some CX :: nil, Some DX)
+  | Oshll => (None :: Some CX :: nil, None)
+  | Oshrl => (None :: Some CX :: nil, None)
+  | Oshrlu => (None :: Some CX :: nil, None)
+  | Oshrxlimm _ => (Some AX :: nil, Some AX)
+  | _ => (nil, None)
+  end.
+
+Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
+  match ef with
+  | EF_memcpy sz al =>
+     if zle sz 32 then (Some AX :: Some DX :: nil, nil) else (Some DI :: Some SI :: nil, nil)
+  | EF_builtin name sg =>
+     if string_dec name "__builtin_negl" then
+       (Some DX :: Some AX :: nil, Some DX :: Some AX :: nil)
+     else if string_dec name "__builtin_addl"
+          || string_dec name "__builtin_subl" then
+       (Some DX :: Some AX :: Some CX :: Some BX :: nil, Some DX :: Some AX :: nil)
+     else if string_dec name "__builtin_mull" then
+       (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil)
+     else if string_dec name "__builtin_va_start" then
+       (Some DX :: nil, nil)
+     else if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then
+       (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil)
+     else
+       (nil, nil)
+  | _ => (nil, nil)
+  end.
+
+Global Opaque
+    destroyed_by_op destroyed_by_load destroyed_by_store
+    destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
+    destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
+    mregs_for_operation mregs_for_builtin.
+
+(** Two-address operations.  Return [true] if the first argument and
+  the result must be in the same location *and* are unconstrained
+  by [mregs_for_operation]. *)
+
+Definition two_address_op (op: operation) : bool :=
+  match op with
+  | Omove => false
+  | Ointconst _ => false
+  | Olongconst _ => false
+  | Ofloatconst _ => false
+  | Osingleconst _ => false
+  | Oindirectsymbol _ => false
+  | Ocast8signed => false
+  | Ocast8unsigned => false
+  | Ocast16signed => false
+  | Ocast16unsigned => false
+  | Oneg => true
+  | Osub => true
+  | Omul => true
+  | Omulimm _ => true
+  | Omulhs => false
+  | Omulhu => false
+  | Odiv => false
+  | Odivu => false
+  | Omod => false
+  | Omodu => false
+  | Oand => true
+  | Oandimm _ => true
+  | Oor => true
+  | Oorimm _ => true
+  | Oxor => true
+  | Oxorimm _ => true
+  | Onot => true
+  | Oshl => true
+  | Oshlimm _ => true
+  | Oshr => true
+  | Oshrimm _ => true
+  | Oshrximm _ => false
+  | Oshru => true
+  | Oshruimm _ => true
+  | Ororimm _ => true
+  | Oshldimm _ => true
+  | Olea addr => false
+  | Omakelong => true
+  | Olowlong => true
+  | Ohighlong => true
+  | Ocast32signed => false
+  | Ocast32unsigned => false
+  | Onegl => true
+  | Oaddlimm _ => true
+  | Osubl => true
+  | Omull => true
+  | Omullimm _ => true
+  | Omullhs => false
+  | Omullhu => false
+  | Odivl => false
+  | Odivlu => false
+  | Omodl => false
+  | Omodlu => false
+  | Oandl => true
+  | Oandlimm _ => true
+  | Oorl => true
+  | Oorlimm _ => true
+  | Oxorl => true
+  | Oxorlimm _ => true
+  | Onotl => true
+  | Oshll => true
+  | Oshllimm _ => true
+  | Oshrl => true
+  | Oshrlimm _ => true
+  | Oshrxlimm _ => false
+  | Oshrlu => true
+  | Oshrluimm _ => true
+  | Ororlimm _ => true
+  | Oleal addr => false
+  | Onegf => true
+  | Oabsf => true
+  | Oaddf => true
+  | Osubf => true
+  | Omulf => true
+  | Odivf => true
+  | Onegfs => true
+  | Oabsfs => true
+  | Oaddfs => true
+  | Osubfs => true
+  | Omulfs => true
+  | Odivfs => true
+  | Osingleoffloat => false
+  | Ofloatofsingle => false
+  | Ointoffloat => false
+  | Ofloatofint => false
+  | Ointofsingle => false
+  | Osingleofint => false
+  | Olongoffloat => false
+  | Ofloatoflong => false
+  | Olongofsingle => false
+  | Osingleoflong => false
+  | Ocmp c => false
+  end.
+
+(* Constraints on constant propagation for builtins *)
+
+Definition builtin_constraints (ef: external_function) :
+                                       list builtin_arg_constraint :=
+  match ef with
+  | EF_vload _ => OK_addrany :: nil
+  | EF_vstore _ => OK_addrany :: OK_default :: nil
+  | EF_memcpy _ _ => OK_addrany :: OK_addrany :: nil
+  | EF_annot txt targs => map (fun _ => OK_all) targs
+  | EF_debug kind txt targs => map (fun _ => OK_all) targs
+  | _ => nil
+  end.