Allow casting NULL to an integer

examples/intptr.c

@@ -148,3 +148,12 @@ int roundtrip_and_read4(int* p){
   int *q = (int*) rc_copy_alloc_id(j, p);
   return *q;
 }
+
+/**** Casting NULL and function pointers ***************************************/
+
+[[rc::returns("{0} @ int<i32>")]]
+int cast_NULL() {
+  return (int) NULL;
+}
+
+// TODO: add casting for function pointers

examples/proofs/intptr/generated_code.v

@@ -189,6 +189,9 @@ Section code.
   Definition loc_254 : location_info := LocationInfo file_0 146 16 146 29.
   Definition loc_255 : location_info := LocationInfo file_0 146 28 146 29.
   Definition loc_256 : location_info := LocationInfo file_0 146 28 146 29.
+  Definition loc_261 : location_info := LocationInfo file_0 156 2 156 30.
+  Definition loc_262 : location_info := LocationInfo file_0 156 9 156 29.
+  Definition loc_263 : location_info := LocationInfo file_0 156 15 156 29.
 
   (* Definition of function [int_ptr1]. *)
   Definition impl_int_ptr1 : function := {|
@@ -494,4 +497,19 @@ Section code.
       ]> $∅
     )%E
   |}.
+
+  (* Definition of function [cast_NULL]. *)
+  Definition impl_cast_NULL : function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_261 ;
+        Return (LocInfoE loc_262 (UnOp (CastOp $ IntOp i32) (PtrOp) (LocInfoE loc_263 (NULL))))
+      ]> $∅
+    )%E
+  |}.
 End code.

examples/proofs/intptr/generated_spec.v

@@ -73,4 +73,8 @@ Section spec.
   Definition type_of_roundtrip_and_read4 :=
     fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
       → ∃ () : (), (n @ (int (i32))); (p ◁ₗ (n @ (int (i32)))).
+
+  (* Specifications for function [cast_NULL]. *)
+  Definition type_of_cast_NULL :=
+    fn(∀ () : (); True) → ∃ () : (), ((0) @ (int (i32))); True.
 End spec.

examples/proofs/intptr/proof_files

+generated_proof_cast_NULL.v
 generated_proof_int_ptr1.v
 generated_proof_int_ptr2.v
 generated_proof_int_ptr3.v

theories/lang/lang.v

@@ -337,6 +337,10 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
     val_of_int_repr (IRLoc l) it = Some vt →
     block_alive l σ.(st_heap) →
     eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
+| CastOpPINull it σ vs vt:
+    vs = NULL →
+    val_of_Z 0 it = Some vt →
+    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
 | CastOpIP it σ vs vt l l':
     val_to_loc_weak vs it = Some l →
     val_of_loc l' = vt →

theories/lang/lifting.v

@@ -355,9 +355,22 @@ Lemma wp_cast_ptr_int Φ v v' l E it:
 Proof.
   iIntros (Hv Hv') "HΦ".
   iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"].
-  iIntros (σ ?) "Hctx". iDestruct (alloc_alive_loc_to_block_alive with "HΦ Hctx") as %?.
+  iIntros (σ ?) "Hctx". iDestruct (alloc_alive_loc_to_block_alive with "HΦ Hctx") as %Hb.
   iPureIntro. split.
-  - by inversion 1; simplify_eq.
+  - move: (Hb) => [?[??]]. have ? := val_to_of_loc NULL_loc. inversion 1; unfold NULL in *; by simplify_eq.
+  - move => ->. by econstructor.
+Qed.
+
+Lemma wp_cast_null_int Φ v E it:
+  val_of_Z 0 it = Some v →
+  ▷ Φ v -∗
+  WP UnOp (CastOp (IntOp it)) PtrOp (Val NULL) @ E {{ Φ }}.
+Proof.
+  iIntros (Hv) "HΦ".
+  iApply wp_unop_det. iSplit; [|done].
+  iIntros (σ ?) "Hctx". iPureIntro. split.
+  - inversion 1; simplify_eq => //. revert select (block_alive _ _) => -[?[??]].
+    have ? := val_to_of_loc NULL_loc. unfold NULL in *; by simplify_eq.
   - move => ->. by econstructor.
 Qed.
 

theories/typing/own.v

@@ -548,6 +548,19 @@ Section null.
     TypedBinOp l (l ◁ₗ{β} ty) v2 (v2 ◁ᵥ null) op PtrOp PtrOp :=
     λ T, i2p (type_binop_ptr_null v2 op T l ty β n).
 
+  Lemma type_cast_null_int it v T:
+    (T (i2v 0 it) (t2mt (0 @ int it))) -∗
+    typed_un_op v (v ◁ᵥ null) (CastOp (IntOp it)) PtrOp T.
+  Proof.
+    iIntros "HT" (-> Φ) "HΦ".
+    iApply wp_cast_null_int.
+    { by apply: (val_of_Z_bool false). }
+    iModIntro. iApply ("HΦ" with "[] HT").
+    iPureIntro. apply: val_to_Z_to_int_repr_Z. apply: (i2v_bool_Some false).
+  Qed.
+  Global Instance type_cast_null_int_inst v it:
+    TypedUnOpVal v null (CastOp (IntOp it)) PtrOp :=
+    λ T, i2p (type_cast_null_int it v T).
 End null.
 
 Section optionable.