[CN-Exec] Struct initializer issues

[ZippeyKeys12]

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

[ZippeyKeys12]

@rbanerjee20

[ZippeyKeys12]

It might be because of spurious CN_LOADs on struct initializers

[rbanerjee20]

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_LOAD isn't actually spurious - it gets added wherever there is an AilErvalue in 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 before CN_LOAD is 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]

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.

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]

@rbanerjee20 are these fixed now?