fold/docs/research/symbolic-modeling-research-2026-06-03.md

Fold symbolic modeling research note — solver state, guards, memory, CFG

Date: 2026-06-03

Purpose: summarize the research pass requested after the YAMS null/div false-positive triage. The goal is not to turn Fold into angr, KLEE, CBMC, or CSA, but to borrow the mature pieces that address Fold's current weak spots: deeper guard propagation, path-sensitive CFG joins, expression identity, memory/access-path modeling, and explicit preconditions.

Research inputs

• Sage/tool routing was checked first; no project-specific Sage route suggestions were returned.
• PaperBridge CLI was used because no PaperBridge MCP server was visible in the Sage hub. Relevant hits included:
  • Dai et al., A Memory Model for Symbolic Execution, DOI 10.1109/ifcsta.2009.11.
  • KLEE / path-condition papers, including Cadar et al., KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.
  • Static null-pointer/path-sensitive analysis literature, including PANDA/Pulse-related results.
• Web search covered angr docs, KLEE OSDI paper, and Clang Static Analyzer ProgramState/ConstraintManager docs.
• GitHub/source evidence was inspected for:
  • angr SimState, solver plugin, and memory concretization strategy code.
  • LLVM Clang Static Analyzer ProgramState.h and ConstraintManager.h.
  • CBMC symbolic-execution equation/guard code via code search.
  • Infer Pulse docs/source snippets for memory model and latent-vs-manifest errors.

What mature analyzers consistently separate

1. Program state is more than a variable map

Fold currently has a useful SymbolicEnv: current variable expressions, array/heap arrays, member cache, ranges, non-null marks, a path_ predicate, precision tags, observer pointer, and a heap model. This is close to a state object, but the APIs still make it too easy to manually push/restore path_ and to add detector-specific side tables.

Mature tools make the state boundary explicit:

• Clang Static Analyzer ProgramState is documented as the tuple of Environment (expression values), Store (locations), and symbolic constraints / generic client data. It is functional/persistent, and infeasible states are represented as nullptr.
• angr SimState registers memory/register/solver plugins and exposes add_constraints, satisfiable, copy, step, and merge as state operations. A _global_condition is applied to added constraints, memory reads, and related operations.
• KLEE ExecutionState carries its constraint set and address space together; path forking copies the state and extends each child with its branch condition.

Implication for Fold: make SymbolicState / PathState a first-class wrapper around SymbolicEnv instead of letting detectors and walkers manipulate path, memory, and side facts independently. SymbolicEnv can remain the implementation detail.

2. Branching is an assume operation, not ad hoc path concatenation

Clang CSA exposes assume(cond, true/false) and assumeDual(cond) through ConstraintManager; each return value is either a feasible new state or null. The header comments explicitly define this as the principal mechanism for path-sensitivity. CBMC records guarded SSA steps and later converts guards into solver implications. KLEE forks states and extends each child's path condition. angr likewise adds constraints to a state and has explicit state merge conditions.

Implication for Fold: create one path API:

struct AssumeResult { optional<State> truthy; optional<State> falsy; };
AssumeResult assume(State s, z3::expr condition);
optional<State> assume(State s, z3::expr condition, bool polarity);
State join(State then_state, State else_state, z3::expr condition);

Every if, loop guard, switch edge, short-circuit operator, ternary, and P-Code CBRANCH should use this API. The recent loop-unroll fix is exactly the kind of bug this API should prevent by construction.

3. Guards should remain attached to facts and effects

CBMC's equation model records assignments, assumptions, constraints, and gotos with guards, then emits implications such as guard => constraint. This avoids losing the branch condition when the analysis later joins paths.

Fold currently joins variable values with ite in some places and stores some non-null/range facts in side maps. This works for simple cases but is fragile for:

• facts learned under a guard but consumed after nested joins;
• early-return guard shapes;
• switch/case paths;
• loop body effects that are only valid under the loop guard;
• member/call-product aliases used as div-by-zero subjects.

Implication for Fold: keep guarded facts as first-class data:

struct GuardedFact {
    z3::expr guard;
    FactKind kind;              // NonNull, Range, Equality, SizeRelation, etc.
    AccessPath subject;
    z3::expr value_or_predicate;
};

At a sink, prove/refute by querying state.path && fact.guard && sink_condition. At a join, either retain both guarded facts or produce a safe merged fact only when both arms prove the same property.

4. Memory needs region/access-path identity, not just expression text

angr models memory through state plugins and uses explicit read/write concretization strategies for symbolic addresses. Clang CSA uses MemRegion plus store bindings and SVal values. Infer Pulse models stack variables as abstract addresses and heap edges such as addr --field/access--> addr2; unknown calls scramble reachable state optimistically to avoid false positives. KLEE keeps memory objects in the state's address space and reasons over object bounds.

Fold has stack/local bindings, arrays, heap-array helpers, buffer-size trackers, a heap model, and a member cache. The weak point is identity: member expressions, implicit this, repeated .size()/.empty() calls, and pointer aliases can still be modeled by cache keys or fresh expressions that are too narrow.

Implication for Fold: define canonical access paths:

