[preview | do not merge] motoko-san contributions by Serokell #4500
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
The `moc --viper` command outputs generated Viper code to stdout and diagnostic messages to stderr. * Prior to this change, test/run.sh used the `run` helper to produce .vpr files. The `run` helper always merges stdout and stderr, which results in ill-formed .vpr files if there are any diagnostic messages. * Now test/run.sh has an additional helper `run_stderr` that keeps stdout and stderr separate. By using it instead of `run` we ensure that .vpr files are not contaminated with diagnostics. Run `make -C test/viper` to confirm that this fixes broken Viper tests. Note that `run_stderr` is a copy of `run` with minor tweaks, so this solution introduces some technical debt. A more principled approach would be to separate stdout and stderr in all commands (i.e. wholly replace `run` with `run_stderr`), but I opted not to do that at this time to avoid a massive overhaul of the test suite.
New features: * arguments and return values of primitive types (Int, Bool) * multiple function arguments * early return from functions New test cases: * test/viper/simple-funs.mo * test/viper/counter.mo
|
Dear @int-index, In order to potentially merge your code in this open-source repository and therefore proceed with your contribution, we need to have your approval on DFINITY's CLA. If you decide to agree with it, please visit this issue and read the instructions there. Once you have signed it, re-trigger the workflow on this PR to see if your code can be merged. — The DFINITY Foundation |
New features: * invariants in while-loops New test cases: * test/viper/loop-invariant.mo
|
Could you add instructions here on how to get the current version of the tool working with the motoko-san extension, please? |
aterga
reviewed
Apr 17, 2024
Bug fixes: * pretty-printing of MethodCallS * arguments in private functions * calls with n=1 arguments New features: * method calls in let/var declarations * method calls in assignments * method calls in return statements New test cases: * test/viper/method-call.mo
New features: * translate Nat to Int New test cases: * test/viper/nats.mo Future work: encode in Viper that Nats are non-negative.
Problem: Currently used z3 version abnormally fails on GA macOS runners. Solution: Use 'z3_4_12' instead of 'z3' in nix setup.
[DMS-31] motoko-san: enable viper tests
+ add type into into `ctxt.ids` to be able generate loop invariants + make internal function `args` return Motoko type to be able save their type into ctxt.ids + make internal function `rets` return also access predicates
New features: * monomorphise method calls before translation New test cases: * test/viper/polymono.mo
Problem: permissions are reset incorrectly. Namely, after initialization write access was dropped by exhaling full permission which leads to forgetting assigned before values Solution: do not exhale anything for mutable array and exhale-inhale wildcard for immutable which models losing write access better
crusso
reviewed
May 8, 2024
src/viper/prelude.ml
Outdated
| field $bool: Bool | ||
| field $ref: Ref | ||
| field $array: Array | ||
| /* END PRELUDE */|prelude} |
There was a problem hiding this comment.
Suggested change
| /* END PRELUDE */|prelude} | |
| /* END PRELUDE */|prelude} | |
crusso
reviewed
May 8, 2024
| let body' = ActorU(id_opt, decs') in | ||
| (* let _ = List.map (fun d -> print_endline (Wasm.Sexpr.to_string 80 (Arrange.dec_field d))) decs' in *) | ||
| { u with it = {imports; body = { body with it = body' } } } | ||
| | _ -> u |
There was a problem hiding this comment.
Suggested change
| | _ -> u | |
| | _ -> u | |
crusso
reviewed
May 8, 2024
|
|
||
| let mono_calls_visitor (stk : mono_goal Stack.t) : visitor = | ||
| { visit_exp = (function | ||
| | {it = CallE({it = VarE v; at = v_at; note = v_note},inst,e); at; note} -> |
There was a problem hiding this comment.
Curious: how would you handle first-class uses of a polymorphic functions? Create a record of monomorphic ones?
There was a problem hiding this comment.
Yes, in case of higher-rank usage that would be a plausible strategy. A record of monomorphic functions could indeed represent a finite set of instantiations of a polymorphic function.
However, a first-class use is not necessarily higher-rank. E.g. in map(f, xs) where f is polymorphic, it wouldn't be necessary to turn f into a record of functions because all elements xs are of a single type. So we will end up with e.g. map$Int(f$Int, xs) if the elements are integers.
Actual higher-rank usage is rare in practice and I'm not sure if we should invest effort into supporting it.
crusso
reviewed
May 8, 2024
| @@ -5,3 +5,4 @@ assert:return true; | |||
|
|
|||
| // `invariant` is a keyword in verification mode only | |||
| assert:invariant true; | |||
| assert:loop:invariant true; | |||
There was a problem hiding this comment.
Suggested change
| assert:loop:invariant true; | |
| assert:loop:invariant true; | |
crusso
reviewed
May 8, 2024
| }; | ||
| return j; | ||
| }; | ||
| } |
Problem: tuples cause parsing errors in code like the following: ($prj(t1, 0)).$int := a ($prj(t1, 1)).$int := b Solution: add a semicolon at the end of each statement
Refactor and improve assign_stmts to allow field assignment and automatically create temporary variables. Co-authored-by: Golovin Pavel <gopavel0@gmail.com>
* unify the VarD cases in dec_field' * reuse assign_stmts for initialization * generalize access_pred to expression LHSs * remove unused ctxt argument in array_size_inv * use seqn' in (ghost_)inits
* introduce the var:return syntax to refer to the result variable in assertions * fix a validation failure in reverse.mo using the new syntax
Co-authored-by: Golovin Pavel <gopavel0@gmail.com>
…s-in-switch-patterns [DMS-40] Support numeric, boolean literals and wildcards in switch patterns
Problem: `await Reverse.reverse()` hangs (infinite loop) Diagnosis: `i` in copy_xarray wasn't being incremented Solution: add the increment, as well as assertions to ensure sufficient array access permissions
This change fixes the Viper translation of let-bound variants by removing normalization from `infer_exp` in `typing.ml`, thus making the nominal type accessible in `trans.ml`
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.
This PR serves as a platform to preview and discuss the ongoing work to extend
motoko-sanwith new features. This is only a work-in-progress at the moment but we welcome all feedback!