Bitcode rewrite modeling

Several dependencies in one rule

The transfer DSL already accepts several edges. For a function with two input values and a reference output, a reviewed dependency model can be written as:

Use sources(...) and targets(...) to group edges. Every listed source contributes to every listed destination in that declaration. Several declarations form one combined summary: sources are read at function entry, each destination receives the union of its explicit contributors, and declaration order does not sequence assignments. Unspecified fields remain unchanged. A self-edge explicitly retains the old destination dependency:

Here previous receives the entry-time requested, with no dependency on acceleration. Grouping expands to ordinary edges in persisted configuration. Equal sources are read once; contributors to one destination result in one store. A constant assignment cannot share its destination with another contributor. These declarations do not express conditional writes or state-dependent contributor selection.

An output parameter must be a writable pointer/reference. A change to a parameter passed by value is local to the callee and is not a caller-visible output. Plain endpoints describe dependencies without specifying arithmetic, string termination, selected field offsets, initialization, or a conditional state update. Review the generated operations and the caller's later use of the value. For example, an enum-to-string function must return a pointer to string storage if a caller subsequently reads the string.

Use memory(input, byteRange(...), ..., arrays = listOf(countedArray(...))) to select pointed-to input data. Fixed ranges exclude padding; counted arrays include the count and read elements only while the count is within capacity and the element is active. Transfer arrays have no floating-point tolerance.

Selected-memory transfers currently support scalar return destinations. They lower directly to bounded LLVM byte loads and a dependency union. Reading each byte preserves dependencies from interior-field stores that PhASAR can miss with a wider load. They do not reproduce enum acceptance or numeric comparisons. Count guards preserve valid memory accesses; an analysis without path-feasibility checks can conservatively include paths through those guards. Floating-point inputs transferred to integer returns use their bit representation, avoiding the poison that an out-of-range floating-to-integer numeric conversion can produce. Generated transfer bodies retain their dependencies through P5 optimization, and final-body validation checks the configured memory reads and guards.

Parameter names and scalar fields

Use parameter("name", "path.to.scalar"), thisObject("path.to.scalar"), and returnValue("path.to.scalar") for scalar reads and assignments. Omit the field for a scalar parameter or return. A named pointer/reference parameter without a field selects its scalar payload, including a wrapper containing exactly one scalar. parameter("input") to parameter("output") can therefore copy a referenced integer or clock value without byte ranges. Configuration names parameters and fields; compiler metadata supplies their source indexes, types, and layout. For example:

Returned fields use the same operation, including when the C++ ABI passes a hidden sret output pointer. For a returned sample containing timestamp and velocity:

Every scalar in a returned object must have a transfer. Set zeroInitializeReturn = true explicitly when unassigned returned scalars must be zero, such as pitch and roll in a planar pose. This initializes those fields; it does not add contributors to them. It is rejected without named return destinations. A rule cannot mix whole-return and return-member destinations. Returning an optional object, pointer, container, or stateful object still requires a model that preserves its required effects and invariants.

Paths follow embedded classes/structs, C++ reference members and unambiguous non-virtual base classes. A path can end at a scalar or an embedded wrapper containing exactly one scalar: parameter("first", "timestamp") can therefore refer to a Clock::time_point without naming private chrono fields. For a receiver with const Time& cycle_time_, transfer(from = thisObject("cycle_time_"), to = returnValue()) reads the referenced scalar on each call. Compiler metadata supplies each reference-slot offset and pointee layout; a stored address is never substituted for the pointee value. Nested paths can cross several reference members. Writable referents can also be selected as destinations; const referents reject writes, including when their containing object is mutable. Conversely, a const receiver can contain a mutable reference. All source values and destination addresses are captured before stores, preserving aliases. These forms require a receiver or referenced parameter object; they do not support reference members in aggregate returns or counted-array operations.

By-value member reads require one LLVM scalar carrier; parameters split across multiple LLVM arguments are rejected. By-value parameters are not caller-visible write destinations.

Leaves support 8/16/32/64-bit integers and enums, Booleans, float, and double. Missing/ambiguous members, bitfields, static-member selectors, volatile/atomic accesses, virtual bases, ordinary pointer-member traversal, unions, multi-scalar leaves, and writes through const objects are rejected. A compiler-identified constructor may initialize const scalar members in its own receiver, including embedded members. This exception never permits writes through a const parameter or reference member, or writes from an ordinary method.

