add difference between pointers

frontend/coq_pp.ml

@@ -158,6 +158,9 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
           | (OpPtr(l), OpInt(_), SubOp  ) ->
               pp "(%a) at_neg_offset{%a, PtrOp, %a} (%a)" pp_expr e1
                 (pp_layout false) l pp_op_type ty2 pp_expr e2
+          | (OpPtr(l1), OpPtr(l2), SubOp  ) ->
+              pp "(%a) sub_ptr{%a, PtrOp, PtrOp} (%a)" pp_expr e1
+                (pp_layout false) l1 pp_expr e2
           | (OpPtr(_), OpInt(_), _      ) ->
               panic_no_pos "Binop [%a] not supported on pointers."
                 pp_bin_op op

theories/lang/lang.v

@@ -17,8 +17,10 @@ Inductive op_type : Set :=
 Inductive bin_op : Set :=
 | AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
 | ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | Comma
-(* Ptr is the second argument and pffset the first *)
-| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
+(* Ptr is the second argument and offset the first *)
+| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout)
+| PtrDiffOp (ly : layout).
+
 
 Inductive un_op : Set :=
 | NotBoolOp | NotIntOp | NegOp | CastOp (ot : op_type).
@@ -238,6 +240,14 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
     heap_state_loc_in_bounds (l offset{ly}ₗ -o) 0 σ.(st_heap) →
     (* TODO: should we have an alignment check here? *)
     eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly}ₗ -o))
+| PtrDiffOpPP v1 v2 σ l1 l2 ly v:
+    val_to_loc v1 = Some l1 →
+    val_to_loc v2 = Some l2 →
+    l1.1 = l2.1 →
+    valid_ptr l1 σ.(st_heap) →
+    valid_ptr l2 σ.(st_heap) →
+    val_of_Z ((l1.2 - l1.2) `div` ly.(ly_size)) ptrdiff_t None = Some v →
+    eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
 | EqOpPNull v1 v2 σ l v:
     heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
     val_to_loc v1 = Some l →

theories/lang/notation.v

@@ -53,6 +53,8 @@ Notation "e1 'at_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrOffsetOp ly) ot2 ot
   (at level 70, format "e1  at_offset{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.
 Notation "e1 'at_neg_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrNegOffsetOp ly) ot2 ot1 e2%E e1%E)
   (at level 70, format "e1  at_neg_offset{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.
+Notation "e1 'sub_ptr{' ly , ot1 , ot2 } e2" := (BinOp (PtrDiffOp ly) ot2 ot1 e1%E e2%E)
+  (at level 70, format "e1  sub_ptr{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <-{ ly , o } e2 ; s" := (Assign o ly e1%E e2%E s%E)
   (at level 80, s at level 200, format "'[v' e1  '<-{' ly ',' o '}'  e2 ';' '/' s ']'") : expr_scope.