in checker/src/abstract_value.rs [5805:6265]
fn refine_parameters_and_paths(
&self,
args: &[(Rc<Path>, Rc<AbstractValue>)],
result: &Option<Rc<Path>>,
pre_env: &Environment,
post_env: &Environment,
// An offset to add to locals from the called function so that they do not clash with caller locals.
fresh: usize,
) -> Rc<AbstractValue> {
match &self.expression {
Expression::Bottom | Expression::Top => self.clone(),
Expression::Add { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.addition(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::AddOverflows {
left,
right,
result_type,
} => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.add_overflows(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*result_type,
),
Expression::And { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.and(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::BitAnd { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.bit_and(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::BitNot {
operand,
result_type,
} => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.bit_not(*result_type),
Expression::BitOr { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.bit_or(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::BitXor { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.bit_xor(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::Cast {
operand,
target_type,
} => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.cast(*target_type),
Expression::CompileTimeConstant(..) => self.clone(),
Expression::ConditionalExpression {
condition,
consequent,
alternate,
} => {
let mut cond =
condition.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if let Some(c) = cond.as_bool_if_known() {
if c {
consequent
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
} else {
alternate
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
}
} else {
if condition.expression.contains_local_variable(false) {
// The condition contains local state of the callee and could not be
// satisfied by refining other parts of the condition with call site state.
if let Some(promotable_condition) = cond.extract_promotable_disjuncts(false)
{
// The overall condition can be satisfied by our caller
// so simplify the condition to just that part.
cond = promotable_condition;
} else {
// The condition can not be satisfied without knowing the callee state
// so just join (and thus avoid keeping around a potentially large useless expression).
return consequent
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.join(alternate.refine_parameters_and_paths(
args, result, pre_env, post_env, fresh,
));
}
}
cond.conditional_expression(
consequent
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
alternate
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
)
}
}
Expression::Div { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.divide(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::Equals { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.equals(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::GreaterOrEqual { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.greater_or_equal(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::GreaterThan { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.greater_than(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::HeapBlock {
abstract_address,
is_zeroed,
} => AbstractValue::make_from(
Expression::HeapBlock {
abstract_address: *abstract_address + fresh,
is_zeroed: *is_zeroed,
},
1,
),
Expression::HeapBlockLayout {
length,
alignment,
source,
} => AbstractValue::make_from(
Expression::HeapBlockLayout {
length: length
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
alignment: alignment
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
source: *source,
},
1,
),
Expression::InitialParameterValue { path, var_type } => {
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, pre_env, fresh);
if let PathEnum::Computed { value } | PathEnum::Offset { value } =
&refined_path.value
{
return value.clone();
} else if let Some(val) = pre_env.value_at(&refined_path) {
return val.clone();
}
// If the path does not have a known value in the pre environment, make an unknown
// value. If the path is still rooted in parameter make sure that it does not get
// affected by subsequent side effects on the parameter.
if refined_path.is_rooted_by_parameter() {
// This will not get refined again
AbstractValue::make_initial_parameter_value(*var_type, refined_path)
} else {
// The value is rooted in a local variable leaked from the callee or
// in a static. In the latter case we want lookup_and_refine_value to
// to see this. In the former, refinement is a no-op.
AbstractValue::make_typed_unknown(*var_type, refined_path)
}
}
Expression::IntrinsicBinary { left, right, name } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.intrinsic_binary(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*name,
),
Expression::IntrinsicBitVectorUnary {
operand,
bit_length,
name,
} => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.intrinsic_bit_vector_unary(*bit_length, *name),
Expression::IntrinsicFloatingPointUnary { operand, name } => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.intrinsic_floating_point_unary(*name),
Expression::Join { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.join(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::LessOrEqual { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.less_or_equal(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::LessThan { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.less_than(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::LogicalNot { operand } => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.logical_not(),
Expression::Memcmp {
left,
right,
length,
} => {
let refined_left =
left.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
let refined_right =
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
let refined_length =
length.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if let Expression::CompileTimeConstant(ConstantDomain::U128(len)) =
&refined_length.expression
{
let n = *len as usize;
let arr1 = refined_left.try_resolve_as_byte_array(post_env);
let arr2 = refined_right.try_resolve_as_byte_array(post_env);
if let (Some(arr1), Some(arr2)) = (&arr1, &arr2) {
let n1 = usize::min(n, arr1.len());
let n2 = usize::min(n, arr2.len());
return Rc::new(
ConstantDomain::I128(arr1[..n1].cmp(&arr2[..n2]) as i32 as i128).into(),
);
}
let str1 = refined_left.try_resolve_as_ref_to_str(post_env);
let str2 = refined_right.try_resolve_as_ref_to_str(post_env);
if let (Some(str1), Some(str2)) = (str1, str2) {
let n1 = usize::min(n, str1.len());
let n2 = usize::min(n, str2.len());
return Rc::new(
ConstantDomain::I128(str1[..n1].cmp(&str2[..n2]) as i32 as i128).into(),
);
}
}
AbstractValue::make_memcmp(refined_left, refined_right, refined_length)
}
Expression::Mul { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.multiply(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::MulOverflows {
left,
right,
result_type,
} => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.mul_overflows(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*result_type,
),
Expression::Ne { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.not_equals(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::Neg { operand } => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.negate(),
Expression::Offset { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.offset(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::Or { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.or(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::Reference(path) => {
// if the path is a parameter, the reference is an artifact of its type
// and needs to be removed in the call context
match &path.value {
PathEnum::Parameter { ordinal } => {
if *ordinal > args.len() {
warn!("Summary refers to a parameter that does not have a matching argument");
Rc::new(BOTTOM)
} else {
args[*ordinal - 1].1.clone()
}
}
_ => {
let refined_path = path
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
AbstractValue::make_reference(refined_path)
}
}
}
Expression::Rem { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.remainder(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::Shl { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.shift_left(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::ShlOverflows {
left,
right,
result_type,
} => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.shl_overflows(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*result_type,
),
Expression::Shr { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.shr(right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)),
Expression::ShrOverflows {
left,
right,
result_type,
} => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.shr_overflows(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*result_type,
),
Expression::Sub { left, right } => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.subtract(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::SubOverflows {
left,
right,
result_type,
} => left
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.sub_overflows(
right.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*result_type,
),
Expression::Switch {
discriminator,
cases,
default,
} => discriminator
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.switch(
cases
.iter()
.map(|(case_val, result_val)| {
(
case_val.refine_parameters_and_paths(
args, result, pre_env, post_env, fresh,
),
result_val.refine_parameters_and_paths(
args, result, pre_env, post_env, fresh,
),
)
})
.collect(),
default.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
),
Expression::TaggedExpression { operand, tag } => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.add_tag(*tag),
Expression::Transmute {
operand,
target_type,
} => operand
.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
.transmute(*target_type),
Expression::UninterpretedCall {
callee,
arguments,
result_type,
path,
} => {
let refined_callee =
callee.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
let refined_arguments = arguments
.iter()
.map(|arg| {
arg.refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
})
.collect();
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
refined_callee.uninterpreted_call(refined_arguments, *result_type, refined_path)
}
Expression::UnknownModelField { path, default } => {
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if !matches!(&refined_path.value, PathEnum::Computed { .. }) {
if let Some(val) = post_env.value_at(&refined_path) {
// This environment has a value for the model field.
val.clone()
} else if refined_path.is_rooted_by_parameter() {
// Keep passing the buck to the next caller.
AbstractValue::make_from(
Expression::UnknownModelField {
path: refined_path,
default: default.clone(),
},
default.expression_size.saturating_add(1),
)
} else {
// The buck stops here and the environment does not have a value for model field.
default.clone()
}
} else {
AbstractValue::make_from(
Expression::UnknownModelField {
path: refined_path,
default: default.clone(),
},
1,
)
}
}
Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
} => AbstractValue::make_tag_check(
operand.refine_parameters_and_paths(args, result, pre_env, post_env, fresh),
*tag,
*checking_presence,
),
Expression::UnknownTagField { path } => {
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if !matches!(&refined_path.value, PathEnum::Computed { .. }) {
if let Some(val) = post_env.value_at(&refined_path) {
// This environment has a value for the tag field.
val.clone()
} else if !refined_path.is_rooted_by_parameter() {
// Return the dummy untagged value if refined_path is not rooted by a function parameter.
Rc::new(DUMMY_UNTAGGED_VALUE)
} else {
// Otherwise, return again an unknown tag field.
AbstractValue::make_from(
Expression::UnknownTagField { path: refined_path },
1,
)
}
} else {
AbstractValue::make_from(Expression::UnknownTagField { path: refined_path }, 1)
}
}
Expression::Variable { path, var_type } => {
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if let PathEnum::Computed { value }
| PathEnum::HeapBlock { value }
| PathEnum::Offset { value } = &refined_path.value
{
value.clone()
} else if let Some(val) = post_env.value_at(&refined_path) {
val.clone()
} else if refined_path.eq(path) {
self.clone()
} else {
AbstractValue::make_typed_unknown(*var_type, refined_path)
}
}
Expression::WidenedJoin { path, operand } => {
let refined_path =
path.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
let refined_operand =
operand.refine_parameters_and_paths(args, result, pre_env, post_env, fresh);
if matches!(refined_operand.expression, Expression::Join { .. }) {
refined_operand.widen(&refined_path)
} else {
AbstractValue::make_typed_unknown(operand.expression.infer_type(), refined_path)
}
}
}
}