qute

commits

Clone the repository to access all 661 commits.

• .githooks/
• .guix/
• LICENSES/
• qute-cli/
• qute-symex/
• qute-syntax/
• qute/
• .gitignore
• README.md
• REUSE.toml
• cabal.project

Qute

Qute is a work-in-progress software analysis framework built around the QBE intermediate language. Architecturally, it is composed of several modular Haskell libraries, which enable the implementation of static and dynamic software analysis techniques for QBE programs. The foundation of the framework is a formal (yet executable) description of the QBE specification, which is implemented using an abstract monad. Currently, Qute focuses primarily on dynamic software analysis through symbolic execution.

For further details, see the Qute paper.

Status

Qute is still in early stages of development, not all desired functionality has been implemented and bugs are to be expected in the existing functionality. Nonetheless, it supports all relevant features of the QBE specification and is thus compatible with existing compiler frontends for QBE. This includes the cproc and SCC (with an upstreamed patch) C compilers as well as the Hare compiler.

Architecture

The foundation of this project is a formal, yet executable, description of the QBE intermediate language. At the time of writing, it targets v1.3 of the QBE specification. The syntax is specified using literate Haskell and parser combinators in the qute-syntax library. The language semantics are expressed in a modular way by distinguishing abstract and actual semantics. Abstract semantics of the QBE language are described in terms of a Simulator monad (i.e., an abstract monad). This monad must then be instantiated, whereby actual semantics are specified. Presently, the following instantiations are supported:

1. Concrete semantics, provided by Language.QBE.Simulator.Default.State.
2. Symbolic (specifically concolic) semantics through Language.QBE.Simulator.Concolic.State.

The former is primarily useful for simulation of programs written in the QBE intermediate language. The latter is intended for automated software testing using symbolic execution and—as demonstrated below—can be used to automatically generate test inputs. Central to this end is the abstract description of QBE semantics that is provided, together with a concrete instantiation, by the qute library. Further, a symbolic instantiation is provided in a separate qute-symex library.

Additionally, executable programs are provided through qute-cli. These programs can be used directly from a shell, without interacting with the Haskell codebase. Presently the following executable program components are available:

1. qute: A simulator for QBE programs built on top of the concrete semantics.
2. qute-symex: An automated software testing tool facilitating the symbolic semantics.

These program components operate directly on QBE input programs.

Installation

All Haskell libraries provided in this repository are available on Hackage and can hence be installed directly using Cabal, the Haskell language package manager. As an example, qute-cli can be installed using:

$ cabal install qute-cli

However, to obtain a compatible GHC toolchain and external software (such as constraint solvers), installation using Guix is recommended. For example, in order to install the qute-cli component and the Bitwuzla solver using Guix:

$ guix time-machine -C .guix/channels.scm -- install -L .guix/modules/ qute-cli bitwuzla

Afterwards, if Guix is configured correctly, the aforementioned program components (qute and qute-symex) should be available in your $PATH. Note that you can also install additional packages, for example, the cproc or simple-cc QBE-based C compilers this way.

Demonstration

Qute shines when used as a library to implement custom static and dynamic analysis techniques based on QBE. For details in this regard, refer to the Hackage documentation of the provided Haskell libraries. Additionally, the qute-cli package provides several program components which can be used without writing your own Haskell code. The following subsections demonstrate the utilization of this program components.

Concrete Execution

Consider the following “Hello, World!” program:

#include <stdarg.h>
#include <stdio.h>

int
vsum(int count, ...)
{
    int sum = 0;
    va_list args;

    va_start(args, count);
    for (int i = 0; i < count; i++) {
        sum += va_arg(args, int);
    }
    va_end(args);

    return sum;
}

int
main(void)
{
    return vsum(4, 23, 5, 4, 10); // 42
}

In order to concretly execute this program using qute, we need to obtain an equivalent representation in QBE. To this end, we can invoke the cproc compiler as follows:

$ cproc -emit-qbe hello.c

The resulting QBE file can then be executed with the concrete semantics using:

