[feliperodri]

Why

Values read from shadow memory of a pointer-typed object never become constants during symbolic execution, so goto-symex explores branches on them that can never be taken. A get_field on such an object yields (unsignedbv)c, where c is a pointer constant holding the field value repeated over the pointer's bytes. simplify_typecast folds this cast for NULL but not for other integer-address constants.

The cost is real. We hit this in Kani, which is adding Tree Borrows aliasing checks that keep the tags of pointers stored in memory in shadow memory. Every loaded tag stayed symbolic, so the monitor's branches were all explored. On our tests, harnesses whose stack objects hold pointers got up to 12x slower with this missing, and some ran out of 12 GB. Heap objects were unaffected, because their shadow is a byte array. The new regression test is a minimal version: 955 symex steps and 100 VCCs remaining without the fold, 48 steps and 0 VCCs with it.

Change

(τ)c is rewritten to the bit-vector constant with c's bits when:

• c is a non-NULL pointer constant_exprt;
• τ is unsignedbv, signedbv or bv;
• τ has the same width as c.

This matches the encoding in both back ends:

• bv_pointerst::convert_pointer_type encodes a non-NULL pointer constant as build_constant(bvrep2integer(value)), and a pointer-to-integer cast as zero_extension, which is the identity at equal width.
• smt2_convt prints the constant as (_ bvK w) and the cast as ((_ extract w-1 0) ·).

So the rewrite replaces a closed term by one with the same value. Symbolic execution can only prune branches that are infeasible either way.

Unaffected:

• NULL, address_of and other non-constant pointers;
• casts that change width.

Where I'd like input

• Is simplify_typecast the right place? The alternative is to make shadow memory avoid pointer-typed shadow cells, which I haven't explored.
• I kept the rule to equal widths. Folding wider casts through zero extension would be just as sound, but I had no use for it.

Testing

• The new unit test in unit/util/simplify_expr.cpp fails without the change and passes with it. All [core][util] unit tests pass.
• The new regression/cbmc-shadow-memory/pointer-object-constant1 fails without the change and passes with it. It checks that the infeasible branch leaves nothing in --program-only.
• regression/cbmc-shadow-memory and regression/cbmc-primitives pass.
• regression/cbmc: 1143 pass. 4 fail identically with and without the change, because the host's gcc 7 lacks -std=gnu2x (_BitInt1, predefined-constants1, static_assert1, typeof2).

---

• Each commit message has a non-empty body, explaining why the change was made.
• Regression tests are included, in the same commit as the fix.
• My PR is restricted to a single bugfix.
• No unrelated white-space or formatting changes.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.91%. Comparing base (8fcda33) to head (5a3c19e).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9238   +/-   ##
========================================
  Coverage    80.91%   80.91%           
========================================
  Files         1718     1718           
  Lines       190292   190320   +28     
  Branches        73       73           
========================================
+ Hits        153974   153999   +25     
- Misses       36318    36321    +3     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[peterschrammel]

The alternative is to make shadow memory avoid pointer-typed shadow cells, which I haven't explored.

IMO, this would complicate things unnecessarily. For example, you would need to redeclare pointer-free versions of structs containing pointer-typed fields.

[kroening]

We should try to find out whether this is at all guaranteed by the standard.