From 62a2b37a638453669e06044ee669fa99d7b32235 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Dec 2019 14:44:12 +0100
Subject: [PATCH] pointer arithmetic: properly check the operation

---
 theories/heap_lang/lang.v          | 8 +++++++-
 theories/heap_lang/metatheory.v    | 2 +-
 theories/heap_lang/proph_erasure.v | 2 +-
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 45a3fde8c..2471844ed 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -523,6 +523,12 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   | OffsetOp => None (* Pointer arithmetic *)
   end.
 
+Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
+  match op, v2 with
+  | OffsetOp, (LitInt off) => Some $ LitLoc (l1 +â‚— off)
+  | _, _ => None
+  end.
+
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
     (* Crucially, this compares the same way as [CmpXchg]! *)
@@ -534,7 +540,7 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
     match v1, v2 with
     | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
     | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
-    | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l +â‚— off)
+    | LitV (LitLoc l1), LitV v2 => LitV <$> bin_op_eval_loc op l1 v2
     | _, _ => None
     end.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 49629d63e..090b22601 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -88,7 +88,7 @@ Lemma  bin_op_eval_closed op v1 v2 v':
   is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
   is_closed_val v'.
 Proof.
-  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int;
+  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
     repeat case_match; by naive_solver.
 Qed.
 
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index f12382ee3..5f18f7667 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -174,7 +174,7 @@ Lemma bin_op_eval_erase op v1 v2 v' :
   bin_op_eval op (erase_val v1) (erase_val v2) = Some v' ↔
   ∃ w, bin_op_eval op v1 v2 = Some w ∧ erase_val w = v'.
 Proof.
-  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool;
+  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc;
     split; [intros ?|intros (?&?&?)];
       repeat (case_match; simplify_eq/=); eauto.
   - eexists _; split; eauto; simpl.
-- 
GitLab