update operational semantics for shift operators

theories/lang/lang.v

@@ -919,14 +919,24 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
     (* we need to take `quot` and `rem` here for the correct rounding
     behavior, i.e. rounding towards 0 (instead of `div` and `mod`,
     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 and what sideconditions they have *)
+    | DivOp => if decide (n2 = 0) then None else Some (n1 `quot` n2)
+    | ModOp => if decide (n2 = 0) then None else Some (n1 `rem` n2)
     | AndOp => Some (Z.land n1 n2)
     | OrOp => Some (Z.lor n1 n2)
     | XorOp => Some (Z.lxor n1 n2)
-    | ShlOp => Some (n1 ≪ n2)
-    | ShrOp => Some (n1 ≫ n2)
+    (* For shift operators (`ShlOp` and `ShrOp`), without considering integer promotions,
+       behaviors are defined if:
+       - lhs is nonnegative, and
+       - rhs does not exceed the number of bits in lhs. *)
+    (* In other words, behaviors are undetermined if any of the below happens:
+       - lhs is negative (for `>>`: implementation-defined)
+       - rhs is negative
+       - rhs is greater or equal the number of bits in lhs *)
+    | ShlOp => if decide (n1 < 0 ∨ n2 < 0 ∨ bits_per_int it ≤ n2) then None else Some (n1 ≪ n2)
+    (* NOTE: when lhs is negative, Coq's `≫` is not semantically equivalent to C's `>>`.
+       Counterexample: Coq `-1000 ≫ 10 = 0`; C `-1000 >> 10 == -1`.
+       This is because `≫` is implemented by `Z.div`. *)
+    | ShrOp => if decide (n1 < 0 ∨ n2 < 0 ∨ bits_per_int it ≤ n2) then None else Some (n1 ≫ n2)
     | _ => None
     end = Some n →
     val_to_int v1 it = Some n1 →

theories/typing/int.v

@@ -344,13 +344,14 @@ Section programs.
     iApply (wp_binop_det v). iSplit.
     - iIntros (σ v') "_ !%". split.
       + destruct op => //.
-        all: inversion 1; destruct n2; simplify_eq/=.
+        all: inversion 1; simplify_eq/=.
+        4,5,9,10: rewrite decide_False in H1; last lia.
         all: destruct it as [? []]; simplify_eq/= => //.
         all: try by rewrite ->it_in_range_mod in * => //; simplify_eq.
-      + move => ->; destruct op, n2 => //; econstructor => // => //.
+      + move => ->; destruct op => //; econstructor => // => //.
+        4,6,11,13: by inversion Hsc; rewrite decide_False; last lia => //.
         all: destruct it as [? []]; simplify_eq/= => //.
-        all: try by rewrite it_in_range_mod; simplify_eq/=.
-        all: by destruct_and!.
+        all: try by rewrite it_in_range_mod.
     - iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.
   Qed.
   Global Program Instance type_add_int_int_inst it v1 n1 v2 n2: