diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs index 8ed41780..74c290b6 100644 --- a/checker/src/abstract_value.rs +++ b/checker/src/abstract_value.rs @@ -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; @@ -170,6 +170,12 @@ impl AbstractValue { result_type: ExpressionType, operation: fn(Rc, Rc, ExpressionType) -> Expression, ) -> Rc { + 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) } @@ -181,6 +187,9 @@ impl AbstractValue { result_type: ExpressionType, operation: fn(Rc, ExpressionType) -> Expression, ) -> Rc { + 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) } @@ -191,6 +200,9 @@ impl AbstractValue { operand: Rc, operation: fn(Rc) -> Expression, ) -> Rc { + 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) } @@ -458,6 +470,13 @@ impl AbstractValueTrait for Rc { /// Returns an element that is "self && other". #[logfn_inputs(TRACE)] fn and(&self, other: Rc) -> Rc { + // 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 @@ -476,13 +495,9 @@ impl AbstractValueTrait for Rc { // [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 } => { @@ -2326,11 +2341,7 @@ impl AbstractValueTrait for Rc { 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. @@ -2894,6 +2905,9 @@ impl AbstractValueTrait for Rc { /// 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 { + 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 { diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs index 68392013..664438fe 100644 --- a/checker/src/block_visitor.rs +++ b/checker/src/block_visitor.rs @@ -709,6 +709,9 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> is_post_condition: bool, ) -> Option { 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!() @@ -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 @@ -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 { diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index 18817d32..10635c45 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -383,8 +383,11 @@ 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()); @@ -392,7 +395,16 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx 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 diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index b0817f19..eb16590a 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -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 diff --git a/checker/src/environment.rs b/checker/src/environment.rs index a482a688..65b8b0cc 100644 --- a/checker/src/environment.rs +++ b/checker/src/environment.rs @@ -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 {