$ qute hello.qbe
$ echo $?
42

Note that qute also supports more sophisticated output function, such as printf(3). Unfortunately, using such functions requires compiling a C standard library to a QBE representation. Currently, SCC’s libc is used for this purpose. More information is available separately.

Symbolic Execution

Symbolic execution is a dynamic software analysis technique that explores reachable program paths based on a symbolic input variable (i.e., an input source). As an example, consider the following C program:

#include <stdio.h>
#include <stddef.h>

// Convert a memory region to an unconstrained symbolic value. Like calloc(3), it can
// account for memory regions which store multiple elements (nelem) of a specific size
// (elsiz). The give name is used to identify the symbolic variable and must be unique.
extern void qute_make_symbolic(void *ptr, size_t nelem, size_t elsiz, const char *name);

int main(void) {
    int a;
    qute_make_symbolic(&a, 1, sizeof(a), "a");
    if (a == 42) {
        puts("you found the answer");
    } else {
        puts("not the answer");
    }

    return 0;
}

Since this program uses functions from stdio.h, it requires a libc. Therefore, it requires some additional software and is thus best run in the provided Guix environment. To obtain this environment with the required software, run the following command:

$ guix time-machine -C .guix/channels.scm -- shell -L .guix/modules/ qute-cli bitwuzla simple-cc ktest-tool
[env]$ 

Within this environment, we can compile the example code using a modified variant of SCC which includes a Qute-compatible libc:

[env]$ scc -c -o example.qbe example.c -R

Afterward, we can preload the Qute-compatible libc to symbolically execute the QBE representation of the example using qute-symex. Within the Guix environment, the Qute libc is available via $GUIX_ENVIRONMENT/lib/scc/amd64-qute/libc.a, thus we run it as follows:

[env]$ qute-symex --preload "$GUIX_ENVIRONMENT/lib/scc/amd64-qute/libc.a" --test-cases=tests/ --write-all example.qbe

This will yield the following output:

not the answer
you found the answer

---
Amount of paths: 2

This indicates that we found two execution paths through our program based on the symbolic variable a. Due to the --test-cases option, qute-symex will create a tests/ directory that contains test inputs in the ktest format, one for each execution path (--write-all). These files can be inspected with the ktest-tool from KLEE (which is included in the Guix development environment described below). For example:

[env]$ ktest-tool tests/test000002.ktest
ktest file : 'tests/test000002.ktest'
args       : ['example.qbe']
num objects: 1
object 0: name: 'a_e1'
object 0: size: 4
object 0: data: b'*\x00\x00\x00'
object 0: hex : 0x2a000000
object 0: int : 42
object 0: uint: 42
object 0: text: *...

This tells us that the second execution path, where the program prints you found the answer, was triggered with a1 := 42. From these files, we can—for example—automatically generate high-coverage test cases. In the future, it will be possible to replay selected .ktest files using qute-cli.

Tutorials

More practical examples wrt. utilization of Qute and symbolic execution are available separately:

• Executing Hare Programs using Qute
• Validating Hare’s Sort Module using Symbolic Execution
• Running Application Code with a C Standard Library
• An Introduction to Automated Software Testing using Symbolic Execution (uses KLEE)

Design Goals

This project is intentionally written in a simple subset of the Haskell programming language. It should be usable by anyone with a basic Haskell background (e.g., as obtained by reading Learn You a Haskell for Great Good!). Further, the project should require minimal long-term maintenance and should also support older GHC versions. Therefore, it uses the GHC2021 language standard and avoids usage of additional language extensions. Further, whenever possible, dependencies on external libraries that are not bundled by GHC must be avoided.

Development

Code should be formatted using ormolu. Git hooks performing several sanity checks, including ensuring the proper code formatting, are available. These hooks can be enabled using:

$ git config --local core.hooksPath .githooks

Further, a Guix environment for development purposes can be obtained using:

$ guix time-machine -C .guix/channels.scm -- shell -CN -L .guix/modules/ -m .guix/manifest.scm

License

This project uses the REUSE Specification to indicated used software license.