Skip to content

Commit

Permalink
Adding combinatorial proptests to test runtime access specifiers.
Browse files Browse the repository at this point in the history
  • Loading branch information
wrwg committed Oct 21, 2023
1 parent 3562af0 commit 4daf3b5
Show file tree
Hide file tree
Showing 25 changed files with 625 additions and 66 deletions.
4 changes: 3 additions & 1 deletion crates/aptos-admin-service/src/server/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,11 @@
use crate::server::utils::reply_with_status;
use aptos_config::config::NodeConfig;
use aptos_logger::info;
#[cfg(target_os = "linux")]
use hyper::Method;
use hyper::{
service::{make_service_fn, service_fn},
Body, Method, Request, Response, Server, StatusCode,
Body, Request, Response, Server, StatusCode,
};
use std::{
convert::Infallible,
Expand Down
1 change: 1 addition & 0 deletions third_party/move/move-binary-format/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -31,3 +31,4 @@ serde_json = "1.0.64"
[features]
default = []
fuzzing = ["proptest", "proptest-derive", "arbitrary", "move-core-types/fuzzing"]
testing = []
9 changes: 7 additions & 2 deletions third_party/move/move-binary-format/src/file_format_common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -507,8 +507,13 @@ pub(crate) mod versioned_data {
},
};
if version == 0 || version > u32::min(max_version, VERSION_MAX) {
return Err(PartialVMError::new(StatusCode::UNKNOWN_VERSION));
} else if version == VERSION_NEXT && !cfg!(test) && !cfg!(feature = "fuzzing") {
return Err(PartialVMError::new(StatusCode::UNKNOWN_VERSION)
.with_message(format!("bytecode version {} unsupported", version)));
} else if version == VERSION_NEXT
&& !cfg!(test)
&& !cfg!(feature = "testing")
&& !cfg!(feature = "fuzzing")
{
return Err(
PartialVMError::new(StatusCode::UNKNOWN_VERSION).with_message(format!(
"bytecode version {} only allowed in test code",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ use move_binary_format::{
Bytecode, CodeOffset, CompiledModule, FunctionDefinition, FunctionDefinitionIndex,
FunctionHandle, FunctionHandleIndex, StructDefinitionIndex,
},
file_format_common::VERSION_7,
safe_unwrap,
};
use move_core_types::vm_status::StatusCode;
Expand Down Expand Up @@ -183,12 +182,9 @@ impl<'a> AcquiresVerifier<'a> {
let function_handle = self.module.function_handle_at(fh_idx);
let mut function_acquired_resources =
self.function_acquired_resources(function_handle, fh_idx);
if self.module.version < VERSION_7 {
// TODO: consolidate acquires with access control and borrow analysis
for acquired_resource in &function_acquired_resources {
if !self.annotated_acquires.contains(acquired_resource) {
return Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset));
}
for acquired_resource in &function_acquired_resources {
if !self.annotated_acquires.contains(acquired_resource) {
return Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset));
}
}
self.actual_acquires
Expand All @@ -201,16 +197,11 @@ impl<'a> AcquiresVerifier<'a> {
sd_idx: StructDefinitionIndex,
offset: CodeOffset,
) -> PartialVMResult<()> {
if self.module.version < VERSION_7 {
// TODO: consolidate acquires with access control and borrow analysis
if self.annotated_acquires.contains(&sd_idx) {
self.actual_acquires.insert(sd_idx);
Ok(())
} else {
Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset))
}
} else {
if self.annotated_acquires.contains(&sd_idx) {
self.actual_acquires.insert(sd_idx);
Ok(())
} else {
Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset))
}
}

