weavec::Core — the model

lib/Core contains the ownership, integer and spatial domains without AST or Clang dependencies. It depends only on the C++ standard library. This is the piece the README asks to keep “as modular as possible”: it can be unit-tested without parsing any code, reused by a different frontend, or embedded in other tools.

RFC 0024 keeps runtime format syntax in the Clang-free Format.h / Format.cpp parser. Its bounded conversion records describe promoted argument categories; Analysis binds those categories to the target’s actual C types. SafetyState holds opaque argument-list lifecycle records and initialized terminated-prefix envelopes. These envelopes are separate from ordinary initialized-byte ranges: an unknown terminator inside a capacity does not initialize the unused tail.

Analysis’s immutable RuntimeModels registry validates call signatures before dispatch. DataflowRuntime.cpp checks memory and stream preconditions, DataflowFormats.cpp binds formats and establishes guarded output facts, and DataflowArgumentLists.cpp handles cursor ownership, consumption and forwarding. They use the existing checked call, callback, output and summary machinery. Source definitions retain priority over library spellings. Ordinary summaries alone never authorize a checked runtime contract. Portable records use checked encoding 9, summary format 23 and sidecar format 24 (RFC 0028).

Header	Purpose
Ownership.h	OwnershipKind lattice (Unknown ⊑ {Owned, Shared, Mutable} ⊑ Raw) and join. Raw is “no guarantee”: tracked, but usable only inside an unsafe region.
Place.h	PlaceId and PlaceTable: structured places (p, s.f, *p, p->f, a[*], a[0]) with parent/descendant/translate queries.
Array.h	Bounded constant/symbolic selectors, half-open intervals, sparse spans and evidence-based membership/disjointness queries (RFC 0015).
Buffer.h	Target-layout descriptors, current initialized-prefix invariants, backing ownership, pointer-sequence identity and guarded buffer postconditions (RFC 0026).
AliasRelation.h	Symmetric may-alias graph over places; closed under copies, plain union at joins (deliberately not transitive). Each edge records the PointerOffset between the two places — the same value (Zero), a constant number of elements, a field, or Unknown — so a pointer derived from another is a name for the same object at a known distance (RFC 0011), and which element of the other end is meant (RFC 0006); separateExact refutes a zero-offset edge on a != edge.
Lifetime.h	LifetimeId and LifetimeConstraints (transitive outlives queries; 'static is id 0).
Borrow.h	Loan (place, kind, lifetime, holder) and BorrowState: may this borrow be created; may this place be moved or mutated; expireHolders drops the loans of holders a predicate declares dead (RFC 0006 liveness).
Integer.h	Target integer types, masked bit-pattern values, bounded modular ranges, concrete/abstract arithmetic, conversion and checked-overflow results (RFC 0017). Implementations are Integer.cpp and CheckedInteger.cpp; neither uses host signed overflow to model target arithmetic.
IntegerExpression.h	Bounded typed expressions and predicates over local places or stable summary paths: constants, inputs, casts, arithmetic, min/max and overflow tests, with validation, substitution and canonical serialization (RFC 0017).
Scalar.h	ValueFact (a set of RFC 0006 outcome classes — zero/positive/negative or null/nonnull — plus an optional exact constant; join, narrow, disjointFrom, implies), GuardOn<Key> (a conjunction of facts about places — PlaceGuard — or summary paths — PathGuard — under which alone a record or effect holds; require, learn, refine, join, drop, bounded by MaxGuardConjuncts) and ScalarTracker (per integer place, what is known about its value; RFC 0009).
Offset.h	PointerOffset: where inside its object a pointer points — Zero, Elements(k), Field(key), Unknown — with plus, negated, toString/parse (RFC 0011).
Spatial.h	Affine (an extent: a constant, or scale * place + constant), SpatialRecord (a place’s extent and offset, and its StringFact — the length of the string the object holds, or that it has no terminator — RFC 0012), SpatialTracker (per place, joined by agreement) and boundsVerdict, the pure decision of RFC 0011’s bounds rules (OutOfBounds, MayBeOutOfBounds, MayReachPastEnd, BeforeStart, and RFC 0012’s AtLeastPastEnd from a lower bound) over KnownBounds (constant upper and lower bounds on either side).
Relation.h	RelationTracker: what the path knows of one integer place against another (Less, LessEqual, Equal, GreaterEqual, Greater, learnt from condition edges, through one equality hop, each with an offset: i < n + k, RFC 0012) and against a constant (learnAtMost/atMost, learnAtLeast/atLeast); forget on a write, join by agreement (RFC 0011).
Moves.h	MoveTracker: which places are currently moved-out/freed (and through which alias), each with an ElementWitness (whole / constant / variable / unknown) saying which element of an a[*] place was named (RFC 0006); a use is only reported when the witnesses match; conservative join. MoveReason::Uninitialized marks a local pointer place that has never been assigned (RFC 0008). Each record carries a PlaceGuard (RFC 0009): learn refutes and erases the records a condition edge contradicts, dropGuardsOn weakens the guards that name a written place.
Raw.h	RawTracker: which places currently hold a raw pointer, why (RawReason: integer cast, WEAVEC_RAW declaration, loaded through a raw pointer, callee result, unchecked callee) and through which alias; union at joins.
Resource.h	ResourceTracker: which places hold an owned resource this function is responsible for (ResourceRecord: origin — allocated or declared WEAVEC_OWNED —, location, release family, escaped, and the number of shares — RFC 0010; the offset a place points at is on its alias edges and in the SpatialTracker, RFC 0011), plus the places known to hold null; records join by union, null facts by intersection (RFC 0007). Each record carries a PlaceGuard (RFC 0009): a resource held only under a fact is cleared, not leaked, on the edge that refutes it.
Nullness.h	NullTracker: per place, whether the pointer it holds is Null, MaybeNull or NonNull (NullRecord: state, where the fact comes from and why — assigned null, a callee’s result or store, a merged null test, a WEAVEC_NULLABLE declaration); no record is unknown and trusted. Joins by the RFC 0008 table (MaybeNull absorbs, Null with anything else is MaybeNull, NonNull with no fact is no fact). A Null/MaybeNull record carries the PlaceGuard of the paths that made it null and, when every other path was non-null, otherwiseNonNull, so refuting the guard makes the record NonNull (RFC 0009).
AnalysisState.h	The dataflow state: moves, loans, aliases, raw pointers, resources, nullness, scalar facts (RFC 0009), extents and offsets (spatial) and integer relations (relations, RFC 0011), inferred kinds, the PendingOutcomes of calls whose consumption (and whose null and non-null stores, RFC 0007/0008) depend on a not-yet-tested result, the flow-sensitive consumed record that feeds outcome classes at return (RFC 0006), and the overwritten caller-visible paths whose entry value has been replaced on every path (RFC 0008), with component-wise join. pathGuard() is the facts of the current path as the guard of a record created here; learn propagates a condition edge’s fact to every guarded record; factOf reads scalar and definite nullness facts through one interface.
Summary.h	FunctionSummary: what a function does to its interface. SummaryPath (param(i)/global(g)/result plus deref/field/index steps), PlaceEffect (read/written/freed/moved, with the release family of a consumption, replaced when every consuming path reinitialised the place, element when every consume went through an element access — RFC 0008 — and when, the PathGuard under which alone the consume happens — RFC 0009), Store (value written into caller-visible memory), ValueSource (fresh — with its release family and, when known, its extent —/copy/borrow/null/raw/unknown, each at a PointerOffset from its root and with a when guard — RFC 0011; alternatives that differ only in their guard are merged by addReturn/addStore), neverReturns (the exit is unreachable; joins by conjunction, RFC 0009), outcomes (per Outcome class — Null, NonNull, Zero, Positive, Negative — the consumption that holds on the paths returning it; RFC 0006), nullOn (per class, the caller places that are null; RFC 0007), nonNullOn and requiresNonNull (per class, the caller places that are non-null; the parameters the function dereferences untested; RFC 0008), requiresExtent (per parameter, the PathAffine extent the body needs behind it, RFC 0011), with join, remapGlobals and the derived consumes/consumesUnconditionally/borrowKind/inferredKind/freshReturnFamily queries.
SummaryIO.h	The stable text form of a FunctionSummary (summary … end records; RFC 0005): printSummary/parseSummary with callbacks that name and resolve globals, so the format is Clang-free and the on-disk sidecar format is defined here.
Scc.h	Tarjan’s strongly connected components over an adjacency list, in reverse topological order; used for the call graph inside a unit and for the unit graph of a program.
Diagnostic.h	Diagnostic, stable ids in diag:: (with All, isKnown, isWarningByDefault), FixItHint, DiagnosticSink, and an in-memory DiagnosticCollector.
SourceLocation.h	Frontend-neutral positions with an opaque slot for the frontend’s native encoding.

The core never sees a clang::VarDecl; it sees a PlaceId. It never sees a clang::SourceLocation; it sees a core::SourceLocation whose opaque field the frontend fills in so it can report at the exact original position. RFC 0017 extends ValueFact with typed integer ranges and GuardOn with integer predicates. AnalysisState retains numeric expressions, conditions and writes; FunctionSummary::numericOutputs and expression-bearing PathAffine values extend the earlier scalar and affine interfaces. Spatial requirements also retain the first accessed byte, so a negative start cannot be mistaken for an empty access.