Fixed indices may appear in a member path, for example parameter("input", "topics[2].status") to returnValue("selected_status"), or constant(3) to returnValue("topics[2].integrity"). Compiler metadata supplies the array capacity and element layout; out-of-range indices, ordinary pointer indexing and unsupported array wrappers fail explicitly. Native arrays and wrappers containing one fixed array are supported. Each destination retains separate contributors; indexing does not imply an array-wide union. Returned arrays follow the same complete-payload coverage or explicit zeroInitializeReturn requirement as other returned members.

For a parameter-selected read, use element(parameter("input", "topics"), parameter("topic_id"), "status") as a transfer source. The optional last argument selects one scalar field in the element; omit it for a scalar array. The index is an integer or enum parameter (by value or reference), with a maximum width of 64 bits. Compiler metadata supplies the fixed capacity, stride and field offset. This reads the selected element; it does not join the other elements or reproduce an indexing algorithm in Kotlin. As with an unchecked C++ array access, the caller must supply an index within the fixed capacity. No clamping or fallback is generated. The index and payload are read before any configured destination is written. Pointer arrays, Boolean/floating indices, nested selectors and indexed destinations are rejected. Under NO_CHECK, variable-index facts can still merge according to the native analyzer's array policy; this form preserves the original indexed access. For array-wide operations, use the counted-array, corresponding-element or zero-initialization forms below. All returned payload fields must be supported, including when zero initialization is requested. Member endpoints cannot be combined with memory(...) selectors.

A getter returning an existing global object's identity can use transfer(globalAddress("_ZN3app6objectE"), returnValue()). The argument is the exact LLVM linkage name without @, taken from compiler evidence. The object must already have a definition in the analysis module; this operation does not supply its storage, initialization, virtual table or lifetime. It returns the address without loading the stored payload. Only a single source to a whole pointer return is supported. Missing objects, external declarations, thread-local objects, other address spaces, pointer unions and payload/member destinations are rejected.

Names are exact, case-sensitive source parameter names from DILocalVariable compiler records. They exclude the implicit this receiver and hidden sret output. LLVM argument spellings are not source-name evidence. An absent name, inconsistent name-to-index mapping, or a name-wide selector whose overloads use different parameter names fails explicitly. Use source indexes where necessary: parameter(0, "value") selects the same field as its named counterpart. Existing member(parameter(0), "value"), bare indexed transfers, thisObject, and returnValue remain supported. Bare indexed transfers retain their existing untyped lowering; use a named parameter or a field selector for compiler-resolved reference payloads. Named parameter endpoints belong to transfer rules, not the separate computation/memory-model API or memory(...) selectors.

The exact function's compiler debug signature resolves source parameters and the receiver. Debug types supply the member names, types, and byte locations; configuration contains no layout offsets. The analysis compiler policy includes -g -fstandalone-debug to retain complete types. A declaration-only P5 input needs an exact compiler signature and complete types. When Clang omits the declaration signature for an address-only callback, or retains a declaration signature without parameter names, STIG can use that exact function's P3 signature and parameter records. The LLVM argument/return carriers and ABI attributes, target triple, and data layout must agree. Every referenced record type must already exist completely in P5 with the same compiler identity and physical layout. No original body or guessed layout is imported. The compiler identity is the DICompositeType.identifier value inside LLVM debug metadata, not a separate generated file. A linked P3 class record can lack this value while another record retains it. STIG accepts that copy only when one identified P3 record has the same compiler source declaration, exact member-function linkage names, and complete physical layout. Missing or ambiguous identity evidence and conflicting declarations or layouts fail the import. Signature provenance is retained in !stig.member.transfer.signature.provenance; used type identities and parameter-name records survive optimization in !stig.member.transfer.types for final-body validation. Missing or mismatching evidence is rejected. Older bitcode with incomplete types must be regenerated from P2; an originalSource path alone cannot supply the missing layout.

Member transfers emit typed scalar loads and stores. Each store replaces only the selected scalar; the previous destination is not an additional contributor. Several edges read all sources before writing any destination, so swapping two members preserves both original values. Multiple contributors to one scalar form a dependency union. Scalar type changes use bit transport, including canonical Boolean storage, without reproducing numerical conversions or predicates. Use these summaries where the analysis needs dependencies rather than exact computed values. The solver's treatment of overwrites remains a separate concern: a typed store does not establish that PhASAR will remove previously recorded taint.

Required literal assignments

Use constant(0) to reset all supported scalar payload fields of a referenced object, including nested objects and fixed arrays. Compiler metadata supplies the complete layout; padding and adjacent objects remain untouched. For example:

