Umbrella: make memory-safety checking storage- and property-aware

[shaobo-he]

Summary

SMACK's memory-safety model needs a storage-aware overhaul. A run over 3,000 public SV-COMP 2026 Juliet valid-memsafety tasks exposed three related gaps:

1. stack objects do not become invalid when their lifetime ends;
2. $free does not distinguish heap allocations from stack objects; and
3. valid-memtrack and valid-memcleanup are implemented as the same allocation-counter check, although they have different semantics.

This is an umbrella issue for fixing those problems together and adding regression coverage for the individual SV-COMP memory-safety subproperties.

Related issues:

• smack cannot find this type of memory error #539 reports an escaped stack pointer that remains dereferenceable after its function returns. The maintainer discussion already suggests invalidating alloca objects at function returns.
• Missing memory safety bugs related to globals #190 required memory-safety checks for globals, including rejecting free on a global object. Its historical implementation distinguishes globals by their address range, but it does not provide general allocation provenance.
• Incorrect model of calloc with respect to memory safety #586 covers a separate zero-size calloc memory-safety modeling problem and should remain compatible with this work.

Public benchmark evidence

The experiment used the public SV-COMP 2026 Juliet_Test tasks with valid-memsafety.prp. Property parsing enabled every subproperty requested by the property file. The following counts include only definitive property results.

Wrong violated property: 514 tasks

• 423 tasks expected false(valid-free), but SMACK reported false(valid-memtrack).
• 91 tasks expected false(valid-deref), but SMACK reported false(valid-memtrack).

Affected public benchmark families include:

• CWE590_Free_Memory_Not_on_Heap
• CWE401_Invalid_Free
• CWE590_Deref_Out_Of_Scope_Memory_Not_on_Heap
• CWE590_Use_Stack_Memory_Out_Of_Scope

Representative tasks:

• CWE590_Free_Memory_Not_on_Heap__free_char_alloca_01_bad
• CWE590_Free_Memory_Not_on_Heap__free_int_declare_01_bad
• CWE590_Deref_Out_Of_Scope_Memory_Not_on_Heap__deref_char_declare_01_bad
• CWE590_Use_Stack_Memory_Out_Of_Scope__deref_int64_t_declare_01_bad

The direct valid-free or valid-deref check does not recognize the intended error. A later allocation-counter failure is reported instead.

valid-memtrack false alarms: 24 tasks

Twenty-four tasks expected true for valid-memsafety, but SMACK reported false(valid-memtrack). They are CWE401 flow variants 45 and 68 in which the allocation remains reachable through a global pointer at program exit.

Representative tasks:

• CWE401_Memory_Leak__int_malloc_45_bad
• CWE401_Memory_Leak__int64_t_calloc_68_bad
• CWE401_Memory_Leak__struct_twoIntsStruct_realloc_45_bad

These programs violate valid-memcleanup because allocated memory remains at exit, but they satisfy valid-memtrack because the allocation is still reachable. SMACK currently treats both properties as the same condition.

Root causes

1. No heap-allocation provenance

In share/smack/lib/smack.c, stack allocation and heap allocation ultimately use the same allocation state. $Alloc records whether an address is allocated, but not what kind of storage it denotes.

$free checks that the pointer is a live base address, but it has no explicit "allocated by malloc/calloc/realloc" condition. A stack object can therefore satisfy the current checks. The model then decrements $allocatedCounter, even though that counter is incremented only for heap allocation. This turns an invalid free into a later valid-memtrack violation.

A minimal expected regression is:

#include <stdlib.h>

int main(void) {
  int x;
  free(&x); // false(valid-free)
}

The model should track allocation provenance independently of liveness, for example with a heap-allocation map or an equivalent storage-kind abstraction. $free(p) must require a live heap base and must not mutate allocation/leak state after an invalid free.

2. No stack-lifetime invalidation

An alloca object remains marked allocated after its function returns, so bounds and $Alloc checks accept a later dereference. This is the behavior reported in #539.

A minimal expected regression is:

static int *escaped;

