Reduce redundant pointer checks in goto_check_c

[tautschnig]

Several optimizations to reduce the number and cost of generated pointer checks:

• Retain the assertion deduplication cache across function calls and branch targets
• Deduplicate pointer checks on the same base pointer across struct field accesses
• Handle dereference LHS in cache invalidation
• Generate pointer validity checks on the base pointer in check_rec_member
• Skip the integer-address check when a NULL check is present
• Cache pragma strings to avoid repeated concatenation
• Use hash-based set for assertion dedup
• Avoid redundant or_exprt(false, X) in pointer check generation
• Add object_in_bounds predicate and optimize check_rec_logical_op
• Fold constant offsets in member_offset_expr

Update test descriptors in regression/cbmc/ and
regression/contracts-dfcc/ to match the reduced property counts and changed property names from the pointer check deduplication.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

This PR reduces redundant pointer checks generated by goto_check_c, aiming to lower VCC counts and symex workload while keeping pointer-safety coverage.

Changes:

• Adds a positive-form object-bounds predicate (object_in_bounds) and uses it to simplify pointer checks.
• Improves pointer-check deduplication and cache retention across branch targets and function calls, plus other micro-optimizations (e.g., skipping redundant integer-address checks).
• Updates regression test descriptors to reflect changed property counts/names due to deduplication.

Reviewed changes

Copilot reviewed 38 out of 38 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/util/pointer_predicates.h	Declares new object_in_bounds helper for positive bounds checks.
src/util/pointer_predicates.cpp	Implements object_in_bounds to simplify bounds-check construction.
src/util/pointer_offset_size.cpp	Optimizes member_offset_expr by folding constant offsets during construction.
src/util/pointer_expr.cpp	Switches prophecy bounds logic to use object_in_bounds.
src/ansi-c/goto-conversion/goto_check_c.cpp	Main optimizations: assertion dedup caching, reduced/check skipping, cache invalidation tweaks, and pragma caching.
regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc	Updates expected properties after pointer-check dedup changes.
regression/contracts-dfcc/no_redudant_checks/test.desc	Relaxes expected pointer-arithmetic property numbering after dedup.
regression/cbmc/switch8/test.desc	Updates expected property count after check dedup.
regression/cbmc/simplify-union/test.desc	Updates expected VCC count after simplification improvements.
regression/cbmc/r_w_ok10/test.desc	Adjusts expected bounds-check wording variability (dynamic vs non-dynamic).
regression/cbmc/pragma_cprover_enable_all/test.desc	Updates expected messages/property counts after dedup and wording changes.
regression/cbmc/pointer-predicates/at_bounds1.desc	Adjusts expected bounds message after object_in_bounds refactor.
regression/cbmc/pointer-overflow3/test.desc	Updates expected failures/count after dedup changes.
regression/cbmc/pointer-overflow3/no-simplify.desc	Updates expected bounds-check messages under --no-simplify.
regression/cbmc/pointer-overflow1/test.desc	Broadens pointer-arithmetic expected output patterns after message changes.
regression/cbmc/pointer-extra-checks/test.desc	Updates expected dereference-failure set after skipping integer-address checks.
regression/cbmc/memory_allocation1/test.desc	Makes integer-address dereference expectation robust to renumbering.
regression/cbmc/enum_is_in_range/enum_lhs.desc	Updates expected enum-range-check property/location after property changes.
regression/cbmc/Undefined_Shift1/test.desc	Updates expected property counts after simplification/dedup changes.
regression/cbmc/Quantifiers-copy/test.desc	Updates expected property counts after dedup changes.
regression/cbmc/Pointer_difference2/test.desc	Updates expected pointer-relation property count after dedup changes.
regression/cbmc/Pointer_comparison5/test.desc	Broadens expected “remaining after simplification” count pattern.
regression/cbmc/Pointer_comparison3/test.desc	Updates expected property counts after dedup changes.
regression/cbmc/Malloc4/test.desc	Updates expected pointer-dereference message numbering/wording.
regression/cbmc/Malloc23/test.desc	Updates expected pointer-dereference failures/count after dedup changes.
regression/cbmc/Array_operations1/test.desc	Updates expected property counts after dedup changes.
regression/cbmc/Array_operations1/full-slice.desc	Updates expected property counts after dedup changes.

Comments suppressed due to low confidence (4)

src/util/pointer_predicates.cpp:1

• object_in_bounds takes an offset parameter but the upper-bound check ignores it. If callers pass a non-nil offset to mean “access at (p + offset) of size access_size”, the current predicate can accept out-of-bounds accesses whenever offset is positive. Fix by incorporating offset into the upper-bound sum (and width calculation), or alternatively clarify the API/contract by removing offset from the signature and requiring callers to pre-add it to pointer.
  src/util/pointer_offset_size.cpp:1
• member_offset_expr now returns an expression without simplify_expr, which can leave trivial forms like 0 + dynamic_part intact and may reduce downstream structural matching/dedup effectiveness. Consider at least handling the const_offset == 0 case by returning *dynamic_part directly (or simplifying only this final plus_exprt). Also, return std::move(result); inhibits NRVO; prefer return result; here.
  src/ansi-c/goto-conversion/goto_check_c.cpp:1
• Filtering conditions by matching the human-readable description string is brittle (it will silently break if the message text changes, is localized, or is reused). Prefer adding a stable identifier to conditiont (e.g., an enum kind) and filtering by that, or filter by the predicate form (e.g., c.assertion.id() == ID_implies with integer_address on the LHS) if adding an enum isn’t feasible.
  src/ansi-c/goto-conversion/goto_check_c.cpp:1
• Changing assertion deduplication from (src_expr, guarded_expr) to guarded_expr alone can collapse distinct checks that coincidentally produce an identical guarded predicate but should retain different metadata (e.g., different description/property_class/source-location context). If such collisions exist, the surviving property may carry the wrong message/class for the suppressed check. A more robust approach is to key the cache on (guarded_expr, description, property_class) (or store a small struct) so only truly-equivalent properties are deduplicated.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.