zetzit / zz

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

Q: how to deref C struct? #57

Closed bnoordhuis closed 4 years ago

bnoordhuis commented 4 years ago

At commit ec50a85. Test case:

using <stdio.h>::{printf};
using <dirent.h>::{DIR, (struct dirent) as dirent, opendir, readdir, closedir};

export fn main() -> int {
    DIR mut *d = opendir(".");
    for (;;) {
        dirent *e = readdir(d);
        if (e == 0) {
            break;
        }
        static_attest(safe(e));
        static_attest(safe(*e));
        printf("%d\n", e->ino);
    }
    closedir(d);
    return 0;
}

Fails to build with the following error message:

$ zz
comp [ t::main ]  0 / 1 [---------------------------------------------------------------------------------------------------------------------------------------------] 0.00 %  [ERROR] deref(S20_e) is not accessible as struct. it is ::ext::<dirent.h>::struct dirent
  --> /home/bnoordhuis/src/t/src/main.zz:13:25
   |
13 |         printf("%d\n", e->ino);␊
   |                         ^^
   |
   = cannot use as struct here

  --> /home/bnoordhuis/src/t/src/main.zz:13:16
   |
13 |         printf("%d\n", e->ino);␊
   |                ^-------------^
   |
   = last callsite

comp [ ]  1 / 1 [===================================================================================================================================================] 100.00 %  thread 'main' panicked at 'ICE: dependency ::t::main module doesnt exist', src/pipeline.rs:215:25
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I'm wondering how to make that work. Grepping through zz's source tree, it might simply not be supported yet?

aep commented 4 years ago

Hi,

you cannot use C types as structs, because that's unsafe (related to #22) i think the error message needs improvement here, it should have told you that it's an unknown C type.

it should compile inside an unsafe {} block, but it currently doesn't. as a workaround you can use a C block with

@{{
   c code here
}}@

but that will be removed once unsafe works correctly

bnoordhuis commented 4 years ago

Thanks, I was indeed able to make it work through a C block. For future reference:

``` using ::{DIR, (struct dirent) as dirent, opendir, readdir, closedir}; export fn main() -> int { @{{ #include #include }}@ DIR mut *d = opendir("."); for (;;) { dirent *e = readdir(d); if (e == 0) { break; } static_attest(safe(e)); @{{ printf("%ld\n", e->d_ino); }}@ } closedir(d); return 0; } ```

And more elegantly by copying it to a zz struct:

``` using ::{printf}; using ::{DIR, (struct dirent) as dirent, opendir, readdir, closedir}; struct Dirent { char d_name[256]; u64 d_ino; } fn convert(dirent *t) -> Dirent { Dirent mut e; @{{ #include }}@ @{{ #include }}@ @{{ snprintf(e.d_name, sizeof(e.d_name), "%s", t->d_name); }}@ @{{ e.d_ino = t->d_ino; }}@ return e; } export fn main() -> int { DIR mut *d = opendir("."); for (;;) { dirent *t = readdir(d); if (t == 0) { break; } static_attest(safe(t)); Dirent e = convert(t); printf("%ld %s\n", e.d_ino, e.d_name); } closedir(d); return 0; } ```
aep commented 4 years ago

actually turns out unsafe block works just as expected.

i made the error message more useful

aep commented 4 years ago

note that this has become alot more convenient with unsafe expressions

        printf("%d\n", unsafe<int>(e->ino));