support casts of bools to integers

src/cast.rs

@@ -8,7 +8,7 @@ use value::PrimVal;
 
 impl<'a, 'tcx> EvalContext<'a, 'tcx> {
     pub(super) fn cast_primval(
-        &self,
+        &mut self,
         val: PrimVal,
         src_ty: Ty<'tcx>,
         dest_ty: Ty<'tcx>
@@ -28,6 +28,14 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
                     // TODO(optimization): check to see if the cast has made
                     // the value concrete.
                     Ok(PrimVal::Abstract(sbytes))
+                } else if kind == Bool && dest_kind.is_int() {
+                    let dest_kind = self.ty_to_primval_kind(dest_ty)?;
+                    let primval = self.memory.constraints.add_if_then_else(
+                        val,
+                        dest_kind,
+                        PrimVal::Bytes(1),
+                        PrimVal::Bytes(0));
+                    Ok(primval)
                 } else {
                     unimplemented!()
                 }

src/constraints.rs

@@ -11,6 +11,20 @@ enum VarType {
     Array, // Array of BitVec8, indexed by BitVec64?
 }
 
+impl VarType {
+    fn from_prim_val_kind(kind: PrimValKind) -> Self {
+        use value::PrimValKind::*;
+        match kind {
+            Bool => VarType::Bool,
+            U8 | I8 => VarType::BitVec8,
+            U16 | I16 => VarType::BitVec8,
+            U32 | I32 => VarType::BitVec8,
+            U64 | I64 => VarType::BitVec8,
+            _ => unimplemented!(),
+        }
+    }
+}
+
 #[derive(Debug, Clone, Copy)]
 enum VarOrigin {
     StdIn, // abstract byte read from stdin
@@ -47,6 +61,15 @@ pub enum Constraint {
 
     Compare { op: mir::BinOp, kind: PrimValKind, lhs: PrimVal, rhs: PrimVal, },
 
+    // lhs = if discriminant then then_branch else else_branch
+    IfThenElse {
+        discriminant: PrimVal,
+        kind: PrimValKind,
+        then_branch: PrimVal,
+        else_branch: PrimVal,
+        lhs: PrimVal,
+    },
+
     /// array[index] = value
     ArrayElement {
         array: AbstractVariable,
@@ -186,6 +209,33 @@ impl ConstraintContext {
         primval
     }
 
+    pub fn add_if_then_else(
+        &mut self,
+        discriminant: PrimVal,
+        kind: PrimValKind,
+        then_branch: PrimVal,
+        else_branch: PrimVal
+    ) -> PrimVal {
+        let var_type = VarType::from_prim_val_kind(kind);
+
+        let num_bytes = kind.num_bytes();
+        let mut buffer = [SByte::Concrete(0); 8];
+        for idx in 0..num_bytes {
+            buffer[idx] = SByte::Abstract(self.allocate_abstract_var(var_type, VarOrigin::Inner));
+        }
+
+        let lhs = PrimVal::Abstract(buffer);
+        self.push_constraint(Constraint::IfThenElse {
+            discriminant,
+            kind,
+            then_branch,
+            else_branch,
+            lhs,
+        });
+
+        lhs
+    }
+
     pub fn new_array(&mut self) -> AbstractVariable {
         self.allocate_abstract_var(VarType::Array, VarOrigin::Inner)
     }
@@ -395,6 +445,14 @@ impl ConstraintContext {
                 }
             }
 
+            Constraint::IfThenElse { discriminant, kind, then_branch, else_branch, lhs } => {
+                self.primval_to_ast(&ctx, lhs, kind)._eq(
+                    &self.primval_to_ast(&ctx, discriminant, PrimValKind::Bool).ite(
+                        &self.primval_to_ast(&ctx, then_branch, kind),
+                        &self.primval_to_ast(&ctx, else_branch, kind)))
+
+            }
+
             Constraint::ArrayElement { array, index, value, } => {
                 let c = ::z3::Ast::new_const(
                     &::z3::Symbol::from_int(ctx, array.0),

tests/symbolic.rs

@@ -150,3 +150,11 @@ fn symbolic_slice() {
         "tests/symbolic/slice.rs",
         vec![35]);
 }
+
+#[test]
+fn symbolic_cast_bool() {
+    expect_single_panic(
+        "tests/symbolic/bool_cast.rs",
+        vec![18, 102]);
+
+}

tests/symbolic/bool_cast.rs

+fn main() {
+    use std::io::Read;
+    let mut data = [0; 2];
+    let mut stdin = ::std::io::stdin();
+    stdin.read_exact(&mut data[..]).unwrap();
+
+    let b0 = data[0] == 18;
+    if b0 as i8 == 1 {
+        let b1 = data[1] != 102;
+        if b1 as i8 == 0 {
+            panic!()
+        }
+    }
+}