Expand Down
58 changes: 44 additions & 14 deletions third_party/move/move-compiler-v2/src/bytecode_generator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -521,10 +521,26 @@ impl<'env> Generator<'env> {
self.gen_op_call(targets, id, BytecodeOperation::Pack(*mid, *sid, inst), args)
},
Operation::Select(mid, sid, fid) => {
let inst = self.env().get_node_instantiation(id);
let target = self.require_unary_target(id, targets);
let arg = self.require_unary_arg(id, args);
self.gen_select(target, id, mid.qualified_inst(*sid, inst), *fid, &arg)
// Get the instantiation of the struct. It's not contained in the select
// expression but in the type of it's operand.
if let Some((_, inst)) = self
.env()
.get_node_type(arg.node_id())
.skip_reference()
.get_struct(self.env())
{
self.gen_select(
target,
id,
mid.qualified_inst(*sid, inst.to_vec()),
*fid,
&arg,
)
} else {
self.internal_error(id, "inconsistent type in select expression")
}
},
Operation::Exists(None) => {
let inst = self.env().get_node_instantiation(id);
Expand Down Expand Up @@ -788,13 +804,12 @@ impl<'env> Generator<'env> {
match exp.as_ref() {
ExpData::Temporary(_, temp) => *temp,
ExpData::LocalVar(id, sym) => self.find_local(*id, *sym),
ExpData::Call(_, Operation::Select(..), _) if self.reference_mode() => {
ExpData::Call(id, Operation::Select(..), _) if self.reference_mode() => {
// In reference mode, a selection is interpreted as selecting a reference to the
// field.
let id = exp.node_id();
let ty = Type::Reference(
self.reference_mode_kind,
Box::new(self.env().get_node_type(id)),
Box::new(self.env().get_node_type(*id)),
);
let temp = self.new_temp(ty);
self.gen(vec![temp], exp);
Expand Down Expand Up @@ -844,10 +859,10 @@ impl<'env> Generator<'env> {
impl<'env> Generator<'env> {
fn gen_borrow(&mut self, target: TempIndex, id: NodeId, kind: ReferenceKind, arg: &Exp) {
match arg.as_ref() {
ExpData::Call(_arg_id, Operation::Select(mid, sid, fid), args) => {
ExpData::Call(arg_id, Operation::Select(mid, sid, fid), args) => {
return self.gen_borrow_field(
target,
id,
*arg_id,
kind,
mid.qualified(*sid),
*fid,
Expand Down Expand Up @@ -924,13 +939,28 @@ impl<'env> Generator<'env> {
// Currently no conditions for immutable, so we do allow `&fun().field`.
},
}
let inst = self.env().get_node_instantiation(id);
self.emit_call(
id,
vec![target],
BytecodeOperation::BorrowField(struct_id.module_id, struct_id.id, inst, field_offset),
vec![temp],
);
// Get instantiation of field. It is not contained in the select expression but in the
// type of its operand.
if let Some((_, inst)) = self
.env()
.get_node_type(oper.node_id())
.skip_reference()
.get_struct(self.env())
{
self.emit_call(
id,
vec![target],
BytecodeOperation::BorrowField(
struct_id.module_id,
struct_id.id,
inst.to_vec(),
field_offset,
),
vec![temp],
);
} else {
self.internal_error(id, "inconsistent type in select expression")
}
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,12 @@ struct LabelInfo {

impl<'a> FunctionGenerator<'a> {
/// Runs the function generator for the given function.
pub fn run<'b>(gen: &'a mut ModuleGenerator, ctx: &'b ModuleContext, fun_env: FunctionEnv<'b>) {
pub fn run<'b>(
gen: &'a mut ModuleGenerator,
ctx: &'b ModuleContext,
fun_env: FunctionEnv<'b>,
acquires_list: &BTreeSet<StructId>,
) {
let loc = fun_env.get_loc();
let function = gen.function_index(ctx, &loc, &fun_env);
let visibility = fun_env.visibility();
Expand All @@ -111,11 +116,18 @@ impl<'a> FunctionGenerator<'a> {
} else {
(gen, None)
};
let acquires_global_resources = acquires_list
.iter()
.map(|id| {
let struct_env = fun_env.module_env.get_struct(*id);
gen.struct_def_index(ctx, &struct_env.get_loc(), &struct_env)
})
.collect();
let def = FF::FunctionDefinition {
function,
visibility,
is_entry: fun_env.is_entry(),
acquires_global_resources: vec![],
acquires_global_resources,
code,
};
ctx.checked_bound(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,11 @@ use move_model::{
ty::{PrimitiveType, ReferenceKind, Type},
};
use move_stackless_bytecode::{
function_target_pipeline::FunctionTargetsHolder, stackless_bytecode::Constant,
function_target_pipeline::{FunctionTargetsHolder, FunctionVariant},
stackless_bytecode::{Bytecode, Constant, Operation},
};
use move_symbol_pool::symbol as IR_SYMBOL;
use std::collections::BTreeMap;
use std::collections::{BTreeMap, BTreeSet};

/// Internal state of the module code generator
#[derive(Debug)]
Expand Down Expand Up @@ -144,8 +145,11 @@ impl ModuleGenerator {
for struct_env in module_env.get_structs() {
self.gen_struct(ctx, &struct_env)
}

let acquires_map = ctx.generate_acquires_map(module_env);
for fun_env in module_env.get_functions() {
FunctionGenerator::run(self, ctx, fun_env);
let acquires_list = &acquires_map[&fun_env.get_id()];
FunctionGenerator::run(self, ctx, fun_env, acquires_list);
}
}

Expand Down Expand Up @@ -766,3 +770,63 @@ impl<'env> ModuleContext<'env> {
s.display(self.env.symbol_pool()).to_string()
}
}

impl<'env> ModuleContext<'env> {
/// Acquires analysis. This is temporary until we have the full reference analysis.
fn generate_acquires_map(&self, module: &ModuleEnv) -> BTreeMap<FunId, BTreeSet<StructId>> {
// Compute map with direct usage of resources
let mut usage_map = module
.get_functions()
.into_iter()
.map(|f| (f.get_id(), self.get_function_acquires(&f)))
.collect::<BTreeMap<_, _>>();
// Now run a fixed-point loop: add resources used by called functions until there are no
// changes.
loop {
let mut changes = false;
for fun in module.get_functions() {
if let Some(callees) = fun.get_called_functions() {
let mut usage = usage_map[&fun.get_id()].clone();
let mut local_changes = false;
for callee in callees {
if callee.module_id == module.get_id() {
let count = usage.len();
usage.extend(usage_map[&callee.id].iter().cloned());
if usage.len() > count {
local_changes = true;
}
}
}
if local_changes {
*usage_map.get_mut(&fun.get_id()).unwrap() = usage;
changes = true;
}
}
}
if !changes {
break;
}
}
usage_map
}

fn get_function_acquires(&self, fun: &FunctionEnv) -> BTreeSet<StructId> {
let mut result = BTreeSet::new();
let target = self.targets.get_target(fun, &FunctionVariant::Baseline);
for bc in target.get_bytecode() {
use Bytecode::*;
use Operation::*;
match bc {
Call(_, _, MoveFrom(mid, sid, ..), ..)
| Call(_, _, BorrowGlobal(mid, sid, ..), ..)
| Call(_, _, GetGlobal(mid, sid, ..), ..)
if *mid == fun.module_env.get_id() =>
{
result.insert(*sid);
},
_ => {},
}
}
result
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,25 @@ module 0x42::fields {
struct T {
h: u64,
}
struct G {
f: #0,
}
struct S {
f: u64,
g: fields::T,
}
private fun read_generic_val(x: fields::G<u64>): u64 {
select fields::G.f(x)
}
private fun read_ref(x: &fields::S): u64 {
select fields::T.h(select fields::S.g(x))
}
private fun read_val(x: fields::S): u64 {
select fields::T.h(select fields::S.g(x))
}
private fun write_generic_val(x: &mut fields::G<u64>,v: u64) {
select fields::G.f(x) = v
}
private fun write_local_direct(): fields::S {
{
let x: fields::S = pack fields::S(0, pack fields::T(0));
Expand All @@ -38,12 +47,18 @@ module 0x42::fields {
select fields::T.h(select fields::S.g(x)) = 42;
x
}
spec fun $read_generic_val(x: fields::G<u64>): u64 {
select fields::G.f(x)
}
spec fun $read_ref(x: fields::S): u64 {
select fields::T.h(select fields::S.g(x))
}
spec fun $read_val(x: fields::S): u64 {
select fields::T.h(select fields::S.g(x))
}
spec fun $write_generic_val(x: fields::G<u64>,v: u64) {
select fields::G.f(x) = v
}
spec fun $write_local_direct(): fields::S;
spec fun $write_local_via_ref(): fields::S;
spec fun $write_param(x: &mut fields::S);
Expand All @@ -52,6 +67,18 @@ module 0x42::fields {

============ initial bytecode ================

[variant baseline]
fun fields::read_generic_val($t0: fields::G<u64>): u64 {
var $t1: u64
var $t2: &fields::G<u64>
var $t3: &u64
0: $t2 := borrow_local($t0)
1: $t3 := borrow_field<fields::G<u64>>.f($t2)
2: $t1 := read_ref($t3)
3: return $t1
}


[variant baseline]
fun fields::read_ref($t0: &fields::S): u64 {
var $t1: u64
Expand All @@ -78,6 +105,15 @@ fun fields::read_val($t0: fields::S): u64 {
}


[variant baseline]
fun fields::write_generic_val($t0: &mut fields::G<u64>, $t1: u64) {
var $t2: &mut u64
0: $t2 := borrow_field<fields::G<u64>>.f($t0)
1: write_ref($t2, $t1)
2: return ()
}


[variant baseline]
fun fields::write_local_direct(): fields::S {
var $t0: fields::S
Expand Down
Loading

0 comments on commit 4daf3b5

Please sign in to comment.