concolic-core

The architecture-neutral half of a concolic-execution pipeline.

Every item in this crate is stated over traces, decisions and reports. None names an instruction set, a register, a syscall number or a memory layout. A frontend supplies four things:

• a deterministic concrete reference run;
• a symbolic walk forced along a concrete branch log;
• the flip query at one decision;
• the symbolic surface's names in a model, and how to apply them.

Everything else is fixed here: the frontier, the budgets, the verification predicate, the seven flip outcomes, and the report contract.

The verification law

A path only counts when the frontend's own reference engine re-ran the model and agreed. A Sat model alone is never a witness.

The predicate is same decision sites, same directions as the walked prefix, opposite at exactly the flipped site. Operand values are deliberately excluded from the path: a changed input necessarily moves the operands of earlier comparisons that still go the same way, so a predicate comparing whole records rejects genuine flips.

The flip ledger

An attempted flip ends in one structured outcome - Verified, ProvenUnflippable, SolverUnknown, NotPosed, RunFailed, Unconfirmed, or AlreadyExplored - rather than a bare count. A count of failed attempts is not a diagnosis; the structured outcome is what separates "the solver proved this fixed" from "the walker and the run disagreed".

use concolic_core::{BranchRec, FlipOutcome};

// A frontend returns the new trace; the core classifies what the flip reached.
let prefix = [BranchRec { site: 0x9000, taken: true }];
assert_eq!(prefix[0].site, 0x9000);

License

Apache-2.0.