Fix problems with tag propagation from component to container

checker/src/abstract_value.rs

@@ -4,28 +4,31 @@
 // LICENSE file in the root directory of this source tree.
 
 #![allow(clippy::declare_interior_mutable_const)]
+
+use std::cell::RefCell;
+use std::collections::HashSet;
+use std::fmt::{Debug, Formatter, Result};
+use std::hash::Hash;
+use std::hash::Hasher;
+use std::rc::Rc;
+
+use log_derive::{logfn, logfn_inputs};
+use serde::{Deserialize, Serialize};
+
+use mirai_annotations::*;
+
 use crate::bool_domain::BoolDomain;
 use crate::constant_domain::ConstantDomain;
 use crate::environment::Environment;
 use crate::expression::Expression::{ConditionalExpression, Join};
 use crate::expression::{Expression, ExpressionType};
 use crate::interval_domain::{self, IntervalDomain};
 use crate::k_limits;
+use crate::known_names::KnownNames;
 use crate::path::{Path, PathEnum, PathSelector};
 use crate::path::{PathRefinement, PathRoot};
 use crate::tag_domain::{Tag, TagDomain};
 
-use crate::known_names::KnownNames;
-use log_derive::{logfn, logfn_inputs};
-use mirai_annotations::*;
-use serde::{Deserialize, Serialize};
-use std::cell::RefCell;
-use std::collections::HashSet;
-use std::fmt::{Debug, Formatter, Result};
-use std::hash::Hash;
-use std::hash::Hasher;
-use std::rc::Rc;
-
 // See https://github.com/facebookexperimental/MIRAI/blob/main/documentation/AbstractValues.md.
 
 /// Mirai is an abstract interpreter and thus produces abstract values.
@@ -292,8 +295,7 @@ impl AbstractValue {
         }
     }
 
-    #[logfn_inputs(DEBUG)]
-    #[logfn(DEBUG)]
+    #[logfn_inputs(TRACE)]
     fn make_presence_check(&self, tag: Tag) -> Rc<AbstractValue> {
         let exp_tag_prop_opt = self.expression.get_tag_propagation();
 
@@ -311,14 +313,24 @@ impl AbstractValue {
                 return Rc::new(FALSE);
             }
 
-            Expression::InitialParameterValue { .. }
-            | Expression::UnknownModelField { .. }
-            | Expression::UnknownTagField { .. }
-            | Expression::Variable { .. } => {
+            Expression::InitialParameterValue { path, .. }
+            | Expression::UnknownModelField { path, .. }
+            | Expression::UnknownTagField { path, .. }
+            | Expression::Variable { path, .. } => {
                 let expression_size = self.expression_size.saturating_add(1);
+                let root = path.get_path_root();
+                let operand =
+                    if root != path && tag.is_propagated_by(TagPropagation::SuperComponent) {
+                        AbstractValue::make_typed_unknown(
+                            ExpressionType::NonPrimitive,
+                            Path::new_tag_field(root.clone()),
+                        )
+                    } else {
+                        Rc::new(self.clone())
+                    };
                 return AbstractValue::make_from(
                     Expression::UnknownTagCheck {
-                        operand: Rc::new(self.clone()),
+                        operand,
                         tag,
                         checking_presence: true,
                     },
@@ -364,7 +376,7 @@ impl AbstractValue {
                     Rc::new(TRUE)
                 } else {
                     operand.make_presence_check(tag)
-                }
+                };
             }
 
             Expression::WidenedJoin { operand, .. } => return operand.make_presence_check(tag),
@@ -532,7 +544,7 @@ impl AbstractValue {
                     Rc::new(FALSE)
                 } else {
                     operand.make_absence_check(tag)
-                }
+                };
             }
 
             Expression::WidenedJoin { operand, .. } => return operand.make_absence_check(tag),

checker/src/block_visitor.rs

