Treat a size-zero allocation as a real, inaccessible block

[shaobo-he]

malloc(0) returned an arbitrary pointer under SMACK's default memory model. This fixes it in all three models, in both the plain and the --check=memory-safety builds, and closes a second hole the memory-safety free had for null arguments.

The rule

This adopts the SV-COMP rule — "malloc and alloca always return a valid pointer, i.e., the memory allocation never fails" (rules, "Definitions") — which conforms to the C standard: C11 §7.22.3 ¶1 makes a size-zero allocation implementation-defined, "either a null pointer is returned, or the behavior is as if the size were some nonzero value, except that the returned pointer shall not be used to access an object", and the rule selects the second behavior. That is also what glibc does.

What SMACK did

model	malloc(0) before	consequence
no-reuse-impls (default)	unassigned — the body only assigns p inside if (n > 0)	the program continues with an arbitrary pointer: it can alias a live object, so a store through it clobbers that object and a free of it is an invalid free
reuse	NULL, and $Alloc[0] := true	a second malloc(0) is unsatisfiable (p == 0 again but !old($Alloc[p])), so everything after it verifies vacuously — assert(p != 0) and assert(p == 0) both "verify"
no-reuse	NULL	not what SV-COMP assumes; and free of it hit the hole below

The aws-c-common SV-COMP harnesses reach this through bounded_malloc(cursor->len), bounded_malloc(cap) and bounded_malloc(list->current_size) with unconstrained sizes.

The fix

The n > 0 guards are what gave a size-zero request that treatment, so they go: every clause of every $$alloc now holds unconditionally. For a positive size nothing changes — each clause said exactly this under the guard. For a size-zero request the procedure reserves address space as if the size were one while recording size zero, so any access is an invalid dereference under --check=memory-safety and free is valid.

Two facts have to be stated that the guarded text could not:

• $CurrAddr advances strictly. $CurrAddr - n >= p permits $CurrAddr == p when n == 0, so a second request could return the same address.
• $base(p) == p. The range quantifier over [p, p + n) is empty for n == 0, and $free requires it.

The reuse model's disjointness clause is unchanged from develop — its strict < already places a size-zero block outside every live block, and !old($Alloc[p]) gives distinctness independently. $malloc counts the block, so --check=memleak reports it when it leaks and stays balanced when it is freed. alloca, calloc and realloc go through the same procedure.

An earlier revision of this branch expressed the same rule as max(n, 1) inside the contract terms. It is equivalent, but the if-expression is expensive for the bit-vector solvers, so the guard-free form above replaced it — see Cost below.

free(NULL). The reuse and no-reuse memory-safety $free is spec-only, and every postcondition about $Alloc was guarded by p != 0, so after free(NULL) — a no-op per C11 §7.22.3.3 — nothing constrained the allocation map and the next free(q) of a live block failed its precondition. free(NULL) and the realloc(NULL, n) idiom triggered it directly; every free of a malloc(0) result did too. A frame for the p == 0 case closes it.

