Skip to content

Commit 18baba2

Browse files
jyao15bors-diem
jyao15
authored and
bors-diem
committed
print new values of havocked variables in error trace
Closes: #446
1 parent 8d001ee commit 18baba2

File tree

12 files changed

+153
-11
lines changed

12 files changed

+153
-11
lines changed

‎language/move-prover/boogie-backend/src/boogie_wrapper.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ pub enum TraceEntry {
9696
Exp(NodeId, ModelValue),
9797
SubExp(NodeId, ModelValue),
9898
GlobalMem(NodeId, ModelValue),
99+
InfoLine(String),
99100
}
100101

101102
// Error message matching
@@ -384,6 +385,10 @@ impl<'env> BoogieWrapper<'env> {
384385
}
385386
}
386387
}
388+
InfoLine(info_line) => {
389+
// information that should be displayed to the user
390+
display.push(format!(" {}", info_line));
391+
}
387392
_ => {}
388393
}
389394
}
@@ -648,6 +653,10 @@ impl<'env> BoogieWrapper<'env> {
648653
let value = self.extract_value(value)?;
649654
Ok(TraceEntry::GlobalMem(node_id, value))
650655
}
656+
"info" => match value {
657+
Some(info_line) => Ok(TraceEntry::InfoLine(info_line.trim().to_string())),
658+
None => Ok(TraceEntry::InfoLine("".to_string())),
659+
},
651660
_ => Err(ModelParseError::new(&format!(
652661
"unrecognized augmented trace entry `{}`",
653662
name

‎language/move-prover/boogie-backend/src/bytecode_translator.rs‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -727,7 +727,17 @@ impl<'env> FunctionTranslator<'env> {
727727

728728
// Print debug comments.
729729
if let Some(comment) = fun_target.get_debug_comment(attr_id) {
730-
emitln!(writer, "// {}", comment);
730+
if comment.starts_with("info: ") {
731+
// if the comment is annotated with "info: ", it should be displayed to the user
732+
emitln!(
733+
writer,
734+
"assume {{:print \"${}(){}\"}} true;",
735+
&comment[..4],
736+
&comment[4..]
737+
);
738+
} else {
739+
emitln!(writer, "// {}", comment);
740+
}
731741
}
732742

733743
// Track location for execution traces.

‎language/move-prover/bytecode/src/debug_instrumentation.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ impl FunctionTargetProcessor for DebugInstrumenter {
9292
for idx in affected_variables {
9393
// Only emit this for user declared locals, not for ones introduced
9494
// by stack elimination.
95-
if idx < fun_env.get_local_count() {
95+
if !fun_env.is_temporary(idx) {
9696
builder.emit_with(|id| {
9797
Call(id, vec![], Operation::TraceLocal(idx), vec![idx], None)
9898
});

‎language/move-prover/bytecode/src/loop_analysis.rs‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,72 @@ impl LoopAnalysisProcessor {
171171
});
172172
}
173173

174+
// trace implicitly reassigned variables after havocking
175+
let affected_variables: BTreeSet<_> = loop_info
176+
.val_targets
177+
.iter()
178+
.chain(loop_info.mut_targets.iter().map(|(idx, _)| idx))
179+
.collect();
180+
181+
// Only emit this for user declared locals, not for ones introduced
182+
// by stack elimination.
183+
let affected_non_temporary_variables: BTreeSet<_> = affected_variables
184+
.into_iter()
185+
.filter(|&idx| !func_env.is_temporary(*idx))
186+
.collect();
187+
188+
if affected_non_temporary_variables.is_empty() {
189+
// no user declared local is havocked
190+
builder.set_next_debug_comment(format!(
191+
"info: enter loop {}",
192+
match loop_info.invariants.is_empty() {
193+
true => "",
194+
false => ", loop invariant holds at current state",
195+
}
196+
));
197+
} else {
198+
// show the havocked locals to user
199+
let affected_non_temporary_variable_names: Vec<_> =
200+
affected_non_temporary_variables
201+
.iter()
202+
.map(|&idx| {
203+
func_env
204+
.symbol_pool()
205+
.string(func_env.get_local_name(*idx))
206+
.to_string()
207+
})
208+
.collect();
209+
let joined_variables_names_str =
210+
affected_non_temporary_variable_names.join(", ");
211+
builder.set_next_debug_comment(format!(
212+
"info: enter loop, variable(s) {} havocked and reassigned",
213+
joined_variables_names_str
214+
));
215+
}
216+
217+
// track the new values of havocked user declared locals
218+
for idx_ in &affected_non_temporary_variables {
219+
let idx = *idx_;
220+
builder.emit_with(|id| {
221+
Bytecode::Call(
222+
id,
223+
vec![],
224+
Operation::TraceLocal(*idx),
225+
vec![*idx],
226+
None,
227+
)
228+
});
229+
}
230+
231+
// after showing the havocked locals and their new values, show the following message
232+
if !affected_non_temporary_variables.is_empty()
233+
&& !loop_info.invariants.is_empty()
234+
{
235+
builder.set_next_debug_comment(
236+
"info: loop invariant holds at current state".to_string(),
237+
);
238+
}
239+
174240
// add an additional assumption that the loop did not abort
175241
let exp =
176242
builder.mk_not(builder.mk_bool_call(ast::Operation::AbortFlag, vec![]));

‎language/move-prover/tests/sources/functional/aborts_if.exp‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,6 @@ error: function does not abort under this condition
6363
= at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
6464
= x = <redacted>
6565
= at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
66-
= <redacted> = <redacted>
6766
= at tests/sources/functional/aborts_if.move:147: abort_at_2_or_3_spec_incorrect
6867
= at tests/sources/functional/aborts_if.move:151: abort_at_2_or_3_spec_incorrect (spec)
6968

@@ -82,8 +81,6 @@ error: abort not covered by any of the `aborts_if` clauses
8281
= at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
8382
= x = <redacted>
8483
= at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
85-
= <redacted> = <redacted>
86-
= at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
8784
= ABORTED
8885

8986
error: abort not covered by any of the `aborts_if` clauses
@@ -102,8 +99,6 @@ error: abort not covered by any of the `aborts_if` clauses
10299
= at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
103100
= x = <redacted>
104101
= at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
105-
= <redacted> = <redacted>
106-
= at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
107102
= ABORTED
108103

109104
error: function does not abort under this condition

‎language/move-prover/tests/sources/functional/choice.cvc5_exp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ error: post-condition does not hold
5151
= at tests/sources/functional/choice.move:16: simple_incorrect
5252
= b = <redacted>
5353
= at tests/sources/functional/choice.move:17: simple_incorrect
54-
= <redacted> = <redacted>
5554
= result = <redacted>
5655
= at tests/sources/functional/choice.move:18: simple_incorrect
5756
= at tests/sources/functional/choice.move:22: simple_incorrect (spec)

‎language/move-prover/tests/sources/functional/choice.exp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ error: post-condition does not hold
5151
= at tests/sources/functional/choice.move:16: simple_incorrect
5252
= b = <redacted>
5353
= at tests/sources/functional/choice.move:17: simple_incorrect
54-
= <redacted> = <redacted>
5554
= result = <redacted>
5655
= at tests/sources/functional/choice.move:18: simple_incorrect
5756
= at tests/sources/functional/choice.move:22: simple_incorrect (spec)

‎language/move-prover/tests/sources/functional/invariants.exp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,6 @@ error: data invariant does not hold
4949
= at tests/sources/functional/invariants.move:143
5050
= at tests/sources/functional/invariants.move:158: lifetime_invalid_S_branching
5151
= a = <redacted>
52-
= <redacted> = <redacted>
5352
= x_ref = <redacted>
5453
= at tests/sources/functional/invariants.move:160: lifetime_invalid_S_branching
5554
= at tests/sources/functional/invariants.move:143

‎language/move-prover/tests/sources/functional/loops.exp‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@ error: abort not covered by any of the `aborts_if` clauses
1414
= at tests/sources/functional/loops.move:77: iter10_abort_incorrect
1515
= i = <redacted>
1616
= at tests/sources/functional/loops.move:79: iter10_abort_incorrect
17+
= enter loop, variable(s) i havocked and reassigned
18+
= i = <redacted>
19+
= loop invariant holds at current state
1720
= at tests/sources/functional/loops.move:80: iter10_abort_incorrect
1821
= at tests/sources/functional/loops.move:78: iter10_abort_incorrect
1922
= at tests/sources/functional/loops.move:82: iter10_abort_incorrect
@@ -28,6 +31,8 @@ error: unknown assertion failed
2831
= at tests/sources/functional/loops.move:233: iter10_assert_instead_of_invariant
2932
= i = <redacted>
3033
= at tests/sources/functional/loops.move:235: iter10_assert_instead_of_invariant
34+
= enter loop, variable(s) i havocked and reassigned
35+
= i = <redacted>
3136

3237
error: function does not abort under this condition
3338
┌─ tests/sources/functional/loops.move:58:9
@@ -38,6 +43,9 @@ error: function does not abort under this condition
3843
= at tests/sources/functional/loops.move:48: iter10_no_abort_incorrect
3944
= i = <redacted>
4045
= at tests/sources/functional/loops.move:50: iter10_no_abort_incorrect
46+
= enter loop, variable(s) i havocked and reassigned
47+
= i = <redacted>
48+
= loop invariant holds at current state
4149
= at tests/sources/functional/loops.move:51: iter10_no_abort_incorrect
4250
= at tests/sources/functional/loops.move:49: iter10_no_abort_incorrect
4351
= at tests/sources/functional/loops.move:58: iter10_no_abort_incorrect (spec)
@@ -67,6 +75,9 @@ error: induction case of the loop invariant does not hold
6775
= x = <redacted>
6876
= at tests/sources/functional/loops.move:222: loop_invariant_induction_invalid
6977
= at tests/sources/functional/loops.move:223: loop_invariant_induction_invalid
78+
= enter loop, variable(s) x havocked and reassigned
79+
= x = <redacted>
80+
= loop invariant holds at current state
7081
= at tests/sources/functional/loops.move:225: loop_invariant_induction_invalid
7182
= at tests/sources/functional/loops.move:221: loop_invariant_induction_invalid
7283
= x = <redacted>
@@ -84,6 +95,10 @@ error: induction case of the loop invariant does not hold
8495
= at tests/sources/functional/loops.move:185: loop_with_two_back_edges_incorrect
8596
= at tests/sources/functional/loops.move:188: loop_with_two_back_edges_incorrect
8697
= at tests/sources/functional/loops.move:189: loop_with_two_back_edges_incorrect
98+
= enter loop, variable(s) x, y havocked and reassigned
99+
= x = <redacted>
100+
= y = <redacted>
101+
= loop invariant holds at current state
87102
= at tests/sources/functional/loops.move:191: loop_with_two_back_edges_incorrect
88103
= y = <redacted>
89104
= at tests/sources/functional/loops.move:193: loop_with_two_back_edges_incorrect
@@ -100,6 +115,9 @@ error: base case of the loop invariant does not hold
100115
= y = <redacted>
101116
= at tests/sources/functional/loops.move:140: nested_loop_inner_invariant_incorrect
102117
= at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect
118+
= enter loop, variable(s) x, y havocked and reassigned
119+
= x = <redacted>
120+
= y = <redacted>
103121
= at tests/sources/functional/loops.move:144: nested_loop_inner_invariant_incorrect
104122
= at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect
105123

@@ -114,8 +132,14 @@ error: induction case of the loop invariant does not hold
114132
= y = <redacted>
115133
= at tests/sources/functional/loops.move:140: nested_loop_inner_invariant_incorrect
116134
= at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect
135+
= enter loop, variable(s) x, y havocked and reassigned
136+
= x = <redacted>
137+
= y = <redacted>
117138
= at tests/sources/functional/loops.move:144: nested_loop_inner_invariant_incorrect
118139
= at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect
140+
= enter loop, variable(s) y havocked and reassigned
141+
= y = <redacted>
142+
= loop invariant holds at current state
119143
= at tests/sources/functional/loops.move:147: nested_loop_inner_invariant_incorrect
120144
= y = <redacted>
121145
= at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect
@@ -132,6 +156,12 @@ error: induction case of the loop invariant does not hold
132156
= at tests/sources/functional/loops.move:115: nested_loop_outer_invariant_incorrect
133157
= at tests/sources/functional/loops.move:118: nested_loop_outer_invariant_incorrect
134158
= at tests/sources/functional/loops.move:119: nested_loop_outer_invariant_incorrect
159+
= enter loop, variable(s) x, y havocked and reassigned
160+
= x = <redacted>
161+
= y = <redacted>
162+
= loop invariant holds at current state
135163
= at tests/sources/functional/loops.move:122: nested_loop_outer_invariant_incorrect
164+
= enter loop, variable(s) y havocked and reassigned
165+
= y = <redacted>
136166
= x = <redacted>
137167
= at tests/sources/functional/loops.move:119: nested_loop_outer_invariant_incorrect

‎language/move-prover/tests/sources/functional/loops_with_memory_ops.exp‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,24 @@ error: unknown assertion failed
2525
= at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
2626
= at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
2727
= at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
28+
= enter loop, variable(s) a, b, i, x, y havocked and reassigned
29+
= a = <redacted>
30+
= b = <redacted>
31+
= i = <redacted>
32+
= x = <redacted>
33+
= y = <redacted>
34+
= loop invariant holds at current state
2835
= at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
2936
= at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
3037
= at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
3138
= at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
3239
= at tests/sources/functional/loops_with_memory_ops.move:73: nested_loop2
40+
= enter loop, variable(s) x, y havocked and reassigned
41+
= x = <redacted>
42+
= y = <redacted>
3343
= at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
44+
= enter loop, variable(s) y havocked and reassigned
45+
= y = <redacted>
3446
= b = <redacted>
3547
= a = <redacted>
3648
= at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
@@ -64,12 +76,24 @@ error: induction case of the loop invariant does not hold
6476
= at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
6577
= at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
6678
= at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
79+
= enter loop, variable(s) a, b, i, x, y havocked and reassigned
80+
= a = <redacted>
81+
= b = <redacted>
82+
= i = <redacted>
83+
= x = <redacted>
84+
= y = <redacted>
85+
= loop invariant holds at current state
6786
= at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
6887
= at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
6988
= at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
7089
= at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
7190
= at tests/sources/functional/loops_with_memory_ops.move:73: nested_loop2
91+
= enter loop, variable(s) x, y havocked and reassigned
92+
= x = <redacted>
93+
= y = <redacted>
7294
= at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
95+
= enter loop, variable(s) y havocked and reassigned
96+
= y = <redacted>
7397
= b = <redacted>
7498
= a = <redacted>
7599
= at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2

0 commit comments

Comments
 (0)