semantics and typing rule for NotIntOp

examples/proofs/tests/generated_code.v

@@ -113,6 +113,56 @@ Section code.
   Definition loc_148 : location_info := LocationInfo file_0 41 18 41 19.
   Definition loc_149 : location_info := LocationInfo file_0 41 24 41 25.
   Definition loc_150 : location_info := LocationInfo file_0 40 14 40 15.
+  Definition loc_155 : location_info := LocationInfo file_0 48 2 48 29.
+  Definition loc_156 : location_info := LocationInfo file_0 49 2 49 30.
+  Definition loc_157 : location_info := LocationInfo file_0 50 2 50 39.
+  Definition loc_158 : location_info := LocationInfo file_0 51 2 51 41.
+  Definition loc_159 : location_info := LocationInfo file_0 52 2 52 41.
+  Definition loc_160 : location_info := LocationInfo file_0 53 2 53 37.
+  Definition loc_161 : location_info := LocationInfo file_0 54 2 54 33.
+  Definition loc_162 : location_info := LocationInfo file_0 55 2 55 38.
+  Definition loc_163 : location_info := LocationInfo file_0 58 2 58 21.
+  Definition loc_164 : location_info := LocationInfo file_0 59 2 59 19.
+  Definition loc_165 : location_info := LocationInfo file_0 59 9 59 17.
+  Definition loc_166 : location_info := LocationInfo file_0 59 9 59 11.
+  Definition loc_167 : location_info := LocationInfo file_0 59 10 59 11.
+  Definition loc_168 : location_info := LocationInfo file_0 59 15 59 17.
+  Definition loc_169 : location_info := LocationInfo file_0 59 16 59 17.
+  Definition loc_170 : location_info := LocationInfo file_0 58 9 58 19.
+  Definition loc_171 : location_info := LocationInfo file_0 58 9 58 14.
+  Definition loc_172 : location_info := LocationInfo file_0 58 10 58 14.
+  Definition loc_173 : location_info := LocationInfo file_0 58 12 58 13.
+  Definition loc_174 : location_info := LocationInfo file_0 58 18 58 19.
+  Definition loc_175 : location_info := LocationInfo file_0 55 9 55 36.
+  Definition loc_176 : location_info := LocationInfo file_0 55 9 55 22.
+  Definition loc_177 : location_info := LocationInfo file_0 55 9 55 22.
+  Definition loc_178 : location_info := LocationInfo file_0 55 26 55 36.
+  Definition loc_179 : location_info := LocationInfo file_0 54 9 54 31.
+  Definition loc_180 : location_info := LocationInfo file_0 54 9 54 23.
+  Definition loc_181 : location_info := LocationInfo file_0 54 9 54 23.
+  Definition loc_182 : location_info := LocationInfo file_0 54 27 54 31.
+  Definition loc_183 : location_info := LocationInfo file_0 53 9 53 35.
+  Definition loc_184 : location_info := LocationInfo file_0 53 9 53 21.
+  Definition loc_185 : location_info := LocationInfo file_0 53 9 53 21.
+  Definition loc_186 : location_info := LocationInfo file_0 53 25 53 35.
+  Definition loc_187 : location_info := LocationInfo file_0 52 31 52 40.
+  Definition loc_188 : location_info := LocationInfo file_0 52 31 52 32.
+  Definition loc_189 : location_info := LocationInfo file_0 52 31 52 32.
+  Definition loc_190 : location_info := LocationInfo file_0 52 35 52 40.
+  Definition loc_191 : location_info := LocationInfo file_0 52 36 52 40.
+  Definition loc_192 : location_info := LocationInfo file_0 52 36 52 40.
+  Definition loc_195 : location_info := LocationInfo file_0 51 32 51 40.
+  Definition loc_196 : location_info := LocationInfo file_0 51 32 51 33.
+  Definition loc_197 : location_info := LocationInfo file_0 51 32 51 33.
+  Definition loc_198 : location_info := LocationInfo file_0 51 36 51 40.
+  Definition loc_199 : location_info := LocationInfo file_0 51 36 51 40.
+  Definition loc_202 : location_info := LocationInfo file_0 50 30 50 38.
+  Definition loc_203 : location_info := LocationInfo file_0 50 30 50 31.
+  Definition loc_204 : location_info := LocationInfo file_0 50 30 50 31.
+  Definition loc_205 : location_info := LocationInfo file_0 50 34 50 38.
+  Definition loc_206 : location_info := LocationInfo file_0 50 34 50 38.
+  Definition loc_209 : location_info := LocationInfo file_0 49 19 49 29.
+  Definition loc_212 : location_info := LocationInfo file_0 48 22 48 28.
 
   (* Definition of function [test1]. *)
   Definition impl_test1 : function := {|
@@ -385,4 +435,43 @@ Section code.
       ]> $∅
     )%E
   |}.
