From 4b1b47a2a30d0c8b067059778f3abf16361f2c01 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 25 Jul 2024 11:31:10 -0400 Subject: [PATCH] crucible-llvm: Support atomic operations introduced in LLVM 9+ This adapts `crucible-llvm` to new atomic operations introduced in LLVM 9 and later: * This bumps the `llvm-pretty` submodule to incorporate the changes from https://github.com/GaloisInc/llvm-pretty/pull/138 and https://github.com/GaloisInc/llvm-pretty/pull/140. * This bumps the `llvm-pretty-bc-parser` submodule to incorporate changes from https://github.com/GaloisInc/llvm-pretty-bc-parser/pull/274. * This updates `crucible-llvm`'s semantics for the `atomicrmw` instruction to account for atomic `fadd`, `fsub`, `fmax`, `fmin`, `uinc_wrap`, and `udec_wrap` operations. * This ensures that all atomic operations have a corresponding `crux-llvm` test case. --- crucible-llvm/CHANGELOG.md | 2 + .../Crucible/LLVM/Translation/Instruction.hs | 135 ++++++++++++++++-- .../test-data/golden/atomicrmw-faddsubxchg.ll | 40 ++++++ .../atomicrmw-faddsubxchg.pre-clang9.z3.good | 4 + .../golden/atomicrmw-faddsubxchg.z3.good | 1 + .../test-data/golden/atomicrmw-fmaxmin.ll | 34 +++++ .../atomicrmw-fmaxmin.pre-clang15.z3.good | 4 + .../golden/atomicrmw-fmaxmin.z3.good | 1 + .../test-data/golden/atomicrmw-uincdecwrap.ll | 38 +++++ .../atomicrmw-uincdecwrap.pre-clang16.z3.good | 4 + .../golden/atomicrmw-uincdecwrap.z3.good | 1 + crux-llvm/test-data/golden/atomicrmw.ll | 88 ++++++++++++ crux-llvm/test-data/golden/atomicrmw.z3.good | 1 + crux-llvm/test/Test.hs | 1 + dependencies/llvm-pretty | 2 +- dependencies/llvm-pretty-bc-parser | 2 +- 16 files changed, 344 insertions(+), 14 deletions(-) create mode 100644 crux-llvm/test-data/golden/atomicrmw-faddsubxchg.ll create mode 100644 crux-llvm/test-data/golden/atomicrmw-faddsubxchg.pre-clang9.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw-faddsubxchg.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw-fmaxmin.ll create mode 100644 crux-llvm/test-data/golden/atomicrmw-fmaxmin.pre-clang15.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw-fmaxmin.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw-uincdecwrap.ll create mode 100644 crux-llvm/test-data/golden/atomicrmw-uincdecwrap.pre-clang16.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw-uincdecwrap.z3.good create mode 100644 crux-llvm/test-data/golden/atomicrmw.ll create mode 100644 crux-llvm/test-data/golden/atomicrmw.z3.good diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md index a9f9c3f5e..ac32c6775 100644 --- a/crucible-llvm/CHANGELOG.md +++ b/crucible-llvm/CHANGELOG.md @@ -18,6 +18,8 @@ argument. To retrieve the current symbolic backend, use `Lang.Crucible.Simulator.OverrideSim.ovrWithBackend`. * Add overrides for integer-related `llvm.vector.reduce.*` intrinsics. +* Add support for atomic `fadd`, `fsub`, `fmax`, `fmin`, `uinc_wrap`, and + `udec_wrap` operations in `atomicrmw` instructions. # 0.6 -- 2024-02-05 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs index b1b2ee710..43d0b2c35 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs @@ -1073,6 +1073,7 @@ caseptr w tpr bvCase ptrCase x = continueLambda c_label (branch cond bv_label ptr_label) atomicRWOp :: + forall s arch ret. L.AtomicRWOp -> LLVMExpr s arch -> LLVMExpr s arch -> @@ -1083,25 +1084,132 @@ atomicRWOp op x y = | Just Refl <- testEquality w w' -> do xbv <- pointerAsBitvectorExpr w x' ybv <- pointerAsBitvectorExpr w y' - let newval = case op of - L.AtomicXchg -> ybv - L.AtomicAdd -> app $ BVAdd w xbv ybv - L.AtomicSub -> app $ BVSub w xbv ybv - L.AtomicAnd -> app $ BVAnd w xbv ybv - L.AtomicNand -> app $ BVNot w $ app $ BVAnd w xbv ybv - L.AtomicOr -> app $ BVOr w xbv ybv - L.AtomicXor -> app $ BVXor w xbv ybv - L.AtomicMax -> app $ BVSMax w xbv ybv - L.AtomicMin -> app $ BVSMin w xbv ybv - L.AtomicUMax -> app $ BVUMax w xbv ybv - L.AtomicUMin -> app $ BVUMin w xbv ybv + newval <- bvOp w xbv ybv return $ BaseExpr (LLVMPointerRepr w) $ BitvectorAsPointerExpr w newval + (Scalar _archProxy (FloatRepr fi) xf, Scalar _archPrxy' (FloatRepr fi') yf) + | Just Refl <- testEquality fi fi' + -> do newval <- floatingOp fi xf yf + return $ BaseExpr (FloatRepr fi) newval + _ -> fail $ unlines [ "atomicRW operation on incompatible values" , "Operation: " ++ show op , "Value 1: " ++ show x , "Value 2: " ++ show y ] + where + -- Translate an atomic operation over bitvector values, respecting the + -- semantics described in this part of the LLVM Language Reference Manual: + -- https://releases.llvm.org/16.0.0/docs/LangRef.html#id229 + -- + -- Note that `xbv` corresponds to `*ptr` and `ybv` corresponds to `val` in + -- the Reference Manual. + bvOp :: + forall w. + (1 <= w) => + NatRepr w -> + Expr LLVM s (BVType w) -> + Expr LLVM s (BVType w) -> + LLVMGenerator s arch ret (Expr LLVM s (BVType w)) + bvOp w xbv ybv = + case op of + L.AtomicXchg -> pure ybv + L.AtomicAdd -> pure $ app $ BVAdd w xbv ybv + L.AtomicSub -> pure $ app $ BVSub w xbv ybv + L.AtomicAnd -> pure $ app $ BVAnd w xbv ybv + L.AtomicNand -> pure $ app $ BVNot w $ app $ BVAnd w xbv ybv + L.AtomicOr -> pure $ app $ BVOr w xbv ybv + L.AtomicXor -> pure $ app $ BVXor w xbv ybv + L.AtomicMax -> pure $ app $ BVSMax w xbv ybv + L.AtomicMin -> pure $ app $ BVSMin w xbv ybv + L.AtomicUMax -> pure $ app $ BVUMax w xbv ybv + L.AtomicUMin -> pure $ app $ BVUMin w xbv ybv + L.AtomicUIncWrap -> + -- This is the same thing as + -- + -- (*ptr u>= val) ? 0 : (*ptr + 1) + -- + -- from the LLVM semantics, but with a double-negated condition to + -- account for the Crucible CFG language not having a BVUge operation + -- (only BVUlt). + let c = app $ Not $ app $ BVUlt w xbv ybv -- ~(*ptr u< val) + t = zero + f = app $ BVAdd w xbv one in + pure $ app $ BVIte c w t f + L.AtomicUDecWrap -> + -- This is the same thing as + -- + -- ((*ptr == 0) || (*ptr u> val)) ? val : (*ptr - 1) + -- + -- from the LLVM semantics, but with a double-negated condition to + -- account for the Crucible CFG language not having a BVUgt operation + -- (only BVUle). + let c1 = app $ BVEq w xbv zero + c2 = app $ Not $ app $ BVUle w xbv ybv -- ~(*ptr u<= val) + c = app $ Or c1 c2 + t = xbv + f = app $ BVSub w xbv one in + pure $ app $ BVIte c w t f + + L.AtomicFAdd -> nonBvError + L.AtomicFSub -> nonBvError + L.AtomicFMax -> nonBvError + L.AtomicFMin -> nonBvError + where + zero, one :: Expr LLVM s (BVType w) + zero = app $ BVLit w $ BV.zero w + one = app $ BVLit w $ BV.one w + + nonBvError :: forall a. LLVMGenerator s arch ret a + nonBvError = + reportError $ fromString $ unwords + [ "Invalid atomic bitvector operation" + , "Operation: " ++ show op + , "Value 1: " ++ show xbv + , "Value 2: " ++ show ybv + ] + + -- Translate an atomic operation over floating-point values, respecting the + -- semantics described in this part of the LLVM Language Reference Manual: + -- https://releases.llvm.org/16.0.0/docs/LangRef.html#id229 + -- + -- Note that `xf` corresponds to `*ptr` and `yf` corresponds to `val` in the + -- Reference Manual. + floatingOp :: + forall fi. + FloatInfoRepr fi -> + Expr LLVM s (FloatType fi) -> + Expr LLVM s (FloatType fi) -> + LLVMGenerator s arch ret (Expr LLVM s (FloatType fi)) + floatingOp fi xf yf = + case op of + L.AtomicXchg -> pure yf + L.AtomicFAdd -> pure $ app $ FloatAdd fi RNE xf yf + L.AtomicFSub -> pure $ app $ FloatSub fi RNE xf yf + L.AtomicFMax -> pure $ app $ FloatMax fi xf yf + L.AtomicFMin -> pure $ app $ FloatMin fi xf yf + + L.AtomicAdd -> nonFloatingError + L.AtomicSub -> nonFloatingError + L.AtomicAnd -> nonFloatingError + L.AtomicNand -> nonFloatingError + L.AtomicOr -> nonFloatingError + L.AtomicXor -> nonFloatingError + L.AtomicMax -> nonFloatingError + L.AtomicMin -> nonFloatingError + L.AtomicUMax -> nonFloatingError + L.AtomicUMin -> nonFloatingError + L.AtomicUIncWrap -> nonFloatingError + L.AtomicUDecWrap -> nonFloatingError + where + nonFloatingError :: forall a. LLVMGenerator s arch ret a + nonFloatingError = + reportError $ fromString $ unwords + [ "Invalid atomic floating-point operation" + , "Operation: " ++ show op + , "Value 1: " ++ show xf + , "Value 2: " ++ show yf + ] floatingCompare :: L.FCmpOp -> @@ -1713,6 +1821,9 @@ generateInstr retType lab defSet instr assign_f k = ptr' <- transTypedValue ptr case valTy of IntType _ -> pure () + FloatType -> pure () + DoubleType -> pure () + X86_FP80Type -> pure () _ -> fail $ unwords ["Invalid argument type on atomicrw, expected integer type", show ptr] llvmTypeAsRepr valTy $ \expectTy -> diff --git a/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.ll b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.ll new file mode 100644 index 000000000..78a8a9919 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.ll @@ -0,0 +1,40 @@ +@.str = private unnamed_addr constant [8 x i8] c"atomics\00" + +declare void @crucible_assert(i8 noundef zeroext, i8* noundef, i32 noundef) + +define float @atomic_fadd(float* %ptr, float %val) { + %old = atomicrmw fadd float* %ptr, float %val acquire + ret float %old +} + +define float @atomic_fsub(float* %ptr, float %val) { + %old = atomicrmw fsub float* %ptr, float %val acquire + ret float %old +} + +define float @atomic_xchg(float* %ptr, float %val) { + %old = atomicrmw xchg float* %ptr, float %val acquire + ret float %old +} + +define void @test_atomic_float_op(float (float*, float)* %atomic_op, float %expected_old, float %val, float %expected_new) { + %ptr = alloca float + store float %expected_old, float* %ptr + %actual_old = call float %atomic_op(float* %ptr, float %val) + %actual_new = load float, float* %ptr + %cmp_old = fcmp oeq float %expected_old, %actual_old + %cmp_new = fcmp oeq float %expected_new, %actual_new + %cmp_old_zext = zext i1 %cmp_old to i8 + %cmp_new_zext = zext i1 %cmp_new to i8 + %str_cast = bitcast [8 x i8]* @.str to i8* + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + ret void +} + +define i32 @main() { + call void @test_atomic_float_op(float (float*, float)* @atomic_fadd, float 2.5, float 3.0, float 5.5) + call void @test_atomic_float_op(float (float*, float)* @atomic_fsub, float 3.5, float 2.0, float 1.5) + call void @test_atomic_float_op(float (float*, float)* @atomic_xchg, float 2.5, float 3.0, float 3.0) + ret i32 0 +} diff --git a/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.pre-clang9.z3.good b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.pre-clang9.z3.good new file mode 100644 index 000000000..9ab1c2db6 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.pre-clang9.z3.good @@ -0,0 +1,4 @@ +SKIP_TEST + +This test case requires the use of atomic `fadd` and `fsub` operations, which +are only available in LLVM 9 or later. diff --git a/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.z3.good b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.z3.good new file mode 100644 index 000000000..9c7ea10d9 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-faddsubxchg.z3.good @@ -0,0 +1 @@ +[Crux] Overall status: Valid. diff --git a/crux-llvm/test-data/golden/atomicrmw-fmaxmin.ll b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.ll new file mode 100644 index 000000000..5caf9e0ef --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.ll @@ -0,0 +1,34 @@ +@.str = private unnamed_addr constant [8 x i8] c"atomics\00" + +declare void @crucible_assert(i8 noundef zeroext, i8* noundef, i32 noundef) + +define float @atomic_fmax(float* %ptr, float %val) { + %old = atomicrmw fmax float* %ptr, float %val acquire + ret float %old +} + +define float @atomic_fmin(float* %ptr, float %val) { + %old = atomicrmw fmin float* %ptr, float %val acquire + ret float %old +} + +define void @test_atomic_float_op(float (float*, float)* %atomic_op, float %expected_old, float %val, float %expected_new) { + %ptr = alloca float + store float %expected_old, float* %ptr + %actual_old = call float %atomic_op(float* %ptr, float %val) + %actual_new = load float, float* %ptr + %cmp_old = fcmp oeq float %expected_old, %actual_old + %cmp_new = fcmp oeq float %expected_new, %actual_new + %cmp_old_zext = zext i1 %cmp_old to i8 + %cmp_new_zext = zext i1 %cmp_new to i8 + %str_cast = bitcast [8 x i8]* @.str to i8* + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + ret void +} + +define i32 @main() { + call void @test_atomic_float_op(float (float*, float)* @atomic_fmax, float 2.5, float 3.0, float 3.0) + call void @test_atomic_float_op(float (float*, float)* @atomic_fmin, float 2.5, float 3.0, float 2.5) + ret i32 0 +} diff --git a/crux-llvm/test-data/golden/atomicrmw-fmaxmin.pre-clang15.z3.good b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.pre-clang15.z3.good new file mode 100644 index 000000000..0e5416722 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.pre-clang15.z3.good @@ -0,0 +1,4 @@ +SKIP_TEST + +This test case requires the use of atomic `fmax` and `fmin` operations, which +are only available in LLVM 15 or later. diff --git a/crux-llvm/test-data/golden/atomicrmw-fmaxmin.z3.good b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.z3.good new file mode 100644 index 000000000..9c7ea10d9 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-fmaxmin.z3.good @@ -0,0 +1 @@ +[Crux] Overall status: Valid. diff --git a/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.ll b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.ll new file mode 100644 index 000000000..fb44695ee --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.ll @@ -0,0 +1,38 @@ +@.str = private unnamed_addr constant [8 x i8] c"atomics\00" + +declare void @crucible_assert(i8 noundef zeroext, i8* noundef, i32 noundef) + +define i32 @atomic_uinc_wrap(i32* %ptr, i32 %val) { + %old = atomicrmw uinc_wrap i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_udec_wrap(i32* %ptr, i32 %val) { + %old = atomicrmw udec_wrap i32* %ptr, i32 %val acquire + ret i32 %old +} + +define void @test_atomic_i32_op(i32 (i32*, i32)* %atomic_op, i32 %expected_old, i32 %val, i32 %expected_new) { + %ptr = alloca i32 + store i32 %expected_old, i32* %ptr + %actual_old = call i32 %atomic_op(i32* %ptr, i32 %val) + %actual_new = load i32, i32* %ptr + %cmp_old = icmp eq i32 %expected_old, %actual_old + %cmp_new = icmp eq i32 %expected_new, %actual_new + %cmp_old_zext = zext i1 %cmp_old to i8 + %cmp_new_zext = zext i1 %cmp_new to i8 + %str_cast = bitcast [8 x i8]* @.str to i8* + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + ret void +} + +define i32 @main() { + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_uinc_wrap, i32 0, i32 0, i32 0) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_uinc_wrap, i32 3, i32 2, i32 0) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_uinc_wrap, i32 2, i32 3, i32 3) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_udec_wrap, i32 0, i32 0, i32 0) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_udec_wrap, i32 3, i32 2, i32 2) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_udec_wrap, i32 2, i32 3, i32 1) + ret i32 0 +} diff --git a/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.pre-clang16.z3.good b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.pre-clang16.z3.good new file mode 100644 index 000000000..c5a3508de --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.pre-clang16.z3.good @@ -0,0 +1,4 @@ +SKIP_TEST + +This test case requires the use of atomic `uinc_wrap` and `udec_wrap` +operations, which are only available in LLVM 16 or later. diff --git a/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.z3.good b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.z3.good new file mode 100644 index 000000000..9c7ea10d9 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw-uincdecwrap.z3.good @@ -0,0 +1 @@ +[Crux] Overall status: Valid. diff --git a/crux-llvm/test-data/golden/atomicrmw.ll b/crux-llvm/test-data/golden/atomicrmw.ll new file mode 100644 index 000000000..f89be0ad0 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw.ll @@ -0,0 +1,88 @@ +@.str = private unnamed_addr constant [8 x i8] c"atomics\00" + +declare void @crucible_assert(i8 noundef zeroext, i8* noundef, i32 noundef) + +define i32 @atomic_xchg(i32* %ptr, i32 %val) { + %old = atomicrmw xchg i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_add(i32* %ptr, i32 %val) { + %old = atomicrmw add i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_sub(i32* %ptr, i32 %val) { + %old = atomicrmw sub i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_and(i32* %ptr, i32 %val) { + %old = atomicrmw and i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_nand(i32* %ptr, i32 %val) { + %old = atomicrmw nand i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_or(i32* %ptr, i32 %val) { + %old = atomicrmw or i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_xor(i32* %ptr, i32 %val) { + %old = atomicrmw xor i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_max(i32* %ptr, i32 %val) { + %old = atomicrmw max i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_min(i32* %ptr, i32 %val) { + %old = atomicrmw min i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_umax(i32* %ptr, i32 %val) { + %old = atomicrmw umax i32* %ptr, i32 %val acquire + ret i32 %old +} + +define i32 @atomic_umin(i32* %ptr, i32 %val) { + %old = atomicrmw umin i32* %ptr, i32 %val acquire + ret i32 %old +} + +define void @test_atomic_i32_op(i32 (i32*, i32)* %atomic_op, i32 %expected_old, i32 %val, i32 %expected_new) { + %ptr = alloca i32 + store i32 %expected_old, i32* %ptr + %actual_old = call i32 %atomic_op(i32* %ptr, i32 %val) + %actual_new = load i32, i32* %ptr + %cmp_old = icmp eq i32 %expected_old, %actual_old + %cmp_new = icmp eq i32 %expected_new, %actual_new + %cmp_old_zext = zext i1 %cmp_old to i8 + %cmp_new_zext = zext i1 %cmp_new to i8 + %str_cast = bitcast [8 x i8]* @.str to i8* + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + call void @crucible_assert(i8 noundef zeroext %cmp_old_zext, i8* noundef %str_cast, i32 noundef 0) + ret void +} + +define i32 @main() { + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_xchg, i32 2, i32 3, i32 3) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_add, i32 2, i32 3, i32 5) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_sub, i32 3, i32 2, i32 1) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_and, i32 2, i32 3, i32 2) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_nand, i32 2, i32 3, i32 4294967293) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_or, i32 2, i32 3, i32 3) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_xor, i32 2, i32 3, i32 1) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_max, i32 4294967293, i32 3, i32 3) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_min, i32 4294967293, i32 3, i32 4294967293) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_umax, i32 2, i32 3, i32 3) + call void @test_atomic_i32_op(i32 (i32*, i32)* @atomic_umin, i32 2, i32 3, i32 2) + ret i32 0 +} diff --git a/crux-llvm/test-data/golden/atomicrmw.z3.good b/crux-llvm/test-data/golden/atomicrmw.z3.good new file mode 100644 index 000000000..9c7ea10d9 --- /dev/null +++ b/crux-llvm/test-data/golden/atomicrmw.z3.good @@ -0,0 +1 @@ +[Crux] Overall status: Valid. diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs index 325ebe513..9f4b56ee2 100644 --- a/crux-llvm/test/Test.hs +++ b/crux-llvm/test/Test.hs @@ -43,6 +43,7 @@ cube = TS.mkCUBE { TS.inputDirs = ["test-data/golden"] , TS.validParams = [ ("solver", Just ["z3", "cvc5"]) , ("loop-merging", Just ["loopmerge", "loop"]) , ("clang-range", Just [ "recent-clang" + , "pre-clang9" , "pre-clang11" , "pre-clang12" , "pre-clang13" diff --git a/dependencies/llvm-pretty b/dependencies/llvm-pretty index 780e7c01c..725bd01c4 160000 --- a/dependencies/llvm-pretty +++ b/dependencies/llvm-pretty @@ -1 +1 @@ -Subproject commit 780e7c01cbd0b85172f11ea8edf0d7bbe6a84967 +Subproject commit 725bd01c4be76538cf9606696b780415d901c040 diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser index 395754789..0f789a1fb 160000 --- a/dependencies/llvm-pretty-bc-parser +++ b/dependencies/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 395754789b2f1b1f3ffae22383f9522a3e44d68e +Subproject commit 0f789a1fb5150363e573dbe602e0dcd8bbf9f23c