Target integers and compositional bounds (RFC 0017)

RFC 0017 specifies the target-integer and spatial model. The validation report records correctness checks, corpus diagnostics, performance measurements and supported boundaries.

Core represents types from one through 64 bits, signedness and boolean conversion behavior. IntegerValue stores an unsigned bit pattern; IntegerRange keeps at most two intervals in numeric order. Transfers model unsigned wrap, signed validity, comparisons and conversion before projecting legacy constants or sign classes. _Bool converts any nonzero value to one. An invalid operation supplies no invented value; possibly invalid operations cannot establish a branch fact. Changing loop ranges widen to type endpoints.

IntegerExpression<Key> holds canonical typed operations over inputs, including products, min/max and checked-overflow predicates. Expressions are limited to 64 nodes, depth 12 and 32,768 serialized characters. Guards admit at most eight conjuncts, including numeric predicates; numeric outputs keep at most eight alternatives. Exceeding representational limits loses precision or records incomplete coverage. These bounds do not limit source allocation sizes.

The Analysis implementation separates the following responsibilities:

File in lib/Analysis	Responsibility
IntegerSupport.h	Read Clang target widths, signedness, bit-field storage widths and operators; recognize checked builtins and value-preserving conversions.
DataflowIntegers.cpp	Evaluate typed AST ranges without discarding implicit casts, refine comparisons, translate numeric guards, diagnose definite invalid operations and record spatial outcomes.
DataflowIntegerExpressions.cpp	Lower and intern bounded expressions, use affine forms only where justified, substitute interface inputs and snapshot expression dependencies.
DataflowIntegerStatements.cpp	Compute compound assignments in their promoted type before storage conversion; refine converted switch values and case ranges.
DataflowCheckedIntegers.cpp	Apply overflow builtins and their output writes; specialize checked-product calloc/reallocarray success and failure.
DataflowIntegerProofs.cpp	Use range bounds, overflow-success predicates and matching MAX / count guards to establish non-overflow.
DataflowNumericOutputs.cpp	Capture guarded numeric returns and caller-visible writes, snapshot inputs before call effects, and install final output facts afterward.
DataflowNumericInputs.cpp	Capture every numeric contract dependency before the callee writes its input storage; retire prior snapshot generations.
DataflowGuardCompleteness.cpp	Require each must-contract premise to survive projection, accepting equivalent predicates that deduplicate.
DataflowLoopRequirements.cpp	Recognize eligible unit-stride loops with stable bounds; exclude early exits and unsupported induction from minimum requirements.
DataflowDynamicExtents.cpp	Capture VLA dimensions and sizeof, check dimension bounds, and derive array-subobject extents from target record layout.

Dataflow.cpp connects these transfers to ordinary scalar state, ownership guards, reference-count adjustments and spatial requirements. Array, string, heap and sized-field code use the same numeric facts. Numeric writes and may-alias writes invalidate dependencies; allocation, output and VLA snapshots retain earlier values under bounded source-site identities. Reusing a snapshot site invalidates stale dependencies. Inferred pointer/count field witnesses carry the C multiplication type through ProgramDatabase and sidecars.

The monotone set of overwritten numeric inputs uses packed PlaceSet words; copying a large CFG state does not allocate a tree node for every written place. Recursive function components join fresh summaries into the previous approximation, including reporting passes. May-effect guards weaken, must postconditions retain agreement, and separately guarded requirements keep their premises. This prevents alternating numeric/temporal guard projections from cycling while retaining the existing convergence failure limit.

An abstract range endpoint can prove an access safe or establish a definite violation, but cannot alone witness the possible-boundary diagnostic. Source constraints such as i <= 8 provide that witness; a type-derived upper bound such as INT_MAX - 1 under i < unknown_count does not.

C values and byte intervals are distinct. malloc(n * sizeof(T)) receives the actual C multiplication result, including unsigned wrap. An access first evaluates its index in C, then computes its first byte and exclusive end using checked mathematical byte arithmetic. A wrapped product’s mathematical upper bound may establish a violation, but cannot establish that an access fits. Repeated expression identity supports one-past-product checks without general nonlinear solving. VLA extents use captured positive dimensions where the byte product is representable. Flexible tails use allocation bytes minus the target field offset, retaining the enclosing object’s lifetime and release identity; fixed-array subobjects keep their own bounds.

PathAffine can carry a typed expression followed by mathematical byte scaling. ExtentRequirement carries its guard, exclusive end and optional start. Supported zero-based, unit-stride loops with two upper bounds export a minimum bound. Early-exit and other unsupported loops do not produce inferred must-requirements: a possible access alone cannot establish a required bound for every caller. Arbitrary strides and induction remain outside this inference. Caller arguments are converted to the interface types before substitution. Unresolved requirements can pass through wrappers, while an unsupported condition is never deleted to create an unconditional caller error.

SpatialCheck records Proven, Violation or Unresolved. Proving an access requires both lower and upper bounds; violations retain the existing definite or supported reachable-boundary policy. The final reporting pass aggregates checks by source operation. --dump-analysis prints spatial: proven=<n> violation=<n> unresolved=<n> and unresolved reason counts. These counts are independent of unsafe-region reporting and warning controls. A caller requirement is an obligation, not a proof that all callers satisfy it.

SummaryFormatVersion is 23 and SidecarFormatVersion is 24. Numeric outputs use numeric <path> value ... records; requires-extent retains optional start intervals and typed guards. Core validates types, operators, paths, shapes and limits. Comparison, global remapping and dependency invalidation visit expression leaves and conditions; losing a required global invalidates the dependent expression or premise. Frontend transports these facts through the existing whole-program engine. Rebuild older object sidecars.

Unknown arbitrary indices remain unresolved without automatically producing out-of-bounds. Unsupported numeric projections use analysis-incomplete. Integers wider than 64 bits, general nonlinear inequalities, arbitrary loop invariants, unrestricted alias/provenance models, unions and type punning, byte-encoded pointers, GC invariants and concurrency remain outside the model. Trusted annotations and WEAVEC_ASSUME do not widen actual allocations. There is no runtime instrumentation, --verify flag or whole-program certificate.