RTFM-4-SURE SRP analysis example

Description of the application

The example system consists of three tasks with two shared resources.

These are defined in src/main.c

This file also contains a few assignments which aims to introduce both the tool and SRP-analysis.

The build system handles the switching between "analysis" and "execution" stages via pre-processor macros.

Installation

Dependencies

• Rust compiler, recommended via rustup

• stlink (for udev rules for stm32)

• openocd

• base-devel

• arm-none-eabi-gcc

• arm-none-eabi-gdb

• arm-none-eabi-binutils

• llvm

• clang

• KLEE 2

  yay -S rustup stlink openocd base-devel arm-none-eabi-gcc arm-none-eabi-gdb arm-none-eabi-binutils llvm clang

  yay klee

Get the actual program (from your regular computer, not the container):

git clone https://gitlab.henriktjader.com/d7020e/d7020e_srp.git
cd d7020e_srp

git checkout klee

ITM

cargo install itm

Start the ITM tracing tool

(Only needed the first time)

mkfifo /tmp/swo.log

Start the parser:

itmdump -Ff /tmp/swo.log

Notice, the itmdump tool must be started BEFORE the openocd session (see Debug) in order to capture the ITM trace.

OpenOCD

Start OpenOCD on the host, connect it to your microcontroller.

openocd -f st_nucleo_f4_itm.cfg

The st_nucleo_f4_itm.cfg file is located in the git repo.

Troubleshooting:

Make sure your user is member of uucp (Arch) dailup or serial etc, depending on distro. Access to the serial port is required.

Configure GDB

Add the following to ~/.gdbinit

set auto-load safe-path /

Running

To run the suite of tools:

make bench

After a successful run the output folder contains a database and scripts for parsing this database.

SRP lab in d7020e

Install

Open terminal

cd ~/workspace
git clone https://gitlab.henriktjader.com/d7020e/d7020e_srp.git

The code for KLEE-analysis is acquired by running:

git checkout klee

Command Line setup

Shorthand for running with KLEE-analysis is

make bench

Please inspect the Makefile if you are curious how this is done.

Eclipse setup

Start eclipse through the window manager

Import project to eclipse,

Import->Existing Projects into Workspace

Choose

d7020e_srp

and Finish

Compile

Here you have many options, you can use the Ctrl-B, or the Sledgehammer icon e.g.

ITM

We use the ITM tracing for this example. Open a terminal in eclipse (Shift-Ctrl-Alt T) or the terminal icon (monitor symbol) click Ok (default setting).

Start the ITM tracing tool

itmdump /tmp/swo.log

Notice, the itmdump tool must be started BEFORE the openocd session (see Debug) in order to capture the ITM trace.

Debug

Setup

Select the boxed d7020e_srp Debug oldgdb, and click the cogwheel. Under Debugger/GDB Client Setup, change the path to the executable (/home/arch/Downloads/gcc-arm-none-eabi-5_4-2016q3/bin/arm-none-eabi-gdb).

Run/Debug

To run the program you will use the debugger integrated in eclipse. It uses openocd to communicate with the nucleo board, and gdb to flash the image (generated .elf file) and interact (running, stepping, setting breakpoints etc.).

Select the boxed d7020e_srp Debug oldgdb and click the boxed green bug icon. (There are other ways as well.)

This will start openocd and gdb, and by default break at main. To execute the program to end, click the play icon.

For further info on gdb debugging in eclipse see e.g., http://gnuarmeclipse.github.io/debug/

The trace_printf is redirected to the ITM port, and you should get a trace of your program in the terminal.

Notice, that setting breakpoints in the code may be a bit wonky, we use macros and that confuses the eclipse gdb interface. The BREAKPOINT macro infers a compiler barrier that "should" allow you to break at those (there are two such BREAKPOINTs in the exampe, try put a breakpoint on those to see how it works) . Stepping in code that causes interrupts is also wonky, e.g., when sigle stepping over a JOB_REQUEST (that "pends" the corresponding interrupt handler), the pend bit is not correctly handeled (and the corresponding interrupt not taken). These problems are present for this project only, but general to the gdb debug integration, so be aware.

If not using Eclipse the way to start openocd is by invoking:

openocd -f st_nuclie_f4_itm.cfg

in a separate terminal.

Problems

If openocd fails to start, one possible error is that the /tmp/swo.log file has been locked to a bad state. Actually its not an ordinary file but rather a (linux/posix) FIFO, allowing the openocd to pipe data to the itmdump tool. You may want to stop the itmdump and restart it, and try to launch the debugger again.

Tips

If you want, you can inspect the BASEPRI register (you find it under Registers) to see the system ceiling, but be aware that the priority is the hardware prio, shifted. (See how we use the __set_BASEPRI_MAX in the LOCK macro.)

The current running priority is a bit harder to see, however you see the call stack (in the Debug window, and we know the prio for each task/job/interrupt handler). Notice, the call stack shows the name of the handlers, but we have defined the mapping, so its easy to reverse, right!