Skip to content

Commit

Permalink
[move-prover] fix error filtering in boogie-wrapper
Browse files Browse the repository at this point in the history
Currently the prover collects three types of errors from Boogie:
- verification errors
- inconclusive errors
- inconsistency errors

In addition, in the collector for verification errors, there is a check
that if an error message does not belong to other known categories of
errors, it will mark the error message as an unknown boogie error.

Unfortunately the filter is not working now (maybe because Boogie has
changed the output format), leading to error messages being marked as
unknown (while they should be marked as inconclusive).

This commit re-organized the error parsing logic and uses the REGEX
patterns consistently for both early filtering as well as actual error
parsing.

Closes: aptos-labs#8541
meng-xu-cs authored and bors-libra committed Jun 15, 2021
1 parent 2860098 commit bcfe3b5
Showing 1 changed file with 20 additions and 19 deletions.
39 changes: 20 additions & 19 deletions language/move-prover/boogie-backend/src/boogie_wrapper.rs
Original file line number Diff line number Diff line change
@@ -90,6 +90,18 @@ pub enum TraceEntry {
Exp(NodeId, ModelValue),
}

// Error message matching
static VERIFICATION_DIAG_STARTS: Lazy<Regex> =
Lazy::new(|| Regex::new(r"(?m)^assert_failed\((?P<args>[^)]*)\): (?P<msg>.*)$").unwrap());

static INCONCLUSIVE_DIAG_STARTS: Lazy<Regex> = Lazy::new(|| {
Regex::new(r"(?m)^.*\((?P<line>\d+),(?P<col>\d+)\).*Verification(?P<str>.*)(inconclusive|out of resource|timed out).*$")
.unwrap()
});

static INCONSISTENCY_DIAG_STARTS: Lazy<Regex> =
Lazy::new(|| Regex::new(r"(?m)^inconsistency_detected\((?P<args>[^)]*)\)").unwrap());

impl<'env> BoogieWrapper<'env> {
/// Calls boogie on the given file. On success, returns a struct representing the analyzed
/// output of boogie.
@@ -355,26 +367,19 @@ impl<'env> BoogieWrapper<'env> {

/// Extracts verification errors from Boogie output.
fn extract_verification_errors(&self, out: &str) -> Vec<BoogieError> {
// Need to add any diag which is not processed by this function (like
// inconclusive) to this list so its not reported as unexpected boogie
// output.
const OTHER_DIAG_START: &[&str] = &[
"inconclusive",
"out of resource",
"timed out",
"inconsistency_detected",
];
static VERIFICATION_DIAG_STARTS: Lazy<Regex> = Lazy::new(|| {
Regex::new(r"(?m)^assert_failed\((?P<args>[^)]*)\): (?P<msg>.*)$").unwrap()
});
let mut errors = vec![];
let mut at = 0;
while let Some(cap) = VERIFICATION_DIAG_STARTS.captures(&out[at..]) {
let inbetween = out[at..at + cap.get(0).unwrap().start()].trim();
at = usize::saturating_add(at, cap.get(0).unwrap().end());
let msg = cap.name("msg").unwrap().as_str();

if !inbetween.is_empty() && !OTHER_DIAG_START.iter().any(|s| inbetween.starts_with(s)) {
// Filter diags that we know and will be processed later (e.g., inconclusive).
// Other unknown diags will be reported as unexpected boogie output.
if !inbetween.is_empty()
&& !INCONCLUSIVE_DIAG_STARTS.is_match(inbetween)
&& !INCONSISTENCY_DIAG_STARTS.is_match(inbetween)
{
// This is unexpected text and we report it as an internal error
errors.push(BoogieError {
kind: BoogieErrorKind::Internal,
@@ -574,10 +579,7 @@ impl<'env> BoogieWrapper<'env> {

/// Extracts inconclusive (timeout) errors.
fn extract_inconclusive_errors(&self, out: &str) -> Vec<BoogieError> {
let diag_re =
Regex::new(r"(?m)^.*\((?P<line>\d+),(?P<col>\d+)\).*Verification(?P<str>.*)(inconclusive|out of resource|timed out).*$")
.unwrap();
diag_re
INCONCLUSIVE_DIAG_STARTS
.captures_iter(&out)
.filter_map(|cap| {
let str = cap.name("str").unwrap().as_str();
@@ -614,8 +616,7 @@ impl<'env> BoogieWrapper<'env> {

/// Extracts inconsistency errors.
fn extract_inconsistency_errors(&self, out: &str) -> Vec<BoogieError> {
let diag_re = Regex::new(r"(?m)^inconsistency_detected\((?P<args>[^)]*)\)").unwrap();
diag_re
INCONSISTENCY_DIAG_STARTS
.captures_iter(&out)
.map(|cap| {
let args = cap.name("args").unwrap().as_str();

0 comments on commit bcfe3b5

Please sign in to comment.