Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
shaobo-he merged 3 commits into from
Aug 27, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
42c08dd
Treat a size-zero allocation as a real, inaccessible block
shaobo-he Aug 26, 2026
85c0333
Frame the allocation map across free(NULL)
shaobo-he Aug 26, 2026
88d2bbf
Give a global with no bytes a size of zero
shaobo-he Aug 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 24 additions & 8 deletions lib/smack/SmackRep.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1267,6 +1267,12 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,

unsigned size = 0;
bool external = false;
// Whether `size` is this object's real size. It is not for an external
// declaration, whose definition we cannot see, nor for an unsized type;
// both fall back to a placeholder below. An object whose type is sized but
// empty -- a zero-length array, an empty struct -- has a real size of zero,
// which has to be told apart from those two cases.
bool sizeKnown = false;

if (v->isThreadLocal())
ax.push_back(Attr::attr("treadLocal"));
Expand All @@ -1281,15 +1287,19 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,
if (const PointerType *t = dyn_cast<const PointerType>(g->getType())) {

// in case we can determine the size of the element type ...
if (t->getPointerElementType()->isSized())
if (t->getPointerElementType()->isSized()) {
size = storageSize(t->getPointerElementType());
sizeKnown = true;
}

// otherwise (e.g. for function declarations), use a default size
else
size = 1024;

} else
} else {
size = storageSize(g->getType());
sizeKnown = true;
}

if (!g->hasName() || !STRING_CONSTANT.match(g->getName().str())) {
if (numElems > 1)
Expand All @@ -1303,22 +1313,28 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,

decls.push_back(Decl::constant(name, Naming::PTR_TYPE, ax, false));

if (!size)
size = targetData->getPrefTypeAlignment(v->getType());
// Reserving address space and recording the object's size are two different
// jobs, and they part company for an object with no bytes: it still needs an
// address of its own, distinct from every other object, but every access to
// it is out of bounds. Give it the type's alignment to sit in and record its
// size as it is.
unsigned reserved =
size ? size : targetData->getPrefTypeAlignment(v->getType());

// Add padding between globals to be able to check memory overflows/underflows
const unsigned globalsPadding = 1024;
if (external) {
decls.push_back(Decl::axiom(Expr::eq(
Expr::id(name), Expr::fn("$add.ref", Expr::id(Naming::GLOBALS_BOTTOM),
pointerLit(externsOffset -= size)))));
pointerLit(externsOffset -= reserved)))));
} else {
decls.push_back(Decl::axiom(Expr::eq(
Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding)))));
decls.push_back(Decl::axiom(
Expr::eq(Expr::id(name),
pointerLit(globalsOffset -= (reserved + globalsPadding)))));
}

if (!llvm::isa<Function>(v) && allocate)
globalAllocations[v] = size;
globalAllocations[v] = sizeKnown ? size : reserved;

