Repository navigation
Concolic Explorer #4937
Description
ConcolicExplorer builds the proof the Checker validates: a concrete seed names one path, the Checker folds it into edges plus a remainder, and that remainder's model is the next seed — repeated until no satisfiable remainder is left.
worklist ← [ (root, get_model(φ)) ] # an open node + a concrete seed for it
while worklist:
(node, seed) ← worklist.pop()
τ ← generate_proof_trace(seed) # run the seed on the LLVM backend → rule sequence
S ← node
loop:
r ← guided_execute(S, τ) # fold edges; stop at first SAT remainder or trace end
record r.edge
case r:
SAT remainder (guard g): # taken rule covers only part of S
record branch g (→ r.S')
worklist.push( (node ∧ ¬g, r.model) ) # still-uncovered region: more guards to find
S, τ ← r.S', τ[r.consumed:] # continue along the taken branch
UNKNOWN:
emit UndecidedObligation; break
TRACE END:
close S' (cover to target / loop, terminal, or Failed counterexample); break
# worklist empty ⇒ every remainder unsatisfiable or covered ⇒ all paths covered
Limitations
- Non-deterministic semantics. Concrete execution takes one rule per state (by priority), so it can never witness several rules applying to the same concrete state — hence the deterministic-semantics scope.
- Rules missing from the concrete trace. Some rules never fire in concrete execution (e.g. symbolic-only
[symbolic]rules and lemmas), so the LLVM trace cannot name them; the symbolic side must supply them itself. This may need composable symbolic execution to ensure the concolic execution only works for thesrcwithout theassumeinstructions in thetest.
Activity