From b457186be53f6eb23e6c7f6119a011da5a39e3f5 Mon Sep 17 00:00:00 2001 From: Zejun Zhao Date: Sat, 5 Sep 2026 12:07:23 +0800 Subject: [PATCH] Verify atomic conversions and operation wrappers Add an independent Challenge 7 proof package with complete type and ordering coverage, ownership and invariant rejection controls, and an ARM64 macOS CI job. Build the explicit VeriFast update from pinned release inputs and preserve the library runtime source. Co-authored-by: GPT-6 --- .github/workflows/verifast-atomics.yml | 58 + .../core/sync/atomic.rs/.gitattributes | 2 + .../core/sync/atomic.rs/.gitignore | 16 + verifast-proofs/core/sync/atomic.rs/README.md | 116 ++ verifast-proofs/core/sync/atomic.rs/check.py | 32 + .../sync/atomic.rs/checks/decoder/check.py | 99 ++ .../checks/decoder/intrinsic-gate.rs | 12 + .../atomic.rs/checks/decoder/original-mir.txt | 603 ++++++++ .../atomic.rs/checks/operations/annotate.py | 30 + .../checks/operations/build-controls.py | 124 ++ .../atomic.rs/checks/operations/positive.rs | 79 ++ .../sync/atomic.rs/checks/operations/run.py | 73 + .../operations/unsized-domain-rejected.rs | 8 + .../sync/atomic.rs/checks/refinement/check.py | 36 + .../refinement/rc-integer-original/lib.rs | 10 + .../refinement/rc-integer-verified/lib.rs | 13 + .../checks/refinement/rc-original/lib.rs | 25 + .../refinement/rc-other-original/lib.rs | 15 + .../refinement/rc-other-verified/lib.rs | 18 + .../checks/refinement/rc-positive/lib.rs | 40 + .../checks/refinement/rc-wrong-order/lib.rs | 40 + .../source/alignment-generic-negative.rs | 7 + .../source/alignment-generic64-negative.rs | 9 + .../source/alignment-minimum-positive.rs | 7 + .../checks/source/alignment-positive.rs | 9 + .../checks/source/alignment-wrong-negative.rs | 7 + .../sync/atomic.rs/checks/source/check.py | 37 + .../checks/source/double-convert-negative.rs | 141 ++ .../checks/source/double-recover-negative.rs | 141 ++ .../checks/source/macro-second-negative.rs | 11 + .../checks/source/own-sharing-usize.rs | 134 ++ .../checks/source/self-free-negative.rs | 13 + .../atomic.rs/checks/source/self-positive.rs | 24 + .../core/sync/atomic.rs/proof/check.py | 75 + .../core/sync/atomic.rs/proof/generate.py | 104 ++ .../proof/templates/atomic-ptr-share.rs | 94 ++ .../atomic.rs/proof/templates/from-ptr.rs | 23 + .../proof/templates/integer-share.rs | 69 + .../sync/atomic.rs/proof/templates/lib.rs | 5 + .../core/sync/atomic.rs/source-lock.json | 8 + .../core/sync/atomic.rs/toolchain/build.py | 143 ++ .../sync/atomic.rs/toolchain/provenance.json | 42 + .../verifast-26.01-atomic-source.patch | 1214 +++++++++++++++++ 43 files changed, 3766 insertions(+) create mode 100644 .github/workflows/verifast-atomics.yml create mode 100644 verifast-proofs/core/sync/atomic.rs/.gitattributes create mode 100644 verifast-proofs/core/sync/atomic.rs/.gitignore create mode 100644 verifast-proofs/core/sync/atomic.rs/README.md create mode 100644 verifast-proofs/core/sync/atomic.rs/check.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/decoder/check.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/decoder/intrinsic-gate.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/decoder/original-mir.txt create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/operations/annotate.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/operations/build-controls.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/operations/positive.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/operations/run.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/operations/unsized-domain-rejected.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/check.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-original/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-verified/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-original/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-original/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-verified/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-positive/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-wrong-order/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic64-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/alignment-minimum-positive.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/alignment-positive.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/alignment-wrong-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/check.py create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/double-convert-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/double-recover-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/macro-second-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/own-sharing-usize.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/self-free-negative.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/checks/source/self-positive.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/check.py create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/generate.py create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/templates/atomic-ptr-share.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/templates/from-ptr.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/templates/integer-share.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/proof/templates/lib.rs create mode 100644 verifast-proofs/core/sync/atomic.rs/source-lock.json create mode 100644 verifast-proofs/core/sync/atomic.rs/toolchain/build.py create mode 100644 verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json create mode 100644 verifast-proofs/core/sync/atomic.rs/toolchain/verifast-26.01-atomic-source.patch diff --git a/.github/workflows/verifast-atomics.yml b/.github/workflows/verifast-atomics.yml new file mode 100644 index 0000000000000..b6144c0c90e49 --- /dev/null +++ b/.github/workflows/verifast-atomics.yml @@ -0,0 +1,58 @@ +name: VeriFast atomics + +on: + workflow_dispatch: + merge_group: + pull_request: + branches: [main] + push: + paths: + - 'library/core/src/sync/atomic.rs' + - 'library/core/src/intrinsics/mod.rs' + - 'rust-toolchain.toml' + - 'verifast-proofs/core/sync/atomic.rs/**' + - '.github/workflows/verifast-atomics.yml' + +permissions: + contents: read + +jobs: + atomics: + name: Atomic safety including 128-bit types + runs-on: macos-14 + timeout-minutes: 30 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Install pinned Rust compiler components + run: rustup toolchain install nightly-2025-11-25 --profile minimal --component rustc-dev,llvm-tools-preview,rust-src + - name: Cache verified download inputs and Cargo dependencies + uses: actions/cache@v4 + with: + path: | + ${{ runner.temp }}/atomic-downloads + ${{ runner.temp }}/atomic-cargo + key: atomic-build-macos-arm64-${{ hashFiles('verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json') }} + - name: Build experimental VeriFast and check the complete atomic scope + run: >- + python3 verifast-proofs/core/sync/atomic.rs/toolchain/build.py + --workdir "$RUNNER_TEMP/atomic-build" + --downloads "$RUNNER_TEMP/atomic-downloads" + --cargo-home "$RUNNER_TEMP/atomic-cargo" + --check + - name: Upload proof coverage, generated sources, and build evidence + if: always() + uses: actions/upload-artifact@v4 + with: + name: atomic-safety-evidence + path: | + ${{ runner.temp }}/atomic-build/build-manifest.json + ${{ runner.temp }}/atomic-build/*.log + verifast-proofs/core/sync/atomic.rs/proof/*.log + verifast-proofs/core/sync/atomic.rs/proof/coverage.json + verifast-proofs/core/sync/atomic.rs/proof/verified/*.rs + verifast-proofs/core/sync/atomic.rs/proof/normalized-original/*.rs + verifast-proofs/core/sync/atomic.rs/checks/**/*.log + verifast-proofs/core/sync/atomic.rs/checks/operations/results.json diff --git a/verifast-proofs/core/sync/atomic.rs/.gitattributes b/verifast-proofs/core/sync/atomic.rs/.gitattributes new file mode 100644 index 0000000000000..74a97ccb7a385 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/.gitattributes @@ -0,0 +1,2 @@ +# Preserve release-relative patch bytes, including CRLF and context whitespace. +toolchain/verifast-26.01-atomic-source.patch -text -whitespace diff --git a/verifast-proofs/core/sync/atomic.rs/.gitignore b/verifast-proofs/core/sync/atomic.rs/.gitignore new file mode 100644 index 0000000000000..884677216dca5 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/.gitignore @@ -0,0 +1,16 @@ +__pycache__/ +*.log +*.rmeta +*.rlib +*.o +/proof/original/ +/proof/normalized-original/ +/proof/verified/ +/proof/clients*.rs +/proof/coverage.json +/checks/operations/*.rs +!/checks/operations/positive.rs +!/checks/operations/unsized-domain-rejected.rs +/checks/operations/results.json +/checks/decoder/replay-runtime/ +/checks/decoder/replay-fixtures/ diff --git a/verifast-proofs/core/sync/atomic.rs/README.md b/verifast-proofs/core/sync/atomic.rs/README.md new file mode 100644 index 0000000000000..a4c7f5f3ca1bf --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/README.md @@ -0,0 +1,116 @@ +# Challenge 7: atomic safety + +This is an independently authored proposed solution for +[Challenge 7](https://github.com/model-checking/verify-rust-std/issues/83). It uses +VeriFast with the explicit source update in `toolchain/`. VeriFast is an approved +tool; this particular update is unreleased and requires review. Passing this +directory's checks does not by itself establish committee acceptance. + +## Verified scope + +| Requirement | Proof and enforced coverage | +| --- | --- | +| `from_ptr` | Bool, generic Ptr, all signed/unsigned 8/16/32/64/128-bit types, and Isize/Usize: all 14 bodies must appear in verifier output. | +| Pointer values and element sizes | The pointer proof is generic over sized `T`, with arbitrary stored addresses. Concrete intrinsic callers also cover element sizes 0, 1, 2, 3, and 4. | +| Unsafe operation wrappers | All 15 current wrappers, including signed minimum and both compare-exchange variants. | +| Intrinsics | All 91 legal ordering combinations of the 15 current const-generic intrinsics, matched to the challenge's order-suffixed names. | +| Panic paths | Invalid load/store and compare-exchange failure orderings execute the real panic paths and preserve atomic permissions on unwind. | +| Source connection | Pinned source digests, complete module refinement after documented metadata preparation, and explicit coverage checks. | + +The proof covers the challenge's required unsafe functions. It does not claim +that every public safe method in the atomic module has been verified. Optional +panic-avoidance contracts for those public methods are not part of this solution. +No runtime implementation in `library/` is changed. + +## Ownership and validity + +`from_ptr` accepts either initialized ordinary ownership or an existing atomic +share. A ghost boolean selects the permission path. Fresh conversion borrows +the ordinary storage for the returned reference's lifetime and retains a unique +recovery token. Reusing a share creates no recovery token. Both paths return +sharing and reference-initialization permissions. Fourteen concrete callers +each create and use two references to the same storage. + +The sharing interpretation contains a fractional lifetime borrow of typed +atomic ownership. Integers and raw pointers accept all values of their type; +the boolean interpretation accepts only bytes 0 and 1. Ordinary ownership +establishes allocation validity and initialization. Atomic ownership additionally +requires actual atomic alignment and excludes conflicting ordinary or mixed-size +accesses through the verifier's existing atomic-mask model. Splitting the +atomic resource permits concurrent atomic access; converting it back requires +recovering its complete permission and ending the relevant borrow. + +Intrinsic contracts require the correct operand domain. `T: Copy` alone is +insufficient. Integer updates use the same integer type; pointer updates use +`usize`; signed and unsigned min/max have separate domains. Pointer-domain +lemmas require a sized pointee. Stores, swaps, and compare-exchanges require a +valid new value. Arithmetic and bitwise updates require a proved closure witness +carrying the operand type identities, operation, invariant, and update value. +Boolean AND/OR/XOR witnesses pass; invariant-breaking NAND/addition witnesses +fail. Loads preserve validity and may use a resource derived from fractional +ordinary ownership. Writes require a resource derived from full ordinary ownership. + +## Trusted boundary and source preparation + +The trusted boundary consists of Rust's primitive atomic semantics, VeriFast's +existing RustBelt lifetime/atomic model, the primitive contracts added by the +patch, and rustc's exported ABI layout. The model proves safety under its +permissions and invariants; it does not establish general concurrent functional +correctness or a hardware memory-model theorem. + +The patch adds concrete atomic-order translation, operand guards, compiler +resolved `Self`, propagation of macro contracts to every expansion, and +compiler-derived struct alignment. Generic `repr(align(N))` supplies a minimum +alignment and divisibility fact, not an assertion of exact alignment. The +primitive update model includes explicit u8 equations and restricted boolean-byte +value tables. Those primitive facts remain reviewable trusted contracts. + +`source-lock.json` pins both the atomic implementation and intrinsic declarations. +The generator copies the current complete atomic module and replaces its 18 +`rustc_diagnostic_item` attributes with documentation attributes in both proof +inputs. This prevents duplicate diagnostic items when checking the module beside +the compiler's `core` dependency. The refinement claim is between these prepared +inputs. In the verified input, the existing reference expression is assigned to +a local result variable to attach ghost steps; whole-module refinement checks +that transformation. All other executable code is preserved. + +No reference-creation check, unwind path, or dead-code check is disabled. No false +precondition skips required types or orderings. Negative controls reject invalid +types/orderings, missing domain or closure witnesses, ordinary/fractional write +permissions, invalid boolean values, uninitialized conversion, and duplicate +ownership/recovery. Isolated mutated-MIR decoder tests are not counted as Rust +proofs; their replay exporter is never used in the real proof runtime. + +## Reproduction + +Use native ARM64 macOS with Python 3.12 or newer and the pinned Rust toolchain: + +```sh +rustup toolchain install nightly-2025-11-25 --profile minimal --component rustc-dev,llvm-tools-preview,rust-src +python3 verifast-proofs/core/sync/atomic.rs/toolchain/build.py \ + --workdir /tmp/atomic-build \ + --downloads /tmp/atomic-downloads \ + --cargo-home /tmp/atomic-cargo \ + --check +``` + +The build directory must not exist. Archives and the patch are checked against +pinned SHA-256 digests. The decoder revision and Cargo dependency locks are +pinned. The script extracts fresh sources/dependencies, builds the verifier, +refinement checker, and Rust MIR exporter, then runs all proof and rejection +checks. It writes logs, a build manifest, and a relocation wrapper in that build +directory. `--offline` is supported when all archive and Cargo inputs are cached. + +The dedicated GitHub workflow uses `macos-14` because the pinned x86_64 Linux +target does not expose 128-bit atomics, including with `cmpxchg16b` enabled. The +proof runner fails if either 128-bit instantiation is missing. GitHub documents +`macos-14` as an ARM64 standard runner in its +[runner reference](https://docs.github.com/en/actions/reference/runners/github-hosted-runners). + +The CI artifact includes the generated proof sources, per-function coverage, +control results, and fresh-build manifest. To rerun checks using a built runtime: + +```sh +/tmp/atomic-build/with-build-env python3 verifast-proofs/core/sync/atomic.rs/check.py \ + /tmp/atomic-build/verifast-26.01/bin +``` diff --git a/verifast-proofs/core/sync/atomic.rs/check.py b/verifast-proofs/core/sync/atomic.rs/check.py new file mode 100644 index 0000000000000..323db8232fa47 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/check.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +"""Run every safety, source-connection, and negative-control gate for atomics.""" +from pathlib import Path +import json +import subprocess +import sys + +if len(sys.argv) != 2: + raise SystemExit('usage: check.py /absolute/path/to/experimental-runtime/bin') +base = Path(__file__).resolve().parent +runtime = Path(sys.argv[1]).resolve() +checks = [ + ('source and fresh/shared callers', base / 'proof/check.py', runtime), + ('compiler/layout/ownership controls', base / 'checks/source/check.py', runtime / 'verifast'), + ('intrinsic types, orderings, and invariants', base / 'checks/operations/run.py', runtime / 'verifast'), + ('ordering refinement controls', base / 'checks/refinement/check.py', runtime / 'refinement-checker'), +] +for name, script, argument in checks: + print('Checking ' + name, flush=True) + subprocess.run([sys.executable, str(script), str(argument)], check=True) +provenance = json.loads((base / 'toolchain/provenance.json').read_text()) +schema = runtime.parent.parent / provenance['source_archive_prefix'] / 'src/rust_frontend/vf_mir/vf_mir.capnp' +print('Checking malformed MIR with an isolated replay exporter', flush=True) +subprocess.run([sys.executable, str(base / 'checks/decoder/check.py'), str(runtime), str(schema)], check=True) +coverage = json.loads((base / 'proof/coverage.json').read_text()) +operations = json.loads((base / 'checks/operations/results.json').read_text()) +assert len(coverage['from_ptr_functions_verified']) == 14 +assert len(coverage['generic_operation_wrappers_verified']) == 15 +assert len(coverage['fresh_and_shared_callers_verified']) == 14 +assert all(coverage['from_ptr_negative_controls'].values()) +assert len(operations) == 29 and all(result['passed'] for result in operations) +print('PASS: complete required atomic proof scope and all configured rejection controls.', flush=True) diff --git a/verifast-proofs/core/sync/atomic.rs/checks/decoder/check.py b/verifast-proofs/core/sync/atomic.rs/checks/decoder/check.py new file mode 100644 index 0000000000000..2a6f8f9daac42 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/decoder/check.py @@ -0,0 +1,99 @@ +"""Adversarial MIR decoder tests, NOT Rust proofs or a proof exporter. + +Replay mutated copies of the real pinned exporter output through an isolated +runtime. The actual proof runtime and exporter are never modified. +""" +from pathlib import Path +import os +import subprocess +import sys + +repo = next(p for p in Path(__file__).resolve().parents if (p / 'library/core/src/sync/atomic.rs').is_file()) +base = Path(__file__).resolve().parent +runtime = base / 'replay-runtime' +fixtures = base / 'replay-fixtures' +runtime.mkdir(exist_ok=True) +fixtures.mkdir(exist_ok=True) +if len(sys.argv) != 3: + raise SystemExit('usage: check.py /path/to/runtime/bin /path/to/vf_mir.capnp') +proof_bin = Path(sys.argv[1]).resolve() +for source in proof_bin.iterdir(): + target = runtime / source.name + if source.name != 'vf-rust-mir-exporter' and not target.exists(): + target.symlink_to(source) +exporter = runtime / 'vf-rust-mir-exporter' +exporter.write_text('#!/bin/sh\nset -eu\ncat "$TF_REPLAY_CAPNP"\n') +exporter.chmod(0o755) + +original = (base / 'original-mir.txt').read_text().replace('__ATOMIC_DECODER_FIXTURE__', str(base / 'intrinsic-gate.rs')) +leaf = '( leaf = (data = (h = 0, l = 0), size = 4) )' +branch = 'branch = [\n ' + leaf + ' ]' +assert original.count(branch) == 1 + +def replace_once(old, new): + assert original.count(old) == 1, (old, original.count(old)) + return original.replace(old, new) + +def replace_value_with_param(): + start = original.index('value = (\n ty = (') + begin = original.index('(', start) + depth = 1 + end = begin + 1 + while depth: + depth += (original[end] == '(') - (original[end] == ')') + end += 1 + return original[:start] + 'param = (index = 0, name = "ORD")' + original[end:] + +malformed = 'expected a concrete fieldless AtomicOrdering enum constant' +cases = { + 'valid-relaxed': (original, 'No matching heap chunks:'), + 'valid-release': (replace_once(leaf, leaf.replace('l = 0', 'l = 1')), 'No matching heap chunks:'), + 'valid-seqcst': (replace_once(leaf, leaf.replace('l = 0', 'l = 4')), 'No matching heap chunks:'), + 'other-enum': (replace_once('std::intrinsics::AtomicOrdering', 'unrelated::AtomicOrdering'), malformed), + 'data-type-u16': (replace_once('type = (\n kind = (uInt = (u8 = void)) )', 'type = (kind = (uInt = (u16 = void)))'), malformed), + 'data-type-tuple': (replace_once('type = (\n kind = (uInt = (u8 = void)) )', 'type = (kind = (tuple = [(kind = (uInt = (u8 = void))), (kind = (uInt = (u8 = void)))]))'), malformed), + 'data-type-param': (replace_once('type = (\n kind = (uInt = (u8 = void)) )', 'type = (kind = (param = "T"))'), malformed), + 'integer-instead-of-enum': (replace_once('ty = (\n kind = (\n adt = (\n id = (\n name = \"std::intrinsics::AtomicOrdering\" ),\n kind = (enumKind = void),\n substs = [] ) ) )', 'ty = (kind = (uInt = (u32 = void)))'), malformed), + 'struct-kind': (replace_once('enumKind = void', 'structKind = void'), malformed), + 'union-kind': (replace_once('enumKind = void', 'unionKind = void'), malformed), + 'enum-has-type-args': (replace_once('substs = []', 'substs = [(kind = (type = (kind = (uInt = (u8 = void))))) ]'), malformed), + 'empty-branch': (replace_once(branch, 'branch = []'), malformed), + 'payload-branch': (replace_once(branch, 'branch = [' + leaf + ', ' + leaf + ']'), malformed), + 'bare-leaf': (replace_once(branch, 'leaf = (data = (h = 0, l = 0), size = 4)'), malformed), + 'scalar-width-0': (replace_once(leaf, leaf.replace('size = 4', 'size = 0')), malformed), + 'scalar-width-1': (replace_once(leaf, leaf.replace('size = 4', 'size = 1')), malformed), + 'scalar-width-8': (replace_once(leaf, leaf.replace('size = 4', 'size = 8')), malformed), + 'symbolic-param': (replace_value_with_param(), malformed), + 'late-bound-param': (replace_once('lateBoundGenericParamCount = 0', 'lateBoundGenericParamCount = 1'), 'late-bound generic arguments are not permitted'), + 'invalid-acquire': (replace_once(leaf, leaf.replace('l = 0', 'l = 2')), 'Acquire and AcqRel are not permitted for stores'), + 'invalid-acqrel': (replace_once(leaf, leaf.replace('l = 0', 'l = 3')), 'Acquire and AcqRel are not permitted for stores'), + 'index-5': (replace_once(leaf, leaf.replace('l = 0', 'l = 5')), 'invalid AtomicOrdering variant index'), + 'index-over-u32': (replace_once(leaf, leaf.replace('l = 0', 'l = 4294967296')), 'invalid AtomicOrdering variant index'), + 'index-high-u64': (replace_once(leaf, leaf.replace('h = 0', 'h = 1')), 'invalid AtomicOrdering variant index'), + 'other-function': (replace_once('std::intrinsics::atomic_store', 'unrelated::atomic_store'), 'Unsupported constant value tree'), +} +# The fixture's surrounding pointer type still says u8, so changing only +# the intrinsic type to u16 reaches argument type checking. It is not a proof. +cases['data-type-u16'] = (cases['data-type-u16'][0], 'Type mismatch') +cases['data-type-tuple'] = (cases['data-type-tuple'][0], 'operand must be an integer') +cases['data-type-param'] = (cases['data-type-param'][0], 'No such type parameter') +schema = Path(sys.argv[2]).resolve() +include = Path(os.environ['CAPNP_INC_DIR']) +summary = [] +for name, (fixture, expected) in cases.items(): + text_file = fixtures / f'{name}.txt' + binary_file = fixtures / f'{name}.bin' + log_file = fixtures / f'{name}.log' + text_file.write_text(fixture) + binary = subprocess.run(['capnp', 'encode', '-I' + str(include), str(schema), 'VfMir'], input=fixture.encode(), stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=True).stdout + binary_file.write_bytes(binary) + env = dict(os.environ, TF_REPLAY_CAPNP=str(binary_file)) + result = subprocess.run([str(runtime / 'verifast'), '-rustc_args', '--edition=2024 --crate-type=lib', str(base / 'intrinsic-gate.rs')], cwd=repo, env=env, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, text=True, timeout=30) + log_file.write_text('LOCALPATCH / MUTATED MIR REPLAY TEST ONLY\n' + result.stdout) + ok = result.returncode != 0 and expected in result.stdout + summary.append(f'{name}: {"PASS" if ok else "FAIL"} (exit {result.returncode}); expected {expected}') + if not ok: + print(result.stdout) + raise RuntimeError(name) +(base / 'translator-mutations.log').write_text('LOCALPATCH / MUTATED MIR REPLAY TESTS ONLY\n' + '\n'.join(summary) + '\n') +print('\n'.join(summary)) diff --git a/verifast-proofs/core/sync/atomic.rs/checks/decoder/intrinsic-gate.rs b/verifast-proofs/core/sync/atomic.rs/checks/decoder/intrinsic-gate.rs new file mode 100644 index 0000000000000..7a99be24872f7 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/decoder/intrinsic-gate.rs @@ -0,0 +1,12 @@ +#![feature(core_intrinsics)] + +// Exact current-Rust intrinsic shape used by the atomic_store wrapper. +unsafe fn store_relaxed(dst: *mut u8, val: u8) +//@ req *dst |-> _; +//@ ens *dst |-> val; +//@ on_unwind_ens false; +{ + unsafe { + std::intrinsics::atomic_store::(dst, val) + } +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/decoder/original-mir.txt b/verifast-proofs/core/sync/atomic.rs/checks/decoder/original-mir.txt new file mode 100644 index 0000000000000..f7140c48d9cfb --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/decoder/original-mir.txt @@ -0,0 +1,603 @@ +( adtDefs = (nil = void), + bodies = [ + ( defKind = (fn = void), + defPath = "store_relaxed", + contract = ( + annotations = [ + ( raw = "//@ req *dst |-> _;", + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 5, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 5, + col = (pos = 18) ) ) ), + startLine = 5, + startCol = 1, + endLine = 5, + endCol = 20 ), + ( raw = "//@ ens *dst |-> val;", + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 6, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 6, + col = (pos = 20) ) ) ), + startLine = 6, + startCol = 1, + endLine = 6, + endCol = 22 ), + ( raw = "//@ on_unwind_ens false;", + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 7, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 7, + col = (pos = 23) ) ) ), + startLine = 7, + startCol = 1, + endLine = 7, + endCol = 25 ) ], + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 46) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 8, + col = (pos = 0) ) ) ) ), + inputs = [ + ( kind = ( + rawPtr = ( + ty = ( + kind = (uInt = (u8 = void)) ), + mutability = (mut = void) ) ) ), + ( kind = (uInt = (u8 = void)) ) ], + localDecls = [ + ( mutability = (mut = void), + id = (name = "_0"), + ty = (kind = (tuple = [])), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 46) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 46) ) ) ) ) ), + ( mutability = (not = void), + id = (name = "_1"), + ty = ( + kind = ( + rawPtr = ( + ty = ( + kind = (uInt = (u8 = void)) ), + mutability = (mut = void) ) ) ), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 24) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 27) ) ) ) ) ), + ( mutability = (not = void), + id = (name = "_2"), + ty = ( + kind = (uInt = (u8 = void)) ), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 38) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 41) ) ) ) ) ), + ( mutability = (mut = void), + id = (name = "_3"), + ty = ( + kind = ( + rawPtr = ( + ty = ( + kind = (uInt = (u8 = void)) ), + mutability = (mut = void) ) ) ), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 90) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 93) ) ) ) ) ), + ( mutability = (mut = void), + id = (name = "_4"), + ty = ( + kind = (uInt = (u8 = void)) ), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 95) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 98) ) ) ) ) ) ], + basicBlocks = [ + ( id = (index = 0), + statements = [ + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 90) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 93) ) ) ) ), + kind = ( + storageLive = (name = "_3") ) ), + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 90) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 93) ) ) ) ), + kind = ( + assign = ( + lhsPlace = ( + local = (name = "_3"), + projection = [], + localIsMutable = true, + kind = (other = void) ), + rhsRvalue = ( + use = ( + copy = ( + local = (name = "_1"), + projection = [], + localIsMutable = false, + kind = (other = void) ) ) ) ) ) ), + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 95) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 98) ) ) ) ), + kind = ( + storageLive = (name = "_4") ) ), + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 95) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 98) ) ) ) ), + kind = ( + assign = ( + lhsPlace = ( + local = (name = "_4"), + projection = [], + localIsMutable = true, + kind = (other = void) ), + rhsRvalue = ( + use = ( + copy = ( + local = (name = "_2"), + projection = [], + localIsMutable = false, + kind = (other = void) ) ) ) ) ) ) ], + terminator = ( + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 8) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 99) ) ) ) ), + kind = ( + call = ( + func = ( + constant = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 8) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 89) ) ) ), + const = ( + val = ( + constValue = (zeroSized = void), + ty = ( + kind = ( + fnDef = ( + id = ( + name = "std::intrinsics::atomic_store" ), + substs = [ + ( kind = ( + type = ( + kind = (uInt = (u8 = void)) ) ) ), + ( kind = ( + const = ( + kind = ( + value = ( + ty = ( + kind = ( + adt = ( + id = ( + name = "std::intrinsics::AtomicOrdering" ), + kind = (enumKind = void), + substs = [] ) ) ), + valTree = ( + branch = [ + ( leaf = (data = (h = 0, l = 0), size = 4) ) ] ) ) ) ) ) ) ], + lateBoundGenericParamCount = 0 ) ) ) ) ) ) ), + args = [ + ( move = ( + local = (name = "_3"), + projection = [], + localIsMutable = true, + kind = (other = void) ) ), + ( move = ( + local = (name = "_4"), + projection = [], + localIsMutable = true, + kind = (other = void) ) ) ], + destination = ( + local = (name = "_0"), + projection = [], + localIsMutable = true, + kind = (other = void) ), + callSpan = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 8) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 99) ) ) ), + unwindAction = (unreachable = void), + target = (something = (index = 1)) ) ) ), + isCleanup = false ), + ( id = (index = 1), + statements = [ + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 98) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 99) ) ) ) ), + kind = ( + storageDead = (name = "_4") ) ), + ( sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 98) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 10, + col = (pos = 99) ) ) ) ), + kind = ( + storageDead = (name = "_3") ) ) ], + terminator = ( + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 12, + col = (pos = 1) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 12, + col = (pos = 1) ) ) ) ), + kind = (return = void) ), + isCleanup = false ) ], + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 12, + col = (pos = 1) ) ) ), + impSpan = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 8, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 12, + col = (pos = 1) ) ) ), + varDebugInfo = [ + ( name = (name = "dst"), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 24) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 27) ) ) ) ), + value = ( + place = ( + local = (name = "_1"), + projection = [], + localIsMutable = false, + kind = (other = void) ) ) ), + ( name = (name = "val"), + sourceInfo = ( + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 38) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 41) ) ) ) ), + value = ( + place = ( + local = (name = "_2"), + projection = [], + localIsMutable = false, + kind = (other = void) ) ) ) ], + ghostStmts = [], + unsafety = (unsafe = void), + hirGenerics = ( + params = [], + whereClause = void, + span = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 23) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 23) ) ) ) ), + isTraitFn = false, + isDropFn = false, + ghostDeclBlocks = [], + output = (kind = (tuple = [])), + predicates = [], + generics = [], + fnSigSpan = ( + regular = ( + lo = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 0) ), + hi = ( + file = ( + name = ( + real = ( + localPath = "__ATOMIC_DECODER_FIXTURE__" ) ) ), + line = 4, + col = (pos = 46) ) ) ), + visibility = (restricted = void), + isFromExpansion = false, + loopSpecBlocks = [] ) ], + ghostDeclBatches = [], + traitImpls = [], + directives = [], + traits = (nil = void), + modules = [], + targetTriple = "arm64-apple-macosx", + pointerWidth = 64, + tyAliases = [] ) diff --git a/verifast-proofs/core/sync/atomic.rs/checks/operations/annotate.py b/verifast-proofs/core/sync/atomic.rs/checks/operations/annotate.py new file mode 100644 index 0000000000000..4eccd839937ae --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/operations/annotate.py @@ -0,0 +1,30 @@ +"""Add contracts to the exact generic operation-wrapper signatures.""" +OPS = ['store','load','swap','add','sub','compare_exchange','compare_exchange_weak', + 'and','nand','or','xor','max','min','umax','umin'] +RMW = {'add':'Add','sub':'Sub','and':'And','nand':'Nand','or':'Or','xor':'Xor'} + +def annotate(source): + for op in OPS: + name = 'atomic_' + op + anchor = 'unsafe fn ' + name + '<' + assert source.count(anchor) == 1, name + start = source.index(anchor) + body = source.index('{', start) + q = 'std::intrinsics::' + domain = q + (f'atomic_{"unsigned" if op.startswith("u") else "signed"}_type::()' if op in ['max','min','umax','umin'] else 'atomic_rmw_types::()' if op in RMW else 'atomic_type::()') + inner = '?g' if op == 'load' else '1' + pre = f'{domain} == true &*& [?f]{q}atomic_points_to(dst, {inner}, ?inv_)' + post = f'[f]{q}atomic_points_to(dst, {"g" if op == "load" else "1"}, inv_)' + if op not in ['load', *RMW]: + pre += ' &*& inv_(' + ('new' if op.startswith('compare_exchange') else 'val') + ') == true' + if op in RMW: + pre += f' &*& [_]{q}is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), {q}Rmw{RMW[op]}, inv_, val)' + if op in ['store','load','compare_exchange','compare_exchange_weak']: + pre = 'thread_token(?t) &*& ' + pre + post = 'thread_token(t) &*& ' + post + unwind = post if op in ['store','load','compare_exchange','compare_exchange_weak'] else 'false' + if op != 'store': + post += ' &*& match result { Result::Ok(v) => inv_(v) == true, Result::Err(v) => inv_(v) == true }' if op.startswith('compare_exchange') else ' &*& inv_(result) == true' + contract = f'\n//@ req {pre};\n//@ ens {post};\n//@ on_unwind_ens {unwind};\n' + source = source[:body].rstrip() + contract + source[body:] + return source diff --git a/verifast-proofs/core/sync/atomic.rs/checks/operations/build-controls.py b/verifast-proofs/core/sync/atomic.rs/checks/operations/build-controls.py new file mode 100644 index 0000000000000..34d4c68d42594 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/operations/build-controls.py @@ -0,0 +1,124 @@ +"""Generate concrete, independent callers and deliberately invalid calls.""" +from pathlib import Path +base = Path(__file__).resolve().parent +header = '#![feature(core_intrinsics)]\n#![allow(internal_features)]\n/*@\nfix accepts(value: T) -> bool { true }\nfix bool_byte(value: u8) -> bool { value == 0 || value == 1 }\n@*/\n' +q = 'std::intrinsics::' +orders = ['Relaxed','Release','Acquire','AcqRel','SeqCst'] +rmw = {'xadd':'Add','xsub':'Sub','and':'And','nand':'Nand','or':'Or','xor':'Xor'} + +def witness(ty, op, val='val', second=None): + second = second or ty + return f''' /*@ + produce_lem_ptr_chunk {q}atomic_rmw_preserves<{ty}, {second}>(typeid({ty}), typeid({second}), {q}Rmw{rmw[op]}, accepts, {val})(old) {{ + }}; + @*/ + //@ leak {q}is_atomic_rmw_preserves::<{ty}, {second}>(_, typeid({ty}), typeid({second}), {q}Rmw{rmw[op]}, accepts, {val}); +''' + +matrix = header +names = [] +for op in ['store','load','xchg','cxchg','cxchgweak', *rmw, 'max','min','umax','umin']: + ty = 'i8' if op in ['max','min'] else 'u8' + primary = ['Relaxed','Release','SeqCst'] if op == 'store' else ['Relaxed','Acquire','SeqCst'] if op == 'load' else orders + for order in primary: + for failure in (['Relaxed','Acquire','SeqCst'] if op in ['cxchg','cxchgweak'] else [None]): + name = op + '_' + order.lower() + ('_' + failure.lower() if failure else '') + names.append(name) + ty_args = ty + (', ' + ty if op in rmw else '') + ty_args += ', {' + q + 'AtomicOrdering::' + order + '}' + if failure: + ty_args += ', {' + q + 'AtomicOrdering::' + failure + '}' + call_args = 'dst' if op == 'load' else 'dst, val, val' if failure else 'dst, val' + result = '' if op == 'store' else f' -> ({ty}, bool)' if failure else ' -> ' + ty + ptr = '*const' if op == 'load' else '*mut' + fraction = '?g' if op == 'load' else '1' + matrix += f'''\nunsafe fn {name}(dst: {ptr} {ty}, val: {ty}){result} +//@ req [?f]{q}atomic_points_to(dst, {fraction}, accepts); +//@ ens [f]{q}atomic_points_to(dst, {'g' if op == 'load' else '1'}, accepts); +//@ on_unwind_ens false; +{{ +''' + if op in rmw: + matrix += witness(ty, op) + matrix += f' unsafe {{ {q}atomic_{op}::<{ty_args}>({call_args}) }}\n}}\n' +assert len(names) == 91 +(base / 'ordering-matrix.rs').write_text(matrix) + +types = header +for ty in ['i8','u8','i16','u16','i32','u32','i64','u64','i128','u128','isize','usize']: + types += f'''\nunsafe fn domain_{ty}(dst: *mut {ty}, val: {ty}) -> {ty} +//@ req [?f]{q}atomic_points_to(dst, 1, accepts); +//@ ens [f]{q}atomic_points_to(dst, 1, accepts); +//@ on_unwind_ens false; +{{ +''' + witness(ty,'xadd') + f''' unsafe {{ + {q}atomic_store::<{ty}, {{{q}AtomicOrdering::Relaxed}}>(dst, val); + {q}atomic_xadd::<{ty}, {ty}, {{{q}AtomicOrdering::SeqCst}}>(dst, val) + }} +}} +''' +for size in range(5): + ty = f'*mut [u8; {size}]' + types += f'''\nunsafe fn pointer_size_{size}(dst: *mut {ty}, val: usize, new: {ty}) -> {ty} +//@ req [?f]{q}atomic_points_to(dst, 1, accepts); +//@ ens [f]{q}atomic_points_to(dst, 1, accepts); +//@ on_unwind_ens false; +{{ + //@ {q}atomic_domain_ptr::<[u8; {size}]>(); +''' + witness(ty,'xadd',second='usize') + f''' unsafe {{ + {q}atomic_store::<{ty}, {{{q}AtomicOrdering::Relaxed}}>(dst, new); + {q}atomic_xadd::<{ty}, usize, {{{q}AtomicOrdering::SeqCst}}>(dst, val) + }} +}} +''' +(base / 'type-domains.rs').write_text(types) + +def negative(name, ty='u8', update=None, op='store', order='Relaxed', failure=None, + pre=None, post=None, ghost='', generic=''): + update = update or ty + if pre is None: + pre = f'[?f]{q}atomic_points_to(dst, 1, accepts)' + if post is None: + post = f'[f]{q}atomic_points_to(dst, 1, accepts)' + type_args = ty + (', ' + update if op in rmw else '') + type_args += ', {' + q + 'AtomicOrdering::' + order + '}' + if failure: + type_args += ', {' + q + 'AtomicOrdering::' + failure + '}' + call_args = 'dst' if op == 'load' else 'dst, val, val' if failure else 'dst, val' + code = f'''\nunsafe fn invalid{generic}(dst: *mut {ty}, val: {update}) +//@ req {pre}; +//@ ens {post}; +//@ on_unwind_ens false; +{{ +{ghost} unsafe {{ {q}atomic_{op}::<{type_args}>({call_args}); }} +}} +''' + (base / (name + '.rs')).write_text(header + code) + +for name, ty in [('type-bool','bool'), ('type-float','f32'), ('type-tuple','(u8,u8)'), ('type-fat-pointer','*mut [u8]')]: + negative(name, ty) +negative('missing-domain', 'T', generic='') +negative('missing-resource', pre='true', post='true') +negative('ordinary-resource', pre='*dst |-> ?old', post='*dst |-> _') +negative('fractional-write', pre=f'{q}atomic_points_to(dst, 1/2, accepts)', post=f'{q}atomic_points_to(dst, 1/2, accepts)') +negative('missing-closure', op='xadd') +negative('wrong-closure-op', op='xadd', ghost=witness('u8','xsub')) +negative('wrong-closure-type', op='xadd', ghost=witness('u16','xadd',val='0')) +negative('mismatched-integers', ty='u8', update='u16', op='xadd') +negative('pointer-update-type', ty='*mut u8', update='u8', op='xadd') +negative('signed-max-unsigned', op='max') +negative('unsigned-min-signed', ty='i8', op='umin') +negative('store-acquire', order='Acquire') +negative('store-acqrel', order='AcqRel') +negative('load-release', op='load', order='Release') +negative('load-acqrel', op='load', order='AcqRel') +negative('cxchg-failure-release', op='cxchg', failure='Release') +negative('cxchgweak-failure-acqrel', op='cxchgweak', failure='AcqRel') +negative('invalid-bool-store', pre=f'[?f]{q}atomic_points_to(dst, 1, bool_byte) &*& val == 2', post=f'[f]{q}atomic_points_to(dst, 1, bool_byte)') +negative('invalid-bool-cxchg', op='cxchg', failure='Relaxed', pre=f'[?f]{q}atomic_points_to(dst, 1, bool_byte) &*& val == 2', post=f'[f]{q}atomic_points_to(dst, 1, bool_byte)') + +positive = (base / 'positive.rs').read_text() +boolean = positive[positive.index('unsafe fn bool_and'):positive.index('unsafe fn bool_or')] +(base / 'bool-nand-rejected.rs').write_text(header + boolean.replace('bool_and','bool_nand').replace('RmwAnd','RmwNand').replace('bytes_and','bytes_nand').replace('atomic_and','atomic_nand')) +(base / 'bool-add-rejected.rs').write_text(header + boolean.replace('bool_and','bool_add').replace('RmwAnd','RmwAdd').replace('atomic_rmw_bool_bytes_and','atomic_rmw_u8_add').replace('atomic_and','atomic_xadd')) +print('Generated 91 ordering callers, 12 integer/5 pointer domain callers, and 25 rejection cases.') diff --git a/verifast-proofs/core/sync/atomic.rs/checks/operations/positive.rs b/verifast-proofs/core/sync/atomic.rs/checks/operations/positive.rs new file mode 100644 index 0000000000000..493372e2b5096 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/operations/positive.rs @@ -0,0 +1,79 @@ +#![feature(core_intrinsics)] + +/*@ +fix accepts(value: T) -> bool { true } +fix bool_byte(value: u8) -> bool { value == 0 || value == 1 } +@*/ + +// A generic caller can construct an actual invariant-closure witness. The +// operand domain remains a requirement, since Copy is insufficient by itself. +unsafe fn generic_add(dst: *mut T, val: U) -> T +//@ req std::intrinsics::atomic_rmw_types::() == true &*& [?f]std::intrinsics::atomic_points_to(dst, 1, accepts); +//@ ens [f]std::intrinsics::atomic_points_to(dst, 1, accepts); +//@ on_unwind_ens false; +{ + /*@ + produce_lem_ptr_chunk std::intrinsics::atomic_rmw_preserves(typeid(T), typeid(U), std::intrinsics::RmwAdd, accepts, val)(old) { + }; + @*/ + //@ leak std::intrinsics::is_atomic_rmw_preserves::(_, typeid(T), typeid(U), std::intrinsics::RmwAdd, accepts, val); + let result = unsafe { std::intrinsics::atomic_xadd::(dst, val) }; + result +} + +unsafe fn bool_and(dst: *mut u8, val: u8) -> u8 +//@ req [?f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(val) == true; +//@ ens [f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(result) == true; +//@ on_unwind_ens false; +{ + /*@ + produce_lem_ptr_chunk std::intrinsics::atomic_rmw_preserves(typeid(u8), typeid(u8), std::intrinsics::RmwAnd, bool_byte, val)(old) { + assert bool_byte(old) == true; + assert bool_byte(val) == true; + std::intrinsics::atomic_rmw_bool_bytes_and(old, val); + if old == 0 {} else {} + if val == 0 {} else {} + }; + @*/ + //@ leak std::intrinsics::is_atomic_rmw_preserves::(_, typeid(u8), typeid(u8), std::intrinsics::RmwAnd, bool_byte, val); + let result = unsafe { std::intrinsics::atomic_and::(dst, val) }; + result +} + +unsafe fn bool_or(dst: *mut u8, val: u8) -> u8 +//@ req [?f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(val) == true; +//@ ens [f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(result) == true; +//@ on_unwind_ens false; +{ + /*@ + produce_lem_ptr_chunk std::intrinsics::atomic_rmw_preserves(typeid(u8), typeid(u8), std::intrinsics::RmwOr, bool_byte, val)(old) { + assert bool_byte(old) == true; + assert bool_byte(val) == true; + std::intrinsics::atomic_rmw_bool_bytes_or(old, val); + if old == 0 {} else {} + if val == 0 {} else {} + }; + @*/ + //@ leak std::intrinsics::is_atomic_rmw_preserves::(_, typeid(u8), typeid(u8), std::intrinsics::RmwOr, bool_byte, val); + let result = unsafe { std::intrinsics::atomic_or::(dst, val) }; + result +} + +unsafe fn bool_xor(dst: *mut u8, val: u8) -> u8 +//@ req [?f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(val) == true; +//@ ens [f]std::intrinsics::atomic_points_to(dst, 1, bool_byte) &*& bool_byte(result) == true; +//@ on_unwind_ens false; +{ + /*@ + produce_lem_ptr_chunk std::intrinsics::atomic_rmw_preserves(typeid(u8), typeid(u8), std::intrinsics::RmwXor, bool_byte, val)(old) { + assert bool_byte(old) == true; + assert bool_byte(val) == true; + std::intrinsics::atomic_rmw_bool_bytes_xor(old, val); + if old == 0 {} else {} + if val == 0 {} else {} + }; + @*/ + //@ leak std::intrinsics::is_atomic_rmw_preserves::(_, typeid(u8), typeid(u8), std::intrinsics::RmwXor, bool_byte, val); + let result = unsafe { std::intrinsics::atomic_xor::(dst, val) }; + result +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/operations/run.py b/verifast-proofs/core/sync/atomic.rs/checks/operations/run.py new file mode 100644 index 0000000000000..b1875452f9c07 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/operations/run.py @@ -0,0 +1,73 @@ +"""Require positive proof coverage and specific diagnostics for unsafe controls.""" +from pathlib import Path +import json +import re +import subprocess +import sys + +base = Path(__file__).resolve().parent +if len(sys.argv) != 2: + raise SystemExit('usage: run.py /absolute/path/to/experimental/verifast') +verifier = Path(sys.argv[1]).resolve() +subprocess.run([sys.executable, str(base / 'build-controls.py')], check=True) +cases = { + 'positive': (True, '0 errors found', 4), + 'ordering-matrix': (True, '0 errors found', 91), + 'type-domains': (True, '0 errors found', 17), + 'type-bool': (False, 'operand must be an integer', None), + 'type-float': (False, 'Floating point types are not yet supported', None), + 'type-tuple': (False, 'operand must be an integer', None), + 'type-fat-pointer': (False, 'operand must be an integer', None), + 'unsized-domain-rejected': (False, 'must implement trait Sized', None), + 'missing-domain': (False, 'Cannot prove std::intrinsics::atomic_type', None), + 'missing-resource': (False, 'No matching heap chunks: [_]std::intrinsics::atomic_points_to', None), + 'ordinary-resource': (False, 'No matching heap chunks: [_]std::intrinsics::atomic_points_to', None), + 'fractional-write': (False, 'No matching heap chunks: [_]std::intrinsics::atomic_points_to', None), + 'missing-closure': (False, 'No matching heap chunks: [_]std::intrinsics::is_atomic_rmw_preserves', None), + 'wrong-closure-op': (False, 'No matching heap chunks: [_]std::intrinsics::is_atomic_rmw_preserves', None), + 'wrong-closure-type': (False, 'No matching heap chunks: [_]std::intrinsics::is_atomic_rmw_preserves', None), + 'mismatched-integers': (False, 'RMW operands must be the same integer type', None), + 'pointer-update-type': (False, 'RMW operands must be the same integer type', None), + 'signed-max-unsigned': (False, 'signed min/max require a signed integer', None), + 'unsigned-min-signed': (False, 'unsigned min/max require an unsigned integer', None), + 'store-acquire': (False, 'Acquire and AcqRel are not permitted for stores', None), + 'store-acqrel': (False, 'Acquire and AcqRel are not permitted for stores', None), + 'load-release': (False, 'Release and AcqRel are not permitted for loads', None), + 'load-acqrel': (False, 'Release and AcqRel are not permitted for loads', None), + 'cxchg-failure-release': (False, 'Release and AcqRel are not permitted for compare-exchange failure', None), + 'cxchgweak-failure-acqrel': (False, 'Release and AcqRel are not permitted for compare-exchange failure', None), + 'invalid-bool-store': (False, 'Cannot prove', None), + 'invalid-bool-cxchg': (False, 'Cannot prove', None), + 'bool-nand-rejected': (False, 'Consuming function type postcondition', None), + 'bool-add-rejected': (False, 'Consuming function type postcondition', None), +} +results = [] +for name, (success, diagnostic, expected_count) in cases.items(): + result = subprocess.run([str(verifier), '-verbose', '1', '-rustc_args', + '--edition=2024 --crate-type=lib', str(base / (name + '.rs'))], + capture_output=True, text=True) + output = result.stdout + result.stderr + functions = re.findall(r"Verifying function '([^']+)'", output) + functions = [fn for fn in functions if not fn.startswith('std::') and fn != 'open_full_borrow_'] + # Ignore included standard ghost lemmas; require each real Rust function + # declared in the concrete source to appear in the verification output. + expected = set(re.findall(r'unsafe fn (\w+)', (base / (name + '.rs')).read_text())) + coverage = expected <= set(functions) + ok = (result.returncode == 0) == success and diagnostic in output + if success: + ok = ok and coverage and len(expected) == expected_count and 'arm64-apple-macosx (LP64)' in output + lines = output.splitlines() + saved = '\n'.join(line for line in lines if 'Verifying function ' in line or 'errors found' in line) + if not success or not ok: + saved = output + (base / (name + '.log')).write_text(saved + '\n') + results.append({'name': name, 'passed': ok, 'expected_success': success, + 'exit': result.returncode, 'expected_diagnostic': diagnostic, + 'rust_functions_covered': sorted(expected & set(functions))}) + print(f'{name}: {"PASS" if ok else "FAIL"} (exit {result.returncode})') + if not ok: + print('\n'.join(line for line in lines if 'error:' in line)[:2000]) +(base / 'results.json').write_text(json.dumps(results, indent=2) + '\n') +if not all(r['passed'] for r in results): + raise SystemExit('Some controls did not produce the expected result.') +print(f'PASS: {len(results)} operation controls; 91 concrete orderings and all 17 operand-type witnesses covered.') diff --git a/verifast-proofs/core/sync/atomic.rs/checks/operations/unsized-domain-rejected.rs b/verifast-proofs/core/sync/atomic.rs/checks/operations/unsized-domain-rejected.rs new file mode 100644 index 0000000000000..418c49bf924ec --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/operations/unsized-domain-rejected.rs @@ -0,0 +1,8 @@ +/*@ +lem unsized_pointer_domain() + req true; + ens std::intrinsics::atomic_type::<*[u8]>() == true; +{ + std::intrinsics::atomic_domain_ptr::<[u8]>(); +} +@*/ diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/check.py b/verifast-proofs/core/sync/atomic.rs/checks/refinement/check.py new file mode 100644 index 0000000000000..f36527cfadbcc --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/check.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 +"""Run the isolated AtomicOrdering refinement checks against a supplied checker.""" +from pathlib import Path +import subprocess +import sys + +if len(sys.argv) != 2: + raise SystemExit("usage: python3 rc-run.py /absolute/path/to/refinement-checker") + +base = Path(__file__).resolve().parent +checker = Path(sys.argv[1]).resolve() +cases = [ + ("rc-positive", "rc-original", "rc-positive", True, + ["No refinement errors found", "checking refinement"]), + ("rc-wrong-order", "rc-original", "rc-wrong-order", False, + ["The constants", "are not equal", "AtomicOrdering::Relaxed", "AtomicOrdering::SeqCst"]), + ("rc-other-enum", "rc-other-original", "rc-other-verified", False, + ["Branch not supported (expected a fieldless AtomicOrdering constant)"]), + ("rc-integer", "rc-integer-original", "rc-integer-verified", True, + ["No refinement errors found", "checking refinement"]), +] +failures = [] +for label, original, verified, should_pass, evidence in cases: + command = [str(checker), "--verbose", "0", str(base / original / "lib.rs"), + str(base / verified / "lib.rs")] + result = subprocess.run(command, capture_output=True, text=True) + output = result.stdout + result.stderr + (base / (label + "-local-patched26.01-checker.log")).write_text( + f"Tool: {checker}\nProvenance: local modified VeriFast 26.01, not the approved release binary\n\n" + output) + accepted = (result.returncode == 0) == should_pass and all(s in output for s in evidence) + print(f"{label}: {'PASS' if accepted else 'FAIL'} (checker exit {result.returncode})") + if not accepted: + failures.append(label) + print(output) +if failures: + raise SystemExit("Unexpected result: " + ", ".join(failures)) diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-original/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-original/lib.rs new file mode 100644 index 0000000000000..b54273c652f77 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-original/lib.rs @@ -0,0 +1,10 @@ +#![allow(non_snake_case)] + +fn identity(value: [u8; N]) -> [u8; N] { value } + +mod bridge { +} + +pub fn array_identity(value: [u8; 3]) -> [u8; 3] { + identity::<3>(value) +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-verified/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-verified/lib.rs new file mode 100644 index 0000000000000..c55737276da3d --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-integer-verified/lib.rs @@ -0,0 +1,13 @@ +#![allow(non_snake_case)] + +fn identity(value: [u8; N]) -> [u8; N] { value } + +mod bridge { + pub fn array_identity__VeriFast_wrapper(value: [u8; 3]) -> [u8; 3] { + super::identity::<3>(value) + } +} + +pub fn array_identity(value: [u8; 3]) -> [u8; 3] { + bridge::array_identity__VeriFast_wrapper(value) +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-original/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-original/lib.rs new file mode 100644 index 0000000000000..29897a7c4e98a --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-original/lib.rs @@ -0,0 +1,25 @@ +#![feature(core_intrinsics)] +#![allow(non_snake_case, internal_features)] + +mod bridge { +} + +pub unsafe fn exchange_relaxed(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } +} + +pub unsafe fn exchange_release(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } +} + +pub unsafe fn exchange_acquire(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } +} + +pub unsafe fn exchange_acqrel(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } +} + +pub unsafe fn exchange_seqcst(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-original/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-original/lib.rs new file mode 100644 index 0000000000000..2ca831a6c5207 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-original/lib.rs @@ -0,0 +1,15 @@ +#![feature(adt_const_params)] +#![allow(incomplete_features, non_snake_case)] +use std::marker::ConstParamTy; + +#[derive(ConstParamTy, PartialEq, Eq)] +enum AtomicOrdering { Relaxed, Release, Acquire, AcqRel, SeqCst } + +fn marker() {} + +mod bridge { +} + +pub fn call_marker() { + marker::<{ AtomicOrdering::Relaxed }>(); +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-verified/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-verified/lib.rs new file mode 100644 index 0000000000000..3b69b516008d9 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-other-verified/lib.rs @@ -0,0 +1,18 @@ +#![feature(adt_const_params)] +#![allow(incomplete_features, non_snake_case)] +use std::marker::ConstParamTy; + +#[derive(ConstParamTy, PartialEq, Eq)] +enum AtomicOrdering { Relaxed, Release, Acquire, AcqRel, SeqCst } + +fn marker() {} + +mod bridge { + pub fn call_marker__VeriFast_wrapper() { + super::marker::<{ super::AtomicOrdering::Relaxed }>(); + } +} + +pub fn call_marker() { + bridge::call_marker__VeriFast_wrapper(); +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-positive/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-positive/lib.rs new file mode 100644 index 0000000000000..f5cb397fd0a8b --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-positive/lib.rs @@ -0,0 +1,40 @@ +#![feature(core_intrinsics)] +#![allow(non_snake_case, internal_features)] + +mod bridge { + pub unsafe fn exchange_relaxed__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_release__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_acquire__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_acqrel__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_seqcst__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } +} + +pub unsafe fn exchange_relaxed(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_relaxed__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_release(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_release__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_acquire(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_acquire__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_acqrel(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_acqrel__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_seqcst(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_seqcst__VeriFast_wrapper(dst, val) } +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-wrong-order/lib.rs b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-wrong-order/lib.rs new file mode 100644 index 0000000000000..930a1afb5a357 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/refinement/rc-wrong-order/lib.rs @@ -0,0 +1,40 @@ +#![feature(core_intrinsics)] +#![allow(non_snake_case, internal_features)] + +mod bridge { + pub unsafe fn exchange_relaxed__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_release__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_acquire__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_acqrel__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } + pub unsafe fn exchange_seqcst__VeriFast_wrapper(dst: *mut u8, val: u8) -> u8 { + unsafe { std::intrinsics::atomic_xchg::(dst, val) } + } +} + +pub unsafe fn exchange_relaxed(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_relaxed__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_release(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_release__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_acquire(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_acquire__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_acqrel(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_acqrel__VeriFast_wrapper(dst, val) } +} + +pub unsafe fn exchange_seqcst(dst: *mut u8, val: u8) -> u8 { + unsafe { bridge::exchange_seqcst__VeriFast_wrapper(dst, val) } +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic-negative.rs new file mode 100644 index 0000000000000..7862475b46f77 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic-negative.rs @@ -0,0 +1,7 @@ +#[repr(C, align(8))] +struct Generic { value: T } +unsafe fn no_single_alignment_for_every_instantiation() +//@ req true; +//@ ens std::mem::align_of::>() == 8; +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic64-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic64-negative.rs new file mode 100644 index 0000000000000..b78f48edb3eed --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-generic64-negative.rs @@ -0,0 +1,9 @@ +#[repr(C, align(64))] +struct WideAlignment { value: u8 } +#[repr(C, align(8))] +struct Generic { value: T } +unsafe fn minimum_alignment_is_not_exact_alignment() +//@ req true; +//@ ens std::mem::align_of::>() == 8; +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-minimum-positive.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-minimum-positive.rs new file mode 100644 index 0000000000000..c44b0bbdded41 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-minimum-positive.rs @@ -0,0 +1,7 @@ +#[repr(C, align(8))] +struct Generic { value: T } +unsafe fn minimum_alignment_for_every_instantiation() +//@ req true; +//@ ens std::mem::align_of::>() >= 8 &*& std::mem::align_of::>() % 8 == 0; +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-positive.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-positive.rs new file mode 100644 index 0000000000000..726a7fca92f68 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-positive.rs @@ -0,0 +1,9 @@ +#[repr(C, align(32))] +struct AlignedByte { value: u8 } +#[repr(C, align(1))] +struct AlignedWide { value: u64 } +unsafe fn check_layouts() +//@ req true; +//@ ens std::mem::align_of::() == 32 &*& std::mem::align_of::() == 8; +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-wrong-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-wrong-negative.rs new file mode 100644 index 0000000000000..aa77511d89ef4 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/alignment-wrong-negative.rs @@ -0,0 +1,7 @@ +#[repr(C, align(1))] +struct AlignedWide { value: u64 } +unsafe fn alignment_attribute_is_not_exact_alignment() +//@ req true; +//@ ens std::mem::align_of::() == 1; +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/check.py b/verifast-proofs/core/sync/atomic.rs/checks/source/check.py new file mode 100644 index 0000000000000..ba504ce27bec8 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/check.py @@ -0,0 +1,37 @@ +#!/usr/bin/env python3 +"""Require specific positive and negative results from the experimental tool.""" +from pathlib import Path +import subprocess +import sys + +if len(sys.argv) != 2: + raise SystemExit('usage: run.py /absolute/path/to/verifast') +base = Path(__file__).resolve().parent +verifier = Path(sys.argv[1]).resolve() +cases = [ + ('self-positive', True, '0 errors found'), + ('self-free-negative', False, 'No such type parameter, inductive datatype, class, interface, or function type: Self'), + ('alignment-positive', True, '0 errors found'), + ('alignment-minimum-positive', True, '0 errors found'), + ('alignment-wrong-negative', False, 'Cannot prove alignof(AlignedWide_type_info) = 1'), + ('alignment-generic-negative', False, 'Cannot prove alignof(Generic_type_info(T_typeid)) = 8'), + ('alignment-generic64-negative', False, 'Cannot prove alignof(Generic_type_info(WideAlignment_type_info)) = 8'), + ('macro-second-negative', False, "Verifying function 'second_must_fail'"), + ('own-sharing-usize', True, '0 errors found'), + ('double-convert-negative', False, 'No matching heap chunks: points_to'), + ('double-recover-negative', False, 'No matching heap chunks: borrow_end_token'), +] +failed = [] +for name, success, diagnostic in cases: + result = subprocess.run([str(verifier), '-skip_specless_fns', '-rustc_args', + '--edition=2024 --crate-type=lib', str(base / (name + '.rs'))], + capture_output=True, text=True) + output = result.stdout + result.stderr + (base / (name + '.log')).write_text(output) + matches = (result.returncode == 0) == success and diagnostic in output + print(f'{name}: {"PASS" if matches else "FAIL"} (exit {result.returncode})') + if not matches: + failed.append(name) + print(output) +if failed: + raise SystemExit('Unexpected result: ' + ', '.join(failed)) diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/double-convert-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/double-convert-negative.rs new file mode 100644 index 0000000000000..ad642efc21596 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/double-convert-negative.rs @@ -0,0 +1,141 @@ +#![feature(core_intrinsics)] +#![allow(internal_features)] +use std::cell::UnsafeCell; + +#[repr(C, align(1))] +pub struct AtomicU8 { + v: UnsafeCell, +} + +unsafe impl Sync for AtomicU8 {} + +/*@ +fix accepts_u8(value: u8) -> bool { true } +pred_ctor own_atomic_contents(p: *u8)(;) = std::intrinsics::atomic_points_to(p, 1, accepts_u8); +pred .own(t, value) = true; +pred .share(k, t, l) = [_]frac_borrow(k, own_atomic_contents(ref_origin(l) as *u8)); + +lem AtomicU8_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *AtomicU8) + req lifetime_inclusion(k1, k) == true &*& [_]AtomicU8_share(k, t, l); + ens [_]AtomicU8_share(k1, t, l); +{ + open AtomicU8_share(k, t, l); + frac_borrow_mono(k, k1, own_atomic_contents(ref_origin(l) as *u8)); + close AtomicU8_share(k1, t, l); + leak AtomicU8_share(k1, t, l); +} + +lem AtomicU8_sync(t1: thread_id_t) + req is_Sync(typeid(AtomicU8)) == true &*& [_]AtomicU8_share(?k, ?t0, ?l); + ens [_]AtomicU8_share(k, t1, l); +{ + open AtomicU8_share(k, t0, l); + close AtomicU8_share(k, t1, l); + leak AtomicU8_share(k, t1, l); +} + +lem AtomicU8_share_full(k: lifetime_t, t: thread_id_t, l: *AtomicU8) + req atomic_mask(MaskTop) &*& full_borrow(k, AtomicU8_full_borrow_content(t, l)) &*& [?q]lifetime_token(k) &*& ref_origin(l) == l; + ens atomic_mask(MaskTop) &*& [_]AtomicU8_share(k, t, l) &*& [q]lifetime_token(k); +{ + open_full_borrow_strong_m_(k, AtomicU8_full_borrow_content(t, l)); + open AtomicU8_full_borrow_content(t, l)(); + open AtomicU8_own(t, _); + div_rem(l as usize, 1); + std::intrinsics::atomic_align_of_u8(); + std::intrinsics::close_atomic_points_to_m(l as *u8, accepts_u8); + close own_atomic_contents(l as *u8)(); + close True(); + produce_lem_ptr_chunk restore_full_borrow_(True, own_atomic_contents(l as *u8), AtomicU8_full_borrow_content(t, l))() { + open True(); + open own_atomic_contents(l as *u8)(); + std::intrinsics::open_atomic_points_to(l as *u8); + close_points_to(l); + assert *l |-> ?value; + close AtomicU8_own(t, value); + open_points_to(l); + close AtomicU8_full_borrow_content(t, l)(); + } { + close_full_borrow_strong_m_(); + } + full_borrow_into_frac_m(k, own_atomic_contents(l as *u8)); + close AtomicU8_share(k, t, l); + leak AtomicU8_share(k, t, l); +} + +lem init_ref_AtomicU8(p: *AtomicU8) + req atomic_mask(Nlft) &*& ref_init_perm(p, ?x) &*& [_]AtomicU8_share(?k, ?t, x) &*& [?q]lifetime_token(k); + ens atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]AtomicU8_share(k, t, p) &*& [_]frac_borrow(k, ref_initialized_(p)); +{ + open AtomicU8_share(k, t, x); + open_ref_init_perm_AtomicU8(p); + close_ref_initialized_AtomicU8(p, 1); + close ref_initialized_::(p)(); + borrow_m(k, ref_initialized_(p)); + leak borrow_end_token(k, ref_initialized_(p)); + full_borrow_into_frac_m(k, ref_initialized_(p)); + close AtomicU8_share(k, t, p); + leak AtomicU8_share(k, t, p); +} +@*/ + +impl AtomicU8 { + pub const unsafe fn from_ptr<'a>(ptr: *mut u8) -> &'a AtomicU8 + //@ req type_interp::() &*& atomic_mask(MaskTop) &*& [?q]lifetime_token('a) &*& *ptr |-> ?value; + //@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [q]lifetime_token('a) &*& [_]AtomicU8_share('a, currentThread, result) &*& [_]ref_initialized(result) &*& [_]frac_borrow('a, ref_initialized_(result)) &*& ref_origin(result) == ref_origin(ptr as *AtomicU8) &*& borrow_end_token('a, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ on_unwind_ens false; + { + //@ close_points_to(ptr as *AtomicU8); + //@ assert *(ptr as *AtomicU8) |-> ?atomic; + //@ close AtomicU8_own(currentThread, atomic); + //@ open_points_to(ptr as *AtomicU8); + //@ close AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)(); + //@ borrow('a, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ share_full_borrow::('a, currentThread, ptr as *AtomicU8); + //@ let p = precreate_ref(ptr as *AtomicU8); + //@ init_ref_share::('a, currentThread, p); + //@ open_frac_borrow('a, ref_initialized_(p), q); + //@ open [?f]ref_initialized_::(p)(); + let result = unsafe { &*ptr.cast() }; + //@ close [f]ref_initialized_::(p)(); + //@ close_frac_borrow(f, ref_initialized_(p)); + //@ close_ref_initialized_AtomicU8(p, 1); + //@ leak ref_initialized(p); + result + } + + pub fn store_relaxed<'a>(&'a self, value: u8) + //@ req [_]AtomicU8_share('a, currentThread, self) &*& [?q]lifetime_token('a); + //@ ens [q]lifetime_token('a); + //@ on_unwind_ens false; + { + //@ open AtomicU8_share('a, currentThread, self); + //@ let f = open_frac_borrow('a, own_atomic_contents(ref_origin(self) as *u8), q); + //@ open [f]own_atomic_contents(ref_origin(self) as *u8)(); + unsafe { std::intrinsics::atomic_store::(self.v.get(), value) } + //@ close [f]own_atomic_contents(ref_origin(self) as *u8)(); + //@ close_frac_borrow(f, own_atomic_contents(ref_origin(self) as *u8)); + } +} + +unsafe fn recover_plain_storage(ptr: *mut u8) +//@ req [_]lifetime_dead_token(?k) &*& borrow_end_token(k, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); +//@ ens *ptr |-> ?stored_value; +//@ on_unwind_ens false; +{ + //@ borrow_end(k, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ open AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)(); + //@ open AtomicU8_own(currentThread, _); +} + +unsafe fn creation_store_recovery<'a>(ptr: *mut u8, value: u8) +//@ req type_interp::() &*& atomic_mask(MaskTop) &*& lifetime_token('a) &*& *ptr |-> ?initial_value; +//@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [_]lifetime_dead_token('a) &*& *ptr |-> ?stored_value; +//@ on_unwind_ens false; +{ + let atomic: &'a AtomicU8 = unsafe { AtomicU8::from_ptr/*@::<'a>@*/(ptr) }; + let second: &'a AtomicU8 = unsafe { AtomicU8::from_ptr/*@::<'a>@*/(ptr) }; + atomic.store_relaxed/*@::<'a>@*/(value); + //@ end_lifetime('a); + unsafe { recover_plain_storage(ptr) }; +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/double-recover-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/double-recover-negative.rs new file mode 100644 index 0000000000000..87ea4eea8ed1e --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/double-recover-negative.rs @@ -0,0 +1,141 @@ +#![feature(core_intrinsics)] +#![allow(internal_features)] +use std::cell::UnsafeCell; + +#[repr(C, align(1))] +pub struct AtomicU8 { + v: UnsafeCell, +} + +unsafe impl Sync for AtomicU8 {} + +/*@ +fix accepts_u8(value: u8) -> bool { true } +pred_ctor own_atomic_contents(p: *u8)(;) = std::intrinsics::atomic_points_to(p, 1, accepts_u8); +pred .own(t, value) = true; +pred .share(k, t, l) = [_]frac_borrow(k, own_atomic_contents(ref_origin(l) as *u8)); + +lem AtomicU8_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *AtomicU8) + req lifetime_inclusion(k1, k) == true &*& [_]AtomicU8_share(k, t, l); + ens [_]AtomicU8_share(k1, t, l); +{ + open AtomicU8_share(k, t, l); + frac_borrow_mono(k, k1, own_atomic_contents(ref_origin(l) as *u8)); + close AtomicU8_share(k1, t, l); + leak AtomicU8_share(k1, t, l); +} + +lem AtomicU8_sync(t1: thread_id_t) + req is_Sync(typeid(AtomicU8)) == true &*& [_]AtomicU8_share(?k, ?t0, ?l); + ens [_]AtomicU8_share(k, t1, l); +{ + open AtomicU8_share(k, t0, l); + close AtomicU8_share(k, t1, l); + leak AtomicU8_share(k, t1, l); +} + +lem AtomicU8_share_full(k: lifetime_t, t: thread_id_t, l: *AtomicU8) + req atomic_mask(MaskTop) &*& full_borrow(k, AtomicU8_full_borrow_content(t, l)) &*& [?q]lifetime_token(k) &*& ref_origin(l) == l; + ens atomic_mask(MaskTop) &*& [_]AtomicU8_share(k, t, l) &*& [q]lifetime_token(k); +{ + open_full_borrow_strong_m_(k, AtomicU8_full_borrow_content(t, l)); + open AtomicU8_full_borrow_content(t, l)(); + open AtomicU8_own(t, _); + div_rem(l as usize, 1); + std::intrinsics::atomic_align_of_u8(); + std::intrinsics::close_atomic_points_to_m(l as *u8, accepts_u8); + close own_atomic_contents(l as *u8)(); + close True(); + produce_lem_ptr_chunk restore_full_borrow_(True, own_atomic_contents(l as *u8), AtomicU8_full_borrow_content(t, l))() { + open True(); + open own_atomic_contents(l as *u8)(); + std::intrinsics::open_atomic_points_to(l as *u8); + close_points_to(l); + assert *l |-> ?value; + close AtomicU8_own(t, value); + open_points_to(l); + close AtomicU8_full_borrow_content(t, l)(); + } { + close_full_borrow_strong_m_(); + } + full_borrow_into_frac_m(k, own_atomic_contents(l as *u8)); + close AtomicU8_share(k, t, l); + leak AtomicU8_share(k, t, l); +} + +lem init_ref_AtomicU8(p: *AtomicU8) + req atomic_mask(Nlft) &*& ref_init_perm(p, ?x) &*& [_]AtomicU8_share(?k, ?t, x) &*& [?q]lifetime_token(k); + ens atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]AtomicU8_share(k, t, p) &*& [_]frac_borrow(k, ref_initialized_(p)); +{ + open AtomicU8_share(k, t, x); + open_ref_init_perm_AtomicU8(p); + close_ref_initialized_AtomicU8(p, 1); + close ref_initialized_::(p)(); + borrow_m(k, ref_initialized_(p)); + leak borrow_end_token(k, ref_initialized_(p)); + full_borrow_into_frac_m(k, ref_initialized_(p)); + close AtomicU8_share(k, t, p); + leak AtomicU8_share(k, t, p); +} +@*/ + +impl AtomicU8 { + pub const unsafe fn from_ptr<'a>(ptr: *mut u8) -> &'a AtomicU8 + //@ req type_interp::() &*& atomic_mask(MaskTop) &*& [?q]lifetime_token('a) &*& *ptr |-> ?value; + //@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [q]lifetime_token('a) &*& [_]AtomicU8_share('a, currentThread, result) &*& [_]ref_initialized(result) &*& [_]frac_borrow('a, ref_initialized_(result)) &*& ref_origin(result) == ref_origin(ptr as *AtomicU8) &*& borrow_end_token('a, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ on_unwind_ens false; + { + //@ close_points_to(ptr as *AtomicU8); + //@ assert *(ptr as *AtomicU8) |-> ?atomic; + //@ close AtomicU8_own(currentThread, atomic); + //@ open_points_to(ptr as *AtomicU8); + //@ close AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)(); + //@ borrow('a, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ share_full_borrow::('a, currentThread, ptr as *AtomicU8); + //@ let p = precreate_ref(ptr as *AtomicU8); + //@ init_ref_share::('a, currentThread, p); + //@ open_frac_borrow('a, ref_initialized_(p), q); + //@ open [?f]ref_initialized_::(p)(); + let result = unsafe { &*ptr.cast() }; + //@ close [f]ref_initialized_::(p)(); + //@ close_frac_borrow(f, ref_initialized_(p)); + //@ close_ref_initialized_AtomicU8(p, 1); + //@ leak ref_initialized(p); + result + } + + pub fn store_relaxed<'a>(&'a self, value: u8) + //@ req [_]AtomicU8_share('a, currentThread, self) &*& [?q]lifetime_token('a); + //@ ens [q]lifetime_token('a); + //@ on_unwind_ens false; + { + //@ open AtomicU8_share('a, currentThread, self); + //@ let f = open_frac_borrow('a, own_atomic_contents(ref_origin(self) as *u8), q); + //@ open [f]own_atomic_contents(ref_origin(self) as *u8)(); + unsafe { std::intrinsics::atomic_store::(self.v.get(), value) } + //@ close [f]own_atomic_contents(ref_origin(self) as *u8)(); + //@ close_frac_borrow(f, own_atomic_contents(ref_origin(self) as *u8)); + } +} + +unsafe fn recover_plain_storage(ptr: *mut u8) +//@ req [_]lifetime_dead_token(?k) &*& borrow_end_token(k, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); +//@ ens *ptr |-> ?stored_value; +//@ on_unwind_ens false; +{ + //@ borrow_end(k, AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)); + //@ open AtomicU8_full_borrow_content(currentThread, ptr as *AtomicU8)(); + //@ open AtomicU8_own(currentThread, _); +} + +unsafe fn creation_store_recovery<'a>(ptr: *mut u8, value: u8) +//@ req type_interp::() &*& atomic_mask(MaskTop) &*& lifetime_token('a) &*& *ptr |-> ?initial_value; +//@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [_]lifetime_dead_token('a) &*& *ptr |-> ?stored_value; +//@ on_unwind_ens false; +{ + let atomic: &'a AtomicU8 = unsafe { AtomicU8::from_ptr/*@::<'a>@*/(ptr) }; + atomic.store_relaxed/*@::<'a>@*/(value); + //@ end_lifetime('a); + unsafe { recover_plain_storage(ptr) }; + unsafe { recover_plain_storage(ptr) }; +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/macro-second-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/macro-second-negative.rs new file mode 100644 index 0000000000000..e6d9ecfe35b18 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/macro-second-negative.rs @@ -0,0 +1,11 @@ +macro_rules! must_return_one { + ($name:ident, $value:expr) => { + unsafe fn $name() -> u8 + //@ req true; + //@ ens result == 1; + //@ on_unwind_ens false; + { $value } + } +} +must_return_one!(first_passes, 1); +must_return_one!(second_must_fail, 2); diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/own-sharing-usize.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/own-sharing-usize.rs new file mode 100644 index 0000000000000..86dcf0db19909 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/own-sharing-usize.rs @@ -0,0 +1,134 @@ +#![feature(core_intrinsics)] +#![allow(internal_features)] +use std::cell::UnsafeCell; + +#[repr(C, align(8))] +pub struct AtomicUsize { + v: UnsafeCell, +} + +unsafe impl Sync for AtomicUsize {} + +/*@ +fix accepts_usize(value: usize) -> bool { true } +pred_ctor own_atomic_contents(p: *usize)(;) = std::intrinsics::atomic_points_to(p, 1, accepts_usize); +pred .own(t, value) = true; +pred .share(k, t, l) = [_]frac_borrow(k, own_atomic_contents(ref_origin(l) as *usize)); + +lem AtomicUsize_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *AtomicUsize) + req lifetime_inclusion(k1, k) == true &*& [_]AtomicUsize_share(k, t, l); + ens [_]AtomicUsize_share(k1, t, l); +{ + open AtomicUsize_share(k, t, l); + frac_borrow_mono(k, k1, own_atomic_contents(ref_origin(l) as *usize)); + close AtomicUsize_share(k1, t, l); + leak AtomicUsize_share(k1, t, l); +} + +lem AtomicUsize_sync(t1: thread_id_t) + req is_Sync(typeid(AtomicUsize)) == true &*& [_]AtomicUsize_share(?k, ?t0, ?l); + ens [_]AtomicUsize_share(k, t1, l); +{ + open AtomicUsize_share(k, t0, l); + close AtomicUsize_share(k, t1, l); + leak AtomicUsize_share(k, t1, l); +} + +lem AtomicUsize_share_full(k: lifetime_t, t: thread_id_t, l: *AtomicUsize) + req atomic_mask(MaskTop) &*& full_borrow(k, AtomicUsize_full_borrow_content(t, l)) &*& [?q]lifetime_token(k) &*& ref_origin(l) == l; + ens atomic_mask(MaskTop) &*& [_]AtomicUsize_share(k, t, l) &*& [q]lifetime_token(k); +{ + open_full_borrow_strong_m_(k, AtomicUsize_full_borrow_content(t, l)); + open AtomicUsize_full_borrow_content(t, l)(); + open AtomicUsize_own(t, _); + close_points_to(l); + to_u8s_(l); + from_u8s_(l); + assert (l as usize) % std::mem::align_of::() == 0; + assert std::mem::align_of::() == 8; + open_points_to(l); + std::intrinsics::atomic_align_of_usize(); + std::intrinsics::close_atomic_points_to_m(l as *usize, accepts_usize); + close own_atomic_contents(l as *usize)(); + close True(); + produce_lem_ptr_chunk restore_full_borrow_(True, own_atomic_contents(l as *usize), AtomicUsize_full_borrow_content(t, l))() { + open True(); + open own_atomic_contents(l as *usize)(); + std::intrinsics::open_atomic_points_to(l as *usize); + close_points_to(l); + assert *l |-> ?value; + close AtomicUsize_own(t, value); + open_points_to(l); + close AtomicUsize_full_borrow_content(t, l)(); + } { + close_full_borrow_strong_m_(); + } + full_borrow_into_frac_m(k, own_atomic_contents(l as *usize)); + close AtomicUsize_share(k, t, l); + leak AtomicUsize_share(k, t, l); +} + +lem init_ref_AtomicUsize(p: *AtomicUsize) + req atomic_mask(Nlft) &*& ref_init_perm(p, ?x) &*& [_]AtomicUsize_share(?k, ?t, x) &*& [?q]lifetime_token(k); + ens atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]AtomicUsize_share(k, t, p) &*& [_]frac_borrow(k, ref_initialized_(p)); +{ + open AtomicUsize_share(k, t, x); + open_ref_init_perm_AtomicUsize(p); + close_ref_initialized_AtomicUsize(p, 1); + close ref_initialized_::(p)(); + borrow_m(k, ref_initialized_(p)); + leak borrow_end_token(k, ref_initialized_(p)); + full_borrow_into_frac_m(k, ref_initialized_(p)); + close AtomicUsize_share(k, t, p); + leak AtomicUsize_share(k, t, p); +} +@*/ + +impl AtomicUsize { + pub const unsafe fn from_ptr<'a>(ptr: *mut usize) -> &'a AtomicUsize + //@ req type_interp::() &*& atomic_mask(MaskTop) &*& [?q]lifetime_token('a) &*& *ptr |-> ?value &*& ptr as usize % std::mem::align_of::() == 0; + //@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [q]lifetime_token('a) &*& [_]AtomicUsize_share('a, currentThread, result) &*& [_]ref_initialized(result) &*& [_]frac_borrow('a, ref_initialized_(result)) &*& ref_origin(result) == ref_origin(ptr as *AtomicUsize) &*& borrow_end_token('a, AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)); + //@ on_unwind_ens false; + { + //@ close_points_to(ptr as *AtomicUsize); + //@ assert *(ptr as *AtomicUsize) |-> ?atomic; + //@ close AtomicUsize_own(currentThread, atomic); + //@ open_points_to(ptr as *AtomicUsize); + //@ close AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)(); + //@ borrow('a, AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)); + //@ share_full_borrow::('a, currentThread, ptr as *AtomicUsize); + //@ let p = precreate_ref(ptr as *AtomicUsize); + //@ init_ref_share::('a, currentThread, p); + //@ open_frac_borrow('a, ref_initialized_(p), q); + //@ open [?f]ref_initialized_::(p)(); + let result = unsafe { &*ptr.cast() }; + //@ close [f]ref_initialized_::(p)(); + //@ close_frac_borrow(f, ref_initialized_(p)); + //@ close_ref_initialized_AtomicUsize(p, 1); + //@ leak ref_initialized(p); + result + } + + pub fn store_relaxed<'a>(&'a self, value: usize) + //@ req [_]AtomicUsize_share('a, currentThread, self) &*& [?q]lifetime_token('a); + //@ ens [q]lifetime_token('a); + //@ on_unwind_ens false; + { + //@ open AtomicUsize_share('a, currentThread, self); + //@ let f = open_frac_borrow('a, own_atomic_contents(ref_origin(self) as *usize), q); + //@ open [f]own_atomic_contents(ref_origin(self) as *usize)(); + unsafe { std::intrinsics::atomic_store::(self.v.get(), value) } + //@ close [f]own_atomic_contents(ref_origin(self) as *usize)(); + //@ close_frac_borrow(f, own_atomic_contents(ref_origin(self) as *usize)); + } +} + +unsafe fn recover_plain_storage(ptr: *mut usize) +//@ req [_]lifetime_dead_token(?k) &*& borrow_end_token(k, AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)); +//@ ens *ptr |-> ?stored_value; +//@ on_unwind_ens false; +{ + //@ borrow_end(k, AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)); + //@ open AtomicUsize_full_borrow_content(currentThread, ptr as *AtomicUsize)(); + //@ open AtomicUsize_own(currentThread, _); +} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/self-free-negative.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/self-free-negative.rs new file mode 100644 index 0000000000000..e4bfc5c0066c3 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/self-free-negative.rs @@ -0,0 +1,13 @@ +struct A { value: u8 } +impl A { + unsafe fn check_self() + //@ req true; + //@ ens typeid(Self) == typeid(A); + //@ on_unwind_ens false; + {} +} +unsafe fn no_self_in_free_function() +//@ req true; +//@ ens typeid(Self) == typeid(A); +//@ on_unwind_ens false; +{} diff --git a/verifast-proofs/core/sync/atomic.rs/checks/source/self-positive.rs b/verifast-proofs/core/sync/atomic.rs/checks/source/self-positive.rs new file mode 100644 index 0000000000000..ae6bdd543915b --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/checks/source/self-positive.rs @@ -0,0 +1,24 @@ +struct A { value: u8 } +struct B { value: u16 } +struct Wrap { value: T } +impl A { + unsafe fn check_self() + //@ req true; + //@ ens typeid(Self) == typeid(A); + //@ on_unwind_ens false; + {} +} +impl B { + unsafe fn check_self() + //@ req true; + //@ ens typeid(Self) == typeid(B); + //@ on_unwind_ens false; + {} +} +impl Wrap { + unsafe fn check_self() + //@ req true; + //@ ens typeid(Self) == typeid(Wrap); + //@ on_unwind_ens false; + {} +} diff --git a/verifast-proofs/core/sync/atomic.rs/proof/check.py b/verifast-proofs/core/sync/atomic.rs/proof/check.py new file mode 100644 index 0000000000000..bf7b094b86e9b --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/check.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 +"""Check source identity, all from_ptr and generic wrapper proofs, and refinement.""" +from pathlib import Path +import json +import re +import subprocess +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent.parent / 'checks/operations')) +from annotate import OPS + +if len(sys.argv) != 2: + raise SystemExit('usage: run.py /absolute/path/to/experimental-runtime/bin') +base = Path(__file__).resolve().parent +runtime = Path(sys.argv[1]).resolve() +subprocess.run([sys.executable, str(base / 'generate.py')], check=True) +expected = {'atomic::AtomicBool::from_ptr', 'atomic::AtomicPtr::::from_ptr'} +expected.update('atomic::Atomic' + kind + '::from_ptr' + for kind in ('I8','U8','I16','U16','I32','U32','I64','U64','I128','U128','Isize','Usize')) +expected_wrappers = {'atomic::atomic_' + op for op in OPS} +args = '--edition=2024 --crate-type=lib' +command = [str(runtime / 'verifast'), '-verbose', '1', '-skip_specless_fns', + '-rustc_args', args, str(base / 'verified/lib.rs')] +result = subprocess.run(command, capture_output=True, text=True) +output = result.stdout + result.stderr +verified = set(re.findall(r"Verifying function '([^']+::from_ptr)'", output)) +wrappers = set(re.findall(r"Verifying function '(atomic::atomic_[^']+)'", output)) +target_match = re.search(r'target: (.*)\)', output) +target = target_match.group(1) if target_match else None +(base / 'proof.log').write_text('\n'.join(line for line in output.splitlines() + if 'Verifying function ' in line or 'errors found' in line or 'error:' in line) + '\n') +if result.returncode != 0 or '0 errors found' not in output or verified != expected or wrappers != expected_wrappers or target != 'arm64-apple-macosx (LP64)': + (base / 'failure.log').write_text(output) + raise SystemExit(f'Proof/coverage failed: exit={result.returncode}, missing={sorted((expected-verified) | (expected_wrappers-wrappers))}, extra={sorted((verified-expected) | (wrappers-expected_wrappers))}') +command = [str(runtime / 'refinement-checker'), '--verbose', '0', '--rustc-args', args, + str(base / 'normalized-original/lib.rs'), str(base / 'verified/lib.rs')] +result = subprocess.run(command, capture_output=True, text=True) +output = result.stdout + result.stderr +(base / 'refinement.log').write_text(output) +if result.returncode != 0 or 'No refinement errors found' not in output: + raise SystemExit('Refinement failed; see refinement.log') +expected_clients = {'clients::alias_' + name for name in ('bool','ptr','i8','u8','i16','u16','i32','u32','i64','u64','i128','u128','isize','usize')} +result = subprocess.run([str(runtime / 'verifast'), '-verbose','1','-skip_specless_fns', + '-rustc_args',args,str(base / 'clients-lib.rs')], capture_output=True, text=True) +output = result.stdout + result.stderr +clients = set(re.findall(r"Verifying function '(clients::alias_[^']+)'", output)) +(base / 'clients.log').write_text('\n'.join(line for line in output.splitlines() if 'Verifying function ' in line or 'errors found' in line or 'error:' in line) + '\n') +if result.returncode != 0 or '0 errors found' not in output or clients != expected_clients: + (base / 'failure.log').write_text(output) + raise SystemExit('Fresh/shared caller coverage failed') +client_controls = {} +for name, diagnostic in [('double-fresh','No matching heap chunks: points_to'), + ('shared-without-permission','No matching heap chunks: [_]atomic::AtomicBool_share'), + ('uninitialized','No matching heap chunks: points_to')]: + result = subprocess.run([str(runtime / 'verifast'), '-skip_specless_fns', '-rustc_args',args, + str(base / f'clients-{name}-lib.rs')], capture_output=True, text=True) + output = result.stdout + result.stderr + (base / f'clients-{name}.log').write_text(output) + client_controls[name] = result.returncode != 0 and diagnostic in output + if not client_controls[name]: + raise SystemExit(f'Unexpected {name} control: ' + output) +(base / 'coverage.json').write_text(json.dumps({ + 'runtime': str(runtime), 'approved_release': False, + 'rust_edition': 2024, 'target': target, + 'source_identity_checked': True, + 'source_normalization': 'rustc_diagnostic_item attributes changed to doc attributes in both proof inputs', + 'from_ptr_functions_verified': sorted(verified), + 'generic_operation_wrappers_verified': sorted(wrappers), + 'panic_paths_verified': True, + 'allow_dead_code': False, + 'fresh_and_shared_callers_verified': sorted(clients), + 'from_ptr_negative_controls': client_controls, + 'refinement_passed': True, + 'remaining': ['independent model and source-boundary review', 'acceptance of tool patch and source preparation', 'CI integration'], +}, indent=2) + '\n') +print(f'PASS: exact source copy, all {len(verified)} from_ptr bodies, all {len(wrappers)} generic operation wrappers, panic paths, {len(clients)} fresh/shared callers, 3 negative controls, and whole-module refinement after documented metadata normalization.') diff --git a/verifast-proofs/core/sync/atomic.rs/proof/generate.py b/verifast-proofs/core/sync/atomic.rs/proof/generate.py new file mode 100644 index 0000000000000..1909ee71104ed --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/generate.py @@ -0,0 +1,104 @@ +from pathlib import Path +import importlib.util + +base = Path(__file__).resolve().parent +(base / 'verified').mkdir(exist_ok=True) +repository = next(p for p in base.parents if (p / 'library/core/src/sync/atomic.rs').is_file()) +import json +import hashlib +lock = json.loads((base.parent / 'source-lock.json').read_text()) +for name, digest in lock['sources'].items(): + assert hashlib.sha256((repository / name).read_bytes()).hexdigest() == digest, f'Source changed; review and update the proof: {name}' +source = (repository / 'library/core/src/sync/atomic.rs').read_text() +(base / 'original').mkdir(exist_ok=True) +(base / 'original/atomic.rs').write_text(source) +(base / 'original/lib.rs').write_text((base / 'templates/lib.rs').read_text()) +normalized = source.replace('rustc_diagnostic_item = ', 'doc = ') +original = base / 'normalized-original' +original.mkdir(exist_ok=True) +(original / 'atomic.rs').write_text(normalized) +(original / 'lib.rs').write_text((base / 'original/lib.rs').read_text()) + +ghost_template = (base / 'templates/integer-share.rs').read_text() +ghosts = [] +for t, atomic in [('i8','AtomicI8'),('u8','AtomicU8'),('i16','AtomicI16'),('u16','AtomicU16'),('i32','AtomicI32'),('u32','AtomicU32'),('i64','AtomicI64'),('u64','AtomicU64'),('i128','AtomicI128'),('u128','AtomicU128'),('isize','AtomicIsize'),('usize','AtomicUsize')]: + block = ghost_template.replace('AtomicU8',atomic).replace('u8',t).replace('own_atomic_contents','own_atomic_contents_'+t) + block = block.replace(' div_rem(l as usize, 1);', " close_points_to(l);\n to_u8s_(l);\n from_u8s_(l);\n open_points_to(l);") + ghosts.append(block) +bool_ghost = ghost_template.replace('AtomicU8','AtomicBool').replace('accepts_u8','accepts_bool_byte').replace('own_atomic_contents','own_atomic_bool_contents') +bool_ghost = bool_ghost.replace('fix accepts_bool_byte(value: u8) -> bool { true }', 'fix accepts_bool_byte(value: u8) -> bool { value == 0 || value == 1 }') +bool_ghost = bool_ghost.replace('pred .own(t, value) = true;', 'pred .own(t, value) = value.v == 0 || value.v == 1;') +ghosts.append(bool_ghost) +ghosts.append((base / 'templates/atomic-ptr-share.rs').read_text()) +ghost = '\n\n'.join(ghosts) +attributes = ''' #[inline] + #[stable(feature = "atomic_from_ptr", since = "1.75.0")] + #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] +''' +old = attributes + ''' pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type { + // SAFETY: guaranteed by the caller + unsafe { &*ptr.cast() } + }''' +assert normalized.count(old) == 1 +method = (base / 'templates/from-ptr.rs').read_text() +verified = normalized.replace(old, attributes + method) +bool_original = """ pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool { + // SAFETY: guaranteed by the caller + unsafe { &*ptr.cast() } + }""" +bool_method = method.replace("ptr: *mut $int_type) -> &'a $atomic_type", "ptr: *mut bool) -> &'a AtomicBool") +bool_method = bool_method.replace(' close_points_to(ptr as *Self);', ' points_to_bool_to_u8(ptr);\n close_points_to(ptr as *Self);') +assert verified.count(bool_original) == 1 +verified = verified.replace(bool_original, bool_method) +ptr_original = """ pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr { + // SAFETY: guaranteed by the caller + unsafe { &*ptr.cast() } + }""" +ptr_method = method.replace("ptr: *mut $int_type) -> &'a $atomic_type", "ptr: *mut *mut T) -> &'a AtomicPtr") +ptr_method = ptr_method.replace('type_interp::()', 'type_interp::() &*& type_interp::()') +assert verified.count(ptr_original) == 1 +verified = verified.replace(ptr_original, ptr_method) + +anchor = '#[cfg(target_has_atomic_load_store)]\nmacro_rules! atomic_int {' +assert verified.count(anchor) == 1 +verified = verified.replace(anchor, ghost + '\n\n' + anchor) +module_spec = importlib.util.spec_from_file_location('atomic_operation_annotations', base.parent / 'checks/operations/annotate.py') +operation_annotations = importlib.util.module_from_spec(module_spec) +module_spec.loader.exec_module(operation_annotations) +verified = operation_annotations.annotate(verified) +(base / 'verified/atomic.rs').write_text(verified) +(base / 'verified/lib.rs').write_text((base / 'original/lib.rs').read_text()) +clients_root = (base / 'original/lib.rs').read_text().replace('pub mod atomic;', '#[path="verified/atomic.rs"]\npub mod atomic;\nmod clients;') +(base / 'clients-lib.rs').write_text(clients_root) +clients = 'use crate::atomic::*;\n\n' +for primitive, atomic, name in [('bool','AtomicBool','bool'), ('*mut T','AtomicPtr','ptr'), *[(t,'Atomic'+a,t) for t,a in [('i8','I8'),('u8','U8'),('i16','I16'),('u16','U16'),('i32','I32'),('u32','U32'),('i64','I64'),('u64','U64'),('i128','I128'),('u128','U128'),('isize','Isize'),('usize','Usize')]]]: + generics = "<'a, T>" if name == 'ptr' else "<'a>" + interp = f'type_interp::<{atomic}>() &*& ' + ('type_interp::() &*& ' if name == 'ptr' else '') + constructor = 'AtomicPtr::' if name == 'ptr' else atomic + call_args = "T, 'a" if name == 'ptr' else "'a" + clients += f'''unsafe fn alias_{name}{generics}(ptr: *mut {primitive}) -> (&'a {atomic}, &'a {atomic}) +//@ req {interp}atomic_mask(MaskTop) &*& [?q]lifetime_token('a) &*& *ptr |-> ?value &*& ptr as usize % std::mem::align_of::<{atomic}>() == 0; +//@ ens {interp}atomic_mask(MaskTop) &*& [q]lifetime_token('a) &*& [_](<{atomic}>.share)('a, currentThread, result.0) &*& [_](<{atomic}>.share)('a, currentThread, result.1) &*& borrow_end_token('a, (<{atomic}>.full_borrow_content)(currentThread, ptr as *{atomic})); +//@ on_unwind_ens false; +{{ + //@ close exists::(true); + let first = unsafe {{ {constructor}::from_ptr/*@::<{call_args}>@*/(ptr) }}; + //@ close exists::(false); + let second = unsafe {{ {constructor}::from_ptr/*@::<{call_args}>@*/(ptr) }}; + (first, second) +}} + +''' +import re +clients = '\n'.join(re.sub(r'\bAtomic(?=[A-Z])', 'atomic::Atomic', line) if line.startswith('//@') else line for line in clients.splitlines()) + '\n' +(base / 'clients.rs').write_text(clients) +first_client = clients[:clients.index('unsafe fn alias_ptr')] +negative_clients = { + 'double-fresh': first_client.replace('close exists::(false)', 'close exists::(true)'), + 'shared-without-permission': first_client.replace('close exists::(true)', 'close exists::(false)'), + 'uninitialized': first_client.replace(' &*& *ptr |-> ?value', ''), +} +for name, client_source in negative_clients.items(): + (base / f'clients-{name}.rs').write_text(client_source) + (base / f'clients-{name}-lib.rs').write_text(clients_root.replace('mod clients;', f'#[path="clients-{name}.rs"]\nmod clients;')) +print('Generated experimental normalized-original and Self-annotated verified copies.') diff --git a/verifast-proofs/core/sync/atomic.rs/proof/templates/atomic-ptr-share.rs b/verifast-proofs/core/sync/atomic.rs/proof/templates/atomic-ptr-share.rs new file mode 100644 index 0000000000000..682c53cbe86be --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/templates/atomic-ptr-share.rs @@ -0,0 +1,94 @@ +/*@ +lem ptr_alignment_product(x: i32, y: i32) + req true; + ens x * (std::mem::size_of::() * y) == std::mem::size_of::() * (x * y); +{} + +fix accepts_ptr(value: *T) -> bool { true } +pred_ctor own_atomic_ptr_contents(p: **T)(;) = std::intrinsics::atomic_points_to(p, 1, accepts_ptr); +pred >.own(t, value) = true; +pred >.share(k, t, l) = [_]frac_borrow(k, own_atomic_ptr_contents::(ref_origin(l) as **T)); + +lem AtomicPtr_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *AtomicPtr) + req type_interp::() &*& lifetime_inclusion(k1, k) == true &*& [_]AtomicPtr_share::(k, t, l); + ens type_interp::() &*& [_]AtomicPtr_share::(k1, t, l); +{ + open AtomicPtr_share::(k, t, l); + frac_borrow_mono(k, k1, own_atomic_ptr_contents::(ref_origin(l) as **T)); + close AtomicPtr_share::(k1, t, l); + leak AtomicPtr_share::(k1, t, l); +} + +lem AtomicPtr_sync(t1: thread_id_t) + req type_interp::() &*& is_Sync(typeid(AtomicPtr)) == true &*& [_]AtomicPtr_share::(?k, ?t0, ?l); + ens type_interp::() &*& [_]AtomicPtr_share::(k, t1, l); +{ + open AtomicPtr_share::(k, t0, l); + close AtomicPtr_share::(k, t1, l); + leak AtomicPtr_share::(k, t1, l); +} + +lem AtomicPtr_send(t1: thread_id_t) + req type_interp::() &*& is_Send(typeid(AtomicPtr)) == true &*& AtomicPtr_own::(?t0, ?value); + ens type_interp::() &*& AtomicPtr_own::(t1, value); +{ + open AtomicPtr_own::(t0, value); + close AtomicPtr_own::(t1, value); +} + +lem AtomicPtr_share_full(k: lifetime_t, t: thread_id_t, l: *AtomicPtr) + req type_interp::() &*& atomic_mask(MaskTop) &*& full_borrow(k, AtomicPtr_full_borrow_content::(t, l)) &*& [?q]lifetime_token(k) &*& ref_origin(l) == l; + ens type_interp::() &*& atomic_mask(MaskTop) &*& [_]AtomicPtr_share::(k, t, l) &*& [q]lifetime_token(k); +{ + open_full_borrow_strong_m_(k, AtomicPtr_full_borrow_content::(t, l)); + open AtomicPtr_full_borrow_content::(t, l)(); + open AtomicPtr_own::(t, _); + close_points_to(l); + to_u8s_(l); + from_u8s_(l); + open_points_to(l); + let a = std::mem::align_of::>(); + let n = std::mem::size_of::(); + assert (l as usize) % a == 0; + assert a % n == 0; + assert a >= n; + div_rem_nonneg(l as usize, a); + div_rem_nonneg(a, n); + ptr_alignment_product((l as usize) / a, a / n); + div_rem_nonneg_unique(l as usize, n, (l as usize) / a * (a / n), 0); + std::intrinsics::atomic_align_of_ptr::(); + std::intrinsics::close_atomic_points_to_m(l as **T, accepts_ptr); + close own_atomic_ptr_contents::(l as **T)(); + close True(); + produce_lem_ptr_chunk restore_full_borrow_(True, own_atomic_ptr_contents::(l as **T), AtomicPtr_full_borrow_content::(t, l))() { + open True(); + open own_atomic_ptr_contents::(l as **T)(); + std::intrinsics::open_atomic_points_to(l as **T); + close_points_to(l); + assert *l |-> ?value; + close AtomicPtr_own::(t, value); + open_points_to(l); + close AtomicPtr_full_borrow_content::(t, l)(); + } { + close_full_borrow_strong_m_(); + } + full_borrow_into_frac_m(k, own_atomic_ptr_contents::(l as **T)); + close AtomicPtr_share::(k, t, l); + leak AtomicPtr_share::(k, t, l); +} + +lem init_ref_AtomicPtr(p: *AtomicPtr) + req type_interp::() &*& atomic_mask(Nlft) &*& ref_init_perm(p, ?x) &*& [_]AtomicPtr_share::(?k, ?t, x) &*& [?q]lifetime_token(k); + ens type_interp::() &*& atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]AtomicPtr_share::(k, t, p) &*& [_]frac_borrow(k, ref_initialized_(p)); +{ + open AtomicPtr_share::(k, t, x); + open_ref_init_perm_AtomicPtr(p); + close_ref_initialized_AtomicPtr(p, 1); + close ref_initialized_::>(p)(); + borrow_m(k, ref_initialized_(p)); + leak borrow_end_token(k, ref_initialized_(p)); + full_borrow_into_frac_m(k, ref_initialized_(p)); + close AtomicPtr_share::(k, t, p); + leak AtomicPtr_share::(k, t, p); +} +@*/ diff --git a/verifast-proofs/core/sync/atomic.rs/proof/templates/from-ptr.rs b/verifast-proofs/core/sync/atomic.rs/proof/templates/from-ptr.rs new file mode 100644 index 0000000000000..db6b5e445001f --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/templates/from-ptr.rs @@ -0,0 +1,23 @@ + pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type + //@ req type_interp::() &*& atomic_mask(MaskTop) &*& [?q]lifetime_token('a) &*& exists::(?fresh) &*& (if fresh { *ptr |-> ?value } else { [_](.share)('a, currentThread, ptr as *Self) }) &*& ptr as usize % std::mem::align_of::() == 0; + //@ ens type_interp::() &*& atomic_mask(MaskTop) &*& [q]lifetime_token('a) &*& [_](.share)('a, currentThread, result) &*& [_](.share)('a, currentThread, ptr as *Self) &*& [_]frac_borrow('a, ref_initialized_(result)) &*& ref_origin(result) == ref_origin(ptr as *Self) &*& (if fresh { borrow_end_token('a, (.full_borrow_content)(currentThread, ptr as *Self)) } else { true }); + //@ on_unwind_ens false; + { + //@ open exists::(fresh); + /*@ if fresh { + close_points_to(ptr as *Self); + assert *(ptr as *Self) |-> ?atomic; + close .own(currentThread, atomic); + close_full_borrow_content::(currentThread, ptr as *Self); + borrow('a, (.full_borrow_content)(currentThread, ptr as *Self)); + share_full_borrow::('a, currentThread, ptr as *Self); + } @*/ + //@ let p = precreate_ref(ptr as *Self); + //@ init_ref_share::('a, currentThread, p); + //@ open_frac_borrow('a, ref_initialized_(p), q); + //@ open [?f]ref_initialized_::(p)(); + let result = unsafe { &*ptr.cast() }; + //@ close [f]ref_initialized_::(p)(); + //@ close_frac_borrow(f, ref_initialized_(p)); + result + } \ No newline at end of file diff --git a/verifast-proofs/core/sync/atomic.rs/proof/templates/integer-share.rs b/verifast-proofs/core/sync/atomic.rs/proof/templates/integer-share.rs new file mode 100644 index 0000000000000..ae1306d39b0bf --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/templates/integer-share.rs @@ -0,0 +1,69 @@ +/*@ +fix accepts_u8(value: u8) -> bool { true } +pred_ctor own_atomic_contents(p: *u8)(;) = std::intrinsics::atomic_points_to(p, 1, accepts_u8); +pred .own(t, value) = true; +pred .share(k, t, l) = [_]frac_borrow(k, own_atomic_contents(ref_origin(l) as *u8)); + +lem AtomicU8_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *AtomicU8) + req lifetime_inclusion(k1, k) == true &*& [_]AtomicU8_share(k, t, l); + ens [_]AtomicU8_share(k1, t, l); +{ + open AtomicU8_share(k, t, l); + frac_borrow_mono(k, k1, own_atomic_contents(ref_origin(l) as *u8)); + close AtomicU8_share(k1, t, l); + leak AtomicU8_share(k1, t, l); +} + +lem AtomicU8_sync(t1: thread_id_t) + req is_Sync(typeid(AtomicU8)) == true &*& [_]AtomicU8_share(?k, ?t0, ?l); + ens [_]AtomicU8_share(k, t1, l); +{ + open AtomicU8_share(k, t0, l); + close AtomicU8_share(k, t1, l); + leak AtomicU8_share(k, t1, l); +} + +lem AtomicU8_share_full(k: lifetime_t, t: thread_id_t, l: *AtomicU8) + req atomic_mask(MaskTop) &*& full_borrow(k, AtomicU8_full_borrow_content(t, l)) &*& [?q]lifetime_token(k) &*& ref_origin(l) == l; + ens atomic_mask(MaskTop) &*& [_]AtomicU8_share(k, t, l) &*& [q]lifetime_token(k); +{ + open_full_borrow_strong_m_(k, AtomicU8_full_borrow_content(t, l)); + open AtomicU8_full_borrow_content(t, l)(); + open AtomicU8_own(t, _); + div_rem(l as usize, 1); + std::intrinsics::atomic_align_of_u8(); + std::intrinsics::close_atomic_points_to_m(l as *u8, accepts_u8); + close own_atomic_contents(l as *u8)(); + close True(); + produce_lem_ptr_chunk restore_full_borrow_(True, own_atomic_contents(l as *u8), AtomicU8_full_borrow_content(t, l))() { + open True(); + open own_atomic_contents(l as *u8)(); + std::intrinsics::open_atomic_points_to(l as *u8); + close_points_to(l); + assert *l |-> ?value; + close AtomicU8_own(t, value); + open_points_to(l); + close AtomicU8_full_borrow_content(t, l)(); + } { + close_full_borrow_strong_m_(); + } + full_borrow_into_frac_m(k, own_atomic_contents(l as *u8)); + close AtomicU8_share(k, t, l); + leak AtomicU8_share(k, t, l); +} + +lem init_ref_AtomicU8(p: *AtomicU8) + req atomic_mask(Nlft) &*& ref_init_perm(p, ?x) &*& [_]AtomicU8_share(?k, ?t, x) &*& [?q]lifetime_token(k); + ens atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]AtomicU8_share(k, t, p) &*& [_]frac_borrow(k, ref_initialized_(p)); +{ + open AtomicU8_share(k, t, x); + open_ref_init_perm_AtomicU8(p); + close_ref_initialized_AtomicU8(p, 1); + close ref_initialized_::(p)(); + borrow_m(k, ref_initialized_(p)); + leak borrow_end_token(k, ref_initialized_(p)); + full_borrow_into_frac_m(k, ref_initialized_(p)); + close AtomicU8_share(k, t, p); + leak AtomicU8_share(k, t, p); +} +@*/ \ No newline at end of file diff --git a/verifast-proofs/core/sync/atomic.rs/proof/templates/lib.rs b/verifast-proofs/core/sync/atomic.rs/proof/templates/lib.rs new file mode 100644 index 0000000000000..5174291c8f74a --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/proof/templates/lib.rs @@ -0,0 +1,5 @@ +#![feature(core_intrinsics, staged_api, rustc_attrs, cfg_target_has_atomic, cfg_target_has_atomic_equal_alignment, decl_macro, const_trait_impl, const_convert, deprecated_suggestion)] +#![allow(internal_features)] +#![stable(feature = "atomic_source_proof", since = "1.0.0")] +use core::{cell, fmt, hint, intrinsics, ptr}; +pub mod atomic; diff --git a/verifast-proofs/core/sync/atomic.rs/source-lock.json b/verifast-proofs/core/sync/atomic.rs/source-lock.json new file mode 100644 index 0000000000000..b69c6beed88ec --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/source-lock.json @@ -0,0 +1,8 @@ +{ + "repository_revision": "ad7590c3dbdfeb97f2b4c7254dc5f4787ca9e783", + "rust": "nightly-2025-11-25", + "sources": { + "library/core/src/sync/atomic.rs": "d038c12276122db2a1e0ec8453df3b20302be6bf74d3108aca1fe2b09c678160", + "library/core/src/intrinsics/mod.rs": "28678854f5401c08bcc675531c4b167c7c08f7599887757ee5fd246072f0f815" + } +} diff --git a/verifast-proofs/core/sync/atomic.rs/toolchain/build.py b/verifast-proofs/core/sync/atomic.rs/toolchain/build.py new file mode 100644 index 0000000000000..735e04d671501 --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/toolchain/build.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Rebuild the experimental atomic verifier from pinned release inputs. + +The source and dependency trees are freshly extracted. No previous verifier +binary is used except for unchanged runtime resources from the verified release. +""" +from pathlib import Path +import argparse +import hashlib +import json +import os +import platform +import shlex +import shutil +import subprocess +import tarfile + +parser = argparse.ArgumentParser() +parser.add_argument('--workdir', type=Path, required=True) +parser.add_argument('--downloads', type=Path, required=True) +parser.add_argument('--cargo-home', type=Path) +parser.add_argument('--offline', action='store_true') +parser.add_argument('--check', action='store_true') +args = parser.parse_args() +base = Path(__file__).resolve().parent +repo = next(p for p in base.parents if (p / 'library/core/src/sync/atomic.rs').is_file()) +provenance = json.loads((base / 'provenance.json').read_text()) +if platform.system() != 'Darwin' or platform.machine() != 'arm64': + raise SystemExit('This complete-type proof build requires native ARM64 macOS.') +work = args.workdir.resolve() +if work.exists(): + raise SystemExit(f'Refusing to reuse a previous build tree: {work}') +work.mkdir(parents=True) +downloads = args.downloads.resolve() +downloads.mkdir(parents=True, exist_ok=True) + +def sha(path): + h = hashlib.sha256() + with path.open('rb') as stream: + for chunk in iter(lambda: stream.read(1024 * 1024), b''): + h.update(chunk) + return h.hexdigest() + +def run(command, *, cwd=repo, env=None, log=None): + print('+ ' + shlex.join(map(str, command)), flush=True) + if log: + with (work / log).open('w') as output: + subprocess.run(list(map(str, command)), cwd=cwd, env=env, stdout=output, stderr=subprocess.STDOUT, check=True) + else: + subprocess.run(list(map(str, command)), cwd=cwd, env=env, check=True) + +inputs = [ + ('verifast-source-26.01.tar.gz', 'https://api.github.com/repos/verifast/verifast/tarball/26.01', provenance['source_archive_sha256']), + ('vfdeps-adf88dc-macos-aarch64.txz', 'https://github.com/verifast/vfdeps/releases/download/25.01/vfdeps-adf88dc-macos-aarch64.txz', provenance['vfdeps_archive_sha256']), + ('verifast-26.01-macos-aarch.tar.gz', 'https://github.com/verifast/verifast/releases/download/26.01/verifast-26.01-macos-aarch.tar.gz', 'f316062f224b51f0956bf7375f34089558f4847671ef60e13899da6e079caf00'), +] +for name, url, digest in inputs: + archive = downloads / name + if not archive.exists(): + if args.offline: + raise SystemExit(f'Missing offline input: {archive}') + run(['curl','--fail','--location','--retry','3','--output',archive,url]) + if sha(archive) != digest: + raise SystemExit(f'Archive digest mismatch: {archive}') + print(f'Extracting verified {name}', flush=True) + with tarfile.open(archive) as packed: + # All release links are relative. The data filter rejects extraction + # outside this fresh build directory and disallows special files. + packed.extractall(work, filter='data') + +source = work / provenance['source_archive_prefix'] +deps = work / 'vfdeps-adf88dc' +runtime = work / 'verifast-26.01' +patch = base / 'verifast-26.01-atomic-source.patch' +if sha(patch) != provenance['source_patch_sha256']: + raise SystemExit('Patch digest does not match its provenance record.') +run(['git','apply','--check',patch], cwd=source) +run(['git','apply',patch], cwd=source) + +env = os.environ.copy() +cargo_home = (args.cargo_home or (work / 'cargo-home')).resolve() +decoder = work / 'decoder' +env.update({ + 'CARGO_HOME': str(cargo_home), + 'PATH': os.pathsep.join([str(deps / 'bin'), str(decoder / 'bin'), env['PATH']]), + 'OCAMLLIB': str(deps / 'lib/ocaml'), + 'OCAMLPATH': str(deps / 'lib/ocaml'), + 'OCAMLFIND_CONF': str(deps / 'etc/findlib-relocated.conf'), + 'CAML_LD_LIBRARY_PATH': str(deps / 'lib/ocaml/stublibs'), + 'DYLD_LIBRARY_PATH': str(deps / 'lib'), + 'CAPNP_INCLUDE': str(deps / 'include'), + 'CAPNP_INC_DIR': str(deps / 'include'), + 'Z3_DLL_DIR': str(deps / 'lib'), +}) +(deps / 'etc/findlib-relocated.conf').write_text( + f'destdir="{deps / "lib/ocaml"}"\npath="{deps / "lib/ocaml"}"\n' + 'ocamlc="ocamlc.opt"\nocamlopt="ocamlopt.opt"\nocamldep="ocamldep.opt"\nocamldoc="ocamldoc.opt"\n') +rust = provenance['rust'] +run(['rustc','+' + rust,'--version'], env=env) +offline = ['--offline'] if args.offline else [] +run(['cargo','+' + rust,'install','--locked','--git','https://github.com/btj/capnpc-ocaml-decoder', + '--rev',provenance['decoder_utility_commit'],'--root',decoder,*offline], env=env, log='decoder-build.log') +run(['cargo','+' + rust,'build','--release','--locked',*offline,'--manifest-path', + source / 'src/rust_frontend/vf_mir_exporter/Cargo.toml'], env=env, log='exporter-build.log') +run(['dune','build','vfconsole/vfconsole.exe','refinement_checker/main.exe'], cwd=source / 'src', env=env, log='verifier-build.log') + +stage = [ + ('src/_build/default/vfconsole/vfconsole.exe','bin/verifast'), + ('src/_build/default/refinement_checker/main.exe','bin/refinement-checker'), + ('src/rust_frontend/vf_mir_exporter/target/release/vf_mir_exporter','bin/vf-rust-mir-exporter'), + ('bin/rust/std/lib.rsspec','bin/rust/std/lib.rsspec'), +] +for source_name, destination_name in stage: + destination = runtime / destination_name + destination.unlink() + shutil.copy2(source / source_name, destination) +(runtime / 'bin/VERSION').write_text('26.01-local-atomic-source\n26.01 + LOCAL atomic-source probe (unsubmitted experimental patch)\n') + +# This wrapper is portable between checkouts: only generated output contains +# absolute relocation paths. It does not replace the user's global toolchain. +wrapper = work / 'with-build-env' +keys = ['CARGO_HOME','PATH','OCAMLLIB','OCAMLPATH','OCAMLFIND_CONF','CAML_LD_LIBRARY_PATH', + 'DYLD_LIBRARY_PATH','CAPNP_INCLUDE','CAPNP_INC_DIR','Z3_DLL_DIR'] +wrapper.write_text('#!/bin/sh\nset -eu\n' + ''.join('export ' + key + '=' + shlex.quote(env[key]) + '\n' for key in keys) + 'exec "$@"\n') +wrapper.chmod(0o755) + +if args.check: + run(['python3',base.parent / 'check.py',runtime / 'bin'], env=env, log='proof-suite.log') +manifest = { + 'approved_release': False, + 'fresh_source_build': True, + 'rust': rust, + 'platform': platform.platform(), + 'input_archives': {name: digest for name, _, digest in inputs}, + 'patch_sha256': sha(patch), + 'decoder_revision': provenance['decoder_utility_commit'], + 'patched_sources': {name: sha(source / name) for name in provenance['modified_files']}, + 'staged_outputs': {destination: sha(runtime / destination) for _, destination in stage}, + 'proof_suite_passed': args.check, + 'runtime': str(runtime), +} +(work / 'build-manifest.json').write_text(json.dumps(manifest, indent=2) + '\n') +print(f'PASS: fresh build{" and proof suite" if args.check else ""}; manifest: {work / "build-manifest.json"}', flush=True) diff --git a/verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json b/verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json new file mode 100644 index 0000000000000..588b893c6afdb --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json @@ -0,0 +1,42 @@ +{ + "status": "proposed VeriFast 26.01 update; unreleased and subject to review", + "verifast_base": "26.01", + "source_archive_prefix": "verifast-verifast-dcfad5b", + "source_archive_sha256": "0bcffc9ff57c0adf3d659c27a9b0e504bb0be878d84e7a4841cb7616633ff0a7", + "vfdeps_archive_sha256": "8bd48b02aa1887321d28b8490fe5803ea045845324f5d2adf49e72ddb6643bc1", + "vfdeps_release": "25.01", + "vfdeps_asset": "vfdeps-adf88dc-macos-aarch64.txz", + "decoder_utility_commit": "2d6606d9b59cd0c88a66729f3f076c10c0c8e0b2", + "rust": "nightly-2025-11-25", + "target": "arm64-apple-macosx (LP64)", + "runtime": "verifast-26.01 in the fresh build directory", + "runtime_label": "26.01-local-atomic-source", + "approved_release": false, + "modified_files": [ + "src/frontend/ast.ml", + "src/frontend/ocaml_expr_of_ast.ml", + "src/SExpressionEmitter.ml", + "src/verifast1.ml", + "src/rust_frontend/vf_mir/vf_mir.capnp", + "src/rust_frontend/vf_mir_exporter/src/lib.rs", + "src/rust_frontend/vf_mir_exporter/src/preprocessor.rs", + "src/rust_frontend/vf_mir_translator/rust_parser.ml", + "src/rust_frontend/vf_mir_translator/vf_mir_translator.ml", + "src/refinement_checker/refinement_checker.ml", + "bin/rust/std/lib.rsspec" + ], + "source_patch_sha256": "689ade100389e4a7d9a4e3fcc47ad51d9bfb61d6d103afbdf875cfe77077d48f", + "rust_edition": 2024, + "new_gates": [ + "compiler-resolved Self", + "repeated macro contracts", + "compiler ABI alignment and repr alignment lower bound", + "all 14 from_ptr bodies and complete module refinement after metadata normalization", + "all 15 generic operation wrappers including unwind paths", + "91 concrete legal ordering combinations", + "12 integer and 5 pointer element-size domain witnesses", + "29 operation controls including boolean invariant failures", + "25 malformed MIR decoder controls in a separate replay runtime", + "all 14 from_ptr fresh/shared callers and three ownership rejection controls" + ] +} diff --git a/verifast-proofs/core/sync/atomic.rs/toolchain/verifast-26.01-atomic-source.patch b/verifast-proofs/core/sync/atomic.rs/toolchain/verifast-26.01-atomic-source.patch new file mode 100644 index 0000000000000..d8331ccd048ec --- /dev/null +++ b/verifast-proofs/core/sync/atomic.rs/toolchain/verifast-26.01-atomic-source.patch @@ -0,0 +1,1214 @@ +--- a/src/frontend/ast.ml ++++ b/src/frontend/ast.ml +@@ -1120,6 +1120,8 @@ + struct_attr = + | Packed + | ReprC ++ | RustcAbiAlignment of int (* Compiler-exported fact, not a source annotation. *) ++ | RustcMinimumAlignment of int + and constant_value = (* ?constant_value *) + IntConst of big_int + | BoolConst of bool +--- a/src/frontend/ocaml_expr_of_ast.ml ++++ b/src/frontend/ocaml_expr_of_ast.ml +@@ -1170,6 +1170,8 @@ + and of_struct_attr = function + Packed -> c "Packed" + | ReprC -> c "ReprC" ++| RustcAbiAlignment n -> C ("RustcAbiAlignment", [I n]) ++| RustcMinimumAlignment n -> C ("RustcMinimumAlignment", [I n]) + and of_constant_value = function + IntConst n -> C ("IntConst", [BigInt n]) + | BoolConst b -> C ("BoolConst", [B b]) +--- a/src/SExpressionEmitter.ml ++++ b/src/SExpressionEmitter.ml +@@ -170,6 +170,9 @@ + + let sexpr_of_attr : struct_attr -> sexpression = function + | Packed -> Symbol "packed" ++ | ReprC -> Symbol "repr-c" ++ | RustcAbiAlignment n -> List [Symbol "rustc-abi-alignment"; Number (Big_int.big_int_of_int n)] ++ | RustcMinimumAlignment n -> List [Symbol "rustc-minimum-alignment"; Number (Big_int.big_int_of_int n)] + + let sexpr_of_field (Field (loc, ghostness, type_expr, name, binding, visibility, final, expr)) : sexpression = + build_list +--- a/src/verifast1.ml ++++ b/src/verifast1.ml +@@ -6500,6 +6500,21 @@ + ctxt#assume_forall name [trigger] (List.map (fun x -> ctxt#type_inductive) tparams) fact + end + in ++ List.iter (function ++ | RustcAbiAlignment n -> ++ if dialect <> Some Rust || tparams <> [] || n <= 0 || n land (n - 1) <> 0 then ++ static_error l "Invalid compiler-exported concrete ABI alignment" None; ++ let type_info = ctxt#mk_app type_info_func [] in ++ ctxt#assert_term (ctxt#mk_eq (mk_alignof type_info) (ctxt#mk_intlit n)) ++ | RustcMinimumAlignment n -> ++ if dialect <> Some Rust || n <= 0 || n land (n - 1) <> 0 then ++ static_error l "Invalid compiler-exported minimum alignment" None; ++ assume_axiom (fun _ targs _ -> ++ let a = mk_alignof (ctxt#mk_app type_info_func targs) in ++ (sn ^ "_minimum_alignment", a, ++ ctxt#mk_and (ctxt#mk_le (ctxt#mk_intlit n) a) ++ (ctxt#mk_eq (ctxt#mk_mod a (ctxt#mk_intlit n)) (ctxt#mk_intlit 0)))) ++ | _ -> ()) attrs; + let packed = List.mem Packed attrs in + let repr_c = dialect <> Some Rust || List.mem ReprC attrs in + assume_axiom (fun _ _ s -> (sn ^ "_size_limits", s, ctxt#mk_and (ctxt#mk_lt (ctxt#mk_intlit 0) s) (ctxt#mk_le s max_uintptr_term))); +--- a/src/rust_frontend/vf_mir/vf_mir.capnp ++++ b/src/rust_frontend/vf_mir/vf_mir.capnp +@@ -279,6 +279,8 @@ + predicates @7: List(Predicate); + implementsDrop @8: Bool; + isReprC @11: Bool; ++ knownAlignment @12: UInt64; # Zero if unknown; otherwise rustc's ABI alignment. ++ reprAlignment @13: UInt64; # Zero if absent; repr(align(N)) requires alignment to be a multiple of N. + } + + enum AliasTyKind { +@@ -870,6 +872,7 @@ + isTraitFn @12: Bool; + isDropFn @13: Bool; # Implements std::ops::Drop::drop + visibility @22: Visibility; ++ implSelfTy @26: Option(Ty); # Compiler-resolved Self for an inherent or trait impl. + } + + struct Trait { +--- a/src/rust_frontend/vf_mir_exporter/src/lib.rs ++++ b/src/rust_frontend/vf_mir_exporter/src/lib.rs +@@ -926,6 +926,10 @@ + // Encode traits (consumes annotations) + self.encode_traits(&mut req_adt_defs, vf_mir_cpn.reborrow()); + ++ // An annotation in a macro definition belongs to every expansion ++ // of that function. Keep an immutable source snapshot so consuming ++ // the first expansion does not silently leave later ones specless. ++ let source_body_annots = self.annots.clone(); + vf_mir_cpn.fill_bodies(&self.bodies, |mut body_cpn, (body, span)| { + Self::encode_span_data( + self.tcx, +@@ -944,6 +948,11 @@ + ) + }) + .collect::>(); ++ if body.span.from_expansion() { ++ annots = source_body_annots.iter().filter(|annot| { ++ body_span.contains(annot.span().expect("Dummy annot found during serialization").data()) ++ }).cloned().collect(); ++ } + let mut_annots = annots.extract_if(|annot| { + annot.kind == GhostRangeKind::Mut + }).map(|annot| { +@@ -1094,6 +1103,22 @@ + }); + adt_def_cpn.set_implements_drop(adt_def.has_dtor(tcx)); + adt_def_cpn.set_is_repr_c(adt_def.repr().c()); ++ if let Some(alignment) = adt_def.repr().align { ++ adt_def_cpn.set_repr_alignment(alignment.bytes()); ++ } ++ // Do not turn the alignment of one instantiation into a fact about ++ // every instantiation of a generic type. This first implementation ++ // deliberately exports layout only for types without parameters. ++ if tcx.generics_of(adt_def.did()).count() == 0 { ++ let adt_ty = tcx.type_of(adt_def.did()).instantiate_identity(); ++ let typing_env = ty::TypingEnv { ++ typing_mode: ty::TypingMode::PostAnalysis, ++ param_env: ty::ParamEnv::empty(), ++ }; ++ if let Ok(layout) = tcx.layout_of(typing_env.as_query_input(adt_ty)) { ++ adt_def_cpn.set_known_alignment(layout.align.abi.bytes()); ++ } ++ } + } + + fn encode_adt_kind(adt_kind: ty::AdtKind, mut adt_kind_cpn: adt_kind_cpn::Builder<'_>) { +@@ -1309,6 +1334,12 @@ + } + + if let Some(impl_did) = tcx.impl_of_assoc(def_id) { ++ Self::encode_ty( ++ tcx, ++ enc_ctx, ++ tcx.type_of(impl_did).instantiate_identity(), ++ body_cpn.reborrow().init_impl_self_ty().init_something(), ++ ); + let impl_hir_gens = tcx.hir_get_generics(impl_did.expect_local()).unwrap(); + let impl_hir_generics_cpn = body_cpn.reborrow().init_impl_block_hir_generics(); + let impl_hir_generics_some_cpn = impl_hir_generics_cpn.init_something(); +--- a/src/rust_frontend/vf_mir_exporter/src/preprocessor.rs ++++ b/src/rust_frontend/vf_mir_exporter/src/preprocessor.rs +@@ -68,7 +68,7 @@ + Mut, + } + +-#[derive(Debug)] ++#[derive(Clone, Debug)] + pub struct GhostRange { + in_fn_body: bool, + pub kind: GhostRangeKind, +--- a/src/rust_frontend/vf_mir_translator/rust_parser.ml ++++ b/src/rust_frontend/vf_mir_translator/rust_parser.ml +@@ -4,6 +4,11 @@ + open Parser + open Big_int + open Verifast0 ++ ++(* Set only while parsing one compiler-exported impl body; restored even when ++ parsing fails. Outside an impl, Self retains its existing trait-parameter ++ interpretation. The exporter supplies the type, not the function's name. *) ++let impl_self_ty : Ast.type_expr option ref = ref None + + let expr_of_lft_param_expr loc e = CallExpr (loc, "lft_of", [], [], [LitPat (Typeid (loc, TypeExpr e))], Static) + let expr_of_lft_param loc x = expr_of_lft_param_expr loc (match x with "'static" -> ManifestTypeExpr (loc, StaticLifetime) | _ -> IdentTypeExpr (loc, None, x)) +@@ -107,7 +112,8 @@ + parse_type as tp + ] -> RustRefTypeExpr (l, lft, mutability, tp) + | [ (l, Kwd "any") ] -> ManifestTypeExpr (l, AnyType) +-| [ (l, Kwd "Self") ] -> IdentTypeExpr (l, None, "Self") ++| [ (l, Kwd "Self") ] -> ++ (match !impl_self_ty with Some ty -> ty | None -> IdentTypeExpr (l, None, "Self")) + | [ (l, Kwd "("); + [%let tp = function%parser + [ (_, Kwd ")") ] -> StructTypeExpr (l, Some "std_tuple_0_", None, [], []) +--- a/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml ++++ b/src/rust_frontend/vf_mir_translator/vf_mir_translator.ml +@@ -1314,15 +1314,105 @@ + "std::mem::ManuallyDrop::deref_mut" + | _ -> name + ++ (* Preserve every concrete AtomicOrdering when selecting a trusted contract. ++ Generic operands are admitted only because every selected contract also ++ requires a ghost type-domain fact. Concrete invalid types are rejected here ++ before rustc's later monomorphization diagnostics could be skipped. *) ++ and specialize_atomic_intrinsic (fn_def_ty_cpn : D.ty_kind_fn_def_ty) ++ (loc : Ast.loc) = ++ let name = fn_def_ty_cpn.id.name in ++ let intrinsic = ++ match String.split_on_char ':' name with ++ | [("core" | "std"); ""; "intrinsics"; ""; op] -> Some op ++ | _ -> None ++ in ++ match intrinsic with ++ | Some (("atomic_store" | "atomic_load" | "atomic_xchg" | ++ "atomic_cxchg" | "atomic_cxchgweak" | "atomic_xadd" | ++ "atomic_xsub" | "atomic_and" | "atomic_nand" | "atomic_or" | ++ "atomic_xor" | "atomic_max" | "atomic_min" | "atomic_umax" | ++ "atomic_umin") as op) -> ++ let reject message = Ast.static_error loc (op ^ ": " ^ message) None in ++ if fn_def_ty_cpn.late_bound_generic_param_count <> 0 then ++ reject "late-bound generic arguments are not permitted"; ++ let rmw_pair = List.mem op ["atomic_xadd"; "atomic_xsub"; "atomic_and"; ++ "atomic_nand"; "atomic_or"; "atomic_xor"] in ++ let comparison = op = "atomic_cxchg" || op = "atomic_cxchgweak" in ++ let type_count = if rmw_pair then 2 else 1 in ++ let order_count = if comparison then 2 else 1 in ++ if List.length fn_def_ty_cpn.substs <> type_count + order_count then ++ reject "incorrect type/ordering argument count"; ++ let rec split n xs = if n = 0 then [], xs else ++ match xs with x :: xs -> let a, b = split (n - 1) xs in x :: a, b ++ | [] -> assert false in ++ let type_args, order_args = split type_count fn_def_ty_cpn.substs in ++ let operand (arg : D.generic_arg) = match arg.kind with ++ | Type ty -> ty ++ | _ -> reject "expected a type argument before ordering constants" in ++ let primary = operand (List.hd type_args) in ++ let is_integer (ty : D.ty) = match ty.kind with ++ | Int _ | UInt _ -> true | _ -> false in ++ let is_param (ty : D.ty) = match ty.kind with Param _ -> true | _ -> false in ++ let is_supported_pointer (ty : D.ty) = match ty.kind with ++ | RawPtr {ty = {kind = (Slice _ | Str | Dynamic _ | Foreign)}} -> false ++ | RawPtr _ -> true ++ | _ -> false in ++ if not (is_param primary || is_integer primary || is_supported_pointer primary) then ++ reject "operand must be an integer, thin raw pointer, or a generic type with an atomic-domain precondition"; ++ if List.mem op ["atomic_max"; "atomic_min"] then ++ (match primary.kind with Int _ | Param _ -> () ++ | _ -> reject "signed min/max require a signed integer operand"); ++ if List.mem op ["atomic_umax"; "atomic_umin"] then ++ (match primary.kind with UInt _ | Param _ -> () ++ | _ -> reject "unsigned min/max require an unsigned integer operand"); ++ if rmw_pair then begin ++ let secondary = operand (List.nth type_args 1) in ++ if not (is_param secondary || is_integer secondary) then ++ reject "RMW update operand must be an integer or a generic type"; ++ if not (is_param primary || is_param secondary) then ++ match primary.kind, secondary.kind with ++ | Int a, Int b when a = b -> () ++ | UInt a, UInt b when a = b -> () ++ | RawPtr _, UInt USize -> () ++ | _ -> reject "RMW operands must be the same integer type or (thin pointer, usize)" ++ end; ++ let ordering (arg : D.generic_arg) = match arg.kind with ++ | Const {kind = Value { ++ ty = {kind = Adt { ++ id = {name = ("core::intrinsics::AtomicOrdering" | ++ "std::intrinsics::AtomicOrdering")}; ++ kind = EnumKind; substs = []; ++ }}; ++ val_tree = Branch [Leaf {data; size = 4}]; ++ }} -> ++ (match Stdint.Uint128.to_string (DecoderAux.uint128_get data) with ++ | "0" -> "relaxed" | "1" -> "release" | "2" -> "acquire" ++ | "3" -> "acqrel" | "4" -> "seqcst" ++ | _ -> reject "invalid AtomicOrdering variant index") ++ | _ -> reject "expected a concrete fieldless AtomicOrdering enum constant encoded as one u32 variant index" in ++ let orders = List.map ordering order_args in ++ if op = "atomic_store" && List.mem (List.hd orders) ["acquire"; "acqrel"] then ++ reject "Acquire and AcqRel are not permitted for stores"; ++ if op = "atomic_load" && List.mem (List.hd orders) ["release"; "acqrel"] then ++ reject "Release and AcqRel are not permitted for loads"; ++ if comparison && List.mem (List.nth orders 1) ["release"; "acqrel"] then ++ reject "Release and AcqRel are not permitted for compare-exchange failure"; ++ Some ("std::intrinsics::" ^ op ^ "_" ^ String.concat "_" orders, type_args) ++ | _ -> None ++ ++ + and translate_fn_def_ty (fn_def_ty_cpn : D.ty_kind_fn_def_ty) (loc : Ast.loc) + = + let id_cpn = fn_def_ty_cpn.id in + let id = id_cpn.name in +- let name = TrName.translate_def_path id in ++ let name, substs_cpn = ++ match specialize_atomic_intrinsic fn_def_ty_cpn loc with ++ | Some specialization -> specialization ++ | None -> TrName.translate_def_path id, fn_def_ty_cpn.substs ++ in + let late_bound_generic_param_count = + fn_def_ty_cpn.late_bound_generic_param_count + in +- let substs_cpn = fn_def_ty_cpn.substs in + let* substs = + ListAux.try_map + (fun subst_cpn -> translate_generic_arg subst_cpn loc) +@@ -2206,17 +2296,19 @@ + | `TrOperandMove (Var (_, fn_name), place_is_mutable) -> + translate_regular_fn_call [] fn_name + | `TrTypedConstantFn fn_def_ty_cpn -> ( +- let fn_name = fn_def_ty_cpn.id.name in +- let substs_cpn = fn_def_ty_cpn.substs in +- let fn_name = translate_fn_name fn_name substs_cpn in +- let substs_cpn = +- substs_cpn +- @ List.init fn_def_ty_cpn.late_bound_generic_param_count +- (fun i : D.generic_arg -> +- { kind = Lifetime { id = "'erased" } }) +- in + let fn_name, substs_cpn = +- Args.body_tr_defs_ctx.fn_specializer fn_name substs_cpn ++ match specialize_atomic_intrinsic fn_def_ty_cpn call_loc with ++ | Some specialization -> specialization ++ | None -> ++ let substs_cpn = fn_def_ty_cpn.substs in ++ let fn_name = translate_fn_name fn_def_ty_cpn.id.name substs_cpn in ++ let substs_cpn = ++ substs_cpn ++ @ List.init fn_def_ty_cpn.late_bound_generic_param_count ++ (fun i : D.generic_arg -> ++ { kind = Lifetime { id = "'erased" } }) ++ in ++ Args.body_tr_defs_ctx.fn_specializer fn_name substs_cpn + in + let* substs = + ListAux.try_map +@@ -4679,7 +4771,7 @@ + [], + Static ))) + +- let translate_body (body_tr_defs_ctx : body_tr_defs_ctx) (body_cpn : BodyRd.t) ++ let translate_body_without_self_context (body_tr_defs_ctx : body_tr_defs_ctx) (body_cpn : BodyRd.t) + = + let open BodyRd in + let var_id_trs_map_ref = ref [] in +@@ -5021,6 +5113,21 @@ + ({ id = loc; info = env_map } : VF0.debug_info_rust_fe) ) + | DefKind.AssocFn -> failwith "Todo: MIR Body kind AssocFn" + | _ -> Error (`TrBodyFatal "Unknown MIR Body kind") ++ ++ let translate_body body_tr_defs_ctx body_cpn = ++ let* self_ty = ++ match OptionRd.get (BodyRd.impl_self_ty_get body_cpn) with ++ | OptionRd.Nothing -> Ok None ++ | OptionRd.Something ty -> ++ let* loc = translate_span_data (BodyRd.fn_sig_span_get body_cpn) in ++ let* ty = translate_decoded_ty (D.decode_ty (VfMirRd.of_pointer ty)) loc in ++ Ok (Some ty.Mir.vf_ty) ++ in ++ let previous = !Rust_parser.impl_self_ty in ++ Rust_parser.impl_self_ty := self_ty; ++ Fun.protect ++ ~finally:(fun () -> Rust_parser.impl_self_ty := previous) ++ (fun () -> translate_body_without_self_context body_tr_defs_ctx body_cpn) + + let translate_visibility (vis : D.visibility) = + match vis with +@@ -6037,6 +6144,34 @@ + let vis_cpn = vis_get adt_def_cpn in + let* vis = translate_visibility @@ D.decode_visibility vis_cpn in + let is_local = is_local_get adt_def_cpn in ++ let known_alignment = known_alignment_get adt_def_cpn in ++ let alignment_attrs = ++ if known_alignment = Stdint.Uint64.zero then [] ++ else begin ++ if vf_tparams <> [] then ++ Ast.static_error def_loc "A concrete ABI alignment for a generic ADT is not supported" None; ++ (* Rust's maximum permitted alignment is 2^29; this also makes the ++ conversion to the host OCaml int unambiguous. *) ++ if known_alignment > Stdint.Uint64.of_int (1 lsl 29) then ++ Ast.static_error def_loc "Invalid compiler-exported ABI alignment" None; ++ let n = Stdint.Uint64.to_int known_alignment in ++ if n <= 0 || n land (n - 1) <> 0 then ++ Ast.static_error def_loc "Invalid compiler-exported ABI alignment" None; ++ [Ast.RustcAbiAlignment n] ++ end ++ in ++ let repr_alignment = repr_alignment_get adt_def_cpn in ++ let alignment_attrs = ++ if repr_alignment = Stdint.Uint64.zero then alignment_attrs ++ else begin ++ if repr_alignment > Stdint.Uint64.of_int (1 lsl 29) then ++ Ast.static_error def_loc "Invalid compiler-exported minimum alignment" None; ++ let n = Stdint.Uint64.to_int repr_alignment in ++ if n <= 0 || n land (n - 1) <> 0 then ++ Ast.static_error def_loc "Invalid compiler-exported minimum alignment" None; ++ Ast.RustcMinimumAlignment n :: alignment_attrs ++ end ++ in + let kind_cpn = kind_get adt_def_cpn in + let* kind, fds, fds_no_zst, def, aux_decls = + match AdtKindRd.get kind_cpn with +@@ -6057,7 +6192,7 @@ + (*instance_pred_decl list*) [], + (*is polymorphic*) false ), + (*struct_attr list*) +- if is_repr_c_get adt_def_cpn then [ ReprC ] else [] ) ++ (if is_repr_c_get adt_def_cpn then [ Ast.ReprC ] else []) @ alignment_attrs ) + in + let struct_typedef_aux = + Ast.TypedefDecl +--- a/src/refinement_checker/refinement_checker.ml ++++ b/src/refinement_checker/refinement_checker.ml +@@ -85,6 +85,15 @@ + + let string_of_region = function + Region s -> s ++ ++type atomic_ordering = AtomicRelaxed | AtomicRelease | AtomicAcquire | AtomicAcqRel | AtomicSeqCst ++ ++let string_of_atomic_ordering = function ++ AtomicRelaxed -> "Relaxed" ++| AtomicRelease -> "Release" ++| AtomicAcquire -> "Acquire" ++| AtomicAcqRel -> "AcqRel" ++| AtomicSeqCst -> "SeqCst" + + type literal_const_expr = + BoolValue of bool +@@ -105,6 +114,7 @@ + and const_expr = + ParamConstExpr of string + | LiteralConstExpr of literal_const_expr ++| AtomicOrderingConst of string * atomic_ordering + and ty = + Bool + | Int of int_width +@@ -148,6 +158,7 @@ + let string_of_const_expr = function + ParamConstExpr param -> Printf.sprintf "ParamConstExpr %s" param + | LiteralConstExpr literal -> string_of_literal_const_expr literal ++| AtomicOrderingConst (name, ordering) -> name ^ "::" ^ string_of_atomic_ordering ordering + + let rec string_of_ty = function + Bool -> "Bool" +@@ -297,7 +308,25 @@ + let valtree = value_cpn.val_tree in + match valtree with + Leaf scalar_int_cpn -> LiteralConstExpr (decode_scalar_int ty scalar_int_cpn) +- | Branch _ -> failwith "Branch not supported" ++ | Branch branches -> ++ (* The pinned exporter encodes a fieldless enum as a singleton branch ++ containing its u32 variant index. Keep AtomicOrdering nominal and ++ distinct from integer constants; do not generalize this to other ADTs. *) ++ begin match ty, branches with ++ Adt (name, Enum, []), [Leaf {data; size=4}] ++ when name = "std::intrinsics::AtomicOrdering" || name = "core::intrinsics::AtomicOrdering" -> ++ let ordering = ++ match Stdint.Uint128.to_string (decode_uint128 data) with ++ "0" -> AtomicRelaxed ++ | "1" -> AtomicRelease ++ | "2" -> AtomicAcquire ++ | "3" -> AtomicAcqRel ++ | "4" -> AtomicSeqCst ++ | _ -> failwith "Unsupported AtomicOrdering variant index" ++ in ++ AtomicOrderingConst (name, ordering) ++ | _ -> failwith "Branch not supported (expected a fieldless AtomicOrdering constant)" ++ end + + type call_path = basic_block_path option + and basic_block_path = {bb_caller: basic_block_path option; bb_index: int} +@@ -619,6 +648,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + } + ); + ( +@@ -716,6 +746,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + } + ); + ("std::result::Result::::map", +@@ -955,6 +986,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + }); + ("std::result::Result::::map_err", + let span = Regular +@@ -1193,6 +1225,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + }); + ("std::option::Option::::map", + let span = Regular +@@ -1409,6 +1442,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + }); + "std::option::Option::::unwrap_or_else", + let span = Regular +@@ -1589,6 +1623,7 @@ + is_trait_fn=false; + is_drop_fn=false; + visibility=Public; ++ impl_self_ty=Nothing; + } + ] + +--- a/bin/rust/std/lib.rsspec ++++ b/bin/rust/std/lib.rsspec +@@ -326,6 +326,53 @@ + req true; + ens atomic_align_of::() == std::mem::size_of::(); + ++ // Atomic integer alignment is its size in the Rust atomic ABI. These are ++ // safety contracts for the trusted primitive operations, distinct from ++ // rustc-exported alignment of the actual enclosing struct. ++ lem_auto atomic_align_of_i8(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_i16(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_u16(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_i32(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_u32(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_i64(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_u64(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_i128(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_u128(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem_auto atomic_align_of_isize(); ++ req true; ++ ens atomic_align_of::() == std::mem::size_of::(); ++ ++ lem atomic_align_of_ptr(); ++ req true; ++ ens atomic_align_of::<*T>() == std::mem::size_of::(); ++ + pred atomic_points_to(p: *T, frac: real, inv_: fix(T, bool);); + + lem close_atomic_points_to_m(p: *T, inv_: fix(T, bool)); +@@ -338,21 +385,654 @@ + + @*/ + ++ // BEGIN LOCAL ATOMIC OPERATION MODEL ++ // The domain facts denote exactly the supported Rust intrinsic operand ++ // classes. Generic callers must establish them; T: Copy alone is not enough. ++ /*@ ++ fix atomic_type() -> bool; ++ fix atomic_signed_type() -> bool; ++ fix atomic_unsigned_type() -> bool; ++ fix atomic_rmw_types() -> bool; ++ ++ inductive atomic_rmw_op = RmwAdd | RmwSub | RmwAnd | RmwNand | RmwOr | RmwXor; ++ // The result of the primitive wrapping arithmetic/bitwise update. This ++ // function is abstract here; closure witnesses must work for its result. ++ fix atomic_rmw_value(stored_type: *_, update_type: *_, op: atomic_rmw_op, old: t, val: u) -> t; ++ lem_type atomic_rmw_preserves(stored_type: *_, update_type: *_, op: atomic_rmw_op, inv_: fix(t, bool), val: u) = lem(old: t); ++ req inv_(old) == true; ++ ens inv_(atomic_rmw_value(stored_type, update_type, op, old, val)) == true; ++ ++ lem_auto atomic_domain_i8(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_i8_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_i8_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_u8(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_u8_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_u8_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_i16(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_i16_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_i16_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_u16(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_u16_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_u16_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_i32(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_i32_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_i32_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_u32(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_u32_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_u32_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_i64(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_i64_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_i64_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_u64(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_u64_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_u64_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_i128(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_i128_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_i128_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_u128(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_u128_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_u128_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_isize(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_isize_sign(); ++ req true; ++ ens atomic_signed_type::() == true; ++ lem_auto atomic_domain_isize_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ lem_auto atomic_domain_usize(); ++ req true; ++ ens atomic_type::() == true; ++ lem_auto atomic_domain_usize_sign(); ++ req true; ++ ens atomic_unsigned_type::() == true; ++ lem_auto atomic_domain_usize_rmw(); ++ req true; ++ ens atomic_rmw_types::() == true; ++ ++ // A raw pointer to a sized type is thin. Pointer values need not be ++ // dereferenceable and the update operand is a byte count or bit mask. ++ lem atomic_domain_ptr(); ++ req true; ++ ens atomic_type::<*T>() == true &*& atomic_rmw_types::<*T, usize>() == true; ++ @*/ ++ ++ /*@ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwAnd, old, val)) atomic_rmw_u8_and(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwAnd, old, val) == (old & val); ++ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwNand, old, val)) atomic_rmw_u8_nand(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwNand, old, val) == (255 - (old & val)); ++ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwOr, old, val)) atomic_rmw_u8_or(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwOr, old, val) == (old | val); ++ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwXor, old, val)) atomic_rmw_u8_xor(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwXor, old, val) == (old ^ val); ++ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwAdd, old, val)) atomic_rmw_u8_add(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwAdd, old, val) == ((old + val) % 256); ++ ++ lem_auto(atomic_rmw_value(typeid(u8), typeid(u8), RmwSub, old, val)) atomic_rmw_u8_sub(old: u8, val: u8); ++ req true; ++ ens atomic_rmw_value(typeid(u8), typeid(u8), RmwSub, old, val) == ((old - val + 256) % 256); ++ ++ @*/ ++ ++ /*@ ++ // Exact restricted value tables for boolean-byte clients. ++ lem atomic_rmw_bool_bytes_and(old: u8, val: u8); ++ req (old == 0 || old == 1) &*& (val == 0 || val == 1); ++ ens atomic_rmw_value::(typeid(u8), typeid(u8), RmwAnd, old, val) == (old * val); ++ ++ lem atomic_rmw_bool_bytes_nand(old: u8, val: u8); ++ req (old == 0 || old == 1) &*& (val == 0 || val == 1); ++ ens atomic_rmw_value::(typeid(u8), typeid(u8), RmwNand, old, val) == (255 - old * val); ++ ++ lem atomic_rmw_bool_bytes_or(old: u8, val: u8); ++ req (old == 0 || old == 1) &*& (val == 0 || val == 1); ++ ens atomic_rmw_value::(typeid(u8), typeid(u8), RmwOr, old, val) == (if old == 0 { val } else { 1 }); ++ ++ lem atomic_rmw_bool_bytes_xor(old: u8, val: u8); ++ req (old == 0 || old == 1) &*& (val == 0 || val == 1); ++ ens atomic_rmw_value::(typeid(u8), typeid(u8), RmwXor, old, val) == (if old == val { 0 } else { 1 }); ++ ++ @*/ ++ + unsafe fn atomic_store_relaxed(dst: *mut T, val: T); +- //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; + //@ ens [f]atomic_points_to(dst, 1, inv_); + //@ on_unwind_ens false; +- ++ + unsafe fn atomic_store_release(dst: *mut T, val: T); +- //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; + //@ ens [f]atomic_points_to(dst, 1, inv_); + //@ on_unwind_ens false; +- ++ + unsafe fn atomic_store_seqcst(dst: *mut T, val: T); +- //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; + //@ ens [f]atomic_points_to(dst, 1, inv_); + //@ on_unwind_ens false; +- ++ ++ unsafe fn atomic_load_relaxed(dst: *const T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, ?g, ?inv_); ++ //@ ens [f]atomic_points_to(dst, g, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_load_acquire(dst: *const T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, ?g, ?inv_); ++ //@ ens [f]atomic_points_to(dst, g, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_load_seqcst(dst: *const T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, ?g, ?inv_); ++ //@ ens [f]atomic_points_to(dst, g, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xchg_relaxed(dst: *mut T, val: T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xchg_release(dst: *mut T, val: T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xchg_acquire(dst: *mut T, val: T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xchg_acqrel(dst: *mut T, val: T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xchg_seqcst(dst: *mut T, val: T) -> T; ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_relaxed_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_relaxed_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_relaxed_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_release_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_release_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_release_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acquire_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acquire_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acquire_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acqrel_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acqrel_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_acqrel_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_seqcst_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_seqcst_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchg_seqcst_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_relaxed_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_relaxed_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_relaxed_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_release_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_release_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_release_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acquire_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acquire_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acquire_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acqrel_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acqrel_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_acqrel_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_seqcst_relaxed(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_seqcst_acquire(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_cxchgweak_seqcst_seqcst(dst: *mut T, old: T, val: T) -> (T, bool); ++ //@ req atomic_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result.0) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xadd_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAdd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xadd_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAdd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xadd_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAdd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xadd_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAdd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xadd_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAdd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xsub_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwSub, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xsub_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwSub, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xsub_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwSub, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xsub_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwSub, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xsub_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwSub, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_and_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAnd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_and_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAnd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_and_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAnd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_and_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAnd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_and_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwAnd, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_nand_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwNand, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_nand_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwNand, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_nand_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwNand, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_nand_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwNand, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_nand_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwNand, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_or_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwOr, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_or_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwOr, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_or_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwOr, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_or_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwOr, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_or_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwOr, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xor_relaxed(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwXor, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xor_release(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwXor, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xor_acquire(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwXor, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xor_acqrel(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwXor, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_xor_seqcst(dst: *mut T, val: U) -> T; ++ //@ req atomic_rmw_types::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& [_]is_atomic_rmw_preserves::(?preserves, typeid(T), typeid(U), RmwXor, inv_, val); ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_max_relaxed(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_max_release(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_max_acquire(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_max_acqrel(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_max_seqcst(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_min_relaxed(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_min_release(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_min_acquire(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_min_acqrel(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_min_seqcst(dst: *mut T, val: T) -> T; ++ //@ req atomic_signed_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umax_relaxed(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umax_release(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umax_acquire(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umax_acqrel(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umax_seqcst(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umin_relaxed(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umin_release(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umin_acquire(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umin_acqrel(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ unsafe fn atomic_umin_seqcst(dst: *mut T, val: T) -> T; ++ //@ req atomic_unsigned_type::() == true &*& [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true; ++ //@ ens [f]atomic_points_to(dst, 1, inv_) &*& inv_(result) == true; ++ //@ on_unwind_ens false; ++ ++ // END LOCAL ATOMIC OPERATION MODEL ++ + } + + mod mem {