From e6236758436333740c27a48d8f6dfd04051e2819 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Jun 2026 19:38:00 +0000 Subject: [PATCH] cprover: establish liveness for the __CPROVER_allocate side effect The state encoder special-cases calls to `malloc`/`posix_memalign`/`realloc` by tying the allocation to the current state (`update_state(state, lhs, allocate_exprt(state, size, type))`), which establishes that the result is a live dynamic object. The generic `__CPROVER_allocate` side effect, however, was left as-is during expression evaluation, so an assignment `p = __CPROVER_allocate(...)` never established the object's liveness. As a result, "pointer safe" properties over a freshly allocated object were spuriously refuted, even though cprover has axioms for `ID_allocate`. A function merely named `malloc` (even bodyless) was handled correctly while the same `__CPROVER_allocate` under any other name was not -- the behavior keyed on the C library name rather than the GOTO primitive. Handle the `__CPROVER_allocate` side effect uniformly in `evaluate_expr_rec` by rewriting it to an `allocate_exprt` tied to the current state, mirroring the malloc special case. This makes cprover treat the GOTO allocation primitive directly, independent of any C-level allocator name. The guard requires exactly two operands (matching c_typecheck_expr, which rejects any other ID_allocate) and the size is taken from the first operand. The second operand -- the zero-initialisation flag, with which calloc lowers to `__CPROVER_allocate(size, 1)` -- is not modelled: like the malloc/posix_memalign/realloc cases the allocated contents remain nondeterministic. This is a sound over-approximation. Soundness is preserved: safe allocations verify (pointer safe), while out-of-bounds accesses and functional bugs over allocated objects are still refuted. Regression tests in regression/cprover/pointers: allocate1 proves the in-bounds case safe and pins the `allocate(state, ...)` rewrite of the side effect; allocate2 confirms an out-of-bounds access is still refuted; allocate3 documents the unmodelled zero-initialisation as a KNOWNBUG (a read of calloc-style memory is refuted to be 0 rather than proven). Co-authored-by: Kiro --- regression/cprover/pointers/allocate1.c | 14 ++++++++++++ regression/cprover/pointers/allocate1.desc | 10 +++++++++ regression/cprover/pointers/allocate2.c | 13 +++++++++++ regression/cprover/pointers/allocate2.desc | 8 +++++++ regression/cprover/pointers/allocate3.c | 15 +++++++++++++ regression/cprover/pointers/allocate3.desc | 13 +++++++++++ src/cprover/state_encoding.cpp | 26 ++++++++++++++++++++++ 7 files changed, 99 insertions(+) create mode 100644 regression/cprover/pointers/allocate1.c create mode 100644 regression/cprover/pointers/allocate1.desc create mode 100644 regression/cprover/pointers/allocate2.c create mode 100644 regression/cprover/pointers/allocate2.desc create mode 100644 regression/cprover/pointers/allocate3.c create mode 100644 regression/cprover/pointers/allocate3.desc diff --git a/regression/cprover/pointers/allocate1.c b/regression/cprover/pointers/allocate1.c new file mode 100644 index 00000000000..9bf9c490900 --- /dev/null +++ b/regression/cprover/pointers/allocate1.c @@ -0,0 +1,14 @@ +// Regression test for cprover establishing liveness of __CPROVER_allocate. +// Before the fix the "pointer p safe" checks over the allocated object were +// spuriously refuted; after the fix they are proved like for malloc. +void *__CPROVER_allocate(__CPROVER_size_t, int); + +int *p; + +int main() +{ + p = __CPROVER_allocate(sizeof(int) * 10, 0); + p[2] = 123; + __CPROVER_assert(p[2] == 123, "property 1"); + return 0; +} diff --git a/regression/cprover/pointers/allocate1.desc b/regression/cprover/pointers/allocate1.desc new file mode 100644 index 00000000000..67427331684 --- /dev/null +++ b/regression/cprover/pointers/allocate1.desc @@ -0,0 +1,10 @@ +CORE +allocate1.c +--text --solve --inline +^EXIT=0$ +^SIGNAL=0$ +^\(\d+\) ∀ ς : state \. S\d+\(ς\) ⇒ S\d+\(ς\[❝main::\$tmp::malloc_value❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[\d+\]\)\)\]\)$ +^\[main\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$ +^\[main\.pointer\.2\] line \d+ pointer .* safe: SUCCESS$ +^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ +-- diff --git a/regression/cprover/pointers/allocate2.c b/regression/cprover/pointers/allocate2.c new file mode 100644 index 00000000000..602aaccbc2f --- /dev/null +++ b/regression/cprover/pointers/allocate2.c @@ -0,0 +1,13 @@ +// Soundness companion: an out-of-bounds access to an __CPROVER_allocate'd +// object must still be refuted (the liveness fix must not mask it). +void *__CPROVER_allocate(__CPROVER_size_t, int); + +int *p; + +int main() +{ + p = __CPROVER_allocate(sizeof(int), 0); + p[5] = 123; + __CPROVER_assert(p[5] == 123, "property 1"); + return 0; +} diff --git a/regression/cprover/pointers/allocate2.desc b/regression/cprover/pointers/allocate2.desc new file mode 100644 index 00000000000..5662b470707 --- /dev/null +++ b/regression/cprover/pointers/allocate2.desc @@ -0,0 +1,8 @@ +CORE +allocate2.c +--text --solve --inline +^EXIT=10$ +^SIGNAL=0$ +^\[main\.pointer\.1\] line \d+ pointer .* safe: REFUTED$ +^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ +-- diff --git a/regression/cprover/pointers/allocate3.c b/regression/cprover/pointers/allocate3.c new file mode 100644 index 00000000000..567105ca10f --- /dev/null +++ b/regression/cprover/pointers/allocate3.c @@ -0,0 +1,15 @@ +// Known limitation: __CPROVER_allocate(size, 1) is the calloc lowering and +// requests zero-initialised memory, but the cprover state encoder drops the +// zero-init operand and models nondeterministic contents (like malloc), so a +// read of the freshly-allocated memory cannot be proven to be 0. Documented +// as a KNOWNBUG; promote to CORE if/when zeroing is modelled. +void *__CPROVER_allocate(__CPROVER_size_t, int); + +int *p; + +int main() +{ + p = __CPROVER_allocate(sizeof(int), 1); // calloc-style: zero-initialised + __CPROVER_assert(p[0] == 0, "property 1"); + return 0; +} diff --git a/regression/cprover/pointers/allocate3.desc b/regression/cprover/pointers/allocate3.desc new file mode 100644 index 00000000000..cba01aa2828 --- /dev/null +++ b/regression/cprover/pointers/allocate3.desc @@ -0,0 +1,13 @@ +KNOWNBUG +allocate3.c +--text --solve --inline +^EXIT=0$ +^SIGNAL=0$ +^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ +-- +-- +The calloc lowering __CPROVER_allocate(size, 1) requests zero-initialised +memory, but the cprover state encoder drops the zero-init operand and models +nondeterministic contents (matching malloc/posix_memalign/realloc), so +`p[0] == 0` is currently REFUTED rather than SUCCESS. Marked KNOWNBUG to +document the limitation; promote to CORE if/when zeroing is modelled. diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 39e89cb0d45..decbfe4bc1d 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -338,6 +338,32 @@ exprt state_encodingt::evaluate_expr_rec( } else if(what.id() == ID_side_effect) { + const auto &side_effect = to_side_effect_expr(what); + if( + side_effect.get_statement() == ID_allocate && + side_effect.operands().size() == 2 && + side_effect.type().id() == ID_pointer) + { + // __CPROVER_allocate is handled like the malloc call (see the malloc + // handling in function_call_symbol below): tie the allocation to the + // current state so its result is a live dynamic object. Without this, + // the generic allocate side effect leaves liveness unestablished, and + // "pointer safe" properties over the allocated object are spuriously + // refuted. c_typecheck_expr rejects an ID_allocate without exactly two + // operands (size, zero-init flag), so the size() == 2 check documents + // that invariant rather than building an allocation from a partial + // operand list; the side effect's type is always void *, so the + // ID_pointer conjunct is defensive only. + // + // NOTE: operands()[1] is the zero-initialisation flag (calloc lowers to + // __CPROVER_allocate(size, 1)); like the malloc/posix_memalign/realloc + // cases this backend does not model zeroing, so the allocated contents + // are left nondeterministic. TODO: model zeroing. + auto size_evaluated = evaluate_expr_rec( + loc, state, side_effect.operands().front(), bound_symbols); + return allocate_exprt{ + state, size_evaluated, to_pointer_type(side_effect.type())}; + } // leave as is return what; }