OTAWA plugin tutorial

Dependencies

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

Software:

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

Libraries (development version):

• libxml2
• libxslt

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

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

Installing OTAWA v2

To download and install OTAWA v2, first download the following script and execute it using python:

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

You will also need to install the OTAWA plugins for ARM, and lp-solve. Go to <otawa dir>/bin (where otawa dir is the directory where you just installed otawa) and type:

python3 otawa-install.py otawa-arm otawa-lp_solve5

Warning: to install plugins, do not use otawa-install.py in <otawa_dir>.

Setting the environment

Modify your environment variables as follows:

• add <otawa dir>/bin to variable PATH
• add <otawa dir>/lib to variable LD_LIBRARY_PATH

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 <plugin list> --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 <plugin list> --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.