Week 06 · Block II Simplification
Bogus control flow and opaque predicates
Four branches the programmer wrote, twenty-two a tool injected, and the question of how you tell them apart when you do not have the source.
Which of these twenty-six conditional branches did the programmer actually write?
Bogus control flow adds branches that never go both ways, guarded by predicates whose value the transformer knows and the analyst is supposed not to. It also clones real code, so that the branch has somewhere plausible to go.
The target for this week and the next two was written to make the distinction checkable. It has exactly four conditions, each with a constant you will recognise on sight.
The four genuine conditions#
showcase.c — demo_bogus_control_flow
ground truth: four conditionsuint32_t result = 0x11111111u;
if (x == 0x1337u) {
result ^= 0x22222222u;
} else {
result += 0x3333u;
}
if (y > 0x12340000u) {
result += 0x4444u;
}
if ((x & 0xFFu) == 0x37u) {
result ^= 0x55555555u;
}
if ((y & 1u) == 0u) {
result -= 0x6666u;
} else {
result += 0x7777u;
}the clean build of it
39 instructions, 11 blocks, four Jcc140001210: 4883ec10 sub rsp, 0x10
140001214: 8954240c mov dword ptr [rsp + 0xc], edx
140001218: 894c2408 mov dword ptr [rsp + 8], ecx
14000121c: c744240411111111 mov dword ptr [rsp + 4], 0x11111111
140001224: 817c240837130000 cmp dword ptr [rsp + 8], 0x1337
14000122c: 0f8512000000 jne 0x140001244
140001232: 8b442404 mov eax, dword ptr [rsp + 4]
140001236: 3522222222 xor eax, 0x22222222
14000123b: 89442404 mov dword ptr [rsp + 4], eax
14000123f: e90d000000 jmp 0x140001251
140001244: 8b442404 mov eax, dword ptr [rsp + 4]
140001248: 0533330000 add eax, 0x3333
14000124d: 89442404 mov dword ptr [rsp + 4], eax
140001251: 817c240c00003412 cmp dword ptr [rsp + 0xc], 0x12340000
140001259: 0f860d000000 jbe 0x14000126c
14000125f: 8b442404 mov eax, dword ptr [rsp + 4]An equality test against 0x1337, a threshold against 0x12340000, a
low-byte test against 0x37, and a parity test. In the clean listing the
first one is cmp dword ptr [rsp + 8], 0x1337 followed by jne — a direct
transliteration. Eleven blocks, fourteen edges, four conditional branches:
that is the whole function.
Every one of those four is path-dependent: whether it is taken depends on the arguments, and both directions are reachable. Keep that word. An opaque predicate is not “a branch whose outcome depends on something obscure” — it is a branch one of whose directions is unreachable, by construction, and the whole of week 7 is about how you would show that.
What the pass adds#
the same function, with bogus control flow
the predicate, at the top of the function140001630: 55 push rbp
140001631: 4883ec40 sub rsp, 0x40
140001635: 488d6c2440 lea rbp, [rsp + 0x40]
14000163a: 8955f8 mov dword ptr [rbp - 8], edx
14000163d: 894dfc mov dword ptr [rbp - 4], ecx
140001640: 8b05d6790800 mov eax, dword ptr [rip + 0x879d6]
140001646: 8b0dcc790800 mov ecx, dword ptr [rip + 0x879cc]
14000164c: 89c2 mov edx, eax
14000164e: 83ea01 sub edx, 1
140001651: 0fafc2 imul eax, edx
140001654: 83e001 and eax, 1
140001657: 83f800 cmp eax, 0
14000165a: 0f94c0 sete al
14000165d: 83f90a cmp ecx, 0xa
140001660: 0f9cc1 setl cl
140001663: 08c8 or al, cl
140001665: a801 test al, 1
140001667: 0f8505000000 jne 0x140001672
14000166d: e973050000 jmp 0x140001be5
140001672: 8b55fc mov edx, dword ptr [rbp - 4]
140001675: 448b4df8 mov r9d, dword ptr [rbp - 8]
140001679: b810000000 mov eax, 0x10Read it instruction by instruction. Two movs load a pair of writable globals
through RIP-relative addressing — 0x14008901C into eax and 0x140089018
into ecx. Then edx = eax − 1, imul eax, edx, and eax, 1, cmp eax, 0,
sete al. That is the algebraic half: g · (g − 1) & 1 == 0. The other half
is cmp ecx, 0xa / setl cl — a signed comparison of the second global
against ten. or al, cl, test al, 1, and the jne at 0x1667 goes to the
real code while the fall-through goes to a stub.
So the gate is a disjunction, and its first disjunct is the interesting one:
the product of two consecutive integers is even, so the low bit is zero, so the
sete always sets al — which makes the whole or always true and the branch
always taken.
Over the integers. Over 32-bit values with wraparound you would want to check, and “I can see it is always true” is not a check. Week 7 stops looking at it and proves it instead.
Note also why the globals are there at all. A predicate over initialised constants would fold away during compilation. A predicate over writable globals cannot be folded, because the compiler cannot prove that nothing writes them — which is the same fact the analysis in week 7 has to work around.
The graph#
The clean target: eleven entry-reachable blocks. You can read the source off this graph.
The same function after the pass: seventy entry-reachable blocks. The repeated diamond shapes are the injected gates, each with a clone of real code on one side.

