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
// Copyright (c) The Diem Core Contributors
// Copyright (c) The Move Contributors
// SPDX-License-Identifier: Apache-2.0
//! Transformation which injects well-formed assumptions at top-level entry points of verified
//! functions. These assumptions are both about parameters and any memory referred to by
//! the code. For ghost memory, the transformation also assumes initial values if provided.
//!
//! This needs to be run *after* function specifications and global invariants have been
//! injected because only then we know all accessed memory.
//!
//! This phase need to be run *before* data invariant instrumentation, because the latter relies
//! on the well-formed assumptions, augmenting them with the data invariant.
//! Because data invariants cannot refer to global memory, they are not relevant for memory
//! usage, and their injection therefore can happen after this phase.
use crate::{
function_data_builder::FunctionDataBuilder,
function_target::FunctionData,
function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
stackless_bytecode::PropKind,
usage_analysis::UsageProcessor,
};
use move_model::{
ast::{Operation, QuantKind},
exp_generator::ExpGenerator,
model::FunctionEnv,
ty::BOOL_TYPE,
};
use num::{BigUint, Zero};
pub struct WellFormedInstrumentationProcessor {}
impl WellFormedInstrumentationProcessor {
pub fn new() -> Box<Self> {
Box::new(Self {})
}
}
impl FunctionTargetProcessor for WellFormedInstrumentationProcessor {
fn process(
&self,
targets: &mut FunctionTargetsHolder,
fun_env: &FunctionEnv<'_>,
data: FunctionData,
) -> FunctionData {
if !data.variant.is_verified() {
// only need to do this for verified functions
return data;
}
// Rerun usage analysis for this function.
let usage = UsageProcessor::analyze(targets, fun_env, &data);
let mut builder = FunctionDataBuilder::new(fun_env, data);
builder.set_loc(fun_env.get_loc().at_start());
let old_code = std::mem::take(&mut builder.data.code);
// Inject well-formedness assumptions for parameters.
for param in 0..builder.fun_env.get_parameter_count() {
let exp = builder.mk_call(
&BOOL_TYPE,
Operation::WellFormed,
vec![builder.mk_temporary(param)],
);
builder.emit_prop(PropKind::Assume, exp);
}
// Inject well-formedness assumption for used memory.
for mem in usage.accessed.all {
let struct_env = builder.global_env().get_struct_qid(mem.to_qualified_id());
if struct_env.is_native_or_intrinsic() {
// If this is native or intrinsic memory, skip this.
continue;
}
let exp = builder
.mk_inst_mem_quant_opt(QuantKind::Forall, &mem, &mut |val| {
Some(builder.mk_call(&BOOL_TYPE, Operation::WellFormed, vec![val]))
})
.expect("quant defined");
builder.emit_prop(PropKind::Assume, exp);
// If this is ghost memory, assume it exists, and if it has an initializer,
// assume it has this value.
if let Some(spec_var) = struct_env.get_ghost_memory_spec_var() {
let mem_ty = mem.to_type();
let zero_addr = builder.mk_address_const(BigUint::zero());
let exists = builder.mk_call_with_inst(
&BOOL_TYPE,
vec![mem_ty.clone()],
Operation::Exists(None),
vec![zero_addr.clone()],
);
builder.emit_prop(PropKind::Assume, exists);
let svar_module = builder.global_env().get_module(spec_var.module_id);
let svar = svar_module.get_spec_var(spec_var.id);
if let Some(init) = &svar.init {
let mem_val = builder.mk_call_with_inst(
&mem_ty,
mem.inst.clone(),
Operation::Pack(mem.module_id, mem.id),
vec![init.clone()],
);
let mem_access = builder.mk_call_with_inst(
&mem_ty,
vec![mem_ty.clone()],
Operation::Global(None),
vec![zero_addr],
);
let eq_with_init =
builder.mk_bool_call(Operation::Identical, vec![mem_access, mem_val]);
builder.emit_prop(PropKind::Assume, eq_with_init);
}
}
}
// Append the old code
for bc in old_code {
builder.emit(bc);
}
builder.data
}
fn name(&self) -> String {
"entry_point_instrumenter".to_string()
}
}