[move-prover] Preparation for new invariant handling

More general global invariant processing, dealing with opaque
functions and temporarily disabled invariants.

This is a first simple step.
* Added flag --inv_v2 to enable new processing (false by default).
* Added pragmas disable_invariant_in_body (allows invariant not to hold
  in the body of a function)
* Added pragma delegate_invariant_to_caller (says that invariant does
  not necessarily hold when this function is called, and does not need
  to be proved in the function).
* Added regular expression to find declarations of friend modules to
  identify a superset of all modules that we need to process
* Created a version 2 of global_invariant_instrumentation.  When --inv_v2
  is set, GlobalInvariantProcessorV2 is added to the pipeline.

Closes: aptos-labs#7747

language/move-model/src/model.rs

@@ -59,8 +59,10 @@ use crate::{
         ConditionKind, Exp, GlobalInvariant, ModuleName, PropertyBag, PropertyValue, Spec,
         SpecBlockInfo, SpecFunDecl, SpecVarDecl, Value,
     },
-    pragmas::{FRIEND_PRAGMA, INTRINSIC_PRAGMA, OPAQUE_PRAGMA, VERIFY_PRAGMA,
-              DISABLE_INVARIANTS_IN_BODY_PRAGMA, DELEGATE_INVARIANTS_TO_CALLER_PRAGMA},
+    pragmas::{
+        DELEGATE_INVARIANTS_TO_CALLER_PRAGMA, DISABLE_INVARIANTS_IN_BODY_PRAGMA, FRIEND_PRAGMA,
+        INTRINSIC_PRAGMA, OPAQUE_PRAGMA, VERIFY_PRAGMA,
+    },
     symbol::{Symbol, SymbolPool},
     ty::{PrimitiveType, Type},
 };
@@ -2371,7 +2373,6 @@ impl<'env> FunctionEnv<'env> {
         self.is_pragma_true(DELEGATE_INVARIANTS_TO_CALLER_PRAGMA, || false)
     }
 
