experiment: Viper integration #3477
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Which viper is that? |
|
|
Nice! |
Adds reverse (Viper -> Motoko) source region mapping.
* clean up junk * split `pp_stmt` * do XON/XOFF wrapping centrally in `pp_stmt` * `prog_mapped` also points to the right (generated) file
Set up testing infrastructure for Viper - moved tests to `test/viper` - added `Makefile` - augmented `run.sh` - accepted initial output - the `.vpr` files are also checked with `silicon` backend Run these by `make -C test/viper` but this is not (yet) added to the outer `Makefile`.
This implements actor-global invariants. They get (currently) declared with a actor-level `assert` and translated to a Viper macro, that gets both `require`d and `ensure`d from each method by calls to those macros. TODOs: - [ ] find better syntax - [x] use invariant(s) for pre/postconditions on each actor method - [x] `self` access in `define` - [x] `__init__` should only have a postcondition (depends on #3486) - [x] allow more than one invariant
…3486) This PR extends the Motoko to Viper translation with initialization statements for each actor private field. These statements form the body of a special `__init__` method (that establishes the canister's invariant for the first time). Main assumptions: * Initializing expressions can be translated as expressions; no imperative code (a.k.a. Viper statements) needs to be used * The name `__init__` is not used elsewhere in the program * The method `__init__` should be supplied with permissions to write into each actor private field (alternatively, the translation would need to be extended with `inhale` statements corresponding to each field)
This changes the srcloc of certain Viper subexpression to better track the original Motoko.
It still has somewhat outdated backends, but we never had problems with those. But this gives a non-moving download URL, so that's a win!
Just look in `src/mo_def/arrange.ml`.
ggreif
force-pushed
the
viper
branch
2 times, most recently
from
98c563f
to
55af544
Compare
Turns out I was doing a bunch of things wrong. Now we make the relevant `Lexer_lib.mode` accessible from the parser productions (previously it just accessed a constant thing). This makes `--viper` to select the `verification` mode in the parser too (lexer was already fine).
|
Can |
Yes. We desugar it to the mathematical thing. That uses $ env MOC_UNLOCK_VERIFICATION=1 rlwrap moc
> false implies (1 / 0 == 1);
> stdin:1.16-1.21: execution error, arithmetic overflowInput: $ cat short.mo
false implies (1 / 0 == 1);Compiled: $ env MOC_UNLOCK_VERIFICATION=1 rlwrap moc -wasi-system-api short.mo
$ wasmtime short.wasm
$ echo $?
0 |
ggreif
reviewed
Nov 22, 2022
This PR adds a readme file that covers the following aspects behind Formal Motoko: (1) Disclaimer; (2) Introduction — Overview | Formal specification | Static vs. dynamic assertions | Testing vs. formal verification | Precondition of public functions | Examples; (3) Contributing — Building | Running | Testing | File structure | Further information
aterga
approved these changes
Nov 25, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Motoko-san, an experimental verification method
This PR adds (very experimental) Viper code generation from (a limited subset of) Motoko. This is a proof of concept, showing that we can generate appropriate assertions so that Viper can diagnose concurrency (e.g. re-entrancy) bugs. A few tests are provided to demonstrate this.
Note that this is (a.t.m.) not directed towards the general public, rather towards folks with verification experience.
To use the Viper capabilities
--viperon the command line (Viper generation)env MOC_UNLOCK_VERIFICATION=1(regular compilation using extended grammar)When the verification features are enabled, a convenience logical operator
impliesbecomes a keyword. It has the following truth table:impliesb