Home

Awesome

SymEx-VP RIOT

Basic application illustrating use of SymEx-VP with RIOT.

Usage

To build and use them follow the [instructions in the RIOT repository][riot-setup]. If all prerequisites are installed, application can simply be compiled using:

$ make -C <application>

Afterwards, a compiled application can be executed with SymEx-VP. Assuming that SymEx-VP is in $PATH, simply run the following command to execute one of the provided applications:

$ make -C <application> simulate

By default, applications are executed with a five minute time budget and SymEx-VP stops executing upon encountering the first error.

Description

As described in the SymEx-VP repo, there are basically three aspects regarding the employment of VP-based concolic software testing. The following listing briefly explains how these aspects are implemented in the RIOT context.

  1. Symbolic Inputs: The RIOT applications provided in this repository generate symbolic inputs explicitly via the SymbolicCTRL peripheral. Functions for interacting with this peripheral are available in ./include/symex.h.
  2. Termination Points: Termination points are also declared explicitly by invoking vp_symbolic_ctrl(SYMEX_EXIT) from ./include/symex.h after performed tests are completed.
  3. Path Analyzers: For clarity, no specific path analyzer is employed in this repository. However, we discuss such path analyzer in other work [1] [2] [3]. The example applications provided here are presently only able to detect invocations of RIOT's panic handler (e.g. on failing assertions) as errors through the provided panic.c file.