-
     /// Returns true if this function mutates any references (i.e. has &mut parameters).
     pub fn is_mutating(&self) -> bool {
         self.get_parameters()

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

@@ -0,0 +1,272 @@
+// Copyright (c) The Diem Core Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+// Transformation which injects global invariants into the bytecode.
+
+#[allow(unused_imports)]
+use log::{debug, info, log, warn};
+
+use crate::{
+    function_data_builder::FunctionDataBuilder,
+    function_target::FunctionData,
+    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
+    options::{ProverOptions, PROVER_DEFAULT_OPTIONS},
+    stackless_bytecode::{BorrowNode, Bytecode, Operation, PropKind},
+    usage_analysis,
+};
+
+use crate::spec_translator::SpecTranslator;
+
+use move_model::{
+    ast::{ConditionKind, GlobalInvariant},
+    model::{FunctionEnv, GlobalEnv, GlobalId, QualifiedId, StructId},
+    pragmas::CONDITION_ISOLATED_PROP,
+};
+use std::collections::BTreeSet;
+
+const GLOBAL_INVARIANT_FAILS_MESSAGE: &str = "global memory invariant does not hold";
+
+pub struct GlobalInvariantInstrumentationProcessorV2 {}
+
+impl GlobalInvariantInstrumentationProcessorV2 {
+    pub fn new() -> Box<Self> {
+        Box::new(Self {})
+    }
+}
+
+impl FunctionTargetProcessor for GlobalInvariantInstrumentationProcessorV2 {
+    fn process(
+        &self,
+        _targets: &mut FunctionTargetsHolder,
+        fun_env: &FunctionEnv<'_>,
+        data: FunctionData,
+    ) -> FunctionData {
+        if fun_env.is_native() || fun_env.is_intrinsic() {
+            // Nothing to do.
+            return data;
+        }
+        if data.variant != FunctionVariant::Verification && !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;
+        }
+
+        let options = fun_env
+            .module_env
+            .env
+            .get_extension::<ProverOptions>()
+            .unwrap_or_else(|| &*PROVER_DEFAULT_OPTIONS);
+
+        Instrumenter::run(options, fun_env, data)
+    }
+
+    fn name(&self) -> String {
+        "global_invariant_instrumenter_v2".to_string()
+    }
+
+    fn initialize(&self, _env: &GlobalEnv, _targets: &mut FunctionTargetsHolder) {
+        // This function can be used to compute any needed information ahead
+        // of the time `process` is called for each individual function.
+        //
+        // In order to iterate over all functions in targets, one can use code as below:
+        //
+        //   let mut analysis_info = AnalysisInfo::new();
+        //   for (qfun_id, variant) in targets.get_funs_and_variants() {
+        //       let fun_env = env.get_module(qfun_id.module_id).into_function(qfun_id.id);
+        //       let fun_target = targets.get_target(&fun_env, variant);
+        //       << Do something with fun_env/fun_target >>
+        //   }
+        //   // Store the computed info into an extension in the environment
+        //   env.set_extension(analysis_info);
+        //
+        // One can then use in `process` the following to retrieve the analysis result.
+        //
+        //   let analysis_info = env.get_extension::<AnalysisInfo>();
+        //   ...
+    }
+}
+
+struct Instrumenter<'a> {
+    _options: &'a ProverOptions,
+    builder: FunctionDataBuilder<'a>,
+}
+
+impl<'a> Instrumenter<'a> {
+    fn run(
+        options: &'a ProverOptions,
+        fun_env: &FunctionEnv<'a>,
+        data: FunctionData,
+    ) -> FunctionData {
+        let builder = FunctionDataBuilder::new(fun_env, data);
+        let mut instrumenter = Instrumenter {
+            _options: options,
+            builder,
+        };
+        instrumenter.instrument();
+        instrumenter.builder.data
+    }
+
+    fn instrument(&mut self) {
+        // Extract and clear current code
+        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 {
+            self.instrument_entrypoint()
+        } else {
+            BTreeSet::new()
+        };
+
+        // Generate new instrumented code.
+        for bc in old_code {
+            self.instrument_bytecode(bc, &assumed_at_update);
+        }
+    }
+
+    fn instrument_entrypoint(&mut self) -> BTreeSet<GlobalId> {
+        // Emit an assume of all invariants over memory touched by this function, and which
+        // stem from modules in the dependency graph.
+        //
+        // Also returns the set of invariant ids which are to be assumed before an update
+        // happens instead here at the entrypoint. It is more efficient to emit those assumes
+        // not until they are actually needed. Those invariants include (a) those which are
+        // marked by the user explicitly as `[isolated]` (b) those which are not declared
+        // in dependent modules and from which the code should therefore not depend on, apart
+        // of for the update itself.
+        let env = self.builder.global_env();
+        let mut invariants = BTreeSet::new();
+        let mut invariants_for_modified_memory = BTreeSet::new();
+        for mem in usage_analysis::get_used_memory(&self.builder.get_target()) {
+            invariants.extend(env.get_global_invariants_for_memory(*mem));
+        }
+        for mem in usage_analysis::get_modified_memory(&self.builder.get_target()) {
+            invariants_for_modified_memory.extend(env.get_global_invariants_for_memory(*mem));
+        }
+
+        let mut assumed_at_update = BTreeSet::new();
+        let module_env = &self.builder.fun_env.module_env;
+        let mut translated = SpecTranslator::translate_invariants(
+            &mut self.builder,
+            invariants.iter().filter_map(|id| {
+                env.get_global_invariant(*id).filter(|inv| {
+                    if inv.kind == ConditionKind::Invariant {
+                        if module_env.is_transitive_dependency(inv.declaring_module)
+                            && !module_env
+                                .env
+                                .is_property_true(&inv.properties, CONDITION_ISOLATED_PROP)
+                                .unwrap_or(false)
+                        {
+                            true
+                        } else {
+                            assumed_at_update.insert(*id);
+                            false
+                        }
+                    } else {
+                        false
+                    }
+                })
+            }),
+        );
+        for (loc, _, cond) in std::mem::take(&mut translated.invariants) {
+            self.builder.set_next_debug_comment(format!(
+                "global invariant {}",
+                loc.display(self.builder.global_env())
+            ));
+            self.builder
+                .emit_with(|id| Bytecode::Prop(id, PropKind::Assume, cond));
+        }
+        assumed_at_update
+    }
+
+    fn instrument_bytecode(&mut self, bc: Bytecode, assumed_at_update: &BTreeSet<GlobalId>) {
+        use BorrowNode::*;
+        use Bytecode::*;
+        use Operation::*;
+        match &bc {
+            Call(_, _, WriteBack(GlobalRoot(mem), _), ..) => {
+                self.emit_invariants_for_update(*mem, assumed_at_update, move |builder| {
+                    builder.emit(bc);
+                })
+            }
+            Call(_, _, MoveTo(mid, sid, _), ..) | Call(_, _, MoveFrom(mid, sid, _), ..) => self
+                .emit_invariants_for_update(
+                    mid.qualified(*sid),
+                    assumed_at_update,
+                    move |builder| {
+                        builder.emit(bc);
+                    },
+                ),
+            _ => self.builder.emit(bc),
+        }
+    }
+
+    fn emit_invariants_for_update<F>(
+        &mut self,
+        mem: QualifiedId<StructId>,
+        assumed_at_update: &BTreeSet<GlobalId>,
+        emit_update: F,
+    ) where
+        F: FnOnce(&mut FunctionDataBuilder<'_>),
+    {
+        // Translate the invariants, computing any state to be saved as well. State saves are
+        // necessary for update invariants which contain the `old(..)` expressions.
+        let invariants = self.get_verified_invariants_for_mem(mem);
+        let mut translated =
+            SpecTranslator::translate_invariants(&mut self.builder, invariants.iter().cloned());
+
+        // Emit all necessary state saves for 'update' invariants.
+        self.builder
+            .set_next_debug_comment("state save for global update invariants".to_string());
+        for (mem, label) in std::mem::take(&mut translated.saved_memory) {
+            self.builder
+                .emit_with(|id| Bytecode::SaveMem(id, label, mem));
+        }
+        for (var, label) in std::mem::take(&mut translated.saved_spec_vars) {
+            self.builder
+                .emit_with(|id| Bytecode::SaveSpecVar(id, label, var));
+        }
+        self.builder.clear_next_debug_comment();
+
+        // For all invariants which are assumed at update, emit an assume before the memory update.
+        for (_, _, cond) in translated
+            .invariants
+            .iter()
+            .filter(|(_, id, _)| assumed_at_update.contains(id))
+        {
+            self.builder
+                .emit_with(|id| Bytecode::Prop(id, PropKind::Assume, cond.clone()));
+        }
+
+        // Emit the code which performs the update on `mem`.
+        emit_update(&mut self.builder);
+
+        // Emit assertions of translated invariants.
+        for (loc, _, cond) in std::mem::take(&mut translated.invariants) {
+            self.builder.set_next_debug_comment(format!(
+                "global invariant {}",
+                loc.display(self.builder.global_env())
+            ));
+            self.builder
+                .set_loc_and_vc_info(loc, GLOBAL_INVARIANT_FAILS_MESSAGE);
+            self.builder
+                .emit_with(|id| Bytecode::Prop(id, PropKind::Assert, cond));
+        }
+    }
+
+    /// Returns the invariants which need to be verified if the given memory is updated.
+    /// This filters out those invariants which stem from modules which are not verification
+    /// target.
+    fn get_verified_invariants_for_mem(
+        &self,
+        mem: QualifiedId<StructId>,
+    ) -> Vec<&'a GlobalInvariant> {
+        let env = self.builder.global_env();
+        env.get_global_invariants_for_memory(mem)
+            .iter()
+            .filter_map(|id| {
+                env.get_global_invariant(*id)
+                    .filter(|inv| env.get_module(inv.declaring_module).is_target())
+            })
+            .collect()
+    }
+}

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

