-
Notifications
You must be signed in to change notification settings - Fork 13.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Refactor contract builtin macro + error handling
Instead of parsing the different components of a function signature, eagerly look for either the `where` keyword or the function body. - Also address feedback to use `From` instead of `TryFrom` in cranelift contract and ubcheck codegen.
- Loading branch information
Showing
7 changed files
with
280 additions
and
73 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
//! Test for some of the existing limitations and the current error messages. | ||
//! Some of these limitations may be removed in the future. | ||
#![feature(rustc_contracts)] | ||
#![allow(dead_code)] | ||
|
||
/// Represent a 5-star system. | ||
struct Stars(u8); | ||
|
||
impl Stars { | ||
fn is_valid(&self) -> bool { | ||
self.0 <= 5 | ||
} | ||
} | ||
|
||
trait ParseStars { | ||
#[core::contracts::ensures(|ret| ret.is_none_or(Stars::is_valid))] | ||
//~^ ERROR contract annotations is only supported in functions with bodies | ||
fn parse_string(input: String) -> Option<Stars>; | ||
|
||
#[core::contracts::ensures(|ret| ret.is_none_or(Stars::is_valid))] | ||
//~^ ERROR contract annotations is only supported in functions with bodies | ||
fn parse<T>(input: T) -> Option<Stars> where T: for<'a> Into<&'a str>; | ||
} | ||
|
||
fn main() { | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
error: contract annotations is only supported in functions with bodies | ||
--> $DIR/contract-annotation-limitations.rs:17:5 | ||
| | ||
LL | #[core::contracts::ensures(|ret| ret.is_none_or(Stars::is_valid))] | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
||
error: contract annotations is only supported in functions with bodies | ||
--> $DIR/contract-annotation-limitations.rs:21:5 | ||
| | ||
LL | #[core::contracts::ensures(|ret| ret.is_none_or(Stars::is_valid))] | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
||
error: aborting due to 2 previous errors | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,70 @@ | ||
//! Test that contracts can be applied to generic functions. | ||
//@ revisions: unchk_pass chk_pass chk_fail_pre chk_fail_post chk_const_fail | ||
// | ||
//@ [unchk_pass] run-pass | ||
//@ [chk_pass] run-pass | ||
// | ||
//@ [chk_fail_pre] run-fail | ||
//@ [chk_fail_post] run-fail | ||
//@ [chk_const_fail] run-fail | ||
// | ||
//@ [unchk_pass] compile-flags: -Zcontract-checks=no | ||
// | ||
//@ [chk_pass] compile-flags: -Zcontract-checks=yes | ||
//@ [chk_fail_pre] compile-flags: -Zcontract-checks=yes | ||
//@ [chk_fail_post] compile-flags: -Zcontract-checks=yes | ||
//@ [chk_const_fail] compile-flags: -Zcontract-checks=yes | ||
|
||
#![feature(rustc_contracts)] | ||
|
||
use std::ops::Sub; | ||
|
||
/// Dummy fn contract that precondition fails for val < 0, and post-condition fail for val == 1 | ||
#[core::contracts::requires(val > 0u8.into())] | ||
#[core::contracts::ensures(|ret| *ret > 0u8.into())] | ||
fn decrement<T>(val: T) -> T | ||
where T: PartialOrd + Sub<Output=T> + From<u8> | ||
{ | ||
val - 1u8.into() | ||
} | ||
|
||
/// Create a structure that takes a constant parameter. | ||
#[allow(dead_code)] | ||
struct Capped<const MAX: usize>(usize); | ||
|
||
/// Now declare a function to create stars which shouldn't exceed 5 stars. | ||
// Add redundant braces to ensure the built-in macro can handle this syntax. | ||
#[allow(unused_braces)] | ||
#[core::contracts::requires(num <= 5)] | ||
unsafe fn stars_unchecked(num: usize) -> Capped<{ 5 }> { | ||
Capped(num) | ||
} | ||
|
||
|
||
fn main() { | ||
check_decrement(); | ||
check_stars(); | ||
} | ||
|
||
fn check_stars() { | ||
// This should always pass. | ||
let _ = unsafe { stars_unchecked(3) }; | ||
|
||
// This violates the contract. | ||
#[cfg(any(unchk_pass, chk_const_fail))] | ||
let _ = unsafe { stars_unchecked(10) }; | ||
} | ||
|
||
fn check_decrement() { | ||
// This should always pass | ||
assert_eq!(decrement(10u8), 9u8); | ||
|
||
// This should fail requires but pass with no contract check. | ||
#[cfg(any(unchk_pass, chk_fail_pre))] | ||
assert_eq!(decrement(-2i128), -3i128); | ||
|
||
// This should fail ensures but pass with no contract check. | ||
#[cfg(any(unchk_pass, chk_fail_post))] | ||
assert_eq!(decrement(1i32), 0i32); | ||
} |
52 changes: 52 additions & 0 deletions
52
tests/ui/contracts/disallow-contract-annotation-on-non-fn.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
//! Checks for compilation errors related to adding contracts to non-function items. | ||
#![feature(rustc_contracts)] | ||
#![allow(dead_code)] | ||
|
||
#[core::contracts::requires(true)] | ||
//~^ ERROR contract annotations can only be used on functions | ||
struct Dummy(usize); | ||
|
||
#[core::contracts::ensures(|v| v == 100)] | ||
//~^ ERROR contract annotations can only be used on functions | ||
const MAX_VAL: usize = 100; | ||
|
||
// FIXME: Improve the error message here. The macro thinks this is a function. | ||
#[core::contracts::ensures(|v| v == 100)] | ||
//~^ ERROR contract annotations is only supported in functions with bodies | ||
type NewDummy = fn(usize) -> Dummy; | ||
|
||
#[core::contracts::ensures(|v| v == 100)] | ||
//~^ ERROR contract annotations is only supported in functions with bodies | ||
const NEW_DUMMY_FN : fn(usize) -> Dummy = || { Dummy(0) }; | ||
|
||
#[core::contracts::requires(true)] | ||
//~^ ERROR contract annotations can only be used on functions | ||
impl Dummy { | ||
|
||
// This should work | ||
#[core::contracts::ensures(|ret| ret.0 == v)] | ||
fn new(v: usize) -> Dummy { | ||
Dummy(v) | ||
} | ||
} | ||
|
||
#[core::contracts::ensures(|dummy| dummy.0 > 0)] | ||
//~^ ERROR contract annotations can only be used on functions | ||
impl From<usize> for Dummy { | ||
// This should work. | ||
#[core::contracts::ensures(|ret| ret.0 == v)] | ||
fn from(value: usize) -> Self { | ||
Dummy::new(value) | ||
} | ||
} | ||
|
||
/// You should not be able to annotate a trait either. | ||
#[core::contracts::requires(true)] | ||
//~^ ERROR contract annotations can only be used on functions | ||
pub trait DummyBuilder { | ||
fn build() -> Dummy; | ||
} | ||
|
||
fn main() { | ||
} |
Oops, something went wrong.