nrc / libhoare

Design by contract style assertions for Rust

LibHoare

Simple Rust support for design by contract-style assertions. Supports

• preconditions (precond),
• postconditions (postcond),
• invariants (pre and post) (invariant).

Each macro takes a predicate given as a string parameter. Each macro is available in a debug_ version which only checks the assertion in debug builds, they should be zero overhead in non-debug builds. You can use result inside a postcondition to get the value returned by the function.

Preconditions are checked on entry to a function. Postconditions are checked when leaving the function by any path.

(The library is named for Tony, not Graydon. Or rather it is named for the logic which was named after Tony).

Using libhoare

You can use libhoare with Cargo by adding

[dependencies.hoare]
git = "https://github.com/nick29581/libhoare.git"

to your projects Cargo manifest.

Otherwise, download this repo, build it (see build instructions below), make sure the path to the compiled libhoare is on your library path in some way (one way of doing this is to export LD_LIBRARY_PATH=/path/to/libhoare/obj before building).

Then (whether or not you used Cargo), in your crate you will need the following boilerplate:

#![feature(plugin, custom_attribute)]

#![plugin(hoare)]

Then you can use the macros as shown below.

Examples:

#[precond="x > 0"]
#[postcond="result > 1"]
fn foo(x: int) -> int {
    let y = 45 / x;
    y + 1
}


struct Bar {
    f1: int,
    f2: int
}

#[invariant="x.f1 < x.f2"]
fn baz(x: &mut Bar) {
    x.f1 += 10;
    x.f2 += 10;
}

fn main() {
    foo(12);
    foo(26);
    // task '<main>' failed at 'precondition of foo (x > 0)'
    // foo(-3);

    let mut b = Bar { f1: 0, f2: 10 };
    baz(&mut b);
    b.f2 = 100;
    baz(&mut b);
    b.f2 = -5;
    // task '<main>' failed at 'invariant entering baz (x.f1 < x.f2)'
    // baz(&mut b);
}

You can use contracts on methods as well as functions, but they are not as well tested.

Contents

All the code for checking conditions is in libhoare. Currently, there is only a single file, lib.rs.

The test directory contains unit tests for the library.

The eg directory contains a few examples of how to use the library:

• hello.rs is a very simple (hello world!) example of how to use an invariant (useful as a basic test case);
• doc.rs contains the examples above, so we can check they compiler and run;
• lexer.rs is a more realistic example of use - a simple (and certainly not industrial-strength) lexer for a very small language.

Building

To build libhoare from the top level of your checked out repo run

cargo build

(if using cargo) or

$RUSTC ./libhoare/lib.rs

This will create libhoare.rs in the current directory, you might want to specify an output file using -o.

To build the examples run eg.sh in the top level and to run the tests run tests.sh. Both of these assume that you have a sibling directory called obj and that you used

$RUSTC ./libhoare/lib.rs -o "../obj/libhoare.so"

to build libhoare. Examples are created in ../obj

TODO

