pointer arithmetic: properly check the operation

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.
 

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.
 

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.