Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

1 files changed, 8 insertions, 4 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index 45b50d6f..44ed5908 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -188,15 +188,19 @@ Definition add_unknown (n: numbering) (rd: reg) :=
               n.(num_eqs)
               (PTree.set rd n.(num_next) n.(num_reg)).
 
-(** [kill_load n] removes all equations involving memory loads.
+(** [kill_load n] removes all equations involving memory loads,
+  as well as those involving memory-dependent operators.
   It is used to reflect the effect of a memory store, which can
   potentially invalidate all such equations. *)
 
 Fixpoint kill_load_eqs (eqs: list (valnum * rhs)) : list (valnum * rhs) :=
   match eqs with
   | nil => nil
-  | (_, Load _ _ _) :: rem => kill_load_eqs rem
-  | v_rh :: rem => v_rh :: kill_load_eqs rem
+  | eq :: rem =>
+      match eq with
+      | (_, Op op _)  => if op_depends_on_memory op then kill_load_eqs rem else eq :: kill_load_eqs rem
+      | (_, Load _ _ _) => kill_load_eqs rem
+      end
   end.
 
 Definition kill_loads (n: numbering) : numbering :=
@@ -252,7 +256,7 @@ Definition equation_holds
      (vres: valnum) (rh: rhs) : Prop :=
   match rh with
   | Op op vl =>
-      eval_operation ge sp op (List.map valuation vl) =
+      eval_operation ge sp op (List.map valuation vl) m =
       Some (valuation vres)
   | Load chunk addr vl =>
       exists a,