Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file! { #[test] test1 verus_code! { fn test1() { assert(true); assert(!false); assert(true && true); assert(true || false); assert(true); } } => Ok(())}
test_verify_one_file! { #[test] test1_fails verus_code! { fn test1() { assert(true); assert(true && false); // FAILS assert(false); assert(false); } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test2 verus_code! { uninterp spec fn f(i: int, j: int) -> bool;
fn test2(b: bool, x: int, y: int, z: int) { assert(b || !b);
assume(b); assert(b);
assert(x == y ==> f(x, y) == f(y, x));
assert(x + y == y + x);
assume(x <= y && y <= z); assert(x <= z); } } => Ok(())}
test_verify_one_file! { #[test] test2_fails verus_code! { fn test2(b: bool, x: int, y: int, z: int) { assume(x <= y && y <= z); assert(x < z); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_assign verus_code! { fn test_assign(a: int, b: int) { let c = a + b; assert(c == a + b);
let d = false; assert(!d);
assert(c < a + b); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_assign_mut verus_code! { fn test_assign_mut(a: int, b: int) { let mut c = a; c = c + b; assert(c == a + b); assert(c == a); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_spec_fn verus_code! { spec fn f1(i: int, j: int) -> bool { i <= j }
spec fn f2(i: int, j: int) -> bool { let x = i; let y = j; x < y }
#[verifier(opaque)] spec fn f3(i: int, j: int) -> bool { f1(j, i) }
fn test_spec_fn(a: int, b: int) { hide(f2);
assume(f2(a, b)); proof { reveal(f2); } assert(f1(a, b));
proof { reveal(f3); } assert(f3(b, a)); assert(f3(a, b)); // FAILS } } => Err(err) => assert_one_fails(err)}
const TEST_REQUIRES1: &str = verus_code_str! { proof fn test_requires1(a: int, b: int, c: int) requires a <= b, #![verifier::proof_note("Test label #1")] b <= c, { assert(a <= c); }};
test_verify_one_file! { #[test] test_requires2 TEST_REQUIRES1.to_string() + verus_code_str! { proof fn test_requires2(a: int, b: int, c: int) { assume(a <= b); assume(b <= c); test_requires1(a + a, b + b, c + c); test_requires1(a + a, b + b, a + c); // FAILS } } => Err(err) => assert_help_error_msg(err, "note: Test label #1")}
test_verify_one_file! { #[test] test_requires3 TEST_REQUIRES1.to_string() + verus_code_str! { fn test_requires3(a: int, b: int, c: int) { assume(a <= b); assume( #[verifier::proof_note("Test label #2")] (b <= c) ); proof { test_requires1(a + a, b + b, c + c); test_requires1(a + c, b + b, c + c); // FAILS } } } => Err(err) => assert_one_fails(err)}
const TEST_RET: &str = verus_code_str! { proof fn test_ret(a: int, b: int) -> (ret: int) requires a <= b, ensures #![verifier::proof_note("Test label #3")] ret <= a + b, ret <= a + a, // FAILS ret <= b + b, { a + b }};
test_verify_one_file! { #[test] test_ret TEST_RET.to_string() => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_proof_note_on_requires verus_code! { fn example(x: u64, y: u64) -> (z: u64) requires #![verifier::proof_note("Property 732")] x == y, { x + y }
fn caller() { let _ = example(1, 2); // precondition fails } } => Err(err) => assert_help_error_msg(err, "note: Property 732")}
test_verify_one_file! { #[test] test_multiple_proof_notes_on_requires verus_code! { fn example(x: u64, y: u64) -> (z: u64) requires #![verifier::proof_note("Property 732")] #![verifier::proof_note("Property 451")] x == y, { x + y } } => Err(err) => assert_vir_error_msg(err, "at most one `proof_note` attribute is allowed")}
test_verify_one_file! { #[test] test_proof_note_on_ensures verus_code! { fn example(x: u64, y: u64) -> (z: u64) ensures #![verifier::proof_note("Property 732")] z == x + y, { x }
fn caller() { let _ = example(1, 2); // postcondition fails } } => Err(err) => assert_help_error_msg(err, "note: Property 732")}
test_verify_one_file! { #[test] test_multiple_proof_notes_on_ensures verus_code! { fn example(x: u64, y: u64) -> (z: u64) ensures #![verifier::proof_note("Property 732")] #![verifier::proof_note("Property 451")] z == x + y, { x } } => Err(err) => assert_vir_error_msg(err, "at most one `proof_note` attribute is allowed")}
test_verify_one_file! { #[test] test_proof_note_on_assert verus_code! { fn caller() { #[verifier::proof_note("Statement known to be false")] assert(1 > 2); // assertion fails } } => Err(err) => assert_help_error_msg(err, "note: Statement known to be false")}
test_verify_one_file! { #[test] test_multiple_proof_notes_on_assert verus_code! { fn caller() { #[verifier::proof_note("Statement known to be false")] #[verifier::proof_note("This is another proof label")] assert(1 > 2); // assertion fails } } => Err(err) => assert_vir_error_msg(err, "at most one `proof_note` attribute is allowed")}
test_verify_one_file_with_options! { #[test] test_proof_note_on_assume_with_no_cheating ["--no-cheating"] => verus_code! { fn caller() { #[verifier::proof_note("Statement known to be false")] assume(1 > 2); // assumption fails } } => Err(err) => assert_help_error_msg(err, "note: Statement known to be false")}
test_verify_one_file! { #[test] test_multiple_proof_notes_on_assume verus_code! { fn caller() { #[verifier::proof_note("Statement known to be false")] #[verifier::proof_note("This is another proof label")] assume(1 > 2); // assumption fails } } => Err(err) => assert_vir_error_msg(err, "at most one `proof_note` attribute is allowed")}
test_verify_one_file! { #[test] test_custom_err_on_assert verus_code! { fn caller() { #[verifier::custom_err("Custom assert error")] assert(1 > 2); } } => Err(err) => assert_vir_error_msg(err, "Custom assert error")}
test_verify_one_file! { #[test] test_multiple_custom_errs_on_assert verus_code! { fn caller() { #[verifier::custom_err("Custom assert error")] #[verifier::custom_err("Another custom error")] assert(1 > 2); } } => Err(err) => assert_vir_error_msg(err, "at most one `proof_note` attribute is allowed")}
test_verify_one_file_with_options! { #[test] test_custom_err_on_assume_with_no_cheating ["--no-cheating"] => verus_code! { fn caller() { #[verifier::custom_err("Custom assume error")] assume(1 > 2); } } => Err(err) => assert_vir_error_msg(err, "Custom assume error")}
test_verify_one_file! { #[test] test_custom_err_on_requires verus_code! { fn example(x: u64, y: u64) -> (z: u64) requires #![verifier::custom_err("Custom requires error")] x == y, { x }
fn caller() { let _ = example(1, 2); } } => Err(err) => assert_vir_error_msg(err, "Custom requires error")}
test_verify_one_file! { #[test] test_custom_err_on_ensures verus_code! { fn example(x: u64, y: u64) -> (z: u64) ensures #![verifier::custom_err("Custom ensures error")] z == x + y, { x }
fn caller() { let _ = example(1, 2); } } => Err(err) => assert_vir_error_msg(err, "Custom ensures error")}
test_verify_one_file! { #[test] test_ret2 TEST_RET.to_string() + verus_code_str! { proof fn test_ret2(a: int, b: int) -> (ret: int) requires a <= b, ensures ret <= a + b, ret <= a + a, ret <= b + b, { let mut x = test_ret(a, a); x = test_ret(x, x); assert(x <= 4 * a); x = test_ret(b, b); x = test_ret(x, x); assert(x <= 4 * b); x = test_ret(a + 1, a + 2); x = test_ret(x + 3, x + 4); assert(x <= 4 * a + 4 + 6); x = test_ret(a, b); x } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_exec_fun1 verus_code! { fn f(x: u64) -> u64 { 5 }
fn g(x: u64) -> u64 { f(x) } } => Ok(())}
test_verify_one_file! { #[test] test_ensures_ret_val_collision verus_code! { fn f(k: u32, n: u32) -> ((_, n): (u32, u32)) ensures n <= k, { (42, k / 2) } } => Err(err) => assert_vir_error_msg(err, "return value name collides with a parameter name")}
test_verify_one_file! { #[test] test_short_circuit verus_code! { fn f1(a: bool, b: bool) { let mut x: u64 = 0; let y = a && b; let z = a && { x = x + 1; b }; assert(y == z); assert((x == 1) == a); }
fn f2(a: bool, b: bool) { let mut x: u64 = 0; let y = a || b; let z = a || { x = x + 1; b }; assert(y == z); assert((x == 1) == !a); } } => Ok(())}
test_verify_one_file! { #[test] test_short_circuit1 verus_code! { proof fn f3(a: bool, b: bool) { let mut x: u64 = 0; let y: bool = imply(a, b); let z: bool = imply(a, { x = add(x, 1); b }); assert(y == z); assert((x == 1) == a); } } => Ok(())}
test_verify_one_file! { #[test] test_short_circuit2 verus_code! { fn f1(a: bool, b: bool) { let mut x: u64 = 0; let y = a && b; let z = a && { x = x + 1; b }; assert(y == z); assert(x == 0); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_short_circuit3 verus_code! { fn f1(a: bool, b: bool) { let mut x: u64 = 0; let y = a && b; let z = a && { x = x + 1; b }; assert(y == z); assert(x == 1); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_paren verus_code! { fn test_paren() { {{{{if true {} else {}}}}} ((((if true {} else {})))) } } => Ok(())}
test_verify_one_file! { #[test] test_fail_assign_non_mut verus_code! { fn test1() { let x: u64 = 10; x = 20; } } => Err(err) => assert_rust_error_msg(err, "cannot assign twice to immutable variable")}
test_verify_one_file! { #[test] test_fail_return_value_parameter_same_name verus_code! { fn foo(x: u64) -> (x: bool) ensures x || !x { x > 10 } } => Err(err) => assert_vir_error_msg(err, "return value name collides with a parameter name")}
test_verify_one_file! { #[test] test_ensures_type_inference verus_code! { struct Foo { pub b: bool, }
spec fn get_b(foo: Foo) -> bool { foo.b }
fn test1() -> (b: Foo) ensures get_b(b) { Foo { b: true } } } => Ok(())}
test_verify_one_file! { #[test] test_decl_init_let_pass verus_code! { fn test1() { let x: u64; #[allow(unused_assignments)] x = 23; } } => Ok(())}
test_verify_one_file! { #[test] test_decl_init_let_fail verus_code! { fn test1() { let x: u64; assert(x == 23); // FAILS x = 23; }
fn test2(a: bool) { let x: u64; if a { x = 1; } else { x = 2; } assert(a ==> (x == 1)); assert(false); // FAILS } } => Err(e) => assert_fails(e, 2)}
test_verify_one_file! { #[test] bool_xor verus_code! { fn test1() { assert((true ^ true) == false); assert((false ^ true) == true); assert((true ^ false) == true); assert((false ^ false) == false); } } => Ok(())}
test_verify_one_file! { #[test] bool_xor_fails verus_code! { fn test1() { assert((true ^ true) == true); // FAILS } fn test2() { assert((false ^ true) == false); // FAILS } fn test3() { assert((true ^ false) == false); // FAILS } fn test4() { assert((false ^ false) == true); // FAILS } } => Err(e) => assert_fails(e, 4)}
test_verify_one_file! { #[test] test_init_spec_param_fail_1 verus_code! { proof fn test1(x: u64) { x = 5; } } => Err(e) => assert_vir_error_msg(e, "variable `x` is not marked mutable")}
test_verify_one_file! { #[test] test_init_spec_param_fail_2 verus_code! { spec fn test1(x: u64) { x = 5; } } => Err(e) => assert_vir_error_msg(e, "assignment is not allowed inside pure context")}
test_verify_one_file! { // TODO restore this test when erasure is overhauled #[ignore] #[test] equal_regression_148 code! { #[verifier::proof] fn f() { equal(1 as nat, 1); } } => Ok(())}
test_verify_one_file! { #[test] test_big_and verus_code! { proof fn test() { assert({ &&& true &&& true }); } } => Ok(())}
test_verify_one_file! { #[test] test_big_and_fail verus_code! { proof fn test() { assert({ &&& true &&& false }); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_big_or verus_code! { proof fn test() { assert({ ||| true ||| false }); } } => Ok(())}
test_verify_one_file! { #[test] test_big_or_fail verus_code! { proof fn test() { assert({ ||| fails ||| false }); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_big_and_syntax_vs_forall verus_code! { spec fn test() -> bool { &&& forall|i: int| true &&& i == 0 } } => Err(e) => assert_rust_error_msg(e, "cannot find value `i`")}
test_verify_one_file! { #[test] test_compound_assign verus_code! { fn test1(y: &mut u32) { let mut x: i32 = 1; x += 2; assert({ x == 3 as i32 }); *y /= 2; assert({ *y == *old(y)/2 }); }
proof fn test2a() { let mut x: u8 = 200; x = (x + 100u8) as u8; assert(x < 256); }
proof fn test2b() { let mut x: u8 = 200; x += 100u8; assert(x < 256); }
fn test3a() { let mut x: u8 = 200; x = x / (x + 1); assert(x < 256); }
fn test3b() { let mut x: u8 = 200; x /= (x + 1); assert(x < 256); }
} => Ok(())}
test_verify_one_file! { #[test] test_compound_assign_fail verus_code! { fn test1(x: &mut u32, y: u32) { *x /= y; // FAILS }
fn test2(x: i8) { let mut x = x; x += 1; // FAILS }
fn test3a() { let mut x: u8 = 200; x = x + 100u8; // FAILS assert(x < 256); }
fn test3b() { let mut x: u8 = 200; x += 100u8; // FAILS assert(x < 256); }
} => Err(err) => assert_fails(err, 4)}
test_verify_one_file! { #[test] test_spec_eq_type_error_1 verus_code! { fn test(a: u64, b: Option<u64>) requires a == b { } } => Err(err) => assert_rust_error_msg(err, "the trait bound")}
test_verify_one_file! { #[test] test_spec_eq_type_error_2 verus_code! { fn test(a: u64, b: std::sync::Arc<Option<u64>>) requires a == b { } } => Err(err) => assert_rust_error_msg(err, "the trait bound")}
test_verify_one_file! { #[test] test_spec_eq_type_error_3 verus_code! { fn test(a: u64, b: spec_fn(u64)->nat) requires a == b { } } => Err(err) => assert_rust_error_msg(err, "the trait bound")}
test_verify_one_file! { #[test] test_spec_eq_type_error_4 verus_code! { trait A { type AT; }
fn test<X: A>(a: (u64, nat), b: <X as A>::AT) requires a == b { } } => Err(err) => assert_rust_error_msg(err, "the trait bound")}
test_verify_one_file! { #[test] test_spec_eq_type_error_5 verus_code! { fn test() { let a = |x: i32| x + 3; assert(a == 5); } } => Err(err) => assert_rust_error_msg(err, "the trait bound")}
test_verify_one_file! { #[test] test_spec_eq_trait_error verus_code! { fn f<A: SpecEq<A>>() {} } => Err(err) => assert_vir_error_msg(err, "cannot use trait marked `verifier::internal_trait`")}
test_verify_one_file! { #[test] test_mut_param verus_code! { fn test1(mut x: u32) requires x < 10, ensures // mut params are always evaluated to their original // value in postconditions x < 10, { assert(x < 20); x = 100; assert(x == 100); }
fn test2(mut x: u32) requires x < 10; ensures x == 100, // FAILS { assert(x < 20); x = 100; assert(x == 100); }
proof fn test3(mut x: int) { x += 1; }
struct T { x: i32, y: u64, }
fn test4(mut t: T) { let y = t.y; t.x = 100; assert(t.x == 100); assert(t.y == y); } } => Err(err) => assert_fails(err, 1)}
test_verify_one_file! { #[test] test_mut_param_spec_fail verus_code! { spec fn f(mut x: i32) -> i32; } => Err(err) => assert_vir_error_msg(err, "mut argument not allowed for spec functions")}
test_verify_one_file! { #[test] test_mut_self verus_code! { struct T { i: u64 }
impl T { fn test(mut self) -> (u: u64) requires self.i == 0, ensures u == self.i { self.i = 20; assert(self.i == 20); 0 }
fn test2(mut self) -> (s: Self) requires self.i == 0, ensures self.i == 0 && s.i == 20 { self.i = 20; assert(self.i == 20); self } } } => Ok(())}
test_verify_one_file! { #[test] test_rlimit_20 verus_code! { #[verifier::rlimit(20)] fn test1() { assert(true); assert(!false); assert(true && true); assert(true || false); assert(true); } } => Ok(())}
test_verify_one_file! { #[test] test_rlimit_inf verus_code! { #[verifier::rlimit(infinity)] fn test1() { assert(true); } } => Ok(())}
test_verify_one_file! { #[test] test_bodyless_fn verus_code! { // We allow a final comma in the ensures // list for a bodyless function trait Marshalable { spec fn is_marshalable(&self) -> bool; exec fn _is_marshalable(&self) -> (res: bool) ensures res == self.is_marshalable(), ; } } => Ok(())}
test_verify_one_file! { #[test] destructuring_assignment_unsupported verus_code! { fn test() { let mut a = 0; let mut b = 0; (a, b) = (1, 2); } } => Err(err) => assert_vir_error_msg(err, "Verus does not currently support destructuring assignment")}
test_verify_one_file! { #[test] ensures_clause_no_named_ret_value verus_code! { fn test() -> u8 ensures 0 == 1 // FAILS { 1 } } => Err(err) => assert_fails(err, 1)}
test_verify_one_file! { #[test] test_bitwise_bool_ops verus_code! { fn test_or(a: bool, b: bool) { let x = a | b; assert(x <==> (a || b));
let mut y = a; y |= b; assert(y <==> (a || b)); }
fn test_and(a: bool, b: bool) { let x = a & b; assert(x <==> (a && b));
let mut y = a; y &= b; assert(y <==> (a && b)); }
fn test_or_with_side_effect(a: bool, b: bool) { let mut side_tester = 0;
let x = a | ({ side_tester = 1; b }); assert(x <==> (a || b)); assert(side_tester == 1);
let mut y = a; y |= ({ side_tester = 2; b }); assert(y <==> (a || b)); assert(side_tester == 2); }
fn test_and_with_side_effect(a: bool, b: bool) { let mut side_tester = 0;
let x = a & ({ side_tester = 1; b }); assert(x <==> (a && b)); assert(side_tester == 1);
let mut y = a; y &= ({ side_tester = 2; b }); assert(y <==> (a && b)); assert(side_tester == 2); } } => Ok(())}