Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Boogie Backend Redesign #153

Open
DavePearce opened this issue May 12, 2022 · 3 comments
Open

Boogie Backend Redesign #153

DavePearce opened this issue May 12, 2022 · 3 comments

Comments

@DavePearce
Copy link
Member

DavePearce commented May 12, 2022

(see also #72, #120 and #142)

This is an attempt to log the various problems with the current approach.

  • Functions. Translating a Whiley function as a boogie function is fraught with difficulties (why?). A better solution would be to translate them as procedures. This has a bunch of knock-on effects. In particular, we cannot use preconditions / postconditions in procedures. Instead, we must use assume and assert statements. Also, it means function calls have to be pulled out of expressions. In effect, we end up with something much closer to bytecode.
  • Properties. These are translated into boogie functions. But, how do we enforce their preconditions / postconditions (e.g. parameter / return types). Likewise, internal consistency requirements, such as indices within bounds? Potentially, a separate property check procedure is required for this.
  • Control Flow. Current challenges with extracting method calls from conditions mean that we often fall back to unstructured control-flow (e.g. for loops). Overall, I thing its simply better to do this all the time.
  • Boxing / Unboxing. It should be possible to eliminate the need for boxing / unboxing. This can done using algebraic datatypes, and types like Vec. See also Boogie Sequences #109. Questions remain around the heap and template.
  • Types. Dafny uses something like <A>[ref, Field A]A for representing parts of the heap (see Memory T below). Boogie also has built-in support for "sequences" (see here), and supports tuple assignments.
  • Casts. These appear to be a problem in my current design.
  • Error Reporting. You can supply messages in assertions which can help with error reporting (see here). Syntax is {:msg "your text goes here"}
@DavePearce
Copy link
Member Author

DavePearce commented May 12, 2022

Some observations from the move prover (see here):

  • Defines Vec T for implementing arrays.
  • Defines Memory T for implementing a memory holding type T.
  • Defines specific bitwise operators over int types. This will be useful for Whiley when I remove byte.

See also this paper:

@DavePearce
Copy link
Member Author

DavePearce commented May 14, 2022

More thoughts:

  • Will need overflow checking for fixed-width types
  • Can a procedure ever be pure? If not cannot implement Whiley function perfectly using them.
  • Can property call functions? If not, could inline their preconditions. Also use a separate check for their return values / internal conditions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant