Repository navigation
[CN-Exec] Struct initializer issues #925
Description
Macros get confused with commas in struct initializers, which can be fixed with CN_IGNORE_COMMA, but it just fails then.
This limits user's abilities to reproduce failing inputs when testing.
List reverse example
struct int_list {
int head;
struct int_list *tail;
};
/*@
datatype seq {
Seq_Nil {},
Seq_Cons {i32 head, datatype seq tail}
}
predicate (datatype seq) IntList(pointer p) {
if (is_null(p)) {
return Seq_Nil{};
} else {
take H = Owned<struct int_list>(p);
take tl = IntList(H.tail);
return (Seq_Cons { head: H.head, tail: tl });
}
}
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
match xs {
Seq_Nil {} => {
ys
}
Seq_Cons {head : h, tail : zs} => {
Seq_Cons {head: h, tail: append(zs, ys)}
}
}
}
function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
match xs {
Seq_Nil {} => {
Seq_Cons {head: y, tail: Seq_Nil{}}
}
Seq_Cons {head: x, tail: zs} => {
Seq_Cons{head: x, tail: snoc (zs, y)}
}
}
}
function [rec] (datatype seq) rev(datatype seq xs) {
match xs {
Seq_Nil {} => {
Seq_Nil {}
}
Seq_Cons {head : h, tail : zs} => {
snoc (rev(zs), h)
}
}
}
@*/
struct int_list *IntList_rev_aux(struct int_list *xs, struct int_list *ys)
/*@ requires take L1 = IntList(xs); @*/
/*@ requires take L2 = IntList(ys); @*/
/*@ ensures take R = IntList(return); @*/
/*@ ensures R == append(rev(L2), L1); @*/
{
if (ys == 0) {
return xs;
} else {
struct int_list *tmp = ys->tail;
ys->head = -1;
ys->tail = xs;
return IntList_rev_aux(ys, tmp);
}
}
struct int_list *IntList_rev(struct int_list *xs)
/*@ requires take L1 = IntList(xs); @*/
/*@ ensures take L1_rev = IntList(return); @*/
/*@ ensures L1_rev == rev(L1); @*/
{
return IntList_rev_aux(0, xs);
}
void *cn_malloc(unsigned long);
int main() {
struct int_list *ys = cn_malloc(sizeof(struct int_list));
*ys = (struct int_list){.head = 10, .tail = 0};
struct int_list *xs = cn_malloc(sizeof(struct int_list));
*xs = (struct int_list){.head = 7, .tail = ys};
IntList_rev(xs);
return 0;
}
Activity
ZippeyKeys12 commentedon Mar 10, 2025
@rbanerjee20
[-][CN-Exec] Struct initializer fails to compile[/-][+][CN-Exec] Struct initializer issues[/+]ZippeyKeys12 commentedon Mar 10, 2025
It might be because of spurious
CN_LOADs on struct initializersrbanerjee20 commentedon Apr 4, 2025
Hi @ZippeyKeys12, I've had a further look into this. I fixed the syntactic problem by adding an extra pair of parentheses around the struct initialiser, but then as you said, it fails anyway at runtime. The
CN_LOADisn't actually spurious - it gets added wherever there is anAilErvaluein the source (see here), which wraps around Ail expressions including compound literals like this. It's failing at runtime because the address of the struct initialiser hasn't been mapped into the ownership ghost state beforeCN_LOADis called, which performs a check and loads. This will require some further discussion (which we've already started doing) and a better understanding of how to handle compound literals more generally before I can implement a true fix.In the meantime, it's a bit more verbose, but if you could initialise without using a compound literal but by struct member one-by-one, that should work.
ZippeyKeys12 commentedon Apr 4, 2025
The code in question is synthesized at runtime, so this would require a rewrite of that system. There might be other benefits to a rewrite, so I'll see.
If it's going to take a while to fix, you should put this information in a warning for when the instrumented code uses struct initializers.
ZippeyKeys12 commentedon Nov 21, 2025
@rbanerjee20 are these fixed now?