OTAWA plugin tutorial

Dependencies

First, ensure that you have installed all the required dependencies.

Software:

• GCC / C++
• Git
• CMake
• Python 2.7
• Flex and Bison
• ARM C compiler

Libraries (development version):

• libxml2
• libxslt

For example, on Ubuntu/Debian, all the dependencies can be installed by typing:

sudo apt install build-essential python2 git cmake flex bison libxml2-dev libxslt-dev ocaml gcc-arm-none-eabi

Installing OTAWA v2

Then, you can download and install OTAWA v2, from here:

http://www.otawa.fr/

To downaload and install OTAWA, you first download the script

http://www.tracesgroup.net/otawa/packages/otawa-install.py

then execute the script using python 2.7.

The script is compatible with python 2.7 (NOT python 3). If your default python installation is python3, you need to edit the first line of otawa-install.py and replace #!/usr/bin/python by #!/usr/bin/python2

You will probably need to install the OTAWA plugins for ARM, and lp-solve. Go to the directory containing otawa-install.py and type:

./otawa-install.py -R <otawa dir> otawa-arm otawa-lp_solve5

where <otawa dir> is the desired OTAWA installation directory.

Setting environment

You will need to do the following:

• put <otawa dir>/bin in your PATH environment variable
• put <otawa dir>/lib in your LD_LIBRARY_PATH environment variable

Compiling the plug-ins

Go to the plugin source directory, then type make.

Using a plug-in

In order to develop a program that uses an OTAWA plugin, you will need to use additionnal compiler and linker flags:

The compiler flags can be retrieved by the following command: otawa-config --cflags where <plugin list> is the list of plugins (space-separated) required by your program. If you omit <plugin list>, then your program will only have access to the "core" OTAWA functionnality.

In a similar way, you ca retrieve the required linker flags: otawa-config --libs

Creating a plugin-in

In order to create a plug-in, you must create a <MyPluginName>.eld file (where MyPluginName is the name of your plugin). This file contains general plugin information (name, author, etc.)

You will need to have a class Plugin, heriting from the OTAWA ProcessorPlugin class, declared with the ELM_PLUGIN macro in the .cpp file.

Your plugin will need to be compiled and linked as if it were a standalone program using OTAWA (see previous section), except that you must add the -shared linker flag to produce a .so library. If your plugin requires/depends on another plugin, you must list this dependency it in the otawa-config command used to retrieve the flags for the compilation of your plugin.

Then, your plugin must be installed in $HOME/.otawa/proc/otawa/ to be detected by OTAWA.