zetzit / zz

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

cast of function pointer should not be allowed #139

Open mb64 opened 3 years ago

mb64 commented 3 years ago

It would be helpful to know how much typechecking is done by ZZ. I was under the impression it did full typechecking, so I was surprised to find that the following program transpiled to C without error:

using <stdio.h>::{printf};

fn output(int *x) {
    printf("%d\n", *x);
}

fn function() {}

export fn main() -> int {
    output(function);
}

Of course, clang halted compilation with an error. Either way, it would help to clarify in the documentation about typechecking.

aep commented 3 years ago

so there's multiple answers to this.

First of all zetz doesn't have a type checker. Let me know what wording sounded like it does, so we can fix that.

On the issue of this being an invalid cast. Zetz is a prove assistant for C. You can cast anything into anything as long as you don't violate any smt models. Since there aren't any, this passes.

However, zetz is supposed to catch UB by default, and this is UB, so this is still a bug. The issue is a) that printf is completely unconstrained until someone writes a model for it, but also b) a function pointer is unconstrained for backwards compat with union casts, which i havent figured out yet..