Table Of Contents

Welcome to the Sireum Bakar v2 Documentation

author:Jason Belt, Zhi Zhang, Jakub Jedryszek, Robby
contact:{ belt, zhangzhi, jjedrys, robby } @k-state.edu
organization:SAnToS Laboratory, Kansas State University
last updated:November 08, 2013; 02:23 PM

Acknowledgement

The development of Sireum Bakar is supported in part by the US Air Force Office of Scientific Research grant no. FA9550-09-0138 and the US National Science Foundation (NSF) CAREER award CCF-0644288.

Introduction

Getting Started

Sireum Core repository stores some of the core components of the Sireum (v2) software analysis platform.

Sireum Bakar repository stores various Spark/Ada translation tools and source code analysis and verification tools, which are built on top of Sireum Core components. It provides a useful development platform and can be extended to build various kinds of software static analyzers.

Setting up Development Environment

  1. Download and install Sireum (development release) by following the instructions at: http://www.sireum.org/download.

  2. Launch Sireum Development Environment (DE) (add -h for help to supply custom Eclipse command-line arguments such as configuring memory):

    sireum launch sireumdev

    Pick a directory for your workspace when asked. Moreover, agree when asked to run Scala diagnostics; enable JDT Weaving for Scala IDE and then quit DE; relaunch Sireum DE.

  3. Add SIREUM_HOME/apps/platform/java in Eclipe’s Java Installed JREs preference page, and make it the default. In addition, set Eclipse’s Java Compiler compliance level to 1.7. (If Eclipse shows you a dialog box indicating that “Subversive Native Library Not Available”, it means that you do not have native SVN installed; click Ok to close the dialog box. You can correct this issue by setting SVN Interface Client to “SVNKit” in the Eclipse’s Team->SVN preference page.)

  4. Import all projects in:

    • Sireum Core Prelude Repo
      • read-only: https://github.com/sireum/prelude.git
      • read-write: git@github.com:sireum/prelude.git
    • Sireum Parser Repo
      • read-only: https://github.com/sireum/parser.git
      • read-write: git@github.com:sireum/parser.git
    • Sireum Core Repo
      • read-only: https://github.com/sireum/core.git
      • read-write: git@github.com:sireum/core.git

    This should import projects such as sireum-core-test.

  5. Run all Sireum Core tests by right clicking the project sireum-core-test and selecting Run As and then Scala JUnit Test; all tests should pass.

  6. If you are making changes to the codebase, import the following in the respective Eclipse preference pages:

    Make sure to run Java source clean up before committing Java code. Similarly, make sure to run Scala formatter before committing Scala code.

Sireum Bakar Tool Sets

Import Sireum Bakar projects at:

  • read-only: https://github.com/sireum/bakar.git
  • read-write: git@github.com:sireum/bakar.git

Note

Steps to import a project in Git: Click the following Eclipse menus: Window > Show View > Other... > Git > Git Repositories, select Clone a Git Repository and add the clone to this view, and then put the git location, for example https://github.com/sireum/bakar.git, at URI. Finally, unfold the Git repository and right click Working Directory and choose Imports Projects... to import all projects under the Git repository into current Eclipse working space.

sireum is a software analysis platform developed by KSU SAnToS group,

bakar means spark, and

jago means coq in Indonesian.

Spark and Ada Front-End: Translators

Overview

This section describes various translators for Spark/Ada 2012 program representation to representations using different programming/input languages.

Ada-to-XML Translator: gnat2xml

gnat2xml translates Ada 2012 programs to a fully resolved Abstract Syntax Tree (AST) XML representation with an accompanying XML schema. The representation is based on GNAT ASIS representation, but the AST definitions are designed to be “typed”; that is, in contrast to ASIS where AST nodes are generic, AST kinds representing different language features have different types represented in the XML schema (as distinct complex types). The generated XML representation of Ada programs retains the following information:

  1. Symbol information
  2. Type information
  3. Location information

The most recent generated schema (with KSU patches) can be found at:

