A2 — Recover the semantics

Given a flattened or gated function, a recovered graph and a set of solver results, decide what has been established — and defend the boundary you draw.

Due: 7 May 2027 · Weight: 30%

The brief#

Here is a function with opaque control flow, a recovered control-flow graph, a set of frozen solver results, and a one-paragraph claim that somebody has made about it. Decide whether the claim is supported. Show your working.

A1 asked what happened to a program. A2 asks a harder question: what does this pile of evidence actually entitle anyone to say?

What you are given#

A bundle containing, for one target function:

• the exact disassembly of the target, and the clean comparator’s;
• a recovered control-flow graph, with its counting convention stated;
• frozen solver artefacts for several branches — the path prefix, the branch condition, both queries as .smt2 files, and the recorded status of each;
• the retained runtime output of the binary;
• a claim, written as an analyst’s summary paragraph, which may be supported, partly supported, or wrong.

One of the branches in your bundle is a genuine source condition. Finding it is part of the work; a submission that treats every branch as injected has missed the control that makes the rest meaningful.

What you submit#

One PDF, six to eight pages:

1. The function. What it appears to compute, and the evidence for that.
2. Branch by branch. For each branch you discuss: the path prefix P, the condition C, the two obligations P ∧ C and P ∧ ¬C, the recorded status of each, and your classification — one-sided under P, two-sided, or undetermined. Quote the file.
3. The assumptions. What the analysis assumed about memory, about globals, and about the initial state. For each assumption, one sentence on what changes if it does not hold.
4. The graph. What the recovered graph tells you and what its convention excludes. If you quote block counts, they must be within one convention.
5. The verdict. Is the supplied claim supported? Answer plainly — yes, partly, or no — then say which specific words in it go beyond the evidence, and what evidence would settle it.

How it is marked#

Two failure modes are worth naming in advance, because they are the ones that cost the most marks.

The first is collapsing a path-local result into a global one. UNSAT for P ∧ ¬C says that, for states covered by P and under the analysis’s model, that edge is not taken. It does not say the branch is universally opaque. The course has a specimen where a workflow yields zero proofs from arbitrary entry state and three from three once a captured initialised state is imported — same solver, same branches, different assumption. If your submission cannot express that distinction, it cannot adjudicate the claim.

The second is reading the graph as the answer. A recovered graph is a recovery; it is incomplete at indirect jumps by construction, and its block count belongs to one convention. Two of this course’s specimens exist specifically because a smaller graph was wrong.

Marks are for the reasoning, not for agreeing with the marker. A well-argued “partly supported, and here is the sentence that is doing the overreaching” scores above a correct verdict with thin working.

Analysis success

A tool ran, produced output, and did not error.

Semantic proof

A property holds — under a stated model, state and path prefix.

Binary rewriting

Bytes changed and a file still loads.

Runtime correctness

The program answered correctly, on the inputs that were actually run.

A2 lives in columns one and two, and asks you to say why column four has not been reached.

Declaring your working#

As for A1: discussion of the evidence is encouraged and declared, the written analysis is individual, and any tool you relied on is named with its version and treated as a claim rather than a result.