Bitwise operations (#579)

This PR implements implements bitwise operators and fixing a bug
uncovered doing so.

## Bitwise Operators

Bitwise operators `&` "And", `|` "Or", `^` "Xor":
- `&`, `|`, `^` on integers
- `&`, `|`, `^` on booleans
- `&`, `|`, `^` on borrows (Not completed, stuck on `GlobalAllocs` /
promoteds)
both LHS and RHS of the operation must have the same type.

Shifts `<<` and `>>` are also implemented, although shifts are broken
down into these commands:
- `Shl` shift left with wrapping on overflow
- `Shr` arithmetic shift right with wrapping on overflow
- `ShlUnchecked` shift left with UB on overflow
- `ShrUnchecked` arithmetic shift right with UB on overflow
where overflow is defined as the right hand arg (shift amount) being
greater than the number of bits in the left hand arg.

Concrete proofs are added for the above, borrows are currently failing.

## Bug Found and Fixed

This PR also uncovered a bug we had in how we were handling `Terminator`
`SwitchInt`. This value is _always_ interpreted as an unsigned value
(even if the branching is on a negative value). We were considering the
magnitude of the value, but needed to interpret the bits as unsigned.

---------

Co-authored-by: devops <[email protected]>

Author: dkcumming

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.161"
+version = "0.3.162"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.161'
+VERSION: Final = '0.3.162'

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -321,7 +321,10 @@ block after the call returns.
 ```
 
 A `SwitchInt` terminator selects one of the blocks given as _targets_,
-depending on the value of a _discriminant_.
+depending on the value of a _discriminant_. If the discriminant is an
+an integer, it is always interpretted as the _unsigned_ value (even if
+negative). E.g. if branching is occuring on `-127_i8`, the discriminant
+will be `129`.
 
 ```k
   syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)]
@@ -331,9 +334,9 @@ depending on the value of a _discriminant_.
            #selectBlock(TARGETS, DISCR)
        </k>
 
-  rule <k> #selectBlock(TARGETS, typedValue(Integer(I, _, _), _, _))
+  rule <k> #selectBlock(TARGETS, typedValue(Integer(I, WIDTH, _), _, _))
          =>
-           #execBlockIdx(#selectBlock(I, TARGETS))
+           #execBlockIdx(#selectBlock(bitRangeInt(I, 0, WIDTH), TARGETS))
        ...
        </k>
 

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1155,13 +1155,106 @@ The `unOpNot` operation works on boolean and integral values, with the usual sem
 
 #### Bit-oriented operations
 
-`binOpBitXor`
-`binOpBitAnd`
-`binOpBitOr`
-`binOpShl`
-`binOpShlUnchecked`
-`binOpShr`
-`binOpShrUnchecked`
+Bitwise operations `binOpBitXor`, `binOpBitAnd`, and `binOpBitOr` are valid between integers, booleans, and borrows; but only if the type of left and right arguments is the same.
+
+TODO: Borrows. Stuck on global allocs / promoteds
+
+Shifts are valid on integers if the right argument (the shift amount) is strictly less than the width of the left argument. Right shifts on negative numbers are arithmetic shifts and preserve the sign. There are two variants (checked and unchecked), checked will wrap on overflow and not trigger UB, unchecked will trigger UB on overflow. The UB case currently gets stuck.
+
+```k
+  syntax Bool ::= isBitwise ( BinOp ) [function, total]
+  // --------------------------------------------------
+  rule isBitwise(binOpBitXor)   => true
+  rule isBitwise(binOpBitAnd)   => true
+  rule isBitwise(binOpBitOr)    => true
+  rule isBitwise(_)             => false [owise]
+  rule onInt(binOpBitXor, X, Y) => X xorInt Y
+  rule onInt(binOpBitAnd, X, Y) => X &Int Y
+  rule onInt(binOpBitOr, X, Y)  => X |Int Y
+
+  syntax Bool ::= onBool( BinOp, Bool, Bool ) [function]
+  // ---------------------------------------------------
+  rule onBool(binOpBitXor, X, Y)  => X xorBool Y
+  rule onBool(binOpBitAnd, X, Y)  => X andBool Y
+  rule onBool(binOpBitOr, X, Y)   => X orBool Y
+
+  syntax Bool ::= isShift ( BinOp ) [function, total]
+  // ------------------------------------------------
+  rule isShift(binOpShl)          => true
+  rule isShift(binOpShlUnchecked) => true
+  rule isShift(binOpShr)          => true
+  rule isShift(binOpShrUnchecked) => true
+  rule isShift(_)                 => false [owise]
+
+  syntax Bool ::= isUncheckedShift ( BinOp ) [function, total]
+  // ------------------------------------------------
+  rule isUncheckedShift(binOpShlUnchecked) => true
+  rule isUncheckedShift(binOpShrUnchecked) => true
+  rule isUncheckedShift(_)                 => false [owise]
+
+  syntax Int ::= onShift( BinOp, Int, Int, Int ) [function]
+  // ---------------------------------------------------
+  rule onShift(binOpShl, X, Y, WIDTH)          => (X <<Int Y) modInt (1 <<Int WIDTH)
+  rule onShift(binOpShr, X, Y, WIDTH)          => (X >>Int Y) modInt (1 <<Int WIDTH)
+  rule onShift(binOpShlUnchecked, X, Y, WIDTH) => (X <<Int Y) modInt (1 <<Int WIDTH)
+  rule onShift(binOpShrUnchecked, X, Y, WIDTH) => (X >>Int Y) modInt (1 <<Int WIDTH)
+
+  rule #compute(
+          BOP,
+          typedValue(Integer(ARG1, WIDTH, SIGNED), TY, _),
+          typedValue(Integer(ARG2, WIDTH, SIGNED), TY, _),
+          false) // unchecked
+    =>
+       typedValue(
+          Integer(onInt(BOP, ARG1, ARG2), WIDTH, SIGNED),
+          TY,
+          mutabilityNot
+        )
+    requires isBitwise(BOP)
+    [preserves-definedness]
+
+  rule #compute(
+          BOP,
+          typedValue(BoolVal(ARG1), TY, _),
+          typedValue(BoolVal(ARG2), TY, _),
+          false) // unchecked
+    =>
+       typedValue(
+          BoolVal(onBool(BOP, ARG1, ARG2)),
+          TY,
+          mutabilityNot
+        )
+    requires isBitwise(BOP)
+    [preserves-definedness]
+
+  rule #compute(
+          BOP,
+          typedValue(Integer(ARG1, WIDTH, false), TY, _),
+          typedValue(Integer(ARG2, _, _), _, _),
+          false) // unchecked
+    =>
+       typedValue(
+          Integer(truncate(onShift(BOP, ARG1, ARG2, WIDTH), WIDTH, Unsigned), WIDTH, false),
+          TY,
+          mutabilityNot
+        )
+    requires isShift(BOP) andBool ((notBool isUncheckedShift(BOP)) orBool ARG2 <Int WIDTH)
+    [preserves-definedness]
+
+  rule #compute(
+          BOP,
+          typedValue(Integer(ARG1, WIDTH, true), TY, _),
+          typedValue(Integer(ARG2, _, _), _, _),
+          false) // unchecked
+    =>
+       typedValue(
+          Integer(truncate(onShift(BOP, ARG1, ARG2, WIDTH), WIDTH, Signed), WIDTH, true),
+          TY,
+          mutabilityNot
+        )
+    requires isShift(BOP) andBool ((notBool isUncheckedShift(BOP)) orBool ARG2 <Int WIDTH)
+    [preserves-definedness]
+```
 
 
 #### Nullary operations for activating certain checks

kmir/src/tests/integration/data/prove-rs/bitwise-not-shift-fail.rs

@@ -0,0 +1,22 @@
+fn main() {
+    // Integers
+    assert!(3_u128 & 7_u128 == 3_u128);
+    assert!(3_u128 | 7_u128 == 7_u128);
+    assert!(3_u128 ^ 7_u128 == 4_u128);
+
+    // Booleans
+    assert!(false | false == false);
+    assert!(true | false == true);
+    assert!(true & true == true);
+    assert!(true & false == false);
+    assert!(true ^ true == false);
+    assert!(true ^ false == true);
+
+    // Borrows
+    assert!(&3 & &7 == 3);
+    assert!(&3 | &7 == 7);
+    assert!(&3 ^ &7 == 4);
+    assert!(&false & &false == false);
+    assert!(&true | &true == true);
+    assert!(&false ^ &false == false);
+}

kmir/src/tests/integration/data/prove-rs/bitwise-shift.rs

