allow wrapping versions of binops in semantics

theories/lang/lang.v

@@ -450,6 +450,15 @@ Proof.
     + rewrite /int_modulus /bits_per_int in HM. lia.
 Qed.
 
+Lemma it_in_range_mod n it:
+  n ∈ it → it_signed it = false →
+  n `mod` int_modulus it = n.
+Proof.
+  move => [??] ?. rewrite Z.mod_small //.
+  destruct it as [? []] => //. unfold min_int, max_int in *. simpl in *.
+  lia.
+Qed.
+
 Fixpoint val_to_loc_go (v : val) (pos : nat) (l : loc) : option loc :=
   match v with
   | (MPtrFrag l' pos')::v' =>
@@ -765,8 +774,6 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
     (* TODO: What is the right int type of the result here? C seems to
     use i32 but maybe we don't want to hard code that. *)
     eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
-(* This defines checked versions of the arithmetic operations which
-are UB if the result is out of bounds for it. *)
 | ArithOpII op v1 v2 σ n1 n2 it n v:
     match op with
     | AddOp => Some (n1 + n2)
@@ -777,7 +784,7 @@ are UB if the result is out of bounds for it. *)
     which round towards floor)*)
     | DivOp => if n2 is 0 then None else Some (n1 `quot` n2)
     | ModOp => if n2 is 0 then None else Some (n1 `rem` n2)
-    (* TODO: Figure out if these are the operations we want *)
+    (* TODO: Figure out if these are the operations we want and what sideconditions they have *)
     | AndOp => Some (Z.land n1 n2)
     | OrOp => Some (Z.lor n1 n2)
     | XorOp => Some (Z.lxor n1 n2)
@@ -787,7 +794,7 @@ are UB if the result is out of bounds for it. *)
     end = Some n →
     val_to_int v1 it = Some n1 →
     val_to_int v2 it = Some n2 →
-    val_of_int n it = Some v →
+    val_of_int (if it_signed it then n else n `mod` int_modulus it) it = Some v →
     eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
 .
 

theories/typing/int.v

@@ -150,11 +150,18 @@ Section programs.
     iIntros (Hop) "HT". iIntros (Hv1 Hv2 Φ) "HΦ".
     iDestruct ("HT" with "[] []" ) as ([v Hv]%val_of_int_is_some) "HT".
     1-2: iPureIntro; by apply: val_of_int_in_range.
+    move: (Hv) => /val_of_int_in_range ?.
     move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. rewrite /i2v Hv/=.
     iApply (wp_binop_det v). iSplit.
-    { iIntros (σ v') "_ !%". split; last (move => ->; destruct op; by econstructor).
-      destruct op => //; inversion 1; by simplify_eq. }
-    iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.
+    - iIntros (σ v') "_ !%". split.
+      + destruct op => //.
+        all: inversion 1; simplify_eq/=.
+        all: destruct it as [? []]; simplify_eq/= => //.
+        all: by rewrite ->it_in_range_mod in * => //; simplify_eq.
+      + move => ->; destruct op => //; econstructor => //.
+        all: destruct it as [? []]; simplify_eq/= => //.
+        all: by rewrite it_in_range_mod; simplify_eq/=.
+    - iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.
   Qed.
   Lemma type_arithop_int_int_div_mod it v1 n1 v2 n2 T n op:
     match op with
@@ -168,12 +175,18 @@ Section programs.
     iIntros (Hop) "HT". iIntros (Hv1 Hv2 Φ) "HΦ".
     iDestruct ("HT" with "[] []" ) as (Hn [v Hv]%val_of_int_is_some) "HT".
     1-2: iPureIntro; by apply: val_of_int_in_range.
+    move: (Hv) => /val_of_int_in_range ?.
     move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. rewrite /i2v Hv/=.
     iApply (wp_binop_det v). iSplit.
-    { iIntros (σ v') "_ !%".
-      split; last (move => ->; destruct op; econstructor => //; by case_match).
-      destruct op => //; inversion 1; simplify_eq; case_match; by simplify_eq. }
-    iApply "HΦ"; last done. by iPureIntro.
+    - iIntros (σ v') "_ !%". split.
+      + destruct op => //.
+        all: inversion 1; destruct n2; simplify_eq/=.
+        all: destruct it as [? []]; simplify_eq/= => //.
+        all: by rewrite ->it_in_range_mod in * => //; simplify_eq.
+      + move => ->; destruct op, n2 => //; econstructor => // => //.
+        all: destruct it as [? []]; simplify_eq/= => //.
+        all: by rewrite it_in_range_mod; simplify_eq/=.
+    - iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.
   Qed.
   Global Program Instance type_add_int_int_inst it v1 n1 v2 n2:
     TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I AddOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1 + n2) _ _).