in checker/src/abstract_value.rs [6283:6582]
fn refine_with(&self, path_condition: &Self, depth: usize) -> Rc<AbstractValue> {
if self.is_bottom() || self.is_top() {
return self.clone();
};
//do not use false path conditions to refine things
checked_precondition!(path_condition.as_bool_if_known().is_none());
if depth >= k_limits::MAX_REFINE_DEPTH {
trace!("max refine depth exceeded during refine_with");
return self.clone();
}
// In this context path_condition is true
if path_condition.eq(self) {
return Rc::new(TRUE);
}
// If the path context constrains the self expression to be equal to a constant, just
// return the constant.
if let Expression::Equals { left, right } = &path_condition.expression {
if let Expression::CompileTimeConstant(..) = &left.expression {
if self.eq(right) {
return left.clone();
}
}
if let Expression::CompileTimeConstant(..) = &right.expression {
if self.eq(left) {
return right.clone();
}
}
}
// Traverse the self expression, looking for recursive refinement opportunities.
// Important, keep the traversal as trivial as possible and put optimizations in
// the transfer functions. Also, keep the transfer functions constant in cost as
// much as possible. Any time they are not, this function becomes quadratic and
// performance becomes terrible.
match &self.expression {
Expression::Bottom | Expression::Top => self.clone(),
Expression::Add { left, right } => left
.refine_with(path_condition, depth + 1)
.addition(right.refine_with(path_condition, depth + 1)),
Expression::AddOverflows {
left,
right,
result_type,
} => left
.refine_with(path_condition, depth + 1)
.add_overflows(right.refine_with(path_condition, depth + 1), *result_type),
Expression::And { left, right } => left
.refine_with(path_condition, depth + 1)
.and(right.refine_with(path_condition, depth + 1)),
Expression::BitAnd { left, right } => left
.refine_with(path_condition, depth + 1)
.bit_and(right.refine_with(path_condition, depth + 1)),
Expression::BitNot {
operand,
result_type,
} => operand
.refine_with(path_condition, depth + 1)
.bit_not(*result_type),
Expression::BitOr { left, right } => left
.refine_with(path_condition, depth + 1)
.bit_or(right.refine_with(path_condition, depth + 1)),
Expression::BitXor { left, right } => left
.refine_with(path_condition, depth + 1)
.bit_xor(right.refine_with(path_condition, depth + 1)),
Expression::Cast {
operand,
target_type,
} => operand
.refine_with(path_condition, depth + 1)
.cast(*target_type),
Expression::CompileTimeConstant(..) => self.clone(),
Expression::ConditionalExpression {
condition,
consequent,
alternate,
} => {
// The implies checks should be redundant, but currently help with precision
// presumably because they are not k-limited like the refinement of the path
// condition. They might also help with performance because they avoid
// two refinements and the expensive and constructor, if they succeed.
// If they mostly fail, they will cost more than they save. It is not
// clear at this point if they are a win, but they are kept for the sake of precision.
if path_condition.implies(condition) {
consequent.refine_with(path_condition, depth + 1)
} else if path_condition.implies_not(condition) {
alternate.refine_with(path_condition, depth + 1)
} else {
let refined_condition = condition.refine_with(path_condition, depth + 1);
let refined_condition_as_bool = refined_condition.as_bool_if_known();
let refined_consequent = consequent.refine_with(path_condition, depth + 1);
if refined_condition_as_bool.unwrap_or(false) {
return refined_consequent;
}
let refined_alternate = alternate.refine_with(path_condition, depth + 1);
if !refined_condition_as_bool.unwrap_or(true) {
return refined_alternate;
}
refined_condition.conditional_expression(refined_consequent, refined_alternate)
}
}
Expression::Div { left, right } => left
.refine_with(path_condition, depth + 1)
.divide(right.refine_with(path_condition, depth + 1)),
Expression::Equals { left, right } => left
.refine_with(path_condition, depth + 1)
.equals(right.refine_with(path_condition, depth + 1)),
Expression::GreaterOrEqual { left, right } => left
.refine_with(path_condition, depth + 1)
.greater_or_equal(right.refine_with(path_condition, depth + 1)),
Expression::GreaterThan { left, right } => left
.refine_with(path_condition, depth + 1)
.greater_than(right.refine_with(path_condition, depth + 1)),
Expression::IntrinsicBinary { left, right, name } => left
.refine_with(path_condition, depth + 1)
.intrinsic_binary(right.refine_with(path_condition, depth + 1), *name),
Expression::IntrinsicBitVectorUnary {
operand,
bit_length,
name,
} => operand
.refine_with(path_condition, depth + 1)
.intrinsic_bit_vector_unary(*bit_length, *name),
Expression::HeapBlock { .. } => self.clone(),
Expression::HeapBlockLayout {
length,
alignment,
source,
} => AbstractValue::make_from(
Expression::HeapBlockLayout {
length: length.refine_with(path_condition, depth + 1),
alignment: alignment.refine_with(path_condition, depth + 1),
source: *source,
},
1,
),
Expression::IntrinsicFloatingPointUnary { operand, name } => operand
.refine_with(path_condition, depth + 1)
.intrinsic_floating_point_unary(*name),
Expression::Join { left, right } => left
.refine_with(path_condition, depth + 1)
.join(right.refine_with(path_condition, depth + 1)),
Expression::LessOrEqual { left, right } => left
.refine_with(path_condition, depth + 1)
.less_or_equal(right.refine_with(path_condition, depth + 1)),
Expression::LessThan { left, right } => left
.refine_with(path_condition, depth + 1)
.less_than(right.refine_with(path_condition, depth + 1)),
Expression::Memcmp {
left,
right,
length,
} => {
let refined_length = length.refine_with(path_condition, depth + 1);
AbstractValue::make_memcmp(left.clone(), right.clone(), refined_length)
}
Expression::Mul { left, right } => left
.refine_with(path_condition, depth + 1)
.multiply(right.refine_with(path_condition, depth + 1)),
Expression::MulOverflows {
left,
right,
result_type,
} => left
.refine_with(path_condition, depth + 1)
.mul_overflows(right.refine_with(path_condition, depth + 1), *result_type),
Expression::Ne { left, right } => left
.refine_with(path_condition, depth + 1)
.not_equals(right.refine_with(path_condition, depth + 1)),
Expression::Neg { operand } => operand.refine_with(path_condition, depth + 1).negate(),
Expression::LogicalNot { operand } => {
operand.refine_with(path_condition, depth + 1).logical_not()
}
Expression::Offset { left, right } => left
.refine_with(path_condition, depth + 1)
.offset(right.refine_with(path_condition, depth + 1)),
Expression::Or { left, right } => {
// Ideally the constructor should do the simplifications, but in practice or
// expressions grow quite large due to composition and it really helps to avoid
// refining the right expression whenever possible, even at the expense of
// more checks here. If the performance of implies and implies_not should become
// significantly worse than it is now, this could become a performance bottle neck.
if path_condition.implies(left) || path_condition.implies(right) {
Rc::new(TRUE)
} else if path_condition.implies_not(left) {
if path_condition.implies_not(right) {
Rc::new(FALSE)
} else {
right.refine_with(path_condition, depth + 1)
}
} else if path_condition.implies_not(right) {
left.refine_with(path_condition, depth + 1)
} else {
left.refine_with(path_condition, depth + 1)
.or(right.refine_with(path_condition, depth + 1))
}
}
Expression::Reference(..) | Expression::InitialParameterValue { .. } => {
// We could refine their paths, which will increase precision, but it does not
// currently seem cost-effective. This does not affect soundness.
self.clone()
}
Expression::Rem { left, right } => left
.refine_with(path_condition, depth + 1)
.remainder(right.refine_with(path_condition, depth + 1)),
Expression::Shl { left, right } => left
.refine_with(path_condition, depth + 1)
.shift_left(right.refine_with(path_condition, depth + 1)),
Expression::ShlOverflows {
left,
right,
result_type,
} => left
.refine_with(path_condition, depth + 1)
.shl_overflows(right.refine_with(path_condition, depth + 1), *result_type),
Expression::Shr { left, right } => left
.refine_with(path_condition, depth + 1)
.shr(right.refine_with(path_condition, depth + 1)),
Expression::ShrOverflows {
left,
right,
result_type,
} => left
.refine_with(path_condition, depth + 1)
.shr_overflows(right.refine_with(path_condition, depth + 1), *result_type),
Expression::Sub { left, right } => left
.refine_with(path_condition, depth + 1)
.subtract(right.refine_with(path_condition, depth + 1)),
Expression::SubOverflows {
left,
right,
result_type,
} => left
.refine_with(path_condition, depth + 1)
.sub_overflows(right.refine_with(path_condition, depth + 1), *result_type),
Expression::Switch {
discriminator,
cases,
default,
} => discriminator.refine_with(path_condition, depth + 1).switch(
cases
.iter()
.map(|(case_val, result_val)| {
(
case_val.refine_with(path_condition, depth + 1),
result_val.refine_with(path_condition, depth + 1),
)
})
.collect(),
default.refine_with(path_condition, depth + 1),
),
Expression::TaggedExpression { operand, tag } => {
operand.refine_with(path_condition, depth + 1).add_tag(*tag)
}
Expression::Transmute {
operand,
target_type,
} => operand
.refine_with(path_condition, depth + 1)
.transmute(*target_type),
Expression::UninterpretedCall {
callee,
arguments,
result_type,
path,
} => callee
.refine_with(path_condition, depth + 1)
.uninterpreted_call(
arguments
.iter()
.map(|v| v.refine_with(path_condition, depth + 1))
.collect(),
*result_type,
path.clone(),
),
Expression::UnknownModelField { .. } => self.clone(),
Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
} => AbstractValue::make_tag_check(
operand.refine_with(path_condition, depth + 1),
*tag,
*checking_presence,
),
Expression::UnknownTagField { .. } => self.clone(),
Expression::Variable { var_type, .. } => {
if *var_type == ExpressionType::Bool {
if path_condition.implies(self) {
return Rc::new(TRUE);
} else if path_condition.implies_not(self) {
return Rc::new(FALSE);
}
}
self.clone()
}
Expression::WidenedJoin { path, operand } => {
operand.refine_with(path_condition, depth + 1).widen(path)
}
}
}