Both panes, close up. The genuine comparisons — 1337h, 12340000h, the
low-byte test — are still there on the right, among the injected predicate
machinery. That is what makes the target usable: ground truth is visible
inside the treated binary.
- conditional branches in the treated target
- 26conditional branches in the treated targetfamily_results.json
- of them injected opaque gates
- 22of them injected opaque gatesfamily_results.json
- genuine source conditions, all two-sided
- 4genuine source conditions, all two-sidedfamily_results.json
- entry-reachable blocks, clean to treated
- 11 → 70entry-reachable blocks, clean to treatedselected_metrics.md
Four implementations, four different amounts of nothing#
Opaque flow: what survives optimization?
BCF = bogus control flow. The observation is about the measured native target.
| Treatment | At O0 | O1 through O3 / Ox | Interpretation |
|---|---|---|---|
| OLLVM BCF | Clones and opaque branches | RESIDUESmall optimized opaque-loop structure | Optimization removes much, not everything. |
| Hikari BCF | Injected native gates already folded | REMOVEDMeasured target matches clean | IR injection does not imply a native predicate. |
| Polaris BCF | Strong cloned/opaque topology | REMOVEDMeasured target matches clean | A strong O0 example can be weak at O1+. |
| Tigress AddOpaque | Initialization-dependent opaque flow | PERSISTS/Ox: 6 conditional jumps vs 1 clean | Runtime state matters to proof and optimization. |
Choose the optimization level deliberately: it can erase the phenomenon being taught.
Scope: demo_bogus_control_flow in the retained optimization study. Jump counts alone do not prove opacity.Open the original lecture figure (SVG)
One row on that table needs unpacking, because it is the week’s most useful correction.
One implementation’s -O0 IR has the same 44-block / 69-edge topology as the
specimen above. Its machine code has 15 blocks and 18 edges. The reason is
that most of its injected guards are literal icmp eq i32 1, 1, and the
backend folds those without being asked. The four conditional jumps that
survive into its machine code are the four genuine source conditions.
So when the week 7 workflow runs on that binary and proves zero injected gates, that is not a failure of the workflow. There were no injected gates left in the machine code to prove anything about. Crediting those four surviving branches as “removed injected predicates” would invert the result completely — and it is exactly the kind of mistake that a workflow reporting only successes would make.
A different mechanism: state, not algebra#
One implementation in this corpus builds its opaque conditions from runtime-initialised program state rather than from an algebraic identity — source-level guards over globals set up at start-up.
Before: the target as recovered, with its guards intact.
After: the same graph, simplified under one captured initialised state.
Both are symbolic projections — a read-only graph, not a rewritten
executable. The difference between them is not a technique, it is an
assumption: the right-hand graph assumes the state that was captured at
run time. Next week that assumption turns zero proofs into three.
Studio: separate the genuine from the injected#
Working from the clean and treated disassembly of the same function:
- Find all four genuine conditions in the treated listing. Give the address of each. Say what you used to identify them.
- Find one injected gate. Write out the predicate it computes, as algebra, from the instructions.
- Now argue that your predicate is always false — and then find the hole in your own argument. The hole is the reason week 7 exists.
- Read the family results file and find the lane where zero gates were proved. Write one sentence explaining why that is not a failure of the prover, citing the block counts.
- showcase.cground truth: the four conditions, in C12 kB
- clean_target_disassembly.txtthe clean target — 39 instructions2 kB
- original_target_disassembly.txtthe treated target — 407 instructions24 kB
- target_function.llpost-pass IR, where the clone regions are visible as IR blocks13 kB
- target_function.llthe second implementation's post-pass IR, for the comparison9 kB
- family_results.jsonbranch counts per lane, injected against genuine9 kB
- opaque_predicate_triton.mdthe study, including the folding correction25 kB
Come to the studio with
The studio assumes you have done these. Each is written so you can tell whether you have, without asking.
- you can read a CFG and identify a loop, a reconverging branch and a dead edge
- you can read `demo_bogus_control_flow` in the source and list its four conditions
- you know why an `-O0` specimen is being used this week