static void save_local(void) {
  int local = 1;
  escaped = &local;
}

int main(void) {
  save_local();
  return *escaped; // false(valid-deref)
}

Each function activation's stack objects should be invalidated on every normal and exceptional exit. llvm.lifetime.end can provide a more precise earlier endpoint when present, but correctness cannot rely exclusively on that intrinsic because frontends do not always emit it.

The design also needs tests for recursion, multiple return sites, escaped interior pointers, and use-after-return through globals and parameters.

3. valid-memtrack is not valid-memcleanup

The SV-COMP adapter maps both valid-memtrack and valid-memcleanup to the same internal MEMLEAK check. The prelude implements that check as:

assert {:valid_memtrack} $allocatedCounter == 0;

This is a cleanup condition: every nonzero-size heap allocation must have been deallocated at exit. It is not a memory-tracking condition, which permits live allocated objects that remain reachable.

These properties need distinct internal flags and implementations:

• valid-memcleanup: no outstanding heap allocations at the relevant program exit;
• valid-memtrack: no allocated object has become unreachable.

Implementing valid-memtrack requires a conservative reachability model rooted in live program pointers. If SMACK cannot model that soundly yet, it should report the property as unsupported/unknown instead of silently substituting valid-memcleanup.

Proposed work

• Represent allocation provenance: heap, stack activation, global, and invalid/freed.
• Require a live heap base in $free; reject stack, global, interior, and already-freed pointers as valid-free violations.
• Keep invalid frees from corrupting allocation-counter state or producing a secondary property alarm.
• Invalidate stack allocations on every function exit, using lifetime intrinsics for additional precision when available.
• Give valid-memtrack and valid-memcleanup separate internal properties and result labels.
• Implement sound reachability for valid-memtrack, or explicitly return unknown until it is supported.
• Ensure a counterexample is reported under the property actually violated (valid-free, valid-deref, valid-memtrack, or valid-memcleanup).
• Add small C regressions for each case above.
• Add a curated public Juliet regression subset covering the affected families and both good/bad variants.

Acceptance criteria

• free of stack or global storage reports false(valid-free) directly.
• dereferencing an escaped pointer after its stack object's lifetime ends reports false(valid-deref).
• an allocated object retained through a live global pointer satisfies valid-memtrack but violates valid-memcleanup.
• a genuinely lost heap object violates valid-memtrack.
• existing heap use-after-free, double-free, bounds, global-memory, and zero-size-allocation tests remain valid.
• the representative Juliet tasks above produce the expected exact SV-COMP subproperty result.

[shaobo-he]

A fourth gap in the same area, measured while auditing #853, on develop @ 9dca4d9.

In SV-COMP mode, valid-memsafety.prp selects valid-deref only. share/smack/svcomp/utils.py:57 tests the subproperties in order:

if "valid-deref" in prop:
    args.check = VProperty.VALID_DEREF

valid-memsafety.prp requests all three of valid-free, valid-deref and valid-memtrack, and valid-deref matches first, so args.check ends up naming that one property. memsafety_subproperty_selection then rewrites every assert {:valid_free} and assert {:valid_memtrack} to assert true, and a valid-free or valid-memtrack violation can never be reported under the property file that asks for it. That is consistent with the note in the description here that the experiment "enabled every subproperty requested by the property file" — the default does not.

Measured over 172 tasks with valid-memsafety.prp through smack-svcomp-wrapper.sh (300 s each): 33 expected-false tasks are reported as verified, and the family is exactly what the mapping predicts —

category	missed	of
ldv-memsafety	23	45
memsafety	7	40
list-ext-properties	2	15
memsafety-bftpd	1	3

19 of the 23 ldv-memsafety misses are the memleaks_test* family — leak tasks, whose property is never checked. Representative: memleaks_test1-1.i, memleaks_test13_1.i, memleaks_test21-1.i, memleaks_test5_1.i.

This looks like it belongs to this umbrella: it is subproperty selection rather than subproperty implementation, but it has to be right before the memtrack/memcleanup split in item 3 can be observed on these benchmarks at all.