Introduce and use the platform-specific Archi module giving:

- endianness
- alignment constraints for 8-byte types
    (which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).


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

13 files changed, 111 insertions, 91 deletions

diff --git a/.depend b/.depend
index d79e968..2b18734 100644
--- a/.depend
+++ b/.depend
@@ -7,8 +7,8 @@ lib/Lattice.vo lib/Lattice.glob lib/Lattice.v.beautified: lib/Lattice.v lib/Coql
 lib/Ordered.vo lib/Ordered.glob lib/Ordered.v.beautified: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo
 lib/Iteration.vo lib/Iteration.glob lib/Iteration.v.beautified: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo
 lib/Integers.vo lib/Integers.glob lib/Integers.v.beautified: lib/Integers.v lib/Coqlib.vo
-lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo
-$(ARCH)/Nan.vo $(ARCH)/Nan.glob $(ARCH)/Nan.v.beautified: $(ARCH)/Nan.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo lib/Floats.vo lib/Integers.vo
+$(ARCH)/Archi.vo $(ARCH)/Archi.glob $(ARCH)/Archi.v.beautified: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo
+lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo $(ARCH)/Archi.vo
 lib/Parmov.vo lib/Parmov.glob lib/Parmov.v.beautified: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo
 lib/UnionFind.vo lib/UnionFind.glob lib/UnionFind.v.beautified: lib/UnionFind.v lib/Coqlib.vo
 lib/Wfsimpl.vo lib/Wfsimpl.glob lib/Wfsimpl.v.beautified: lib/Wfsimpl.v lib/Axioms.vo
@@ -19,9 +19,9 @@ common/Errors.vo common/Errors.glob common/Errors.v.beautified: common/Errors.v
 common/AST.vo common/AST.glob common/AST.v.beautified: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo
 common/Events.vo common/Events.glob common/Events.v.beautified: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo
 common/Globalenvs.vo common/Globalenvs.glob common/Globalenvs.v.beautified: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo
-common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo
+common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo
 common/Memtype.vo common/Memtype.glob common/Memtype.v.beautified: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo
-common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo lib/Intv.vo
+common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Intv.vo lib/Maps.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo
 common/Values.vo common/Values.glob common/Values.v.beautified: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo
 common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo
 common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo
@@ -75,8 +75,8 @@ backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: back
 $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo
 backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo
 backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo
-backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
-backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo
+backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
+backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo
 backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo
 backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
 backend/Linear.vo backend/Linear.glob backend/Linear.v.beautified: backend/Linear.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
@@ -95,7 +95,7 @@ $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmge
 backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
 $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo
 $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
-cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo
+cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo
 cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
 cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo
diff --git a/Makefile b/Makefile
index 28e945f..b527a8c 100644
--- a/Makefile
+++ b/Makefile
@@ -65,7 +65,7 @@ FLOCQ=\
 # General-purpose libraries (in lib/)
 
 LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
-  Iteration.v Integers.v Floats.v Nan.v Parmov.v UnionFind.v Wfsimpl.v \
+  Iteration.v Integers.v Archi.v Floats.v Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v
 
 # Parts common to the front-ends and the back-end (in common/)
diff --git a/arm/Nan.v b/arm/Archi.v
index e2bddf6..e693541 100644
--- a/arm/Nan.v
+++ b/arm/Archi.v
@@ -14,11 +14,16 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** Architecture-dependent parameters for ARM *)
+
+Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
-Require Import Floats.
-Require Import ZArith.
-Require Import Integers.
+
+Definition big_endian := false.
+
+Notation align_int64 := 8%Z (only parsing).
+Notation align_float64 := 8%Z (only parsing).
 
 Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH).
 
@@ -27,3 +32,5 @@ Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 5
       In all other cases, choose first NaN *)
   (Pos.testbit (proj1_sig pl1) 51 &&
    negb (Pos.testbit (proj1_sig pl2) 51))%bool.
+
+Global Opaque big_endian default_pl choose_binop_pl.
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 0851b77..f830d79 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -14,6 +14,7 @@
 
 Require Import FSets.
 Require FSetAVLplus.
+Require Archi.
 Require Import Coqlib.
 Require Import Ordered.
 Require Import Errors.
