Skip to content

Commit

Permalink
Fix delayed tag checks for tags that propagate from components to con…
Browse files Browse the repository at this point in the history 
…tainers (facebookexperimental#1142)
  • Loading branch information
Herman Venter committed Mar 24, 2022
1 parent 8e511b7 commit 6c307db
Show file tree
Hide file tree
Showing 9 changed files with 265 additions and 56 deletions.
4 changes: 2 additions & 2 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Binary file modified binaries/summary_store.tar
View file
Binary file not shown.
52 changes: 32 additions & 20 deletions checker/src/abstract_value.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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();

Expand All @@ -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,
},
Expand Down Expand Up @@ -364,7 +376,7 @@ impl AbstractValue {
Rc::new(TRUE)
} else {
operand.make_presence_check(tag)
}
};
}

Expression::WidenedJoin { operand, .. } => return operand.make_presence_check(tag),
Expand Down Expand Up @@ -532,7 +544,7 @@ impl AbstractValue {
Rc::new(FALSE)
} else {
operand.make_absence_check(tag)
}
};
}

Expression::WidenedJoin { operand, .. } => return operand.make_absence_check(tag),
Expand Down
14 changes: 11 additions & 3 deletions checker/src/block_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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()],
Expand Down
29 changes: 25 additions & 4 deletions checker/src/call_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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)
Expand Down
129 changes: 120 additions & 9 deletions checker/src/expression.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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)]
Expand Down
Loading

0 comments on commit 6c307db

Please sign in to comment.