Globals with no bytes (#854). The same conflation existed for globals, and the third commit fixes it. globalDecl computed one number and used it both to reserve address space, so that distinct globals get distinct addresses, and to record the object's size — which for an empty object are different numbers. A zero-length array got its type's alignment as its size, so int g[0]; g[0] = 1; verified under --check=memory-safety in every model. The reservation keeps the alignment, the recorded size is now the real one, and $galloc gains the same $base(base_addr) == base_addr that $$alloc needed. An external declaration and an unsized type keep their placeholders, so only a genuinely empty object changes.

realloc(p, 0). realloc is modelled as free + malloc, so the rule decides both boundary cases and neither is special-cased. realloc(NULL, n) is malloc(n). realloc(p, 0) frees p and returns a size-zero block that must itself be freed, so using the call as a spelling of free is a leak — glibc instead frees and returns null, and C23 makes the call undefined. The comment on realloc in stdlib.c works this through, and two tests pin both verdicts.

Tests

Every row is checked under all three memory models with Boogie and Corral. Develop's verdicts are per model, no-reuse-impls / reuse / no-reuse.

test	expects	develop	this branch
basic/malloc_zero.c — non-null, pairwise distinct	verified	E / vacuous / E	V V V
basic/malloc_zero_fail.c — asserts p == 0	error	E / vacuous / V	E E E
memory-safety/malloc_zero.c — free is valid	verified	E V E	V V V
malloc_zero_deref_fail, _read_fail, _wide_deref_fail — byte write, read, int write	error	E E E	E E E
malloc_zero_memset_fail, _memcpy_in_fail, _memcpy_out_fail — one byte via a library call	error	E E E	E E E
malloc_zero_no_access.c — zero-length memset/memcpy, p + 0, comparison	verified	E E E	V V V
calloc_zero_deref_fail, alloca_zero_deref_fail (VLA of length 0), realloc_zero_deref_fail	error	E E E	E E E
realloc_grow_zero.c — a zero block grown to 4 bytes, then used	verified	E V V	V V V
realloc_zero_leak_fail.c — realloc(p, 0) used as free (--check=memleak)	error	V V V	E E E
realloc_zero_freed.c — the results of realloc(p, 0) and realloc(NULL, 0) freed	verified	E V V	V V V
malloc_zero_leak_fail.c (--check=memleak)	error	V V V	E E E
malloc_zero_freed.c (--check=memleak; malloc(0) and calloc(0, 4) freed)	verified	E V E	V V V
free_null_then_free.c — free(NULL), realloc(NULL, n), then frees of live blocks	verified	V E E	V V V
global_zero_deref_fail.c — store into a zero-length global (#854)	error	V V V	E E E
global_zero_no_access.c — its neighbours stay accessible	verified	V V V	V V V
basic/global_zero.c — a zero-length global's address is distinct	verified	V V V	V V V

Where develop already says "error" on a dereference row, it is the null-pointer models and the arbitrary-pointer model failing for different reasons; this branch fails them because the block has no bytes. Develop's own free_null.c is unchanged. The two malloc_nondet tests assumed a nonzero size with a comment that malloc(0) "can return anything"; the assumption is about the p[x - 1] access and is now stated that way.

Cost

The max(n, 1) revision was measurably slower for the bit-vector solvers on programs that never call malloc(0); the guard-free form recovers most of it. Sequential, interleaved, on an idle machine:

configuration	develop	max(n,1) revision	this branch
basic/list.c --pointer-encoding=bit-vector --mem-mod no-reuse --unroll=4 (3 reps)	13.6 / 12.1 / 13.5 s	20.7 / 22.1 / 21.0 s	15.9 / 14.5 / 15.8 s
memory-safety/array_free1.c --integer-encoding=bit-vector --mem-mod reuse --unroll=6 --check=memory-safety (2 reps)	139 / 147 s	182 / 191 s	155 / 157 s

All verify in every cell. The residual 9–18 % over develop is the cost of modelling a size-zero allocation at all, where develop did nothing. Under the default encoding the earlier measurements showed parity (data/two_arrays.c 28.9 / 30.5 s vs 31.1 / 31.2 s; array_free1.c --unroll=6 14.2 / 11.9 s vs 11.1 / 13.0 s).

Verification

Measured on this formulation:

• test/c/memory-safety, exhaustive (all three memory models × Boogie + Corral): 276 passed, 0 failed, 0 timeouts, including the twelve new tests.
• The table above: 21 size-zero programs × 3 models, every verdict as expected.
• Emitted Boogie before and after the Zero-length global objects are given their type's alignment as their size #854 commit, 407 programs × 2 memory models: 702 identical, and every one of the 104 differences is either the new one-line $galloc fact or $galloc(g, 8) becoming $galloc(g, 0) for the zero-length global in the new regression. Nothing else moves.

Measured on the max(n, 1) revision of the same change, which produces identical verdicts on all 54 configurations of that table:

• Full regression, exhaustive, 15 folders (basic 522, data 492, strings 186, bits 336, float 216, unroll 60, ntdrivers-simplified 60, locks 78, contracts 27, targeted-checks 84, special 60, simd 30, pthread 30, pthread_extras 22): 0 failures, 0 timeouts.
• SV-COMP memory safety through the wrapper, develop vs branch, 300 s each: memsafety, memsafety-ext, -ext2, -bftpd, heap-manipulation, ldv-memsafety, array-memsafety, list-properties, list-ext-properties — 172 task pairs, verdicts identical. The one differing pair re-ran sequentially to "no errors" on both.
• aws-c-common through the SV-COMP wrapper, 104 (file, property) pairs including all 41 harnesses that can pass a zero size: every verdict and timeout identical to develop.
• Six adversarial audit lenses (layout invariants, every encoding, --pthread, every stdlib allocator, two SV-COMP sweeps, adversarial soundness) found nothing attributable to the change.

Found along the way, not fixed here

All pre-existing on develop and unaffected by this change:

• realloc does not preserve the old block's contents (C11 §7.22.3.5 ¶2), so legal programs are reported buggy. Noted in the new stdlib.c comment.
• The SV-COMP wrapper maps valid-memsafety.prp to valid-deref only, so valid-free and valid-memtrack bugs are never reported; eight expected-false tasks verify because of it.
• free of stack memory passes the heap check — allocas draw from the same $CurrAddr stream, so int x; free(&x) verifies under valid-free.
• calloc may return NULL while malloc and alloca never fail, which is inconsistent with the rule adopted here.
• strlen/strcpy are unchecked externals without --strings; --pthread with reuse/no-reuse is rejected by Corral ("Ensures has a shared global").
• Every aws_array_list_* harness is vacuous: assume_abort_if_not(aws_array_list_is_bounded(&list, 9223372036854775808U, 2)) is unsatisfiable because the literal 2^63 renders as the signed representative.

🤖 Generated with Claude Code