CN: Add support for bitwise subtraction

Though the test looks like it is for pointer difference, the actual
issue is that the elaboration has `array_shift( a_533, signed int,   0 -
a_534)`, and it is the `0 - a534` which was causing the error.

In principle we can/should have pure subtraction at integer and real
types as well, but this can be generalised later as and when the need
arises.

backend/cn/lib/check.ml

@@ -623,7 +623,11 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
           let@ () = WellTyped.ensure_base_type loc ~expect:Bool (bt_of_pexpr pe2) in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (or_ [ v1; v2 ] loc)))
         | OpAdd -> not_yet "OpAdd"
-        | OpSub -> not_yet "OpSub"
+        | OpSub ->
+          let@ () = WellTyped.ensure_bits_type loc expect in
+          let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe1) in
+          let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe2) in
+          check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (sub_ (v1, v2) loc)))
         | OpMul -> not_yet "OpMul"
         | OpRem_f -> not_yet "OpRem_f"
         | OpExp -> not_yet "OpExp")

tests/cn/ptr_diff2.c

@@ -0,0 +1,11 @@
+int* f(int *p)
+/*@ ensures ptr_eq(return, array_shift(p, -1i32)); @*/
+{
+  return p - 1;
+}
+
+int main(void)
+{
+    int arr = 0;
+    f(&arr + 1); 
+}