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

@@ -276,6 +276,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(()),
@@ -2358,6 +2362,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,69 @@
+#![cfg(not(feature = "llvm-9"))] // With LLVM 9 and earlier, Haybale doesn't support AtomicRMW
+
+use haybale::backend::DefaultBackend;
+use haybale::solver_utils::PossibleSolutions;
+use haybale::*;
+use llvm_ir::Name;
+
+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,
+        &proj,
+        Config::default(),
+        Some(vec![
+            ParameterVal::ExactValue(0xFF00),
+            ParameterVal::ExactValue(0x00FF),
+        ]),
+        None,
+        10,
+    );
+    assert_eq!(
+        ret,
+        PossibleSolutions::exactly_one(ReturnValue::Return(0xFF00))
+    );
+
+    let mut em = symex_function(
+        &funcname,
+        &proj,
+        Config::<DefaultBackend>::default(),
+        Some(vec![
+            ParameterVal::ExactValue(0xFF00),
+            ParameterVal::Range(1, 3),
+        ]),
+    ).unwrap();
+    let _ = em
+        .next()
+        .unwrap()
+        .map_err(|e| em.state().full_error_message_with_context(e))
+        .unwrap();
+    let var0 = em.state().get_bv_by_irname(&funcname, &Name::from(0));
+    let var1 = em.state().get_bv_by_irname(&funcname, &Name::from(1));
+    let var3 = em.state().get_bv_by_irname(&funcname, &Name::from(3));
+    let var4 = em.state().get_bv_by_irname(&funcname, &Name::from(4));
+    let var5 = em.state().get_bv_by_irname(&funcname, &Name::from(5));
+    let var6 = em.state().get_bv_by_irname(&funcname, &Name::from(6));
+    let var7 = em.state().get_bv_by_irname(&funcname, &Name::from(7));
+    let var8 = em.state().get_bv_by_irname(&funcname, &Name::from(8));
+    assert!(em.state().bvs_must_be_equal(var3, var0).unwrap());
+    assert!(em.state().bvs_must_be_equal(var4, var1).unwrap());
+    assert!(em.state().bvs_must_be_equal(var5, &var0.add(var1)).unwrap());
+    assert!(em.state().bvs_must_be_equal(var6, var0).unwrap());
+    assert!(em.state().bvs_must_be_equal(var7, &em.state().zero(var7.get_width())).unwrap()); // given the values we provided for %0 and %1, %7 must always be 0
+    let sol8 = em.state().get_possible_solutions_for_bv(var8, 6).unwrap().as_u64_solutions().unwrap();
+    assert_eq!(sol8, PossibleSolutions::exactly_one(3));
+}