[move-prover][spec-flatten] convert the tool into a pipeline architec…

…ture

In the new architecture, each pass (e.g., triming, inlining, arithmetic
simplification, etc) will be pipelined by specifing the `-p` cli option.

Each pass might be executed multiple times by reapting `-p` for the pass
multiple times in the CLI.

language/move-prover/tools/spec-flatten/src/exp_inlining.rs

@@ -0,0 +1,17 @@
+// Copyright (c) The Diem Core Contributors
+// SPDX-License-Identifier: Apache-2.0
+
+use anyhow::Result;
+
+use bytecode::function_target::FunctionTarget;
+use move_model::ast::Spec;
+
+use crate::workflow::WorkflowOptions;
+
+pub(crate) fn inline_all_exp_in_spec(
+    _options: &WorkflowOptions,
+    _target: FunctionTarget,
+    spec: Spec,
+) -> Result<Spec> {
+    Ok(spec)
+}

language/move-prover/tools/spec-flatten/src/flatten.rs → language/move-prover/tools/spec-flatten/src/exp_trimming.rs

@@ -4,42 +4,25 @@
 use anyhow::Result;
 use std::collections::BTreeMap;
 
-use bytecode::{function_target::FunctionTarget, function_target_pipeline::FunctionTargetsHolder};
+use bytecode::function_target::FunctionTarget;
 use move_model::{
     ast::{ConditionKind, Spec},
     model::{FunId, QualifiedId},
 };
 
-use crate::{
-    options::FlattenOptions,
-    workflow::{prepare_with_override, prove},
-};
+use crate::workflow::{prepare_with_override, prove, WorkflowOptions};
 
-pub(crate) fn flatten_spec<'env>(
-    options: &FlattenOptions,
-    fun_target: FunctionTarget<'env>,
-    _targets: &'env FunctionTargetsHolder,
+pub(crate) fn trim_aborts_ifs(
+    options: &WorkflowOptions,
+    target: FunctionTarget,
+    spec: Spec,
 ) -> Result<Spec> {
-    let fun_env = fun_target.func_env;
+    let fun_env = target.func_env;
     let mut fun_options = options.clone();
     fun_options.target = Some(fun_env.get_simple_name_string().to_string());
 
-    let spec = fun_target.get_spec();
-    let new_spec = remove_redundant_aborts_ifs_since(
-        &fun_options,
-        fun_env.get_qualified_id(),
-        spec.clone(),
-        0,
-    )?;
-
-    if fun_options.verbose {
-        println!("fun {}", fun_env.get_full_name_str());
-        println!(
-            "  Number of aborts_if trimmed: {} (out of {})",
-            spec.conditions.len() - new_spec.conditions.len(),
-            spec.conditions.len(),
-        );
-    }
+    let new_spec =
+        remove_redundant_aborts_ifs_since(&fun_options, fun_env.get_qualified_id(), spec, 0)?;
     Ok(new_spec)
 }
 
