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

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::fmt::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,196 @@
+// 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();
+    }
+
+    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;
+}