Skip to content

Commit

Permalink
Clarify code for joining with bottom.
Browse files Browse the repository at this point in the history
  • Loading branch information
Herman Venter committed May 8, 2020
1 parent b4d0888 commit d11feab
Show file tree
Hide file tree
Showing 5 changed files with 142 additions and 112 deletions.
36 changes: 25 additions & 11 deletions checker/src/abstract_value.rs
View file
Expand Up @@ -6,7 +6,7 @@
#![allow(clippy::declare_interior_mutable_const)]
use crate::constant_domain::ConstantDomain;
use crate::environment::Environment;
use crate::expression::Expression::{ConditionalExpression, Join, Widen};
use crate::expression::Expression::{ConditionalExpression, Join};
use crate::expression::{Expression, ExpressionType, LayoutSource};
use crate::interval_domain::{self, IntervalDomain};
use crate::k_limits;
Expand Down Expand Up @@ -170,6 +170,12 @@ impl AbstractValue {
result_type: ExpressionType,
operation: fn(Rc<AbstractValue>, Rc<AbstractValue>, ExpressionType) -> Expression,
) -> Rc<AbstractValue> {
if left.is_top() || left.is_bottom() {
return left;
}
if right.is_top() || right.is_bottom() {
return right;
}
let expression_size = left.expression_size.saturating_add(right.expression_size);
Self::make_from(operation(left, right, result_type), expression_size)
}
Expand All @@ -181,6 +187,9 @@ impl AbstractValue {
result_type: ExpressionType,
operation: fn(Rc<AbstractValue>, ExpressionType) -> Expression,
) -> Rc<AbstractValue> {
if operand.is_top() || operand.is_bottom() {
return operand;
}
let expression_size = operand.expression_size.saturating_add(1);
Self::make_from(operation(operand, result_type), expression_size)
}
Expand All @@ -191,6 +200,9 @@ impl AbstractValue {
operand: Rc<AbstractValue>,
operation: fn(Rc<AbstractValue>) -> Expression,
) -> Rc<AbstractValue> {
if operand.is_top() || operand.is_bottom() {
return operand;
}
let expression_size = operand.expression_size.saturating_add(1);
Self::make_from(operation(operand), expression_size)
}
Expand Down Expand Up @@ -458,6 +470,13 @@ impl AbstractValueTrait for Rc<AbstractValue> {
/// Returns an element that is "self && other".
#[logfn_inputs(TRACE)]
fn and(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
// Do these tests here lest BOTTOM get simplified away.
if self.is_bottom() {
return self.clone();
}
if other.is_bottom() {
return other;
}
let self_bool = self.as_bool_if_known();
if let Some(false) = self_bool {
// [false && other] -> false
Expand All @@ -476,13 +495,9 @@ impl AbstractValueTrait for Rc<AbstractValue> {
// [true && other] -> other
other
}
} else if other_bool.unwrap_or(false) || self.is_bottom() {
} else if other_bool.unwrap_or(false) {
// [self && true] -> self
// [BOTTOM && other] -> BOTTOM
self.clone()
} else if other.is_bottom() {
// [self && BOTTOM] -> BOTTOM
other
} else {
match &self.expression {
Expression::And { left: x, right: y } => {
Expand Down Expand Up @@ -2326,11 +2341,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
if let Join { left, right, path } = &other.expression {
return recursive_op(self, left.clone()).join(recursive_op(self, right.clone()), &path);
}
match (&self.expression, &other.expression) {
(Widen { .. }, _) => self.clone(),
(_, Widen { .. }) => other,
_ => operation(self.clone(), other),
}
operation(self.clone(), other)
}

/// Gets or constructs an interval that is cached.
Expand Down Expand Up @@ -2894,6 +2905,9 @@ impl AbstractValueTrait for Rc<AbstractValue> {
/// of refine_paths, which ensures that paths stay unique (dealing with aliasing is expensive).
#[logfn_inputs(TRACE)]
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 {
Expand Down
161 changes: 84 additions & 77 deletions checker/src/block_visitor.rs
View file
Expand Up @@ -709,6 +709,9 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
is_post_condition: bool,
) -> Option<String> {
precondition!(self.bv.check_for_errors);
if cond.is_bottom() {
return None;
}
let (cond_as_bool, entry_cond_as_bool) = self.check_condition_value_and_reachability(cond);

// If we never get here, rather call unreachable!()
Expand Down Expand Up @@ -797,11 +800,13 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
} else {
cond_val.clone()
});
self.bv.current_environment.exit_conditions = self
.bv
.current_environment
.exit_conditions
.insert(cleanup_target, panic_exit_condition);
if !panic_exit_condition.is_bottom() {
self.bv.current_environment.exit_conditions = self
.bv
.current_environment
.exit_conditions
.insert(cleanup_target, panic_exit_condition);
}
};
let normal_exit_condition = self
.bv
Expand All @@ -812,88 +817,90 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
} else {
not_cond_val
});
self.bv.current_environment.exit_conditions = self
.bv
.current_environment
.exit_conditions
.insert(target, normal_exit_condition);
if !normal_exit_condition.is_bottom() {
self.bv.current_environment.exit_conditions = self
.bv
.current_environment
.exit_conditions
.insert(target, normal_exit_condition);

// Check the condition and issue a warning or infer a precondition.
if self.bv.check_for_errors {
if let mir::Operand::Constant(..) = cond {
// Do not complain about compile time constants known to the compiler.
// Leave that to the compiler.
} else {
let (cond_as_bool_opt, entry_cond_as_bool) =
self.check_condition_value_and_reachability(&cond_val);
// Check the condition and issue a warning or infer a precondition.
if self.bv.check_for_errors {
if let mir::Operand::Constant(..) = cond {
// Do not complain about compile time constants known to the compiler.
// Leave that to the compiler.
} else {
let (cond_as_bool_opt, entry_cond_as_bool) =
self.check_condition_value_and_reachability(&cond_val);

// Quick exit if things are known.
if let Some(false) = entry_cond_as_bool {
// We can't reach this assertion, so just return.
return;
}
if let Some(cond_as_bool) = cond_as_bool_opt {
if expected == cond_as_bool {
// If the condition is always as expected when we get here, so there is nothing to report.
// Quick exit if things are known.
if let Some(false) = entry_cond_as_bool {
// We can't reach this assertion, so just return.
return;
}
// The condition is known to differ from expected so if we always get here if called,
// emit a diagnostic.
if entry_cond_as_bool.unwrap_or(false) {
let error = get_assert_msg_description(msg);
if let Some(cond_as_bool) = cond_as_bool_opt {
if expected == cond_as_bool {
// If the condition is always as expected when we get here, so there is nothing to report.
return;
}
// The condition is known to differ from expected so if we always get here if called,
// emit a diagnostic.
if entry_cond_as_bool.unwrap_or(false) {
let error = get_assert_msg_description(msg);
let span = self.bv.current_span;
let error = self.bv.cv.session.struct_span_warn(span, error);
self.bv.emit_diagnostic(error);
// No need to push a precondition, the caller can never satisfy it.
return;
}
}

// At this point, we don't know that this assert is unreachable and we don't know
// that the condition is as expected, so we need to warn about it somewhere.
if self.bv.function_being_analyzed_is_root()
|| self.bv.preconditions.len() >= k_limits::MAX_INFERRED_PRECONDITIONS
{
// Can't make this the caller's problem.
let warning = format!("possible {}", get_assert_msg_description(msg));
let span = self.bv.current_span;
let error = self.bv.cv.session.struct_span_warn(span, error);
self.bv.emit_diagnostic(error);
// No need to push a precondition, the caller can never satisfy it.
let warning = self.bv.cv.session.struct_span_warn(span, warning.as_str());
self.bv.emit_diagnostic(warning);
return;
}
}

// At this point, we don't know that this assert is unreachable and we don't know
// that the condition is as expected, so we need to warn about it somewhere.
if self.bv.function_being_analyzed_is_root()
|| self.bv.preconditions.len() >= k_limits::MAX_INFERRED_PRECONDITIONS
{
// Can't make this the caller's problem.
let warning = format!("possible {}", get_assert_msg_description(msg));
let span = self.bv.current_span;
let warning = self.bv.cv.session.struct_span_warn(span, warning.as_str());
self.bv.emit_diagnostic(warning);
return;
}

// Make it the caller's problem by pushing a precondition.
// After, of course, removing any promoted preconditions that match the current
// source span.
let sp = self.bv.current_span;
self.bv
.preconditions
.retain(|pc| pc.spans.last() != Some(&sp));
if self.bv.preconditions.len() < k_limits::MAX_INFERRED_PRECONDITIONS {
let expected_cond = if expected {
cond_val
} else {
cond_val.logical_not()
};
// To make sure that this assertion never fails, we should either never
// get here (!entry_condition) or expected_cond should be true.
let condition = self
.bv
.current_environment
.entry_condition
.logical_not()
.or(expected_cond);
let message = Rc::new(String::from(get_assert_msg_description(msg)));
let precondition = Precondition {
condition,
message,
provenance: None,
spans: vec![self.bv.current_span],
};
self.bv.preconditions.push(precondition);
// Make it the caller's problem by pushing a precondition.
// After, of course, removing any promoted preconditions that match the current
// source span.
let sp = self.bv.current_span;
self.bv
.preconditions
.retain(|pc| pc.spans.last() != Some(&sp));
if self.bv.preconditions.len() < k_limits::MAX_INFERRED_PRECONDITIONS {
let expected_cond = if expected {
cond_val
} else {
cond_val.logical_not()
};
// To make sure that this assertion never fails, we should either never
// get here (!entry_condition) or expected_cond should be true.
let condition = self
.bv
.current_environment
.entry_condition
.logical_not()
.or(expected_cond);
let message = Rc::new(String::from(get_assert_msg_description(msg)));
let precondition = Precondition {
condition,
message,
provenance: None,
spans: vec![self.bv.current_span],
};
self.bv.preconditions.push(precondition);
}
}
}
};
}

fn get_assert_msg_description<'tcx>(msg: &mir::AssertMessage<'tcx>) -> &'tcx str {
match msg {
Expand Down
18 changes: 15 additions & 3 deletions checker/src/body_visitor.rs
View file
Expand Up @@ -383,16 +383,28 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
}
}
result.unwrap_or_else(|| {
let result =
AbstractValue::make_typed_unknown(result_type.clone(), path.clone());
let result = if let PathEnum::LocalVariable { .. } = path.value {
refined_val
} else {
AbstractValue::make_typed_unknown(result_type.clone(), path.clone())
};
if result_type != ExpressionType::NonPrimitive {
self.current_environment
.update_value_at(path, result.clone());
}
result
})
} else {
AbstractValue::make_typed_unknown(result_type.clone(), path.clone())
let result = if let PathEnum::LocalVariable { .. } = path.value {
refined_val
} else {
AbstractValue::make_typed_unknown(result_type.clone(), path.clone())
};
if result_type != ExpressionType::NonPrimitive {
self.current_environment
.update_value_at(path, result.clone());
}
result
}
} else {
refined_val
Expand Down
1 change: 0 additions & 1 deletion checker/src/call_visitor.rs
View file
Expand Up @@ -305,7 +305,6 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
.active_calls_map
.get(&func_ref.def_id.unwrap())
.unwrap_or(&0u64);
info!("call depth {:?}", call_depth);
let result = self
.block_visitor
.bv
Expand Down
38 changes: 18 additions & 20 deletions checker/src/environment.rs
View file
Expand Up @@ -206,36 +206,34 @@ impl Environment {
}
None => {
checked_assume!(!val1.is_bottom());
let val2 = if !path.is_rooted_by_parameter() {
val1.clone()
if !path.is_rooted_by_parameter() {
// joining val1 and bottom
// The bottom value corresponds to dead (impossible) code, so the join collapses.
value_map = value_map.insert(p, val1.clone());
} else {
AbstractValue::make_from(
Expression::Variable {
path: path.clone(),
var_type: val1.expression.infer_type(),
},
1,
)
let val2 = AbstractValue::make_typed_unknown(
val1.expression.infer_type(),
path.clone(),
);
value_map = value_map.insert(p, join_or_widen(val1, &val2, path));
};
value_map = value_map.insert(p, join_or_widen(val1, &val2, path));
}
}
}
for (path, val2) in value_map2.iter() {
if !value_map1.contains_key(path) {
checked_assume!(!val2.is_bottom());
let val1 = if !path.is_rooted_by_parameter() {
val2.clone()
if !path.is_rooted_by_parameter() {
// joining bottom and val2
// The bottom value corresponds to dead (impossible) code, so the join collapses.
value_map = value_map.insert(path.clone(), val2.clone());
} else {
AbstractValue::make_from(
Expression::Variable {
path: path.clone(),
var_type: val2.expression.infer_type(),
},
1,
)
let val1 = AbstractValue::make_typed_unknown(
val2.expression.infer_type(),
path.clone(),
);
value_map = value_map.insert(path.clone(), join_or_widen(&val1, val2, path));
};
value_map = value_map.insert(path.clone(), join_or_widen(&val1, val2, &path));
}
}
Environment {
Expand Down

0 comments on commit d11feab

Please sign in to comment.