Runtime-dependent, unresolved and bounded functions explained

What are the four proof states in a devirtualization result?

The four proof states are the categories a devirtualization result from Devirt uses to account for every function in scope, and each function sits in exactly one of them.

Each proof state is reported in the result's coverage ledger as a count out of the same total, and the four counts must add up to that total. Devirt checks that sum, that the proof summary agrees with the proven and bounded counts, and that the requested artifacts exist.

The definitions come from the methodology note How to read a devirtualization coverage figure, which also lists functions, basic blocks, instruction handlers and reachable paths as different analysis units; a result should say which one it counts. This article says function throughout, and the same rules hold for any unit. The API reference shows a complete result, where the coverage ledger also carries total, scope and notes, and the proof summary adds sat_count for counterexamples.

What does proven mean in a devirtualization result?

A proven function in a devirtualization result from Devirt is one for which the processing service supplied verification evidence within a declared scope. The proof does not silently extend beyond its environmental assumptions and input bounds, so it says nothing about inputs or environments outside the declared scope.

Devirt's how-it-works page describes the checks behind that evidence. For eligible operations, a solver searches for a counterexample under the stated model: UNSAT supports equivalence within those assumptions, SAT identifies a disagreement, and a timeout leaves the question unresolved. Recovered operations are also lifted to LLVM IR, and the original observations, the lift and independently compiled native execution are compared within the selected inputs. A successful comparison covers its tested inputs.

Solver documentation draws the same line on UNSAT. The cvc5 tutorial on SMT solver outputs calls unsat “a quite strong statement”: no interpretation of the declared symbols satisfies the formula. That statement is about the formula the check encoded, and Devirt's wording matches it: UNSAT supports equivalence within the stated model and assumptions, not for every possible execution.

Readable devirtualized output is a separate deliverable. Semantic names, typed calls and annotations make recovered code easier to inspect, but they do not substitute for equivalence evidence: a readable function can be useful without being proven correct.

What is a runtime-dependent function in devirtualization?

A runtime-dependent function is a recovered function whose conclusion cannot be completed until a specific real input or environment state is known. In a devirtualization result from Devirt, the state records a known dependency: the processing service knows which input or environment state is needed. A trace through one branch does not prove the branch's other outcomes.

Trace-based devirtualization shows why a single trace is not enough. The Thalium write-up on LLVM-powered deobfuscation (2024) deobfuscates a single execution path, and its recovered C code shows a call to a missing block because that path was never visited. Salwan, Bardin and Potet (2018) built a devirtualization approach on taint analysis, symbolic execution and code simplification. They state the gap formally: local correctness means the recovered program behaves like the original for a given input, and completeness means local correctness holds for every input. Completeness is generally lost, they note, because it requires exploring every path of the virtualized program. Their own implementation is limited to programs without memory accesses that depend on user input.

Devirt's recovery keeps a runtime dependency visible. The how-it-works page notes that a handler can have different meanings on different visits; relevant context stays attached, and genuine runtime conditions are not flattened away. Runtime-dependent records what is still needed to complete the conclusion. It does not count as proof.

What is an unresolved function in devirtualization?

An unresolved function is an in-scope function that was inspected, but the available evidence did not settle it. In a devirtualization result from Devirt, the question stayed open within the declared evidence or budget, and the function remains in the denominator instead of disappearing from the result.

The difference between an unresolved and a runtime-dependent function is what is known. A runtime-dependent function has a known dependency on real input or environment state; an unresolved function has a question the available evidence did not close. Published work describes three routes to an unresolved result:

• Checks that run out of time. The cvc5 tutorial says a solver returns unknown when it is unable to solve the input problem, for example when a resource limit stops it before it finds an answer. On the how-it-works page, a timeout leaves the question unresolved.
• Too many paths. Salwan, Bardin and Potet report that their method, built for programs with few paths, can lose large parts of the original code when there are too many paths, yielding an incomplete recovery.
• Features beyond the analysis. Salwan, Bardin and Potet also list multithreading, intensive floating-point arithmetic, self-modification and system calls among the features beyond the scope of their symbolic reasoning. When an unsupported feature is involved in an apparent failure, the Alive2 translation validator lists the features that prevented verification instead of reporting the transformation as incorrect.