return decls;
}
Expand Down
104 changes: 61 additions & 43 deletions share/smack/lib/smack.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1649,13 +1649,25 @@ void __SMACK_decls(void) {
D("function $base(ref) returns (ref);");
D("var $allocatedCounter: int;\n");

// A request of size zero is a real allocation. We adopt the SV-COMP rule
// (sv-comp.sosy-lab.org, rules.php, "Definitions": "We assume that the
// functions malloc and alloca always return a valid pointer, i.e., the
// memory allocation never fails"), which conforms to the C standard: C11
// (ISO/IEC 9899:2011, N1570) 7.22.3 paragraph 1 leaves malloc(0)
// 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. So every $$alloc below reserves address
// space for a size-zero request as if the size were one (the pointer is
// nonzero and distinct from every other object), records size zero (any
// access is an invalid dereference), and the block is freed and tracked
// like any other; before this the default model left the result
// unassigned, i.e. an arbitrary pointer.
D("procedure $malloc(n: ref) returns (p: ref)\n"
"modifies $allocatedCounter;\n"
"{\n"
" call corral_atomic_begin();\n"
" if ($ne.ref.bool(n, $0.ref)) {\n"
" $allocatedCounter := $allocatedCounter + 1;\n"
" }\n"
" $allocatedCounter := $allocatedCounter + 1;\n"
" call p := $$alloc(n);\n"
" call corral_atomic_end();\n"
"}\n");
Expand All @@ -1670,6 +1682,7 @@ void __SMACK_decls(void) {
D("procedure $galloc(base_addr: ref, size: ref)\n"
"{\n"
" assume $Size(base_addr) == size;\n"
" assume $base(base_addr) == base_addr;\n"
" assume (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
"$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
"size)) ==> $base(addr) == base_addr);\n"
Expand All @@ -1680,18 +1693,18 @@ void __SMACK_decls(void) {
"modifies $Alloc, $CurrAddr;\n"
"{\n"
" assume $sle.ref.bool($0.ref, n);\n"
" if ($slt.ref.bool($0.ref, n)) {\n"
" p := $CurrAddr;\n"
" havoc $CurrAddr;\n"
" assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
" assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
" p := $CurrAddr;\n"
" havoc $CurrAddr;\n"
" assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
" assume $sgt.ref.bool($CurrAddr, p);\n"
" assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
"$MALLOC_TOP);\n"
" assume $Size(p) == n;\n"
" assume (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
" assume $Size(p) == n;\n"
" assume $base(p) == p;\n"
" assume (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
"$sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == "
"p);\n"
" $Alloc[p] := true;\n"
" }\n"
" $Alloc[p] := true;\n"
"}\n");

D("procedure $free(p: ref)\n"
Expand All @@ -1717,6 +1730,7 @@ void __SMACK_decls(void) {
D("procedure $galloc(base_addr: ref, size: ref);\n"
"modifies $Alloc, $Size;\n"
"ensures $Size[base_addr] == size;\n"
"ensures $base(base_addr) == base_addr;\n"
"ensures (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
"$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
"size)) ==> $base(addr) == base_addr);\n"
Expand All @@ -1729,17 +1743,17 @@ void __SMACK_decls(void) {
D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
"modifies $Alloc, $Size;\n"
"ensures $sle.ref.bool($0.ref, n);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && "
"$slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n"
"ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n"
"ensures $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, "
"$sub.ref($MALLOC_TOP, n));\n"
"ensures !old($Alloc[p]);\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.disjoint\"} old($Alloc[q]) "
"==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, "
"$Size[q]), p)));\n"
"ensures $Alloc[p];\n"
"ensures $Size[p] == n;\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} "
"q != p ==> $Size[q] == old($Size[q]));\n"
"ensures $base(p) == p;\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} q "
"!= p ==> $Size[q] == old($Size[q]));\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
"q != p ==> $Alloc[q] == old($Alloc[q]));\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
Expand All @@ -1754,6 +1768,9 @@ void __SMACK_decls(void) {
"ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: "
"{:qid \"smack.free.frame.alloc\"} {$Alloc[q]} q != p ==> $Alloc[q] == "
"old($Alloc[q]));\n"
"ensures $eq.ref.bool(p, $0.ref) ==> (forall q: ref :: "
"{:qid \"smack.free.null.frame.alloc\"} {$Alloc[q]} $Alloc[q] == "
"old($Alloc[q]));\n"
"ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
"old($allocatedCounter) - 1;\n"
"ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
Expand All @@ -1769,6 +1786,7 @@ void __SMACK_decls(void) {
D("procedure $galloc(base_addr: ref, size: ref);\n"
"modifies $Alloc;\n"
"ensures $Size(base_addr) == size;\n"
"ensures $base(base_addr) == base_addr;\n"
"ensures (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
"$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
"size)) ==> $base(addr) == base_addr);\n"
Expand All @@ -1779,18 +1797,17 @@ void __SMACK_decls(void) {
D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
"modifies $Alloc, $CurrAddr;\n"
"ensures $sle.ref.bool($0.ref, n);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, "
"n), old($CurrAddr)) && p == old($CurrAddr);\n"
"ensures $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr));\n"
"ensures $sgt.ref.bool($CurrAddr, old($CurrAddr));\n"
"ensures p == old($CurrAddr);\n"
"ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
"$MALLOC_TOP);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $Size(p) == n;\n"
"ensures $slt.ref.bool($0.ref, n) ==> (forall q: ref :: "
"{:qid \"smack.alloc.base\"} {$base(q)} $sle.ref.bool(p, q) && "
"$slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $Alloc[p];\n"
"ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == "
"$0.ref;\n"
"ensures $eq.ref.bool(n, $0.ref)==> $Alloc[p] == old($Alloc)[p];\n"
"ensures $Size(p) == n;\n"
"ensures $base(p) == p;\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
"$sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == "
"p);\n"
"ensures $Alloc[p];\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
"q != p ==> $Alloc[q] == old($Alloc[q]));\n");

Expand All @@ -1802,6 +1819,9 @@ void __SMACK_decls(void) {
"ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: "
"{:qid \"smack.free.frame.alloc\"} {$Alloc[q]} q != p ==> $Alloc[q] == "
"old($Alloc[q]));\n"
"ensures $eq.ref.bool(p, $0.ref) ==> (forall q: ref :: "
"{:qid \"smack.free.null.frame.alloc\"} {$Alloc[q]} $Alloc[q] == "
"old($Alloc[q]));\n"
"ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
"old($allocatedCounter) - 1;\n"
"ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
Expand All @@ -1819,17 +1839,17 @@ void __SMACK_decls(void) {
#if MEMORY_MODEL_NO_REUSE_IMPLS
D("var $CurrAddr:ref;\n");

// Size zero: see the memory-safety $malloc above.
D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n"
"modifies $CurrAddr;\n"
"{\n"
" assume $sge.ref.bool(n, $0.ref);\n"
" if ($sgt.ref.bool(n, $0.ref)) {\n"
" p := $CurrAddr;\n"
" havoc $CurrAddr;\n"
" assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
" assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
" p := $CurrAddr;\n"
" havoc $CurrAddr;\n"
" assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
" assume $sgt.ref.bool($CurrAddr, p);\n"
" assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
"$MALLOC_TOP);\n"
" }\n"
"}\n");

D("procedure $free(p: ref);\n");
Expand All @@ -1841,17 +1861,16 @@ void __SMACK_decls(void) {
D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
"modifies $Alloc, $Size;\n"
"ensures $sle.ref.bool($0.ref, n);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && "
"$slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n"
"ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n"
"ensures $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, "
"$sub.ref($MALLOC_TOP, n));\n"
"ensures !old($Alloc[p]);\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.disjoint\"} old($Alloc[q]) "
"==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, "
"$Size[q]), p)));\n"
"ensures $Alloc[p];\n"
"ensures $Size[p] == n;\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} "
"q != p ==> $Size[q] == old($Size[q]));\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} q "
"!= p ==> $Size[q] == old($Size[q]));\n"
"ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
"q != p ==> $Alloc[q] == old($Alloc[q]));\n");

Expand All @@ -1867,12 +1886,11 @@ void __SMACK_decls(void) {
D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
"modifies $CurrAddr;\n"
"ensures $sle.ref.bool($0.ref, n);\n"
"ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, "
"n), old($CurrAddr)) && p == old($CurrAddr);\n"
"ensures $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr));\n"
"ensures $sgt.ref.bool($CurrAddr, old($CurrAddr));\n"
"ensures p == old($CurrAddr);\n"
"ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
"$MALLOC_TOP);\n"
"ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == "
"$0.ref;\n");
"$MALLOC_TOP);\n");

D("procedure $free(p: ref);\n");
#endif
Expand Down
18 changes: 18 additions & 0 deletions share/smack/lib/stdlib.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,24 @@ void *calloc(size_t num, size_t size) {
return ret;
}

// realloc is modelled as free followed by malloc, which gives the two
// boundary cases their C11 meaning through the allocation procedures in
// smack.c rather than by special-casing them here:
//
// realloc(NULL, n) is malloc(n), because free(NULL) is a no-op (7.22.3.3).
// realloc(p, 0) frees p and returns a size-zero block. Under the rule
// adopted in smack.c -- allocation never fails, and a size-zero request
// behaves "as if the size were some nonzero value, except that the
// returned pointer shall not be used to access an object" (7.22.3p1) --
// that block is a real allocation: it is not null, it may not be
// dereferenced, and it must be freed. So a program that drops the result
// of realloc(p, 0) leaks it, which test/c/memory-safety/
// realloc_zero_leak_fail.c pins. glibc instead frees p and returns null,
// and C23 makes the call undefined, so code that uses realloc(p, 0) as a
// spelling of free() is reported as a leak here; write free(p) instead.
//
// What this model does not do is preserve the contents of the old block
// across the call, which 7.22.3.5p2 requires.
void *realloc(void *ptr, size_t size) {
void *ret;
__VERIFIER_atomic_begin();
Expand Down
17 changes: 17 additions & 0 deletions test/c/basic/global_zero.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
#include "smack.h"

// @expect verified

// A global with no bytes still gets an address distinct from every other
// object's.
int g[0];
int h[2];
int k;

int main(void) {
__VERIFIER_assert((char *)g != (char *)h);
__VERIFIER_assert((char *)g != (char *)&k);
h[0] = 7;
__VERIFIER_assert(h[0] == 7);
return 0;
}
21 changes: 21 additions & 0 deletions test/c/basic/malloc_zero.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#include "smack.h"
#include <stdlib.h>

// @expect verified

// Without memory-safety checks the result of malloc(0) is still a fresh
// non-null pointer, distinct from every other allocation, under every
// memory model.
int main(void) {
char *p = malloc(0);
char *q = malloc(0);
int *r = malloc(sizeof(int));
__VERIFIER_assert(p != 0);
__VERIFIER_assert(q != 0);
__VERIFIER_assert(p != q);
__VERIFIER_assert((void *)p != (void *)r);
free(p);
free(q);
free(r);
return 0;
}
10 changes: 10 additions & 0 deletions test/c/basic/malloc_zero_fail.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
#include "smack.h"
#include <stdlib.h>

// @expect error

int main(void) {
char *p = malloc(0);
__VERIFIER_assert(p == 0); // malloc(0) does not return a null pointer
return 0;
}
14 changes: 14 additions & 0 deletions test/c/memory-safety/alloca_zero_deref_fail.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#include "smack.h"
#include <stdlib.h>

// @expect error

// A variable-length array of length zero is a size-zero stack allocation;
// SV-COMP's rule covers alloca as well as malloc.
int main(void) {
unsigned n = __VERIFIER_nondet_unsigned();
__VERIFIER_assume(n == 0);
char a[n];
a[0] = 1;
return 0;
}
13 changes: 13 additions & 0 deletions test/c/memory-safety/calloc_zero_deref_fail.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
#include "smack.h"
#include <stdlib.h>

// @expect error

// calloc(0, n) allocates zero bytes (SMACK's calloc may also fail, and a
// null dereference is invalid too).
int main(void) {
int *p = calloc(0, sizeof(int));
p[0] = 1;
free(p);
return 0;
}
Loading
Loading