[move-prover] Setting the stage for negative (e.g. soundness) verific…

…ation tests.

This PR resolves a TODO around the management of annotations for function data. Specifically, it makes the `Annotations` type clonable. As annotations are build on top of the `Any` type, this wasn't working without extra effort before, and created some ugly workarounds.

As a result, we can now freely create function variants which opens the door for negative tests like "soundness" checks. For that, we can simply introduce a new processor which uses `FunctionData::fork(&self, variant)` to create a new variant which will then be passed on and compiled by the Boogie backend.

Closes: diem#7833

language/move-prover/boogie-backend/src/boogie_wrapper.rs

@@ -25,7 +25,7 @@ use crate::prover_task_runner::{ProverTaskRunner, RunBoogieWithSeeds};
 // DEBUG
 // use backtrace::Backtrace;
 use crate::options::BoogieOptions;
-use bytecode::function_target_pipeline::FunctionTargetsHolder;
+use bytecode::function_target_pipeline::{FunctionTargetsHolder, FunctionVariant};
 use move_model::{
     ast::TempIndex,
     model::{NodeId, QualifiedId},
@@ -203,7 +203,8 @@ impl<'env> BoogieWrapper<'env> {
                     }
                     Temporary(fun, idx, value) if error.model.is_some() => {
                         let fun_env = self.env.get_function(*fun);
-                        let fun_target = self.targets.get_annotated_target(&fun_env);
+                        let fun_target =
+                            self.targets.get_target(&fun_env, FunctionVariant::Baseline);
                         if *idx < fun_target.get_local_count() {
                             let var_name = fun_target
                                 .get_local_name(*idx)
@@ -229,7 +230,8 @@ impl<'env> BoogieWrapper<'env> {
                     }
                     Result(fun, idx, value) if error.model.is_some() => {
                         let fun_env = self.env.get_function(*fun);
-                        let fun_target = self.targets.get_annotated_target(&fun_env);
+                        let fun_target =
+                            self.targets.get_target(&fun_env, FunctionVariant::Baseline);
                         let n = fun_target.get_return_count();
                         if *idx < n {
                             let var_name = if n > 1 {

language/move-prover/boogie-backend/src/bytecode_translator.rs

@@ -198,11 +198,14 @@ impl<'env> ModuleTranslator<'env> {
             if func_env.is_native() || func_env.is_intrinsic() {
                 continue;
             }
-            let verification_info =
-                verification_analysis::get_info(&self.targets.get_annotated_target(&func_env));
+            let verification_info = verification_analysis::get_info(
+                &self
+                    .targets
+                    .get_target(&func_env, FunctionVariant::Baseline),
+            );
             for variant in self.targets.get_target_variants(&func_env) {
-                if verification_info.verified && variant == FunctionVariant::Verification
-                    || verification_info.inlined && variant == FunctionVariant::Baseline
+                if verification_info.verified && variant.is_verified()
+                    || verification_info.inlined && !variant.is_verified()
                 {
                     self.translate_function(variant, &self.targets.get_target(&func_env, variant));
                 }
@@ -225,8 +228,8 @@ impl<'env> ModuleTranslator<'env> {
         let (args, rets) = self.generate_function_args_and_returns(fun_target);
 
         let (suffix, attribs) = match variant {
-            FunctionVariant::Baseline => ("", "{:inline 1} ".to_string()),
-            FunctionVariant::Verification => {
+            FunctionVariant::Baseline => ("".to_string(), "{:inline 1} ".to_string()),
+            FunctionVariant::Verification(flavor) => {
                 let timeout = fun_target
                     .func_env
                     .get_num_pragma(TIMEOUT_PRAGMA, || self.options.vc_timeout);
@@ -238,7 +241,11 @@ impl<'env> ModuleTranslator<'env> {
                 } else {
                     format!("{{:timeLimit {}}} ", timeout)
                 };
-                ("$verify", attribs)
+                if flavor.is_empty() {
+                    ("$verify".to_string(), attribs)
+                } else {
+                    (format!("$verify_{}", flavor), attribs)
+                }
             }
         };
         self.writer.set_location(&fun_target.get_loc());
@@ -356,7 +363,7 @@ impl<'env> ModuleTranslator<'env> {
         }
 
         // Initial assumptions
-        if variant == FunctionVariant::Verification {
+        if variant.is_verified() {
             self.translate_verify_entry_assumptions(fun_target);
         }
 

language/move-prover/bytecode/src/annotations.rs

@@ -1,15 +1,58 @@
 // Copyright (c) The Diem Core Contributors
 // SPDX-License-Identifier: Apache-2.0
 
+use itertools::Itertools;
 use std::{
     any::{Any, TypeId},
     collections::BTreeMap,
+    fmt::{Debug, Formatter, Result},
+    rc::Rc,
 };
 
 /// A container for an extensible, dynamically typed set of annotations.
-#[derive(Debug, Default)]
+#[derive(Default, Clone)]
 pub struct Annotations {
-    map: BTreeMap<TypeId, Box<dyn Any>>,
+    map: BTreeMap<TypeId, Data>,
+}
+
+/// An internal struct to represent annotation data. This carries in addition to the
+/// dynamically typed value a function for cloning this value. This works
+/// around the restriction that we cannot use a trait to call into an Any type, so we need
+/// to maintain the "vtable" by ourselves.
+struct Data {
+    value: Box<dyn Any>,
+    clone_fun: Rc<dyn Fn(&Box<dyn Any>) -> Box<dyn Any>>,
+}
+
+impl Data {
+    fn new<T: Any + Clone>(x: T) -> Self {
+        let clone_fun = Rc::new(|x: &Box<dyn Any>| -> Box<dyn Any> {
+            Box::new(x.downcast_ref::<T>().unwrap().clone())
+        });
+        Self {
+            value: Box::new(x),
+            clone_fun,
+        }
+    }
+}
+
+impl Clone for Data {
+    fn clone(&self) -> Self {
+        Self {
+            value: (self.clone_fun)(&self.value),
+            clone_fun: self.clone_fun.clone(),
+        }
+    }
+}
+
+impl Debug for Annotations {
+    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
+        write!(
+            f,
+            "annotations{{{}}}",
+            self.map.keys().map(|t| format!("{:?}", t)).join(", ")
+        )
+    }
 }
 
 impl Annotations {
@@ -22,28 +65,31 @@ impl Annotations {
     /// Gets annotation of type T.
     pub fn get<T: Any>(&self) -> Option<&T> {
         let id = TypeId::of::<T>();
-        self.map.get(&id).and_then(|d| d.downcast_ref::<T>())
+        self.map.get(&id).and_then(|d| d.value.downcast_ref::<T>())
     }
 
     /// Gets annotation of type T or creates one from default.
-    pub fn get_or_default_mut<T: Any + Default>(&mut self) -> &mut T {
+    pub fn get_or_default_mut<T: Any + Default + Clone>(&mut self) -> &mut T {
         let id = TypeId::of::<T>();
         self.map
             .entry(id)
-            .or_insert_with(|| Box::new(T::default()))
+            .or_insert_with(|| Data::new(T::default()))
+            .value
             .downcast_mut::<T>()
             .expect("cast successful")
     }
 
     /// Sets annotation of type T.
-    pub fn set<T: Any>(&mut self, x: T) {
+    pub fn set<T: Any + Clone>(&mut self, x: T) {
         let id = TypeId::of::<T>();
-        self.map.insert(id, Box::new(x));
+        self.map.insert(id, Data::new(x));
     }
 
     /// Removes annotation of type T.
     pub fn remove<T: Any>(&mut self) -> Option<Box<T>> {
         let id = TypeId::of::<T>();
-        self.map.remove(&id).and_then(|d| d.downcast::<T>().ok())
+        self.map
+            .remove(&id)
+            .and_then(|d| d.value.downcast::<T>().ok())
     }
 }

language/move-prover/bytecode/src/borrow_analysis.rs

@@ -18,7 +18,10 @@ use move_model::{
     ast::TempIndex,
     model::{FunctionEnv, QualifiedId},
 };
-use std::collections::{BTreeMap, BTreeSet};
+use std::{
+    borrow::BorrowMut,
+    collections::{BTreeMap, BTreeSet},
+};
 use vm::file_format::CodeOffset;
 
 /// Borrow graph edge abstract domain.
@@ -287,12 +290,14 @@ impl BorrowInfo {
     }
 }
 
+#[derive(Clone)]
 pub struct BorrowInfoAtCodeOffset {
     pub before: BorrowInfo,
     pub after: BorrowInfo,
 }
 
 /// Borrow annotation computed by the borrow analysis processor.
+#[derive(Clone)]
 pub struct BorrowAnnotation(BTreeMap<CodeOffset, BorrowInfoAtCodeOffset>);
 
 impl BorrowAnnotation {
@@ -330,8 +335,10 @@ impl FunctionTargetProcessor for BorrowAnalysisProcessor {
             BorrowAnnotation(propagator.run(&data.code))
         };
         // Annotate function target with computed borrow data.
-        data.annotations.set::<BorrowAnnotation>(borrow_annotation);
-        data.annotations.remove::<LiveVarAnnotation>();
+        data.annotations
+            .borrow_mut()
+            .set::<BorrowAnnotation>(borrow_annotation);
+        data.annotations.borrow_mut().remove::<LiveVarAnnotation>();
         data
     }
 

language/move-prover/bytecode/src/data_invariant_instrumentation.rs

@@ -13,7 +13,7 @@
 use crate::{
     function_data_builder::FunctionDataBuilder,
     function_target::FunctionData,
-    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
+    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
     options::ProverOptions,
     stackless_bytecode::{Bytecode, Operation, PropKind},
 };
@@ -72,8 +72,7 @@ impl<'a> Instrumenter<'a> {
     ) -> FunctionData {
         // Function is instrumented for verification if this is the verification variant,
         // or if it is function with a friend which is verified in the friends context.
-        let for_verification =
-            data.variant == FunctionVariant::Verification || fun_env.has_friend();
+        let for_verification = data.variant.is_verified() || fun_env.has_friend();
         let builder = FunctionDataBuilder::new(fun_env, data);
         let mut instrumenter = Instrumenter {
             _options: options,

language/move-prover/bytecode/src/function_target.rs

@@ -44,7 +44,7 @@ impl<'env> Clone for FunctionTarget<'env> {
 
 /// Holds the owned data belonging to a FunctionTarget, contained in a
 /// `FunctionTargetsHolder`.
-#[derive(Debug)]
+#[derive(Debug, Clone)]
 pub struct FunctionData {
     /// The function variant.
     pub variant: FunctionVariant,
@@ -65,9 +65,10 @@ pub struct FunctionData {
     /// A map from byte code attribute to a message to be printed out if verification
     /// fails at this bytecode.
     pub vc_infos: BTreeMap<AttrId, String>,
-    /// Annotations associated with this function.
+    /// Annotations associated with this function. This is shared between multiple function
+    /// variants.
     pub annotations: Annotations,
-    /// A map from local names to temp indices in code.
+    /// A mapping from symbolic names to temporaries.
     pub name_to_index: BTreeMap<Symbol, usize>,
     /// A cache of targets modified by this function.
     pub modify_targets: BTreeMap<QualifiedId<StructId>, Vec<Exp>>,
@@ -379,16 +380,7 @@ impl FunctionData {
         assert_ne!(self.variant, new_variant);
         FunctionData {
             variant: new_variant,
-            code: self.code.clone(),
-            local_types: self.local_types.clone(),
-            return_types: self.return_types.clone(),
-            acquires_global_resources: self.acquires_global_resources.clone(),
-            locations: self.locations.clone(),
-            debug_comments: self.debug_comments.clone(),
-            vc_infos: self.vc_infos.clone(),
-            annotations: Default::default(),
-            name_to_index: self.name_to_index.clone(),
-            modify_targets: self.modify_targets.clone(),
+            ..self.clone()
         }
     }
 }

language/move-prover/bytecode/src/function_target_pipeline.rs

@@ -24,17 +24,33 @@ pub enum FunctionVariant {
     /// The baseline variant which was created from the original Move bytecode and is then
     /// subject of multiple transformations.
     Baseline,
-    /// The variant which is instrumented for verification. Only functions which are target
-    /// of verification have one of those.
-    Verification,
+    /// A variant which is instrumented for verification. Only functions which are target
+    /// of verification have one of those. There can be multiple verification variants,
+    /// identified by a well-known string.
+    Verification(&'static str),
 }
 
+impl FunctionVariant {
+    pub fn is_verified(&self) -> bool {
+        matches!(self, FunctionVariant::Verification(..))
+    }
+}
+
+/// The variant for regular verification.
+pub const REGULAR_VERIFICATION_VARIANT: &str = "";
+
 impl std::fmt::Display for FunctionVariant {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         use FunctionVariant::*;
         match self {
             Baseline => write!(f, "baseline"),
-            Verification => write!(f, "verification"),
+            Verification(s) => {
+                if s.is_empty() {
+                    write!(f, "verification")
+                } else {
+                    write!(f, "verification[{}]", s)
+                }
+            }
         }
     }
 }
@@ -126,23 +142,6 @@ impl FunctionTargetsHolder {
         FunctionTarget::new(func_env, &data)
     }
 
-    /// Gets the function target from the variant which owns the annotations.
-    /// TODO(refactoring): the need for this function should be removed once refactoring
-    ///    finishes and old boilerplate can be removed.
-    pub fn get_annotated_target<'env>(
-        &'env self,
-        func_env: &'env FunctionEnv<'env>,
-    ) -> FunctionTarget<'env> {
-        if self
-            .get_target_variants(func_env)
-            .contains(&FunctionVariant::Verification)
-        {
-            self.get_target(func_env, FunctionVariant::Verification)
-        } else {
-            self.get_target(func_env, FunctionVariant::Baseline)
-        }
-    }
-
     /// Gets all available variants for function.
     pub fn get_target_variants(&self, func_env: &FunctionEnv<'_>) -> Vec<FunctionVariant> {
         self.targets

language/move-prover/bytecode/src/global_invariant_instrumentation.rs

@@ -9,7 +9,7 @@ use log::{debug, info, log, warn};
 use crate::{
     function_data_builder::FunctionDataBuilder,
     function_target::FunctionData,
-    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
+    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
     options::ProverOptions,
     stackless_bytecode::{BorrowNode, Bytecode, Operation, PropKind},
     usage_analysis,
@@ -45,7 +45,7 @@ impl FunctionTargetProcessor for GlobalInvariantInstrumentationProcessor {
             // Nothing to do.
             return data;
         }
-        if data.variant != FunctionVariant::Verification && !fun_env.has_friend() {
+        if !data.variant.is_verified() && !fun_env.has_friend() {
             // Only need to instrument if this is a verification variant, or if the
             // function has a friend and is verified in the friends context.
             return data;
@@ -103,7 +103,7 @@ impl<'a> Instrumenter<'a> {
         let old_code = std::mem::take(&mut self.builder.data.code);
 
         // Emit entrypoint assumptions if this is a verification entry.
-        let assumed_at_update = if self.builder.data.variant == FunctionVariant::Verification {
+        let assumed_at_update = if self.builder.data.variant.is_verified() {
             self.instrument_entrypoint()
         } else {
             BTreeSet::new()

language/move-prover/bytecode/src/global_invariant_instrumentation_v2.rs

@@ -9,7 +9,7 @@ use log::{debug, info, log, warn};
 use crate::{
     function_data_builder::FunctionDataBuilder,
     function_target::FunctionData,
-    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
+    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
     options::ProverOptions,
     stackless_bytecode::{BorrowNode, Bytecode, Operation, PropKind},
     usage_analysis,
@@ -45,7 +45,7 @@ impl FunctionTargetProcessor for GlobalInvariantInstrumentationProcessorV2 {
             // Nothing to do.
             return data;
         }
-        if data.variant != FunctionVariant::Verification && !fun_env.has_friend() {
+        if !data.variant.is_verified() && !fun_env.has_friend() {
             // Only need to instrument if this is a verification variant, or if the
             // function has a friend and is verified in the friends context.
             return data;
@@ -103,7 +103,7 @@ impl<'a> Instrumenter<'a> {
         let old_code = std::mem::take(&mut self.builder.data.code);
 
         // Emit entrypoint assumptions if this is a verification entry.
-        let assumed_at_update = if self.builder.data.variant == FunctionVariant::Verification {
+        let assumed_at_update = if self.builder.data.variant.is_verified() {
             self.instrument_entrypoint()
         } else {
             BTreeSet::new()