+
+  (* Definition of function [test_bits]. *)
+  Definition impl_test_bits : function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+      ("selecting_bits", it_layout u32);
+      ("mask", it_layout u32);
+      ("clearing_bits", it_layout u32);
+      ("setting_bits", it_layout u32);
+      ("a", it_layout u32)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "mask" <-{ it_layout u32 }
+          LocInfoE loc_212 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_212 (i2v 240 i32))) ;
+        "a" <-{ it_layout u32 }
+          LocInfoE loc_209 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_209 (i2v 305419896 i32))) ;
+        "setting_bits" <-{ it_layout u32 }
+          LocInfoE loc_202 ((LocInfoE loc_203 (use{it_layout u32} (LocInfoE loc_204 ("a")))) |{IntOp u32, IntOp u32} (LocInfoE loc_205 (use{it_layout u32} (LocInfoE loc_206 ("mask"))))) ;
+        "selecting_bits" <-{ it_layout u32 }
+          LocInfoE loc_195 ((LocInfoE loc_196 (use{it_layout u32} (LocInfoE loc_197 ("a")))) &{IntOp u32, IntOp u32} (LocInfoE loc_198 (use{it_layout u32} (LocInfoE loc_199 ("mask"))))) ;
+        "clearing_bits" <-{ it_layout u32 }
+          LocInfoE loc_187 ((LocInfoE loc_188 (use{it_layout u32} (LocInfoE loc_189 ("a")))) &{IntOp u32, IntOp u32} (LocInfoE loc_190 (UnOp NotIntOp (IntOp u32) (LocInfoE loc_191 (use{it_layout u32} (LocInfoE loc_192 ("mask"))))))) ;
+        locinfo: loc_160 ;
+        assert: (LocInfoE loc_183 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_183 ((LocInfoE loc_184 (use{it_layout u32} (LocInfoE loc_185 ("setting_bits")))) ={IntOp u32, IntOp u32} (LocInfoE loc_186 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_186 (i2v 305420024 i32)))))))) ;
+        locinfo: loc_161 ;
+        assert: (LocInfoE loc_179 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_179 ((LocInfoE loc_180 (use{it_layout u32} (LocInfoE loc_181 ("selecting_bits")))) ={IntOp u32, IntOp u32} (LocInfoE loc_182 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_182 (i2v 112 i32)))))))) ;
+        locinfo: loc_162 ;
+        assert: (LocInfoE loc_175 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_175 ((LocInfoE loc_176 (use{it_layout u32} (LocInfoE loc_177 ("clearing_bits")))) ={IntOp u32, IntOp u32} (LocInfoE loc_178 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_178 (i2v 305419784 i32)))))))) ;
+        locinfo: loc_163 ;
+        assert: (LocInfoE loc_170 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_170 ((LocInfoE loc_171 (UnOp NotIntOp (IntOp i32) (LocInfoE loc_172 (UnOp NegOp (IntOp i32) (LocInfoE loc_173 (i2v 2 i32)))))) ={IntOp i32, IntOp i32} (LocInfoE loc_174 (i2v 1 i32)))))) ;
+        locinfo: loc_164 ;
+        assert: (LocInfoE loc_165 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_165 ((LocInfoE loc_166 (UnOp NotIntOp (IntOp i32) (LocInfoE loc_167 (i2v 0 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_168 (UnOp NegOp (IntOp i32) (LocInfoE loc_169 (i2v 1 i32)))))))) ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
 End code.

examples/proofs/tests/generated_proof_test_bits.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tests Require Import generated_code.
+From refinedc.examples.tests Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tests.c]. *)
+Section proof_test_bits.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [test_bits]. *)
+  Lemma type_test_bits :
+    ⊢ typed_function impl_test_bits type_of_test_bits.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "test_bits" ([]) => local_selecting_bits local_mask local_clearing_bits local_setting_bits local_a.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "test_bits" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "test_bits".
+  Qed.
+End proof_test_bits.

examples/proofs/tests/generated_spec.v

@@ -23,4 +23,8 @@ Section spec.
   (* Specifications for function [test_ternary]. *)
   Definition type_of_test_ternary :=
     fn(∀ () : (); True) → ∃ () : (), (void); True.
+
+  (* Specifications for function [test_bits]. *)
+  Definition type_of_test_bits :=
+    fn(∀ () : (); True) → ∃ () : (), (void); True.
 End spec.

examples/proofs/tests/proof_files

 generated_proof_return1.v
 generated_proof_test1.v
