Add tests for mutability

kmir/pyproject.toml

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

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.156'
+VERSION: Final = '0.3.157'

kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs

@@ -0,0 +1,31 @@
+use std::cell::RefCell;
+
+struct Counter {
+    value: RefCell<i32>,
+}
+
+impl Counter {
+    fn new(start: i32) -> Self {
+        Counter { value: RefCell::new(start) }
+    }
+
+    fn increment(&self) {
+        *self.value.borrow_mut() += 1;
+    }
+
+    fn get(&self) -> i32 {
+        *self.value.borrow()
+    }
+}
+
+fn main() {
+    let counter = Counter::new(0);
+    // println!("Before: {}", counter.get());
+
+    // We only have &counter, but can still mutate inside
+    counter.increment();
+    counter.increment();
+
+    assert!(2 == counter.get());
+    // println!("After: {}", counter.get());
+}

kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs

@@ -0,0 +1,31 @@
+use std::cell::Cell;
+
+struct Counter {
+    value: Cell<i32>,
+}
+
+impl Counter {
+    fn new(start: i32) -> Self {
+        Counter { value: Cell::new(start) }
+    }
+
+    fn increment(&self) {
+        self.value.set(self.get() + 1);
+    }
+
+    fn get(&self) -> i32 {
+        self.value.get()
+    }
+}
+
+fn main() {
+    let counter = Counter::new(0);
+    // println!("Before: {}", counter.get());
+
+    // We only have &counter, but can still mutate inside
+    counter.increment();
+    counter.increment();
+
+    assert!(2 == counter.get());
+    // println!("After: {}", counter.get());
+}

kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs

@@ -0,0 +1,11 @@
+use std::cell::UnsafeCell;
+
+fn main() {
+    let data = UnsafeCell::new(0);
+
+    unsafe {
+        *data.get() += 42;
+    }
+
+    assert!(data.into_inner() == 42)
+}

kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "interior_mut_fail" ) globalAllocEntry ( 2 , Memory ( allocatio
+│   function: main
+│   span: 288
+│
+│  (138 steps)
+└─ 3 (stuck, leaf)
+    rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p
+    span: 88
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "interior_mut2_fail" ) globalAllocEntry ( 1 , Memory ( allocati
+│   function: main
+│   span: 120
+│
+│  (129 steps)
+└─ 3 (stuck, leaf)
+    rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p
+    span: 50
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "interior_mut3_fail" ) globalAllocEntry ( 1 , Memory ( allocati
+│   function: main
+│   span: 67
+│
+│  (48 steps)
+└─ 3 (stuck, leaf)
+    rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p
+    span: 52
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/ub/mut_const.rs

@@ -0,0 +1,16 @@
+fn main() {
+    let mut prior = 1;
+    let x = 10;
+
+    // println!("Before: {}", x);
+    let _y = &x; // <-- need something else on the stack for the offset to work
+    let prior_mut = &mut prior as *mut i32;
+
+    unsafe {
+        let prior_alias = prior_mut.add(1);
+        *prior_alias = 20;
+    }
+
+    // println!("After: {}", x);
+    assert!(x == 20);
+}

kmir/src/tests/integration/test_integration.py

@@ -438,6 +438,9 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
 PROVING_FILES = list(PROVING_DIR.glob('*.rs'))
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
+    'interior-mut-fail',
+    'interior-mut2-fail',
+    'interior-mut3-fail',
     'assert_eq_exp-fail',
     'bitwise-fail',
 ]

package/version

@@ -1 +1 @@
-0.3.156
+0.3.157