Properly handle zero-element arrays in global variables

Fixes #9.

Cargo.toml

@@ -12,7 +12,7 @@ license = "MIT"
 
 [dependencies]
 llvm-ir = "0.6.0"
-boolector = "0.4.0"
+boolector = "0.4.1"
 either = "1.5.3"
 itertools = "0.9.0"
 reduce = "0.1"

src/state.rs

@@ -957,8 +957,15 @@ where
                                     name, &initializer
                                 );
                                 initialized.set(true);
-                                let write_val = self.const_to_bv(initializer)?;
-                                self.write_without_mut(addr, write_val)?;
+                                // Global variables could be zero-element arrays, or structs
+                                // containing zero-element arrays, so we use
+                                // `const_to_bv_maybe_zerowidth()`
+                                if let Some(bv) = self.const_to_bv_maybe_zerowidth(initializer)? {
+                                    // If that returned `None`, the global is a zero-element array,
+                                    // in which case we don't want to initialize it (and can't, or
+                                    // we'd get a panic about a 0-width BV)
+                                    self.write_without_mut(addr, bv)?;
+                                }
                             }
                             Ok(addr.clone())
                         },
@@ -1134,6 +1141,34 @@ where
         }
     }
 
+    /// Convert a `Constant` to the appropriate `BV`, allowing for the `Constant`
+    /// to possibly be zero-width (LLVM 0-element array is the only way for that
+    /// to happen) or be a struct with zero-width elements (i.e., struct with one
+    /// or more elements being a 0-element array).
+    ///
+    /// Returns `Ok(None)` if the result would be a zero-width `BV`.
+    fn const_to_bv_maybe_zerowidth(&self, c: &Constant) -> Result<Option<B::BV>> {
+        match c {
+            Constant::Null(ty) | Constant::AggregateZero(ty) | Constant::Undef(ty) => {
+                match self.size(ty) {
+                    0 => Ok(None),
+                    bits => Ok(Some(self.zero(bits))),
+                }
+            },
+            Constant::Struct { values, .. } => {
+                values
+                    .iter()
+                    .filter(|v| self.size(&v.get_type()) > 0)
+                    .map(|v| self.const_to_bv_maybe_zerowidth(v).transpose().unwrap()) // since we `filter()`'d first, we should have all `Some`s here. We transpose-unwrap Result<Option<BV>> to Result<BV>
+                    .reduce(|a, b| Ok(b?.concat(&a?))) // the lambda has type Fn(Result<B::BV>, Result<B::BV>) -> Result<B::BV>
+                    .transpose()
+            },
+            Constant::Array { elements, .. } if elements.is_empty() => Ok(None),
+            // note that Constant::Vector cannot have 0 elements, per LLVM LangRef
+            _ => self.const_to_bv(c).map(|bv| Some(bv)),
+        }
+    }
+
     /// Given a `Constant::Struct` and a series of `ExtractValue` indices, get the
     /// final `Constant` referred to
     fn simplify_const_ev(

tests/basic_tests.rs

@@ -26,6 +26,12 @@ fn get_issue_4_32bit_project() -> Project {
         .unwrap_or_else(|e| panic!("Failed to parse module {:?}: {}", modname, e))
 }
 
+fn get_issue_9_project() -> Project {
+    let modname = "tests/bcfiles/issue_9.bc";
+    Project::from_bc_path(&Path::new(modname))
+        .unwrap_or_else(|e| panic!("Failed to parse module {:?}: {}", modname, e))
+}
+
 #[test]
 fn no_args_nozero() {
     let funcname = "no_args_nozero";
@@ -318,3 +324,22 @@ fn issue_4_32bit() {
         PossibleSolutions::exactly_two(ReturnValue::Return(2), ReturnValue::Abort)
     );
 }
+
+#[test]
+fn issue_9() {
+    let funcname = "issue_9::Foo::ez3";
+    init_logging();
+    let proj = get_issue_9_project();
+    let ret = get_possible_return_values_of_func(
+        funcname,
+        vec![Some(1)],
+        &proj,
+        Config::default(),
+        None,
+        10,
+    );
+    assert_eq!(
+        ret,
+        PossibleSolutions::exactly_two(ReturnValue::Return(1), ReturnValue::Abort)
+    );
+}

tests/bcfiles/Makefile

@@ -8,6 +8,7 @@ RUST32BIT=--target i686-unknown-linux-gnu
 .PHONY: all
 all: basic.bc basic.ll \
 			issue_4.bc issue_4.ll \
+			issue_9.bc issue_9.ll \
 			memory.bc memory.ll \
 			loop.bc loop.ll \
 			struct.bc struct.ll \