Skip to content

crucible-mir: Support pointer arguments in atomic_xchg override #1712

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
RyanGlScott wants to merge 1 commit into
base: master
Choose a base branch
from
Open

crucible-mir: Support pointer arguments in atomic_xchg override #1712

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions crucible-mir/CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,8 @@ This release supports [version
values to instead return `MirAggregate` values explicitly. The
`mirAggregate_zst`, `mirAggregate_zstIO`, and `mirAggregate_zstSim` functions
have been introduced to make this process easier.
* Extend the override for the `atomic_xchg` intrinsic to support storing
pointer values in addition to integer values.
Comment on lines +60 to +61
Copy link
Contributor Author

@RyanGlScott RyanGlScott Jan 21, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This changelog entry may need to be moved depending on the timing of the upcoming Crux release.


# 0.5 -- 2025-11-09

Expand Down
78 changes: 61 additions & 17 deletions crucible-mir/src/Mir/TransCustom.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1925,6 +1925,9 @@ atomic_cxchg_impl = \_substs -> Just $ CustomOp $ \opTys ops -> case (opTys, ops
writeMirRef tpr ref new
buildTupleMaybeM [ty, TyBool] $
[Just $ MirExp tpr old, Just $ MirExp C.BoolRepr eq]
-- TODO(#1710): Implement pointer support.
| MirReferenceRepr <- tpr ->
mirFail "atomic_cxchg does not support pointer types"
_ -> mirFail $ "BUG: invalid arguments to atomic_cxchg: " ++ show ops

atomic_fence_impl :: CustomRHS
Expand All @@ -1934,20 +1937,31 @@ atomic_fence_impl = \_substs -> Just $ CustomOp $ \_ ops -> case ops of

-- Common implementation for all atomic read-modify-write operations. These
-- all read the value, apply some operation, write the result back, and return
-- the old value.
-- the old value. This is parameterized by two callback functions. The first is
-- called when the value has an integer type, and the second is called when the
-- value has a pointer type.
atomic_rmw_impl ::
String ->
(forall w h s ret. (1 <= w) =>
C.NatRepr w ->
R.Expr MIR s (C.BVType w) ->
R.Expr MIR s (C.BVType w) ->
MirGenerator h s ret (R.Expr MIR s (C.BVType w))) ->
(forall h s ret.
R.Expr MIR s MirReferenceType ->
R.Expr MIR s MirReferenceType ->
MirGenerator h s ret (R.Expr MIR s MirReferenceType)) ->
CustomRHS
atomic_rmw_impl name rmw = \_substs -> Just $ CustomOp $ \_ ops -> case ops of
atomic_rmw_impl name rmwBv rmwPtr = \_substs -> Just $ CustomOp $ \_ ops -> case ops of
[MirExp MirReferenceRepr ref, MirExp tpr val]
| C.BVRepr w <- tpr -> do
old <- readMirRef tpr ref
new <- rmw w old val
new <- rmwBv w old val
writeMirRef tpr ref new
return $ MirExp tpr old
| MirReferenceRepr <- tpr -> do
old <- readMirRef tpr ref
new <- rmwPtr old val
writeMirRef tpr ref new
return $ MirExp tpr old
_ -> mirFail $ "BUG: invalid arguments to atomic_" ++ name ++ ": " ++ show ops
Expand All @@ -1959,10 +1973,33 @@ makeAtomicRMW ::
R.Expr MIR s (C.BVType w) ->
R.Expr MIR s (C.BVType w) ->
MirGenerator h s ret (R.Expr MIR s (C.BVType w))) ->
(forall h s ret.
R.Expr MIR s MirReferenceType ->
R.Expr MIR s MirReferenceType ->
MirGenerator h s ret (R.Expr MIR s MirReferenceType)) ->
[(ExplodedDefId, CustomRHS)]
makeAtomicRMW name rmw =
makeAtomicRMW name rmwBv rmwPtr =
makeAtomicIntrinsics (Text.pack name) allAtomicOrderings $
atomic_rmw_impl name rmw
atomic_rmw_impl name rmwBv rmwPtr

-- | A specialized version of 'makeAtomicRMW' that always fails if the second
-- argument has a pointer type.
makeAtomicRMWNoPtrs ::
String ->
(forall w h s ret. (1 <= w) =>
C.NatRepr w ->
R.Expr MIR s (C.BVType w) ->
R.Expr MIR s (C.BVType w) ->
MirGenerator h s ret (R.Expr MIR s (C.BVType w))) ->
[(ExplodedDefId, CustomRHS)]
makeAtomicRMWNoPtrs name rmwBv = makeAtomicRMW name rmwBv rmwPtr
where
rmwPtr ::
forall h s ret.
R.Expr MIR s MirReferenceType ->
R.Expr MIR s MirReferenceType ->
MirGenerator h s ret (R.Expr MIR s MirReferenceType)
rmwPtr _ _ = mirFail $ "BUG: atomic_" ++ name ++ " does not support pointer types"

-- These names are taken from
-- https://github.com/rust-lang/rust/blob/22b4c688956de0925f7a10a79cb0e1ca35f55425/library/core/src/sync/atomic.rs#L3039-L3043
Expand All @@ -1978,18 +2015,25 @@ atomic_funcs =
makeAtomicIntrinsics "fence" fenceVariants atomic_fence_impl ++
makeAtomicIntrinsics "singlethreadfence" fenceVariants atomic_fence_impl ++
concat [
makeAtomicRMW "xchg" $ \_w _old val -> return val,
makeAtomicRMW "xadd" $ \w old val -> return $ R.App $ E.BVAdd w old val,
makeAtomicRMW "xsub" $ \w old val -> return $ R.App $ E.BVSub w old val,
makeAtomicRMW "and" $ \w old val -> return $ R.App $ E.BVAnd w old val,
makeAtomicRMW "or" $ \w old val -> return $ R.App $ E.BVOr w old val,
makeAtomicRMW "xor" $ \w old val -> return $ R.App $ E.BVXor w old val,
makeAtomicRMW "nand" $ \w old val ->
return $ R.App $ E.BVNot w $ R.App $ E.BVAnd w old val,
makeAtomicRMW "max" $ \w old val -> return $ R.App $ E.BVSMax w old val,
makeAtomicRMW "min" $ \w old val -> return $ R.App $ E.BVSMin w old val,
makeAtomicRMW "umax" $ \w old val -> return $ R.App $ E.BVUMax w old val,
makeAtomicRMW "umin" $ \w old val -> return $ R.App $ E.BVUMin w old val
-- Intrinsics that only support integer arguments.
makeAtomicRMWNoPtrs "max" $ \w old val -> return $ R.App $ E.BVSMax w old val,
makeAtomicRMWNoPtrs "min" $ \w old val -> return $ R.App $ E.BVSMin w old val,
makeAtomicRMWNoPtrs "umax" $ \w old val -> return $ R.App $ E.BVUMax w old val,
makeAtomicRMWNoPtrs "umin" $ \w old val -> return $ R.App $ E.BVUMin w old val,

-- Intrinsics that support both integer and pointer arguments. Note
-- that we only implement pointer support for a subset of these
-- intrinsics at present.
-- TODO(#1710): Implement pointer support for the remaining ones.
makeAtomicRMW "xchg"
(\_w _old val -> return val) (\_old val -> return val),
makeAtomicRMWNoPtrs "xadd" $ \w old val -> return $ R.App $ E.BVAdd w old val,
makeAtomicRMWNoPtrs "xsub" $ \w old val -> return $ R.App $ E.BVSub w old val,
makeAtomicRMWNoPtrs "and" $ \w old val -> return $ R.App $ E.BVAnd w old val,
makeAtomicRMWNoPtrs "or" $ \w old val -> return $ R.App $ E.BVOr w old val,
makeAtomicRMWNoPtrs "xor" $ \w old val -> return $ R.App $ E.BVXor w old val,
makeAtomicRMWNoPtrs "nand" $ \w old val ->
return $ R.App $ E.BVNot w $ R.App $ E.BVAnd w old val
]
where
-- See https://github.com/rust-lang/rust/blob/22b4c688956de0925f7a10a79cb0e1ca35f55425/library/core/src/sync/atomic.rs#L3008-L3012
Expand Down
21 changes: 21 additions & 0 deletions crux-mir/test/conc_eval/sync/atomic_ptr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
use std::sync::atomic::{AtomicPtr, Ordering};

#[cfg_attr(crux, crux::test)]
fn crux_test() {
let ptr = &mut 5;
let some_ptr = AtomicPtr::new(ptr);
let other_ptr = &mut 10;
let value = some_ptr.swap(other_ptr, Ordering::Relaxed);
let other_value = some_ptr.load(Ordering::Relaxed);
assert_eq!(unsafe { *value }, 5);
assert_eq!(unsafe { *other_value }, 10);

let another_ptr = &mut 15;
some_ptr.store(another_ptr, Ordering::Relaxed);
let another_value = some_ptr.load(Ordering::Relaxed);
assert_eq!(unsafe { *another_value }, 15);
}

pub fn main() {
println!("{:?}", crux_test());
}
Loading