@@ -814,8 +815,8 @@ Definition transfer_use_def (args: list reg) (res: reg) (args': list mreg) (res'
   assertion (can_undef undefs e1);
   add_equations args args' e1.
 
-Definition kind_first_word := if big_endian then High else Low.
-Definition kind_second_word := if big_endian then Low else High.
+Definition kind_first_word := if Archi.big_endian then High else Low.
+Definition kind_second_word := if Archi.big_endian then Low else High.
 
 (** The core transfer function.  It takes a set [e] of equations that must
   hold "after" and a block shape [shape] representing a matching pair
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 1e637f9..4c39fee 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -14,6 +14,7 @@
   RTL to LTL). *)
 
 Require Import FSets.
+Require Archi.
 Require Import Coqlib.
 Require Import Ordered.
 Require Import Errors.
@@ -1745,8 +1746,8 @@ Proof.
 (* load pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
-  set (v2' := if big_endian then v2 else v1) in *.
-  set (v1' := if big_endian then v1 else v2) in *.
+  set (v2' := if Archi.big_endian then v2 else v1) in *.
+  set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')).
   { eapply add_equations_lessdef; eauto. }
@@ -1759,7 +1760,7 @@ Proof.
     eapply add_equations_satisf; eauto. assumption.
     rewrite Regmap.gss. apply Val.lessdef_trans with v1'; auto. 
     subst v. unfold v1', kind_first_word.
-    destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
+    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
   assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')).
@@ -1777,7 +1778,7 @@ Proof.
     eapply add_equations_satisf; eauto. assumption.
     apply Val.lessdef_trans with v2'; auto. 
     rewrite Regmap.gss. subst v. unfold v2', kind_second_word.
-    destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
+    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
   }
   exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]].
   econstructor; split.
@@ -1799,8 +1800,8 @@ Proof.
 (* load first word of a pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
-  set (v2' := if big_endian then v2 else v1) in *.
-  set (v1' := if big_endian then v1 else v2) in *.
+  set (v2' := if Archi.big_endian then v2 else v1) in *.
+  set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')).
   { eapply add_equations_lessdef; eauto. }
@@ -1811,7 +1812,7 @@ Proof.
   { eapply parallel_assignment_satisf; eauto.
     apply Val.lessdef_trans with v1'; auto. 
     subst v. unfold v1', kind_first_word.
-    destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
+    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
@@ -1830,8 +1831,8 @@ Proof.
 (* load second word of a pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
-  set (v2' := if big_endian then v2 else v1) in *.
-  set (v1' := if big_endian then v1 else v2) in *.
+  set (v2' := if Archi.big_endian then v2 else v1) in *.
+  set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')).
   { eapply add_equations_lessdef; eauto. }
@@ -1843,7 +1844,7 @@ Proof.
   { eapply parallel_assignment_satisf; eauto.
     apply Val.lessdef_trans with v2'; auto. 
     subst v. unfold v2', kind_second_word.
-    destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
+    destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
   exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. 
@@ -1888,12 +1889,12 @@ Proof.
 
 (* store 2 *)
 - exploit Mem.storev_int64_split; eauto. 
-  replace (if big_endian then Val.hiword rs#src else Val.loword rs#src)
+  replace (if Archi.big_endian then Val.hiword rs#src else Val.loword rs#src)
      with (sel_val kind_first_word rs#src)
-       by (unfold kind_first_word; destruct big_endian; reflexivity).
-  replace (if big_endian then Val.loword rs#src else Val.hiword rs#src)
+       by (unfold kind_first_word; destruct Archi.big_endian; reflexivity).
+  replace (if Archi.big_endian then Val.loword rs#src else Val.hiword rs#src)
      with (sel_val kind_second_word rs#src)
-       by (unfold kind_second_word; destruct big_endian; reflexivity).
+       by (unfold kind_second_word; destruct Archi.big_endian; reflexivity).
   intros [m1 [STORE1 STORE2]].
   exploit (exec_moves mv1); eauto. intros [ls1 [X Y]].
   exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1.
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 5c68602..b21eeb0 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -150,9 +150,9 @@ let block_of_RTL_instr funsig tyenv = function
         | None -> assert false
         | Some addr' ->
             [Xload(Mint32, addr, vregs tyenv args,
-                   V((if big_endian then dst else twin_reg dst), Tint));
+                   V((if Archi.big_endian then dst else twin_reg dst), Tint));
              Xload(Mint32, addr', vregs tyenv args,
-                   V((if big_endian then twin_reg dst else dst), Tint));
+                   V((if Archi.big_endian then twin_reg dst else dst), Tint));
              Xbranch s]
       end else
         [Xload(chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s]
@@ -162,9 +162,9 @@ let block_of_RTL_instr funsig tyenv = function
         | None -> assert false
         | Some addr' ->
             [Xstore(Mint32, addr, vregs tyenv args,
-                   V((if big_endian then src else twin_reg src), Tint));
+                   V((if Archi.big_endian then src else twin_reg src), Tint));
              Xstore(Mint32, addr', vregs tyenv args,
-                   V((if big_endian then twin_reg src else src), Tint));
+                   V((if Archi.big_endian then twin_reg src else src), Tint));
              Xbranch s]
       end else
         [Xstore(chunk, addr, vregs tyenv args, vreg tyenv src); Xbranch s]
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index ec4780e..5cd032d 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -18,6 +18,7 @@
 Require Import Coqlib.
 Require Import AST.
 Require Import Errors.
+Require Archi.
 
 (** * Syntax of types *)
 
@@ -172,9 +173,9 @@ Fixpoint alignof (t: type) : Z :=
       | Tint I16 _ _ => 2
       | Tint I32 _ _ => 4
       | Tint IBool _ _ => 1
-      | Tlong _ _ => 8
+      | Tlong _ _ => Archi.align_int64
       | Tfloat F32 _ => 4
-      | Tfloat F64 _ => 8
+      | Tfloat F64 _ => Archi.align_float64
       | Tpointer _ _ => 4
       | Tarray t' _ _ => alignof t'
       | Tfunction _ _ _ => 1
@@ -214,10 +215,14 @@ Proof.
   induction t; apply X; simpl; auto.
   exists 0%nat; auto.
   destruct i.
-    exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto.
-    exists 0%nat; auto. exists 3%nat; auto.
+    exists 0%nat; auto.
+    exists 1%nat; auto.
+    exists 2%nat; auto.
+    exists 0%nat; auto.
+    (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
   destruct f.
-    exists 2%nat; auto. exists 3%nat; auto.
+    exists 2%nat; auto.
+    (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity).
   exists 2%nat; auto.
   exists 0%nat; auto.
   exists 2%nat; auto.
@@ -311,8 +316,8 @@ Local Transparent alignof.
   induction t; simpl; intros.
 - apply Zdivide_refl.
 - rewrite H. destruct i; apply Zdivide_refl.
-- rewrite H; apply Zdivide_refl.
-- rewrite H. destruct f; apply Zdivide_refl.
+- rewrite H. exists (8 / Archi.align_int64); reflexivity. 
+- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. 
 - rewrite H; apply Zdivide_refl.
 - destruct H. rewrite H. apply Z.divide_mul_l; auto. 
 - apply Zdivide_refl.
diff --git a/common/Memdata.v b/common/Memdata.v
index 47f8471..d8d347e 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -17,6 +17,7 @@
 (** In-memory representation of values. *)
 
 Require Import Coqlib.
+Require Archi.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -146,10 +147,8 @@ Fixpoint int_of_bytes (l: list byte): Z :=
   | b :: l' => Byte.unsigned b + int_of_bytes l' * 256
   end.
 
-Parameter big_endian: bool.
-
 Definition rev_if_be (l: list byte) : list byte :=
-  if big_endian then List.rev l else l.
+  if Archi.big_endian then List.rev l else l.
 
 Definition encode_int (sz: nat) (x: Z) : list byte :=
   rev_if_be (bytes_of_int sz x).
@@ -168,7 +167,7 @@ Qed.
 Lemma rev_if_be_length:
   forall l, length (rev_if_be l) = length l.
 Proof.
-  intros; unfold rev_if_be; destruct big_endian.
+  intros; unfold rev_if_be; destruct Archi.big_endian.
   apply List.rev_length.
   auto.
 Qed.
@@ -200,7 +199,7 @@ Qed.
 Lemma rev_if_be_involutive:
   forall l, rev_if_be (rev_if_be l) = l.
 Proof.
-  intros; unfold rev_if_be; destruct big_endian. 
+  intros; unfold rev_if_be; destruct Archi.big_endian. 
   apply List.rev_involutive. 
   auto.
 Qed.
@@ -914,8 +913,8 @@ Lemma decode_val_int64:
   forall l1 l2,
   length l1 = 4%nat -> length l2 = 4%nat ->
   decode_val Mint64 (l1 ++ l2) =
-  Val.longofwords (decode_val Mint32 (if big_endian then l1 else l2))
-                  (decode_val Mint32 (if big_endian then l2 else l1)).
+  Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
+                  (decode_val Mint32 (if Archi.big_endian then l2 else l1)).
 Proof.
   intros. unfold decode_val.
   assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end).
@@ -935,7 +934,7 @@ Proof.
     generalize (int_of_bytes_range l). rewrite H1. 
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). 
     omega.
-  unfold decode_int, rev_if_be. destruct big_endian; rewrite B1; rewrite B2.
+  unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2.
   + rewrite <- (rev_length b1) in L1. 
     rewrite <- (rev_length b2) in L2.
     rewrite rev_app_distr.
@@ -946,9 +945,9 @@ Proof.
   + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal.
     rewrite !UR by auto. rewrite int_of_bytes_append. 
     rewrite L1. change (Z.of_nat 4 * 8) with 32. ring.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
 Qed.
 
 Lemma bytes_of_int_append:
@@ -987,10 +986,10 @@ Qed.
 Lemma encode_val_int64:
   forall v,
   encode_val Mint64 v =
-     encode_val Mint32 (if big_endian then Val.hiword v else Val.loword v)
-  ++ encode_val Mint32 (if big_endian then Val.loword v else Val.hiword v).
+     encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v)
+  ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v).
 Proof.
-  intros. destruct v; destruct big_endian eqn:BI; try reflexivity;
+  intros. destruct v; destruct Archi.big_endian eqn:BI; try reflexivity;
   unfold Val.loword, Val.hiword, encode_val.
   unfold inj_bytes. rewrite <- map_app. f_equal. 
   unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal.
diff --git a/common/Memory.v b/common/Memory.v
index 79fc8a0..0260a89 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -31,6 +31,7 @@ Require Import Axioms.
 Require Import Coqlib.
 Require Intv.
 Require Import Maps.
+Require Archi.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -891,8 +892,8 @@ Theorem load_int64_split:
   forall m b ofs v,
   load Mint64 m b ofs = Some v ->
   exists v1 v2,
-     load Mint32 m b ofs = Some (if big_endian then v1 else v2)
-  /\ load Mint32 m b (ofs + 4) = Some (if big_endian then v2 else v1)
+     load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
+  /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
   /\ v = Val.longofwords v1 v2.
 Proof.
   intros. 
@@ -909,10 +910,10 @@ Proof.
   exploit loadbytes_load. eexact LB2.
   simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
-  exists (decode_val Mint32 (if big_endian then bytes1 else bytes2));
-  exists (decode_val Mint32 (if big_endian then bytes2 else bytes1)).
-  split. destruct big_endian; auto.
-  split. destruct big_endian; auto.
+  exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
+  exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
+  split. destruct Archi.big_endian; auto.
+  split. destruct Archi.big_endian; auto.
   rewrite EQ. rewrite APP. apply decode_val_int64.
   erewrite loadbytes_length; eauto. reflexivity. 
   erewrite loadbytes_length; eauto. reflexivity. 
@@ -922,8 +923,8 @@ Theorem loadv_int64_split:
   forall m a v,
   loadv Mint64 m a = Some v ->
   exists v1 v2,
-     loadv Mint32 m a = Some (if big_endian then v1 else v2)
-  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if big_endian then v2 else v1)
+     loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
+  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
   /\ v = Val.longofwords v1 v2.
 Proof.
   intros. destruct a; simpl in H; try discriminate.
@@ -1674,8 +1675,8 @@ Theorem store_int64_split:
   forall m b ofs v m',
   store Mint64 m b ofs v = Some m' ->
   exists m1,
-     store Mint32 m b ofs (if big_endian then Val.hiword v else Val.loword v) = Some m1
-  /\ store Mint32 m1 b (ofs + 4) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+     store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
 Proof.
   intros. 
   exploit store_valid_access_3; eauto. intros [A B]. simpl in *.
@@ -1694,8 +1695,8 @@ Theorem storev_int64_split:
   forall m a v m',
   storev Mint64 m a v = Some m' ->
   exists m1,
-     storev Mint32 m a (if big_endian then Val.hiword v else Val.loword v) = Some m1
-  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+     storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
 Proof.
   intros. destruct a; simpl in H; try discriminate.
   exploit store_int64_split; eauto. intros [m1 [A B]].
diff --git a/extraction/extraction.v b/extraction/extraction.v
index b1cd8fd..6556c87 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -12,7 +12,6 @@
 
 Require Coqlib.
 Require Wfsimpl.
-Require Nan.
 Require AST.
 Require Iteration.
 Require Floats.
@@ -34,17 +33,10 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
 (* Wfsimpl *)
 Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
 
-(* Floats *)
-Extract Constant Floats.Float.default_pl => "Nan.default_pl".
-Extract Constant Floats.Float.choose_binop_pl => "Nan.choose_binop_pl".
-
 (* AST *)
 Extract Constant AST.ident_of_string =>
   "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)".
 
-(* Memdata *)
-Extract Constant Memdata.big_endian => "Memdataaux.big_endian".
-
 (* Memory - work around an extraction bug. *)
 Extraction NoInline Memory.Mem.valid_pointer.
 
@@ -140,5 +132,4 @@ Separate Extraction
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg
    RTL.instr_defs RTL.instr_uses
    Machregs.mregs_for_operation Machregs.mregs_for_builtin
-   Machregs.two_address_op
-   Nan.default_pl Nan.choose_binop_pl.
+   Machregs.two_address_op.
diff --git a/ia32/Nan.v b/ia32/Archi.v
index f3e777e..a2e136c 100644
--- a/ia32/Nan.v
+++ b/ia32/Archi.v
@@ -14,13 +14,21 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** Architecture-dependent parameters for IA32 *)
+
+Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
-Require Import Floats.
-Require Import ZArith.
-Require Import Integers.
 
-Program Definition default_pl : bool * nan_pl 53 := (true, nat_iter 51 xO xH).
+Definition big_endian := false.
+
+Notation align_int64 := 4%Z (only parsing).
+Notation align_float64 := 4%Z (only parsing).
+
+Program Definition default_pl : bool * nan_pl 53 := 
+  (true, nat_iter 51 xO xH).
 
 Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
-  false.                        (** always choose first NaN *)
+  false.                        (**r always choose first NaN *)
+
+Global Opaque big_endian default_pl choose_binop_pl.
diff --git a/lib/Floats.v b/lib/Floats.v
index 0a30836..5502927 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -26,6 +26,7 @@ Require Import Fcalc_round.
 Require Import Fcalc_bracket.
 Require Import Fprop_Sterbenz.
 Require Import Program.
+Require Archi.
 
 Close Scope R_scope.
 
@@ -268,18 +269,15 @@ Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit
 - a choice function determining which of the payload arguments to choose,
   when an operation is given two NaN arguments. *)
 
-Parameter default_pl : bool*nan_pl 53.
-Parameter choose_binop_pl : bool -> nan_pl 53 -> bool -> nan_pl 53 -> bool.
-
 Definition binop_pl (x y: binary64) : bool*nan_pl 53 :=
   match x, y with
   | B754_nan s1 pl1, B754_nan s2 pl2 =>
-      if choose_binop_pl s1 pl1 s2 pl2
+      if Archi.choose_binop_pl s1 pl1 s2 pl2
       then (s2, transform_quiet_pl pl2)
       else (s1, transform_quiet_pl pl1)
   | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
   | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
-  | _, _ => default_pl
+  | _, _ => Archi.default_pl
   end.
 
 Definition add: float -> float -> float := b64_plus binop_pl mode_NE. (**r addition *)
@@ -1235,8 +1233,9 @@ Proof.
       etransitivity. apply H.
       symmetry. etransitivity. apply H0.
       f_equal. destruct Bsign; reflexivity.
-  - destruct f as [[]|[]| |]; try discriminate; try reflexivity.
-    simpl. destruct (choose_binop_pl b n b n); auto.
+  - destruct f as [[]|[]| |]; try discriminate; simpl. 
+    auto. auto. auto. auto.
+    destruct (Archi.choose_binop_pl b n b n); auto.
 Qed.
 
 Program Definition pow2_float (b:bool) (e:Z) (H:-1023 < e < 1023) : float :=
diff --git a/powerpc/Nan.v b/powerpc/Archi.v
index c230789..0672dce 100644
--- a/powerpc/Nan.v
+++ b/powerpc/Archi.v
@@ -14,13 +14,21 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** Architecture-dependent parameters for PowerPC *)
+
+Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
-Require Import Floats.
-Require Import ZArith.
-Require Import Integers.
 
-Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH).
+Definition big_endian := false.
+
+Notation align_int64 := 8%Z (only parsing).
+Notation align_float64 := 8%Z (only parsing).
+
+Program Definition default_pl : bool * nan_pl 53 := 
+  (true, nat_iter 51 xO xH).
 
 Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
-  false.
+  false.                        (**r always choose first NaN *)
+
+Global Opaque big_endian default_pl choose_binop_pl.