in checker/src/z3_solver.rs [1004:1160]
fn get_as_numeric_z3_ast(&self, expression: &Expression) -> (bool, z3_sys::Z3_ast) {
match expression {
Expression::HeapBlock { .. } => {
let path = Path::get_as_path(AbstractValue::make_from(expression.clone(), 1));
self.numeric_variable(&path, expression.infer_type())
}
Expression::Add { left, right } => {
self.numeric_binary_var_arg(left, right, z3_sys::Z3_mk_fpa_add, z3_sys::Z3_mk_add)
}
Expression::AddOverflows {
left,
right,
result_type,
} => self.numeric_binary_overflow_vararg(left, right, *result_type, z3_sys::Z3_mk_add),
Expression::Div { left, right } => {
self.numeric_binary(left, right, z3_sys::Z3_mk_fpa_div, z3_sys::Z3_mk_div)
}
Expression::Join { left, right, .. } => self.numeric_join(left, right),
Expression::Mul { left, right } => {
self.numeric_binary_var_arg(left, right, z3_sys::Z3_mk_fpa_mul, z3_sys::Z3_mk_mul)
}
Expression::MulOverflows {
left,
right,
result_type,
} => self.numeric_binary_overflow_vararg(left, right, *result_type, z3_sys::Z3_mk_mul),
Expression::Rem { left, right } => self.numeric_rem(left, right),
Expression::Sub { left, right } => {
self.numeric_binary_var_arg(left, right, z3_sys::Z3_mk_fpa_sub, z3_sys::Z3_mk_sub)
}
Expression::SubOverflows {
left,
right,
result_type,
} => self.numeric_binary_overflow_vararg(left, right, *result_type, z3_sys::Z3_mk_sub),
Expression::And { .. }
| Expression::Equals { .. }
| Expression::GreaterOrEqual { .. }
| Expression::GreaterThan { .. }
| Expression::LessOrEqual { .. }
| Expression::LessThan { .. }
| Expression::LogicalNot { .. }
| Expression::Ne { .. }
| Expression::Or { .. } => self.numeric_boolean_op(expression),
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);
}
}
self.numeric_bitwise_expression(expression)
}
Expression::BitOr { .. } | Expression::BitXor { .. } => {
self.numeric_bitwise_expression(expression)
}
Expression::BitNot {
operand,
result_type,
} => self.numeric_bitwise_not(operand, *result_type),
Expression::Cast {
operand,
target_type,
} => self.numeric_cast(&operand.expression, *target_type),
Expression::CompileTimeConstant(const_domain) => {
self.numeric_const(expression, const_domain)
}
Expression::ConditionalExpression {
condition,
consequent,
alternate,
} => self.numeric_conditional(condition, consequent, alternate),
Expression::IntrinsicBinary { .. } => unsafe {
let expresssion_type = expression.infer_type();
let sym = self.get_symbol_for(expression);
let sort = self.get_sort_for(expresssion_type);
//todo: use the name to select an appropriate Z3 function
(
expresssion_type.is_floating_point_number(),
z3_sys::Z3_mk_const(self.z3_context, sym, sort),
)
},
Expression::InitialParameterValue { path, .. }
| Expression::UninterpretedCall { path, .. }
| Expression::UnknownModelField { path, .. }
| Expression::UnknownTagField { path }
| Expression::Variable { path, .. } => {
self.numeric_variable(path, expression.infer_type())
}
Expression::IntrinsicBitVectorUnary { .. } => unsafe {
//todo: use the name to select an appropriate Z3 bitvector function
let sym = self.get_symbol_for(expression);
(
false,
z3_sys::Z3_mk_const(self.z3_context, sym, self.int_sort),
)
},
Expression::IntrinsicFloatingPointUnary { .. } => unsafe {
//todo: use the name to select an appropriate Z3 floating point function
let sym = self.get_symbol_for(expression);
let sort = self.get_sort_for(expression.infer_type());
(true, z3_sys::Z3_mk_const(self.z3_context, sym, sort))
},
Expression::Neg { operand } => self.numeric_neg(operand),
Expression::Offset { .. } => unsafe {
use self::ExpressionType::*;
let expr_type = expression.infer_type();
let expr_type = match expr_type {
Bool | ThinPointer | NonPrimitive => ExpressionType::I128,
t => t,
};
let is_float = expr_type.is_floating_point_number();
let sym = self.get_symbol_for(expression);
let sort = self.get_sort_for(expr_type);
(is_float, z3_sys::Z3_mk_const(self.z3_context, sym, sort))
},
Expression::Reference(path) => self.numeric_reference(path),
Expression::Shl { left, right } => self.numeric_shl(left, right),
Expression::Shr { left, right, .. } => self.numeric_shr(left, right),
Expression::Switch {
discriminator,
cases,
default,
} => (
default.expression.infer_type().is_floating_point_number(),
self.general_switch(discriminator, cases, default, |e| {
self.get_as_numeric_z3_ast(e).1
}),
),
Expression::TaggedExpression { operand, .. } => {
self.get_as_numeric_z3_ast(&operand.expression)
}
Expression::Transmute { target_type, .. } => unsafe {
let sym = self.get_symbol_for(expression);
let sort = self.get_sort_for(*target_type);
(
target_type.is_floating_point_number(),
z3_sys::Z3_mk_const(self.z3_context, sym, sort),
)
},
Expression::Top | Expression::Bottom => unsafe {
(
false,
z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, self.int_sort),
)
},
Expression::WidenedJoin { path, operand } => self.numeric_widen(path, operand),
_ => unsafe {
debug!("uninterpreted expression: {:?}", expression);
let sym = self.get_symbol_for(expression);
(
false,
z3_sys::Z3_mk_const(self.z3_context, sym, self.int_sort),
)
},
}
}