qsym

 1## Symbolic execution for the QBE IL
 2
 3qsym is a [symbolic execution][symex wikipedia] tool for the [QBE][qbe web] intermediate language.
 4The tool leverages [Z3][z3 web] to execute QBE IL based on [SMT bitvectors][smt wikipedia].
 5This enables qsym to reason about conditional jumps in the QBE IL, exploring both branches (if feasible under the current constraints).
 6
 7### Status
 8
 9qsym is in very early stages of development and presently mostly a proof-of-concept.
10The underlying parser for the QBE IL ([qbe-reader][qbe-reader github]) is also not yet complete, hence it does not support every syntactically valid QBE IL input yet.
11Furthermore, it is assumed that input programs are well typed, e.g. no type checks are performed for instruction arguments.
12Simple programs generated using a QBE frontend (e.g. [cproc][cproc repo]) can already be explored.
13
14### Installation
15
16Clone the repository and run the following command:
17
18    $ cargo install --path .
19
20### Usage Example
21
22Presently, qsym treats the parameters of a selected function as unconstrained symbolic and executes this function.
23Consider the following example:
24
25    $ cat input.qbe
26    function w $main(w %a) {
27    @start
28            %a =w add 0, %a
29            jnz %a, @end1, @end2
30    @end1
31            %exit =w add 0, 1
32            hlt
33    @end2
34            %exit =w add 0, 2
35            hlt
36    }
37    $ qsym input.qbe main
38    [jnz] Exploring path for label 'end1'
39    Halting executing
40    Local variables:
41    	a = |main:a|
42    	exit = #x00000001
43    Symbolic variable values:
44    	main:a -> #x00000002
45
46    [jnz] Exploring path for label 'end2'
47    Halting executing
48    Local variables:
49    	a = |main:a|
50    	exit = #x00000002
51    Symbolic variable values:
52    	main:a -> #x00000000
53
54For the provided example program, qsym discovers two possible execution paths through the function `main`.
55In the first execution path the symbolic variable `%a` is zero, in the other it is non-zero.
56
57### License
58
59This program is free software: you can redistribute it and/or modify it
60under the terms of the GNU Affero General Public License as published by
61the Free Software Foundation, either version 3 of the License, or (at
62your option) any later version.
63
64This program is distributed in the hope that it will be useful, but
65WITHOUT ANY WARRANTY; without even the implied warranty of
66MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Affero
67General Public License for more details.
68
69You should have received a copy of the GNU Affero General Public License
70along with this program. If not, see <https://www.gnu.org/licenses/>.
71
72[qbe web]: https://c9x.me/compile/
73[symex wikipedia]: https://en.wikipedia.org/wiki/Symbolic_execution
74[z3 web]: https://github.com/Z3Prover/z3
75[smt wikipedia]: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
76[qbe-reader github]: https://github.com/nmeum/qbe-reader
77[cproc repo]: https://sr.ht/~mcf/cproc