support atomicrmw instructions (with LLVM 10)

Fixes #12.

README.md

@@ -272,9 +272,11 @@ or of course you can generate local documentation with `cargo doc --open`.
 Currently, the official crates.io releases of `haybale` (`0.6.x` series)
 depend on Boolector 3.2.1 and either LLVM 9 or 10, depending on whether you
 select the `llvm-9` or `llvm-10` feature.
-As of this writing, choosing `llvm-9` vs `llvm-10` has no effect on
-`haybale`'s features or interface; the only difference is the ability to
-analyze bitcode generated with LLVM 10.
+As of this writing, choosing `llvm-9` vs `llvm-10` has essentially no effect
+on `haybale`'s features or interface; the only difference is the ability to
+analyze bitcode generated with LLVM 10. (And the LLVM 10 version can process
+`AtomicRMW` instructions; see
+[#12](https://github.com/PLSysSec/haybale/issues/12).)
 
 LLVM 8 is supported on the `llvm-8` branch of this repo. This version is
 approximately at feature parity with `haybale` 0.2.1, and will likely be

src/symex.rs

@@ -226,6 +226,10 @@ where
                     Instruction::Phi(phi) => self.symex_phi(phi),
                     Instruction::Select(select) => self.symex_select(select),
                     Instruction::CmpXchg(cmpxchg) => self.symex_cmpxchg(cmpxchg),
+                    #[cfg(feature = "llvm-9")]
+                    Instruction::AtomicRMW(_) => return Err(Error::UnsupportedInstruction("LLVM `AtomicRMW` instruction is not supported for the LLVM 9 version of Haybale; see Haybale issue #12".into())),
+                    #[cfg(feature = "llvm-10")]
+                    Instruction::AtomicRMW(armw) => self.symex_atomicrmw(armw),
                     Instruction::Call(call) => match self.symex_call(call) {
                         Err(e) => Err(e),
                         Ok(None) => Ok(()),
@@ -2308,6 +2312,41 @@ where
         self.state
             .record_bv_result(cmpxchg, match_flag.concat(&read_value))
     }
+
+    #[cfg(feature = "llvm-10")]
+    fn symex_atomicrmw(&mut self, armw: &'p instruction::AtomicRMW) -> Result<()> {
+        debug!("Symexing atomicrmw {:?}", armw);
+        use llvm_ir::instruction::RMWBinOp;
+        let op_size = self
+            .state
+            .size_in_bits(&self.state.type_of(armw))
+            .ok_or_else(|| {
+                Error::MalformedInstruction("AtomicRMW result is an opaque struct type".into())
+            })?;
+        let addr = self.state.operand_to_bv(&armw.address)?;
+        let val = self.state.operand_to_bv(&armw.value)?;
+        let read_val = self.state.read(&addr, op_size)?;
+        let modified_val = match armw.operation {
+            RMWBinOp::Xchg => val,
+            RMWBinOp::Add => read_val.add(&val),
+            RMWBinOp::Sub => read_val.sub(&val),
+            RMWBinOp::And => read_val.and(&val),
+            RMWBinOp::Nand => read_val.and(&val).not(),
+            RMWBinOp::Or => read_val.or(&val),
+            RMWBinOp::Xor => read_val.xor(&val),
+            RMWBinOp::Max => read_val.sgt(&val).cond_bv(&read_val, &val),
+            RMWBinOp::Min => read_val.slt(&val).cond_bv(&read_val, &val),
+            RMWBinOp::UMax => read_val.ugt(&val).cond_bv(&read_val, &val),
+            RMWBinOp::UMin => read_val.ult(&val).cond_bv(&read_val, &val),
+            RMWBinOp::FAdd | RMWBinOp::FSub => {
+                return Err(Error::UnsupportedInstruction(
+                    "Floating-point operation in an AtomicRMW".into(),
+                ))
+            },
+        };
+        self.state.write(&addr, modified_val)?;
+        self.state.record_bv_result(armw, read_val)
+    }
 }
 
 // Is the given `Constant` a `GlobalReference`

tests/bcfiles/Makefile

@@ -4,6 +4,7 @@ CFLAGS=-O3
 RUSTC=rustc
 RUSTFLAGS=--crate-type=lib
 RUST32BIT=--target i686-unknown-linux-gnu
+LLVMAS=$$LLVM9PATH/bin/llvm-as
 
 .PHONY: all
 all: basic.bc basic.ll \
@@ -26,6 +27,7 @@ all: basic.bc basic.ll \
 			throwcatch.bc throwcatch.ll \
 			abort.bc abort.ll \
 			panic.bc panic.ll \
+			atomicrmw.bc atomicrmw.ll \
 			32bit/issue_4.bc 32bit/issue_4.ll \
 
 %.ll : %.c
@@ -76,8 +78,12 @@ linkedlist.ll : linkedlist.c
 linkedlist.bc : linkedlist.c
 	$(CC) -O0 -c -emit-llvm $^ -o $@
 
+# atomicrmw.ll is a .ll file written by hand, so we need to compile the .bc from the .ll
+atomicrmw.bc : atomicrmw.ll
+	$(LLVMAS) $< -o $@
+
 .PHONY: clean
 clean:
-	find . -name "*.ll" | xargs rm
+	find . -name "*.ll" | grep -v "atomicrmw.ll" | xargs rm
 	find . -name "*.bc" | xargs rm
 	find . -name "*~" | xargs rm

tests/bcfiles/atomicrmw.ll

@@ -0,0 +1,32 @@
+source_filename = "<no source file>"
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-apple-macosx10.15.0"
+
+define i32 @atomicrmwops(i32, i32) local_unnamed_addr {
+  %addr = alloca i32, align 4
+
+  ; initial value at %addr is %0
+  store i32 %0, i32* %addr, align 4
+
+  %3 = atomicrmw xchg i32* %addr, i32 %1 monotonic
+  ; now %3 is %0 and the value is %1
+
+  %4 = atomicrmw add i32* %addr, i32 %3 acquire
+  ; now %4 is %1 and the value is %1 + %3 (so, %1 + %0)
+
+  %5 = atomicrmw sub i32* %addr, i32 %1 release
+  ; now %5 is %1 + %0 and the value is %0
+
+  %6 = atomicrmw and i32* %addr, i32 %4 acq_rel
+  ; now %6 is %0 and the value is %0 & %1
+
+  %7 = atomicrmw xor i32* %addr, i32 3 seq_cst
+  ; now %7 is %0 & %1 and the value is (%0 & %1) ^ 3
+
+  %8 = atomicrmw umax i32* %addr, i32 %0 monotonic
+  ; now %8 is (%0 & %1) ^ 3 and the value is umax(%8, %0)
+
+  %9 = load i32, i32* %addr, align 4
+
+  ret i32 %9
+}

tests/rmw_tests.rs

@@ -0,0 +1,34 @@
+#![cfg(not(feature = "llvm-9"))] // With LLVM 9 and earlier, Haybale doesn't support AtomicRMW
+
+use haybale::solver_utils::PossibleSolutions;
+use haybale::*;
+
+fn init_logging() {
+    // capture log messages with test harness
+    let _ = env_logger::builder().is_test(true).try_init();
+}
+
+fn get_project() -> Project {
+    let modname = "tests/bcfiles/atomicrmw.bc";
+    Project::from_bc_path(modname)
+        .unwrap_or_else(|e| panic!("Failed to parse module {:?}: {}", modname, e))
+}
+
+#[test]
+fn atomicrmw() {
+    init_logging();
+    let proj = get_project();
+    let funcname: String = "atomicrmwops".into();
+    let ret = get_possible_return_values_of_func(
+        &funcname,
+        vec![Some(0xFF00), Some(0x00FF)],
+        &proj,
+        Config::default(),
+        None,
+        10,
+    );
+    assert_eq!(
+        ret,
+        PossibleSolutions::exactly_one(ReturnValue::Return(0xFF00))
+    );
+}