Skip to content

Home

Jump to bottom
Mark Utting edited this page Jun 14, 2022 · 18 revisions

Welcome to the bil-to-boogie-translator wiki!

Architecture Overview of the Translator

Parser

[Unfinished]

The parser has two stages, the parsing phase and the walking phase.

Parsing 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.

Walking/Listening phase

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.

Analysis phases (including verification conditions)

Boogie code generation

TODO List

  • minor fixes to old-state version:
    • turning off constant propagation
    • adding examples.
    • update readme on how to run new examples
  • New Intermediate Representation (IR) Design:
    • review intermediate representation (State data structure)
    • 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

Design Decisions

  • 2022-06-01: decided to record design decisions.

Future Ideas

  • infer loop invariants
Clone this wiki locally