Keep track of tag checks from preconditions

checker/src/abstract_value.rs

@@ -391,6 +391,7 @@ pub trait AbstractValueTrait: Sized {
     fn refine_paths(&self, environment: &Environment) -> Self;
     fn refine_parameters(&self, arguments: &[(Rc<Path>, Rc<AbstractValue>)], fresh: usize) -> Self;
     fn refine_with(&self, path_condition: &Self, depth: usize) -> Self;
+    fn replace_tags(&self, tags: Rc<TagDomain>) -> Self;
     fn uninterpreted_call(
         &self,
         arguments: Vec<Rc<AbstractValue>>,
@@ -2624,7 +2625,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             }
 
             Expression::TaggedExpression { operand, tag } => {
-                return operand.get_cached_tags().add_tag(*tag);
+                return operand.get_cached_tags().set_tag(*tag, BoolDomain::True);
             }
 
             Expression::Widen { operand, .. } => {
@@ -3513,6 +3514,18 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         }
     }
 
+    /// Replace the tag abstraction of `self` with the given one.
+    /// This routine can only be used for keeping track of tag information from preconditions.
+    #[logfn_inputs(TRACE)]
+    fn replace_tags(&self, tags: Rc<TagDomain>) -> Rc<AbstractValue> {
+        Rc::new(AbstractValue {
+            expression: self.expression.clone(),
+            expression_size: self.expression_size,
+            interval: RefCell::new(self.interval.borrow().clone()),
+            tags: RefCell::new(Some(tags)),
+        })
+    }
+
     /// Returns a domain whose corresponding set of concrete values include all of the values
     /// that the call expression might return at runtime. The function to be called will not
     /// have been summarized for some reason or another (for example, it might be a foreign function).

checker/src/environment.rs

@@ -6,6 +6,7 @@
 use crate::abstract_value;
 use crate::abstract_value::AbstractValue;
 use crate::abstract_value::AbstractValueTrait;
+use crate::bool_domain::BoolDomain;
 use crate::expression::{Expression, ExpressionType};
 use crate::path::{Path, PathEnum, PathSelector};
 use crate::tag_domain::Tag;
@@ -356,4 +357,45 @@ impl Environment {
         let new_abs = cond.conditional_expression(old_abs.add_tag(tag), old_abs);
         self.value_map.insert_mut(path, new_abs);
     }
+
+    /// Refine the tag abstraction of all values recorded in `self` by inspecting the entry condition.
+    /// If entry condition implies `UnknownTagCheck { path, tag, checking_presence }`, we want to
+    /// update the tag abstraction of the value located at `path` in a way the the presence of `tag`
+    /// is set to `checking_presence`.
+    #[logfn_inputs(TRACE)]
+    pub fn refine_tags(&mut self) {
+        self.refine_tags_with_entry_condition(&self.entry_condition.clone());
+    }
+
+    /// Refine the tag abstraction of all values recorded in `self` by inspecting `entry_cond`.
+    #[logfn_inputs(TRACE)]
+    fn refine_tags_with_entry_condition(&mut self, entry_cond: &Rc<AbstractValue>) {
+        match &entry_cond.expression {
+            Expression::And { left, right } => {
+                self.refine_tags_with_entry_condition(left);
+                self.refine_tags_with_entry_condition(right);
+            }
+            Expression::UnknownTagCheck {
+                path,
+                tag,
+                checking_presence,
+            } => {
+                let value_map = self.value_map.clone();
+                if let Some(value) = value_map.get(path) {
+                    let cached_tags = value.get_cached_tags();
+                    let refined_tags = cached_tags.set_tag(
+                        *tag,
+                        if *checking_presence {
+                            BoolDomain::True
+                        } else {
+                            BoolDomain::False
+                        },
+                    );
+                    let refined_value = value.replace_tags(Rc::new(refined_tags));
+                    self.value_map.insert_mut(path.clone(), refined_value);
+                }
+            }
+            _ => {}
+        }
+    }
 }

checker/src/fixed_point_visitor.rs

@@ -107,6 +107,7 @@ impl<'fixed, 'analysis, 'compilation, 'tcx, E>
         };
         self.in_state.insert(bb, i_state.clone());
         self.bv.current_environment = i_state;
+        self.bv.current_environment.refine_tags();
         let mut block_visitor = BlockVisitor::new(self.bv);
         block_visitor.visit_basic_block(bb, &mut self.terminator_state);
         self.out_state

checker/src/tag_domain.rs

@@ -164,11 +164,11 @@ impl TagDomain {
 
 /// Transfer functions
 impl TagDomain {
-    /// Return a new tag domain element by setting `tag` to True in `self`.
+    /// Return a new tag domain element by setting `tag` to `val` in `self`.
     #[logfn_inputs(TRACE)]
-    pub fn add_tag(&self, tag: Tag) -> Self {
+    pub fn set_tag(&self, tag: Tag, val: BoolDomain) -> Self {
         TagDomain {
-            map: self.map.insert(tag, BoolDomain::True),
+            map: self.map.insert(tag, val),
             value_for_untracked_tags: self.value_for_untracked_tags,
         }
     }

checker/tests/run-pass/tag_domain.rs

@@ -26,8 +26,9 @@ const SECRET_SANITIZER: TagPropagationSet = tag_propagation_set!(TagPropagation:
 
 type SecretSanitizer = SecretSanitizerKind<SECRET_SANITIZER>;
 
-pub fn test() {
-    let secret = 23333;
+pub fn test(secret: i32) {
+    precondition!(does_not_have_tag!(&secret, SecretTaint));
+    precondition!(does_not_have_tag!(&secret, SecretSanitizer));
 
     add_tag!(&secret, SecretTaint);
     verify!(has_tag!(&secret, SecretTaint));