struct RegionKey { FunctionFrame frame; DeclOrSynthetic object; AllocationSite alloc; };
struct AccessPath { RegionKey base; vector<Access> edges; };
// Access = Field(name), Deref, Element(index_expr), CallResult(summary_id), SizeOf, LengthOf, ...

Use AccessPath as the subject key for non-null marks, range facts, member values, call-summary returns, and report fact IDs. Textual expression hashes can remain a fallback, not the primary identity.

5. Unknown/external calls should have explicit havoc/precondition semantics

Infer Pulse's docs are useful here: Pulse reports a null dereference when all conditions are manifest, treats some parameter-dependent bugs as latent, and makes optimistic assumptions about unknown calls by scrambling reachable state. This is a better model than either suppressing all external-precondition cases or reporting them as equal-confidence bugs.

Implication for Fold: separate:

• Manifest finding: sink reachable under current state without external preconditions.
• Latent/precondition finding: sink requires a caller-provided condition, e.g. param != nullptr, size > 0, callback returns non-null.
• Unknown-call havoc: unknown function invalidates/scrambles reachable memory and facts according to a policy, rather than preserving stale facts or globally dropping the path.

This maps cleanly to Fold's confidence tiers: latent/precondition findings should not be Proved unless a caller or contract discharges the precondition.

Tool-by-tool lessons for Fold

Tool	Relevant mature idea	What Fold should adopt	What Fold should not adopt now
angr	Plugin-based SimState; constraints via solver plugin; merge conditions; memory concretization strategies	Explicit state operations, merge conditions, symbolic-address policy, future binary/P-Code path exploration	Full Python-in-process engine or full binary symbolic execution as the default scan lane
KLEE	ExecutionState = constraints + address space; fork on branches; generate concrete witnesses	Optional confirmation adapter; entry-reachability validation; object/bounds mental model	Embedding KLEE into source scanning; blocking on KLEE availability
Clang Static Analyzer	Immutable ProgramState; Environment + Store + constraints; assumeDual; null state means infeasible	assume API, functional state snapshots, persistent side facts, null/infeasible child pruning	Reimplementing the full CSA engine
CBMC	Guarded SSA equation; assignments/constraints/gotos carry guards; joins via guarded implications	Guarded facts/effects and better join semantics	Whole-program bounded model checking as Fold's default scanner
Infer Pulse	Access-path heap graph; latent vs manifest bugs; optimistic unknown-call havoc	Precondition classification, access-path memory, unknown-call policy	Under-approximate-only reporting for all Fold detectors
CodeQL	Declarative dataflow and query-level precision controls	Useful for benchmark comparison and detector design vocabulary	Replacing Fold's solver-backed sink queries

Recommended Fold architecture target

Core state type

Introduce a small source-lane state facade without ripping out SymbolicEnv:

class SourcePathState {
  SymbolicEnv env;
  z3::expr path;
  GuardedFactSet facts;
  MemoryModel memory;
  PrecisionTag precision;
  Trace trace;
};

Initial implementation can store path in env for compatibility, but all new CFG code should go through SourcePathState helpers.

State operations

• assume(cond) returns feasible true/false children after a bounded solver check.
• addFact(kind, subject, predicate) records fact under current path.
• assign(subject, value) bumps SSA/version and kills dependent facts.
• load/store(access_path) routes memory through region/access-path identity.
• join(cond, then, else) merges bindings, memory, non-null, ranges, and facts using guarded data, not detector-specific heuristics.
• havoc(reachable_from_args, policy) handles unknown calls.

Detector contract

Detectors should ask state questions instead of recomputing guards:

• isProvedNonNull(subject)
• canBeNull(subject)
• isProvedNonZero(subject)
• canBeZero(subject)
• range(subject)
• witness(sink_condition)

This keeps null-deref/div/oob/sql detectors from each inventing a partial path model.

Phased implementation plan

Phase 0 — state API shim, no behavior change

• Add source_path_state.hpp/cpp wrapping SymbolicEnv path operations.
• Route SecurityWalker path push/restore through assume/withPath helpers.
• Add unit tests that assert nested if, switch, and loop paths call the shared API.

Phase 1 — feasible-child pruning everywhere

• Use bounded solver checks for if, for/while guard, switch case, ternary, logical &&/||.
• Preserve current budgets; on timeout degrade to imprecise rather than abort.
• Regression targets: YAMS reported files, existing loop OOB fix, switch/case div guards.

Phase 2 — canonical subjects/access paths

• Implement AccessPath for:
  • local variables;
  • implicit/explicit this fields;
  • simple pointer deref and field chains;
  • zero-arg stable query calls (size, empty, length, count).
• Move member cache, non-null marks, and range facts toward AccessPath keys.
• Keep existing string/cache fallback while measuring hit/miss rates.

Phase 3 — guarded facts and joins

• Store non-null/range/equality facts as guarded facts.
• Join facts by retaining guarded alternatives first; only collapse to unguarded facts when both arms prove the same fact.
• Use guarded facts for div-by-zero product aliases and null deref after early returns.

Phase 4 — external preconditions and unknown-call havoc

