crucible-llvm: Support atomic operations introduced in LLVM 9+ (#1226)

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 GaloisInc/llvm-pretty#138 and GaloisInc/llvm-pretty#140. * This bumps the `llvm-pretty-bc-parser` submodule to incorporate changes from GaloisInc/llvm-pretty-bc-parser#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.
GaloisInc · Jul 26, 2024 · b8ff9be · b8ff9be
1 parent 8cc5e17
commit b8ff9be
Show file tree

Hide file tree

Showing 16 changed files with 344 additions and 14 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.