fn get_as_bv_z3_ast()

in checker/src/z3_solver.rs [1770:1890]

• 120 lines of code
• 1 McCabe index (conditional complexity)

    fn get_as_bv_z3_ast(&self, expression: &Expression, num_bits: u32) -> z3_sys::Z3_ast {
        match expression {
            Expression::Add { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvadd)
            }
            Expression::AddOverflows {
                left,
                right,
                result_type,
            } => self.bv_overflows(
                left,
                right,
                *result_type,
                z3_sys::Z3_mk_bvadd_no_overflow,
                z3_sys::Z3_mk_bvadd_no_underflow,
            ),
            Expression::Div { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvsdiv)
            }
            Expression::Mul { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvmul)
            }
            Expression::MulOverflows {
                left,
                right,
                result_type,
            } => self.bv_overflows(
                left,
                right,
                *result_type,
                z3_sys::Z3_mk_bvmul_no_overflow,
                z3_sys::Z3_mk_bvmul_no_underflow,
            ),
            Expression::Rem { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvsrem)
            }
            Expression::Sub { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvsub)
            }
            Expression::SubOverflows {
                left,
                right,
                result_type,
            } => self.bv_overflows(
                left,
                right,
                *result_type,
                z3_sys::Z3_mk_bvsub_no_underflow,
                z3_sys::Z3_mk_bvsub_no_overflow,
            ),
            Expression::And { .. }
            | Expression::Equals { .. }
            | Expression::GreaterOrEqual { .. }
            | Expression::GreaterThan { .. }
            | Expression::LessOrEqual { .. }
            | Expression::LessThan { .. }
            | Expression::LogicalNot { .. }
            | Expression::Ne { .. }
            | Expression::Or { .. } => self.bv_boolean_op(expression, num_bits),
            Expression::BitAnd { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvand)
            }
            Expression::BitNot {
                operand,
                result_type,
            } => self.bv_not(num_bits, operand, *result_type),
            Expression::BitOr { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvor)
            }
            Expression::BitXor { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvxor)
            }
            Expression::Cast {
                target_type,
                operand,
            } => self.bv_cast(&operand.expression, *target_type, num_bits),
            Expression::CompileTimeConstant(const_domain) => {
                self.bv_constant(num_bits, const_domain)
            }
            Expression::ConditionalExpression {
                condition,
                consequent,
                alternate,
            } => self.bv_conditional(num_bits, condition, consequent, alternate),
            Expression::IntrinsicBitVectorUnary { .. } => unsafe {
                //todo: use the name to select an appropriate Z3 bitvector function
                let sym = self.get_symbol_for(expression);
                let sort = z3_sys::Z3_mk_bv_sort(self.z3_context, num_bits);
                z3_sys::Z3_mk_const(self.z3_context, sym, sort)
            },
            Expression::Join { left, right, .. } => self.bv_join(left, right, num_bits),
            Expression::Neg { operand } => self.bv_neg(num_bits, operand),
            Expression::Offset { .. } => unsafe {
                let sym = self.get_symbol_for(expression);
                let sort = z3_sys::Z3_mk_bv_sort(self.z3_context, num_bits);
                z3_sys::Z3_mk_const(self.z3_context, sym, sort)
            },
            Expression::Reference(path) => self.bv_reference(num_bits, path),
            Expression::Shl { left, right } => {
                self.bv_binary(num_bits, left, right, z3_sys::Z3_mk_bvshl)
            }
            Expression::Shr { left, right } => self.bv_shr_by(num_bits, left, right),
            Expression::Top | Expression::Bottom => unsafe {
                let sort = z3_sys::Z3_mk_bv_sort(self.z3_context, num_bits);
                z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, sort)
            },
            Expression::Transmute { .. } => unsafe {
                let sym = self.get_symbol_for(expression);
                let sort = z3_sys::Z3_mk_bv_sort(self.z3_context, num_bits);
                z3_sys::Z3_mk_const(self.z3_context, sym, sort)
            },
            Expression::UninterpretedCall { path, .. }
            | Expression::InitialParameterValue { path, .. }
            | Expression::Variable { path, .. } => self.bv_variable(path, num_bits),
            Expression::WidenedJoin { path, .. } => self.bv_widen(path, num_bits),
            _ => {
                let path = Path::get_as_path(AbstractValue::make_from(expression.clone(), 1));
                self.bv_variable(&path, num_bits)
            }
        }
    }