https://github.com/sireum/bakar/blob/master/sireum-bakar-xml/src/main/resources/gnatxml.xsd

The gnat2xml source code is available at:

The initial version of gnat2xml is developed by AdaCore, Inc. as a sub-contract of Kansas State University’s U.S. Air Force Office of Scientific Research (AFOSR) award No. FA9550-09-0138. It is licensed under the GNU Public License (GPL) v3.

Java Target

Contact

Jason Belt

The Bakar Java translator generates Java binding from gnat2xml-generated schema using the Java Architecture for XML Binding (JAXB – http://jaxb.java.net), which is a part of the Java Standard Development Kit.

To fine-tune JAXB generated Java classes, we developed a custom JAXB binding, which can be found at:

https://github.com/sireum/bakar/blob/master/sireum-bakar-xml/src/main/resources/external.xsd

The generated classes can be found at:

https://github.com/sireum/bakar/tree/master/sireum-bakar-xml/src/main/java/org/sireum/bakar/xml

By using the JAXB runtime library, gnat2xml-generated Ada XML representations can be directly loaded as Java objects (instances of the Java classes generated by using JAXB).

Scala Target

Contact

Jason Belt

The Bakar Scala Translator generates Scala extractor object definitions. The main purpose is to be enable pattern matching of Ada JAXB Java objects. The translator uses Java reflection on JAXB generated Java classes in order to generate the extractors.

The generated extractors are available at:

https://github.com/sireum/bakar/tree/master/sireum-bakar-xml/src/main/scala/org/sireum/bakar/xml

Jago: Coq and OCaml Targets

Contact

Zhi Zhang

There are two kinds of Bakar Jago translators provided for the Coq and OCaml targets: (1) Type Translator, which translates gnat2xml-generated Ada XML Schema to (inductive) type definitions in Coq and OCaml, and (2) Program Translator, which translates Ada programs from gnat2xml-generated Ada fully resolved AST XML to Coq and OCaml code that constructs the AST.

Note

The Jago translation toolset currently handles a subset of SPARK 2014. Pre/Post aspects are not handled as the GNAT toolset version for the initial gnat2xml tool does not allow contracts to be attached directly to subprogram bodies.

Type Translator

Similar to the Bakar Scala Translator, the Bakar Jago Type Translator uses Java reflection on JAXB generated Java classes in order to generate Coq and OCaml type definitions. The translator uses a template-based approach; this allows us to use the same translator codebase for the Coq and OCaml targets by using two templates.

Below are a couple of design guidelines that we used when developing the translator:

  1. The generated AST type definitions should be based on CompCert Cminor AST definitions.

    For example, Cminor uses non-negative values to represent identifiers; we follow this style by using natural numbers to represent identifiers/names. More concretely, for example, idnum denotes local/global variables and has type nat, procnum denotes subprogram names, pkgnum denotes package names, and typenum denotes either standard data types or user defined types. The AST structure for expressions and statements is also organized in the same way as Cminor.

  2. The generated AST type should preserve fully resolved AST information.

    This is in contrast to Cminor where we have, for example, type information for (sub-) expressions, symbol information, and location information, etc. To ease attaching such information on AST nodes, we assign a unique number for each AST node that serves as keys for various tables (e.g., type tables).

  3. The generated OCaml AST type definitions should be the same as the result of extracting Coq AST type definitions to OCaml (with some extraction configuration to represent native types such as nat and bool).

The generated type definitions are avaiable at:

Program Translator

Given gnat2xml-generated Ada XML representations, the Bakar Jago Program Translator uses JAXB to load the representations as Java objects (instances of Bakar Java Translator generated classes) and use the Scala extractors produced by the Bakar Scala Translator to translate the Ada AST to Coq and OCaml. Similar to the Type Translator, the Program Translator uses a template-based approach.

Jago Command-Line Options

Three steps are needed to do type and program translations for Ada:

  1. Ada XML Schema and Ada XML AST must be generated using gnat2xml
  2. Java classes and Java objects must be generated for Ada XML Schema and Ada XML AST
  3. Do type and program translation for Ada based on its corresponding Java classes and Java objects

Step 1 and 2 are necessary preprocessing operations in our Jago translation tool chain, so make sure that the tool gnat2xml is installed and available in current envirenment before running Jago translator.

Usage:

./sireum bakar mode [options] [<src-files>] [<Output file>], where
  • sireum is a software analysis platform developed by KSU SAnToS group, bakar means spark in Indonesian, and ./sireum bakar is a toolset for analyzing Spark/Ada program.
  • mode provides a switch between Type Translator and Program Translator. Available modes:
    • type: generate type definitions
    • program: translation of Spark/Ada programs
  • available options using type switch are:
    • -h | --help
    • -t | --type  [Default: Coq, Choices: (Ocaml, Coq)]
  • available options using program switch are:
    • -h | --help
    • -p | --program  [Default: Coq, Choices: (Ocaml, Coq)]
  • src-files specifies the Spark/Ada programs to be translated by Program Translator and it’s only used in program switch
  • Output file denotes the target file where the translated objects are written into. The translation results are printed in console if Output file is not supplied

Examples:

  • $ ./sireum bakar type -t Coq (in Windows: sireum bakar type -t Coq)
    • this command calls the Type Translator to generate Coq type definitions for Ada XML schema and print the results on console
  • $ ./sireum bakar type -t Ocaml typ.ocaml
    • this command calls the Type Translator to generate Ocaml type definitions for Ada XML schema and write the results in typ.ocaml
  • $ ./sireum bakar program -p Coq linear_div_fn.adb
    • this command calls the Program Translator to generate Coq objects for Spark/Ada program linear_div_fn.adb and print the results on console
  • $ ./sireum bakar program -p Ocaml linear_div_fn.adb ~/o.ocaml
    • this command calls the Program Translator to translate Spark/Ada program linear_div_fn.ada into Ocaml program and write the results into o.ocaml under the user home directory

Example

Consider a simple Spark example that is available at:

https://github.com/sireum/bakar/blob/master/sireum-bakar-test/src/test/resources/org/sireum/example/bakar/2012-gnat/jago/linear_div_with_loopInvariant.adb

Below are the generated program definitions by the Bakar Jago Program Translator:

In the generated Coq or OCaml representations, the Spark program is translated into a CompilationUnit data structure as defined in Coq AST type or OCaml AST type. Take the Coq representations as example:

  • Library_Unit consists of three elements:
    • the nat number 1 is its AST number
    • the Libray_Subprogram structure represents the procedure body declaration
    • the data structure tt_exptype_table and tt_typename_table are the type table for expressions referred to in the compilation unit
  • Library_Subprogram consists of:
    • its AST number 2, and
    • procedure body declaration represented as Procedure structure
  • Procedure consists of:
    • its AST number 3
    • the procedure body declaration with a record
  • Procedure represents the procedure, and Function represents the function.

    For the procedure defined by Procedure, it consists of:

    • procedure_astnum is the procedure’s AST number
    • procedure_name is the procedure name
    • procedure_contracts defines the aspect specification (for example Pre or Post) for the procedure
    • procedure_parameter_profile defines a list of parameters
    • procedure_declarative_part declares a list of local variables used in the procedure
    • procedure_statements is the procedure body, which consists of a sequence of statements
  • Each assignment is constructed with S_Assignment.

    For example, assignment Remainder := Dividend will be translated into the following OCaml program:

    S_Assignment (13, (*Remainder*) 4, Evar (14, (*Dividend*) 1))

    where:

    • 13 is the AST number for the assignment statement
    • 4 is the identifier number for left-hand side variable Remainder
    • 14 is the AST number for the variable expression Dividend, which is represented with identifier number 1
  • Loop Invariant is defined as a statement and it’s represented with S_Loop_Invariant, which is only allowed to appear in the loop.

  • The type table for the package body is a record, which consists of two fields:

    • tt_exptype_table is a type table that maps the expression AST number to its type number
    • tt_typename_table is a type table that maps the type number to the type URI and the AST number declaring it if it is a user defined type. Integer and Boolean are standard types, so there is no declaring AST number (hence, None for its declaring AST number).

    For example, the pair (47, 1) in tt_exptype_table indicates the expression AST node numbered 47, which is Remainder - Divisor, has the type 1. According to tt_typename_table, 1 is an Integer defined in Standard.

Jago: Formalization for SPARK 2014 Subset in Coq

Overview

From HILT‘13 paper (titled “Towards The Formalization of SPARK 2014 Semantics With Explicit Run-time Checks Using Coq” by Pierre Courtieu, Maria Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jerome Guitton and Trevor Jennings) abstract:

We present the first steps of a broad effort to develop a formal representation of SPARK 2014 suitable for supporting machine-verified static analyses and translations. In our initial work, we have developed technology (Jago) for translating the GNAT compiler’s abstract syntax trees into the Coq proof assistant, and we have formalized in Coq the dynamic semantics for a toy subset of the SPARK 2014 language. SPARK 2014 programs must ensure the absence of certain run-time errors (for example, those arising while performing division by zero, accessing non existing array cells, overflow on integer computation). The main novelty in our semantics is the encoding of (a small part of) the run-time checks performed by the compiler to ensure that any well-formed terminating SPARK programs do not lead to erroneous execution. This and other results are mechanically proved using the Coq proof assistant. The modeling of on-the-fly run-time checks within the semantics lays the foundation for future work on mechanical reasoning about SPARK 2014 program correctness (in the particular area of robustness) and for studying the correctness of compiler optimizations concerning run-time checks, among others.

Formalization in Coq

For Coq development:

For the presentation in HILT‘13:

Alir

Kiasan

GNAT Programming Studio (GPS) Plugins

Contact

Jakub Jedryszek

Bakar GPS Kiasan plugin

Requirements

  1. Sireum installed
  2. Sireum features installed:
    • BakarDev
    • BakarV1
    • SireumDev
  3. If running on Ubuntu: libjpeg 6.2 must be installed (sudo apt-get install libjpeg62).

Quick setup

  1. Pull sireum-bakar-gps project from assembla repository.
  2. Create soft links in gnat/share/gps/plug-ins/ directory:
    • ln -s $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/sireum.py $YOUR_GNAT_DIR/share/gps/plug-ins/sireum.py
    • ln -s $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan
    • ln -s $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/email $YOUR_GNAT_DIR/share/gps/plug-ins/email

Manual setup

  1. Pull sireum-bakar-gps project from assembla repository.
  2. Copy following files to gnat/share/gps/plug-ins/ directory:
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/sireum.py $YOUR_GNAT_DIR/share/gps/plug-ins/sireum.py
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/simplejson $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan/simplejson
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/gpshelper.py $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan/gpshelper.py
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/gui.py $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan/gui.py
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/logic.py $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan/logic.py
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/models.py $YOUR_GNAT_DIR/share/gps/plug-ins/kiasan/models.py
    • cp $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/email $YOUR_GNAT_DIR/share/gps/plug-ins/email

Usage

  1. Open some SPARK project (e.g.: $YOUR_WORKSPACE/sireum-bakar/sireum-bakar-gps/src/kiasan/test/test_projects/test_proj1/test_proj1.gpr)
  2. Build: Build -> Project -> Build All (or just click icon ‘build all’ in GPS tool bar)
  3. Run Kiasan plugin (2 alternatives):
    • Rightclick on package or subprogram name, and choose: Sireum -> Run Kiasan
    • Put cursor on package or subprogram name, and choose from program menu: Sireum -> Run Kiasan
  4. Double click on package/subprogram will highlight lines
  5. Double click on subprogram will load execution cases

Preferences

To change Kiasan plugin preferences go to: Edit -> Preferences -> Sireum -> Kiasan