The command line
bitwright-cli builds a bitwright binary: simplify for anyone with an expression to read,
and the other commands for rule authors. Reports go to standard output
(also when a check fails); errors, including a rule file’s compile diagnostics, go to standard
error. A command exits with 0 on success, 1 when a check fails (or lint finds errors), and 2
on bad usage or unreadable input. -- ends the options, for an expression starting with -.
| Command | What it does |
|---|---|
bitwright check rules.bwr | Checks every rule’s soundness and examples; exits 1 unless every rule is sound and every example holds. --thorough checks more widths and bits exhaustively; --prove also proves each rule with the native prover at widths too wide to enumerate (8, 32 and 64; binary16, 32 and 64); --ledger out.proof writes the proof ledger; --against rules.bwr.proof compares with an existing ledger. |
bitwright lint rules.bwr | Prints every diagnostic, rendered with its position. |
bitwright smt rules.bwr | Prints each rule’s soundness obligation as SMT-LIB, separated by (reset), at every admitted assignment of the widths 8, 32 and 64; a rule admitted at none of those gets three other admitted assignments. --widths 13 (one width per width variable) and --rule group::name narrow it. A rule with no obligation prints a line the solver echoes (SKIPPED …) and the command exits 1. |
bitwright catalog [rules.bwr] | A Markdown catalog of the rules: the built-in rules without a file. |
bitwright lean [rules.bwr] [--at 8] | The rules as Lean 4 theorems over BitVec: for every width with sorry proofs, or with --at at fixed widths proved by bv_decide (see Checking rules). |
bitwright prove opt.txt | Verifies compiler transformations in the Alive syntax (Pre:, source, =>, target): each target must refine its source under LLVM’s semantics of poison, undefined behavior and floating point, at every width left open; a counterexample shows small inputs and each side’s values as LLVM IR constants. --widths 8,32 and --conflicts narrow it. Exits 1 unless every transformation is valid. See Verifying compiler transformations. |
bitwright infer opt.txt | Infers each transformation’s precondition over its symbolic constants and verifies it. |
bitwright lift block.vex | Reads lifted code (Ghidra p-code, VEX as pyvex prints it, an LLVM IR function; `–from pcode |
bitwright tv before.ll after.ll | Translation validation: each function of the second file must refine the function of the same name in the first (or @tgt refine @src of one file), for a subset of LLVM IR. |
bitwright explain BW0302 | What a diagnostic code means and how to fix it. |
bitwright simplify '<expr>' | Simplifies an expression (--width 32), deobfuscating: the rules, the normal-form passes and the MBA service with the native normal-form solver, every answer proved by bitwright itself; --standard runs only the rules and the standard passes. Each --assume '<predicate>' adds a 1-bit constraint; a result that relies on constraints is followed by # relies on 0, 2 (their positions among the --assume options). Each --rules my.bwr adds a rule file’s rules after the built-in ones, vouched for by the ledger my.bwr.proof next to it if there is one, else checked first (the command exits 1 unless every rule is sound). --file exprs.txt simplifies each line of a file on its own, on --jobs threads. |
Simplifying from the shell
$ bitwright simplify --width 64 -- '(x & y) * (x | y) + (x & ~y) * (~x & y)'
x * y
$ bitwright simplify --width 8 -- '(x ^ 0xa5) * 0x3d * 0xf5'
(x ^ -91) * 97
$ bitwright simplify --width 32 -- '((a - b) >>u 31) ^ (((a ^ b) & (a ^ (a - b))) >>u 31)'
zext<32>(a <s b)
$ bitwright simplify --width 32 --assume 'x <u 16' --assume 'y == 3' -- '(x & 0xf0) + y * x'
x * 3 # relies on 0, 1
$ bitwright simplify --width 64 -- 'fp.div.rne.f64(x, 0x4010000000000000)'
fp.mul.rne.f64(x, 0x3fd0000000000000)
The expression is in the text syntax, floating-point operations
included; symbols have the --width (64 by default) unless they say otherwise (b:8).
--file simplifies a file of expressions, one per line (- reads standard input), each on its
own and on up to --jobs threads (all the machine runs at once by default). It prints one line
per line read, blank lines and # comments as they are:
$ cat exprs.txt
# from the obfuscated function
(x ^ y) + 2 * (x & y)
(x | y) - (x & ~y)
$ bitwright simplify --width 32 --file exprs.txt --jobs 8
# from the obfuscated function
x + y
y
Rules of your own join the built-in ones with --rules; bitwright check my.bwr --ledger my.bwr.proof once saves checking them on every call:
$ cat my.bwr
bitwright 1;
group mine {
/// Every bit is set in x or in ~x.
#[example("popcnt(p:8) + popcnt(~p:8)" => "8:8")]
rule popcnt_complement<W>(x: W) { popcnt(x) + popcnt(~x) => W }
}
$ bitwright simplify --width 32 --rules my.bwr -- 'popcnt(x) + popcnt(~x)'
32:32
Rule files
A typical workflow for a rule file:
bitwright lint my.bwr
bitwright check my.bwr --ledger my.bwr.proof
bitwright smt my.bwr | z3 -in | sort | uniq -c # every line should be `unsat` (or `| bitwuzla`)
and in continuous integration:
bitwright check my.bwr --against my.bwr.proof
which fails when a rule changed without its ledger being regenerated, when a rule is not sound, or when an example stopped holding.