-
Notifications
You must be signed in to change notification settings - Fork 0
Home
Welcome to the bil-to-boogie-translator wiki!
[Unfinished]
The parser has two stages, the parsing phase and the walking phase.
In the parsing phase primarily depends on the rules laid out in the BilAdt.g4 grammar file. The text is converted into lexical tokens, which are then parsed to form a parse tree.
Antlr does this by compiling (converting?) the grammar into java source, which is capable of taking a string input and creating the aforementioned parse tree.
The Walking/Listening phase primarily depends on the AdtStatementLoader.scala file. The Antlr walker essentially traverses the parse tree generated in the previous phase, and performs actions when entering and exiting each token.
The primary goal of this stage is to produce a "State" data structure from our parse tree, which is our representation of the program. We output information from this stage such as the list of statements, and we also keep a dictionary of expressions which we use in the statements.
- review intermediate representation (State data structure)
- add some examples for new ADT parser
- update readme on how to run new examples
- update tests
- investigate ARM stack semantics
- cleanup generation of memory accesses
- generating rely-guarantee & verification conditions only when needed (memory accesses, branches etc)
- combine reg31 and stack pointer
- review constant propagation and folding
- use information from new parser
- split inference from replacing?
- start with simple boolean security levels
- fix rely conditions and implement guarantees
- alternate representation to bit-vectors
- use ints instead where possible
- or simple booleans for single bits
- improved memory model
- points-to analysis (partition memory)
- investigate LLVM data structure analysis algorithm (https://llvm.org/pubs/2007-06-10-PLDI-DSA.pdf)
- separate stack from heap (more reliably)
- 2022-06-01: decided to record design decisions.
- infer loop invariants