Skip to content

Commit

Permalink
Update to latest Rust
Browse files Browse the repository at this point in the history
  • Loading branch information
Jakub Bukaj committed Mar 2, 2015
1 parent a6db1e8 commit f378c25
Show file tree
Hide file tree
Showing 15 changed files with 88 additions and 119 deletions.
3 changes: 0 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
[package]

name = "hoare"
version = "0.1.1"
authors = [ "nrc@ncameron.org" ]
Expand All @@ -8,8 +7,6 @@ repository = "https://github.com/nick29581/libhoare"
readme = "readme.md"

[lib]

name = "hoare"
crate_type = ["dylib"]
path = "libhoare/lib.rs"
plugin = true
7 changes: 0 additions & 7 deletions eg.sh

This file was deleted.

13 changes: 6 additions & 7 deletions eg/doc.rs → examples/doc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,24 +8,23 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.

#![feature(phase)]
#![feature(plugin)]

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

// Examples from readme.md

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


struct Bar {
f1: int,
f2: int
f1: i64,
f2: i64
}

#[invariant="x.f1 < x.f2"]
Expand Down
13 changes: 6 additions & 7 deletions eg/hello.rs → examples/hello.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,18 +8,17 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.

#![feature(phase)]
#![feature(plugin)]

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

#[precond="x != 0"]
fn foo(x: int) {
println!("hello world! {}", x);
fn foo(x: i64) {
println!("hello world! {}", x);
}

#[debug_invariant="*x > 60"]
fn bar<X: std::fmt::Show>(x: &mut int, y: X) -> int {
fn bar<X: std::fmt::Display>(x: &mut i64, y: X) -> i64 {
println!("hello world! {} {}", x, y);
*x += 20;
35
Expand All @@ -31,5 +30,5 @@ fn main() {

// A slightly more interesting test case.
let mut x = 65;
bar::<int>(&mut x, 10);
bar::<i64>(&mut x, 10);
}
43 changes: 21 additions & 22 deletions eg/lexer.rs → examples/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,22 +23,21 @@
// inside the quotes and the quotes themselves are a single token (including
// symbols and whitespace).

#![feature(phase)]
#![feature(plugin)]

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

use std::collections::hashmap::HashSet;
use std::collections::HashSet;

// Symbols with special meaning
static COMMA: &'static str = ",";
static OR: &'static str = "|";
static COLON: &'static str = ":";
static ARROW: &'static str = "::=";
static TICK: &'static str = "`";
const COMMA: &'static str = ",";
const OR: &'static str = "|";
const COLON: &'static str = ":";
const ARROW: &'static str = "::=";
const TICK: &'static str = "`";

static TS: &'static [&'static str] = &[COMMA, OR, COLON, ARROW, TICK];
static INDEXES: &'static [uint] = &[0, 1, 2, 3, 4];
static INDEXES: &'static [usize] = &[0, 1, 2, 3, 4];

static QUOTE: char = '\'';

Expand All @@ -58,16 +57,16 @@ pub fn tokenise(input: &'static str) -> Vec<&'static str> {

struct Lexer {
input: &'static str,
start: uint,
end: uint,
start: usize,
end: usize,
}

#[postcond="result.start == result.end"]
#[postcond="__result.start == __result.end"]
fn new_lexer(input: &'static str) -> Lexer {
Lexer {
input: input,
start: 0u,
end: 0u,
start: 0,
end: 0,
}
}

Expand All @@ -90,7 +89,7 @@ fn next(this: &mut Lexer) -> Option<&'static str> {
// Returns the current token.
#[precond="this.end > this.start"]
fn cur_token(this: &Lexer) -> &'static str {
this.input.slice(this.start, this.end)
&this.input[this.start..this.end]
}

// Advance start to next non-whitespace char, or EOF.
Expand All @@ -107,7 +106,7 @@ fn scan_to_token(this: &mut Lexer) {
#[postcond="this.end - this.start > 0 && !is_space(this, this.end-1)"]
fn scan_token(this: &mut Lexer) {
// The set of possible terminals we could be lexing.
let mut terminals: HashSet<uint> = HashSet::new();
let mut terminals: HashSet<usize> = HashSet::new();

// If the token is quoted, eat the opening quote and remember to eat the
// closing quote at the end.
Expand All @@ -118,7 +117,7 @@ fn scan_token(this: &mut Lexer) {
terminals.extend(INDEXES.iter().map(|i| *i));
// See if the first char matches any terminal. Means we'll match the
// first char twice, but no biggie.
terminals = terminals.move_iter().filter(
terminals = terminals.into_iter().filter(
|t| this.input.as_bytes()[this.start] == TS[*t].as_bytes()[0]).collect();
this.end += 1;
(false, terminals.len() > 0)
Expand Down Expand Up @@ -153,14 +152,14 @@ fn scan_token(this: &mut Lexer) {
} else {
false
};
terminals = terminals.move_iter().filter(|t| {
terminals = terminals.into_iter().filter(|t| {
let offset = this.end - this.start;
offset < TS[*t].len()
&& this.input.as_bytes()[this.end] == TS[*t].as_bytes()[offset]
}).collect();
if terminals.len() == 0 {
// Got to the end of the only possibility.
assert!(winner, "WHOOPS! Went from >1 to 0 possibilities to lex")
assert!(winner, "WHOOPS! Went from >1 to 0 possibilities to lex");
return;
}
} else {
Expand All @@ -178,13 +177,13 @@ fn scan_token(this: &mut Lexer) {

// true if self.start points to whitespace (space or newline)
#[precond="index < this.input.as_bytes().len()"]
fn is_space(this: &Lexer, index: uint) -> bool {
fn is_space(this: &Lexer, index: usize) -> bool {
this.input.as_bytes()[index] == ' ' as u8 || this.input.as_bytes()[index] == '\n' as u8
}

// true if self.start points to '
#[precond="index < this.input.as_bytes().len()"]
fn is_quote(this: &Lexer, index: uint) -> bool {
fn is_quote(this: &Lexer, index: usize) -> bool {
this.input.as_bytes()[index] == QUOTE as u8
}

Expand Down
47 changes: 22 additions & 25 deletions libhoare/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,7 @@

// See ../readme.md for an overview.

#![crate_type="dylib"]
#![crate_name="hoare"]
#![feature(plugin_registrar)]
#![feature(quote)]
#![feature(plugin_registrar, quote, rustc_private)]

extern crate rustc;
extern crate syntax;
Expand All @@ -31,17 +28,17 @@ use rustc::plugin::Registry;
#[plugin_registrar]
pub fn plugin_registrar(reg: &mut Registry) {
reg.register_syntax_extension(token::intern("precond"),
Modifier(box precond));
Modifier(Box::new(precond)));
reg.register_syntax_extension(token::intern("postcond"),
Modifier(box postcond));
Modifier(Box::new(postcond)));
reg.register_syntax_extension(token::intern("invariant"),
Modifier(box invariant));
Modifier(Box::new(invariant)));
reg.register_syntax_extension(token::intern("debug_precond"),
Modifier(box debug_precond));
Modifier(Box::new(debug_precond)));
reg.register_syntax_extension(token::intern("debug_postcond"),
Modifier(box debug_postcond));
Modifier(Box::new(debug_postcond)));
reg.register_syntax_extension(token::intern("debug_invariant"),
Modifier(box debug_invariant));
Modifier(Box::new(debug_invariant)));
}

fn precond(cx: &mut ExtCtxt,
Expand All @@ -55,7 +52,7 @@ fn precond(cx: &mut ExtCtxt,
Some(pred) => pred,
None => return item.clone()
};
let pred_str = pred.get();
let pred_str = &pred;
let pred = cx.parse_expr(pred_str.to_string());

// Construct the wrapper function.
Expand All @@ -64,7 +61,7 @@ fn precond(cx: &mut ExtCtxt,
let mut stmts = Vec::new();
stmts.push(assert(&*cx, "precondition of", &fn_name, pred.clone(), pred_str));

let fn_name = ast::Ident::new(token::intern(format!("__inner_fn_{}", fn_name).as_slice()));
let fn_name = ast::Ident::new(token::intern(&format!("__inner_fn_{}", fn_name)));
// Construct the inner function.
let inner_item = P(Item { attrs: Vec::new(), vis: ast::Inherited, .. (*item).clone() });
stmts.push(fn_decl(sp, fn_name, inner_item));
Expand Down Expand Up @@ -99,7 +96,7 @@ fn postcond(cx: &mut ExtCtxt,
Some(pred) => pred,
None => return item.clone()
};
let pred_str = pred.get();
let pred_str = &pred;
// Rename `return` to `__result`
let pred_str = pred_str.replace("return", "__result");
let pred = cx.parse_expr(pred_str.clone());
Expand All @@ -108,7 +105,7 @@ fn postcond(cx: &mut ExtCtxt,
let fn_name = token::get_ident(item.ident);

let mut stmts = Vec::new();
let fn_ident = ast::Ident::new(token::intern(format!("__inner_{}", fn_name).as_slice()));
let fn_ident = ast::Ident::new(token::intern(&format!("__inner_{}", fn_name)));
// Construct the inner function.
let inner_item = P(Item { attrs: Vec::new(), vis: ast::Inherited, .. (*item).clone() });
stmts.push(fn_decl(sp, fn_ident, inner_item));
Expand All @@ -121,7 +118,7 @@ fn postcond(cx: &mut ExtCtxt,
let ty_args = ty_args(generics, sp);
stmts.push(assign_expr(&*cx, fn_ident, args, ty_args));

stmts.push(assert(&*cx, "postcondition of", &fn_name, pred, pred_str.as_slice()));
stmts.push(assert(&*cx, "postcondition of", &fn_name, pred, &pred_str[..]));

let body = fn_body(cx, stmts, sp);
P(Item { node: ast::ItemFn(decl.clone(), style, abi, generics.clone(), body),
Expand All @@ -145,7 +142,7 @@ fn invariant(cx: &mut ExtCtxt,
Some(pred) => pred,
None => return item.clone()
};
let pred_str = pred.get();
let pred_str = &pred;
let pred = cx.parse_expr(pred_str.to_string());

// Construct the wrapper function.
Expand All @@ -154,7 +151,7 @@ fn invariant(cx: &mut ExtCtxt,
let mut stmts = Vec::new();
stmts.push(assert(&*cx, "invariant entering", &fn_name, pred.clone(), pred_str));

let fn_ident = ast::Ident::new(token::intern(format!("__inner_{}", fn_name).as_slice()));
let fn_ident = ast::Ident::new(token::intern(&format!("__inner_{}", fn_name)));
// Construct the inner function.
let inner_item = P(Item { attrs: Vec::new(), vis: ast::Inherited, .. (*item).clone() });
stmts.push(fn_decl(sp, fn_ident, inner_item));
Expand Down Expand Up @@ -200,7 +197,8 @@ fn debug_invariant(cx: &mut ExtCtxt,
}

// Executes f if we are compiling in debug mode, returns item otherwise.
fn if_debug(cx: &mut ExtCtxt, f: |&mut ExtCtxt| -> P<Item>, item: P<Item>) -> P<Item> {
fn if_debug<F>(cx: &mut ExtCtxt, f: F, item: P<Item>) -> P<Item>
where F: Fn(&mut ExtCtxt) -> P<Item> {
if !cx.cfg().iter().any(
|item| item.node == ast::MetaWord(token::get_name(token::intern("ndebug")))) {
f(cx)
Expand All @@ -224,7 +222,7 @@ fn make_predicate(cx: &ExtCtxt,
match &attr.node {
&ast::MetaNameValue(ref name, ref lit) => {
if name == &token::get_name(token::intern(cond_name)) ||
name == &token::get_name(token::intern(debug_name(cond_name).as_slice())) {
name == &token::get_name(token::intern(&debug_name(cond_name)[..])) {
match &lit.node {
&ast::LitStr(ref lit, _) => {
Some(lit.clone())
Expand All @@ -235,8 +233,7 @@ fn make_predicate(cx: &ExtCtxt,
}
}
} else {
cx.span_err(sp, format!("unexpected name in condition: {}",
name).as_slice());
cx.span_err(sp, &format!("unexpected name in condition: {}", name)[..]);
None
}
},
Expand All @@ -254,7 +251,8 @@ fn assert(cx: &ExtCtxt,
fn_name: &token::InternedString,
pred: P<ast::Expr>,
pred_str: &str) -> P<ast::Stmt> {
let label = format!("\"{} {} ({})\"", cond_type, fn_name, pred_str);
let label = format!("\"{} {} ({})\"", cond_type, fn_name,
pred_str.replace("\"", "\\\""));
let label = cx.parse_expr(label);
quote_stmt!(&*cx, assert!($pred, $label);)
}
Expand All @@ -275,7 +273,7 @@ fn is_sane_pattern(pat: &ast::Pat) -> bool {
&ast::PatIdent(..) => false,
&ast::PatEnum(_, Some(ref ps)) | &ast::PatTup(ref ps) => ps.iter().all(|p| is_sane_pattern(&**p)),
&ast::PatEnum(..) => false,
&ast::PatBox(ref p) | &ast::PatRegion(ref p) => is_sane_pattern(&**p)
&ast::PatBox(ref p) | &ast::PatRegion(ref p, _) => is_sane_pattern(&**p)
}
}

Expand All @@ -287,7 +285,7 @@ fn args(cx: &ExtCtxt, decl: &ast::FnDecl, sp: Span) -> Option<Vec<ast::TokenTree
}

let cm = &cx.parse_sess.span_diagnostic.cm;
let mut args = decl.inputs.iter().map(|a| {
let args = decl.inputs.iter().map(|a| {
// span_to_snippet really shouldn't return None, so I hope the
// unwrap is OK. Not sure we can do anything it is does in any case.
cx.parse_tts(cm.span_to_snippet(a.pat.span).unwrap())
Expand Down Expand Up @@ -347,7 +345,6 @@ fn fn_body(cx: &ExtCtxt,
stmts: Vec<P<ast::Stmt>>,
sp: Span) -> P<ast::Block> {
P(ast::Block {
view_items: vec!(),
stmts: stmts,
expr: Some(result_expr(&*cx)),
id: ast::DUMMY_NODE_ID,
Expand Down
24 changes: 8 additions & 16 deletions test.sh
Original file line number Diff line number Diff line change
@@ -1,18 +1,10 @@
cargo test
echo cfail tests
echo
$RUSTC test/cfail-1.rs -L ../obj
$RUSTC test/cfail-2.rs -L ../obj
$RUSTC test/cfail-3.rs -L ../obj
$RUSTC test/cfail-4.rs -L ../obj
$RUSTC test/cfail-5.rs -L ../obj
$RUSTC test/cfail-6.rs -L ../obj
echo
echo unit tests
echo
$RUSTC test/mod.rs --test -L ../obj -o ../obj/test
../obj/test
echo
echo rpass tests
echo
$RUSTC test/rpass-1.rs -L ../obj -o ../obj/rpass-1
../obj/rpass-1
$RUSTC tests-cfail/cfail-1.rs -L ./target
$RUSTC tests-cfail/cfail-2.rs -L ./target
$RUSTC tests-cfail/cfail-3.rs -L ./target
$RUSTC tests-cfail/cfail-4.rs -L ./target
$RUSTC tests-cfail/cfail-5.rs -L ./target
$RUSTC tests-cfail/cfail-6.rs -L ./target
echo
Loading

0 comments on commit f378c25

Please sign in to comment.