zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

procedural macros #41

Closed aep closed 4 years ago

aep commented 4 years ago

fixes #40

jwerle commented 4 years ago

This is great! In the test I see that bob() is called inline as an argument to printf. That makes me assume that the function returns a char pointer, but it in fact just calls printf, with no returnable value. Does that test currently pass?

jwerle commented 4 years ago

So the idea is the stdout of a macro is used as a return value. Does the macro support inline return values?

aep commented 4 years ago

macros do not have return values. they expand to an arbitrary expression

could you give me an example of what you mean by "inline return value" ?

jwerle commented 4 years ago

@aep yes, by inline return value I meant the closet thing to pre-processor expression evaluation inline at the call site so things like

macro add(x, y) { x + y }
printf("%d\n", add(1, 2));

work as intended

aep commented 4 years ago

Yes. zz will never support a string preprocessor where the macro can expand to arbitrary text.

This leads to very confusing ASTs.

Add in your case should be a function, not a macro

However, if you have a more specific use case, maybe I can optimize the macro semantics.

jwerle commented 4 years ago

Yes, the add() example is contrived but I imagine more complex examples like loop abstractions:

macro loop() {
 while (1)
}

loop {
  // caller explicitly breaks
}

macro each(list, i) {
  for (int i = 0, item = list.items[i]; i < list.length; ++i)
}

struct List+L {
  int length;
  void *items[L];
}

fn push(List+L, void *item) -> int {
  self->items[self->length] = items
}

fn create(List+L mut new *self) {
  self->length = L;
  memset(self->items, 0 L * sizeof(self->items));
}

new+4 list = create();
each(list, i, item) {
  printf("%s\n", (char *) item);
}

After playing around with the procmacros branch I understand the intention with macros here. They are not intended to mirror the pre-processor's behavior but be like micro programs that just emit an AST to be evaluated inline with the reset of the program source.

aep commented 4 years ago

ah yes, that is intentionally not allowed, because creating arbitrary control flow items is difficult to prove and unreadable for humans.

however, you can always use the regular C prepro to prepro ZZ

aep commented 4 years ago

to clarify, you CAN create the thing you want, it just needs to be complete control structures rather than incomplete items.

so something like


macro each(list, i, block) {
  printf("for (int i = 0, item = list.items[i]; i < list.length; ++i) {");
  printf("%s", block.to_zz());
  printf("}");
}

new+4 list = create();
each(list, i, item, {
  printf("%s\n", (char *) item);
})
jwerle commented 4 years ago

@aep That is great. Is .to_zz() implemented? What's the API look like for macros now?

aep commented 4 years ago

Nope. Arguments aren't even implemented :)

I'll get to it when the kid's asleep

jwerle commented 4 years ago

sounds great, thank you! :]

aep commented 4 years ago

arguments are sort of there. there's some sugar missing, but essentially it works like this:

macro repeat(rep, times)
{
  err::assert(rep.typ == ast::Expression::LiteralString);
  err::assert(times.typ == ast::Expression::Literal);

  printf("\"");
  for (int mut i = 0; i < atoi(times.val.literal); i++) {
    printf("%s", rep.val.string);
  }
  printf("\"");
}

fn main() {
  char *xxx = repeat("x", 3);
}
jwerle commented 4 years ago

Looks great. Thanks for the docs too