Issues with invalid x86 addressing modes (Github issue #183)

- x86/Op: in 32-bit mode all addressings are valid because offsets are always interpreted as 32-bit signed integers in Asmgen.
- x86/ConstpropOp: in addr_strength_reduction, make sure no invalid addressing mode is generated.

1 files changed, 19 insertions, 14 deletions

diff --git a/x86/Op.v b/x86/Op.v
index 18f9e092..8ace5067 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -196,24 +196,29 @@ Defined.
 
 Global Opaque eq_condition eq_addressing eq_operation.
 
-(** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode.
-    The following function checks that an addressing mode is valid, i.e. that
-    the offsets are in range. *)
+(** In addressing modes, offsets are 32-bit signed integers, even in
+    64-bit mode.  The following function checks that an addressing
+    mode is valid, i.e. that the offsets are in range.
+    The check always succeeds in 32-bit mode because offsets are
+    always 32-bit integers and are normalized as 32-bit signed integers
+    during code generation (see [Asmgen.normalize_addrmode_32]). *)
 
 Definition offset_in_range (n: Z) : bool := zle Int.min_signed n && zle n Int.max_signed.
 
 Definition addressing_valid (a: addressing) : bool :=
-  match a with
-  | Aindexed n => offset_in_range n
-  | Aindexed2 n => offset_in_range n
-  | Ascaled sc ofs => offset_in_range ofs
-  | Aindexed2scaled sc ofs => offset_in_range ofs
-  | Aglobal s ofs => true
-  | Abased s ofs => true
-  | Abasedscaled sc s ofs => true
-  | Ainstack ofs => offset_in_range (Ptrofs.signed ofs)
-  end.
-
+  if Archi.ptr64 then
+    match a with
+    | Aindexed n => offset_in_range n
+    | Aindexed2 n => offset_in_range n
+    | Ascaled sc ofs => offset_in_range ofs
+    | Aindexed2scaled sc ofs => offset_in_range ofs
+    | Aglobal s ofs => true
+    | Abased s ofs => true
+    | Abasedscaled sc s ofs => true
+    | Ainstack ofs => offset_in_range (Ptrofs.signed ofs)
+    end
+  else true.
+  
 (** * Evaluation functions *)
 
 (** Evaluation of conditions, operators and addressing modes applied