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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164

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

use super::cfg::CFG;
use crate::{diagnostics::Diagnostics, hlir::ast::*};
use std::collections::BTreeMap;

/// Trait for finite-height abstract domains. Infinite height domains would require a more complex
/// trait with widening and a partial order.
pub trait AbstractDomain: Clone + Sized {
    fn join(&mut self, other: &Self) -> JoinResult;
}

#[derive(Debug, PartialEq, Eq, Copy, Clone)]
pub enum JoinResult {
    Unchanged,
    Changed,
}

#[derive(Clone)]
enum BlockPostcondition {
    /// Unprocessed block
    Unprocessed,
    /// Analyzing block was successful
    Success,
    /// Analyzing block ended in an error
    Error(Diagnostics),
}

#[derive(Clone)]
struct BlockInvariant<State> {
    /// Precondition of the block
    pre: State,
    /// Postcondition of the block---just success/error for now
    post: BlockPostcondition,
}

/// A map from block id's to the pre/post of each block after a fixed point is reached.
type InvariantMap<State> = BTreeMap<Label, BlockInvariant<State>>;

fn collect_states_and_diagnostics<State>(
    map: InvariantMap<State>,
) -> (BTreeMap<Label, State>, Diagnostics) {
    let mut diags = Diagnostics::new();
    let final_states = map
        .into_iter()
        .map(|(lbl, BlockInvariant { pre, post })| {
            if let BlockPostcondition::Error(ds) = post {
                diags.extend(ds)
            }
            (lbl, pre)
        })
        .collect();
    (final_states, diags)
}

/// Take a pre-state + instruction and mutate it to produce a post-state
/// Auxiliary data can be stored in self.
pub trait TransferFunctions {
    type State: AbstractDomain;

    /// Execute local@instr found at index local@index in the current basic block from pre-state
    /// local@pre.
    /// Should return an AnalysisError if executing the instruction is unsuccessful, and () if
    /// the effects of successfully executing local@instr have been reflected by mutatating
    /// local@pre.
    /// Auxilary data from the analysis that is not part of the abstract state can be collected by
    /// mutating local@self.
    /// The last instruction index in the current block is local@last_index. Knowing this
    /// information allows clients to detect the end of a basic block and special-case appropriately
    /// (e.g., normalizing the abstract state before a join).
    fn execute(
        &mut self,
        pre: &mut Self::State,
        lbl: Label,
        idx: usize,
        command: &Command,
    ) -> Diagnostics;
}

pub trait AbstractInterpreter: TransferFunctions {
    /// Analyze procedure local@function_view starting from pre-state local@initial_state.
    fn analyze_function(
        &mut self,
        cfg: &dyn CFG,
        initial_state: Self::State,
    ) -> (BTreeMap<Label, Self::State>, Diagnostics) {
        let mut inv_map: InvariantMap<Self::State> = InvariantMap::new();
        let start = cfg.start_block();
        let mut next_block = Some(start);

        while let Some(block_label) = next_block {
            let block_invariant = inv_map
                .entry(block_label)
                .or_insert_with(|| BlockInvariant {
                    pre: initial_state.clone(),
                    post: BlockPostcondition::Unprocessed,
                });

            let (post_state, errors) = self.execute_block(cfg, &block_invariant.pre, block_label);
            block_invariant.post = if errors.is_empty() {
                BlockPostcondition::Success
            } else {
                BlockPostcondition::Error(errors)
            };

            // propagate postcondition of this block to successor blocks
            let mut next_block_candidate = cfg.next_block(block_label);
            for next_block_id in cfg.successors(block_label) {
                match inv_map.get_mut(next_block_id) {
                    Some(next_block_invariant) => {
                        let join_result = {
                            let old_pre = &mut next_block_invariant.pre;
                            old_pre.join(&post_state)
                        };
                        match join_result {
                            JoinResult::Unchanged => {
                                // Pre is the same after join. Reanalyzing this block would produce
                                // the same post
                            }
                            JoinResult::Changed => {
                                // If the cur->successor is a back edge, jump back to the beginning
                                // of the loop, instead of the normal next block
                                if cfg.is_back_edge(block_label, *next_block_id) {
                                    next_block_candidate = Some(*next_block_id);
                                }
                                // Pre has changed, the post condition is now unknown for the block
                                next_block_invariant.post = BlockPostcondition::Unprocessed
                            }
                        }
                    }
                    None => {
                        // Haven't visited the next block yet. Use the post of the current block as
                        // its pre
                        inv_map.insert(
                            *next_block_id,
                            BlockInvariant {
                                pre: post_state.clone(),
                                post: BlockPostcondition::Success,
                            },
                        );
                    }
                }
            }
            next_block = next_block_candidate;
        }
        collect_states_and_diagnostics(inv_map)
    }

    fn execute_block(
        &mut self,
        cfg: &dyn CFG,
        pre_state: &Self::State,
        block_lbl: Label,
    ) -> (Self::State, Diagnostics) {
        let mut state = pre_state.clone();
        let mut diags = Diagnostics::new();
        for (idx, cmd) in cfg.commands(block_lbl) {
            diags.extend(self.execute(&mut state, block_lbl, idx, cmd));
        }
        (state, diags)
    }
}