1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

// Copyright (c) The Diem Core Contributors
// Copyright (c) The Move Contributors
// SPDX-License-Identifier: Apache-2.0

use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::{fmt, str::FromStr};

use move_binary_format::file_format::CodeOffset;

use crate::{
    ast::Spec,
    model::{FunId, GlobalEnv, ModuleId, QualifiedId},
};

mod pass;
mod pass_inline;

pub use pass::SpecRewriter;
use pass_inline::SpecPassInline;

/// Available simplifications passes to run after tbe model is built
#[derive(Clone, Debug, Serialize, Deserialize)]
pub enum SimplificationPass {
    Inline,
}

impl FromStr for SimplificationPass {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        let r = match s {
            "inline" => SimplificationPass::Inline,
            _ => return Err(s.to_string()),
        };
        Ok(r)
    }
}

impl fmt::Display for SimplificationPass {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Inline => write!(f, "inline"),
        }
    }
}

/// A rewriter pipeline that is composed of a chain of spec rewriters. Note that this composite
/// rewriter is also a spec rewriter.
pub struct SpecRewriterPipeline {
    rewriters: Vec<Box<dyn SpecRewriter>>,
}

impl SpecRewriterPipeline {
    /// Construct a pipeline rewriter by a list of passes
    pub fn new(pipeline: &[SimplificationPass]) -> Self {
        let mut result = Self { rewriters: vec![] };
        for entry in pipeline {
            match entry {
                SimplificationPass::Inline => {
                    result.rewriters.push(Box::new(SpecPassInline::default()))
                }
            }
        }
        result
    }
}

impl SpecRewriter for SpecRewriterPipeline {
    fn rewrite_module_spec(
        &mut self,
        env: &GlobalEnv,
        module_id: ModuleId,
        spec: &Spec,
    ) -> Result<Option<Spec>> {
        let mut current_spec = None;
        for rewriter in self.rewriters.iter_mut() {
            if let Some(new_spec) = rewriter.rewrite_module_spec(
                env,
                module_id,
                current_spec.as_ref().unwrap_or(spec),
            )? {
                current_spec = Some(new_spec);
            }
        }
        Ok(current_spec)
    }

    fn rewrite_function_spec(
        &mut self,
        env: &GlobalEnv,
        fun_id: QualifiedId<FunId>,
        spec: &Spec,
    ) -> Result<Option<Spec>> {
        let mut current_spec = None;
        for rewriter in self.rewriters.iter_mut() {
            if let Some(new_spec) = rewriter.rewrite_function_spec(
                env,
                fun_id,
                current_spec.as_ref().unwrap_or(spec),
            )? {
                current_spec = Some(new_spec);
            }
        }
        Ok(current_spec)
    }

    fn rewrite_inline_spec(
        &mut self,
        env: &GlobalEnv,
        fun_id: QualifiedId<FunId>,
        code_offset: CodeOffset,
        spec: &Spec,
    ) -> Result<Option<Spec>> {
        let mut current_spec = None;
        for rewriter in self.rewriters.iter_mut() {
            if let Some(new_spec) = rewriter.rewrite_inline_spec(
                env,
                fun_id,
                code_offset,
                current_spec.as_ref().unwrap_or(spec),
            )? {
                current_spec = Some(new_spec);
            }
        }
        Ok(current_spec)
    }
}