@@ -1346,7 +1346,13 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
                         let span = self.bv.current_span.source_callsite();
                         let warning = self.bv.cv.session.struct_span_warn(
                             span,
-                            format!("the {} may have a {} tag", value_name, tag_name).as_str(),
+                            format!(
+                                "the {} {} have a {} tag",
+                                value_name,
+                                if checking_presence { "may not" } else { "may" },
+                                tag_name
+                            )
+                            .as_str(),
                         );
                         self.bv.emit_diagnostic(warning);
                     } else if promotable_entry_condition.is_none()
@@ -1395,8 +1401,10 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
                     let precondition = Precondition {
                         condition,
                         message: Rc::from(format!(
-                            "the {} may have a {} tag",
-                            value_name, tag_name
+                            "the {} {} have a {} tag",
+                            value_name,
+                            if checking_presence { "may not" } else { "may" },
+                            tag_name
                         )),
                         provenance: None,
                         spans: vec![self.bv.current_span.source_callsite()],

checker/src/call_visitor.rs

@@ -1549,11 +1549,9 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx>
 
             // If the tag can be propagated from a sub-component to its container
             if tag.is_propagated_by(TagPropagation::SuperComponent) {
+                let root = source_path.get_path_root();
                 let value_map = self.block_visitor.bv.current_environment.value_map.clone();
-                for (_, value) in value_map
-                    .iter()
-                    .filter(|(p, _)| p.is_rooted_by(&source_path))
-                {
+                for (_, value) in value_map.iter().filter(|(p, _)| p.is_rooted_by(root)) {
                     let mut value = value.clone();
                     if let Expression::Reference(p) = &value.expression {
                         if let PathEnum::HeapBlock { .. } = &p.value {
@@ -2700,6 +2698,29 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx>
                 warn = true;
             }
 
+            // Is the precondition a tag check for a tag that flows from a subcomponent to the
+            // container?
+            if let Expression::UnknownTagCheck {
+                operand,
+                tag,
+                checking_presence,
+            } = &refined_condition.expression
+            {
+                if tag.is_propagated_by(TagPropagation::SuperComponent) {
+                    // Look at sub components. If components that are located via
+                    // pointers are tagged, those tags will not have propagated to here
+                    // because the pointers are unidirectional.
+                    if *checking_presence
+                        && operand.expression.has_tagged_subcomponent(
+                            tag,
+                            &self.block_visitor.bv.current_environment,
+                        )
+                    {
+                        continue;
+                    }
+                }
+            }
+
             // If the current function is not an analysis root, promote the precondition, subject to a k-limit.
             if (!self.block_visitor.bv.function_being_analyzed_is_root()
                 || self.block_visitor.bv.cv.options.diag_level == DiagLevel::Default)

checker/src/expression.rs

@@ -3,19 +3,22 @@
 // This source code is licensed under the MIT license found in the
 // LICENSE file in the root directory of this source tree.
 
-use crate::abstract_value::{AbstractValue, AbstractValueTrait};
-use crate::constant_domain::ConstantDomain;
-use crate::known_names::KnownNames;
-use crate::path::Path;
-use crate::tag_domain::Tag;
+use std::collections::HashSet;
+use std::fmt::{Debug, Formatter, Result};
+use std::rc::Rc;
 
 use log_derive::*;
+use serde::{Deserialize, Serialize};
+
 use mirai_annotations::*;
 use rustc_middle::ty::{FloatTy, IntTy, Ty, TyCtxt, TyKind, TypeAndMut, UintTy};
-use serde::{Deserialize, Serialize};
-use std::collections::HashSet;
-use std::fmt::{Debug, Formatter, Result};
-use std::rc::Rc;
+
+use crate::abstract_value::{AbstractValue, AbstractValueTrait};
+use crate::constant_domain::ConstantDomain;
+use crate::environment::Environment;
+use crate::known_names::KnownNames;
+use crate::path::{Path, PathRoot};
+use crate::tag_domain::Tag;
 
 /// Closely based on the expressions found in MIR.
 #[derive(Serialize, Deserialize, Clone, Eq, PartialEq, Hash, Ord, PartialOrd)]
@@ -912,6 +915,114 @@ impl Expression {
         }
     }
 
+    /// Returns true if the given expression is known to have a subcomponent in the given
+    /// environment that is tagged with the given tag. False does not imply the absence of the tag.
+    #[logfn_inputs(TRACE)]
+    pub fn has_tagged_subcomponent(&self, tag: &Tag, env: &Environment) -> bool {
+        match self {
+            Expression::Add { left, right }
+            | Expression::AddOverflows { left, right, .. }
+            | Expression::And { left, right }
+            | Expression::BitAnd { left, right }
+            | Expression::BitOr { left, right }
+            | Expression::BitXor { left, right }
+            | Expression::Div { left, right }
+            | Expression::Equals { left, right }
+            | Expression::GreaterOrEqual { left, right }
+            | Expression::GreaterThan { left, right }
+            | Expression::IntrinsicBinary { left, right, .. }
+            | Expression::LessOrEqual { left, right }
+            | Expression::LessThan { left, right }
+            | Expression::Mul { left, right }
+            | Expression::MulOverflows { left, right, .. }
+            | Expression::Ne { left, right }
+            | Expression::Offset { left, right }
+            | Expression::Or { left, right }
+            | Expression::Rem { left, right }
+            | Expression::Shl { left, right }
+            | Expression::ShlOverflows { left, right, .. }
+            | Expression::Shr { left, right, .. }
+            | Expression::ShrOverflows { left, right, .. }
+            | Expression::Sub { left, right }
+            | Expression::SubOverflows { left, right, .. } => {
+                left.expression.has_tagged_subcomponent(tag, env)
+                    || right.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::BitNot { operand, .. }
+            | Expression::Cast { operand, .. }
+            | Expression::IntrinsicBitVectorUnary { operand, .. }
+            | Expression::IntrinsicFloatingPointUnary { operand, .. }
+            | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. } => {
+                operand.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::Bottom => false,
+
+            Expression::CompileTimeConstant(..) => false,
+            Expression::ConditionalExpression {
+                condition,
+                consequent,
+                alternate,
+            } => {
+                condition.expression.has_tagged_subcomponent(tag, env)
+                    || consequent.expression.has_tagged_subcomponent(tag, env)
+                    || alternate.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::HeapBlock { .. } => false,
+            Expression::HeapBlockLayout {
+                length, alignment, ..
+            } => {
+                length.expression.has_tagged_subcomponent(tag, env)
+                    || alignment.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::InitialParameterValue { path, .. } => {
+                path.has_tagged_subcomponent(tag, env)
+            }
+            Expression::Join { left, right, .. } => {
+                left.expression.has_tagged_subcomponent(tag, env)
+                    || right.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::Memcmp {
+                left,
+                right,
+                length,
+            } => {
+                left.expression.has_tagged_subcomponent(tag, env)
+                    || right.expression.has_tagged_subcomponent(tag, env)
+                    || length.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::Neg { operand }
+            | Expression::LogicalNot { operand }
+            | Expression::UnknownTagCheck { operand, .. } => {
+                operand.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::Reference(path) => path.has_tagged_subcomponent(tag, env),
+            Expression::Switch {
+                discriminator,
+                cases,
+                default,
+            } => {
+                discriminator.expression.has_tagged_subcomponent(tag, env)
+                    || default.expression.has_tagged_subcomponent(tag, env)
+                    || cases
+                        .iter()
+                        .any(|(_, v)| v.expression.has_tagged_subcomponent(tag, env))
+            }
+            Expression::Top => true,
+            Expression::UninterpretedCall { .. } => true,
+            Expression::UnknownModelField { path, default } => {
+                path.has_tagged_subcomponent(tag, env)
+                    || default.expression.has_tagged_subcomponent(tag, env)
+            }
+            Expression::UnknownTagField { path } | Expression::Variable { path, .. } => {
+                path.has_tagged_subcomponent(tag, env)
+            }
+            Expression::WidenedJoin { operand, .. } => {
+                operand.expression.has_tagged_subcomponent(tag, env)
+            }
+        }
+    }
+
     /// Returns the type of value the expression should result in, if well formed.
     /// (both operands are of the same type for binary operators, conditional branches match).
     #[logfn_inputs(TRACE)]