More time does not clear every case. In Alive2's experiment on five single-file programs, raising the solver timeout from one minute to five increased the pairs proved correct by less than 5% and the pairs proved incorrect by less than 17%.

A timeout and an unresolved function are related but counted separately. Devirt keeps solver timeouts in the proof summary, and the timeout count does not have to equal the number of unresolved functions.

What does permanently bounded mean in devirtualization?

A permanently bounded function lies outside an explicit analysis limit agreed for the engagement. In a devirtualization result from Devirt, bounded functions stay in the total, so removing difficult cases cannot inflate the apparent coverage. The proof summary repeats the count as permanent_bounds_count, and Devirt checks that the two agree.

Permanently bounded is not the same as a bounded proof. Alive2, a translation validation tool for LLVM IR presented at PLDI 2021, unrolls loops up to a set bound and limits execution time and memory. In its authors' words, that means “there are circumstances in which it misses bugs.” A check like that is a proof up to its bound. In Devirt's definition, proof already carries its bounds: proven means verified within a declared scope, and the proof does not extend beyond its input bounds. Permanently bounded marks functions outside the engagement's limit altogether.

A permanent bound is part of the agreed scope. If the bounded functions matter to your question, the methodology note's advice applies: decide whether the evidence answers it or a wider engagement is needed.

Why are SAT and timeout counts not proof states?

SAT and timeout counts are proof-summary outcomes, not extra proof states. A SAT answer means the solver found a counterexample, an input on which the recovered operation and the original disagree, and one counterexample is enough to reject equivalence. A timeout means the check did not finish within its time limit, so it established neither equivalence nor a counterexample.

Neither a SAT answer nor a timeout belongs in the proven count, and both remain in the final record of a Devirt result. The proof summary reports sat_count and timeout_count next to proven_count and permanent_bounds_count, and Devirt checks that the proven and bounded counts match the ledger.

Other verifiers treat an unfinished check the same way. The Solidity SMTChecker documentation explains that a timeout means the solver could not prove either case within the given timeout, and since the result is unknown, the checker reports it as a potential failure.

Why do unproven functions stay in the total?

Unproven functions stay in the total because a coverage percentage means little until you know its denominator. Devirt's teaching ledger makes the arithmetic concrete. It is synthetic, not a service benchmark: 100 selected operations, of which 86 are proven, 7 runtime-dependent, 2 unresolved and 5 permanently bounded. Proven over the total reads 86%. Drop the 14 operations that did not reach proven, and the same work would read 100%.

That arithmetic is why the four proof states must add up to the declared total, and why a result also states its scope. The methodology note asks every result to identify its analysis unit, binary version and execution assumptions, because a percentage without those details cannot show whether two analyses are comparable.

How do other verification tools report unproven results?

Verification tools outside devirtualization draw the same line between proven and unproven results. Three published examples:

• Polyspace Code Prover colors an operation green when it is “proven not to cause a particular error on all execution paths” and orange when it “can cause an error on certain execution paths”. In the example in the MathWorks documentation, the tool cannot prove whether an addition overflows, and the most common reason is that it overflows only for some values of its operands.
• Alive2 reports validated pairs, refinement violations, timeouts, out-of-memory conditions and pairs with unsupported features as separate results in its 2021 evaluation.
• Binary lifter validation: Dasgupta and colleagues (PLDI 2020) validated a binary lifter's translation to LLVM IR and proved it correct for 2,254 of 2,348 functions from LLVM's single-source benchmark suite.

Result categories differ from tool to tool, but each tool reports what it proved separately from what it did not. The devirtualization methods research page covers the five published method families and where each one stops.

How to read each state in your own result

Read a devirtualization result from Devirt in this order:

1. Start with scope. Check the analysis unit, the binary version and the execution assumptions before any count.
2. Read proven within that scope. A proven function says nothing about inputs or environments the scope leaves out.
3. Weigh runtime-dependent functions against your question. If your question turns on the input or environment state a function depends on, that part of the answer is still open.
4. Review unresolved functions and permanent bounds. Then decide whether the evidence answers your research question or a wider engagement is needed.
5. Check the proof summary. The SAT count records counterexamples, and the timeout count records checks that did not finish. Neither is proof.

The methodology note How to read a devirtualization coverage figure sets out the four definitions this article expands. For files you are authorized to analyze, the how-it-works page follows one illustrative file from upload to a result with its ledger.