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 {