From 01c072e47abc3144fd7f217dc97ce2a891f5f6a0 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Tue, 22 Mar 2022 15:55:57 -0700 Subject: [PATCH] Fix delayed tag checks for tags that propagate from components to containers --- Cargo.lock | 4 +- binaries/summary_store.tar | Bin 2189824 -> 2189824 bytes checker/src/abstract_value.rs | 52 +++++---- checker/src/block_visitor.rs | 14 ++- checker/src/call_visitor.rs | 29 ++++- checker/src/expression.rs | 129 +++++++++++++++++++-- checker/src/path.rs | 44 +++++-- checker/tests/run-pass/tag_post_cond.rs | 35 ++++++ checker/tests/run-pass/tag_vector_calls.rs | 14 +-- 9 files changed, 265 insertions(+), 56 deletions(-) create mode 100644 checker/tests/run-pass/tag_post_cond.rs diff --git a/Cargo.lock b/Cargo.lock index 3466408e..fe7dc8f2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -457,9 +457,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.14" +version = "0.4.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51b9bbe6c47d51fc3e1a9b945965946b4c44142ab8792c50835a980d362c2710" +checksum = "6389c490849ff5bc16be905ae24bc913a9c8892e19b2341dbc175e14c341c2b8" dependencies = [ "cfg-if", ] diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index 9550ea91b0c66fc1a1550b87f571cb7b74d65332..4796c4081d0b0d56535e13d1ee1acff80d209199 100644 GIT binary patch delta 674 zcmYk)Ur19?90%}S=Qg+L?#|iWuJ>Nc4P+9%Y}&47MHx~VL6Tr4A^s(?5+olg0xh*$ zq#z2-vOtIeA&jB%?IEy#SiPi}Q4!0mpeQK+WD%05qeXS#^K!m?AHMKwo@f)Axy}xE zPF6Ui>;6zUqKC3g{z!L)xq46#+J%3Ko)cR0H!=TC!r?IQ=;5r8$sbzkvgRh(t6D`oYCjD1-y zJbB3jHxI~|KN^Y=1+Rj{@3GI_p5AT|5(E<#*OFWx?z|zj7U)H!z=N3uQYqqC6$xgb zH$Y>F=rhPc5AyS9tqsY&B*TZBm2|fQg)ws8gUAW`+>TH8Nz8$U4qBq)(kP(+}PP)y99YH$pL4Q6K0}v0+c+5 eY;t+*(@{Rw&&LLu_WgHaYa;reLxNBhVAfyH2>h=A delta 651 zcmYk)Pe>F|00wYp|GK6#zM0t_-^}EWU>g#VuI?JHVF!t_LqV)bNMx;M7G3fn6)2bu z=f zPR_+`+<7=}N^lo4QR$uB&)6#Cr+=c|7CnWWk1OIfam8E-Cqnc{%S`O<$lPS?YrfF5 zod=~nAg?W~hKQxWY9KoUn2D2S1zmk4REb@8$QcDBO)3Ma_aQ=&%#s^Q;mXWXi(7CA zSo=X97r_~m6#>3_RhH3qkaW9Y>{DMTaGfH@CCs<0djm+`CXZa$c251SVB!hs_QJAN zsREH%a<~XP9;hJ|Tb9UMAL3~>;lPwjZjC}~l;>#b=`*#}UX06Fj4Q#9wvdntoe$vZ7#&rSOjAii?h8Gp;-0KGXfR^>LJ)~w zy-kC3S6|r*`;&f|zahrD4^!vOTp7krQ>PCjN^P*{;p7f(?!Ccnxp-PVt7;EMMC)g3alOjE=AJX7>sSjx=`KixpcGfVE zHO$$gb`LYT&0INpSn#?>eD_ef!dNapYtX@GS$tMSfBS!bsjlwNkAZNaf_Z)cw_WX* diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs index 56a391aa..795bce97 100644 --- a/checker/src/abstract_value.rs +++ b/checker/src/abstract_value.rs @@ -4,6 +4,19 @@ // 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; @@ -11,21 +24,11 @@ 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 { 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), diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs index 28d20526..3ec4fd49 100644 --- a/checker/src/block_visitor.rs +++ b/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()], diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index 837aab1d..aa02db9a 100644 --- a/checker/src/call_visitor.rs +++ b/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) diff --git a/checker/src/expression.rs b/checker/src/expression.rs index 50b54326..8f540e86 100644 --- a/checker/src/expression.rs +++ b/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)] diff --git a/checker/src/path.rs b/checker/src/path.rs index 20351ede..ccc86757 100644 --- a/checker/src/path.rs +++ b/checker/src/path.rs @@ -3,23 +3,26 @@ // 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::{self, AbstractValue, AbstractValueTrait}; -use crate::constant_domain::ConstantDomain; -use crate::environment::Environment; -use crate::expression::{Expression, ExpressionType}; -use crate::{k_limits, utils}; - -use log_derive::*; -use mirai_annotations::*; -use rustc_hir::def_id::DefId; -use rustc_middle::ty::{Ty, TyCtxt}; -use serde::{Deserialize, Serialize}; use std::collections::hash_map::DefaultHasher; use std::collections::HashSet; use std::fmt::{Debug, Formatter, Result}; use std::hash::{Hash, Hasher}; use std::rc::Rc; +use log_derive::*; +use serde::{Deserialize, Serialize}; + +use mirai_annotations::*; +use rustc_hir::def_id::DefId; +use rustc_middle::ty::{Ty, TyCtxt}; + +use crate::abstract_value::{self, AbstractValue, AbstractValueTrait}; +use crate::constant_domain::ConstantDomain; +use crate::environment::Environment; +use crate::expression::{Expression, ExpressionType}; +use crate::tag_domain::Tag; +use crate::{k_limits, utils}; + /// During join and widen operations, paths are copied from one environment to another, causing them /// to get rehashed. This turns out to be expensive, so for this case we cache the hash to avoid /// recomputing it. The caching has a cost, so only use this in cases where it is highly likely @@ -217,6 +220,7 @@ impl Debug for PathEnum { pub trait PathRoot: Sized { fn get_path_root(&self) -> &Self; fn get_parameter_root_ordinal(&self) -> Option; + fn has_tagged_subcomponent(&self, tag: &Tag, env: &Environment) -> bool; fn is_rooted_by(&self, root: &Rc) -> bool; fn is_rooted_by_non_local_structure(&self) -> bool; fn is_rooted_by_zeroed_heap_block(&self) -> bool; @@ -244,6 +248,24 @@ impl PathRoot for Rc { } } + /// 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)] + fn has_tagged_subcomponent(&self, tag: &Tag, env: &Environment) -> bool { + let root = self.get_path_root(); + for (p, v) in env.value_map.iter() { + if p != root && !p.is_rooted_by(root) { + continue; + } + if v.has_tag(tag).as_bool_if_known().unwrap_or(false) + || v.expression.has_tagged_subcomponent(tag, env) + { + return true; + } + } + false + } + /// True if path qualifies root, or another qualified path rooted by root. #[logfn_inputs(TRACE)] fn is_rooted_by(&self, root: &Rc) -> bool { diff --git a/checker/tests/run-pass/tag_post_cond.rs b/checker/tests/run-pass/tag_post_cond.rs new file mode 100644 index 00000000..e690790f --- /dev/null +++ b/checker/tests/run-pass/tag_post_cond.rs @@ -0,0 +1,35 @@ +// Copyright (c) Facebook, Inc. and its affiliates. +// +// This source code is licensed under the MIT license found in the +// LICENSE file in the root directory of this source tree. + +// A test for taint tags that flow from components to containers + +#![feature(generic_const_exprs)] +#![allow(incomplete_features)] + +use mirai_annotations::*; + +struct SecretTaintKind {} + +const SECRET_TAINT: TagPropagationSet = tag_propagation_set!(TagPropagation::SuperComponent); + +type SecretTaint = SecretTaintKind; + +pub struct A(u32); + +pub struct B(u32); + +pub fn a_to_b(a: A) -> B { + precondition!(has_tag!(&a, SecretTaint)); + let b = B(a.0); + postcondition!(has_tag!(&b, SecretTaint)); + b +} + +pub fn main() { + let a = A(1); + add_tag!(&a.0, SecretTaint); + let b = a_to_b(a); + verify!(has_tag!(&b, SecretTaint)); +} diff --git a/checker/tests/run-pass/tag_vector_calls.rs b/checker/tests/run-pass/tag_vector_calls.rs index 6909a6b0..b2abb152 100644 --- a/checker/tests/run-pass/tag_vector_calls.rs +++ b/checker/tests/run-pass/tag_vector_calls.rs @@ -83,15 +83,15 @@ pub mod propagation_for_vector_calls { } pub fn test6() { - // let mut bar: Vec = vec![]; - // bar.push(Foo { content: 0 }); - // add_tag!(&bar[0].content, SecretTaint); - // call6(bar); + let mut bar: Vec = vec![]; + bar.push(Foo { content: 0 }); + add_tag!(&bar[0].content, SecretTaint); + call6(bar); } - // fn call6(bar: Vec) { - // precondition!(has_tag!(&bar[0].content, SecretTaint)); - // } + fn call6(bar: Vec) { + precondition!(has_tag!(&bar[0].content, SecretTaint)); + } pub fn test7() { let mut bar: Vec = vec![];