@@ -22,6 +22,7 @@ pub mod function_data_builder;
 pub mod function_target;
 pub mod function_target_pipeline;
 pub mod global_invariant_instrumentation;
+pub mod global_invariant_instrumentation_v2;
 pub mod graph;
 pub mod livevar_analysis;
 pub mod loop_analysis;

language/move-prover/bytecode/tests/testsuite.rs

@@ -117,6 +117,7 @@ fn get_tested_transformation_pipeline(
             pipeline.add_processor(DataInvariantInstrumentationProcessor::new());
             Ok(Some(pipeline))
         }
+        // TODO: Make a version for global_invariant_instrumentation_v2?
         "global_invariant_instrumentation" => {
             let mut pipeline = FunctionTargetPipeline::default();
             pipeline.add_processor(EliminateImmRefsProcessor::new());

language/move-prover/src/cli.rs

@@ -63,6 +63,8 @@ pub struct Options {
     pub prover: ProverOptions,
     /// Options for the prover backend.
     pub backend: BoogieOptions,
+    /// Whether to use the v2 invariant scheme.
+    pub inv_v2: bool,
     /// Options for the documentation generator.
     pub docgen: DocgenOptions,
     /// Options for the ABI generator.
@@ -90,6 +92,7 @@ impl Default for Options {
             move_deps: vec![],
             prover: ProverOptions::default(),
             backend: BoogieOptions::default(),
+            inv_v2: false,
             docgen: DocgenOptions::default(),
             abigen: AbigenOptions::default(),
             errmapgen: ErrmapOptions::default(),
@@ -197,6 +200,11 @@ impl Options {
                     .long("v1")
                     .help("whether to use the old v1 translation and backend")
             )
+            .arg(
+                Arg::with_name("inv_v2")
+                    .long("inv_v2")
+                    .help("whether to use the new v2 invariant processing (with disabled invariants)")
+            )
             .arg(
                 Arg::with_name("negative")
                     .long("negative")
@@ -464,6 +472,9 @@ impl Options {
         if matches.is_present("keep") {
             options.backend.keep_artifacts = true;
         }
+        if matches.is_present("inv_v2") {
+            options.inv_v2 = true;
+        }
         if matches.is_present("negative") {
             options.prover.negative_checks = true;
         }