Expand description
Alignment contract checks and alignment-state refinement. Alignment contract checker for Senryx.
This file owns all APIs related to Align(ptr, T) and path-sensitive
alignment refinement. The checker can currently prove these alignment cases:
- Caller-provided contract facts: the checked graph node already has a
contract fact such as
Align(ptr, T). - Direct pointer/object compatibility: the pointer’s operational trace state (OTS) is known aligned and the modeled pointee object has an ABI alignment that is at least as strong as the contract-required type.
- Pointer arithmetic preservation: the pointer was produced by a
recognized offset operation (
ptr.add,ptr.sub,ptr.offset, byte-level variants, or MIROffset) and the Z3 model proves that every modeled offset keeps the resulting address aligned for the required type. - Runtime alignment guards: branch refinement from calls such as
ptr.is_aligned()marks the checked pointer, and its traced source when available, as aligned or unaligned on the corresponding path.
The algorithm checks cheap local facts first: contract facts, then graph/OTS
facts. It falls back to Z3 only when the graph records symbolic pointer
arithmetic. Generic types are handled by enumerating the finite layout set
discovered by GenericChecker; if that set is empty, the checker uses a
conservative alignment/stride candidate set.