Bitwise operations

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/branch-negative.rs

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

kmir/src/tests/integration/data/prove-rs/shift_negative_min.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/show/bitwise-not-shift-fail.expected

@@ -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/test_integration.py

@@ -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',
 ]
 
 

package/version

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