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).

19 files changed, 3 insertions, 1 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index b94db3ca..641c9fdc 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -2,9 +2,11 @@ include ../Makefile.config
 
 CFLAGS=-O1 -g -Wall
 
-ifeq ($(ARCH),ia32)
+ifeq ($(ARCH),x86)
 ifeq ($(MODEL),64)
 ARCH=x86_64
+else
+ARCH=x86_32
 endif
 endif
 
diff --git a/runtime/ia32/i64_dtos.S b/runtime/x86_32/i64_dtos.S
index 3cc381bf..3cc381bf 100644
--- a/runtime/ia32/i64_dtos.S
+++ b/runtime/x86_32/i64_dtos.S
diff --git a/runtime/ia32/i64_dtou.S b/runtime/x86_32/i64_dtou.S
index 4903f847..4903f847 100644
--- a/runtime/ia32/i64_dtou.S
+++ b/runtime/x86_32/i64_dtou.S
diff --git a/runtime/ia32/i64_sar.S b/runtime/x86_32/i64_sar.S
index cf2233b1..cf2233b1 100644
--- a/runtime/ia32/i64_sar.S
+++ b/runtime/x86_32/i64_sar.S
diff --git a/runtime/ia32/i64_sdiv.S b/runtime/x86_32/i64_sdiv.S
index f6551c7d..f6551c7d 100644
--- a/runtime/ia32/i64_sdiv.S
+++ b/runtime/x86_32/i64_sdiv.S
diff --git a/runtime/ia32/i64_shl.S b/runtime/x86_32/i64_shl.S
index 1fabebce..1fabebce 100644
--- a/runtime/ia32/i64_shl.S
+++ b/runtime/x86_32/i64_shl.S
diff --git a/runtime/ia32/i64_shr.S b/runtime/x86_32/i64_shr.S
index 34196f09..34196f09 100644
--- a/runtime/ia32/i64_shr.S
+++ b/runtime/x86_32/i64_shr.S
diff --git a/runtime/ia32/i64_smod.S b/runtime/x86_32/i64_smod.S
index 28f47ad4..28f47ad4 100644
--- a/runtime/ia32/i64_smod.S
+++ b/runtime/x86_32/i64_smod.S
diff --git a/runtime/ia32/i64_smulh.S b/runtime/x86_32/i64_smulh.S
index cc0f0167..cc0f0167 100644
--- a/runtime/ia32/i64_smulh.S
+++ b/runtime/x86_32/i64_smulh.S
diff --git a/runtime/ia32/i64_stod.S b/runtime/x86_32/i64_stod.S
index d020e2fc..d020e2fc 100644
--- a/runtime/ia32/i64_stod.S
+++ b/runtime/x86_32/i64_stod.S
diff --git a/runtime/ia32/i64_stof.S b/runtime/x86_32/i64_stof.S
index 25b1d4f7..25b1d4f7 100644
--- a/runtime/ia32/i64_stof.S
+++ b/runtime/x86_32/i64_stof.S
diff --git a/runtime/ia32/i64_udiv.S b/runtime/x86_32/i64_udiv.S
index 75305433..75305433 100644
--- a/runtime/ia32/i64_udiv.S
+++ b/runtime/x86_32/i64_udiv.S
diff --git a/runtime/ia32/i64_udivmod.S b/runtime/x86_32/i64_udivmod.S
index dccfc286..dccfc286 100644
--- a/runtime/ia32/i64_udivmod.S
+++ b/runtime/x86_32/i64_udivmod.S
diff --git a/runtime/ia32/i64_umod.S b/runtime/x86_32/i64_umod.S
index a019df28..a019df28 100644
--- a/runtime/ia32/i64_umod.S
+++ b/runtime/x86_32/i64_umod.S
diff --git a/runtime/ia32/i64_umulh.S b/runtime/x86_32/i64_umulh.S
index 449a0f8b..449a0f8b 100644
--- a/runtime/ia32/i64_umulh.S
+++ b/runtime/x86_32/i64_umulh.S
diff --git a/runtime/ia32/i64_utod.S b/runtime/x86_32/i64_utod.S
index 428a3b94..428a3b94 100644
--- a/runtime/ia32/i64_utod.S
+++ b/runtime/x86_32/i64_utod.S
diff --git a/runtime/ia32/i64_utof.S b/runtime/x86_32/i64_utof.S
index 0b58f48b..0b58f48b 100644
--- a/runtime/ia32/i64_utof.S
+++ b/runtime/x86_32/i64_utof.S
diff --git a/runtime/ia32/sysdeps.h b/runtime/x86_32/sysdeps.h
index 9d957a88..9d957a88 100644
--- a/runtime/ia32/sysdeps.h
+++ b/runtime/x86_32/sysdeps.h
diff --git a/runtime/ia32/vararg.S b/runtime/x86_32/vararg.S
index 78666c70..78666c70 100644
--- a/runtime/ia32/vararg.S
+++ b/runtime/x86_32/vararg.S