cprover: establish liveness for the __CPROVER_allocate side effect

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;
+}

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$
+--

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;
+}

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$
+--

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;
+}

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.

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;
   }