A literal assignment preserves required state even though it adds no input contributor. It is not a NOP and does not establish that the analyzer sanitizes earlier taint. constant(Long) and constant(Boolean) are supported. Boolean literals require a Boolean destination; nonzero integers require a single integer or enum scalar. Floating-point initialization supports zero only. Selecting an object or fixed array requires zero and a complete supported payload layout. Const objects (except a constructor's own initialization), by-value parameter destinations, pointers inside the selected payload, unions, and volatile/atomic fields are rejected.

A destination cannot combine a literal assignment with another contributor. Independent assignments and ordinary scalar transfers may share a rule; all input reads happen before destination writes.

Counted arrays by field name

Use the optional count field path to select active elements of an embedded fixed array. The array and its count belong to the same parameter or receiver; the compiler supplies capacity and scalar element layout, including for supported wrappers such as std::array.

parameter(index, field, count = countField) and thisObject(field, count = countField) use the same selection. Paths are relative to the selected object, so a nested array can use parameter("lhs", "validator.samples", count = "validator.sample_count").

The count contributes for empty, valid, and excessive lengths. Each array is read only when its own count is within capacity, and only its active elements are read. These are dependency summaries: they do not reproduce equality, floating-point tolerance, or short circuits between the two objects. An analyzer without path-feasibility checks can conservatively include paths through the count guards.

Named array transfers currently require one-dimensional, contiguous scalar elements and an integer count. Boolean elements, pointer traversal, dynamic containers, array writes, and aggregate-return destinations are unsupported. Other scalar inputs may contribute to the same scalar return, but literal assignments cannot share a counted-array rule. Layout, capacity, and available object bounds are checked before lowering; missing or inconsistent compiler evidence fails explicitly.

Possible array-element dependencies

Wrap a named counted-array source in elements(...) when the result depends on possible element values and the count only bounds the read. This emits compact LLVM directly, with one symbolic indexed read per array and no traversal. The number of generated instructions does not grow with array capacity.

The count does not contribute a data dependency unless an additional scalar transfer explicitly selects it. A zero or excessive count performs no element read. If the original function terminates for an empty array, this summary needs an established nonempty-input invariant or a model preserving that exit. Bounds on the generated read do not imply precise active-prefix facts: NO_CHECK can merge all indices within the declared array capacity. Validate the abstraction against the original LLVM and the surrounding lifecycle.

Compiler metadata supplies offsets, scalar width, stride, capacity and count layout. Single-storage-member anonymous unions, including inherited ones, are supported; overlapping alternatives are rejected. The selected array must have contiguous scalar elements without padding. Ordinary scalar sources may join the same return or scalar field. For example:

This emits one bounded read per distinct array, shared by both destinations, and one store per destination. The delta contributes only to snap. All array and scalar source reads precede writes, including when a destination aliases a source or overwrites an array's count. Array destinations and mixing elements(...) with counted byte reductions in one rule are unsupported. Replacement-body protection and final-P5 validation must preserve the symbolic reads.

Corresponding fixed-array elements

To assign constants to selected fields of active receiver or parameter array elements, supply the array's count and use eachElement(...) as the destination:

This form requires a void function and constant assignments into one embedded fixed array. Compiler types provide its capacity, stride, and selected scalar fields. A single count read bounds the generated loop; zero or excessive counts perform no writes. Within a valid count, only the selected fields of active elements are replaced. The count, inactive elements, other fields, and pointer identities remain unchanged. A consumer replacing an unchecked container loop must establish its valid-count invariant; excessive-count behavior is not inferred from that original loop. Constant validation follows ordinary scalar transfers, including Boolean type checks and zero-only floating-point initialization. Const destinations, pointer fields, reference traversal, overlapping destinations or count storage, noninteger counts, and mixing this form with other transfers are rejected. This operation does not construct or destroy array elements.

Use eachElement(...) on both ends when each input element supplies the corresponding output element. The optional second argument selects a scalar field inside each element:

Compiler metadata supplies capacities, array strides and scalar field layouts. One bounded LLVM loop copies corresponding fields, including supported scalar conversions, without C++ wrappers or checked accessors. The generated instruction count depends on the number of field mappings, not array capacity. Different fields remain separate; this operation does not join all inputs into all output arrays.

Destinations must cover every scalar field of one aggregate sret return, or explicitly use zeroInitializeReturn = true to clear the remaining scalar members. These extra constant stores preserve initialization effects; they do not connect the array inputs to those fields. Its compiler ABI must establish noalias storage, and the source must be a referenced object. For an ADD declaration that omits noalias, STIG requires and imports this guarantee from the exact P3 definition after signature, target and compiler-type checks. It does not infer the guarantee from sret alone. All mapped fixed arrays must have the same positive capacity. Uninitialized partial returns, overlapping output fields, pointer elements, reference-member array paths, counted arrays and mixing with ordinary transfer edges are rejected. Padding is not written. Within each iteration, all input reads precede output writes; noalias keeps writes from affecting later reads. Scalar copies require matching LLVM types; float/double conversion is also supported. Integer width changes are rejected until signedness and their full transfer effects are supported.

As with other rules, verify the final LLVM and source-to-sink dependencies for the selected analyzer. Preserving element addresses in generated code does not establish the analyzer's index precision. Agreement between two results that both omit an expected dependency is not evidence of an acceptable model.

Configured value and memory models

transfer lowers typed configuration directly to LLVM. No replacement C/C++ source is generated. The same model parameters are serialized and rendered by configuration maintenance.

absoluteValue supports float and double. isFinite inspects the IEEE exponent bits and does not convert a floating-point value to an integer. stringLength reads one byte per iteration and carries that byte's nonzero predicate into the increment, preserving an explicit data dependency as well as the loop condition. String models require valid NUL-terminated inputs, as their library contracts do.

For strcmp, select a reviewed C implementation with implementation. Its unsigned-byte reads, first-difference/NUL stopping and returned ordering stay visible in that source. Plain parameter(...) transfers do not select a whole NUL-terminated string: numbered pointer-to-i32 return transfers read one i32 at each pointer and combine those values. They can miss a differing character beyond the first four bytes and read beyond a short string's storage. The former compareStrings DSL helper has been removed; captured STRING_COMPARE model records remain readable and mechanically validatable when reviewing older evidence.

copyMemoryAndAdvance copies a fixed number of bytes through a named pointer member, then reloads and advances that stored pointer by the copied extent. It preserves the order when the destination aliases the cursor storage: the advance uses the pointer after the copy. It copies bytes without a numerical conversion or a domain algorithm.

The supported extents are 1, 2, 4 and 8 bytes, each lowered to one unaligned load/store followed by the pointer reload and update. Compiler metadata supplies the cursor member layout; the member must be a writable byte pointer in an embedded object. Const, volatile/atomic, non-byte and nondefault-address-space cursors are rejected. The source must be a pointer/reference parameter and the function must return void. The caller retains the original validity and capacity preconditions; this operation adds no bounds check. ADD imports the exact original compiler signature from P3 when necessary. Final-P5 validation checks the copy, extent, cursor slot, reload and update order.

bindPointerIfNull stores the incoming pointer identity in a named pointer member only when that member is null. An existing binding causes no store. returnPointerOrStoredGlobal returns the current member pointer, falling back to the current stored pointer value of an exact global symbol when the member is null. Neither operation reads or copies the pointee. For example:

Compiler metadata supplies the embedded member layout in ADD and REWRITE modes. Setters require mutable objects and pointer slots; getters can read const objects and slots. Const pointees are supported because their contents are not accessed. Volatile/atomic slots and nondefault address spaces are rejected. The fallback must be a defined, non-TLS global pointer; its mutable stored value is loaded on every call. Final-P5 validation checks the null test, conditional store or selected return, exact member and global identities, and absence of extra memory effects.

returnAtomicStoredPointerGlobal("sharedPointer") returns a global's current stored pointer using one sequentially consistent atomic load. It requires a parameterless pointer-returning function and mutable, defined, non-TLS storage in the default address space: either a pointer or nested single-field pointer wrappers, explicitly aligned to at least the target pointer width. Integer carriers and other layouts are rejected. The model preserves the shared storage, mutable setters and returned pointee alias; it never substitutes the global's address or initial value. Final-P5 validation checks the exact symbol, atomic ordering, alignment and absence of additional effects.

Memory models use reviewed byte offsets for the target ABI. Configure only the fields actually read or written by the original function; padding is not automatically part of a payload.

zeroMemory requires a void return and nonempty, nonoverlapping ranges. It emits one LLVM memset intrinsic per range, directly; it does not generate C++ or an element-by-element C++ array loop. These constant writes preserve initialization. PhASAR's weak-store policy does not treat them as a sanitizer for earlier taint. equalFields requires two pointer/reference inputs and an integer/Boolean return. Integer fields compare their exact bit patterns. Floating-point fields use ordered equality by default: signed zeros compare equal and NaNs compare unequal.

An explicit floatingPointTolerance(absolute, relative) changes a floating-point field's comparison: finite values are equal when their distance is at most the absolute tolerance or at most the relative tolerance multiplied by the greater magnitude. If either input is nonfinite, equality compares the exact floating-point bit patterns. Choose this policy only when it matches the original implementation.

For arrays, countedArray(offset, type, capacity, countOffset, countType, tolerance) describes an unsigned element count in the same object. equalFields(..., arrays = listOf(...)) rejects unequal counts or counts beyond capacity and compares only active elements. Inactive elements and padding are not read.

Ranges, capacities, constants, endpoint counts, and function types are checked before lowering. Memory extents are also checked against an available LLVM dereferenceable(...) bound. That attribute guarantees accessible bytes; it does not replace review of the complete object layout and lifetime. Unsupported signatures fail instead of receiving a neutral body.

Generated model bodies carry noinline, optnone, "no-builtins", and nounwind; their definitions are retained through llvm.used. Their scalar/memory operations, empty assembly barriers and LLVM intrinsics cannot unwind. P5 replaces invokes of these generated bodies with ordinary calls and normal branches, updating shared-handler PHIs even in protected callers. Real C/C++ replacements do not inherit this guarantee. Asynchronous exception handlers and modules with LLVM's eh-asynch flag retain their unwind edges. P5 runs ipsccp<no-func-spec> to propagate constants across function calls without creating specialized function copies. Specialization can otherwise clone a retained model and remove a constant argument, leaving a signature that no longer matches the configured transfer endpoints. Final-module validation compares all configured operations and constants after normalizing LLVM formatting. Runtime contract tests exercise the generated, optimized LLVM, including string bounds, exceptional floating-point values, padding, inactive arrays, and invalid enum values. These tool tests do not replace the activity's current P5 evidence or analyzer/sink review. Analyzer integration tests additionally check string-byte, scalar, field, and padding dependencies. The production IDE-XTaint solver deliberately uses weak stores: clearing memory preserves the runtime initialization but does not by itself sanitize pre-existing taint in the analysis.

P5 automatically expands the required array/vector/smart-pointer/address helpers inside protected C++ models. This includes address and size accessors of std::vector, std::inplace_vector and amp::inplace_vector; their nested calls must not hide element addresses inside optnone models. It first optimizes the helper bodies, then forces their expansion, while keeping the model's noinline optnone attributes. The same policy applies without explicit rewrite rules and after linking separate compilation units. A conflicting NEVER/protected replacement rule on a required helper fails explicitly. See the compiler sequence and evidence in LLVM toolchain.

Explicit native compiler-input selection

The API below selects an original native compiler input; it is not a stub or a performance rewrite. Do not use it to import selected functions from a file excluded by a file-level softwareUnderAnalysis boundary. It is relevant only to configurations that explicitly permit native implementation inputs beyond that selection:

This is an ADD_FUNCTION_IMPLEMENTATION rule with nativeCompileUnit, selected by an activity use(...) entry. Its compilation unit also supplies P3 provenance. P5 selects the existing P2 compiler-input record, preserving its working directory, compiler arguments, include paths, definitions, and native-action provenance. Existing explicit analysis-header configuration still applies to its selected files. External Bazel paths are resolved against the recorded compiler input, rather than compiled from a guessed path below the repository root.

The repository must be the native build's configured repository. A logical unit must match exactly one distinct recorded compiler input; missing or ambiguous records fail. No compiler recipe is synthesized for a native rule. Only implementation(source = ...) opts into the custom-source workflow. Rewrite evidence identifies a retained native implementation with providerKind = "native_compile_unit" and its original compilation-unit path. The native implementation's callees become real analyzer-input dependencies and must be accounted for in fresh P5 evidence. Selecting it does not establish that those dependencies are already resolved.

Boundary-closure examples

Suppose selected activity code calls send(), while the production implementation of send() calls serialize():

• If an active NOP or transfer transform replaces send(), that transform closes the analyzer-input boundary at send(). The original production body is provenance evidence only, so its call to serialize() does not select a transform or import the real owner of serialize().

• If a configured replacement source defines send() and that replacement calls serialize(), the replacement is real analyzer-input code. serialize() therefore enters the next fixed-point boundary and must be supplied by another selected real unit or an active transform.

• If the compilation unit that owns the production send() is selected in softwareUnderAnalysis, its original body enters P5 without a transform. Its call to serialize() is then a real analyzer-input dependency and must likewise be resolved. A transform must never remain active for send() while that real owner is selected.

P3 may retain an original owner solely to show before-transform provenance. Such provenance-only ownership does not make the owner's callees analyzer-input dependencies; only code that enters P5 establishes the fixed-point boundary.