Model va_arg by giving the callee the arguments it was passed

[shaobo-he]

va_arg reads unconstrained memory today, so a program whose result depends on a variadic argument cannot be verified. This models it precisely, behind --lower-varargs.

The problem

Clang lowers va_arg inline, walking the target's va_list — { i32 gp_offset; i32 fp_offset; i8* overflow_arg_area; i8* reg_save_area; } — but llvm.va_start reaches Boogie as a bodyless declaration:

/* SMACK warning: approximating llvm.va_start (can lead to both
   false alarms and missed detections); */
call llvm.va_start($p3);
$i6 := $load.i32($M.0, $p5);     // gp_offset, never written
$i7 := $ule.i32($i6, 40);        // register path or overflow path?

The list is never initialized, so every va_arg reads an unconstrained value. On develop, __VERIFIER_assert(first(1, 42) == 42) is reported as an error, and sum(3,10,20,30) == 60 "verifies" only at --unroll=1, vacuously — at --unroll=5 it errors.

The SV-COMP frontend takes a different route: #define __builtin_va_arg(ap, t) __builtinx_va_arg(ap), whose body is return 0;. That direction misses bugs instead of inventing them.

Neither path is pinned by a test. test/c/basic/vararg{,_fail}.c assert only on the named parameter, so both pass whatever va_arg returns; one of them even reads a variadic argument that was never passed.

The approach

The groundwork was already there: SMACK monomorphizes variadic callees per call-site signature, so the callee already receives the value — procedure first.i32.i32($i0: i32, p.1: i32), called as first.i32.i32(1, 42). The body just ignores p.1 and does the ABI dance instead.

The new pass connects them. For each direct call to a defined variadic function it clones the callee with the variadic arguments as ordinary parameters, and in the clone replaces llvm.va_start with code that lays those arguments out where the lowering will look for them: one eight-byte slot per argument, overflow_arg_area pointing at the buffer, and both register-save offsets exhausted (gp_offset = 48, fp_offset = 304) so the lowering takes the overflow path whatever the argument's type. Clang's own va_arg code then reads the real values.

Nothing has to recognize the shape of that lowering, which is the point: the fix is four stores at va_start, and every corner of clang's code — the register/overflow branch, the +8 walk, va_copy — keeps working as written.

Putting the values in memory rather than in the clone's parameters is what makes a va_list handed to another function work, as vfprintf does. The obvious alternative — resolve va_arg to the k-th parameter with an if-chain — cannot do that, because the callee cannot evaluate its caller's parameters.

Results

Corral, all three memory models:

test	expects	off	on
the value read is the value passed	verified	error	verified
va_arg in a loop over three arguments	verified	error	verified
argument order	verified	error	verified
a va_list forwarded to another function	verified	error	verified
a nondeterministic value travels	verified	error	verified
a pointer argument, dereferenced	verified	error	verified
a double argument	verified	error	verified
the six _fail twins of the above	error	error	error
existing basic/vararg{,_fail}.c	as before	unchanged	unchanged

Verification

• New folder test/c/varargs, exhaustive (three memory models × Boogie + Corral): 60 passed, 0 failed. Six of the ten are the failing twin of another, so nothing here passes by doing nothing. Added to the CI matrix.
• Flag off is byte-identical to develop: 674 translations over basic, memory-safety, data, strings, bits and float × two memory models, 0 different. The pass is only added to the pipeline when the option is given.
• The rest of the suite has not been run locally; CI covers it.

Limits

Both are refusals that leave the call exactly as it is today, never a wrong answer:

• A variadic list mixing floating-point with integer or pointer arguments. One buffer holding both makes sea-DSA collapse its region, and a float access to a region that is not typed float goes through SMACK's deliberately approximate $store.unsafe.* path, so the value does not come back out. Separating those arguments needs storage the ABI lowering would still have to walk contiguously.
• Arguments passed by value whose ABI classification this pass does not reproduce — structs and arrays.

The slot layout is the x86-64 overflow area, which is the layout SMACK's pinned target uses; a target guard belongs here before this is more than opt-in.

Out of scope, and unchanged: #55 (function pointers to variadic functions) and #252 (invoke to a variadic function) — the pass specializes direct calls only. If this lands, __builtinx_va_arg could be deleted rather than kept as a second, differently-wrong model.

🤖 Generated with Claude Code