Skip to content

Avoid redundant split aggregate memory checks#829

Merged
shaobo-he merged 1 commit into
developfrom
fix-710-split-aggregate-memory-checks
Jul 7, 2026
Merged

Avoid redundant split aggregate memory checks#829
shaobo-he merged 1 commit into
developfrom
fix-710-split-aggregate-memory-checks

Conversation

@shaobo-he

@shaobo-he shaobo-he commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

Fixes #710.

Problem

SplitAggregateValue lowers one aggregate load/store into several scalar
GEP+load/store operations. Since it runs before MemorySafetyChecker, those
synthetic scalar operations were each instrumented independently. For example,
a 16-byte aggregate access could become two 8-byte memory-safety checks even
though the source operation was one aggregate access.

Approach

This keeps the original memory-safety obligation but avoids checking every
scalarized piece:

  • SplitAggregateValue tags the scalar loads/stores it creates with internal
    metadata.
  • The first scalar access produced for a real aggregate load/store is marked as
    the representative whole-aggregate access.
  • MemorySafetyChecker turns that representative access into one check on the
    original aggregate base pointer and aggregate type size.
  • The remaining scalarized accesses are skipped.
  • Split loads/stores used only for internal constant-aggregate materialization
    are skipped without adding a source-level memory-safety obligation.

This is intentionally not a blanket suppression of all split aggregate memory
operations. Aggregate accesses through arbitrary pointers still get checked;
they are just checked once at the original aggregate size.

Regression

Adds a C memory-safety regression for aggregate return lowering. The test uses
-O2 -Xclang -disable-llvm-passes: optimized frontend lowering produces the
aggregate return shape, while disabling later LLVM passes prevents that shape
from being lowered away before SMACK sees it.

The regression checks that fun emits the two real scalar stores into the local
struct plus exactly one 16-byte check for the split aggregate load used to
return the value. Before this change, the same case emitted four 8-byte checks.

Validation

  • ninja -C build -j2
  • git diff --check
  • python3 test/regtest.py --folder c/memory-safety/split-aggregate --languages c --threads 1 --log INFO --all-examples

@shaobo-he shaobo-he force-pushed the fix-710-split-aggregate-memory-checks branch from 9504532 to 391c254 Compare July 6, 2026 23:06
@shaobo-he shaobo-he merged commit b66bab2 into develop Jul 7, 2026
58 checks passed
@shaobo-he shaobo-he deleted the fix-710-split-aggregate-memory-checks branch July 7, 2026 02:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant