1<!--2SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>34SPDX-License-Identifier: GPL-3.0-only5-->67## Qute89Qute is a work-in-progress software analysis framework built around the [QBE] intermediate language.10Architecturally, it is composed of [several][Hackage qute-syntax] [modular][Hackage qute] [Haskell][Hackage qute-symex] [libraries][Hackage qute-cli], which enable the implementation of [static][static software analysis] and [dynamic][dynamic software analysis] software analysis techniques for QBE programs.11The foundation of the framework is a formal (yet executable) description of the QBE specification, which is implemented using an [abstract monad].12Currently, Qute focuses primarily on [dynamic software analysis] through [symbolic execution].1314For further details, see the **[Qute paper][ASYDE]**.1516### Status1718Qute is still in early stages of development, not all desired functionality has been implemented and bugs are to be expected in the existing functionality.19Nonetheless, it supports all relevant features of the [QBE specification][QBE v1.3] and is thus compatible with existing compiler frontends for QBE.20This includes the [cproc] and [SCC] (with an [upstreamed patch][SCC patch]) C compilers as well as the [Hare compiler][Hare].2122### Architecture2324The foundation of this project is a formal, yet executable, description of the QBE intermediate language.25At the time of writing, it targets [v1.3 of the QBE specification][QBE v1.3].26The syntax is specified using [literate Haskell][literate programming] and [parser combinators] in the [`qute-syntax`][Hackage qute-syntax] library.27The language semantics are expressed in a modular way by distinguishing abstract and actual semantics.28*Abstract semantics* of the QBE language are described in terms of a [`Simulator`] monad (i.e., an [abstract monad]).29This monad must then be instantiated, whereby *actual semantics* are specified.30Presently, the following instantiations are supported:31321. Concrete semantics, provided by [`Language.QBE.Simulator.Default.State`].332. [Symbolic][symbolic execution] (specifically [concolic][concolic testing]) semantics through [`Language.QBE.Simulator.Concolic.State`].3435The former is primarily useful for simulation of programs written in the QBE intermediate language.36The latter is intended for automated software testing using [symbolic execution] and—as demonstrated below—can be used to automatically generate test inputs.37Central to this end is the abstract description of QBE semantics that is provided, together with a concrete instantiation, by the [`qute`][Hackage qute] library.38Further, a symbolic instantiation is provided in a separate [`qute-symex`][Hackage qute-symex] library.3940Additionally, executable programs are provided through [`qute-cli`][Hackage qute-cli].41These programs can be used directly from a shell, without interacting with the Haskell codebase.42Presently the following executable program components are available:43441. `qute`: A simulator for QBE programs built on top of the concrete semantics.452. `qute-symex`: An automated software testing tool facilitating the symbolic semantics.4647These program components operate directly on QBE input programs.4849### Installation5051All Haskell libraries provided in this repository are [available on Hackage][Hackage qute] and can hence be installed directly using [Cabal], the Haskell language package manager.52As an example, `qute-cli` can be installed using:5354```55$ cabal install qute-cli56```5758However, to obtain a compatible GHC toolchain and external software (such as constraint solvers), installation using [Guix] is recommended.59For example, in order to install the `qute-cli` component and the [Bitwuzla] solver using Guix:6061```62$ guix time-machine -C .guix/channels.scm -- install -L .guix/modules/ qute-cli bitwuzla63```6465Afterwards, if Guix is configured correctly, the aforementioned program components (`qute` and `qute-symex`) should be available in your `$PATH`.66Note that you can also install additional packages, for example, the [cproc][guix cproc] or [simple-cc][guix simple-cc] QBE-based C compilers this way.6768### Demonstration6970Qute shines when used as a library to implement custom static and dynamic analysis techniques based on QBE.71For details in this regard, refer to the [Hackage documentation][Hackage qute] of the provided Haskell libraries.72Additionally, the [`qute-cli`][Hackage qute-cli] package provides several program components which can be used without writing your own Haskell code.73The following subsections demonstrate the utilization of this program components.7475#### Concrete Execution7677Consider the following "Hello, World!" program:7879```C80#include <stdio.h>8182int main(void) {83 puts("Hello, World!");84 return 0;85}86```8788In order to concretly execute this program using `qute`, we need to obtain an equivalent representation in QBE.89To this end, we can invoke the [cproc] compiler as follows:9091```92$ cproc -emit-qbe hello.c93```9495The resulting QBE file can then be executed with the concrete semantics using:9697```98$ qute hello.qbe99Hello, World!100```101102Note that `qute` is only able to invoke the `puts(3)` function because it intercepts its execution, providing a "simulated" version of it.103Presently, only a limited amount of standard library functions are intercepted in this way.104As such, interactions with the file system or more complex output functions (e.g. `printf(3)`) are currently not supported.105106#### Symbolic Execution107108[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).109As an example, consider the following C program:110111```C112#include <stdio.h>113#include <stddef.h>114115// Convert a memory region to an unconstrained symbolic value. Like calloc(3), it can116// account for memory regions which store multiple elements (nelem) of a specific size117// (elsiz). The give name is used to identify the symbolic variable and must be unique.118extern void qute_make_symbolic(void *ptr, size_t nelem, size_t elsiz, const char *name);119120int main(void) {121 int a;122 qute_make_symbolic(&a, 1, sizeof(a), "a");123 if (a == 42) {124 puts("you found the answer");125 } else {126 puts("not the answer");127 }128129 return 0;130}131```132133This program can be compiled using the QBE-based [cproc] C11 compiler as follows:134135```136$ cproc -emit-qbe example.c137```138139The resulting QBE representation (`example.qbe`) can be symbolically executed using `qute-symex`:140141```142$ qute-symex --write-tests tests/ example.qbe143```144145This will yield the following output:146147```148not the answer149you found the answer150151---152Amount of paths: 2153```154155This indicates that we found two execution paths through our program based on the symbolic variable `a`.156Due to the `--write-tests` option, `qute-symex` will create a `tests/` directory that contains test inputs in the [ktest format][KLEE ktest], one for each execution path.157These files can be inspected with the `ktest-tool` from [KLEE] (which is included in the Guix development environment described below).158For example:159160```161$ ktest-tool tests/test000002.ktest162ktest file : 'tests/test000002.ktest'163args : ['example.qbe']164num objects: 1165object 0: name: 'a1'166object 0: size: 4167object 0: data: b'*\x00\x00\x00'168object 0: hex : 0x2a000000169object 0: int : 42170object 0: uint: 42171object 0: text: *...172```173174This tells us that the second execution path, where the program prints `you found the answer`, was triggered with `a1 := 42`.175From these files, we can—for example—automatically [generate high-coverage test cases][KLEE OSDI].176In the future, it will be possible to replay selected `.ktest` files using `qute-cli`.177178### Tutorials179180More practical examples wrt. utilization of Qute and symbolic execution are available separately:181182* [Executing Hare Programs using Qute](https://notes.8pit.net/notes/zwts.html)183* [Validating Hare’s Sort Module using Symbolic Execution](https://notes.8pit.net/notes/y7n8.html)184* [An Introduction to Automated Software Testing using Symbolic Execution](https://media.ccc.de/v/ho26-146-an-introduction-to-automated-software-testing-using-symbolic-execution) (uses [KLEE])185186### Design Goals187188This project is intentionally written in a simple subset of the [Haskell] programming language.189It should be usable by anyone with a basic Haskell background (e.g., as obtained by reading [Learn You a Haskell for Great Good!][learnyouahaskell]).190Further, the project should require minimal long-term maintenance and should also support older GHC versions.191Therefore, it uses the [GHC2021] language standard and avoids usage of additional language extensions.192Further, whenever possible, dependencies on external libraries that are [not bundled by GHC][GHC libraries] must be avoided.193194### Development195196Code should be formatted using [ormolu][ormolu github].197Git hooks performing several sanity checks, including ensuring the proper code formatting, are available.198These hooks can be enabled using:199200 $ git config --local core.hooksPath .githooks201202Further, a [Guix] environment for development purposes can be obtained using:203204 $ guix time-machine -C .guix/channels.scm -- shell -L .guix/modules/ -m .guix/manifest.scm205206### License207208This project uses the [REUSE Specification] to indicated used software license.209210[QBE]: https://c9x.me/compile/211[QBE vs LLVM]: https://c9x.me/compile/doc/llvm.html212[QBE v1.3]: https://c9x.me/compile/doc/il.html213[QBE jumps]: https://c9x.me/compile/doc/il.html#Jumps214[LLVM]: https://llvm.org/215[KLEE]: https://klee-se.org216[KLEE OSDI]: https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar.pdf#page=9217[KLEE ktest]: https://klee-se.org/releases/docs/v3.1/tutorials/testing-function/#klee-generated-test-cases218[SCC]: https://www.simple-cc.org/219[SCC patch]: https://git.simple-cc.org/scc/commit/575a2d87cac49174b7f53aa6ac5f9186c2165697.html220[cproc]: https://sr.ht/~mcf/cproc/221[Hare]: https://harelang.org/222[Haskell]: https://haskell.org/223[GHC]: https://www.haskell.org/ghc/224[GHC2021]: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/control.html#extension-GHC2021225[GHC libraries]: https://ghc.gitlab.haskell.org/ghc/doc/libraries/index.html226[learnyouahaskell]: https://learnyouahaskell.github.io/chapters.html227[libriscv]: https://github.com/agra-uni-bremen/libriscv228[ormolu github]: https://github.com/tweag/ormolu229[REUSE Specification]: https://reuse.software/spec-3.3/230[Guix]: https://guix.gnu.org231[symbolic execution]: https://en.wikipedia.org/wiki/Symbolic_execution232[concolic testing]: https://en.wikipedia.org/wiki/Concolic_testing233[literate programming]: https://en.wikipedia.org/wiki/Literate_programming234[parser combinators]: https://en.wikipedia.org/wiki/Parser_combinator235[abstract monad]: https://doi.org/10.1145/3607833236[Cabal]: https://www.haskell.org/cabal/237[Bitwuzla]: https://bitwuzla.github.io/238[guix cproc]: https://hpc.guix.info/package/cproc239[guix simple-cc]: https://hpc.guix.info/package/simple-cc240[Hackage qute-symex]: https://hackage.haskell.org/package/qute-symex241[Hackage qute-syntax]: https://hackage.haskell.org/package/qute-syntax242[Hackage qute-cli]: https://hackage.haskell.org/package/qute-cli243[Hackage qute]: https://hackage.haskell.org/package/qute244[dynamic software analysis]: https://en.wikipedia.org/wiki/Dynamic_program_analysis245[static software analysis]: https://en.wikipedia.org/wiki/Static_program_analysis246[ASYDE]: https://www.ibr.cs.tu-bs.de/vss/Publications/2026/tempel_26_qute.pdf247[`Simulator`]: https://hackage-content.haskell.org/package/qute/docs/Language-QBE-Simulator-State.html#t:Simulator248[`Language.QBE.Simulator.Default.State`]: https://hackage-content.haskell.org/package/qute/docs/Language-QBE-Simulator-Default-State.html249[`Language.QBE.Simulator.Concolic.State`]: https://hackage-content.haskell.org/package/qute-symex/docs/Language-QBE-Simulator-Concolic-State.html