From 6a3845a7917edafe087f3cd939c6b4a97b924c0a Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 15:57:26 -0400 Subject: [PATCH 01/11] Added test that uses pointer addition --- kmir/src/tests/integration/data/ub/mut_const.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 kmir/src/tests/integration/data/ub/mut_const.rs diff --git a/kmir/src/tests/integration/data/ub/mut_const.rs b/kmir/src/tests/integration/data/ub/mut_const.rs new file mode 100644 index 000000000..b58d0dd8e --- /dev/null +++ b/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); +} From 4aa80cf6d45bf6bdbddb06bb3640c3c2afe017cb Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 16:11:24 -0400 Subject: [PATCH 02/11] Added failing RefCell test for interior mutability --- .../data/prove-rs/interior-mut-fail.rs | 31 +++++++++++++++++++ .../prove-rs/show/interior-mut-fail.expected | 16 ++++++++++ .../src/tests/integration/test_integration.py | 1 + 3 files changed, 48 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs new file mode 100644 index 000000000..4be7fe1e8 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs @@ -0,0 +1,31 @@ +use std::cell::RefCell; + +struct Counter { + value: RefCell, +} + +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()); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected new file mode 100644 index 000000000..9f8318b70 --- /dev/null +++ b/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 + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 0865d7290..4cef5dc53 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -438,6 +438,7 @@ 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' ] From 84db6d39c3f4f793646e7ade56ea7aafd3d94404 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 16:23:48 -0400 Subject: [PATCH 03/11] make format --- kmir/src/tests/integration/test_integration.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 4cef5dc53..390c014ab 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -436,10 +436,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) PROVING_FILES = list(PROVING_DIR.glob('*.rs')) -PROVE_RS_SHOW_SPECS = [ - 'local-raw-fail', - 'interior-mut-fail' -] +PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail'] @pytest.mark.parametrize( From 622eb8ffa5516b643993df0c9546d9f3ddc6fa6d Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 16:32:03 -0400 Subject: [PATCH 04/11] Added interior mut with Cell --- .../data/prove-rs/interior-mut2-fail.rs | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs new file mode 100644 index 000000000..060085bb2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs @@ -0,0 +1,31 @@ +use std::cell::Cell; + +struct Counter { + value: Cell, +} + +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()); +} From 201527de7ffb74c50c78e77262889c0f6a9e88c9 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 16:38:36 -0400 Subject: [PATCH 05/11] Added show output for interior-mut2-fail.rs --- .../prove-rs/show/interior-mut2-fail.expected | 16 ++++++++++++++++ kmir/src/tests/integration/test_integration.py | 2 +- 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected new file mode 100644 index 000000000..ef75df1fd --- /dev/null +++ b/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 + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 390c014ab..e2dbb1754 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -436,7 +436,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) PROVING_FILES = list(PROVING_DIR.glob('*.rs')) -PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail'] +PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail'] @pytest.mark.parametrize( From 8b2c3bf7b7314de9457905547246589877a3f928 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 17:01:31 -0400 Subject: [PATCH 06/11] Added interior mutability test with UnsafeCell --- .../data/prove-rs/interior-mut3-fail.rs | 11 +++++++++++ .../prove-rs/show/interior-mut3-fail.expected | 16 ++++++++++++++++ kmir/src/tests/integration/test_integration.py | 2 +- 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs new file mode 100644 index 000000000..62411c969 --- /dev/null +++ b/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) +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected new file mode 100644 index 000000000..7cdfd662c --- /dev/null +++ b/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 + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index e2dbb1754..97cf28170 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -436,7 +436,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) PROVING_FILES = list(PROVING_DIR.glob('*.rs')) -PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail'] +PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail', 'interior-mut3-fail'] @pytest.mark.parametrize( From ac342de6f950b8d10ca1746394f26c36b336eb5e Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 8 May 2025 16:11:24 -0400 Subject: [PATCH 07/11] Formatting the tests listed in the prove show harness --- kmir/src/tests/integration/test_integration.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 97cf28170..487c7898a 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -436,7 +436,12 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) PROVING_FILES = list(PROVING_DIR.glob('*.rs')) -PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail', 'interior-mut3-fail'] +PROVE_RS_SHOW_SPECS = [ + 'local-raw-fail', + 'interior-mut-fail', + 'interior-mut2-fail', + 'interior-mut3-fail', +] @pytest.mark.parametrize( From 9f19fa2edb2e28e701490d62406a88666323fb04 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 9 May 2025 12:19:03 -0400 Subject: [PATCH 08/11] debugging --- .github/workflows/test.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index eda33a37e..ce145da4b 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -27,6 +27,7 @@ jobs: version: 0.7.2 - name: 'Update version' run: | + echo "${GITHUB_BASE_REF}" og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) ./package/version.sh bump ${og_version} ./package/version.sh sub From 37cc012b3714ace7024393b7aa7c50384e574460 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 May 2025 16:19:21 +0000 Subject: [PATCH 09/11] Set Version: 0.3.154 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index fe869ab1a..040fd58f2 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.153" +version = "0.3.154" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 0bab6a575..b3414ef65 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.153' +VERSION: Final = '0.3.154' diff --git a/kmir/uv.lock b/kmir/uv.lock index 5786f2a36..6f0c754dd 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.153" +version = "0.3.154" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index 77577f00e..589f2dfa3 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.153 +0.3.154 From e0047646ac3f45576d244f82e3266aa601fc4a56 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 9 May 2025 12:21:02 -0400 Subject: [PATCH 10/11] removed debug logging --- .github/workflows/test.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index ce145da4b..eda33a37e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -27,7 +27,6 @@ jobs: version: 0.7.2 - name: 'Update version' run: | - echo "${GITHUB_BASE_REF}" og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) ./package/version.sh bump ${og_version} ./package/version.sh sub From 617b07447619ff2c4ff7a3c4152215e0ab275c10 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 May 2025 21:21:33 +0000 Subject: [PATCH 11/11] Set Version: 0.3.157 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 2c90be104..a15931f5a 100644 --- a/kmir/pyproject.toml +++ b/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 = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index f419c1a14..11b8242a1 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.156' +VERSION: Final = '0.3.157' diff --git a/kmir/uv.lock b/kmir/uv.lock index f2892868f..2b98ee015 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.156" +version = "0.3.157" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index 59fc32593..a03f12adb 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.156 +0.3.157