zetzit / zz

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

Trying to run any example gives me "expected file" error #150

Closed GoldsteinE closed 3 years ago

GoldsteinE commented 3 years ago
$ zz --version                                                                                                                1
Drunk Octopus 0.1.0
$ cat zz.toml
[project]
version = "0.1"
name = "1"

[dependencies]
$ cat src/main.zz
using <stdio.h>::{printf};

pub theory isopen(Socket*s) -> bool;

struct Socket {
    int mut fd;
}

fn open(Socket mut* self)
    model isopen(*self)
{
    static_attest(isopen(*self) == true);
    static_assert(isopen(*self) == true);
    self->fd = 2;
}

fn read(Socket mut* self)
    where isopen(*self)
    model isopen(*self)
{
    int bla = self->fd;
}

fn close(Socket mut* self)
    where isopen(*self)
    model !isopen(*self)
{
    //convince the symbolic executor that we did something, so we can have new constraints
    *self = Socket{fd: 0};
    static_attest(isopen(*self) == false);
}

export fn main() -> int {

    Socket mut sock = {0};
    open(&sock);
    read(&sock);
    close(&sock);

    printf("hello taint\n");
    return 0;
}
$ zz run
[ERROR zz::parser] "./src/main.zz" :  --> 1:1
  |
1 | using <stdio.h>::{printf};␊
  | ^---
  |
  = expected file
jwerle commented 3 years ago

@GoldsteinE can you also share what uname -a outputs?

aep commented 3 years ago

something happened to your line endings. the pest.rs parser is not very good at reporting a failure to parseline endings and instead just refuses to parse anything at all, resulting in the not so helpful error message

i can see here

1 | using <stdio.h>::{printf};␊

that there's some unprintable character at the end.

GoldsteinE commented 3 years ago
$ uname -a
Linux lptp 5.10.4-arch2-1 #1 SMP PREEMPT Fri, 01 Jan 2021 05:29:53 +0000 x86_64 GNU/Linux

https://gist.github.com/GoldsteinE/2581c1442abc837060f5a2ddc72387cc hexdump'd file β€” no unprintable characters except for newline (0a) itself.

Also tried to just download https://raw.githubusercontent.com/zetzit/zz/master/examples/taint/src/main.zz β€” same error.

aep commented 3 years ago

huh wow thats strange. which zz binary did you use? it might just be a bit old. i just realized http://bin.zetz.it/ has terrible sorting, so the latest one is in the middle

GoldsteinE commented 3 years ago

cargo install zz and the top binary from bin.zetz.it. Will try to find latest prebuilt release

GoldsteinE commented 3 years ago

Where to install modules/?

GoldsteinE commented 3 years ago

Latest version gives me a lot of errors for the same input https://gist.github.com/GoldsteinE/26f7f975418dbd7c44b295d44e6db820

aep commented 3 years ago

thanks, i had totally forgotten about crates.io. i tried yanking it, but doesnt look like it'll let me completely remove it unfortunately.

modules can be relative to the executable. just unzipping it should work.

let me try to reproduce this by downloading the binary myself.

aep commented 3 years ago

hmm cannot reproduce

$ wget http://bin.zetz.it.s3-eu-west-1.amazonaws.com/zz-183-71f43e968b22a799247aab9ddb12dc4a52910888-ubuntu.zip
$ unzip *.zip
$ mkdir foo
$ cd foo
$ wget https://raw.githubusercontent.com/zetzit/zz/master/examples/taint/src/main.zz 
$ ../target/release/zz run
finished [Exe] j                                                                                                                                           
running "/tmp/j/target/test/bin/j"

[INF] j::main hello j

did you set CC environment variable to anything? if not whats your clang or gcc version?

GoldsteinE commented 3 years ago
$ wget http://bin.zetz.it.s3-eu-west-1.amazonaws.com/zz-183-71f43e968b22a799247aab9ddb12dc4a52910888-ubuntu.zip
$ unzip *.zip
$ mkdir foo
$ cd foo
$ mkdir src
$ cd src
$ wget https://raw.githubusercontent.com/zetzit/zz/master/examples/taint/src/main.zz 
$ cd ..
$ cat > zz.toml
[project]
version = "0.1"
name = "1"

[dependencies]
$ zz run
<output linked above>
$ clang --version
clang version 11.0.0
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin
$ gcc --version
gcc (GCC) 10.2.0
Copyright (C) 2020 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
$ echo "$CC"
aep commented 3 years ago

ah yes,

the issue is you created the zz.toml manually with "1" as name, and that really messes up things because that's used as prefix for all C names. i would recommend you just use zz init.

we should probably catch that tho :)

GoldsteinE commented 3 years ago

Oh. zz init didn't work for me because of old version, so I created zz.toml manually. Thanks!

aep commented 3 years ago

thanks for the report. open a new issue any time you need assistance or drop by at discord.