A malloc'd struct cannot be initialised field-by-field (pointer analogue of #101)

[akashlal]

Versions: PAL a9ebbed · F*/Pulse nightly 2026-08-27 · Clang 20.1.8

Closely related to #101 (Using local struct requires lemma call), but for a malloc'd pointer, where the workaround given there does not appear to exist.

Summary

Freshly allocated storage is pts_to_uninit, and it can only leave that state via a whole-struct assignment (*p = (T){...}). Initialising the same struct field by field — the far more common C idiom — does not verify.

Minimal repro

#include "pal.h"
#include <stdlib.h>
#include <stdint.h>

typedef struct R { double x; double y; } R;
_allocated typedef R *R_ptr;

/* 1. whole-struct assignment, then free.                          VERIFIES */
void x1_whole_then_free(void)
{
    R *t = malloc(sizeof(R));
    *t = (R){0.0, 0.0};
    free(t);
}

/* 2. whole-struct assignment, then return the pointer.            VERIFIES */
R_ptr x2_whole_then_return(void)
{
    R *t = malloc(sizeof(R));
    *t = (R){0.0, 0.0};
    return t;
}

/* 3. FIELD-BY-FIELD, then return the pointer.                        FAILS */
R_ptr x3_fields_then_return(void)
{
    R *t = malloc(sizeof(R));
    t->x = 0.8;
    t->y = 0.16;
    return t;
}

/* 4. whole-struct assignment FIRST, then field writes.            VERIFIES */
R_ptr x4_whole_then_fields(void)
{
    R *t = malloc(sizeof(R));
    *t = (R){0.0, 0.0};
    t->x = 0.8;
    return t;
}

$ run-fstar.sh --include out out/Func_x3_fields_then_return.fst
Cannot prove: Struct_R.struct_r__aux_raw_unfolded __anf0

The fourth case is the informative one: once the struct has been initialised wholesale, later field writes are fine. So the blocker is specifically the initial transition out of pts_to_uninit, not field writes as such.

(Probe design note: a function that mallocs and neither frees nor returns the pointer fails regardless, on unaccounted ownership rather than on the property under test. Every case above therefore frees or returns.)

Relationship to #101

#101 reports the same __aux_raw_unfolded obligation for a local struct, with the workaround

_ghost_stmt(struct_s__aux_raw_unfold_uninit var_v);

That works for a local — we use it routinely, via _ghost_stmt($unfold-uninit(T) $&(x));, where $&(x) names a real reference cell. We could not find an equivalent through a pointer:

• _ghost_stmt($unfold-uninit(R) t) → Error 189, Ill-typed term
• _ghost_stmt($unfold-uninit(R) $(t)) → Cannot prove ... __aux_raw_unfolded

If a working form exists, it is not discoverable from doc/pal_surface_syntax.md, which says only that the uninit-variant unfold lemma is "struct only; not auto-applied".

Note: malloc itself is fine

We initially misdiagnosed this as "malloc has no postcondition", which was wrong and is worth stating: PAL models malloc well. test/malloc/malloc.c verifies completely, including

int *arr = (int *) malloc(sizeof(int) * 10);
_assert(arr._length == 10);

so allocation carries both ownership and length. The limitation is the narrower one above.

Impact

We are using PAL to prove spatial memory safety on the Olden and Ptrdist benchmark suites, holding the C source fixed and adding only annotations. olden/power builds its tree with:

t = (Root) malloc(sizeof(*t));
for (i=0; i<NUM_FEEDERS; i++) { ...; t->feeders[i] = l; }
t->theta_R = 0.8;
t->theta_I = 0.16;
return t;

This blocks all four build_* functions and 6 of power's 42 bounds obligations. The one-line C fix (*t = (Root){0};) is not available to us, since we hold the source fixed so that the proof is about the program as written.

Suggested fix

Either make the uninit-variant unfold reachable through a pointer, so the first field write on freshly allocated storage can transition it out of pts_to_uninit; or treat a sequence of field writes covering every field as equivalent to a whole-struct assignment. The former seems more useful, since real code often initialises a subset of fields and leaves the rest for later.

[gebner]

This works for me:

R_ptr x3_fields_then_return(void)
{
    R *t = malloc(sizeof(R));
    _ghost_stmt($unfold-uninit(R) $(t));
    t->x = 0.8;
    t->y = 0.16;
    return t;
}

[akashlal]

You're right, and thank you — my report was wrong. _ghost_stmt($unfold-uninit(R) $(t)); does work, and I should have found that before filing.

For the record, here is how I got it wrong, since it may be worth a doc note. My probe did include the ghost statement, but it also wrote malloc(sizeof(*t)) rather than malloc(sizeof(R)), and that turns out to be the thing that breaks it:

typedef struct R { double x; double y; } R;
_allocated typedef R *R_ptr;

R_ptr k_type_nocast(void) {                 /* VERIFIES */
    R *t = malloc(sizeof(R));
    _ghost_stmt($unfold-uninit(R) $(t));
    t->x = 0.8; t->y = 0.16; return t;
}

R_ptr k_type_cast(void) {                   /* VERIFIES */
    R *t = (R*) malloc(sizeof(R));
    _ghost_stmt($unfold-uninit(R) $(t));
    t->x = 0.8; t->y = 0.16; return t;
}

R_ptr k_star_nocast(void) {                 /* FAILS */
    R *t = malloc(sizeof(*t));
    _ghost_stmt($unfold-uninit(R) $(t));
    t->x = 0.8; t->y = 0.16; return t;
}

R_ptr k_star_cast(void) {                   /* FAILS */
    R *t = (R*) malloc(sizeof(*t));
    _ghost_stmt($unfold-uninit(R) $(t));
    t->x = 0.8; t->y = 0.16; return t;
}

Cannot prove: pts_to_uninit (core_to_ref Struct_R.struct_r __anf0)

The cast makes no difference; sizeof(*t) vs sizeof(R) is the whole of it. Tested on 845d755.

Apologies for the noise on the original report.