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.

3 files changed, 27 insertions, 18 deletions

diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index 759d7c16..f0000a85 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -192,9 +192,11 @@ Nondetfunction addr_strength_reduction_64
 
 Definition addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
-  if Archi.ptr64
-  then addr_strength_reduction_64 addr args vl
-  else addr_strength_reduction_32 addr args vl.
+  if Archi.ptr64 then
+    let addr_args' := addr_strength_reduction_64 addr args vl in
+    if addressing_valid (fst addr_args') then addr_args' else (addr, args)
+  else
+    addr_strength_reduction_32 addr args vl.
 
 Definition make_addimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 5eb46e34..ce20738c 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -292,8 +292,10 @@ Lemma addr_strength_reduction_correct:
   exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
 Proof.
   unfold eval_addressing, addr_strength_reduction. destruct Archi.ptr64.
+- intros until res. destruct (addressing_valid (fst (addr_strength_reduction_64 addr args vl))).
   apply addr_strength_reduction_64_correct.
-  apply addr_strength_reduction_32_correct.
+  intros; exists res; auto.
+- apply addr_strength_reduction_32_correct.
 Qed.
 
 Lemma make_cmp_base_correct:
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