Provide a way to specify an abstract value in a test case

annotations/Cargo.toml

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

annotations/README.md

@@ -35,6 +35,7 @@ Additionally we also have:
 * verify_unreachable! which requires MIRAI to verify that it is not unreachable.
 
 This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are:
+* abstract_value!
 * get_model_field!
 * result!
 * set_model_field!

annotations/src/lib.rs

@@ -5,6 +5,23 @@
 
 // A set of macros and functions to use for annotating source files that are being checked with MIRAI
 
+/// Provides a way to specify a value that should be treated abstractly by the verifier.
+/// The concrete argument provides type information to the verifier and a meaning for
+/// the expression when compiled by the rust compiler.
+///
+/// The expected use case for this is inside test cases. Principally this would be test cases
+/// for the verifier itself, but it can also be used to "fuzz" unit tests in user code.
+#[macro_export]
+macro_rules! abstract_value {
+    ($value:expr) => {
+        if cfg!(mirai) {
+            mirai_annotations::mirai_abstract_value($value)
+        } else {
+            $value
+        }
+    };
+}
+
 /// Equivalent to a no op when used with an unmodified Rust compiler.
 /// When compiled with MIRAI, this causes MIRAI to assume the condition unless it can
 /// prove it to be false.
@@ -890,6 +907,12 @@ macro_rules! verify_unreachable {
     };
 }
 
+// Helper function for MIRAI. Should only be called via the result! macro.
+#[doc(hidden)]
+pub fn mirai_abstract_value<T>(x: T) -> T {
+    x
+}
+
 // Helper function for MIRAI. Should only be called via the assume macros.
 #[doc(hidden)]
 pub fn mirai_assume(_condition: bool) {}

checker/src/known_names.rs

@@ -14,6 +14,7 @@ use std::collections::HashMap;
 pub enum KnownNames {
     /// This is not a known name
     None,
+    MiraiAbstractValue,
     MiraiAssume,
     MiraiAssumePreconditions,
     MiraiGetModelField,
@@ -201,6 +202,7 @@ impl KnownNamesCache {
                     "panicking" => get_known_name_for_panicking_namespace(def_path_data_iter),
                     "slice" => get_known_name_for_slice_namespace(def_path_data_iter),
                     "str" => get_known_name_for_str_namespace(def_path_data_iter),
+                    "mirai_abstract_value" => KnownNames::MiraiAbstractValue,
                     "mirai_assume" => KnownNames::MiraiAssume,
                     "mirai_assume_preconditions" => KnownNames::MiraiAssumePreconditions,
                     "mirai_get_model_field" => KnownNames::MiraiGetModelField,

checker/src/visitors.rs

@@ -1673,6 +1673,11 @@ impl<'analysis, 'compilation, 'tcx, E> MirVisitor<'analysis, 'compilation, 'tcx,
             | KnownNames::StdOpsFunctionFnOnceCallOnce => {
                 return !self.try_to_inline_standard_ops_func(call_info).is_bottom();
             }
+            KnownNames::MiraiAbstractValue => {
+                checked_assume!(call_info.actual_args.len() == 1);
+                self.handle_abstract_value(call_info);
+                return true;
+            }
             KnownNames::MiraiAssume => {
                 checked_assume!(call_info.actual_args.len() == 1);
                 if self.check_for_errors {
@@ -1808,6 +1813,31 @@ impl<'analysis, 'compilation, 'tcx, E> MirVisitor<'analysis, 'compilation, 'tcx,
         false
     }
 
+    /// Replace the call result with an abstract value of the same type as the
+    /// destination place.
+    fn handle_abstract_value(&mut self, call_info: &CallInfo<'_, 'tcx>) {
+        if let Some((place, target)) = &call_info.destination {
+            let path = self.visit_place(place);
+            let expression_type = self.get_place_type(place);
+            let abstract_value = AbstractValue::make_from(
+                Expression::Variable {
+                    path: path.clone(),
+                    var_type: expression_type,
+                },
+                1,
+            );
+            self.current_environment
+                .update_value_at(path, abstract_value);
+            let exit_condition = self.current_environment.entry_condition.clone();
+            self.current_environment.exit_conditions = self
+                .current_environment
+                .exit_conditions
+                .insert(*target, exit_condition);
+        } else {
+            assume_unreachable!();
+        }
+    }
+
     /// Update the state so that the call result is the value of the model field (or the default
     /// value if there is no field).
     fn handle_get_model_field(&mut self, call_info: &CallInfo<'_, 'tcx>) {

checker/tests/run-pass/abstract_value.rs

@@ -0,0 +1,18 @@
+// 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 that uses abstract_value!
+
+#[macro_use]
+extern crate mirai_annotations;
+
+pub fn main() {
+    let a = abstract_value!(6i32);
+    let b = abstract_value!(7i32);
+    assume!(4 < a && a < 8); // a in [5,7]
+    assume!(5 < b && b < 9); // b in [6,8]
+    verify!(30 <= a * b && a * b <= 56); // a*b in [30,56]
+}