Adapt to nightly 2021-02-12

.travis.yml

@@ -4,7 +4,7 @@ os:
   # - windows
 language: rust
 rust:
-- nightly-2021-01-01
+- nightly-2021-02-09
 
 before_install:
 - if [ ${TRAVIS_OS_NAME} == "osx" ]; then curl -L https://github.com/mozilla/grcov/releases/download/v0.5.9/grcov-osx-x86_64.tar.bz2 | tar jxf -; fi

annotations/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 
 name = "mirai-annotations"
-version = "1.10.1"
+version = "1.11.0"
 authors = ["Herman Venter <hermanv@fb.com>"]
 description = "Macros that provide source code annotations for MIRAI"
 repository = "https://github.com/facebookexperimental/MIRAI"

annotations/README.md

@@ -37,7 +37,9 @@ Additionally we also have:
 
 This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are:
 * abstract_value!
+* add_tag!
 * get_model_field!
+* has_tag!  
 * result!
 * set_model_field!
 

annotations/src/lib.rs

@@ -64,6 +64,7 @@ pub enum TagPropagation {
     Sub,
     SubComponent,
     SubOverflows,
+    Transmute,
     UninterpretedCall,
 }
 

checker/src/abstract_value.rs

@@ -194,11 +194,11 @@ impl AbstractValue {
             // The overall expression is going to overflow, so pre-compute the simpler domains from
             // the larger expression and then replace its expression with TOP.
             if left.expression_size < right.expression_size {
-                info!("binary expression right operand abstracted");
+                debug!("binary expression right operand abstracted");
                 right = AbstractValue::make_from(right.expression.clone(), u64::MAX);
                 expression_size = left.expression_size + 1;
             } else {
-                info!("binary expression left operand abstracted");
+                debug!("binary expression left operand abstracted");
                 left = AbstractValue::make_from(left.expression.clone(), u64::MAX);
                 expression_size = right.expression_size + 1;
             }
@@ -310,7 +310,7 @@ impl AbstractValue {
         if expression_size > k_limits::MAX_EXPRESSION_SIZE {
             if expression_size < u64::MAX {
                 trace!("expression {:?}", expression);
-                info!("expression abstracted");
+                debug!("expression abstracted");
             }
             // If the expression gets too large, refining it gets expensive and composing it
             // into other expressions leads to exponential growth. We therefore need to abstract
@@ -484,6 +484,7 @@ pub trait AbstractValueTrait: Sized {
         fresh: usize,
     ) -> Self;
     fn refine_with(&self, path_condition: &Self, depth: usize) -> Self;
+    fn replace_embedded_path_root(&self, old_root: &Rc<Path>, new_root: Rc<Path>) -> Self;
     fn transmute(&self, target_type: ExpressionType) -> Self;
     fn try_resolve_as_byte_array(&self, _environment: &Environment) -> Option<Vec<u8>>;
     fn try_resolve_as_ref_to_str(&self, environment: &Environment) -> Option<Rc<str>>;
@@ -965,7 +966,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 if let Some(trimmed) = self
                     .trim_prefix_conjuncts(k_limits::MAX_EXPRESSION_SIZE - other.expression_size)
                 {
-                    info!("and expression prefix trimmed");
+                    debug!("and expression prefix trimmed");
                     trimmed_self = trimmed;
                 } else {
                     return other;
@@ -1538,23 +1539,23 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 .expression_size
                 .saturating_add(consequent.expression_size);
             if condition_plus_consequent < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                info!("alternate abstracted");
+                debug!("alternate abstracted");
                 alternate = AbstractValue::make_from(alternate.expression.clone(), u64::MAX);
                 expression_size = condition_plus_consequent + 1;
             } else {
                 let condition_plus_alternate = self
                     .expression_size
                     .saturating_add(alternate.expression_size);
                 if condition_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                    info!("consequent abstracted");
+                    debug!("consequent abstracted");
                     consequent = AbstractValue::make_from(consequent.expression.clone(), u64::MAX);
                     expression_size = condition_plus_alternate + 1;
                 } else {
                     let consequent_plus_alternate = consequent
                         .expression_size
                         .saturating_add(alternate.expression_size);
                     if consequent_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                        info!("condition abstracted");
+                        debug!("condition abstracted");
                         condition =
                             AbstractValue::make_from(condition.expression.clone(), u64::MAX);
                         expression_size = consequent_plus_alternate + 1;
@@ -2613,6 +2614,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         match &self.expression {
             Expression::Cast { operand, .. }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => {
                 operand.might_benefit_from_refinement()
             }
@@ -3990,7 +3992,8 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::IntrinsicBitVectorUnary { operand, .. }
             | Expression::IntrinsicFloatingPointUnary { operand, .. }
             | Expression::LogicalNot { operand, .. }
-            | Expression::Neg { operand, .. } => {
+            | Expression::Neg { operand, .. }
+            | Expression::Transmute { operand, .. } => {
                 operand.get_cached_tags().propagate_through(exp_tag_prop)
             }
 
@@ -4061,6 +4064,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::Neg { operand }
             | Expression::LogicalNot { operand }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => {
                 operand.get_widened_subexpression(path)
             }
@@ -4435,6 +4439,12 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             Expression::TaggedExpression { operand, tag } => operand
                 .refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
                 .add_tag(*tag),
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => operand
+                .refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
+                .transmute(target_type.clone()),
             Expression::UninterpretedCall {
                 callee,
                 arguments,
@@ -4562,7 +4572,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         //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 {
-            info!("max refine depth exceeded during refine_with");
+            debug!("max refine depth exceeded during refine_with");
             //todo: perhaps this should go away.
             // right now it deals with the situation where some large expressions have sizes
             // that are not accurately tracked. These really should get fixed.
@@ -4821,6 +4831,12 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             Expression::TaggedExpression { operand, tag } => {
                 operand.refine_with(path_condition, depth + 1).add_tag(*tag)
             }
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => operand
+                .refine_with(path_condition, depth + 1)
+                .transmute(target_type.clone()),
             Expression::UninterpretedCall {
                 callee,
                 arguments,
@@ -4863,22 +4879,75 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         }
     }
 
+    /// Given a left-hand expression that occurs in a Path that is in a root position, look for an embedded
+    /// path that is rooted in old_root and replace the path with one that is rooted in new_root.
+    #[logfn_inputs(TRACE)]
+    fn replace_embedded_path_root(
+        &self,
+        old_root: &Rc<Path>,
+        new_root: Rc<Path>,
+    ) -> Rc<AbstractValue> {
+        match &self.expression {
+            Expression::ConditionalExpression {
+                condition,
+                consequent,
+                alternate,
+            } => {
+                let replaced_consequent =
+                    consequent.replace_embedded_path_root(old_root, new_root.clone());
+                let replaced_alternate = alternate.replace_embedded_path_root(old_root, new_root);
+                condition.conditional_expression(replaced_consequent, replaced_alternate)
+            }
+            Expression::InitialParameterValue { path, var_type } => {
+                AbstractValue::make_initial_parameter_value(
+                    var_type.clone(),
+                    path.replace_root(old_root, new_root),
+                )
+            }
+            Expression::Reference(path) => {
+                AbstractValue::make_reference(path.replace_root(old_root, new_root))
+            }
+            Expression::Variable { path, var_type } => AbstractValue::make_typed_unknown(
+                var_type.clone(),
+                path.replace_root(old_root, new_root),
+            ),
+            Expression::WidenedJoin { path, operand } => {
+                operand.widen(&path.replace_root(old_root, new_root))
+            }
+            _ => {
+                if self.is_top() || self.is_bottom() {
+                    return self.clone();
+                }
+                unimplemented!(
+                    "replacing embedded path root of {:?}, old_root {:?}, new_root {:?}",
+                    self,
+                    old_root,
+                    new_root
+                );
+            }
+        }
+    }
+
     /// A cast that re-interprets existing bits rather than doing conversions.
     /// When the source type and target types differ in length, bits are truncated
     /// or zero filled as appropriate.
     #[logfn(TRACE)]
     fn transmute(&self, target_type: ExpressionType) -> Rc<AbstractValue> {
         if let Expression::CompileTimeConstant(c) = &self.expression {
             Rc::new(c.transmute(target_type).into())
-        } else if target_type.is_integer() {
+        } else if target_type.is_integer() && self.expression.infer_type().is_integer() {
             self.unsigned_modulo(target_type.bit_length())
                 .cast(target_type)
         } else if target_type == ExpressionType::Bool {
             self.unsigned_modulo(target_type.bit_length())
                 .not_equals(Rc::new(ConstantDomain::U128(0).into()))
         } else {
-            // todo: add an expression case that will delay transmutation until the operand refines to a constant
-            AbstractValue::make_typed_unknown(target_type, Path::get_as_path(self.clone()))
+            AbstractValue::make_typed_unary(self.clone(), target_type, |operand, target_type| {
+                Expression::Transmute {
+                    operand,
+                    target_type,
+                }
+            })
         }
     }
 
@@ -5038,6 +5107,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::Neg { operand }
             | Expression::LogicalNot { operand }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => operand.uses(variables),
             Expression::CompileTimeConstant(..) => false,
             Expression::ConditionalExpression {