• Add report evidence field for precondition_required / latent findings.
• Model unknown calls with explicit havoc of reachable memory/facts.
• Add local contracts for common safe APIs and Fold-local fold_assume_* intrinsics.

Phase 5 — binary/P-Code CFG state exploration

• Apply the same state/assume/join concepts to P-Code CBRANCH and machine div/rem gates.
• Keep raw binary string/symbol scans independent.
• Do not lift binary into the source IR; use shared concepts, not shared representation.

Implementation checkpoint — 2026-06-04

Completed PBI-012 modeling increments:

• Phase 0/1: SourcePathState shim plus bounded UNSAT-only pruning for source if, loop guards, switch cases, short-circuit RHS expressions, and ternary arms.
• Phase 2: canonical AccessPath subject identity and additive AccessPath-backed member/range/non-null caches.
• Phase 3: standalone guarded-fact substrate with guarded joins and branch-specific alternatives.
• Phase 4: latent/precondition evidence fields in JSON/SARIF and detector emission for parameter-dependent null/div callsites; conservative unknown-call havoc for mutable reference/address/pointer-reachable facts now clears AccessPath-backed member/range/non-null facts.
• Phase 5: P-Code path sensitivity now includes bounded forward branch exploration: CBRANCH forks taken/fallthrough paths, forward BRANCH jumps stop local fallthrough, and RETURN/indirect branches terminate the current path without broadening bare symbolic binary divisor reporting.
• Follow-up review fixes: hybrid profile merging now preserves source/binary timing and prefilter counters; assertion SIGABRTs inside source-TU analysis are treated as invariant failures rather than silently quarantined TUs.

Latest focused YAMS shard delta:

• /tmp/fold-yams-reported-v7.json: 23 results (10 div-by-zero, 13 null-deref).
• /tmp/fold-yams-reported-v8.json: 20 results (7 div-by-zero, 13 null-deref).
• Removed: post_ingest_enrichment.cpp:91, post_ingest_enrichment.cpp:92, sqlite_vec_backend.cpp:3140.
• No new results relative to v7.

Validation gates exercised during the checkpoint:

• Source/modeling: fold:access_path, fold:source_path_state, fold:guarded_facts, fold:div_by_zero, fold:null_deref, fold:oob_access, fold:scan_e2e.
• Binary/P-Code: fold:pcode_encoder, fold:pcode_summary, fold:binary_backend, fold:scan_e2e.
• Hygiene: lsp_diagnostics on changed C++ files with 0 errors, plus git diff --check.
• Full-suite gates: initial checkpoint passed via monitor #2 (86/86 OK); follow-up branch/havoc/evidence/profile fixes passed meson test -C build/release --print-errorlogs && git diff --check via monitor #3 (87/87 OK, exit 0).

Benchmark and validation gates

• Keep the existing source/binary/hybrid/Rust/Swift goldens.
• Add a Fold production self-scan guard for null/div/oob deltas.
• Keep the YAMS focused shard as a precision guard:
  • /tmp/yams-reported-compile_commands.json
  • latest meaningful report: /tmp/fold-yams-reported-v8.json with 20 null/div findings.
  • baseline report: /tmp/fold-yams-reported-v7.json with 23 null/div findings.
• For each modeling phase, classify the shard findings into:
  • true positive;
  • latent external precondition;
  • deeper CFG/path propagation bug;
  • identity/alias/access-path gap;
  • intentional unsupported case.
• Add one minimal regression per class before changing production behavior.

Concrete next engineering tasks

1. Wire the standalone GuardedFactStore into production SymbolicEnv fact lookups behind a narrow read/query API, with tests before detector migration.
2. Migrate div-by-zero to guarded-fact queries first, then migrate null-deref and oob after div stabilizes.
3. Refine AccessPath havoc from coarse clear-all to dependency-root invalidation for mutable refs, &aggregate, and pointer-reachable calls.
4. Add generic assertion/contract modeling for assert, Fold assertion macros, Expects, and configured project macros without YAMS-specific suppressions.
5. Promote benchmark baselines into a required maturity gate, including structured optional-tool skips and fail-closed malformed-baseline behavior.
6. Keep rerunning the YAMS focused shard and source/binary focused gates after each production behavior change.

Sources

• angr docs: symbolic expressions/solver, SimState, machine state, symbolic memory addressing/concretization strategies.
• angr source inspected: angr/sim_state.py, angr/state_plugins/solver.py, angr/storage/memory_mixins/address_concretization_mixin.py.
• KLEE paper: Cadar et al., KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, OSDI 2008.
• Clang Static Analyzer source/docs: ProgramState.h, ConstraintManager.h, checker development manual, IPA docs.
• CBMC source docs/code search: symex_target, symex_target_equation, symex_goto, ssa_step guarded SSA/equation model.
• Infer Pulse docs and source snippets: interprocedural memory safety analysis, latent/manifest issues, optimistic unknown-call handling, access-path heap model.
• Existing Fold docs: docs/internal/symex-fuzz-landscape.md, docs/research/sast-dast-symbolic-roadmap.md, and current source headers in include/fold/symbolic/encoder.hpp.