Skip to content
This repository has been archived by the owner on Jun 17, 2022. It is now read-only.

Commit

Permalink
change how smt works on branches
Browse files Browse the repository at this point in the history
we dont use push/pop anymore but prepend the branch conditions to each
assignment.  this way ssa sees all assignments of all branches, and the
conditions under which these happen.
  • Loading branch information
aep committed Dec 2, 2019
1 parent f31ff40 commit 7cc4bde
Show file tree
Hide file tree
Showing 28 changed files with 658 additions and 225 deletions.
1 change: 1 addition & 0 deletions .gitignore
@@ -0,0 +1 @@
/target
10 changes: 5 additions & 5 deletions ci.sh
Expand Up @@ -11,16 +11,16 @@ cd $THIS/tests
for i in $THIS/examples/*
do
cd $i
../../target/release/zz --smt-timeout=10000 clean
../../target/release/zz --smt-timeout=10000 run
../../target/release/zz --smt-timeout=10000 test
../../target/release/zz --smt-timeout=20000 clean
../../target/release/zz --smt-timeout=20000 run
../../target/release/zz --smt-timeout=20000 test
done

for i in $THIS/modules/*
do
cd $i
../../target/release/zz --smt-timeout=10000 clean
../../target/release/zz --smt-timeout=10000 test
../../target/release/zz --smt-timeout=20000 clean
../../target/release/zz --smt-timeout=20000 test
done

echo
Expand Down
3 changes: 3 additions & 0 deletions examples/hello/.gitignore
@@ -0,0 +1,3 @@
/target
.gdb_history
vgcore.*
3 changes: 3 additions & 0 deletions examples/taint/.gitignore
@@ -0,0 +1,3 @@
/target
.gdb_history
vgcore.*
10 changes: 6 additions & 4 deletions modules/err/src/lib.zz
Expand Up @@ -31,17 +31,19 @@ export fn check(
) -> bool
model checked(*self)
{
static_attest(checked(*self));
if (self->error != 0) {
backtrace(self, file, scope, line);
static_attest(checked(*self));
return true;
}
return false;
}


fn backtrace(Err+tail mut* self, char * unsafe file, char * unsafe scope, usize line) {
fn backtrace(Err+tail mut* self, char * unsafe file, char * unsafe scope, usize line)
{
if tail > 0 {
static_attest((self->locations).len < tail);
string::format(&(self->locations), "\n %s:%zu \t%s", file, line, scope);
}
}
Expand Down Expand Up @@ -100,15 +102,15 @@ export fn abort(
char* callsite_source<function> unsafe scope,
usize callsite_source<line> line,
)

model checked(*err)
{
static_attest(checked(*err));
if (err->error != 0) {
static_attest(checked(*err));
backtrace(err, file, scope, line);
fprintf(stderr, "fatal error %u: %s%s\n", err->error, err->description, (err->locations).mem);
cabort();
}
static_attest(checked(*err));
}

export fn eprint(Err+tail mut* err)
Expand Down
111 changes: 91 additions & 20 deletions modules/io/src/lib.zz
Expand Up @@ -23,10 +23,10 @@ export enum Result {
Eof,
}

export fntype read_fn (Context ctx, err::Err+et mut* e, u8 mut* to, usize mut* len) -> Result;
export fntype write_fn (Context ctx, err::Err+et mut* e, u8 mut* to, usize mut* len) -> Result;
export fntype wake_fn (Context ctx, err::Err+et mut* e, Wake w);
export fntype close_fn (Context ctx);
export fntype read_fn (Context mut* ctx, err::Err+et mut* e, u8 mut* to, usize mut* len) -> Result;
export fntype write_fn (Context mut* ctx, err::Err+et mut* e, u8* to, usize mut* len) -> Result;
export fntype wake_fn (Context mut* ctx, err::Err+et mut* e, Wake w);
export fntype close_fn (Context mut* ctx);


export struct Context {
Expand All @@ -48,24 +48,95 @@ export struct Io {
export fn read(Io mut* self, err::Err+et mut* e, string::String+st mut* str) -> Result
where st > 1
where err::checked(*e)
where str->len < st
{
if self->read_impl != 0 {
static_attest(safe(self->read_impl));

usize mut l = st - str->len - 1;
Result rr = self->read_impl(self->ctx, e, as<u8 mut*>(str->mem + str->len), &l);
err::check(e);
if rr != Result::Ready {
return rr;
}
str->len += l;
static_attest(len(str->mem) > str->len);
(str->mem)[str->len] = 0;
if self->read_impl == 0 {
err::fail(e, 1, "noimpl");
return Result::Error;
}
static_attest(safe(self->read_impl));

usize mut l = st - str->len - 1;
Result rr = self->read_impl(&self->ctx, e, as<u8 mut*>(str->mem + str->len), &l);
err::check(e);
if rr != Result::Ready {
return rr;
} else {
}
str->len += l;
static_attest(len(str->mem) > str->len);
(str->mem)[str->len] = 0;
return rr;
}

export fn readline(Io mut* self, err::Err+et mut* e, string::String+st mut* str) -> Result
where st > 1
where err::checked(*e)
where str->len < st
where st > 2
{
if self->read_impl == 0 {
err::fail(e, 1, "noimpl");
return Result::Error;
}
static_attest(safe(self->read_impl));

u8 mut buf[2] = {0};
usize mut l = 1;
Result rr = self->read_impl(&self->ctx, e, buf, &l);
err::check(e);
if rr != Result::Ready {
return rr;
}

char ch = as<char>(buf[0]);

if ch == '\n' || ch == '\r' {
return Result::Ready;
}

if !str->push(ch) {
err::fail(e, 1, "oom");
return Result::Error;
}

return Result::Later;
}

export fn write(Io mut* self, err::Err+et mut* e, string::String+st mut* str) -> Result
where st > 1
where err::checked(*e)
where str->len < len(str->mem)
{
if self->write_impl == 0 {
err::fail(e, 1, "noimpl");
return Result::Error;
}
static_attest(safe(self->write_impl));

usize mut l = str->len;
Result rr = self->write_impl(&self->ctx, e, as<u8 mut*>(str->mem + str->len), &l);
err::check(e);
if rr != Result::Ready {
return rr;
}
return rr;
}

export fn write_bytes(Io mut* self, err::Err+et mut* e, u8 *b, usize mut *blen) -> Result
where err::checked(*e)
{
if self->write_impl == 0 {
err::fail(e, 1, "noimpl");
return Result::Error;
}
static_attest(safe(self->write_impl));

Result rr = self->write_impl(&self->ctx, e, b, blen);
err::check(e);
if rr != Result::Ready {
return rr;
}
return rr;
}

export fn close(Io mut* self)
Expand All @@ -74,17 +145,17 @@ export fn close(Io mut* self)
return;
}
static_attest(safe(self->close_impl));
self->close_impl(self->ctx);
self->close_impl(&self->ctx);
}

export fn wake(Io *self, err::Err+et mut* e, Wake w)
export fn wake(Io mut*self, err::Err+et mut* e, Wake w)
where err::checked(*e)
{
if self->wake_impl == 0 {
return;
}
static_attest(safe(self->wake_impl));
self->wake_impl(self->ctx,e,w);
self->wake_impl(&self->ctx,e,w);
}

pub fn drop(Io mut* self) {
Expand Down
24 changes: 11 additions & 13 deletions modules/io/src/main.zz
Expand Up @@ -8,20 +8,22 @@ using <stdio.h>::{perror, printf};


export fn main() -> int {
err::Err+1000 mut e ={0};
err::check(&e);
err::Err+1000 mut e;
err::new(&e);

unix::Async+10 mut async;
unix::new(&async);

io::Io mut i = unix::stdin();
unix::make_async(&i, (io::Async mut*)&async);
unix::make_read_async(&i, (io::Async mut*)&async);

io::Io mut t = io::timeout((io::Async mut*)&async, &e, time::from_seconds(3));
err::abort(&e);

for (;;) {
string::String+20 mut buf2 = {0};
string::String+20 mut buf2;
string::clear(&buf2);

switch t.read(&e, &buf2) {
io::Result::Ready => {
err::abort(&e);
Expand All @@ -39,7 +41,8 @@ export fn main() -> int {
}
err::abort(&e);

string::String+2 mut buf = {0};
string::String+2 mut buf;
string::clear(&buf);
switch i.read(&e, &buf) {
io::Result::Ready => {
printf(">%s<\n", buf.mem);
Expand All @@ -50,16 +53,11 @@ export fn main() -> int {
return 0;
}
}
err::abort(&e);


switch async.wait() {
unix::Result::Ready => {
}
unix::Result::Error => {
perror("poll error");
return 1;
}
}
async.wait(&e);
err::abort(&e);
}
return 0;
}
Expand Down

0 comments on commit 7cc4bde

Please sign in to comment.