in checker/src/fixed_point_visitor.rs [242:334]
fn get_initial_state_from_predecessors(
&mut self,
bb: mir::BasicBlock,
iteration_count: usize,
) -> Environment {
let mut predecessor_states_and_conditions: Vec<(Environment, Rc<AbstractValue>)> =
self.bv.mir.predecessors()[bb]
.iter()
.filter_map(|pred_bb| {
// If the predecessor can only be reached via bb then bb and pred_bb are
// part of the loop body.
let is_loop_back = self.dominators.is_dominated_by(*pred_bb, bb);
if iteration_count == 1 && is_loop_back {
// For the first iteration of the loop body we only want state that
// precedes the body. Normally, the state of a block that is part of the
// loop body will still be in the default state in iteration 1
// and thus get ignored.
// If the loop is nested, however, there will be state from the previous
// iteration of the outer loop, so we have to explicitly ignore the state.
return None;
}
if iteration_count > 1 && !is_loop_back {
// Once the loop body has been interpreted in its initial state (iteration 1)
// we only want state from previous iterations of the loop.
return None;
}
let pred_state = &self.out_state[pred_bb];
if let Some(pred_exit_condition) = pred_state.exit_conditions.get(&bb) {
if pred_exit_condition.as_bool_if_known().unwrap_or(true) {
trace!(
"pred {:?} exits on condition {:?} with {:?}",
pred_bb,
pred_exit_condition,
pred_state
);
Some((pred_state.clone(), pred_exit_condition.clone()))
} else {
// If pred_bb is known to have a false exit condition for bb it can be ignored.
None
}
} else if let mir::BasicBlockData {
is_cleanup: true, ..
} = &self.bv.mir[bb]
{
// A clean up block does not execute starting with the normal exit state of
// a predecessor block. If the predecessor ends on a call, the side effects of
// the call should probably be used to havoc parts of the normal state of
// the predecessor. For now, just proceed as if the predecessor block had no
// effect on its initial state.
// todo: perhaps just leave function constants in the initial state.
Some((
self.terminator_state[pred_bb].clone(),
Rc::new(abstract_value::TRUE),
))
} else {
// If pred_state does not have an exit condition map, it is in its default state
// which means it has not yet been visited, or it is code that is known to always
// panic at runtime. Either way, we don't want to include its out state here.
None
}
})
.collect();
if predecessor_states_and_conditions.is_empty() {
// bb is unreachable, at least in this iteration.
// We therefore give it a false entry condition so that the block analyses knows
// the block is unreachable.
let mut initial_state = self.bv.first_environment.clone();
initial_state.entry_condition = Rc::new(abstract_value::FALSE);
return initial_state;
}
if predecessor_states_and_conditions.len() == 1 {
let (mut state, entry_condition) = predecessor_states_and_conditions.remove(0);
state.entry_condition = entry_condition;
state.exit_conditions = HashTrieMap::default();
state
} else {
let entry_condition = predecessor_states_and_conditions
.iter()
.map(|(_, c)| c.clone())
.reduce(|c1, c2| c1.or(c2))
.unwrap();
trace!("entry_condition {:?}", entry_condition);
let mut state = predecessor_states_and_conditions
.into_iter()
.reduce(|(state1, cond1), (state2, cond2)| {
(state2.conditional_join(state1, &cond2, &cond1), cond1)
})
.expect("one or more states to fold into something")
.0;
state.entry_condition = entry_condition;
state
}
}