From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 9 Apr 2011 16:59:13 +0000
Subject: 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
---
 backend/Cminor.v | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'backend/Cminor.v')

diff --git a/backend/Cminor.v b/backend/Cminor.v
index a3a166c..45e060d 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -254,7 +254,7 @@ Definition eval_compare_null (c: comparison) (n: int) : option val :=
   if Int.eq n Int.zero then eval_compare_mismatch c else None.
 
 Definition eval_binop
-            (op: binary_operation) (arg1 arg2: val): option val :=
+            (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
   match op, arg1, arg2 with
   | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1))
@@ -287,16 +287,19 @@ Definition eval_binop
   | Odivf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.div f1 f2))
   | Ocmp c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmp c n1 n2))
-  | Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
-      if eq_block b1 b2
-      then Some(Val.of_bool(Int.cmp c n1 n2))
-      else eval_compare_mismatch c
-  | Ocmp c, Vptr b1 n1, Vint n2 =>
-      eval_compare_null c n2
-  | Ocmp c, Vint n1, Vptr b2 n2 =>
-      eval_compare_null c n1
   | Ocmpu c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmpu c n1 n2))
+  | Ocmpu c, Vptr b1 n1, Vptr b2 n2 =>
+      if Mem.valid_pointer m b1 (Int.unsigned n1)
+      && Mem.valid_pointer m b2 (Int.unsigned n2) then
+        if eq_block b1 b2
+        then Some(Val.of_bool(Int.cmpu c n1 n2))
+        else eval_compare_mismatch c
+      else None
+  | Ocmpu c, Vptr b1 n1, Vint n2 =>
+      eval_compare_null c n2
+  | Ocmpu c, Vint n1, Vptr b2 n2 =>
+      eval_compare_null c n1
   | Ocmpf c, Vfloat f1, Vfloat f2 =>
       Some (Val.of_bool (Float.cmp c f1 f2))
   | _, _, _ => None
@@ -330,7 +333,7 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Ebinop: forall op a1 a2 v1 v2 v,
       eval_expr a1 v1 ->
       eval_expr a2 v2 ->
-      eval_binop op v1 v2 = Some v ->
+      eval_binop op v1 v2 m = Some v ->
       eval_expr (Ebinop op a1 a2) v
   | eval_Eload: forall chunk addr vaddr v,
       eval_expr addr vaddr ->
-- 
cgit v1.2.3