Home

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

Architecture Overview of the Translator

• Parser
• Analysis phases (including verification conditions)
• Boogie code generation

TODO List

• review intermediate representation (State data structure)
• 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)

Design Decisions

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

Future Ideas

• infer loop invariants