• add tests to RustCI
• tests for debug_ versions of macros - what is the best way to test this?
• better use of macro stuff? (I'm a total beginner at syntax extensions, this all could probably be implemented better).
• better spans.
• better names for scopes (<precondition> rather than <quote expansion>, etc. These appear in the user-visible error messages, so it would be nice if they could be informative).

Wish list:

• object invariants (I think this would need compiler support, if it is possible at all. You would add [#invariant="..."] to a struct, enum, etc. and the invariant would be checked on entering and leaving every method defined in any impl for the object).

libhoare's Issues

Lift restrictions on patterns

You can lift the restrictions on what patterns can be used in function arguments by creating a closure instead of an inner function. See my trace project for an example.

This is a test issue, please ignore it

Issue by nick29581
Wednesday Sep 24, 2014 at 04:46 GMT

For earlier discussion, see rust-lang/rust#17499

This issue was labelled with: A-debuginfo, A-dst, A-iOS in the Rust repository

---

body of the issue

Compile error? attribute `phase` is currently unknown

I can get libhoare crate to compile successfully now, but when I try and use it in my application I'm getting the following error:

   Compiling test v0.1.0 (file:///home/user/test)
src/lib.rs:5:1: 5:17 src/lib.rs:5:1: 5:17 error: The attribute `phase` is currently unknown to the compiler and may have meaning added to it in the future
error: src/lib.rs:5 #[phase(plugin)]
             ^~~~~~~~~~~~~~~~
src/lib.rs:5:1: 5:17 The attribute `phase` is currently unknown to the compiler and may have meaning added to it in the future
src/lib.rs:5 #[phase(plugin)]
             ^~~~~~~~~~~~~~~~

Below is what I put in my src/lib.rs

#![feature(phase)]
#[phase(plugin)]
extern crate hoare;

might be worth checking out how SPARK 2014 does contracts

http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#subprogram-contracts

Allow custom error messages

Just like assertions. Not sure what the syntax should look like.

Refer to precondition state from the postcondition

Example (from Reddit user thiez):

#[postcond = "self.x=\old(self.x)+1"]
fn inc(&mut self) {
    self.x += 1;
}

The /old function in this example allows us to speak about the old state of self.x.

Need to figure out the best syntax for this, perhaps allowing some variables to be introduced and filled with the old values. This probably needs to be opt-in since there will be a cost of the copy.

Compile error? 5 fields vs. 6 fields?

I'm getting the following error message when installing and using libhoare. I'm new to Rust, so It's entirely possible that I've installed it wrong or am using it incorrectly on my end. Any suggestions? And thank you by the way for writing libhoare.

I'm using the following toolset:
cargo 0.4.0-nightly (4e5fdcd 2015-06-29) (built 2015-06-29)
rustc 1.3.0-nightly (faa04a8b9 2015-06-30)

    Updating git repository `https://github.com/nick29581/libhoare.git`
   Compiling hoare v0.1.1 (https://github.com/nick29581/libhoare.git#1623c8ce)
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:48:10: 48:60 error: this pattern has 5 fields, but the corresponding variant has 6 fields [E0023]
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:48         &ast::ItemFn(ref decl, style, abi, ref generics, _) => {
                                                                                             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:48:10: 48:60 help: run `rustc --explain E0023` to see a detailed explanation
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:77:28: 77:89 error: this function takes 6 parameters but 5 parameters were supplied [E0061]
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:77             P(Item { node: ast::ItemFn(decl.clone(), style, abi, generics.clone(), body),
                                                                                                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/home/user/.cargo/git/checkouts/libhoare-548492d426bd31de/master/libhoare/lib.rs:77:28: 77:89 help: run `rustc --explain E0061` to see a detailed explanation

Similar errors repeat multiple times, but I've just included the first one.

Tests for contracts on methods

Weed out dummy spans

I used these a few times out of laziness, should use the attr's span, just requires threading it through a few function calls and the ReturnFolder struct.

Current development

This crate is awesome by it's idea/implemetation. Why isn't it developed anymore?

Make `cargo test` work and add tests to CI

Allow on impl methods

This syntax extension can be used on impl methods by registering it as a MultiModifier instead of a Modifier.

Compilation errors

When I try to build my project with libhoare I'll get many compilation errors. I added the dependency to my Cargo.toml like this:
[dependencies.hoare] git = "https://github.com/nick29581/libhoare.git"

As a result I got 13 erros like this: error[E0425]: cannot find function intern in module token --> C:\Users\user1\.cargo\git\checkouts\libhoare-e8ae5b947a6d22d6\108e29a\libhoare/lib.rs:42:42 | 42 | reg.register_syntax_extension(token::intern("precond"), |
Am I doing something wrong? Thanks in advance.

Use `return` instead of `result`

This would avoid shadowing any arguments called result. Would require mangling the name return in the predicate before injecting it into an assertion. Should also check that it is only used in postconditions.

This is a test issue, please ignore it

Issue by nick29581
Wednesday Sep 24, 2014 at 04:46 GMT

For earlier discussion, see rust-lang/rust#17499

This issue was labelled with: A-debuginfo, A-dst, A-iOS in the Rust repository

---

body of the issue

Debug version of contracts not working.

The "debug_precond", "debug_postcond", and "debug_invariant" contracts are still present when compiled in release mode.

Seems to be related to line 288 in lib.rs.

|item| item.node == ast::MetaWord(token::get_name(token::intern("ndebug")))) {

The ndebug flag has been replaced with "debug_assertions" from what I could find online. I replaced the ndebug string with debug_assertions in that line, but it still doesn't seem to work and I'm not sure how to fix the other portions of that section of code.

libnative does not handle fds with O_NONBLOCK

Issue by kballard
Saturday Apr 05, 2014 at 07:13 GMT
Originally opened as rust-lang/rust#13336

---

libnative does not detect when a read/write fails due to O_NONBLOCK being set on the fd. It makes the assumption that all of its files never have that flag set, because it never sets that flag on them. Unfortunately, this isn't necessarily the case. FIFOs and character device files (e.g. terminals) will actually share the O_NONBLOCK flag among all processes that have the same open file description (e.g. the underlying kernel object that backs the fd).

Using a tiny C program that uses fcntl() to set O_NONBLOCK on its stdout, a FIFO, and a Rust program that writes 32k of output to stdout, I can reproduce this issue 100% of the time. The invocation looks like

> (./mknblock; ./rust_program) > fifo

and on the reading side I just do

> (sleep 1; cat) < fifo

This causes the rust program to return a "Resource temporarily unavailable" error from stdout.write() after writing 8k of output. Removing the call to ./mknblock restores the expected behavior where the rust program will block until the reading side has started consuming input. And further, switching the rust program over to libgreen also causes it to block even with ./mknblock.

---

The C program looks like this:

#include <fcntl.h>
#include <stdio.h>

int main() {
    if (fcntl(1, F_SETFL, O_NONBLOCK) == -1) {
        perror("fcntl");
        return 1;
    }
    return 0;
}

The Rust program is a bit longer, mostly because it prints out information about stdout before it begins writing. It looks like this:

extern crate green;
extern crate rustuv;

use std::io;
use std::io::IoResult;
use std::libc;
use std::os;
use std::mem;

static O_NONBLOCK: libc::c_int = 0x0004;
static O_APPEND: libc::c_int = 0x0008;
static O_ASYNC: libc::c_int = 0x0040;

static F_GETFL: libc::c_int = 3;

unsafe fn print_flags(fd: libc::c_int) -> IoResult<()> {
    let mut stat: libc::stat = mem::uninit();
    if libc::fstat(fd, &mut stat) < 0 {
        try!(writeln!(&mut io::stderr(), "fstat: {}", os::last_os_error()));
        libc::exit(1);
    }

    try!(writeln!(&mut io::stderr(), "stdout: dev={}, ino={}", stat.st_dev, stat.st_ino));

    let flags = libc::fcntl(fd, F_GETFL);
    if flags == -1 {
        try!(writeln!(&mut io::stderr(), "fcntl: {}", os::last_os_error()));
        libc::exit(1);
    }

    let mut v = Vec::new();
    if flags & O_NONBLOCK != 0 {
        v.push("nonblock");
    }
    if flags & O_APPEND != 0 {
        v.push("append");
    }
    if flags & O_ASYNC != 0 {
        v.push("async");
    }

    try!(writeln!(&mut io::stderr(), "flags: {}", v.connect(", ")));
    Ok(())
}

fn run() -> IoResult<()> {
    unsafe { try!(print_flags(1)); }

    let mut out = io::stdio::stdout_raw();
    for i in range(0u, 32) {
        try!(writeln!(&mut io::stderr(), "Writing chunk {}...", i));
        let mut buf = ['x' as u8, ..1024];
        buf[1023] = '\n' as u8;
        match out.write(buf) {
            Ok(()) => (),
            Err(e) => {
                try!(writeln!(&mut io::stderr(), "Error writing chunk {}", i));
                return Err(e);
            }
        }
    }
    Ok(())
}

fn main() {
    match run() {
        Err(e) => {
            (writeln!(&mut io::stderr(), "Error: {}", e)).unwrap();
            os::set_exit_status(1);
        }
        Ok(()) => ()
    }
}

unsafe fn arg_is_dash_g(arg: *u8) -> bool {
    *arg == '-' as u8 &&
        *arg.offset(1) == 'g' as u8 &&
        *arg.offset(2) == 0
}

#[start]
fn start(argc: int, argv: **u8) -> int {
    if argc > 1 && unsafe { arg_is_dash_g(*argv.offset(1)) } {
        green::start(argc, argv, rustuv::event_loop, main)
    } else {
        native::start(argc, argv, main)
    }
}

Better error messages

Would be good to print values of all variables in the predicate which implement Show. Maybe also narrowing down which clause of the predicate failed (assuming it is a bunch of clauses &&-ed together, which I guess will be a common pattern).