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:

```cpp
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:

```cpp
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:

```cpp
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`:

```cpp
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`.