@@ -71,7 +54,7 @@ fn remove_first_aborts_if_since(spec: &Spec, pos: usize) -> (Spec, bool) {
 }
 
 fn remove_first_aborts_if_and_prove_since(
-    options: &FlattenOptions,
+    options: &WorkflowOptions,
     fun_id: QualifiedId<FunId>,
     spec: &Spec,
     pos: usize,
@@ -89,7 +72,7 @@ fn remove_first_aborts_if_and_prove_since(
 }
 
 fn remove_redundant_aborts_ifs_since(
-    options: &FlattenOptions,
+    options: &WorkflowOptions,
     fun_id: QualifiedId<FunId>,
     spec: Spec,
     pos: usize,

language/move-prover/tools/spec-flatten/src/lib.rs

@@ -2,34 +2,74 @@
 // SPDX-License-Identifier: Apache-2.0
 
 use anyhow::{anyhow, Result};
-use std::collections::BTreeMap;
+use std::{collections::BTreeMap, str::FromStr};
+use structopt::StructOpt;
 
 use bytecode::function_target_pipeline::{FunctionVariant, VerificationFlavor};
 use move_model::ast::SpecBlockTarget;
 
 mod ast_print;
-mod flatten;
-mod options;
 mod workflow;
 
-pub use ast_print::SpecPrinter;
-pub use options::FlattenOptions;
+// spec simplification pass
+mod exp_inlining;
+mod exp_trimming;
+
+use ast_print::SpecPrinter;
+use workflow::WorkflowOptions;
+
+/// List of simplification passes available
+#[derive(Clone, Debug)]
+pub enum SimplificationPass {
+    Inline,
+    TrimAbortsIf,
+}
+
+impl FromStr for SimplificationPass {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        let r = match s {
+            "inline" => SimplificationPass::Inline,
+            "trim_aborts_if" => SimplificationPass::TrimAbortsIf,
+            _ => return Err(s.to_string()),
+        };
+        Ok(r)
+    }
+}
+
+/// Options passed into the specification flattening tool.
+#[derive(StructOpt, Clone)]
+pub struct FlattenOptions {
+    /// Options common and shared by the proving workflow and all passes
+    #[structopt(flatten)]
+    pub workflow: WorkflowOptions,
+
+    /// Simplification processing pipeline
+    #[structopt(short, long)]
+    pub pipeline: Vec<SimplificationPass>,
+
+    /// Dump stepwise result
+    #[structopt(long)]
+    pub dump: bool,
+}
 
 //**************************************************************************************************
 // Entrypoint
 //**************************************************************************************************
 
 pub fn run(options: &FlattenOptions) -> Result<()> {
-    let (env, targets) = workflow::prepare(options)?;
+    let workflow_options = &options.workflow;
+    let (env, targets) = workflow::prepare(workflow_options)?;
 
     // make sure the original verification works
-    let proved = workflow::prove(options, &env, &targets)?;
+    let proved = workflow::prove(workflow_options, &env, &targets)?;
     if !proved {
         return Err(anyhow!("Original proof is not successful"));
     }
 
     // flatten spec in target modules
-    let mut flattened_specs = BTreeMap::new();
+    let mut simplified_specs = BTreeMap::new();
     for (fun_id, variant) in targets.get_funs_and_variants() {
         if !matches!(
             variant,
@@ -44,7 +84,7 @@ pub fn run(options: &FlattenOptions) -> Result<()> {
             // only run on specs in target module
             continue;
         }
-        match &options.target {
+        match &workflow_options.target {
             None => {
                 if !fun_env.has_unknown_callers() {
                     // only run on specs for external-facing functions
@@ -59,13 +99,50 @@ pub fn run(options: &FlattenOptions) -> Result<()> {
             }
         }
 
-        let target = targets.get_target(&fun_env, &variant);
-        let new_spec = flatten::flatten_spec(options, target, &targets)?;
-        flattened_specs.insert(fun_id, new_spec);
+        // get a copy of the original spec
+        let fun_target = targets.get_target(&fun_env, &variant);
+        let mut fun_spec = Some(fun_target.get_spec().clone());
+
+        // prepare for stepwise result printing
+        let fun_scope = SpecBlockTarget::Function(fun_id.module_id, fun_id.id);
+        let printer = SpecPrinter::new(&env, &fun_scope);
+        if options.dump {
+            println!(
+                "================ fun {} ================",
+                fun_env.get_full_name_str()
+            );
+        }
+
+        // pass the spec through the simplification pipeline
+        for (i, pass) in options.pipeline.iter().enumerate() {
+            let target = fun_target.clone();
+            let old_spec = fun_spec.take().unwrap();
+            let new_spec = match pass {
+                SimplificationPass::Inline => {
+                    exp_inlining::inline_all_exp_in_spec(workflow_options, target, old_spec)
+                }
+                SimplificationPass::TrimAbortsIf => {
+                    exp_trimming::trim_aborts_ifs(workflow_options, target, old_spec)
+                }
+            }?;
+
+            // dump stepwise results if requested
+            if options.dump {
+                println!("step {} - {:?} {{", i, pass);
+                for cond in &new_spec.conditions {
+                    println!("\t{}", SpecPrinter::convert(printer.print_condition(cond)));
+                }
+                println!("}}");
+            }
+
+            fun_spec = Some(new_spec);
+        }
+
+        simplified_specs.insert(fun_id, fun_spec.unwrap());
     }
 
-    // dump the result
-    for (fun_id, spec) in flattened_specs {
+    // dump the final result
+    for (fun_id, spec) in simplified_specs {
         let fun_env = env.get_function(fun_id);
         let fun_scope = SpecBlockTarget::Function(fun_id.module_id, fun_id.id);
         let printer = SpecPrinter::new(&env, &fun_scope);

language/move-prover/tools/spec-flatten/src/workflow.rs

@@ -3,12 +3,13 @@
 
 use anyhow::{anyhow, Result};
 use std::collections::BTreeMap;
+use structopt::StructOpt;
 
 use bytecode::{
     function_target_pipeline::FunctionTargetsHolder, options::ProverOptions,
     pipeline_factory::default_pipeline_with_options,
 };
-use move_lang::shared::NumericalAddress;
+use move_lang::shared::{parse_named_address, NumericalAddress};
 use move_model::{
     ast::Spec,
     model::{FunId, GlobalEnv, QualifiedId, VerificationScope},
@@ -17,14 +18,39 @@ use move_model::{
 };
 use move_prover::{cli::Options as CliOptions, generate_boogie, verify_boogie};
 
-use crate::options::FlattenOptions;
+/// Options passed into the workflow pipeline.
+#[derive(StructOpt, Clone)]
+pub struct WorkflowOptions {
+    /// Sources of the target modules
+    pub srcs: Vec<String>,
 
-pub(crate) fn prepare(options: &FlattenOptions) -> Result<(GlobalEnv, FunctionTargetsHolder)> {
+    /// Dependencies
+    #[structopt(short = "d", long = "dependency")]
+    pub deps: Vec<String>,
+
+    /// Target function
+    #[structopt(short, long)]
+    pub target: Option<String>,
+
+    /// Do not include default named address
+    #[structopt(long = "no-default-named-addresses")]
+    pub no_default_named_addresses: bool,
+
+    /// Extra mappings for named address
+    #[structopt(short = "a", long = "address", parse(try_from_str = parse_named_address))]
+    pub named_addresses_extra: Option<Vec<(String, NumericalAddress)>>,
+
+    /// Verbose mode
+    #[structopt(short, long)]
+    pub verbose: bool,
+}
+
+pub(crate) fn prepare(options: &WorkflowOptions) -> Result<(GlobalEnv, FunctionTargetsHolder)> {
     prepare_with_override(options, BTreeMap::new())
 }
 
 pub(crate) fn prepare_with_override(
-    options: &FlattenOptions,
+    options: &WorkflowOptions,
     spec_override: BTreeMap<QualifiedId<FunId>, Spec>,
 ) -> Result<(GlobalEnv, FunctionTargetsHolder)> {
     // build mapping for named addresses
@@ -96,7 +122,7 @@ pub(crate) fn prepare_with_override(
 }
 
 pub(crate) fn prove(
-    options: &FlattenOptions,
+    options: &WorkflowOptions,
     env: &GlobalEnv,
     targets: &FunctionTargetsHolder,
 ) -> Result<bool> {
@@ -115,7 +141,7 @@ pub(crate) fn prove(
 // utilities
 //
 
-fn get_prover_options(options: &FlattenOptions) -> ProverOptions {
+fn get_prover_options(options: &WorkflowOptions) -> ProverOptions {
     let verify_scope = match &options.target {
         None => VerificationScope::All,
         Some(target) => VerificationScope::Only(target.clone()),
@@ -126,7 +152,7 @@ fn get_prover_options(options: &FlattenOptions) -> ProverOptions {
     }
 }
 
-fn get_cli_options(options: &FlattenOptions) -> CliOptions {
+fn get_cli_options(options: &WorkflowOptions) -> CliOptions {
     CliOptions {
         move_sources: options.srcs.clone(),
         move_deps: options.deps.clone(),