From 42cdb1b8948415dd103648b66b73a380ef49850f Mon Sep 17 00:00:00 2001 From: David Dill Date: Thu, 7 Apr 2022 20:29:34 -0700 Subject: [PATCH] [move-prover] Report error for unsupported bit operators This bug fix responds to issue #166 "MVP proves arbitrary postconditions when unsupported operators exist." I STILL DO NOT UNDERSTAND SOME OF THE BEHAVIOR. The fix simply reports the unsupported operator as an error when it is encountered. This is a one line change in bytecode_translator.rs. I added a test case tests/sources/functional/unsupported.move for this problem. NOTE: The previous behavior was that, when the bytecode was encountered, the bytecode_translater emitted a comment saying the operator was not supported, and then an "assert false". When Boogie is run stand-alone, it generates and output.bpl.log file with an error trace. However, the prover doesn't seem to notice this and report it with an error trace. The failure is worse than that because (according to the reported bug), the prover doesn't report errors on incorrect postconditions. So, I think we should understand what's going on here and try to make sure there are not other related bugs that could result in false negatives from unreported errors. Closes: #201 --- .../boogie-backend/src/bytecode_translator.rs | 1 + .../tests/sources/functional/unsupported.exp | 6 ++++++ .../tests/sources/functional/unsupported.move | 13 +++++++++++++ 3 files changed, 20 insertions(+) create mode 100644 language/move-prover/tests/sources/functional/unsupported.exp create mode 100644 language/move-prover/tests/sources/functional/unsupported.move diff --git a/language/move-prover/boogie-backend/src/bytecode_translator.rs b/language/move-prover/boogie-backend/src/bytecode_translator.rs index 9c9aff28fc..426423707f 100644 --- a/language/move-prover/boogie-backend/src/bytecode_translator.rs +++ b/language/move-prover/boogie-backend/src/bytecode_translator.rs @@ -1421,6 +1421,7 @@ impl<'env> FunctionTranslator<'env> { ); } BitOr | BitAnd | Xor => { + env.error(&loc, "Unsupported operator"); emitln!( writer, "// bit operation not supported: {:?}\nassert false;", diff --git a/language/move-prover/tests/sources/functional/unsupported.exp b/language/move-prover/tests/sources/functional/unsupported.exp new file mode 100644 index 0000000000..4282eeb945 --- /dev/null +++ b/language/move-prover/tests/sources/functional/unsupported.exp @@ -0,0 +1,6 @@ +Move prover returns: exiting with condition generation errors +error: Unsupported operator + ┌─ tests/sources/functional/unsupported.move:7:37 + │ +7 │ public fun foo(i: u64): u64 { i & 0 } + │ ^ diff --git a/language/move-prover/tests/sources/functional/unsupported.move b/language/move-prover/tests/sources/functional/unsupported.move new file mode 100644 index 0000000000..8cfc6daa23 --- /dev/null +++ b/language/move-prover/tests/sources/functional/unsupported.move @@ -0,0 +1,13 @@ +// false negatives for unsupported operators + +address 0x123 { + + module M { + + public fun foo(i: u64): u64 { i & 0 } + + spec foo { ensures false; } // :( + + } + +}