Introduction

This files describes the contents of the main directory of b2llvm. This is a prototype (yet robust) implementation in Python for the code generation from B to LLVM. In addition, the directory also contains verification and validation artifacts. Further details are given hereafter.

Implementation

The implementation of the prototype is in Python and consists of the following

• b2llvm.py: main source file for a prototype of the translation in Python
• b2llvm: directory with custom modules for b2llvm.py
  • b2llvm/ast.py: Python encoding for B ASTs [todo: s/pict/classes/g]
  • b2llvm/bproject.py: Python class representing some settings of B projects
  • b2llvm/cache.py: Python class for cache. This class is used to store the result of computations that may need to perform several times and to avoid duplicate work.
  • b2llvm/codebuf.py: Python class to store text produced during code generation.
  • b2llvm/loadbxml.py: To load a BXML file into ASTs encodings.
  • b2llvm/names.py: To create LLVM identifiers.
  • b2llvm/opcode.py: Contains string templates to form LLVM source code one-liners.
  • b2llvm/printer.py: To generate human-readable texts corresponding to AST encodings (useful for debugging modules ast.py and loadbxml.py).
  • b2llvm/strutils.py: Custom string functionality.
  • b2llvm/trace.py: This module provides support to output traceability information.
  • b2llvm/translate.py: Generation of LLVM programs from B AST encodings.
• b2llvmio.llvm: LLVM module providing output functions for basic types that are used when the option --emit-printer is set.

V&V

The directory also contains elements for the verification and validation of the traduction

• bxml: directory with sample BXML files
  • bxml.xsd: schema defining the format of BXML files for B modules (from Clearsy)
  • project.xsd: schema defining the format of XML files for B projects (custom)
  • project.xml: settings for a B project (custom)
  • counter.bxml, counter_i.bxml: B machine and implementation of a simple counter (generated by Clearsy tools)
  • wd.bxml, wd_i.bxml: B machine and implementation of a watch-dog timer instantiates counter (generated by Clearsy tools)
  • timer.bxml, timer_r.bxml, timer_i.bxml: B machine, refinement and implementation of a timer instantiates counter (generated by Clearsy tools)
  • ibxml.xsd: (from Clearsy)
  • ioint.bxml: example of a base machine as opposed to a developed machine
  • mult.bxml: B machine and implementation to test arithmetic expressions (generated by Clearsy tools)
  • swap.bxml, swap_i.bxml: B machine and implementation to test assignment, operation parameters, local variables (generated by Clearsy tools)
  • switch.bxml, switch_i.bxml: B machine and implementation to test case instruction (generated by Clearsy tools, broken)
  • thr.bxml, thrdef.bxml: B machine and implementation to test sees clause (generated by Clearsy tools)
• bxml2text.py: Python script that reads a BXML file and prints the corresponding source code (uses b2llvm/ast.py, b2llvm/loadbxml.py, b2llvm/printer.py)
• scaffold-.llvm: some crafted LLVM files to animate LLVM implementation of different B projects.
• Makefile: produces bitcode for B projects. The produced bitcode may then be manually animated with lli-mp-3.1

Currently, the verification and validation infrastructure is functional for the following B projects: counter, wd and timer.

-- David Deharbe, January 2014.