Skip to content

Commit d1f4868

Browse files
authored
wip on old! replacing (#323)
* wip on old! replacing * feat: simplification * cleanup * cleanup * cleanup
1 parent ed8e76a commit d1f4868

3 files changed

Lines changed: 116 additions & 3 deletions

File tree

crates/move-stackless-bytecode/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ pub mod packed_types_analysis;
5050
pub mod pipeline_factory;
5151
pub mod quantifier_iterator_analysis;
5252
pub mod reaching_def_analysis;
53+
pub mod replacement_analysis;
5354
pub mod spec_global_variable_analysis;
5455
pub mod spec_instrumentation;
5556
pub mod spec_purity_analysis;

crates/move-stackless-bytecode/src/pipeline_factory.rs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,11 @@ use crate::{
66
borrow_analysis::BorrowAnalysisProcessor,
77
clean_and_optimize::CleanAndOptimizeProcessor,
88
conditional_merge_insertion::ConditionalMergeInsertionProcessor,
9-
// data_invariant_instrumentation::DataInvariantInstrumentationProcessor,
109
debug_instrumentation::DebugInstrumenter,
1110
deterministic_analysis::DeterministicAnalysisProcessor,
1211
dynamic_field_analysis::DynamicFieldAnalysisProcessor,
1312
eliminate_imm_refs::EliminateImmRefsProcessor,
1413
function_target_pipeline::{FunctionTargetPipeline, FunctionTargetProcessor},
15-
// global_invariant_analysis::GlobalInvariantAnalysisProcessor,
16-
// global_invariant_instrumentation::GlobalInvariantInstrumentationProcessor,
1714
inconsistency_check::InconsistencyCheckInstrumenter,
1815
livevar_analysis::LiveVarAnalysisProcessor,
1916
loop_analysis::LoopAnalysisProcessor,
@@ -27,6 +24,7 @@ use crate::{
2724
options::ProverOptions,
2825
quantifier_iterator_analysis::QuantifierIteratorAnalysisProcessor,
2926
reaching_def_analysis::ReachingDefProcessor,
27+
replacement_analysis::ReplacementAnalysisProcessor,
3028
spec_global_variable_analysis::SpecGlobalVariableAnalysisProcessor,
3129
spec_instrumentation::SpecInstrumentationProcessor,
3230
spec_purity_analysis::SpecPurityAnalysis,
@@ -71,6 +69,7 @@ pub fn default_pipeline_with_options(options: &ProverOptions) -> FunctionTargetP
7169
TypeInvariantAnalysisProcessor::new(),
7270
SpecWellFormedAnalysisProcessor::new(),
7371
QuantifierIteratorAnalysisProcessor::new(),
72+
ReplacementAnalysisProcessor::new(),
7473
]);
7574

7675
if !options.skip_loop_analysis {
Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
use std::collections::BTreeMap;
2+
3+
use move_model::model::{FunId, FunctionEnv, QualifiedId};
4+
5+
use crate::{
6+
function_data_builder::FunctionDataBuilder,
7+
function_target::FunctionData,
8+
function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
9+
stackless_bytecode::{AssignKind, Bytecode, Operation},
10+
};
11+
12+
pub struct ReplacementAnalysisProcessor();
13+
14+
impl ReplacementAnalysisProcessor {
15+
pub fn new() -> Box<Self> {
16+
Box::new(Self())
17+
}
18+
19+
fn is_fn(code: &Bytecode, qid: QualifiedId<FunId>) -> Option<(&Vec<usize>, &Vec<usize>)> {
20+
match code {
21+
Bytecode::Call(_, dest, Operation::Function(mid, fid, _), srcs, _) => {
22+
if qid == mid.qualified(*fid) {
23+
return Some((dest, srcs));
24+
}
25+
}
26+
_ => {}
27+
}
28+
29+
None
30+
}
31+
32+
pub fn find_ref_val_patterns(
33+
&self,
34+
func_env: &FunctionEnv,
35+
data: &FunctionData,
36+
) -> BTreeMap<usize, (Vec<usize>, Vec<usize>)> {
37+
if data.code.len() < 2 {
38+
return BTreeMap::new();
39+
}
40+
41+
let mut matches = BTreeMap::new();
42+
for i in 0..data.code.len() - 1 {
43+
if let Some((dest_val, srcs_val)) =
44+
Self::is_fn(&data.code[i], func_env.module_env.env.prover_val_qid())
45+
{
46+
if let Some((dest_ref, srcs_ref)) =
47+
Self::is_fn(&data.code[i + 1], func_env.module_env.env.prover_ref_qid())
48+
{
49+
if dest_val == srcs_ref {
50+
matches.insert(i, (dest_ref.clone(), srcs_val.clone()));
51+
}
52+
}
53+
}
54+
}
55+
56+
matches
57+
}
58+
59+
pub fn replace_patterns(
60+
&self,
61+
patterns: BTreeMap<usize, (Vec<usize>, Vec<usize>)>,
62+
func_env: &FunctionEnv,
63+
data: FunctionData,
64+
) -> FunctionData {
65+
if patterns.is_empty() {
66+
return data;
67+
}
68+
69+
let mut new_data = data.clone();
70+
new_data.code = vec![]; // NOTE: for some reason it doesnt work properly without copy + erase
71+
72+
let mut builder = FunctionDataBuilder::new(func_env, new_data);
73+
for (offset, bc) in data.code.into_iter().enumerate() {
74+
if patterns.contains_key(&offset) {
75+
continue;
76+
} else if offset > 0 && patterns.contains_key(&(offset - 1)) {
77+
// NOTE: we replace call only with an Assign because it automatically dereferences var
78+
let (dest, srcs) = patterns.get(&(offset - 1)).unwrap();
79+
builder.emit(Bytecode::Assign(
80+
bc.get_attr_id(),
81+
dest[0],
82+
srcs[0],
83+
AssignKind::Copy,
84+
));
85+
} else {
86+
builder.emit(bc);
87+
}
88+
}
89+
90+
builder.data
91+
}
92+
}
93+
94+
impl FunctionTargetProcessor for ReplacementAnalysisProcessor {
95+
fn process(
96+
&self,
97+
targets: &mut FunctionTargetsHolder,
98+
func_env: &FunctionEnv,
99+
data: FunctionData,
100+
_scc_opt: Option<&[FunctionEnv]>,
101+
) -> FunctionData {
102+
if func_env.is_native() {
103+
return data;
104+
}
105+
106+
let patterns = self.find_ref_val_patterns(func_env, &data);
107+
self.replace_patterns(patterns, func_env, data)
108+
}
109+
110+
fn name(&self) -> String {
111+
"replacement_analysis".to_string()
112+
}
113+
}

0 commit comments

Comments
 (0)