in checker/src/z3_solver.rs [214:362]
fn get_as_z3_ast(&self, expression: &Expression) -> z3_sys::Z3_ast {
match expression {
Expression::HeapBlock { .. } => {
let path = Path::get_as_path(AbstractValue::make_from(expression.clone(), 1));
self.general_variable(&path, expression.infer_type())
}
Expression::Add { .. }
| Expression::AddOverflows { .. }
| Expression::Div { .. }
| Expression::IntrinsicBinary { .. }
| Expression::IntrinsicFloatingPointUnary { .. }
| Expression::Mul { .. }
| Expression::MulOverflows { .. }
| Expression::Rem { .. }
| Expression::Sub { .. }
| Expression::SubOverflows { .. } => self.get_as_numeric_z3_ast(expression).1,
Expression::And { left, right } => {
self.general_boolean_op(left, right, z3_sys::Z3_mk_and)
}
Expression::BitAnd { left, right } => {
if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) = left.expression {
if v < u128::MAX && (v + 1).is_power_of_two() {
let p2: Rc<AbstractValue> = Rc::new((v + 1).into());
return self.numeric_rem(right, &p2).1;
}
}
self.get_as_bv_z3_ast(expression, 128)
}
Expression::BitOr { .. } | Expression::BitXor { .. } => {
self.get_as_bv_z3_ast(expression, 128)
}
Expression::BitNot { result_type, .. } => {
self.get_as_bv_z3_ast(expression, u32::from(result_type.bit_length()))
}
Expression::Cast {
operand,
target_type,
} => self.general_cast(operand, *target_type),
Expression::CompileTimeConstant(const_domain) => self.get_constant_as_ast(const_domain),
Expression::ConditionalExpression {
condition,
consequent,
alternate,
} => self.general_conditional(condition, consequent, alternate),
Expression::Equals { left, right } => self.general_relational(
left,
right,
z3_sys::Z3_mk_fpa_eq,
z3_sys::Z3_mk_eq,
z3_sys::Z3_mk_eq,
z3_sys::Z3_mk_eq,
),
Expression::GreaterOrEqual { left, right } => self.general_relational(
left,
right,
z3_sys::Z3_mk_fpa_geq,
z3_sys::Z3_mk_ge,
z3_sys::Z3_mk_bvsge,
z3_sys::Z3_mk_bvuge,
),
Expression::GreaterThan { left, right } => self.general_relational(
left,
right,
z3_sys::Z3_mk_fpa_gt,
z3_sys::Z3_mk_gt,
z3_sys::Z3_mk_bvsgt,
z3_sys::Z3_mk_bvugt,
),
Expression::InitialParameterValue { path, .. }
| Expression::UninterpretedCall { path, .. }
| Expression::UnknownModelField { path, .. }
| Expression::UnknownTagField { path }
| Expression::Variable { path, .. } => {
self.general_variable(path, expression.infer_type())
}
Expression::IntrinsicBitVectorUnary { bit_length, .. } => {
self.get_as_bv_z3_ast(expression, u32::from(*bit_length))
}
Expression::LessOrEqual { left, right } => self.general_relational(
left,
right,
z3_sys::Z3_mk_fpa_leq,
z3_sys::Z3_mk_le,
z3_sys::Z3_mk_bvsle,
z3_sys::Z3_mk_bvule,
),
Expression::LessThan { left, right } => self.general_relational(
left,
right,
z3_sys::Z3_mk_fpa_lt,
z3_sys::Z3_mk_lt,
z3_sys::Z3_mk_bvslt,
z3_sys::Z3_mk_bvult,
),
Expression::LogicalNot { operand } => self.general_logical_not(operand),
Expression::Ne { left, right } => self.general_ne(left, right),
Expression::Neg { operand } => self.general_negation(operand),
Expression::Offset { .. } => unsafe {
let sort = self.get_sort_for(expression.infer_type());
let sym = self.get_symbol_for(expression);
z3_sys::Z3_mk_const(self.z3_context, sym, sort)
},
Expression::Or { left, right } => {
self.general_boolean_op(left, right, z3_sys::Z3_mk_or)
}
Expression::Reference(path) => self.general_reference(path),
Expression::Shl { left, right } => {
self.bv_binary(128, left, right, z3_sys::Z3_mk_bvshl)
}
Expression::Shr { left, right } => self.general_shr(left, right),
Expression::ShlOverflows {
right, result_type, ..
}
| Expression::ShrOverflows {
right, result_type, ..
} => self.general_shift_overflows(right, *result_type),
Expression::Switch {
discriminator,
cases,
default,
} => self.general_switch(discriminator, cases, default, |e| self.get_as_z3_ast(e)),
Expression::TaggedExpression { operand, .. } => self.get_as_z3_ast(&operand.expression),
Expression::Top | Expression::Bottom => unsafe {
z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, self.any_sort)
},
Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
} => {
let check_ast = self.general_has_tag(&operand.expression, tag);
if *checking_presence {
check_ast
} else {
unsafe { z3_sys::Z3_mk_not(self.z3_context, check_ast) }
}
}
Expression::WidenedJoin { path, operand } => {
self.get_ast_for_widened(path, operand, operand.expression.infer_type())
}
Expression::Join { left, right, .. } => self.general_join(left, right),
_ => unsafe {
debug!("uninterpreted expression: {:?}", expression);
let sym = self.get_symbol_for(expression);
let sort = self.get_sort_for(expression.infer_type());
z3_sys::Z3_mk_const(self.z3_context, sym, sort)
},
}
}