use itertools::Itertools;
use move_model::{
ast,
ast::{ExpData, TempIndex, Value},
model::{FunId, FunctionEnv, GlobalEnv, Loc, ModuleId, QualifiedId, QualifiedInstId, StructId},
pragmas::{ABORTS_IF_IS_PARTIAL_PRAGMA, EMITS_IS_PARTIAL_PRAGMA, EMITS_IS_STRICT_PRAGMA},
ty::{Type, TypeDisplayContext, BOOL_TYPE, NUM_TYPE},
};
use crate::{
function_data_builder::FunctionDataBuilder,
function_target::{FunctionData, FunctionTarget},
function_target_pipeline::{
FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant, VerificationFlavor,
},
livevar_analysis::LiveVarAnalysisProcessor,
options::ProverOptions,
reaching_def_analysis::ReachingDefProcessor,
stackless_bytecode::{
AbortAction, AssignKind, AttrId, BorrowEdge, BorrowNode, Bytecode, HavocKind, Label,
Operation, PropKind,
},
usage_analysis, verification_analysis,
};
use move_model::{
ast::Exp,
exp_generator::ExpGenerator,
spec_translator::{SpecTranslator, TranslatedSpec},
};
use std::{
collections::{BTreeMap, BTreeSet},
fmt,
};
const REQUIRES_FAILS_MESSAGE: &str = "precondition does not hold at this call";
const ENSURES_FAILS_MESSAGE: &str = "post-condition does not hold";
const ABORTS_IF_FAILS_MESSAGE: &str = "function does not abort under this condition";
const ABORT_NOT_COVERED: &str = "abort not covered by any of the `aborts_if` clauses";
const ABORTS_CODE_NOT_COVERED: &str =
"abort code not covered by any of the `aborts_if` or `aborts_with` clauses";
const EMITS_FAILS_MESSAGE: &str = "function does not emit the expected event";
const EMITS_NOT_COVERED: &str = "emitted event not covered by any of the `emits` clauses";
fn modify_check_fails_message(
env: &GlobalEnv,
mem: QualifiedId<StructId>,
targs: &[Type],
) -> String {
let targs_str = if targs.is_empty() {
"".to_string()
} else {
let tctx = TypeDisplayContext::WithEnv {
env,
type_param_names: None,
};
format!(
"<{}>",
targs
.iter()
.map(|ty| ty.display(&tctx).to_string())
.join(", ")
)
};
let module_env = env.get_module(mem.module_id);
format!(
"caller does not have permission to modify `{}::{}{}` at given address",
module_env.get_name().display(env.symbol_pool()),
module_env
.get_struct(mem.id)
.get_name()
.display(env.symbol_pool()),
targs_str
)
}
pub struct SpecInstrumentationProcessor {}
impl SpecInstrumentationProcessor {
pub fn new() -> Box<Self> {
Box::new(Self {})
}
}
impl FunctionTargetProcessor for SpecInstrumentationProcessor {
fn initialize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
check_modifies(env, targets);
}
fn process(
&self,
targets: &mut FunctionTargetsHolder,
fun_env: &FunctionEnv<'_>,
mut data: FunctionData,
) -> FunctionData {
assert_eq!(data.variant, FunctionVariant::Baseline);
if fun_env.is_native() || fun_env.is_intrinsic() {
return data;
}
let options = ProverOptions::get(fun_env.module_env.env);
let verification_info =
verification_analysis::get_info(&FunctionTarget::new(fun_env, &data));
let is_verified = verification_info.verified;
let is_inlined = verification_info.inlined;
if is_verified {
let mut verification_data =
data.fork(FunctionVariant::Verification(VerificationFlavor::Regular));
verification_data = Instrumenter::run(&*options, targets, fun_env, verification_data);
targets.insert_target_data(
&fun_env.get_qualified_id(),
verification_data.variant.clone(),
verification_data,
);
}
if is_inlined {
Instrumenter::run(&*options, targets, fun_env, data)
} else {
if !options.for_interpretation {
data.code = vec![];
}
data
}
}
fn name(&self) -> String {
"spec_instrumenter".to_string()
}
fn dump_result(
&self,
f: &mut fmt::Formatter,
env: &GlobalEnv,
targets: &FunctionTargetsHolder,
) -> fmt::Result {
writeln!(f, "\n\n==== spec-instrumenter input specs ====\n")?;
for ref module in env.get_modules() {
if !module.is_target() {
continue;
}
for ref fun in module.get_functions() {
for (variant, target) in targets.get_targets(fun) {
let spec = target.get_spec();
if !spec.conditions.is_empty() {
writeln!(
f,
"fun {}[{}]\n{}",
fun.get_full_name_str(),
variant,
fun.module_env.env.display(spec)
)?;
}
}
}
}
Ok(())
}
}
struct Instrumenter<'a> {
options: &'a ProverOptions,
builder: FunctionDataBuilder<'a>,
ret_locals: Vec<TempIndex>,
ret_label: Label,
can_return: bool,
abort_local: TempIndex,
abort_label: Label,
can_abort: bool,
mem_info: &'a BTreeSet<QualifiedInstId<StructId>>,
}
impl<'a> Instrumenter<'a> {
fn run(
options: &'a ProverOptions,
targets: &mut FunctionTargetsHolder,
fun_env: &FunctionEnv<'a>,
data: FunctionData,
) -> FunctionData {
let props: Vec<_> = data
.code
.iter()
.filter_map(|bc| match bc {
Bytecode::Prop(id, PropKind::Assume, exp)
| Bytecode::Prop(id, PropKind::Assert, exp) => Some((*id, exp.clone())),
_ => None,
})
.collect();
let mut builder = FunctionDataBuilder::new(fun_env, data);
let ret_locals = builder
.data
.return_types
.clone()
.into_iter()
.map(|ty| builder.new_temp(ty))
.collect_vec();
let ret_label = builder.new_label();
let abort_local = builder.new_temp(NUM_TYPE.clone());
let abort_label = builder.new_label();
let auto_trace = options.auto_trace_level.verified_functions()
&& builder.data.variant.is_verified()
|| options.auto_trace_level.functions();
let spec = SpecTranslator::translate_fun_spec(
auto_trace,
false,
&mut builder,
fun_env,
&[],
None,
&ret_locals,
);
let inlined_props: BTreeMap<_, _> = props
.into_iter()
.map(|(id, prop)| {
let loc = builder.get_loc(id);
(
id,
SpecTranslator::translate_inline_property(
&loc,
auto_trace,
&mut builder,
&prop,
),
)
})
.collect();
let mut mem_info = BTreeSet::new();
if auto_trace {
mem_info =
usage_analysis::get_memory_usage(&FunctionTarget::new(fun_env, &builder.data))
.accessed
.get_all_inst(&builder.data.type_args);
}
let mut instrumenter = Instrumenter {
options,
builder,
ret_locals,
ret_label,
can_return: false,
abort_local,
abort_label,
can_abort: false,
mem_info: &mem_info,
};
instrumenter.instrument(&spec, &inlined_props);
let mut data = instrumenter.builder.data;
let reach_def = ReachingDefProcessor::new();
let live_vars = LiveVarAnalysisProcessor::new_no_annotate();
data = reach_def.process(targets, fun_env, data);
live_vars.process(targets, fun_env, data)
}
fn is_verified(&self) -> bool {
self.builder.data.variant.is_verified()
}
fn instrument(
&mut self,
spec: &TranslatedSpec,
inlined_props: &BTreeMap<AttrId, (TranslatedSpec, Exp)>,
) {
use Bytecode::*;
use PropKind::*;
let old_code = std::mem::take(&mut self.builder.data.code);
self.emit_lets(spec, false);
self.builder
.set_loc(self.builder.fun_env.get_loc().at_start()); for (loc, exp) in spec.pre_conditions(&self.builder) {
self.builder.set_loc(loc);
self.builder
.emit_with(move |attr_id| Prop(attr_id, Assume, exp))
}
if self.is_verified() {
for (loc, exp) in &spec.modifies {
let struct_ty = self.builder.global_env().get_node_type(exp.node_id());
self.generate_modifies_check(
PropKind::Assume,
spec,
loc,
&struct_ty,
exp,
exp.call_args()[0].to_owned(),
);
}
for translated_spec in
std::iter::once(spec).chain(inlined_props.values().map(|(s, _)| s))
{
for (mem, label) in &translated_spec.saved_memory {
let mem = mem.clone();
self.builder
.emit_with(|attr_id| SaveMem(attr_id, *label, mem));
}
for (spec_var, label) in &translated_spec.saved_spec_vars {
let spec_var = spec_var.clone();
self.builder
.emit_with(|attr_id| SaveSpecVar(attr_id, *label, spec_var));
}
let saved_params = translated_spec.saved_params.clone();
self.emit_save_for_old(&saved_params);
}
}
for bc in old_code {
self.instrument_bytecode(spec, inlined_props, bc);
}
if self.can_return {
self.generate_return_block(spec);
}
if self.can_abort {
self.generate_abort_block(spec);
}
}
fn instrument_bytecode(
&mut self,
spec: &TranslatedSpec,
inlined_props: &BTreeMap<AttrId, (TranslatedSpec, Exp)>,
bc: Bytecode,
) {
use Bytecode::*;
use Operation::*;
match &bc {
Call(id, _, BorrowGlobal(mid, sid, targs), srcs, _)
| Call(id, _, MoveFrom(mid, sid, targs), srcs, _) => {
let addr_exp = self.builder.mk_temporary(srcs[0]);
self.generate_modifies_check(
PropKind::Assert,
spec,
&self.builder.get_loc(*id),
&Type::Struct(*mid, *sid, targs.to_owned()),
&addr_exp,
addr_exp.clone(),
);
}
Call(id, _, MoveTo(mid, sid, targs), srcs, _) => {
let addr_exp = self.builder.mk_temporary(srcs[1]);
self.generate_modifies_check(
PropKind::Assert,
spec,
&self.builder.get_loc(*id),
&Type::Struct(*mid, *sid, targs.to_owned()),
&addr_exp,
addr_exp.clone(),
);
}
_ => {}
}
match bc {
Ret(id, results) => {
self.builder.set_loc_from_attr(id);
for (i, r) in self.ret_locals.clone().into_iter().enumerate() {
self.builder
.emit_with(|id| Assign(id, r, results[i], AssignKind::Move));
}
let ret_label = self.ret_label;
self.builder.emit_with(|id| Jump(id, ret_label));
self.can_return = true;
}
Abort(id, code) => {
self.builder.set_loc_from_attr(id);
let abort_local = self.abort_local;
let abort_label = self.abort_label;
self.builder
.emit_with(|id| Assign(id, abort_local, code, AssignKind::Move));
self.builder.emit_with(|id| Jump(id, abort_label));
self.can_abort = true;
}
Call(id, dests, Function(mid, fid, targs), srcs, aa) => {
self.instrument_call(id, dests, mid, fid, targs, srcs, aa);
}
Call(id, dests, oper, srcs, _) if oper.can_abort() => {
self.builder.emit(Call(
id,
dests,
oper,
srcs,
Some(AbortAction(self.abort_label, self.abort_local)),
));
self.can_abort = true;
}
Prop(id, kind @ PropKind::Assume, prop) | Prop(id, kind @ PropKind::Assert, prop) => {
match inlined_props.get(&id) {
None => {
self.builder.emit(Prop(id, kind, prop));
}
Some((translated_spec, exp)) => {
self.emit_traces(translated_spec, exp);
self.builder.emit(Prop(id, kind, exp.clone()));
}
}
}
_ => self.builder.emit(bc),
}
}
fn instrument_call(
&mut self,
id: AttrId,
dests: Vec<TempIndex>,
mid: ModuleId,
fid: FunId,
targs: Vec<Type>,
srcs: Vec<TempIndex>,
aa: Option<AbortAction>,
) {
use Bytecode::*;
use PropKind::*;
let targs = &targs;
let env = self.builder.global_env();
let callee_env = env.get_module(mid).into_function(fid);
let callee_opaque = callee_env.is_opaque();
let mut callee_spec = SpecTranslator::translate_fun_spec(
self.options.auto_trace_level.functions(),
true,
&mut self.builder,
&callee_env,
targs,
Some(&srcs),
&dests,
);
self.builder.set_loc_from_attr(id);
self.emit_lets(&callee_spec, false);
self.builder.set_loc_from_attr(id);
if self.is_verified() || callee_opaque {
for (loc, cond) in callee_spec.pre_conditions(&self.builder) {
self.emit_traces(&callee_spec, &cond);
let prop_kind = match self.builder.data.variant {
FunctionVariant::Verification(..) => {
self.builder
.set_loc_and_vc_info(loc, REQUIRES_FAILS_MESSAGE);
Assert
}
FunctionVariant::Baseline => Assume,
};
self.builder.emit_with(|id| Prop(id, prop_kind, cond));
}
}
if self.is_verified() {
let loc = self.builder.get_loc(id);
for (_, exp) in &callee_spec.modifies {
let rty = env.get_node_type(exp.node_id());
let new_addr = exp.call_args()[0].clone();
self.generate_modifies_check(
PropKind::Assert,
&callee_spec,
&loc,
&rty,
exp,
new_addr,
);
}
}
if !callee_env.is_opaque() || self.options.for_interpretation {
self.builder.emit(Call(
id,
dests,
Operation::Function(mid, fid, targs.clone()),
srcs,
Some(AbortAction(self.abort_label, self.abort_local)),
));
self.can_abort = true;
} else {
self.generate_opaque_call(
dests.clone(),
mid,
fid,
targs,
srcs.clone(),
aa.clone(),
true,
);
self.emit_save_for_old(&callee_spec.saved_params);
let callee_aborts_if_is_partial =
callee_env.is_pragma_true(ABORTS_IF_IS_PARTIAL_PRAGMA, || false);
let (abort_cond_temp_opt, code_cond) =
self.generate_abort_opaque_cond(callee_aborts_if_is_partial, &callee_spec);
if let Some(abort_cond_temp) = abort_cond_temp_opt {
let abort_local = self.abort_local;
let abort_label = self.abort_label;
let no_abort_label = self.builder.new_label();
let abort_here_label = self.builder.new_label();
self.builder
.emit_with(|id| Branch(id, abort_here_label, no_abort_label, abort_cond_temp));
self.builder.emit_with(|id| Label(id, abort_here_label));
if let Some(cond) = code_cond {
self.emit_traces(&callee_spec, &cond);
self.builder.emit_with(move |id| Prop(id, Assume, cond));
}
self.builder.emit_with(move |id| {
Call(id, vec![], Operation::TraceAbort, vec![abort_local], None)
});
self.builder.emit_with(|id| Jump(id, abort_label));
self.builder.emit_with(|id| Label(id, no_abort_label));
self.can_abort = true;
}
for (mem, label) in std::mem::take(&mut callee_spec.saved_memory) {
self.builder.emit_with(|id| SaveMem(id, label, mem));
}
for (var, label) in std::mem::take(&mut callee_spec.saved_spec_vars) {
self.builder.emit_with(|id| SaveSpecVar(id, label, var));
}
for (_, exp) in std::mem::take(&mut callee_spec.modifies) {
self.emit_traces(&callee_spec, &exp);
self.builder.emit_with(|id| Prop(id, Modifies, exp));
}
let mut_srcs = srcs
.iter()
.cloned()
.filter(|src| {
let ty = &self.builder.data.local_types[*src];
ty.is_mutable_reference()
&& !self
.builder
.global_env()
.is_wellknown_event_handle_type(ty.skip_reference())
})
.collect_vec();
for src in &mut_srcs {
self.builder.emit_with(|id| {
Call(
id,
vec![],
Operation::Havoc(HavocKind::MutationValue),
vec![*src],
None,
)
});
}
for idx in mut_srcs.into_iter().chain(dests.iter().cloned()) {
let exp = self.builder.mk_call(
&BOOL_TYPE,
ast::Operation::WellFormed,
vec![self.builder.mk_temporary(idx)],
);
self.builder.emit_with(move |id| Prop(id, Assume, exp));
}
self.emit_lets(&callee_spec, true);
self.emit_updates(&callee_spec);
for (_, cond) in std::mem::take(&mut callee_spec.post) {
self.emit_traces(&callee_spec, &cond);
self.builder.emit_with(|id| Prop(id, Assume, cond));
}
for (_, msg, handle, cond) in std::mem::take(&mut callee_spec.emits) {
self.emit_traces(&callee_spec, &msg);
self.emit_traces(&callee_spec, &handle);
if let Some(c) = &cond {
self.emit_traces(&callee_spec, c);
}
let temp_msg = self.builder.emit_let(msg).0;
let temp_handle = self.builder.emit_let_skip_reference(handle).0;
let mut temp_list = vec![temp_msg, temp_handle];
if let Some(cond) = cond {
temp_list.push(self.builder.emit_let(cond).0);
}
self.builder
.emit(Call(id, vec![], Operation::EmitEvent, temp_list, None));
}
if callee_env.is_pragma_true(EMITS_IS_PARTIAL_PRAGMA, || false) {
self.builder
.emit(Call(id, vec![], Operation::EventStoreDiverge, vec![], None));
}
self.generate_opaque_call(dests, mid, fid, targs, srcs, aa, false);
}
}
fn emit_save_for_old(&mut self, vars: &BTreeMap<TempIndex, TempIndex>) {
use Bytecode::*;
for (idx, saved_idx) in vars {
if self.builder.data.local_types[*idx].is_reference() {
self.builder.emit_with(|attr_id| {
Call(
attr_id,
vec![*saved_idx],
Operation::ReadRef,
vec![*idx],
None,
)
})
} else {
self.builder
.emit_with(|attr_id| Assign(attr_id, *saved_idx, *idx, AssignKind::Copy))
}
}
}
fn emit_updates(&mut self, spec: &TranslatedSpec) {
for (loc, lhs, rhs) in &spec.updates {
self.builder.set_loc(loc.clone());
self.emit_traces(spec, lhs);
self.emit_traces(spec, rhs);
let (ghost_mem, _field_id, addr) = lhs
.extract_ghost_mem_access(self.builder.global_env())
.expect("lhs of update valid");
let ghost_mem_ty = ghost_mem.to_type();
let (rhs_temp, _) = self.builder.emit_let(self.builder.mk_call_with_inst(
&ghost_mem_ty,
ghost_mem.inst.clone(),
ast::Operation::Pack(ghost_mem.module_id, ghost_mem.id),
vec![rhs.clone()],
));
let (addr_temp, _) = self.builder.emit_let(addr);
let mem_ref = self
.builder
.new_temp(Type::Reference(true, Box::new(ghost_mem_ty)));
self.builder.emit_with(|id| {
Bytecode::Call(
id,
vec![mem_ref],
Operation::BorrowGlobal(
ghost_mem.module_id,
ghost_mem.id,
ghost_mem.inst.clone(),
),
vec![addr_temp],
None,
)
});
self.builder.emit_with(|id| {
Bytecode::Call(
id,
vec![],
Operation::WriteRef,
vec![mem_ref, rhs_temp],
None,
)
});
self.builder.emit_with(|id| {
Bytecode::Call(
id,
vec![],
Operation::WriteBack(
BorrowNode::GlobalRoot(ghost_mem.clone()),
BorrowEdge::Direct,
),
vec![mem_ref],
None,
)
});
}
}
fn emit_lets(&mut self, spec: &TranslatedSpec, post_state: bool) {
use Bytecode::*;
let lets = spec
.lets
.iter()
.filter(|(_, is_post, ..)| *is_post == post_state);
for (loc, _, temp, exp) in lets {
self.emit_traces(spec, exp);
self.builder.set_loc(loc.to_owned());
let assign = self
.builder
.mk_identical(self.builder.mk_temporary(*temp), exp.clone());
self.builder
.emit_with(|id| Prop(id, PropKind::Assume, assign));
}
}
fn emit_traces(&mut self, spec: &TranslatedSpec, emitted_exp: &ExpData) {
use Bytecode::*;
let node_ids = emitted_exp.node_ids().into_iter().collect::<BTreeSet<_>>();
let traces = spec
.debug_traces
.iter()
.filter(|(_, _, exp)| node_ids.contains(&exp.node_id()));
for (node_id, kind, exp) in traces {
let loc = self.builder.global_env().get_node_loc(*node_id);
self.builder.set_loc(loc);
let temp = if let ExpData::Temporary(_, temp) = exp.as_ref() {
*temp
} else {
self.builder.emit_let(exp.clone()).0
};
self.builder.emit_with(|id| {
Call(
id,
vec![],
Operation::TraceExp(*kind, *node_id),
vec![temp],
None,
)
});
}
for memory in self.mem_info {
self.builder.emit_with(|id| {
Call(
id,
vec![],
Operation::TraceGlobalMem(memory.clone()),
vec![],
None,
)
});
}
}
fn generate_abort_block(&mut self, spec: &TranslatedSpec) {
use Bytecode::*;
let fun_loc = self.builder.fun_env.get_loc().at_end();
self.builder.set_loc(fun_loc);
let abort_label = self.abort_label;
self.builder.emit_with(|id| Label(id, abort_label));
if self.is_verified() {
self.generate_abort_verify(spec);
}
let abort_local = self.abort_local;
self.builder.emit_with(|id| Abort(id, abort_local));
}
fn generate_abort_verify(&mut self, spec: &TranslatedSpec) {
use Bytecode::*;
use PropKind::*;
let is_partial = self
.builder
.fun_env
.is_pragma_true(ABORTS_IF_IS_PARTIAL_PRAGMA, || false);
if !is_partial {
if let Some(cond) = spec.aborts_condition(&self.builder) {
let loc = self.builder.fun_env.get_spec_loc();
self.emit_traces(spec, &cond);
self.builder.set_loc_and_vc_info(loc, ABORT_NOT_COVERED);
self.builder.emit_with(move |id| Prop(id, Assert, cond));
}
}
if spec.has_aborts_code_specs() {
let actual_code = self.builder.mk_temporary(self.abort_local);
if let Some(code_cond) = spec.aborts_code_condition(&self.builder, &actual_code) {
let loc = self.builder.fun_env.get_spec_loc();
self.emit_traces(spec, &code_cond);
self.builder
.set_loc_and_vc_info(loc, ABORTS_CODE_NOT_COVERED);
self.builder
.emit_with(move |id| Prop(id, Assert, code_cond));
}
}
}
fn generate_abort_opaque_cond(
&mut self,
is_partial: bool,
spec: &TranslatedSpec,
) -> (Option<TempIndex>, Option<Exp>) {
let aborts_cond = if is_partial {
None
} else {
spec.aborts_condition(&self.builder)
};
let aborts_cond_temp = if let Some(cond) = aborts_cond {
if matches!(cond.as_ref(), ExpData::Value(_, Value::Bool(false))) {
return (None, None);
}
self.builder.emit_let(cond).0
} else {
self.builder.emit_let_havoc(BOOL_TYPE.clone()).0
};
let aborts_code_cond = if spec.has_aborts_code_specs() {
let actual_code = self.builder.mk_temporary(self.abort_local);
spec.aborts_code_condition(&self.builder, &actual_code)
} else {
None
};
(Some(aborts_cond_temp), aborts_code_cond)
}
fn generate_return_block(&mut self, spec: &TranslatedSpec) {
use Bytecode::*;
use PropKind::*;
self.builder
.set_loc(self.builder.fun_env.get_loc().at_end());
let ret_label = self.ret_label;
self.builder.emit_with(|id| Label(id, ret_label));
let lets_emitted = if !spec.updates.is_empty() {
self.emit_lets(spec, true);
self.emit_updates(spec);
true
} else {
false
};
if self.is_verified() {
if !lets_emitted {
self.emit_lets(spec, true);
}
for (loc, abort_cond, _) in &spec.aborts {
self.emit_traces(spec, abort_cond);
let exp = self.builder.mk_not(abort_cond.clone());
self.builder
.set_loc_and_vc_info(loc.clone(), ABORTS_IF_FAILS_MESSAGE);
self.builder.emit_with(|id| Prop(id, Assert, exp))
}
for (loc, cond) in &spec.post {
self.emit_traces(spec, cond);
self.builder
.set_loc_and_vc_info(loc.clone(), ENSURES_FAILS_MESSAGE);
self.builder
.emit_with(move |id| Prop(id, Assert, cond.clone()))
}
for (loc, cond) in spec.emits_conditions(&self.builder) {
self.emit_traces(spec, &cond);
self.builder.set_loc_and_vc_info(loc, EMITS_FAILS_MESSAGE);
self.builder.emit_with(move |id| Prop(id, Assert, cond))
}
let emits_is_partial = self
.builder
.fun_env
.is_pragma_true(EMITS_IS_PARTIAL_PRAGMA, || false);
let emits_is_strict = self
.builder
.fun_env
.is_pragma_true(EMITS_IS_STRICT_PRAGMA, || false);
if (!spec.emits.is_empty() && !emits_is_partial)
|| (spec.emits.is_empty() && emits_is_strict)
{
let cond = spec.emits_completeness_condition(&self.builder);
let loc = self.builder.fun_env.get_spec_loc();
self.emit_traces(spec, &cond);
self.builder.set_loc_and_vc_info(loc, EMITS_NOT_COVERED);
self.builder.emit_with(move |id| Prop(id, Assert, cond));
}
}
let ret_locals = self.ret_locals.clone();
self.builder.emit_with(move |id| Ret(id, ret_locals))
}
fn generate_modifies_check(
&mut self,
kind: PropKind,
spec: &TranslatedSpec,
loc: &Loc,
resource_type: &Type,
original_exp: &Exp, addr: Exp,
) {
let target = self.builder.get_target();
let (mid, sid, _) = resource_type.require_struct();
if self.is_verified()
&& target
.get_modify_targets_for_type(&mid.qualified(sid))
.is_some()
{
self.emit_traces(spec, original_exp);
let env = self.builder.global_env();
let node_id = env.new_node(loc.clone(), BOOL_TYPE.clone());
env.set_node_instantiation(node_id, vec![resource_type.to_owned()]);
let can_modify =
ExpData::Call(node_id, ast::Operation::CanModify, vec![addr]).into_exp();
if kind == PropKind::Assert {
let (mid, sid, inst) = resource_type.require_struct();
self.builder.set_loc_and_vc_info(
loc.clone(),
&modify_check_fails_message(env, mid.qualified(sid), inst),
);
} else {
self.builder.set_loc(loc.clone());
}
self.builder
.emit_with(|id| Bytecode::Prop(id, kind, can_modify));
}
}
fn generate_opaque_call(
&mut self,
dests: Vec<TempIndex>,
mid: ModuleId,
fid: FunId,
targs: &[Type],
srcs: Vec<TempIndex>,
aa: Option<AbortAction>,
is_begin: bool,
) {
let opaque_op = if is_begin {
Operation::OpaqueCallBegin(mid, fid, targs.to_vec())
} else {
Operation::OpaqueCallEnd(mid, fid, targs.to_vec())
};
self.builder
.emit_with(|id| Bytecode::Call(id, dests, opaque_op, srcs, aa));
}
}
fn check_modifies(env: &GlobalEnv, targets: &FunctionTargetsHolder) {
for module_env in env.get_modules() {
if module_env.is_target() {
for fun_env in module_env.get_functions() {
check_caller_callee_modifies_relation(env, targets, &fun_env);
check_opaque_modifies_completeness(env, targets, &fun_env);
}
}
}
}
fn check_caller_callee_modifies_relation(
env: &GlobalEnv,
targets: &FunctionTargetsHolder,
fun_env: &FunctionEnv,
) {
if fun_env.is_native() || fun_env.is_intrinsic() {
return;
}
let caller_func_target = targets.get_target(fun_env, &FunctionVariant::Baseline);
for callee in fun_env.get_called_functions() {
let callee_fun_env = env.get_function(callee);
if callee_fun_env.is_native() || callee_fun_env.is_intrinsic() {
continue;
}
let callee_func_target = targets.get_target(&callee_fun_env, &FunctionVariant::Baseline);
let callee_modified_memory = usage_analysis::get_memory_usage(&callee_func_target)
.modified
.get_all_uninst();
for target in caller_func_target.get_modify_targets().keys() {
if callee_modified_memory.contains(target)
&& callee_func_target
.get_modify_targets_for_type(target)
.is_none()
{
let loc = caller_func_target.get_loc();
env.error(
&loc,
&format!(
"caller `{}` specifies modify targets for `{}` but callee `{}` does not",
fun_env.get_full_name_str(),
env.get_module(target.module_id)
.into_struct(target.id)
.get_full_name_str(),
callee_fun_env.get_full_name_str()
),
);
}
}
}
}
fn check_opaque_modifies_completeness(
env: &GlobalEnv,
targets: &FunctionTargetsHolder,
fun_env: &FunctionEnv,
) {
let target = targets.get_target(fun_env, &FunctionVariant::Baseline);
if !target.is_opaque() {
return;
}
for mem in usage_analysis::get_memory_usage(&target)
.modified
.all
.iter()
{
if env.is_wellknown_event_handle_type(&Type::Struct(mem.module_id, mem.id, vec![])) {
continue;
}
if env.get_struct_qid(mem.to_qualified_id()).is_ghost_memory() {
continue;
}
let found = target.get_modify_ids().iter().any(|id| mem == id);
if !found {
let loc = fun_env.get_spec_loc();
env.error(&loc,
&format!("function `{}` is opaque but its specification does not have a modifies clause for `{}`",
fun_env.get_full_name_str(),
env.display(mem))
)
}
}
}