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 <stdarg.h>81#include <stdio.h>8283int84vsum(int count, ...)85{86 int sum = 0;87 va_list args;8889 va_start(args, count);90 for (int i = 0; i < count; i++) {91 sum += va_arg(args, int);92 }93 va_end(args);9495 return sum;96}9798int99main(void)100{101 return vsum(4, 23, 5, 4, 10); // 42102}103```104105In order to concretly execute this program using `qute`, we need to obtain an equivalent representation in QBE.106To this end, we can invoke the [cproc] compiler as follows:107108```109$ cproc -emit-qbe hello.c110```111112The resulting QBE file can then be executed with the concrete semantics using:113114```115$ qute hello.qbe116$ echo $?11742118```119120Note that `qute` also supports more sophisticated output function, such as `printf(3)`.121Unfortunately, using such functions requires compiling a C standard library to a QBE representation.122Currently, [SCC's libc][SCC] is used for this purpose.123More information is [available separately][SCC Qute].124125#### Symbolic Execution126127[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).128As an example, consider the following C program:129130```C131#include <stdio.h>132#include <stddef.h>133134// Convert a memory region to an unconstrained symbolic value. Like calloc(3), it can135// account for memory regions which store multiple elements (nelem) of a specific size136// (elsiz). The give name is used to identify the symbolic variable and must be unique.137extern void qute_make_symbolic(void *ptr, size_t nelem, size_t elsiz, const char *name);138139int main(void) {140 int a;141 qute_make_symbolic(&a, 1, sizeof(a), "a");142 if (a == 42) {143 puts("you found the answer");144 } else {145 puts("not the answer");146 }147148 return 0;149}150```151152Since this program uses functions from `stdio.h`, it requires a libc.153Therefore, it requires some additional software and is thus best run in the provided [Guix] environment.154To obtain this environment with the required software, run the following command:155156```157$ guix time-machine -C .guix/channels.scm -- shell -L .guix/modules/ qute-cli bitwuzla simple-cc ktest-tool158[env]$159```160161Within this environment, we can compile the example code using a [modified variant][SCC Qute] of [SCC] which includes a Qute-compatible libc:162163```164[env]$ scc -c -o example.qbe example.c -R165```166167Afterward, we can preload the Qute-compatible libc to symbolically execute the QBE representation of the example using `qute-symex`.168Within the Guix environment, the Qute libc is available via `$GUIX_ENVIRONMENT/lib/scc/amd64-qute/libc.a`, thus we run it as follows:169170```171[env]$ qute-symex --preload "$GUIX_ENVIRONMENT/lib/scc/amd64-qute/libc.a" --test-cases=tests/ --write-all example.qbe172```173174This will yield the following output:175176```177not the answer178you found the answer179180---181Amount of paths: 2182```183184This indicates that we found two execution paths through our program based on the symbolic variable `a`.185Due to the `--test-cases` option, `qute-symex` will create a `tests/` directory that contains test inputs in the [ktest format][KLEE ktest], one for each execution path (`--write-all`).186These files can be inspected with the `ktest-tool` from [KLEE] (which is included in the Guix development environment described below).187For example:188189```190[env]$ ktest-tool tests/test000002.ktest191ktest file : 'tests/test000002.ktest'192args : ['example.qbe']193num objects: 1194object 0: name: 'a_e1'195object 0: size: 4196object 0: data: b'*\x00\x00\x00'197object 0: hex : 0x2a000000198object 0: int : 42199object 0: uint: 42200object 0: text: *...201```202203This tells us that the second execution path, where the program prints `you found the answer`, was triggered with `a1 := 42`.204From these files, we can—for example—automatically [generate high-coverage test cases][KLEE OSDI].205In the future, it will be possible to replay selected `.ktest` files using `qute-cli`.206207### Tutorials208209More practical examples wrt. utilization of Qute and symbolic execution are available separately:210211* [Executing Hare Programs using Qute](https://notes.8pit.net/notes/zwts.html)212* [Validating Hare’s Sort Module using Symbolic Execution](https://notes.8pit.net/notes/y7n8.html)213* [Running Application Code with a C Standard Library](https://notes.8pit.net/notes/kgak.html)214* [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])215216### Design Goals217218This project is intentionally written in a simple subset of the [Haskell] programming language.219It should be usable by anyone with a basic Haskell background (e.g., as obtained by reading [Learn You a Haskell for Great Good!][learnyouahaskell]).220Further, the project should require minimal long-term maintenance and should also support older GHC versions.221Therefore, it uses the [GHC2021] language standard and avoids usage of additional language extensions.222Further, whenever possible, dependencies on external libraries that are [not bundled by GHC][GHC libraries] must be avoided.223224### Development225226Code should be formatted using [ormolu][ormolu github].227Git hooks performing several sanity checks, including ensuring the proper code formatting, are available.228These hooks can be enabled using:229230 $ git config --local core.hooksPath .githooks231232Further, a [Guix] environment for development purposes can be obtained using:233234 $ guix time-machine -C .guix/channels.scm -- shell -CN -L .guix/modules/ -m .guix/manifest.scm235236### License237238This project uses the [REUSE Specification] to indicated used software license.239240[QBE]: https://c9x.me/compile/241[QBE vs LLVM]: https://c9x.me/compile/doc/llvm.html242[QBE v1.3]: https://c9x.me/compile/doc/il.html243[QBE jumps]: https://c9x.me/compile/doc/il.html#Jumps244[LLVM]: https://llvm.org/245[KLEE]: https://klee-se.org246[KLEE OSDI]: https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar.pdf#page=9247[KLEE ktest]: https://klee-se.org/releases/docs/v3.1/tutorials/testing-function/#klee-generated-test-cases248[SCC]: https://www.simple-cc.org/249[SCC patch]: https://git.simple-cc.org/scc/commit/575a2d87cac49174b7f53aa6ac5f9186c2165697.html250[SCC Qute]: https://git.8pit.net/scc/README.qute.md.html251[cproc]: https://sr.ht/~mcf/cproc/252[Hare]: https://harelang.org/253[Haskell]: https://haskell.org/254[GHC]: https://www.haskell.org/ghc/255[GHC2021]: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/control.html#extension-GHC2021256[GHC libraries]: https://ghc.gitlab.haskell.org/ghc/doc/libraries/index.html257[learnyouahaskell]: https://learnyouahaskell.github.io/chapters.html258[libriscv]: https://github.com/agra-uni-bremen/libriscv259[ormolu github]: https://github.com/tweag/ormolu260[REUSE Specification]: https://reuse.software/spec-3.3/261[Guix]: https://guix.gnu.org262[symbolic execution]: https://en.wikipedia.org/wiki/Symbolic_execution263[concolic testing]: https://en.wikipedia.org/wiki/Concolic_testing264[literate programming]: https://en.wikipedia.org/wiki/Literate_programming265[parser combinators]: https://en.wikipedia.org/wiki/Parser_combinator266[abstract monad]: https://doi.org/10.1145/3607833267[Cabal]: https://www.haskell.org/cabal/268[Bitwuzla]: https://bitwuzla.github.io/269[guix cproc]: https://hpc.guix.info/package/cproc270[guix simple-cc]: https://hpc.guix.info/package/simple-cc271[Hackage qute-symex]: https://hackage.haskell.org/package/qute-symex272[Hackage qute-syntax]: https://hackage.haskell.org/package/qute-syntax273[Hackage qute-cli]: https://hackage.haskell.org/package/qute-cli274[Hackage qute]: https://hackage.haskell.org/package/qute275[dynamic software analysis]: https://en.wikipedia.org/wiki/Dynamic_program_analysis276[static software analysis]: https://en.wikipedia.org/wiki/Static_program_analysis277[ASYDE]: https://doi.org/10.1145/3843777.3844530278[`Simulator`]: https://hackage-content.haskell.org/package/qute/docs/Language-QBE-Simulator-State.html#t:Simulator279[`Language.QBE.Simulator.Default.State`]: https://hackage-content.haskell.org/package/qute/docs/Language-QBE-Simulator-Default-State.html280[`Language.QBE.Simulator.Concolic.State`]: https://hackage-content.haskell.org/package/qute-symex/docs/Language-QBE-Simulator-Concolic-State.html