Skip to content

Commit

Permalink
[move-prover] cache all used memories in a set
Browse files Browse the repository at this point in the history 
So that we don't need to keep deriving the `all()` set every time we use
it.

Closes: aptos-labs#9029
  • Loading branch information
@meng-xu-cs @bors-libra
meng-xu-cs authored and bors-libra committed Aug 26, 2021
1 parent 84cf684 commit 5a3e4a8
Show file tree
Hide file tree
Showing 6 changed files with 95 additions and 47 deletions.
7 changes: 7 additions & 0 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions language/move-prover/bytecode/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ log = "0.4.14"
serde = { version = "1.0.124", features = ["derive"] }
serde_json = "1.0.64"
once_cell = "1.7.2"
paste = "1.0.5"
petgraph = "0.5.1"

[dev-dependencies]
Expand Down
8 changes: 2 additions & 6 deletions language/move-prover/bytecode/src/global_invariant_instrumentation_v2.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,11 +120,7 @@ impl Analyzer {
// get memory (list of structs) read or written by the function target,
// then find all invariants in loaded modules that refer to that memory.
let mut invariants_for_used_memory = BTreeSet::new();
for mem in usage_analysis::get_memory_usage(target)
.accessed
.get_all()
.iter()
{
for mem in usage_analysis::get_memory_usage(target).accessed.all.iter() {
invariants_for_used_memory.extend(env.get_global_invariants_for_memory(mem));
}

Expand All @@ -148,7 +144,7 @@ impl Analyzer {
// collect instantiations of this function that are needed to check this global invariant
let mut func_insts = BTreeSet::new();

let fun_mems = usage_analysis::get_memory_usage(target).accessed.get_all();
let fun_mems = &usage_analysis::get_memory_usage(target).accessed.all;
let fun_arity = target.get_type_parameters().len();
for inv_mem in &invariant.mem_usage {
for fun_mem in fun_mems.iter() {
Expand Down
5 changes: 3 additions & 2 deletions language/move-prover/bytecode/src/spec_instrumentation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,8 @@ impl<'a> Instrumenter<'a> {
// Inject well-formedness assumption for used memory.
for mem in usage_analysis::get_memory_usage(&self.builder.get_target())
.accessed
.get_all()
.all
.clone()
{
// If this is native or intrinsic memory, skip this.
let struct_env = self
Expand Down Expand Up @@ -1054,7 +1055,7 @@ fn check_opaque_modifies_completeness(
// an immutable reference. We should find a better way how to deal with event handles.
for mem in usage_analysis::get_memory_usage(&target)
.modified
.get_all()
.all
.iter()
{
if env.is_wellknown_event_handle_type(&Type::Struct(mem.module_id, mem.id, vec![])) {
Expand Down
114 changes: 79 additions & 35 deletions language/move-prover/bytecode/src/usage_analysis.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ use move_model::{
};

use itertools::Itertools;
use paste::paste;
use std::{collections::BTreeSet, fmt, fmt::Formatter};

pub fn get_memory_usage<'env>(target: &FunctionTarget<'env>) -> &'env UsageState {
Expand All @@ -33,6 +34,8 @@ pub struct MemoryUsage {
pub direct: SetDomain<QualifiedInstId<StructId>>,
// The memory transitively used in either the function itself or at least one of its callees.
pub transitive: SetDomain<QualifiedInstId<StructId>>,
// The union of the above sets
pub all: SetDomain<QualifiedInstId<StructId>>,
}

#[derive(Default, Clone)]
Expand All @@ -45,19 +48,23 @@ pub struct UsageState {
pub assumed: MemoryUsage,
// The memory mentioned by the assert expressions in this function.
pub asserted: MemoryUsage,
// The union of the above sets
pub all: MemoryUsage,
}

impl MemoryUsage {
//
// accessors that union the sets
// setters that insert element(s) to related sets
//

pub fn get_all(&self) -> BTreeSet<QualifiedInstId<StructId>> {
self.direct
.iter()
.chain(self.transitive.iter())
.cloned()
.collect()
fn add_direct(&mut self, mem: QualifiedInstId<StructId>) {
self.direct.insert(mem.clone());
self.all.insert(mem);
}

fn add_transitive(&mut self, mem: QualifiedInstId<StructId>) {
self.transitive.insert(mem.clone());
self.all.insert(mem);
}

//
Expand All @@ -79,8 +86,8 @@ impl MemoryUsage {
}

pub fn get_all_inst(&self, inst: &[Type]) -> BTreeSet<QualifiedInstId<StructId>> {
self.get_all()
.into_iter()
self.all
.iter()
.map(|mem| mem.instantiate_ref(inst))
.collect()
}
Expand All @@ -104,7 +111,7 @@ impl MemoryUsage {
}

pub fn get_all_uninst(&self) -> BTreeSet<QualifiedId<StructId>> {
self.get_all()
self.all
.iter()
.map(|mem| mem.module_id.qualified(mem.id))
.collect()
Expand All @@ -116,26 +123,67 @@ impl AbstractDomain for MemoryUsage {
match (
self.direct.join(&other.direct),
self.transitive.join(&other.transitive),
self.all.join(&other.all),
) {
(JoinResult::Unchanged, JoinResult::Unchanged) => JoinResult::Unchanged,
(JoinResult::Unchanged, JoinResult::Unchanged, JoinResult::Unchanged) => {
JoinResult::Unchanged
}
_ => JoinResult::Changed,
}
}
}

macro_rules! generate_inserter {
($field: ident, $method: ident) => {
paste! {
#[allow(dead_code)]
fn [<$method _ $field>](&mut self, mem: QualifiedInstId<StructId>) {
self.$field.$method(mem.clone());
self.all.$method(mem);
}

#[allow(dead_code)]
fn [<$method _ $field _iter>](
&mut self,
mems: impl Iterator<Item = QualifiedInstId<StructId>>
) {
for mem in mems {
self.[<$method _ $field>](mem);
}
}
}
};
}

impl UsageState {
generate_inserter!(accessed, add_direct);
generate_inserter!(accessed, add_transitive);

generate_inserter!(modified, add_direct);
generate_inserter!(modified, add_transitive);

generate_inserter!(assumed, add_direct);
generate_inserter!(assumed, add_transitive);

generate_inserter!(asserted, add_direct);
generate_inserter!(asserted, add_transitive);
}

impl AbstractDomain for UsageState {
fn join(&mut self, other: &Self) -> JoinResult {
match (
self.accessed.join(&other.accessed),
self.modified.join(&other.modified),
self.assumed.join(&other.assumed),
self.asserted.join(&other.asserted),
self.all.join(&other.all),
) {
(
JoinResult::Unchanged,
JoinResult::Unchanged,
JoinResult::Unchanged,
JoinResult::Unchanged,
JoinResult::Unchanged,
) => JoinResult::Unchanged,
_ => JoinResult::Changed,
}
Expand Down Expand Up @@ -173,49 +221,45 @@ impl<'a> TransferFunctions for MemoryUsageAnalysis<'a> {
.cache
.get::<UsageState>(mid.qualified(*fid), &FunctionVariant::Baseline)
{
state
.modified
.transitive
.extend(summary.modified.get_all_inst(inst));
state
.accessed
.transitive
.extend(summary.accessed.get_all_inst(inst));
state
.assumed
.transitive
.extend(summary.assumed.get_all_inst(inst));
state
.asserted
.transitive
.extend(summary.asserted.get_all_inst(inst));
state.add_transitive_accessed_iter(
summary.accessed.get_all_inst(inst).into_iter(),
);
state.add_transitive_modified_iter(
summary.modified.get_all_inst(inst).into_iter(),
);
state.add_transitive_assumed_iter(
summary.assumed.get_all_inst(inst).into_iter(),
);
state.add_transitive_asserted_iter(
summary.asserted.get_all_inst(inst).into_iter(),
);
}
}
MoveTo(mid, sid, inst)
| MoveFrom(mid, sid, inst)
| BorrowGlobal(mid, sid, inst) => {
let mem = mid.qualified_inst(*sid, inst.to_owned());
state.modified.direct.insert(mem.clone());
state.accessed.direct.insert(mem);
state.add_direct_modified(mem.clone());
state.add_direct_accessed(mem);
}
WriteBack(BorrowNode::GlobalRoot(mem), _) => {
state.modified.direct.insert(mem.clone());
state.accessed.direct.insert(mem.clone());
state.add_direct_modified(mem.clone());
state.add_direct_accessed(mem.clone());
}
Exists(mid, sid, inst) | GetGlobal(mid, sid, inst) => {
let mem = mid.qualified_inst(*sid, inst.to_owned());
state.accessed.direct.insert(mem);
state.add_direct_accessed(mem);
}
_ => {}
},
// memory accesses in expressions
Prop(_, kind, exp) => match kind {
Assume => state.assumed.direct.extend(
Assume => state.add_direct_assumed_iter(
exp.used_memory(self.cache.global_env())
.into_iter()
.map(|(usage, _)| usage),
),
Assert => state.asserted.direct.extend(
Assert => state.add_direct_asserted_iter(
exp.used_memory(self.cache.global_env())
.into_iter()
.map(|(usage, _)| usage),
Expand Down Expand Up @@ -282,7 +326,7 @@ impl FunctionTargetProcessor for UsageProcessor {
f,
" {} = {{{}}}",
name,
set.get_all()
set.all
.iter()
.map(|qid| env.display(qid).to_string())
.join(", ")
Expand Down
7 changes: 3 additions & 4 deletions language/move-prover/bytecode/src/verification_analysis_v2.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
//! Analysis which computes an annotation for each function whether
use crate::{
dataflow_domains::SetDomain,
function_target::{FunctionData, FunctionTarget},
function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
options::ProverOptions,
Expand Down Expand Up @@ -348,7 +349,7 @@ fn compute_funs_that_modify_inv(
BTreeMap::new();
for inv_id in target_invariants {
// Collect the global state used by inv_id (this is computed in usage_analysis.rs)
let inv_mem_use: BTreeSet<_> = global_env
let inv_mem_use: SetDomain<_> = global_env
.get_global_invariant(*inv_id)
.unwrap()
.mem_usage
Expand All @@ -362,9 +363,7 @@ fn compute_funs_that_modify_inv(
for fun_env in module_env.get_functions() {
// Get all memory modified by this function.
let fun_target = targets.get_target(&fun_env, &variant);
let modified_memory = usage_analysis::get_memory_usage(&fun_target)
.modified
.get_all();
let modified_memory = &usage_analysis::get_memory_usage(&fun_target).modified.all;
// Add functions to set if it modifies mem used in invariant
// TODO: This should be using unification.
if !modified_memory.is_disjoint(&inv_mem_use) {
Expand Down

0 comments on commit 5a3e4a8

Please sign in to comment.