+generated_proof_test_bits.v
 generated_proof_test_ternary.v
 generated_proof_unreachable.v

examples/tests.c

@@ -41,3 +41,20 @@ void test_ternary(){
   assert((2 ? 3 : 2) == 3);
   assert((&local != NULL ? (return1() ? return1() : unreachable()) + 3 : 2) == 4);
 }
+
+[[rc::returns("void")]]
+void test_bits() {
+  // resource: https://en.cppreference.com/w/c/language/operator_arithmetic
+  unsigned int mask = 0x00f0; // try uint16_t when issue #34 is fixed
+  unsigned int a = 0x12345678;
+  unsigned int setting_bits = a | mask;
+  unsigned int selecting_bits = a & mask;
+  unsigned int clearing_bits = a & ~mask;
+  assert(setting_bits == 0x123456f8);
+  assert(selecting_bits == 0x70);
+  assert(clearing_bits == 0x12345608);
+
+  // bitwise not on signed integers
+  assert(~(-2) == 1);
+  assert(~0 == -1);
+}

theories/lang/base.v

@@ -757,3 +757,23 @@ Proof.
     rewrite -negb_true_iff -Z.bits_opp; last lia.
     by apply: He.
 Qed.
+
+(** Z.lnot (bitwise negation) for unsigned integers with [bits] bits. *)
+Definition Z_lunot (bits n : Z) := 
+  (Z.lnot n `mod` 2 ^ bits)%Z.
+Typeclasses Opaque Z_lunot.
+
+Lemma Z_lunot_spec bits n k:
+  (0 ≤ k < bits)%Z → Z.testbit (Z_lunot bits n) k = negb (Z.testbit n k).
+Proof.
+  move => [? ?].
+  by rewrite Z.mod_pow2_bits_low ?Z.lnot_spec.
+Qed.
+
+Lemma Z_lunot_range bits n:
+  (0 ≤ bits → 0 ≤ Z_lunot bits n < 2 ^ bits)%Z.
+Proof.
+  move => ?.
+  apply: Z.mod_pos_bound.
+  by apply: Z.pow_pos_nonneg.
+Qed.

theories/lang/lang.v

@@ -847,6 +847,10 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
     val_to_int vs it = Some n →
     val_of_int (-n) it = Some vt →
     eval_un_op NegOp (IntOp it) σ vs vt
+| NotIntOpI it σ vs vt n:
+    val_to_int vs it = Some n →
+    val_of_int (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it = Some vt →
+    eval_un_op NotIntOp (IntOp it) σ vs vt
 .
 
 (*** Evaluation of Expressions *)

theories/typing/int.v

@@ -377,6 +377,35 @@ Section programs.
     TypedUnOpVal v (n @ int it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
     λ T, i2p (type_cast_int n it1 it2 v T).
 
+  Lemma type_not_int n1 it v1 T:
+    let n := if it_signed it then Z.lnot n1 else Z_lunot (bits_per_int it) n1 in
+    (⌜n1 ∈ it⌝ -∗ T (i2v n it) (t2mt (n @ int it))) -∗
+    typed_un_op v1 (v1 ◁ᵥ n1 @ int it)%I (NotIntOp) (IntOp it) T.
+  Proof.
+    iIntros (n) "HT". iIntros (Hv1 Φ) "HΦ".
+    have Hn1 : n1 ∈ it by apply: val_of_int_in_range.
+    iDestruct ("HT" with "[//]") as "HT".
+    have : n ∈ it.
+    { move: Hn1.
+      rewrite /n /elem_of /int_elem_of_it /min_int /max_int.
+      destruct (it_signed it).
+      - rewrite /int_half_modulus /Z.lnot. lia.
+      - rewrite /int_modulus => ?.
+        have -> : ∀ a b, a ≤ b - 1 ↔ a < b by lia.
+        have ? := bits_per_int_gt_0 it.
+        apply Z_lunot_range; lia. }
+    rewrite /n => /val_of_int_is_some [v Hv].
+    move: Hv1 => /val_to_of_int Hv1. rewrite /i2v Hv/=.
+    iApply (wp_unop_det v). iSplit.
+    - iIntros (σ v') "_ !%". split.
+      + by inversion 1; simplify_eq.
+      + move => ->. by econstructor.
+    - iIntros "!>". iApply "HΦ"; last done. by iPureIntro.
+  Qed.
+  Global Instance type_not_int_inst n it v:
+    TypedUnOpVal v (n @ int it)%I NotIntOp (IntOp it) :=
+    λ T, i2p (type_not_int n it v T).
+
   (*** bool *)
   Lemma type_val_bool' b:
     ⊢ (val_of_bool b) ◁ᵥ (b @ boolean bool_it).