@@ -0,0 +1,44 @@
+fn main() {
+    // Shl basic
+    assert!(1_u8 << 3_u8 == 8);
+    assert!(1_u8 << 3_i8 == 8); // Negative on RHS if in 0..size
+    assert!(1_i8 << 3_u8 == 8);
+    assert!(1_i8 << 3_i8 == 8);
+    assert!(1_i8 << 7_u8 == -128_i8);
+
+    // Shl Overflow
+    assert!(255_u8 << 1_u8 == 254);   
+    assert!(-127_i8 << 1_u8 == 2);   
+    // assert!(-128_i8 << -1_i8 == 2); // Shift must be in 0..size   
+    // assert!(0_u8 << 8_u8 == 0);     // Shift must be in 0..size   
+
+    // Shr basic
+    assert!(24_u8 >> 3_u8 == 3);
+    assert!(24_u8 >> 3_i8 == 3); // Negative on RHS if in 0..size
+    assert!(24_i8 >> 3_u8 == 3);
+    assert!(24_i8 >> 3_i8 == 3);
+
+    // Shr Overflow
+    assert!(255_u8 >> 1_u8 == 127);   
+    assert!(-127_i8 >> 1_u8 == -64);   // Arithmetic shift sign extends   
+    // assert!(-128_i8 >> -1_i8 == 2); // Shift must be in 0..size   
+    // assert!(0_u8 >> 8_u8 == 0);     // Shift must be in 0..size   
+
+    // ShlUnchecked basic
+    assert!(1_u8.wrapping_shl(3_u32) == 8_u8); // RHS must be u32
+
+    // ShlUnchecked Overflow
+    assert!(255_u8.wrapping_shl(1_u32) == 254_u8);
+    assert!(128_u8.wrapping_shl(1_u32) == 0_u8);
+    assert!((-128_i8).wrapping_shl(3_u32) == 0_i8);
+    assert!((-127_i8).wrapping_shl(3_u32) == 8_i8);
+
+    // ShrUnchecked basic
+    assert!(32_u8.wrapping_shr(2_u32) == 8_u8); // RHS must be u32
+
+    // ShlUnchecked Overflow
+    assert!(255_u8.wrapping_shr(1_u32) == 127_u8);
+    assert!(128_u8.wrapping_shr(1_u32) == 64_u8);
+    assert!((-128_i8).wrapping_shr(3_u32) == -16_i8);
+    assert!((-127_i8).wrapping_shr(1_u32) == -64_i8);
+}

kmir/src/tests/integration/data/prove-rs/bitwise-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/bitwise.rs

@@ -0,0 +1,3 @@
+fn main() {
+    assert!((1_i8 << 7) + 1 == -127_i8);
+}

kmir/src/tests/integration/data/prove-rs/branch-negative.rs

@@ -0,0 +1,13 @@
+fn main() {
+    assert!(1_i8   <<   7_u8 == -128);
+    assert!(1_i16  <<  15_u8 == -32768);
+    assert!(1_i32  <<  31_u8 == -2147483648);
+    assert!(1_i64  <<  63_u8 == -9223372036854775808);
+    assert!(1_i128 << 127_u8 == -170141183460469231731687303715884105728);
+
+    assert!(1_i8   <<   7_u8 ==   i8::MIN);
+    assert!(1_i16  <<  15_u8 ==  i16::MIN);
+    assert!(1_i32  <<  31_u8 ==  i32::MIN);
+    assert!(1_i64  <<  63_u8 ==  i64::MIN);
+    assert!(1_i128 << 127_u8 == i128::MIN);
+}

kmir/src/tests/integration/data/prove-rs/shift_negative_min.rs

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "bitwise_not_shift_fail" ) globalAllocEntry ( 8 , Memory ( allo
+│   function: main
+│   span: 108
+│
+│  (254 steps)
+└─ 3 (stuck, leaf)
+    #readProjection ( typedValue ( Any , ty ( 25 ) , mutabilityNot ) , projectionEle
+    span: 63
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift-fail.expected

@@ -434,7 +434,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
     'interior-mut2-fail',
     'interior-mut3-fail',
     'assert_eq_exp-fail',
-    'bitwise-fail',
+    'bitwise-not-shift-fail',
 ]
 
 

kmir/src/tests/integration/test_integration.py

@@ -1 +1 @@
-0.3.161
+0.3.162