1<!--2SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>34SPDX-License-Identifier: GPL-3.0-only5-->67## README89A work-in-progress software analysis framework built around the [QBE] intermediate language.1011### Motivation1213Existing analysis frameworks are predominantly built around [LLVM].14Unfortunately, LLVM is a fast-moving target with constant changes and updates to its intermediate representation.15Therefore, tooling built on LLVM often requires dated LLVM versions (e.g., [KLEE] currently [recommends LLVM 13][KLEE LLVM] released in 2022).16Obtaining these LLVM versions can be cumbersome and often hinders employment of these tools.17To overcome these issues, maintainers of analysis tooling need to constantly invest time to catch up with LLVM releases instead of focusing on improving their analysis framework.1819In order to reduce the maintenance burden, this project attempts to investigates the utilization of another intermediate language for software analysis: [QBE].20QBE is a much [smaller-scale project][QBE vs LLVM] than LLVM and thereby offers a higher degree of stability.21Further, QBE is simpler than LLVM (e.g., providing fewer operations) and thereby eases the implementation of analysis techniques.22Nonetheless, there exist compiler frontends that can emit a representation in the QBE intermediate representation (which can then be analyzed using quebex!).23For example, [SCC], [cproc], or the [Hare compiler][Hare].2425### Status2627I currently consider this a vertical prototype.28A lot of the desired functionality is already there, but not fully developed and tested.29However, all major features of the [QBE specification][QBE v1.3] are nowadays implemented to some degree.30Consequentially, it is possible to process QBE programs emitted by existing compiler frontends such as the [cproc] C11 compiler.31In terms of analysis features, the implementation currently focuses on dynamic analysis techniques (primarily [symbolic execution]).32Unfortunately, there is basically no documentation for the API and the provided command-line frontends (`quebex` and `quebex-symex`) are presently very rudimentary.3334### Architecture3536The foundation of this project is a formal, yet executable, description of the QBE intermediate language.37At the time of writing, it targets [v1.3 of the QBE specification][QBE v1.3].38The syntax is specified using [literate Haskell][literate programming] and [parser combinators] in the `quebex-syntax` library.39The language semantics are expressed in a modular way by distinguishing abstract and actual semantics.40*Abstract semantics* of the QBE language are described in terms of a `Simulator` monad (i.e., an [abstract monad]).41This monad must then be instantiated, whereby *actual semantics* are specified.42Presently, the following instantiations are supported:43441. Concrete semantics, provided by `Language.QBE.Simulator.Default.State`.452. [Symbolic][symbolic execution] (specifically [concolic][concolic testing]) semantics through `Language.QBE.Simulator.Concolic.State`.4647The former is primarily useful for simulation of programs written in the QBE intermediate language.48The latter intended for automated software testing using [symbolic execution] and—as demonstrated below—can be used to automatically generate test inputs.4950The abstract description of the QBE semantics, in terms of the `Simulator` monad, and its concrete instantiation are provided by the `quebex` library.51The symbolic semantics are implemented by a separate `quebex-symex` library.52Additional semantics (e.g., for [abstract interpretation]) can be implemented by building on top of these existing libraries.5354Further, executable programs are provided by the `quebex-cli` component.55These programs can be used directly from a shell, without interacting with the Haskell codebase.56Presently the following executable program components are available:57581. `quebex`: A simulator for QBE programs built on top of the concrete semantics.592. `quebex-symex`: An automated software testing tool facilitating the symbolic semantics.6061These program components operate directly on QBE input programs.6263### Installation6465After cloning the repository, individual components can be installed using [Cabal] (e.g., `cabal install quebex-cli`).66However, presently the codebase is mainly tested with selected GHC versions; therefore, installation using [Guix] is recommended.67For example, in order to install the `quebex-cli` component and the [Bitwuzla] solver using Guix:6869```70$ guix time-machine -C .guix/channels.scm -- install -L .guix/modules/ quebex-cli bitwuzla71```7273Afterwards, if Guix is configured correctly, the aforementioned program components (`quebex` and `quebex-symex`) should be available in your `$PATH`.74Note 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.75The following section demonstrates usage of these components.7677### Demonstration7879This framework is primarily *intended to be used as a library*, allowing the implementation of both static and dynamic analysis techniques based on QBE.80Presently, it focuses on dynamic analysis, and sufficient documentation of the library interface is still lacking.81Nonetheless, it is already capable of executing QBE representations of complex C code (e.g., as emitted by [cproc]).82In order to experiment with the current capabilities, the following subsections demonstrate utilization of the aforementioned program components.8384#### Concrete Execution8586Consider the following "Hello, World!" program:8788```C89#include <stdio.h>9091int main(void) {92 puts("Hello, World!");93 return 0;94}95```9697In order to concretly execute this program using `quebex`, we need to obtain an equivalent representation in QBE.98To this end, we can invoke the [cproc] compiler as follows:99100```101$ cproc -emit-qbe hello.c102```103104The resulting QBE file can then be executed with the concrete semantics using:105106```107$ quebex hello.qbe108Hello, World!109```110111Note that `quebex` is only able to invoke the `puts(3)` function because it intercepts its execution, providing a "simulated" version of it.112Presently, only a limited amount of standard library functions are intercepted in this way.113As such, interactions with the file system or more complex output functions (e.g. `printf(3)`) are currently not supported.114115#### Symbolic Execution116117[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).118As an example, consider the following C program:119120```C121#include <stdio.h>122#include <stddef.h>123124// Convert a memory region to an unconstrained symbolic value. Like calloc(3), it can125// account for memory regions which store multiple elements (nelem) of a specific size126// (elsiz). The give name is used to identify the symbolic variable and must be unique.127extern void quebex_make_symbolic(void *ptr, size_t nelem, size_t elsiz, const char *name);128129int main(void) {130 int a;131 quebex_make_symbolic(&a, 1, sizeof(a), "a");132 if (a == 42) {133 puts("you found the answer");134 } else {135 puts("not the answer");136 }137138 return 0;139}140```141142This program can be compiled using the QBE-based [cproc] C11 compiler as follows:143144```145$ cproc -emit-qbe example.c146```147148The resulting QBE representation (`example.qbe`) can be symbolically executed using quebex-symex:149150```151$ quebex-symex --write-tests tests/ example.qbe152```153154This will yield the following output:155156```157not the answer158you found the answer159160---161Amount of paths: 2162```163164This indicates that we found two execution paths through our program based on the symbolic variable `a`.165Due to the `--write-tests` option, quebex-symex will create a `tests/` directory that contains test inputs in the [ktest format][KLEE ktest], one for each execution path.166These files can be inspected with the `ktest-tool` from [KLEE] (which is included in the Guix development environment described below).167For example:168169```170$ ktest-tool tests/test000002.ktest171ktest file : 'tests/test000002.ktest'172args : ['example.qbe']173num objects: 1174object 0: name: 'a1'175object 0: size: 4176object 0: data: b'*\x00\x00\x00'177object 0: hex : 0x2a000000178object 0: int : 42179object 0: uint: 42180object 0: text: *...181```182183This tells us that the second execution path, where the program prints `you found the answer`, was triggered with `a1 := 42`.184From these files, we can—for example—automatically [generate high-coverage test cases][KLEE OSDI].185In the future, it will be possible to replay selected `.ktest` files using `quebex-cli`.186187### Design Goals188189This project is intentionally written in a simple subset of the [Haskell] programming language.190It should be usable by anyone with a basic Haskell background (e.g., as obtained by reading [Learn You a Haskell for Great Good!][learnyouahaskell]).191Further, the project should require minimal long-term maintenance and should also support older GHC versions.192Therefore, it uses the [GHC2021] language standard and avoids usage of additional language extensions.193Further, whenever possible, dependencies on external libraries that are [not bundled by GHC][GHC libraries] must be avoided.194195### Development196197Code should be formatted using [ormolu][ormolu github].198Git hooks performing several sanity checks, including ensuring the proper code formatting, are available.199These hooks can be enabled using:200201 $ git config --local core.hooksPath .githooks202203Further, a [Guix] environment for development purposes can be obtained using:204205 $ guix time-machine -C .guix/channels.scm -- shell -L .guix/modules/ -m .guix/manifest.scm206207### License208209This project uses the [REUSE Specification] to indicated used software license.210211[QBE]: https://c9x.me/compile/212[QBE vs LLVM]: https://c9x.me/compile/doc/llvm.html213[QBE v1.3]: https://c9x.me/compile/doc/il.html214[LLVM]: https://llvm.org/215[KLEE]: https://klee-se.org216[KLEE LLVM]: https://klee-se.org/releases/docs/v3.1/build-llvm13/217[KLEE OSDI]: https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar.pdf#page=9218[KLEE ktest]: https://klee-se.org/releases/docs/v3.1/tutorials/testing-function/#klee-generated-test-cases219[SCC]: https://www.simple-cc.org/220[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[abstract interpretation]: https://en.wikipedia.org/wiki/Abstract_interpretation234[literate programming]: https://en.wikipedia.org/wiki/Literate_programming235[parser combinators]: https://en.wikipedia.org/wiki/Parser_combinator236[abstract monad]: https://doi.org/10.1145/3607833237[Cabal]: https://www.haskell.org/cabal/238[Bitwuzla]: https://bitwuzla.github.io/239[guix cproc]: https://hpc.guix.info/package/cproc240[guix simple-cc]: https://hpc.guix.info/package/simple-cc