B2Program

This is the code generator B2Program for generating code from B to other programming languages.

A subset of B is supported for Java and C++ now. The work for code generation for Python, Clojure and C has begun but not continued.

Paper: https://www.researchgate.net/publication/337441241_A_Multi-target_Code_Generator_for_High-Level_B

Citation:

@inbook{inbook,
author = {Vu, Fabian and Hansen, Dominik and K{\"{o}}rner, Philipp and Leuschel, Michael},
year = {2019},
month = {11},
pages = {456-473},
title = {A Multi-target Code Generator for High-Level B},
isbn = {978-3-030-34967-7},
doi = {10.1007/978-3-030-34968-4_25}
}

Note:

• The implementation of the B types in C++ uses persistent set from: https://github.com/arximboldi/immer
• The library must first be installed before the generated C++ code can be used.
• The generated code for C works for a subset of the generated code that works for Java and C++.
• Sets and couples are not supported for C. Including other machines is not supported in C, too. The only types that are implemented for C are BInteger and BBoolean. An example where code generation for C works is the machine Lift.
• Executing all tests requires building Java B Types and installing C++ B Types

Build Java B Types

Primitive Integer: make btypes_primitives

Big Integer: make btypes_big_integer

Install C++ B Types

mkdir build & cd build
cmake ..
make install

Make sure that the immer library and gmpxx library (for big integers) are installed before.

Supported Subset of B

Machine sections:

Note that code is not generated from INVARIANT and ASSERTIONS. These constructs are used for verifying the machine only. CONSTRAINTS and DEFINITIONS clause are not supported for code generation.

Machine inclusion:

Other machine inclusion clauses (SEES, USES, PROMOTES and REFINES) are not supported yet.

Logical Predicates:

Restriction: As universal quantifications and existential quantifications are quantified constructs, the predicate P must constraint the value of the variables x1, ..., xn. P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for each i in {1,...,n}.

Equality:

Booleans:

Sets:

Restriction: Set comprehesions, generalized unions and generalized intersections are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables. The i-th conjunct must constraint xi for each i in {1,...,n}.

Numbers:

Restrictions:

INTEGER, NATURAL and NATURAL1 are infinite sets. They are only supported on the right-hand side of a set predicate.

Set product and set summation are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables. The i-th conjunct must constraint xi for each i in {1,...,n}.

Relations:

Restriction: Set of Relation mostly grows up very fast. They are only supported on the right-hand side of a set predicate.

Functions:

Restriction: Lambda expressions are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables. The i-th conjunct must constraint xi for each i in {1,...,n}.

Sequences:

The following constructs are not supported for code generation: seq(S), seq1(S), iseq(S), iseq1(S) and perm(S). They are only allowed in the predicate of constructs for verification such as invariant or precondition.

Records:

Nested record accesses are also supported.

Strings:

Restriction: STRING is a infinite set. It is only supported on the right-hand side of a set predicate.

LET and IF-THEN-ELSE Expression and Predicate:

Substitution:

Functional Override and Record Access with assignment can be nested.

Preconditions and Assertions are constructs that are relevant for verification. They are ignored at code generation.

Assignments, Operation Calls, Choice from Set and Choice By Predicate can contain many variables on the left-hand side. Furthermore Choice By Predicate can use previous values of variables.

Restriction: Choice by Predicates are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables. The i-th conjunct must constraint xi for each i in {1,...,n}.

Comments are ignored during code generation. Furthermore trees and pragmas are not supported by B2Program.

Usage

Starting the code generator

Gradle

# Java
./gradlew run -Planguage="java" -Pbig_integer="true/false" [-Pminint="minint" -Pmaxint="maxint"] -Pdeferred_set_size="size" -Pfile="<path_relative_to_project_directory>"

# C++
./gradlew run -Planguage="cpp" -Pbig_integer="true/false" [-Pminint="minint" -Pmaxint="maxint"] -Pdeferred_set_size="size" -Pfile="<path_relative_to_project_directory>"

# Python
./gradlew run -Planguage="python" -Pbig_integer="true/false" [-Pminint="minint" -Pmaxint="maxint"] -Pdeferred_set_size="size" -Pfile="<path_relative_to_project_directory>"

# C
./gradlew run -Planguage="c" -Pbig_integer="true/false" [-Pminint="minint" -Pmaxint="maxint"] -Pdeferred_set_size="size" -Pfile="<path_relative_to_project_directory>"

-Pminint and -Pmaxint are optional. The default values cover 32-Bit Integers

JAR-File

1. Run ./gradlew fatJar to build the JAR-file
2. Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as the machine
3. Generate code from the machine

# Java
java -jar B2Program-all-0.1.0-SNAPSHOT java <isBigInteger> <minint> <maxint> <deferred_set_size> <file_path_relative_to_jar_file>

# C++
java -jar B2Program-all-0.1.0-SNAPSHOT cpp <isBigInteger> <minint> <maxint> <deferred_set_size> <file_path_relative_to_jar_file>

# Python
java -jar B2Program-all-0.1.0-SNAPSHOT python <isBigInteger> <minint> <maxint> <deferred_set_size> <file_path_relative_to_jar_file>

# C
java -jar B2Program-all-0.1.0-SNAPSHOT c <isBigInteger> <minint> <maxint> <deferred_set_size> <file_path_relative_to_jar_file>

Note that minint and maxint are not optional when using JAR-File.

Compile the generated code in Java

1. Build JAR for Java B Types (make btypes_primitives or make btypes_big_integer)
2. Move btypes_persistent.jar to same folder as the generated classes
3. javac -cp btypes_primitives-all.jar <files....>
4. Example: javac -cp btypes_primitives-all.jar TrafficLightExec.java TrafficLight.java (Code generated from TrafficLightExec.mch which includes TrafficLight.mch)

Compile the generated code in C++

1. Install C++ B Types or move them (see btypes_primitives or btypes_big_integer folder) to same folder as the generated classes
2. g++ -std=c++14 -O2 -march=native -g -DIMMER_NO_THREAD_SAFETY -o <executable> <main class>
3. Example: g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o TrafficLightExec.exec TrafficLightExec.cpp (TrafficLightExec.mch includes TrafficLight.mch, this command automatically compiles TrafficLight.cpp)

Compile the generated code in C

1. Move BInteger and BBoolean to same folder as generated code (see btypes/src/main/c)
2. gcc <input file> -o <output file>
3. Example: gcc Lift.c -o Lift

Execute the generated code in Java

1. Write a main function in the generated main class
2. java -cp :btypes_primitives-all.jar <main file>
3. Example: java -cp :btypes_primitives-all.jar TrafficLightExec

Execute the generated code in C++

1. Write a main function in the generated main class
2. ./<main file>
3. Example: ./TrafficLightExec.exec

Execute the generated code in C

1. Write a main function in the generated main file
2. ./main.c
3. Example: ./Lift

Steps from B Model to Output of the Generated Code (with primitive types)

Example 1: Lift

The file for Lift.mch is in https://github.com/favu100/b2program/tree/master/src/test/resources/de/hhu/stups/codegenerator. Lift consists of operation to lift up and lift down and getting the floor.

Java

• Run ./gradlew fatJar to build the JAR-file
• Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as Lift.mch
• Generate code for Lift.mch with java -jar B2Program-all-0.1.0-SNAPSHOT.jar java false -2147483648 2147483647 10 Lift.mch
• Write a main method in Lift.java

public static void main(String[] args) {
    Lift lift = new Lift();
    lift.inc();
    lift.inc();
    lift.inc();
    System.out.println(lift.getFloor());
}

• Build B types in btypes_primitives ./gradlew fatJar in the belonging folder or execute makewhich builds btypes_primitives and move it to this folder
• Move btypes_primitives-all.jar to the same folder as Lift.java
• Compile Lift.java with javac -cp btypes_primitives-all.jar Lift.java
• Execute the compiled file for Lift.java with java -cp :btypes_primitives-all.jar Lift
• Output: 3

C++

• Run ./gradlew fatJar to build the JAR-file
• Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as Lift.mch
• Generate code for Lift.mch java -jar B2Program-all-0.1.0-SNAPSHOT.jar cpp false -2147483648 2147483647 10 Lift.mch
• Write a main method in Lift.cpp

int main() {
    Lift lift;
    lift.inc();
    lift.inc();
    lift.inc();
    cout << lift.getFloor() << "\n";;
    return 0;
}

• Install C++ B types with

mkdir build & cd build
cmake ..
make install

• Compile Lift.cpp with g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Lift.exec Lift.cpp
• Execute Lift.exec with ./Lift

Example 2: Cruise_finite1_deterministic_exec

The file for Cruise_finite1_deterministic_exec.mch and Cruise_finite1_deterministic are in https://github.com/favu100/b2program/tree/master/src/test/resources/de/hhu/stups/codegenerator. The machine Cruise_finite1_deterministic_exec includes the machine Cruise_finite1_deterministic. Cruise_finite1_deterministic_exec contains an operation for executing a cycle in the state space of Cruise_finite1_deterministic 100.000 times. Furthermore it has getter operations for all variables.

Java

• Run ./gradlew fatJar to build the JAR-file
• Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as Cruise_finite1_deterministic_exec.mch and Cruise_finite1_deterministic.mch
• Generate code for Cruise_finite1_deterministic_exec.mch java -jar B2Program-all-0.1.0-SNAPSHOT.jar java false -2147483648 2147483647 10 Cruise_finite1_deterministic.mch
• Write a main method in Cruise_finite1_deterministic_exec.java

public static void main(String[] args) {
    Cruise_finite1_deterministic_exec cruise = new Cruise_finite1_deterministic_exec();
    cruise.simulate();
    System.out.println(cruise.getCruiseAllowed());
    System.out.println(cruise.getCruiseActive());
    System.out.println(cruise.getVehicleAtCruiseSpeed());
    System.out.println(cruise.getVehicleCanKeepSpeed());
    System.out.println(cruise.getVehicleTryKeepSpeed());
    System.out.println(cruise.getSpeedAboveMax());
    System.out.println(cruise.getVehicleTryKeepTimeGap());
    System.out.println(cruise.getCruiseSpeedAtMax());
    System.out.println(cruise.getObstaclePresent());
    System.out.println(cruise.getObstacleDistance());
    System.out.println(cruise.getObstacleRelativeSpeed());
    System.out.println(cruise.getObstacleStatusJustChanged());
    System.out.println(cruise.getCCInitialisationInProgress());
    System.out.println(cruise.getCruiseSpeedChangeInProgress());
}

• Build B types in btypes_primitives with ./gradlew fatJar in the belonging folder or execute makewhich builds btypes_primtives and move it to this folder
• Move btypes_primitives-all.jar to the same folder as the generated classes
• Compile Cruise_finite1_deterministic_exec.java and Cruise_finite1_deterministic.java with javac -cp btypes_primitives-all.jar Cruise_finite1_deterministic_exec.java Cruise_finite1_deterministic.java
• Execute the compiled file for Cruise_finite1_deterministic_exec.java with java -cp :btypes_primitives-all.jar Cruise_finite1_deterministic_exec
• Output:

false
false
false
false
false
false
false
false
false
ODnone
RSnone`
false
false
false

C++

• Run ./gradlew fatJar to build the JAR-file
• Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as Cruise_finite1_deterministic_exec.mch and Cruise_finite1_deterministic.mch
• Generate code for Cruise_finite1_deterministic_exec.mch java -jar B2Program-all-0.1.0-SNAPSHOT.jar cpp false -2147483648 2147483647 10 Cruise_finite1_deterministic_exec.mch
• Write a main method in Cruise_finite1_deterministic_exec.cpp

int main() {
    Cruise_finite1_deterministic_exec cruise;
    cruise.simulate();
    cout << cruise.getCruiseAllowed() << "\n";
    cout << cruise.getCruiseActive() << "\n";
    cout << cruise.getVehicleAtCruiseSpeed() << "\n";
    cout << cruise.getVehicleCanKeepSpeed() << "\n";
    cout << cruise.getVehicleTryKeepSpeed() << "\n";
    cout << cruise.getSpeedAboveMax() << "\n";
    cout << cruise.getVehicleTryKeepTimeGap() << "\n";
    cout << cruise.getCruiseSpeedAtMax() << "\n";
    cout << cruise.getObstaclePresent() << "\n";
    cout << cruise.getObstacleDistance() << "\n";
    cout << cruise.getObstacleRelativeSpeed() << "\n";
    cout << cruise.getObstacleStatusJustChanged() << "\n";
    cout << cruise.getCCInitialisationInProgress() << "\n";
    cout << cruise.getCruiseSpeedChangeInProgress() << "\n";
    return 0;
}

• Install C++ B types with

mkdir build & cd build
cmake ..
make install

• Compile Cruise_finite1_deterministic_exec.cpp with g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Cruise_finite1_deterministic_exec.exec Cruise_finite1_deterministic_exec.cpp
• Execute Cruise_finite1_deterministic_exec.exec with ./Cruise_finite1_deterministic_exec
• Output:

false
false
false
false
false
false
false
false
false
ODnone
RSnone`
false
false
false

Performance

Analysis of the Performance is described in benchmarks/README.md.