[compiler-v2] Making v2 the basis of the prover (step #1)

This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following:

- There are two new env processors, the spec_checker and the spec_rewriter:
    - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain.
    - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself.
- Inlining has been extended to deal with specification constructs.
- To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it.
- A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2.
- Multiple test cases have been added.
- The prover driver has been adapted to use the new components.

Author: wrwg

Cargo.lock

@@ -6,11 +6,14 @@
 
 // TODO: move all other `&mut GlobalEnv` processors into this module.
 
-use log::debug;
+use log::trace;
 use move_model::model::GlobalEnv;
 use std::io::Write;
 
 pub mod lambda_lifter;
+pub mod rewrite_target;
+pub mod spec_checker;
+pub mod spec_rewriter;
 
 /// Represents a pipeline of processors working on the global environment.
 #[derive(Default)]
@@ -32,10 +35,10 @@ impl<'a> EnvProcessorPipeline<'a> {
     /// Runs the pipeline. Running will be ended if any of the steps produces an error.
     /// The function returns true if all steps succeeded without errors.
     pub fn run(&self, env: &mut GlobalEnv) -> bool {
-        debug!("before env processor pipeline: {}", env.dump_env());
+        trace!("before env processor pipeline: {}", env.dump_env());
         for (name, proc) in &self.processors {
             proc(env);
-            debug!("after env processor {}", name);
+            trace!("after env processor {}", name);
             if env.has_errors() {
                 return false;
             }
@@ -47,13 +50,13 @@ impl<'a> EnvProcessorPipeline<'a> {
     /// only.
     pub fn run_and_record(&self, env: &mut GlobalEnv, w: &mut impl Write) -> anyhow::Result<bool> {
         let msg = format!("before env processor pipeline:\n{}\n", env.dump_env());
-        debug!("{}", msg);
+        trace!("{}", msg);
         writeln!(w, "// -- Model dump {}", msg)?;
         for (name, proc) in &self.processors {
             proc(env);
             if !env.has_errors() {
                 let msg = format!("after env processor {}:\n{}\n", name, env.dump_env());
-                debug!("{}", msg);
+                trace!("{}", msg);
                 writeln!(w, "// -- Model dump {}", msg)?;
             } else {
                 return Ok(false);

third_party/move/move-compiler-v2/src/env_pipeline/mod.rs

@@ -0,0 +1,197 @@
+// Copyright © Aptos Foundation
+// SPDX-License-Identifier: Apache-2.0
+
+use move_model::{
+    ast::{Exp, Spec, SpecBlockTarget},
+    model::{FunId, GlobalEnv, NodeId, QualifiedId, SpecFunId},
+};
+use std::{
+    collections::{BTreeMap, BTreeSet},
+    mem,
+};
+
+/// Represents a target for rewriting.
+#[derive(Debug, PartialOrd, Ord, PartialEq, Eq, Clone)]
+pub enum RewriteTarget {
+    MoveFun(QualifiedId<FunId>),
+    SpecFun(QualifiedId<SpecFunId>),
+    SpecBlock(SpecBlockTarget),
+}
+
+/// Represents the state of a rewriting target.
+#[derive(Debug, Clone, Eq, PartialEq)]
+pub enum RewriteState {
+    Unchanged,
+    Def(Exp),
+    Spec(Spec),
+    Abstract,
+}
+
+/// Scope for collecting targets.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Ord, PartialOrd)]
+pub enum RewritingScope {
+    CompilationTarget,
+    Everything,
+}
+
+/// Represents a set of rewriting targets in the given state.
+#[derive(Clone)]
+pub struct RewriteTargets {
+    pub targets: BTreeMap<RewriteTarget, RewriteState>,
+}
+
+impl RewriteTargets {
+    /// Create a new set of rewrite targets, collecting them as specified by `scope`.
+    /// Those targets are initially associated with `Unchanged` state.
+    pub fn create(env: &GlobalEnv, scope: RewritingScope) -> Self {
+        let mut targets = vec![];
+        let add_spec =
+            |targets: &mut Vec<RewriteTarget>, sb_target: SpecBlockTarget, spec: &Spec| {
+                if !spec.is_empty() {
+                    targets.push(RewriteTarget::SpecBlock(sb_target))
+                }
+            };
+        for module in env.get_modules() {
+            if scope == RewritingScope::Everything || module.is_target() {
+                for func in module.get_functions() {
+                    let id = func.get_qualified_id();
+                    targets.push(RewriteTarget::MoveFun(id));
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Function(id.module_id, id.id),
+                        &func.get_spec(),
+                    );
+                }
+                for (spec_fun_id, _) in module.get_spec_funs() {
+                    targets.push(RewriteTarget::SpecFun(
+                        module.get_id().qualified(*spec_fun_id),
+                    ));
+                }
+                for struct_env in module.get_structs() {
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Struct(module.get_id(), struct_env.get_id()),
+                        &struct_env.get_spec(),
+                    )
+                }
+                if !module.get_spec().is_empty() {
+                    add_spec(
+                        &mut targets,
+                        SpecBlockTarget::Module(module.get_id()),
+                        &module.get_spec(),
+                    );
+                }
+            }
+        }
+        Self {
+            targets: targets
+                .into_iter()
+                .map(|target| (target, RewriteState::Unchanged))
+                .collect(),
+        }
+    }
+
+    /// Filters the targets according to the predicate.
+    pub fn filter(&mut self, pred: impl Fn(&RewriteTarget, &RewriteState) -> bool) {
+        self.targets = mem::take(&mut self.targets)
+            .into_iter()
+            .filter(|(t, s)| pred(t, s))
+            .collect();
+    }
+
+    /// Iterates all targets.
+    pub fn iter(&self) -> impl Iterator<Item = (&RewriteTarget, &RewriteState)> + '_ {
+        self.targets.iter()
+    }
+
+    /// Returns an iteration of the target keys.
+    pub fn keys(&self) -> impl Iterator<Item = RewriteTarget> + '_ {
+        self.targets.keys().cloned()
+    }
+
+    /// Adds a new rewrite target in state `Unchanged` if it doesn't exist yet. Returns
+    /// a boolean whether the entry is new and a mutable reference to the state.
+    pub fn entry(&mut self, target: RewriteTarget) -> (bool, &mut RewriteState) {
+        let mut is_new = false;
+        let state = self.targets.entry(target).or_insert_with(|| {
+            is_new = true;
+            RewriteState::Unchanged
+        });
+        (is_new, state)
+    }
+
+    /// Gets the current state of the target.
+    pub fn state(&self, target: &RewriteTarget) -> &RewriteState {
+        self.targets.get(target).expect("state defined")
+    }
+
+    /// Gets the mutable current state of the target.
+    pub fn state_mut(&mut self, target: &RewriteTarget) -> &mut RewriteState {
+        self.targets.get_mut(target).expect("state defined")
+    }
+
+    /// Updates the global env based on the current state. This consumes
+    /// the rewrite targets.
+    pub fn write_to_env(self, env: &mut GlobalEnv) {
+        for (target, state) in self.targets {
+            use RewriteState::*;
+            use RewriteTarget::*;
+            match (target, state) {
+                (_, Unchanged) => {},
+                (MoveFun(fnid), Def(def)) => env.set_function_def(fnid, def),
+                (SpecFun(fnid), Def(def)) => env.get_spec_fun_mut(fnid).body = Some(def),
+                (SpecBlock(sb_target), Spec(spec)) => {
+                    *env.get_spec_block_mut(&sb_target) = spec;
+                },
+                _ => panic!("unexpected rewrite target and result combination"),
+            }
+        }
+    }
+}
+
+impl RewriteTarget {
+    /// Gets the call sites for the target.
+    pub fn called_funs_with_call_sites(
+        &self,
+        env: &GlobalEnv,
+    ) -> BTreeMap<QualifiedId<FunId>, BTreeSet<NodeId>> {
+        use RewriteTarget::*;
+        match self {
+            MoveFun(id) => env
+                .get_function(*id)
+                .get_def()
+                .map(|e| e.called_funs_with_callsites())
+                .unwrap_or_default(),
+            SpecFun(id) => env
+                .get_spec_fun(*id)
+                .body
+                .as_ref()
+                .map(|e| e.called_funs_with_callsites())
+                .unwrap_or_default(),
+            SpecBlock(target) => {
+                let spec = env.get_spec_block(target);
+                spec.called_funs_with_callsites()
+            },
+        }
+    }
+
+    /// Get the environment state of this target in form of a RewriteState.
+    pub fn get_env_state(&self, env: &GlobalEnv) -> RewriteState {
+        use RewriteState::*;
+        use RewriteTarget::*;
+        match self {
+            MoveFun(fid) => env
+                .get_function(*fid)
+                .get_def()
+                .map(|e| Def(e.clone()))
+                .unwrap_or(Abstract),
+            SpecFun(fid) => env
+                .get_spec_fun(*fid)
+                .body
+                .clone()
+                .map(Def)
+                .unwrap_or(Abstract),
+            SpecBlock(sb_target) => Spec(env.get_spec_block(sb_target).clone()),
+        }
+    }
+}

third_party/move/move-compiler-v2/src/env_pipeline/rewrite_target.rs

@@ -0,0 +1,128 @@
+// Copyright © Aptos Foundation
+// SPDX-License-Identifier: Apache-2.0
+
+//! The spec checker runs over the specifications of the target modules:
+//!
+//! - It checks whether the constructs they use are pure. If a specification
+//!   expression calls a Move function it checks that for pureness as well.
+//! - It checks whether struct invariants do not depend on global state.
+
+use crate::env_pipeline::rewrite_target::{
+    RewriteState, RewriteTarget, RewriteTargets, RewritingScope,
+};
+use codespan_reporting::diagnostic::Severity;
+use log::info;
+use move_model::{
+    ast::{Exp, Spec},
+    model::{FunId, GlobalEnv, NodeId, QualifiedId},
+    pureness_checker::{FunctionPurenessChecker, FunctionPurenessCheckerMode},
+};
+
+pub fn run_spec_checker(env: &GlobalEnv) {
+    info!("checking specifications");
+
+    // Targets are all spec functions and spec blocks, as well as functions to
+    // process inline specs.
+    let mut targets = RewriteTargets::create(env, RewritingScope::CompilationTarget);
+    targets.filter(|target, _| {
+        matches!(
+            target,
+            RewriteTarget::SpecFun(_) | RewriteTarget::SpecBlock(_) | RewriteTarget::MoveFun(_)
+        )
+    });
+
+    // Walk over those targets and check them for pureness.
+    for target in targets.keys() {
+        match (target.clone(), target.get_env_state(env)) {
+            (RewriteTarget::MoveFun(_), RewriteState::Def(exp)) => {
+                exp.visit_inline_specs(&mut |s| {
+                    check_spec(env, s);
+                    true
+                })
+            },
+            (RewriteTarget::SpecFun(_), RewriteState::Def(exp)) => check_exp(env, &exp),
+            (RewriteTarget::SpecBlock(_), RewriteState::Spec(spec)) => check_spec(env, &spec),
+            _ => {},
+        }
+    }
+}
+
+fn check_exp(env: &GlobalEnv, exp: &Exp) {
+    let mut error_reported = false;
+    let mut checker = FunctionPurenessChecker::new(
+        FunctionPurenessCheckerMode::Specification,
+        |node_id, msg, call_chain| report_error(env, &mut error_reported, node_id, msg, call_chain),
+    );
+    checker.check_exp(env, exp);
+}
+
+fn check_spec(env: &GlobalEnv, spec: &Spec) {
+    let mut error_reported = false;
+    let mut checker = FunctionPurenessChecker::new(
+        FunctionPurenessCheckerMode::Specification,
+        |node_id, msg, call_chain| report_error(env, &mut error_reported, node_id, msg, call_chain),
+    );
+    checker.check_spec(env, spec);
+}
+
+fn report_error(
+    env: &GlobalEnv,
+    error_reported: &mut bool,
+    id: NodeId,
+    msg: &str,
+    call_chain: &[(QualifiedId<FunId>, NodeId)],
+) {
+    // We report the first error only because otherwise the error messages can be
+    // overwhelming, if the user e.g. accidentally calls a complex system function.
+    if *error_reported {
+        return;
+    }
+    // The first call in call_chain is the one from the specification function to
+    // a Move function. We take this as the primary anchor for the error message
+    let print_fun = |f: QualifiedId<FunId>| env.get_function(f).get_name_str();
+    if call_chain.is_empty() {
+        // Direct report
+        env.diag_with_primary_and_labels(
+            Severity::Error,
+            &env.get_node_loc(id),
+            "specification expression cannot use impure construct",
+            msg,
+            vec![],
+        );
+    } else {
+        let (first_fun, first_id) = call_chain[0];
+        let mut call_chain_info = vec![];
+        // First print the sequence of calls leading us to the issue
+        for i in 1..call_chain.len() {
+            let previous_fun = print_fun(call_chain[i - 1].0);
+            let this_fun = print_fun(call_chain[1].0);
+            let this_loc = env.get_node_loc(call_chain[1].1);
+            call_chain_info.push((
+                this_loc,
+                format!(
+                    "transitively calling `{}` from `{}` here",
+                    this_fun, previous_fun
+                ),
+            ))
+        }
+        // Next print the particular issue detected
+        let last_fun = call_chain.last().unwrap().0;
+        call_chain_info.push((
+            env.get_node_loc(id),
+            format!("in `{}`: {}", print_fun(last_fun), msg),
+        ));
+
+        env.diag_with_primary_and_labels(
+            Severity::Error,
+            &env.get_node_loc(first_id),
+            &format!(
+                "specification expression cannot call impure \
+            Move function `{}`",
+                env.get_function(first_fun).get_name_str()
+            ),
+            "called here",
+            call_chain_info,
+        );
+    }
+    *error_reported = true;
+}