mirror of https://codeberg.org/topola/topola.git
build(contracts): use contracts-try v0.7 from crates.io
`contracts-try` is now developed at https://codeberg.org/topola/contracts-try and was extracted from this repo, and rebased upon the original crate sources to ensure proper attribution. This removes the `vendored` directory.
This commit is contained in:
parent
6f237077e3
commit
01deaa4b12
|
|
@ -29,7 +29,7 @@ egui = [
|
||||||
"dep:sys-locale",
|
"dep:sys-locale",
|
||||||
"dep:unic-langid"
|
"dep:unic-langid"
|
||||||
]
|
]
|
||||||
disable_contracts = ["contracts/disable_contracts"]
|
disable_contracts = ["contracts-try/disable_contracts"]
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
thiserror = "1.0"
|
thiserror = "1.0"
|
||||||
|
|
@ -38,7 +38,7 @@ petgraph = "0.6.5"
|
||||||
spade = "2.12.1"
|
spade = "2.12.1"
|
||||||
serde_json = "1.0"
|
serde_json = "1.0"
|
||||||
enum_dispatch = "0.3.13"
|
enum_dispatch = "0.3.13"
|
||||||
contracts = "0.6.3"
|
contracts-try = "0.7"
|
||||||
bimap = "0.6.3"
|
bimap = "0.6.3"
|
||||||
log = "0.4"
|
log = "0.4"
|
||||||
utf8-chars = "3.0.4"
|
utf8-chars = "3.0.4"
|
||||||
|
|
@ -107,9 +107,6 @@ opt-level = 2 # fast and small wasm
|
||||||
[profile.dev.package."*"]
|
[profile.dev.package."*"]
|
||||||
opt-level = 2
|
opt-level = 2
|
||||||
|
|
||||||
[patch.crates-io]
|
|
||||||
contracts = { path = "vendored/contracts" }
|
|
||||||
|
|
||||||
[build-dependencies]
|
[build-dependencies]
|
||||||
clap_mangen = "0.2.23"
|
clap_mangen = "0.2.23"
|
||||||
clap = {version="4.5.18", features = ["derive"] }
|
clap = {version="4.5.18", features = ["derive"] }
|
||||||
|
|
|
||||||
|
|
@ -2,7 +2,7 @@
|
||||||
|
|
||||||
use std::cmp::Ordering;
|
use std::cmp::Ordering;
|
||||||
|
|
||||||
use contracts::debug_requires;
|
use contracts_try::debug_requires;
|
||||||
use enum_dispatch::enum_dispatch;
|
use enum_dispatch::enum_dispatch;
|
||||||
use thiserror::Error;
|
use thiserror::Error;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
use contracts::{debug_ensures, debug_invariant};
|
use contracts_try::{debug_ensures, debug_invariant};
|
||||||
use enum_dispatch::enum_dispatch;
|
use enum_dispatch::enum_dispatch;
|
||||||
use geo::Point;
|
use geo::Point;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
use std::marker::PhantomData;
|
use std::marker::PhantomData;
|
||||||
|
|
||||||
use contracts::debug_invariant;
|
use contracts_try::debug_invariant;
|
||||||
use geo::Point;
|
use geo::Point;
|
||||||
use petgraph::stable_graph::StableDiGraph;
|
use petgraph::stable_graph::StableDiGraph;
|
||||||
use rstar::{primitives::GeomWithData, Envelope, RTree, RTreeObject, AABB};
|
use rstar::{primitives::GeomWithData, Envelope, RTree, RTreeObject, AABB};
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
use contracts::debug_ensures;
|
use contracts_try::debug_ensures;
|
||||||
use enum_dispatch::enum_dispatch;
|
use enum_dispatch::enum_dispatch;
|
||||||
use geo::Point;
|
use geo::Point;
|
||||||
use rstar::AABB;
|
use rstar::AABB;
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
use contracts::debug_ensures;
|
use contracts_try::debug_ensures;
|
||||||
use geo::Point;
|
use geo::Point;
|
||||||
use thiserror::Error;
|
use thiserror::Error;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
use contracts::debug_ensures;
|
use contracts_try::debug_ensures;
|
||||||
use petgraph::data::DataMap;
|
use petgraph::data::DataMap;
|
||||||
|
|
||||||
use crate::drawing::{
|
use crate::drawing::{
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
use contracts::{debug_ensures, debug_requires};
|
use contracts_try::{debug_ensures, debug_requires};
|
||||||
use thiserror::Error;
|
use thiserror::Error;
|
||||||
|
|
||||||
use crate::{
|
use crate::{
|
||||||
|
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
/target
|
|
||||||
**/*.rs.bk
|
|
||||||
Cargo.lock
|
|
||||||
.idea
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
||||||
stages:
|
|
||||||
- fmt-check
|
|
||||||
- test
|
|
||||||
|
|
||||||
fmt-check:
|
|
||||||
stage: fmt-check
|
|
||||||
image: rust:latest
|
|
||||||
before_script:
|
|
||||||
- rustup component add rustfmt
|
|
||||||
script:
|
|
||||||
- cargo fmt --all -- --check
|
|
||||||
|
|
||||||
|
|
||||||
test-stable:
|
|
||||||
stage: test
|
|
||||||
image: rust:latest
|
|
||||||
script:
|
|
||||||
- cargo test --all
|
|
||||||
|
|
||||||
|
|
||||||
test-nightly:
|
|
||||||
stage: test
|
|
||||||
image: rustlang/rust:nightly
|
|
||||||
script:
|
|
||||||
- cargo test --all
|
|
||||||
allow_failure: true
|
|
||||||
|
|
||||||
clippy-tests-stable:
|
|
||||||
stage: test
|
|
||||||
image: rust:latest
|
|
||||||
before_script:
|
|
||||||
- rustup component add clippy
|
|
||||||
script:
|
|
||||||
- cargo clippy --tests
|
|
||||||
|
|
@ -1,91 +0,0 @@
|
||||||
# Changelog
|
|
||||||
All notable changes to this project will be documented in this file.
|
|
||||||
|
|
||||||
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
|
|
||||||
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
|
|
||||||
|
|
||||||
## Unreleased
|
|
||||||
|
|
||||||
## [0.6.3] - 2022-03-13
|
|
||||||
|
|
||||||
### Fixed
|
|
||||||
|
|
||||||
- improved hygiene around `self` parameters
|
|
||||||
- fix contract messages containing `{}` emitting warnings as they are interpreted as format strings
|
|
||||||
|
|
||||||
## [0.6.2] - 2021-07-21
|
|
||||||
|
|
||||||
### Changed
|
|
||||||
|
|
||||||
- better handling of mutable borrows and lifetime relationships for functions
|
|
||||||
with contracts
|
|
||||||
|
|
||||||
## [0.6.1] - 2021-07-13
|
|
||||||
|
|
||||||
### Added
|
|
||||||
|
|
||||||
- support for `impl Trait` return types
|
|
||||||
|
|
||||||
## [0.6.0] - 2020-09-05
|
|
||||||
### Changed
|
|
||||||
- `pre` is now `requires`
|
|
||||||
- `post` is now `ensures`
|
|
||||||
|
|
||||||
## [0.5.2] - 2020-09-05
|
|
||||||
### Fixed
|
|
||||||
- Unused braces in function body generated code are removed
|
|
||||||
|
|
||||||
## [0.5.1] - 2020-08-06
|
|
||||||
### Changed
|
|
||||||
- Trait methods now handle attributes better.
|
|
||||||
|
|
||||||
## [0.5.0] - 2020-08-06
|
|
||||||
### Changed
|
|
||||||
- Implication operator is now `->`.
|
|
||||||
|
|
||||||
## [0.4.0] - 2020-05-01
|
|
||||||
### Added
|
|
||||||
- Added support for MIRAI assertions
|
|
||||||
- Added implication operator
|
|
||||||
|
|
||||||
## [0.3.0] - 2019-07-20
|
|
||||||
### Added
|
|
||||||
- Pseudo-function `old(expr)` which in a post-condition evaluates the expression before function execution.
|
|
||||||
- Automatic generation of documentation containing all contracts.
|
|
||||||
|
|
||||||
## [0.2.2] - 2019-07-17
|
|
||||||
### Fixed
|
|
||||||
- Errors inside functions/methods are now properly reported with the correct source location.
|
|
||||||
### Changed
|
|
||||||
- internal handling of contracts is now done in a single proc-macro pass instead of one for each contract.
|
|
||||||
|
|
||||||
## [0.2.1] - 2019-06-07
|
|
||||||
### Fixed
|
|
||||||
- Functions/methods with explicit return statements no longer skip `post` conditions
|
|
||||||
|
|
||||||
## [0.2.0] - 2014-04-12
|
|
||||||
### Added
|
|
||||||
- `contract_trait` attribute to make all implementors of a trait respect contracts.
|
|
||||||
|
|
||||||
## [0.1.1] - 2019-04-08
|
|
||||||
### Added
|
|
||||||
- Feature flags to override contract behavior.
|
|
||||||
- `disable_contracts` ignores all checks
|
|
||||||
- `override_debug` only checks contracts in debug configurations.
|
|
||||||
- `override_log` only prints using the `log`-crate interface.
|
|
||||||
|
|
||||||
## [0.1.0] - 2019-04-06
|
|
||||||
### Added
|
|
||||||
- attributes `pre`/`post`/`invariant` and `debug_` versions of each.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,40 +0,0 @@
|
||||||
[package]
|
|
||||||
name = "contracts"
|
|
||||||
version = "0.6.3"
|
|
||||||
authors = ["karroffel <therzog@mail.de>"]
|
|
||||||
edition = "2018"
|
|
||||||
repository = "https://gitlab.com/karroffel/contracts"
|
|
||||||
license = "MPL-2.0"
|
|
||||||
readme = "README.md"
|
|
||||||
categories = [
|
|
||||||
"development-tools",
|
|
||||||
"development-tools::procedural-macro-helpers",
|
|
||||||
]
|
|
||||||
keywords = [
|
|
||||||
"design-by-contract",
|
|
||||||
"precondition",
|
|
||||||
"postcondition",
|
|
||||||
"invariant",
|
|
||||||
"verification",
|
|
||||||
]
|
|
||||||
documentation = "https://docs.rs/contracts"
|
|
||||||
description = "Design-by-contract attributes"
|
|
||||||
|
|
||||||
[badges]
|
|
||||||
gitlab = { repository = "karroffel/contracts", branch = "master" }
|
|
||||||
|
|
||||||
[lib]
|
|
||||||
name = "contracts"
|
|
||||||
path = "src/lib.rs"
|
|
||||||
proc-macro = true
|
|
||||||
|
|
||||||
[features]
|
|
||||||
disable_contracts = []
|
|
||||||
override_debug = []
|
|
||||||
override_log = []
|
|
||||||
mirai_assertions = []
|
|
||||||
|
|
||||||
[dependencies]
|
|
||||||
syn = { version = "2.0", features = ["extra-traits", "full", "visit", "visit-mut"] }
|
|
||||||
quote = "1.0"
|
|
||||||
proc-macro2 = "1.0"
|
|
||||||
|
|
@ -1,373 +0,0 @@
|
||||||
Mozilla Public License Version 2.0
|
|
||||||
==================================
|
|
||||||
|
|
||||||
1. Definitions
|
|
||||||
--------------
|
|
||||||
|
|
||||||
1.1. "Contributor"
|
|
||||||
means each individual or legal entity that creates, contributes to
|
|
||||||
the creation of, or owns Covered Software.
|
|
||||||
|
|
||||||
1.2. "Contributor Version"
|
|
||||||
means the combination of the Contributions of others (if any) used
|
|
||||||
by a Contributor and that particular Contributor's Contribution.
|
|
||||||
|
|
||||||
1.3. "Contribution"
|
|
||||||
means Covered Software of a particular Contributor.
|
|
||||||
|
|
||||||
1.4. "Covered Software"
|
|
||||||
means Source Code Form to which the initial Contributor has attached
|
|
||||||
the notice in Exhibit A, the Executable Form of such Source Code
|
|
||||||
Form, and Modifications of such Source Code Form, in each case
|
|
||||||
including portions thereof.
|
|
||||||
|
|
||||||
1.5. "Incompatible With Secondary Licenses"
|
|
||||||
means
|
|
||||||
|
|
||||||
(a) that the initial Contributor has attached the notice described
|
|
||||||
in Exhibit B to the Covered Software; or
|
|
||||||
|
|
||||||
(b) that the Covered Software was made available under the terms of
|
|
||||||
version 1.1 or earlier of the License, but not also under the
|
|
||||||
terms of a Secondary License.
|
|
||||||
|
|
||||||
1.6. "Executable Form"
|
|
||||||
means any form of the work other than Source Code Form.
|
|
||||||
|
|
||||||
1.7. "Larger Work"
|
|
||||||
means a work that combines Covered Software with other material, in
|
|
||||||
a separate file or files, that is not Covered Software.
|
|
||||||
|
|
||||||
1.8. "License"
|
|
||||||
means this document.
|
|
||||||
|
|
||||||
1.9. "Licensable"
|
|
||||||
means having the right to grant, to the maximum extent possible,
|
|
||||||
whether at the time of the initial grant or subsequently, any and
|
|
||||||
all of the rights conveyed by this License.
|
|
||||||
|
|
||||||
1.10. "Modifications"
|
|
||||||
means any of the following:
|
|
||||||
|
|
||||||
(a) any file in Source Code Form that results from an addition to,
|
|
||||||
deletion from, or modification of the contents of Covered
|
|
||||||
Software; or
|
|
||||||
|
|
||||||
(b) any new file in Source Code Form that contains any Covered
|
|
||||||
Software.
|
|
||||||
|
|
||||||
1.11. "Patent Claims" of a Contributor
|
|
||||||
means any patent claim(s), including without limitation, method,
|
|
||||||
process, and apparatus claims, in any patent Licensable by such
|
|
||||||
Contributor that would be infringed, but for the grant of the
|
|
||||||
License, by the making, using, selling, offering for sale, having
|
|
||||||
made, import, or transfer of either its Contributions or its
|
|
||||||
Contributor Version.
|
|
||||||
|
|
||||||
1.12. "Secondary License"
|
|
||||||
means either the GNU General Public License, Version 2.0, the GNU
|
|
||||||
Lesser General Public License, Version 2.1, the GNU Affero General
|
|
||||||
Public License, Version 3.0, or any later versions of those
|
|
||||||
licenses.
|
|
||||||
|
|
||||||
1.13. "Source Code Form"
|
|
||||||
means the form of the work preferred for making modifications.
|
|
||||||
|
|
||||||
1.14. "You" (or "Your")
|
|
||||||
means an individual or a legal entity exercising rights under this
|
|
||||||
License. For legal entities, "You" includes any entity that
|
|
||||||
controls, is controlled by, or is under common control with You. For
|
|
||||||
purposes of this definition, "control" means (a) the power, direct
|
|
||||||
or indirect, to cause the direction or management of such entity,
|
|
||||||
whether by contract or otherwise, or (b) ownership of more than
|
|
||||||
fifty percent (50%) of the outstanding shares or beneficial
|
|
||||||
ownership of such entity.
|
|
||||||
|
|
||||||
2. License Grants and Conditions
|
|
||||||
--------------------------------
|
|
||||||
|
|
||||||
2.1. Grants
|
|
||||||
|
|
||||||
Each Contributor hereby grants You a world-wide, royalty-free,
|
|
||||||
non-exclusive license:
|
|
||||||
|
|
||||||
(a) under intellectual property rights (other than patent or trademark)
|
|
||||||
Licensable by such Contributor to use, reproduce, make available,
|
|
||||||
modify, display, perform, distribute, and otherwise exploit its
|
|
||||||
Contributions, either on an unmodified basis, with Modifications, or
|
|
||||||
as part of a Larger Work; and
|
|
||||||
|
|
||||||
(b) under Patent Claims of such Contributor to make, use, sell, offer
|
|
||||||
for sale, have made, import, and otherwise transfer either its
|
|
||||||
Contributions or its Contributor Version.
|
|
||||||
|
|
||||||
2.2. Effective Date
|
|
||||||
|
|
||||||
The licenses granted in Section 2.1 with respect to any Contribution
|
|
||||||
become effective for each Contribution on the date the Contributor first
|
|
||||||
distributes such Contribution.
|
|
||||||
|
|
||||||
2.3. Limitations on Grant Scope
|
|
||||||
|
|
||||||
The licenses granted in this Section 2 are the only rights granted under
|
|
||||||
this License. No additional rights or licenses will be implied from the
|
|
||||||
distribution or licensing of Covered Software under this License.
|
|
||||||
Notwithstanding Section 2.1(b) above, no patent license is granted by a
|
|
||||||
Contributor:
|
|
||||||
|
|
||||||
(a) for any code that a Contributor has removed from Covered Software;
|
|
||||||
or
|
|
||||||
|
|
||||||
(b) for infringements caused by: (i) Your and any other third party's
|
|
||||||
modifications of Covered Software, or (ii) the combination of its
|
|
||||||
Contributions with other software (except as part of its Contributor
|
|
||||||
Version); or
|
|
||||||
|
|
||||||
(c) under Patent Claims infringed by Covered Software in the absence of
|
|
||||||
its Contributions.
|
|
||||||
|
|
||||||
This License does not grant any rights in the trademarks, service marks,
|
|
||||||
or logos of any Contributor (except as may be necessary to comply with
|
|
||||||
the notice requirements in Section 3.4).
|
|
||||||
|
|
||||||
2.4. Subsequent Licenses
|
|
||||||
|
|
||||||
No Contributor makes additional grants as a result of Your choice to
|
|
||||||
distribute the Covered Software under a subsequent version of this
|
|
||||||
License (see Section 10.2) or under the terms of a Secondary License (if
|
|
||||||
permitted under the terms of Section 3.3).
|
|
||||||
|
|
||||||
2.5. Representation
|
|
||||||
|
|
||||||
Each Contributor represents that the Contributor believes its
|
|
||||||
Contributions are its original creation(s) or it has sufficient rights
|
|
||||||
to grant the rights to its Contributions conveyed by this License.
|
|
||||||
|
|
||||||
2.6. Fair Use
|
|
||||||
|
|
||||||
This License is not intended to limit any rights You have under
|
|
||||||
applicable copyright doctrines of fair use, fair dealing, or other
|
|
||||||
equivalents.
|
|
||||||
|
|
||||||
2.7. Conditions
|
|
||||||
|
|
||||||
Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted
|
|
||||||
in Section 2.1.
|
|
||||||
|
|
||||||
3. Responsibilities
|
|
||||||
-------------------
|
|
||||||
|
|
||||||
3.1. Distribution of Source Form
|
|
||||||
|
|
||||||
All distribution of Covered Software in Source Code Form, including any
|
|
||||||
Modifications that You create or to which You contribute, must be under
|
|
||||||
the terms of this License. You must inform recipients that the Source
|
|
||||||
Code Form of the Covered Software is governed by the terms of this
|
|
||||||
License, and how they can obtain a copy of this License. You may not
|
|
||||||
attempt to alter or restrict the recipients' rights in the Source Code
|
|
||||||
Form.
|
|
||||||
|
|
||||||
3.2. Distribution of Executable Form
|
|
||||||
|
|
||||||
If You distribute Covered Software in Executable Form then:
|
|
||||||
|
|
||||||
(a) such Covered Software must also be made available in Source Code
|
|
||||||
Form, as described in Section 3.1, and You must inform recipients of
|
|
||||||
the Executable Form how they can obtain a copy of such Source Code
|
|
||||||
Form by reasonable means in a timely manner, at a charge no more
|
|
||||||
than the cost of distribution to the recipient; and
|
|
||||||
|
|
||||||
(b) You may distribute such Executable Form under the terms of this
|
|
||||||
License, or sublicense it under different terms, provided that the
|
|
||||||
license for the Executable Form does not attempt to limit or alter
|
|
||||||
the recipients' rights in the Source Code Form under this License.
|
|
||||||
|
|
||||||
3.3. Distribution of a Larger Work
|
|
||||||
|
|
||||||
You may create and distribute a Larger Work under terms of Your choice,
|
|
||||||
provided that You also comply with the requirements of this License for
|
|
||||||
the Covered Software. If the Larger Work is a combination of Covered
|
|
||||||
Software with a work governed by one or more Secondary Licenses, and the
|
|
||||||
Covered Software is not Incompatible With Secondary Licenses, this
|
|
||||||
License permits You to additionally distribute such Covered Software
|
|
||||||
under the terms of such Secondary License(s), so that the recipient of
|
|
||||||
the Larger Work may, at their option, further distribute the Covered
|
|
||||||
Software under the terms of either this License or such Secondary
|
|
||||||
License(s).
|
|
||||||
|
|
||||||
3.4. Notices
|
|
||||||
|
|
||||||
You may not remove or alter the substance of any license notices
|
|
||||||
(including copyright notices, patent notices, disclaimers of warranty,
|
|
||||||
or limitations of liability) contained within the Source Code Form of
|
|
||||||
the Covered Software, except that You may alter any license notices to
|
|
||||||
the extent required to remedy known factual inaccuracies.
|
|
||||||
|
|
||||||
3.5. Application of Additional Terms
|
|
||||||
|
|
||||||
You may choose to offer, and to charge a fee for, warranty, support,
|
|
||||||
indemnity or liability obligations to one or more recipients of Covered
|
|
||||||
Software. However, You may do so only on Your own behalf, and not on
|
|
||||||
behalf of any Contributor. You must make it absolutely clear that any
|
|
||||||
such warranty, support, indemnity, or liability obligation is offered by
|
|
||||||
You alone, and You hereby agree to indemnify every Contributor for any
|
|
||||||
liability incurred by such Contributor as a result of warranty, support,
|
|
||||||
indemnity or liability terms You offer. You may include additional
|
|
||||||
disclaimers of warranty and limitations of liability specific to any
|
|
||||||
jurisdiction.
|
|
||||||
|
|
||||||
4. Inability to Comply Due to Statute or Regulation
|
|
||||||
---------------------------------------------------
|
|
||||||
|
|
||||||
If it is impossible for You to comply with any of the terms of this
|
|
||||||
License with respect to some or all of the Covered Software due to
|
|
||||||
statute, judicial order, or regulation then You must: (a) comply with
|
|
||||||
the terms of this License to the maximum extent possible; and (b)
|
|
||||||
describe the limitations and the code they affect. Such description must
|
|
||||||
be placed in a text file included with all distributions of the Covered
|
|
||||||
Software under this License. Except to the extent prohibited by statute
|
|
||||||
or regulation, such description must be sufficiently detailed for a
|
|
||||||
recipient of ordinary skill to be able to understand it.
|
|
||||||
|
|
||||||
5. Termination
|
|
||||||
--------------
|
|
||||||
|
|
||||||
5.1. The rights granted under this License will terminate automatically
|
|
||||||
if You fail to comply with any of its terms. However, if You become
|
|
||||||
compliant, then the rights granted under this License from a particular
|
|
||||||
Contributor are reinstated (a) provisionally, unless and until such
|
|
||||||
Contributor explicitly and finally terminates Your grants, and (b) on an
|
|
||||||
ongoing basis, if such Contributor fails to notify You of the
|
|
||||||
non-compliance by some reasonable means prior to 60 days after You have
|
|
||||||
come back into compliance. Moreover, Your grants from a particular
|
|
||||||
Contributor are reinstated on an ongoing basis if such Contributor
|
|
||||||
notifies You of the non-compliance by some reasonable means, this is the
|
|
||||||
first time You have received notice of non-compliance with this License
|
|
||||||
from such Contributor, and You become compliant prior to 30 days after
|
|
||||||
Your receipt of the notice.
|
|
||||||
|
|
||||||
5.2. If You initiate litigation against any entity by asserting a patent
|
|
||||||
infringement claim (excluding declaratory judgment actions,
|
|
||||||
counter-claims, and cross-claims) alleging that a Contributor Version
|
|
||||||
directly or indirectly infringes any patent, then the rights granted to
|
|
||||||
You by any and all Contributors for the Covered Software under Section
|
|
||||||
2.1 of this License shall terminate.
|
|
||||||
|
|
||||||
5.3. In the event of termination under Sections 5.1 or 5.2 above, all
|
|
||||||
end user license agreements (excluding distributors and resellers) which
|
|
||||||
have been validly granted by You or Your distributors under this License
|
|
||||||
prior to termination shall survive termination.
|
|
||||||
|
|
||||||
************************************************************************
|
|
||||||
* *
|
|
||||||
* 6. Disclaimer of Warranty *
|
|
||||||
* ------------------------- *
|
|
||||||
* *
|
|
||||||
* Covered Software is provided under this License on an "as is" *
|
|
||||||
* basis, without warranty of any kind, either expressed, implied, or *
|
|
||||||
* statutory, including, without limitation, warranties that the *
|
|
||||||
* Covered Software is free of defects, merchantable, fit for a *
|
|
||||||
* particular purpose or non-infringing. The entire risk as to the *
|
|
||||||
* quality and performance of the Covered Software is with You. *
|
|
||||||
* Should any Covered Software prove defective in any respect, You *
|
|
||||||
* (not any Contributor) assume the cost of any necessary servicing, *
|
|
||||||
* repair, or correction. This disclaimer of warranty constitutes an *
|
|
||||||
* essential part of this License. No use of any Covered Software is *
|
|
||||||
* authorized under this License except under this disclaimer. *
|
|
||||||
* *
|
|
||||||
************************************************************************
|
|
||||||
|
|
||||||
************************************************************************
|
|
||||||
* *
|
|
||||||
* 7. Limitation of Liability *
|
|
||||||
* -------------------------- *
|
|
||||||
* *
|
|
||||||
* Under no circumstances and under no legal theory, whether tort *
|
|
||||||
* (including negligence), contract, or otherwise, shall any *
|
|
||||||
* Contributor, or anyone who distributes Covered Software as *
|
|
||||||
* permitted above, be liable to You for any direct, indirect, *
|
|
||||||
* special, incidental, or consequential damages of any character *
|
|
||||||
* including, without limitation, damages for lost profits, loss of *
|
|
||||||
* goodwill, work stoppage, computer failure or malfunction, or any *
|
|
||||||
* and all other commercial damages or losses, even if such party *
|
|
||||||
* shall have been informed of the possibility of such damages. This *
|
|
||||||
* limitation of liability shall not apply to liability for death or *
|
|
||||||
* personal injury resulting from such party's negligence to the *
|
|
||||||
* extent applicable law prohibits such limitation. Some *
|
|
||||||
* jurisdictions do not allow the exclusion or limitation of *
|
|
||||||
* incidental or consequential damages, so this exclusion and *
|
|
||||||
* limitation may not apply to You. *
|
|
||||||
* *
|
|
||||||
************************************************************************
|
|
||||||
|
|
||||||
8. Litigation
|
|
||||||
-------------
|
|
||||||
|
|
||||||
Any litigation relating to this License may be brought only in the
|
|
||||||
courts of a jurisdiction where the defendant maintains its principal
|
|
||||||
place of business and such litigation shall be governed by laws of that
|
|
||||||
jurisdiction, without reference to its conflict-of-law provisions.
|
|
||||||
Nothing in this Section shall prevent a party's ability to bring
|
|
||||||
cross-claims or counter-claims.
|
|
||||||
|
|
||||||
9. Miscellaneous
|
|
||||||
----------------
|
|
||||||
|
|
||||||
This License represents the complete agreement concerning the subject
|
|
||||||
matter hereof. If any provision of this License is held to be
|
|
||||||
unenforceable, such provision shall be reformed only to the extent
|
|
||||||
necessary to make it enforceable. Any law or regulation which provides
|
|
||||||
that the language of a contract shall be construed against the drafter
|
|
||||||
shall not be used to construe this License against a Contributor.
|
|
||||||
|
|
||||||
10. Versions of the License
|
|
||||||
---------------------------
|
|
||||||
|
|
||||||
10.1. New Versions
|
|
||||||
|
|
||||||
Mozilla Foundation is the license steward. Except as provided in Section
|
|
||||||
10.3, no one other than the license steward has the right to modify or
|
|
||||||
publish new versions of this License. Each version will be given a
|
|
||||||
distinguishing version number.
|
|
||||||
|
|
||||||
10.2. Effect of New Versions
|
|
||||||
|
|
||||||
You may distribute the Covered Software under the terms of the version
|
|
||||||
of the License under which You originally received the Covered Software,
|
|
||||||
or under the terms of any subsequent version published by the license
|
|
||||||
steward.
|
|
||||||
|
|
||||||
10.3. Modified Versions
|
|
||||||
|
|
||||||
If you create software not governed by this License, and you want to
|
|
||||||
create a new license for such software, you may create and use a
|
|
||||||
modified version of this License if you rename the license and remove
|
|
||||||
any references to the name of the license steward (except to note that
|
|
||||||
such modified license differs from this License).
|
|
||||||
|
|
||||||
10.4. Distributing Source Code Form that is Incompatible With Secondary
|
|
||||||
Licenses
|
|
||||||
|
|
||||||
If You choose to distribute Source Code Form that is Incompatible With
|
|
||||||
Secondary Licenses under the terms of this version of the License, the
|
|
||||||
notice described in Exhibit B of this License must be attached.
|
|
||||||
|
|
||||||
Exhibit A - Source Code Form License Notice
|
|
||||||
-------------------------------------------
|
|
||||||
|
|
||||||
This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
file, You can obtain one at http://mozilla.org/MPL/2.0/.
|
|
||||||
|
|
||||||
If it is not possible or desirable to put the notice in a particular
|
|
||||||
file, then You may include the notice in a location (such as a LICENSE
|
|
||||||
file in a relevant directory) where a recipient would be likely to look
|
|
||||||
for such a notice.
|
|
||||||
|
|
||||||
You may add additional accurate notices of copyright ownership.
|
|
||||||
|
|
||||||
Exhibit B - "Incompatible With Secondary Licenses" Notice
|
|
||||||
---------------------------------------------------------
|
|
||||||
|
|
||||||
This Source Code Form is "Incompatible With Secondary Licenses", as
|
|
||||||
defined by the Mozilla Public License, v. 2.0.
|
|
||||||
|
|
@ -1,187 +0,0 @@
|
||||||
# *Design By Contract* for Rust
|
|
||||||
|
|
||||||
[![License][license]][LICENSE]
|
|
||||||
![Build status][build]
|
|
||||||
![Lines of Code][loc]
|
|
||||||
|
|
||||||
[license]: https://img.shields.io/badge/license-MPL%202.0-blue.svg
|
|
||||||
[build]: https://gitlab.com/karroffel/contracts/badges/master/pipeline.svg
|
|
||||||
[loc]: https://tokei.rs/b1/gitlab/karroffel/contracts?category=code
|
|
||||||
|
|
||||||
Annotate functions and methods with "contracts", using *invariants*,
|
|
||||||
*pre-conditions* and *post-conditions*.
|
|
||||||
|
|
||||||
[Design by contract][dbc] is a popular method to augment code with formal
|
|
||||||
interface specifications.
|
|
||||||
These specifications are used to increase the correctness of the code by
|
|
||||||
checking them as assertions at runtime.
|
|
||||||
|
|
||||||
[dbc]: https://en.wikipedia.org/wiki/Design_by_contract
|
|
||||||
|
|
||||||
```rust
|
|
||||||
pub struct Library {
|
|
||||||
available: HashSet<String>,
|
|
||||||
lent: HashSet<String>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Library {
|
|
||||||
fn book_exists(&self, book_id: &str) -> bool {
|
|
||||||
self.available.contains(book_id)
|
|
||||||
|| self.lent.contains(book_id)
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
|
|
||||||
#[debug_ensures(self.available.contains(book_id), "Book now available")]
|
|
||||||
#[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
#[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
|
|
||||||
pub fn add_book(&mut self, book_id: &str) {
|
|
||||||
self.available.insert(book_id.to_string());
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(self.book_exists(book_id))]
|
|
||||||
#[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
|
|
||||||
#[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
|
|
||||||
#[debug_ensures(ret -> self.lent.contains(book_id))]
|
|
||||||
#[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
|
|
||||||
pub fn lend(&mut self, book_id: &str) -> bool {
|
|
||||||
if self.available.contains(book_id) {
|
|
||||||
self.available.remove(book_id);
|
|
||||||
self.lent.insert(book_id.to_string());
|
|
||||||
true
|
|
||||||
} else {
|
|
||||||
false
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
|
|
||||||
#[ensures(self.lent.len() == old(self.lent.len()) - 1)]
|
|
||||||
#[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
#[debug_ensures(!self.lent.contains(book_id))]
|
|
||||||
#[debug_ensures(self.available.contains(book_id), "Book available again")]
|
|
||||||
pub fn return_book(&mut self, book_id: &str) {
|
|
||||||
self.lent.remove(book_id);
|
|
||||||
self.available.insert(book_id.to_string());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
## Attributes
|
|
||||||
|
|
||||||
This crate exposes the `requires`, `ensures` and `invariant` attributes.
|
|
||||||
|
|
||||||
- `requires` are checked before a function/method is executed.
|
|
||||||
- `ensures` are checked after a function/method ran to completion
|
|
||||||
- `invariant`s are checked both before *and* after a function/method ran.
|
|
||||||
|
|
||||||
Additionally, all those attributes have versions with different "modes". See
|
|
||||||
[the Modes section](#Modes) below.
|
|
||||||
|
|
||||||
For `trait`s and trait `impl`s the `contract_trait` attribute can be used.
|
|
||||||
|
|
||||||
More specific information can be found in the crate documentation.
|
|
||||||
|
|
||||||
## Pseudo-functions and operators
|
|
||||||
|
|
||||||
### `old()` function
|
|
||||||
|
|
||||||
One unique feature that this crate provides is an `old()` pseudo-function which
|
|
||||||
allows to perform checks using a value of a parameter before the function call
|
|
||||||
happened. This is only available in `ensures` attributes.
|
|
||||||
|
|
||||||
```rust
|
|
||||||
#[ensures(*x == old(*x) + 1, "after the call `x` was incremented")]
|
|
||||||
fn incr(x: &mut usize) {
|
|
||||||
*x += 1;
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
### `->` operator
|
|
||||||
|
|
||||||
For more complex functions it can be useful to express behaviour using logical
|
|
||||||
implication. Because Rust does not feature an operator for implication, this
|
|
||||||
crate adds this operator for use in attributes.
|
|
||||||
|
|
||||||
```rust
|
|
||||||
#[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
|
|
||||||
fn geeting(person_name: Option<&str>) -> String {
|
|
||||||
let mut s = String::from("Hello");
|
|
||||||
if let Some(name) = person_name {
|
|
||||||
s.push(' ');
|
|
||||||
s.push_str(name);
|
|
||||||
}
|
|
||||||
s.push('!');
|
|
||||||
s
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
This operator is right-associative.
|
|
||||||
|
|
||||||
**Note**: Because of the design of `syn`, it is tricky to add custom operators
|
|
||||||
to be parsed, so this crate performs a rewrite of the `TokenStream` instead.
|
|
||||||
The rewrite works by separating the expression into a part that's left of the
|
|
||||||
`->` operator and the rest on the right side. This means that
|
|
||||||
`if a -> b { c } else { d }` will not generate the expected code.
|
|
||||||
Explicit grouping using parenthesis or curly-brackets can be used to avoid this.
|
|
||||||
|
|
||||||
|
|
||||||
## Modes
|
|
||||||
|
|
||||||
All the attributes (requires, ensures, invariant) have `debug_*` and `test_*` versions.
|
|
||||||
|
|
||||||
- `debug_requires`/`debug_ensures`/`debug_invariant` use `debug_assert!`
|
|
||||||
internally rather than `assert!`
|
|
||||||
- `test_requires`/`test_ensures`/`test_invariant` guard the `assert!` with an
|
|
||||||
`if cfg!(test)`.
|
|
||||||
This should mostly be used for stating equivalence to "slow but obviously
|
|
||||||
correct" alternative implementations or checks.
|
|
||||||
|
|
||||||
For example, a merge-sort implementation might look like this
|
|
||||||
```rust
|
|
||||||
#[test_ensures(is_sorted(input))]
|
|
||||||
fn merge_sort<T: Ord + Copy>(input: &mut [T]) {
|
|
||||||
// ...
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
## Set-up
|
|
||||||
|
|
||||||
To install the latest version, add `contracts` to the dependency section of the
|
|
||||||
`Cargo.toml` file.
|
|
||||||
|
|
||||||
```
|
|
||||||
[dependencies]
|
|
||||||
contracts = "0.6.3"
|
|
||||||
```
|
|
||||||
|
|
||||||
To then bring all procedural macros into scope, you can add `use contracts::*;`
|
|
||||||
in all files you plan to use the contract attributes.
|
|
||||||
|
|
||||||
Alternatively use the "old-style" of importing macros to have them available
|
|
||||||
project-wide.
|
|
||||||
|
|
||||||
```rust
|
|
||||||
#[macro_use]
|
|
||||||
extern crate contracts;
|
|
||||||
```
|
|
||||||
|
|
||||||
## Configuration
|
|
||||||
|
|
||||||
This crate exposes a number of feature flags to configure the assertion behavior.
|
|
||||||
|
|
||||||
- `disable_contracts` - disables all checks and assertions.
|
|
||||||
- `override_debug` - changes all contracts (except `test_` ones) into `debug_*`
|
|
||||||
versions
|
|
||||||
- `override_log` - changes all contracts (except `test_` ones) into a
|
|
||||||
`log::error!()` call if the condition is violated.
|
|
||||||
No abortion happens.
|
|
||||||
- `mirai_assertions` - instead of regular assert! style macros, emit macros
|
|
||||||
used by the [MIRAI] static analyzer. For more documentation of this usage,
|
|
||||||
head to the [MIRAI] repo.
|
|
||||||
|
|
||||||
[MIRAI]: https://github.com/facebookexperimental/MIRAI
|
|
||||||
|
|
||||||
## TODOs
|
|
||||||
|
|
||||||
- implement more contracts for traits.
|
|
||||||
- add a static analyzer à la SPARK for whole-projects using the contracts to
|
|
||||||
make static assertions.
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
# Things to check/change before pushing a release
|
|
||||||
|
|
||||||
1. Run all the tests with `cargo test --all`
|
|
||||||
2. Run `cargo run --example library` to make sure the examples still run properly
|
|
||||||
3. Run `cargo fmt`
|
|
||||||
4. Change version numbers
|
|
||||||
- inside `README.md` in the "Set-up" section
|
|
||||||
- inside `Cargo.toml`
|
|
||||||
5. Write or finish entry in `CHANGELOG.md`
|
|
||||||
6. Run `cargo doc --open` and check if the documentation looks fine and is up to date
|
|
||||||
7. Run `cargo package` and check the output for any unwanted or missing files
|
|
||||||
8. Run `cargo publish` to upload to crates.io
|
|
||||||
|
|
@ -1,73 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
use std::collections::HashSet;
|
|
||||||
|
|
||||||
pub struct Library {
|
|
||||||
available: HashSet<String>,
|
|
||||||
lent: HashSet<String>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Library {
|
|
||||||
fn book_exists(&self, book_id: &str) -> bool {
|
|
||||||
self.available.contains(book_id) || self.lent.contains(book_id)
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
|
|
||||||
#[debug_ensures(self.available.contains(book_id), "Book now available")]
|
|
||||||
#[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
#[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
|
|
||||||
pub fn add_book(&mut self, book_id: &str) {
|
|
||||||
self.available.insert(book_id.to_string());
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(self.book_exists(book_id))]
|
|
||||||
#[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
|
|
||||||
#[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
|
|
||||||
#[debug_ensures(ret -> self.lent.contains(book_id))]
|
|
||||||
#[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
|
|
||||||
pub fn lend(&mut self, book_id: &str) -> bool {
|
|
||||||
if self.available.contains(book_id) {
|
|
||||||
self.available.remove(book_id);
|
|
||||||
self.lent.insert(book_id.to_string());
|
|
||||||
true
|
|
||||||
} else {
|
|
||||||
false
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
|
|
||||||
#[ensures(self.lent.len() == old(self.lent.len()) - 1)]
|
|
||||||
#[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
#[debug_ensures(!self.lent.contains(book_id))]
|
|
||||||
#[debug_ensures(self.available.contains(book_id), "Book available again")]
|
|
||||||
pub fn return_book(&mut self, book_id: &str) {
|
|
||||||
self.lent.remove(book_id);
|
|
||||||
self.available.insert(book_id.to_string());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn main() {
|
|
||||||
let mut lib = Library {
|
|
||||||
available: HashSet::new(),
|
|
||||||
lent: HashSet::new(),
|
|
||||||
};
|
|
||||||
|
|
||||||
lib.add_book("Das Kapital");
|
|
||||||
println!("Adding a book.");
|
|
||||||
|
|
||||||
let lent_successful = lib.lend("Das Kapital");
|
|
||||||
assert!(lent_successful);
|
|
||||||
|
|
||||||
if lent_successful {
|
|
||||||
println!("Lent out the book.");
|
|
||||||
println!("Reading for a bit...");
|
|
||||||
|
|
||||||
println!("Giving back the book.");
|
|
||||||
|
|
||||||
lib.return_book("Das Kapital");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
max_width = 80
|
|
||||||
|
|
@ -1,423 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use proc_macro2::{Ident, Span, TokenStream};
|
|
||||||
use quote::ToTokens;
|
|
||||||
use syn::{
|
|
||||||
spanned::Spanned, visit_mut as visitor, Attribute, Expr, ExprCall, ExprTry,
|
|
||||||
ReturnType, TypeImplTrait,
|
|
||||||
};
|
|
||||||
|
|
||||||
use crate::implementation::{
|
|
||||||
Contract, ContractMode, ContractType, FuncWithContracts,
|
|
||||||
};
|
|
||||||
|
|
||||||
/// Substitution for `old()` expressions.
|
|
||||||
pub(crate) struct OldExpr {
|
|
||||||
/// Name of the variable binder.
|
|
||||||
pub(crate) name: String,
|
|
||||||
/// Expression to be evaluated.
|
|
||||||
pub(crate) expr: Expr,
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Extract calls to the pseudo-function `old()` in post-conditions,
|
|
||||||
/// which evaluates an expression in a context *before* the
|
|
||||||
/// to-be-checked-function is executed.
|
|
||||||
pub(crate) fn extract_old_calls(contracts: &mut [Contract]) -> Vec<OldExpr> {
|
|
||||||
struct OldExtractor {
|
|
||||||
last_id: usize,
|
|
||||||
olds: Vec<OldExpr>,
|
|
||||||
}
|
|
||||||
|
|
||||||
// if the call is a call to old() then the argument will be
|
|
||||||
// returned.
|
|
||||||
fn get_old_data(call: &ExprCall) -> Option<Expr> {
|
|
||||||
// must have only one argument
|
|
||||||
if call.args.len() != 1 {
|
|
||||||
return None;
|
|
||||||
}
|
|
||||||
|
|
||||||
if let Expr::Path(path) = &*call.func {
|
|
||||||
if path.path.is_ident("old") {
|
|
||||||
Some(call.args[0].clone())
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl visitor::VisitMut for OldExtractor {
|
|
||||||
fn visit_expr_mut(&mut self, expr: &mut Expr) {
|
|
||||||
if let Expr::Call(call) = expr {
|
|
||||||
if let Some(mut old_arg) = get_old_data(call) {
|
|
||||||
// if it's a call to old() then add to list of
|
|
||||||
// old expressions and continue to check the
|
|
||||||
// argument.
|
|
||||||
|
|
||||||
self.visit_expr_mut(&mut old_arg);
|
|
||||||
|
|
||||||
let id = self.last_id;
|
|
||||||
self.last_id += 1;
|
|
||||||
|
|
||||||
let old_var_name = format!("__contract_old_{}", id);
|
|
||||||
|
|
||||||
let old_expr = OldExpr {
|
|
||||||
name: old_var_name.clone(),
|
|
||||||
expr: old_arg,
|
|
||||||
};
|
|
||||||
|
|
||||||
self.olds.push(old_expr);
|
|
||||||
|
|
||||||
// override the original expression with the new variable
|
|
||||||
// identifier
|
|
||||||
*expr = {
|
|
||||||
let span = expr.span();
|
|
||||||
|
|
||||||
let ident = syn::Ident::new(&old_var_name, span);
|
|
||||||
|
|
||||||
let toks = quote::quote_spanned! { span=> #ident };
|
|
||||||
|
|
||||||
syn::parse(toks.into()).unwrap()
|
|
||||||
};
|
|
||||||
} else {
|
|
||||||
// otherwise continue visiting the expression call
|
|
||||||
visitor::visit_expr_call_mut(self, call);
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
visitor::visit_expr_mut(self, expr);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut extractor = OldExtractor {
|
|
||||||
last_id: 0,
|
|
||||||
olds: vec![],
|
|
||||||
};
|
|
||||||
|
|
||||||
for contract in contracts {
|
|
||||||
if contract.ty != ContractType::Ensures {
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
for assertion in &mut contract.assertions {
|
|
||||||
use visitor::VisitMut;
|
|
||||||
extractor.visit_expr_mut(assertion);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
extractor.olds
|
|
||||||
}
|
|
||||||
|
|
||||||
fn get_assert_macro(
|
|
||||||
ctype: ContractType, // only Pre/Post allowed.
|
|
||||||
mode: ContractMode,
|
|
||||||
span: Span,
|
|
||||||
) -> Option<Ident> {
|
|
||||||
if cfg!(feature = "mirai_assertions") {
|
|
||||||
match (ctype, mode) {
|
|
||||||
(ContractType::Requires, ContractMode::Always) => {
|
|
||||||
Some(Ident::new("checked_precondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Requires, ContractMode::Debug) => {
|
|
||||||
Some(Ident::new("debug_checked_precondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Requires, ContractMode::Test) => {
|
|
||||||
Some(Ident::new("debug_checked_precondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Requires, ContractMode::Disabled) => {
|
|
||||||
Some(Ident::new("precondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Requires, ContractMode::LogOnly) => {
|
|
||||||
Some(Ident::new("precondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Ensures, ContractMode::Always) => {
|
|
||||||
Some(Ident::new("checked_postcondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Ensures, ContractMode::Debug) => {
|
|
||||||
Some(Ident::new("debug_checked_postcondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Ensures, ContractMode::Test) => {
|
|
||||||
Some(Ident::new("debug_checked_postcondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Ensures, ContractMode::Disabled) => {
|
|
||||||
Some(Ident::new("postcondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Ensures, ContractMode::LogOnly) => {
|
|
||||||
Some(Ident::new("postcondition", span))
|
|
||||||
}
|
|
||||||
(ContractType::Invariant, _) => {
|
|
||||||
panic!("expected Invariant to be narrowed down to Pre/Post")
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
match mode {
|
|
||||||
ContractMode::Always => Some(Ident::new("assert", span)),
|
|
||||||
ContractMode::Debug => Some(Ident::new("debug_assert", span)),
|
|
||||||
ContractMode::Test => Some(Ident::new("debug_assert", span)),
|
|
||||||
ContractMode::Disabled => None,
|
|
||||||
ContractMode::LogOnly => None,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Generate the resulting code for this function by inserting assertions.
|
|
||||||
pub(crate) fn generate(
|
|
||||||
mut func: FuncWithContracts,
|
|
||||||
docs: Vec<Attribute>,
|
|
||||||
olds: Vec<OldExpr>,
|
|
||||||
) -> TokenStream {
|
|
||||||
let func_name = func.function.sig.ident.to_string();
|
|
||||||
|
|
||||||
// creates an assertion appropriate for the current mode
|
|
||||||
let make_assertion = |mode: ContractMode,
|
|
||||||
ctype: ContractType,
|
|
||||||
display: proc_macro2::TokenStream,
|
|
||||||
exec_expr: &Expr,
|
|
||||||
desc: &str| {
|
|
||||||
let span = display.span();
|
|
||||||
let mut result = proc_macro2::TokenStream::new();
|
|
||||||
|
|
||||||
let format_args = quote::quote_spanned! { span=>
|
|
||||||
concat!(concat!(#desc, ": "), stringify!(#display))
|
|
||||||
};
|
|
||||||
|
|
||||||
if mode == ContractMode::LogOnly {
|
|
||||||
result.extend(
|
|
||||||
quote::quote_spanned! { span=>
|
|
||||||
if !(#exec_expr) {
|
|
||||||
log::error!("{}", #format_args);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
.into_iter(),
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
if let Some(assert_macro) = get_assert_macro(ctype, mode, span) {
|
|
||||||
result.extend(
|
|
||||||
quote::quote_spanned! { span=>
|
|
||||||
#assert_macro!(#exec_expr, "{}", #format_args);
|
|
||||||
}
|
|
||||||
.into_iter(),
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
if mode == ContractMode::Test {
|
|
||||||
quote::quote_spanned! { span=>
|
|
||||||
#[cfg(test)] {
|
|
||||||
#result
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
result
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
//
|
|
||||||
// generate assertion code for pre-conditions
|
|
||||||
//
|
|
||||||
|
|
||||||
let pre: proc_macro2::TokenStream = func
|
|
||||||
.contracts
|
|
||||||
.iter()
|
|
||||||
.filter(|c| {
|
|
||||||
c.ty == ContractType::Requires || c.ty == ContractType::Invariant
|
|
||||||
})
|
|
||||||
.flat_map(|c| {
|
|
||||||
let contract_type_name = if c.ty == ContractType::Invariant {
|
|
||||||
format!("{} (as pre-condition)", c.ty.message_name())
|
|
||||||
} else {
|
|
||||||
format!("{}", c.ty.message_name())
|
|
||||||
};
|
|
||||||
|
|
||||||
let desc = if let Some(desc) = c.desc.as_ref() {
|
|
||||||
format!(
|
|
||||||
"{} of {} violated: {}",
|
|
||||||
contract_type_name, func_name, desc
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
format!("{} of {} violated", contract_type_name, func_name)
|
|
||||||
};
|
|
||||||
|
|
||||||
c.assertions.iter().zip(c.streams.iter()).map(
|
|
||||||
move |(expr, display)| {
|
|
||||||
let mode = c.mode.final_mode();
|
|
||||||
|
|
||||||
make_assertion(
|
|
||||||
mode,
|
|
||||||
ContractType::Requires,
|
|
||||||
display.clone(),
|
|
||||||
expr,
|
|
||||||
&desc.clone(),
|
|
||||||
)
|
|
||||||
},
|
|
||||||
)
|
|
||||||
})
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
//
|
|
||||||
// generate assertion code for post-conditions
|
|
||||||
//
|
|
||||||
|
|
||||||
let post: proc_macro2::TokenStream = func
|
|
||||||
.contracts
|
|
||||||
.iter()
|
|
||||||
.filter(|c| {
|
|
||||||
c.ty == ContractType::Ensures || c.ty == ContractType::Invariant
|
|
||||||
})
|
|
||||||
.flat_map(|c| {
|
|
||||||
let contract_type_name = if c.ty == ContractType::Invariant {
|
|
||||||
format!("{} (as post-condition)", c.ty.message_name())
|
|
||||||
} else {
|
|
||||||
format!("{}", c.ty.message_name())
|
|
||||||
};
|
|
||||||
|
|
||||||
let desc = if let Some(desc) = c.desc.as_ref() {
|
|
||||||
format!(
|
|
||||||
"{} of {} violated: {}",
|
|
||||||
contract_type_name, func_name, desc
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
format!("{} of {} violated", contract_type_name, func_name)
|
|
||||||
};
|
|
||||||
|
|
||||||
c.assertions.iter().zip(c.streams.iter()).map(
|
|
||||||
move |(expr, display)| {
|
|
||||||
let mode = c.mode.final_mode();
|
|
||||||
|
|
||||||
make_assertion(
|
|
||||||
mode,
|
|
||||||
ContractType::Ensures,
|
|
||||||
display.clone(),
|
|
||||||
expr,
|
|
||||||
&desc.clone(),
|
|
||||||
)
|
|
||||||
},
|
|
||||||
)
|
|
||||||
})
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
//
|
|
||||||
// bind "old()" expressions
|
|
||||||
//
|
|
||||||
|
|
||||||
let olds = {
|
|
||||||
let mut toks = proc_macro2::TokenStream::new();
|
|
||||||
|
|
||||||
for old in olds {
|
|
||||||
let span = old.expr.span();
|
|
||||||
|
|
||||||
let name = syn::Ident::new(&old.name, span);
|
|
||||||
|
|
||||||
let expr = old.expr;
|
|
||||||
|
|
||||||
let binding = quote::quote_spanned! { span=>
|
|
||||||
let #name = #expr;
|
|
||||||
};
|
|
||||||
|
|
||||||
toks.extend(Some(binding));
|
|
||||||
}
|
|
||||||
|
|
||||||
toks
|
|
||||||
};
|
|
||||||
|
|
||||||
//
|
|
||||||
// wrap the function body in a block so that we can use its return value
|
|
||||||
//
|
|
||||||
|
|
||||||
let body = 'blk: {
|
|
||||||
let mut block = func.function.block.clone();
|
|
||||||
syn::visit_mut::visit_block_mut(&mut ReturnReplacer, &mut block);
|
|
||||||
|
|
||||||
let mut impl_detector = ImplDetector { found_impl: false };
|
|
||||||
syn::visit::visit_return_type(
|
|
||||||
&mut impl_detector,
|
|
||||||
&func.function.sig.output,
|
|
||||||
);
|
|
||||||
|
|
||||||
if !impl_detector.found_impl {
|
|
||||||
if let ReturnType::Type(.., ref return_type) =
|
|
||||||
func.function.sig.output
|
|
||||||
{
|
|
||||||
let mut try_detector = TryDetector { found_try: false };
|
|
||||||
syn::visit::visit_block(&mut try_detector, &mut block);
|
|
||||||
|
|
||||||
if try_detector.found_try {
|
|
||||||
break 'blk quote::quote! { let ret: #return_type = 'run: { try {
|
|
||||||
let ret2: #return_type = #block;
|
|
||||||
ret2?
|
|
||||||
} }; };
|
|
||||||
} else {
|
|
||||||
break 'blk quote::quote! { let ret: #return_type = 'run: #block; };
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
quote::quote! { let ret = 'run: #block; }
|
|
||||||
};
|
|
||||||
|
|
||||||
//
|
|
||||||
// create a new function body containing all assertions
|
|
||||||
//
|
|
||||||
|
|
||||||
let new_block = quote::quote! {
|
|
||||||
|
|
||||||
{
|
|
||||||
#pre
|
|
||||||
|
|
||||||
#olds
|
|
||||||
|
|
||||||
#body
|
|
||||||
|
|
||||||
#post
|
|
||||||
|
|
||||||
ret
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
// insert documentation attributes
|
|
||||||
|
|
||||||
func.function.attrs.extend(docs);
|
|
||||||
|
|
||||||
// replace the old function body with the new one
|
|
||||||
|
|
||||||
func.function.block = Box::new(syn::parse_quote!(#new_block));
|
|
||||||
|
|
||||||
func.function.into_token_stream()
|
|
||||||
}
|
|
||||||
|
|
||||||
struct ReturnReplacer;
|
|
||||||
|
|
||||||
impl syn::visit_mut::VisitMut for ReturnReplacer {
|
|
||||||
fn visit_expr_mut(&mut self, node: &mut Expr) {
|
|
||||||
if let Expr::Return(ret_expr) = node {
|
|
||||||
let ret_expr_expr = ret_expr.expr.clone();
|
|
||||||
*node = syn::parse_quote!(break 'run #ret_expr_expr);
|
|
||||||
}
|
|
||||||
|
|
||||||
syn::visit_mut::visit_expr_mut(self, node);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
struct ImplDetector {
|
|
||||||
found_impl: bool,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a> syn::visit::Visit<'a> for ImplDetector {
|
|
||||||
fn visit_type_impl_trait(&mut self, _node: &'a TypeImplTrait) {
|
|
||||||
self.found_impl = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
struct TryDetector {
|
|
||||||
found_try: bool,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a> syn::visit::Visit<'a> for TryDetector {
|
|
||||||
fn visit_expr_try(&mut self, _node: &'a ExprTry) {
|
|
||||||
self.found_try = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,88 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use crate::implementation::{Contract, ContractMode};
|
|
||||||
use proc_macro2::Span;
|
|
||||||
use proc_macro2::TokenStream;
|
|
||||||
use syn::{parse::Parser, Attribute};
|
|
||||||
|
|
||||||
pub(crate) fn generate_attributes(contracts: &[Contract]) -> Vec<Attribute> {
|
|
||||||
let mut attrs = vec![];
|
|
||||||
|
|
||||||
fn make_attribute(content: &str) -> Attribute {
|
|
||||||
let span = Span::call_site();
|
|
||||||
|
|
||||||
let content_str = syn::LitStr::new(content, span);
|
|
||||||
|
|
||||||
let toks: TokenStream =
|
|
||||||
quote::quote_spanned!( span=> #[doc = #content_str] );
|
|
||||||
|
|
||||||
let parser = Attribute::parse_outer;
|
|
||||||
|
|
||||||
let mut attributes = parser.parse2(toks).unwrap();
|
|
||||||
|
|
||||||
attributes.remove(0)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn print_stream(stream: &TokenStream) -> String {
|
|
||||||
stream.to_string()
|
|
||||||
}
|
|
||||||
|
|
||||||
// header
|
|
||||||
attrs.push(make_attribute("# Contracts"));
|
|
||||||
|
|
||||||
for contract in contracts {
|
|
||||||
let ty = contract.ty;
|
|
||||||
let mode = match contract.mode {
|
|
||||||
ContractMode::Always => None,
|
|
||||||
ContractMode::Disabled => None,
|
|
||||||
ContractMode::Debug => Some("debug"),
|
|
||||||
ContractMode::Test => Some("test"),
|
|
||||||
ContractMode::LogOnly => None,
|
|
||||||
};
|
|
||||||
|
|
||||||
if let Some(desc) = &contract.desc {
|
|
||||||
// document all assertions under the description
|
|
||||||
|
|
||||||
let header_txt = if let Some(name) = mode {
|
|
||||||
format!("{} - {}: {}", ty.message_name(), name, desc)
|
|
||||||
} else {
|
|
||||||
format!("{}: {}", ty.message_name(), desc)
|
|
||||||
};
|
|
||||||
|
|
||||||
attrs.push(make_attribute(&header_txt));
|
|
||||||
|
|
||||||
for (_assert, stream) in
|
|
||||||
contract.assertions.iter().zip(contract.streams.iter())
|
|
||||||
{
|
|
||||||
attrs.push(make_attribute(&format!(
|
|
||||||
" - `{}`",
|
|
||||||
print_stream(stream)
|
|
||||||
)));
|
|
||||||
}
|
|
||||||
|
|
||||||
attrs.push(make_attribute(""));
|
|
||||||
} else {
|
|
||||||
// document each assertion on its own
|
|
||||||
|
|
||||||
for stream in &contract.streams {
|
|
||||||
let doc_str = if let Some(name) = mode {
|
|
||||||
format!(
|
|
||||||
"{} - {}: `{}`",
|
|
||||||
ty.message_name(),
|
|
||||||
name,
|
|
||||||
print_stream(stream)
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
format!("{}: `{}`", ty.message_name(), print_stream(stream))
|
|
||||||
};
|
|
||||||
|
|
||||||
attrs.push(make_attribute(&doc_str));
|
|
||||||
attrs.push(make_attribute(""));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
attrs
|
|
||||||
}
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use crate::implementation::{ContractMode, ContractType, FuncWithContracts};
|
|
||||||
use proc_macro2::TokenStream;
|
|
||||||
|
|
||||||
pub(crate) fn ensures(
|
|
||||||
mode: ContractMode,
|
|
||||||
attr: TokenStream,
|
|
||||||
toks: TokenStream,
|
|
||||||
) -> TokenStream {
|
|
||||||
let ty = ContractType::Ensures;
|
|
||||||
|
|
||||||
let func = syn::parse_quote!(#toks);
|
|
||||||
|
|
||||||
let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);
|
|
||||||
|
|
||||||
f.generate()
|
|
||||||
}
|
|
||||||
|
|
@ -1,94 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use proc_macro2::TokenStream;
|
|
||||||
use quote::ToTokens;
|
|
||||||
use syn::{FnArg, ImplItem, ImplItemFn, Item, ItemFn, ItemImpl};
|
|
||||||
|
|
||||||
use crate::implementation::{ContractMode, ContractType, FuncWithContracts};
|
|
||||||
|
|
||||||
pub(crate) fn invariant(
|
|
||||||
mode: ContractMode,
|
|
||||||
attr: TokenStream,
|
|
||||||
toks: TokenStream,
|
|
||||||
) -> TokenStream {
|
|
||||||
let item: Item = syn::parse_quote!(#toks);
|
|
||||||
|
|
||||||
let name = mode.name().unwrap().to_string() + "invariant";
|
|
||||||
|
|
||||||
match item {
|
|
||||||
Item::Fn(fn_) => invariant_fn(mode, attr, fn_),
|
|
||||||
Item::Impl(impl_) => invariant_impl(mode, attr, impl_),
|
|
||||||
_ => unimplemented!(
|
|
||||||
"The #[{}] attribute only works on functions and impl-blocks.",
|
|
||||||
name
|
|
||||||
),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn invariant_fn(
|
|
||||||
mode: ContractMode,
|
|
||||||
attr: TokenStream,
|
|
||||||
func: ItemFn,
|
|
||||||
) -> TokenStream {
|
|
||||||
let ty = ContractType::Invariant;
|
|
||||||
|
|
||||||
let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);
|
|
||||||
|
|
||||||
f.generate()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Generate the token-stream for an `impl` block with a "global" invariant.
|
|
||||||
fn invariant_impl(
|
|
||||||
mode: ContractMode,
|
|
||||||
invariant: TokenStream,
|
|
||||||
mut impl_def: ItemImpl,
|
|
||||||
) -> TokenStream {
|
|
||||||
// all that is done is prefix all the function definitions with
|
|
||||||
// the invariant attribute.
|
|
||||||
// The following expansion of the attributes will then implement the
|
|
||||||
// invariant just like it's done for functions.
|
|
||||||
|
|
||||||
// The mode received is "raw", so it can't be "Disabled" or "LogOnly"
|
|
||||||
// but it can't hurt to deal with it anyway.
|
|
||||||
let name = match mode.name() {
|
|
||||||
Some(n) => n.to_string() + "invariant",
|
|
||||||
None => {
|
|
||||||
return quote::quote!( #impl_def );
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let invariant_ident =
|
|
||||||
syn::Ident::new(&name, proc_macro2::Span::call_site());
|
|
||||||
|
|
||||||
fn method_uses_self(method: &ImplItemFn) -> bool {
|
|
||||||
let inputs = &method.sig.inputs;
|
|
||||||
|
|
||||||
if !inputs.is_empty() {
|
|
||||||
matches!(inputs[0], FnArg::Receiver(_))
|
|
||||||
} else {
|
|
||||||
false
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
for item in &mut impl_def.items {
|
|
||||||
if let ImplItem::Fn(method) = item {
|
|
||||||
// only implement invariants for methods that take `self`
|
|
||||||
if !method_uses_self(method) {
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
let method_toks = quote::quote! {
|
|
||||||
#[#invariant_ident(#invariant)]
|
|
||||||
#method
|
|
||||||
};
|
|
||||||
|
|
||||||
let met: ImplItemFn = syn::parse_quote!(#method_toks);
|
|
||||||
|
|
||||||
*method = met;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl_def.into_token_stream()
|
|
||||||
}
|
|
||||||
|
|
@ -1,238 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
pub(crate) mod codegen;
|
|
||||||
pub(crate) mod doc;
|
|
||||||
pub(crate) mod ensures;
|
|
||||||
pub(crate) mod invariant;
|
|
||||||
pub(crate) mod parse;
|
|
||||||
pub(crate) mod requires;
|
|
||||||
pub(crate) mod traits;
|
|
||||||
|
|
||||||
use quote::ToTokens;
|
|
||||||
use syn::{Expr, ItemFn};
|
|
||||||
|
|
||||||
pub(crate) use ensures::ensures;
|
|
||||||
pub(crate) use invariant::invariant;
|
|
||||||
use proc_macro2::{Span, TokenStream};
|
|
||||||
pub(crate) use requires::requires;
|
|
||||||
pub(crate) use traits::{contract_trait_item_impl, contract_trait_item_trait};
|
|
||||||
|
|
||||||
/// Checking-mode of a contract.
|
|
||||||
#[derive(Debug, Copy, Clone, Eq, PartialEq)]
|
|
||||||
pub(crate) enum ContractMode {
|
|
||||||
/// Always check contract
|
|
||||||
Always,
|
|
||||||
/// Never check contract
|
|
||||||
Disabled,
|
|
||||||
/// Check contract only in debug builds
|
|
||||||
Debug,
|
|
||||||
/// Check contract only in `#[cfg(test)]` configurations
|
|
||||||
Test,
|
|
||||||
/// Check the contract and print information upon violation, but don't abort
|
|
||||||
/// the program.
|
|
||||||
LogOnly,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl ContractMode {
|
|
||||||
/// Return the prefix of attributes of `self` mode.
|
|
||||||
pub(crate) fn name(self) -> Option<&'static str> {
|
|
||||||
match self {
|
|
||||||
ContractMode::Always => Some(""),
|
|
||||||
ContractMode::Disabled => None,
|
|
||||||
ContractMode::Debug => Some("debug_"),
|
|
||||||
ContractMode::Test => Some("test_"),
|
|
||||||
ContractMode::LogOnly => None,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Computes the contract type based on feature flags.
|
|
||||||
pub(crate) fn final_mode(self) -> Self {
|
|
||||||
// disabled ones can't be "forced", test ones should stay test, no
|
|
||||||
// matter what.
|
|
||||||
if self == ContractMode::Disabled || self == ContractMode::Test {
|
|
||||||
return self;
|
|
||||||
}
|
|
||||||
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
ContractMode::Disabled
|
|
||||||
} else if cfg!(feature = "override_debug") {
|
|
||||||
// log is "weaker" than debug, so keep log
|
|
||||||
if self == ContractMode::LogOnly {
|
|
||||||
self
|
|
||||||
} else {
|
|
||||||
ContractMode::Debug
|
|
||||||
}
|
|
||||||
} else if cfg!(feature = "override_log") {
|
|
||||||
ContractMode::LogOnly
|
|
||||||
} else {
|
|
||||||
self
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// The different contract types.
|
|
||||||
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
|
|
||||||
pub(crate) enum ContractType {
|
|
||||||
Requires,
|
|
||||||
Ensures,
|
|
||||||
Invariant,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl ContractType {
|
|
||||||
/// Get the name that is used as a message-prefix on violation of a
|
|
||||||
/// contract.
|
|
||||||
pub(crate) fn message_name(self) -> &'static str {
|
|
||||||
match self {
|
|
||||||
ContractType::Requires => "Pre-condition",
|
|
||||||
ContractType::Ensures => "Post-condition",
|
|
||||||
ContractType::Invariant => "Invariant",
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Determine the type and mode of an identifier.
|
|
||||||
pub(crate) fn contract_type_and_mode(
|
|
||||||
ident: &str,
|
|
||||||
) -> Option<(ContractType, ContractMode)> {
|
|
||||||
match ident {
|
|
||||||
"requires" => Some((ContractType::Requires, ContractMode::Always)),
|
|
||||||
"ensures" => Some((ContractType::Ensures, ContractMode::Always)),
|
|
||||||
"invariant" => {
|
|
||||||
Some((ContractType::Invariant, ContractMode::Always))
|
|
||||||
}
|
|
||||||
"debug_requires" => {
|
|
||||||
Some((ContractType::Requires, ContractMode::Debug))
|
|
||||||
}
|
|
||||||
"debug_ensures" => {
|
|
||||||
Some((ContractType::Ensures, ContractMode::Debug))
|
|
||||||
}
|
|
||||||
"debug_invariant" => {
|
|
||||||
Some((ContractType::Invariant, ContractMode::Debug))
|
|
||||||
}
|
|
||||||
"test_requires" => {
|
|
||||||
Some((ContractType::Requires, ContractMode::Test))
|
|
||||||
}
|
|
||||||
"test_ensures" => Some((ContractType::Ensures, ContractMode::Test)),
|
|
||||||
"test_invariant" => {
|
|
||||||
Some((ContractType::Invariant, ContractMode::Test))
|
|
||||||
}
|
|
||||||
_ => None,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Representation of a contract
|
|
||||||
#[derive(Debug)]
|
|
||||||
pub(crate) struct Contract {
|
|
||||||
pub(crate) _span: Span,
|
|
||||||
pub(crate) ty: ContractType,
|
|
||||||
pub(crate) mode: ContractMode,
|
|
||||||
pub(crate) assertions: Vec<Expr>,
|
|
||||||
pub(crate) streams: Vec<TokenStream>,
|
|
||||||
pub(crate) desc: Option<String>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Contract {
|
|
||||||
pub(crate) fn from_toks(
|
|
||||||
ty: ContractType,
|
|
||||||
mode: ContractMode,
|
|
||||||
toks: TokenStream,
|
|
||||||
) -> Self {
|
|
||||||
let (assertions, streams, desc) = parse::parse_attributes(toks);
|
|
||||||
|
|
||||||
let span = Span::call_site();
|
|
||||||
|
|
||||||
Self {
|
|
||||||
_span: span,
|
|
||||||
ty,
|
|
||||||
mode,
|
|
||||||
assertions,
|
|
||||||
streams,
|
|
||||||
desc,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// A function that is annotated with contracts
|
|
||||||
#[derive(Debug)]
|
|
||||||
pub(crate) struct FuncWithContracts {
|
|
||||||
pub(crate) contracts: Vec<Contract>,
|
|
||||||
pub(crate) function: ItemFn,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl FuncWithContracts {
|
|
||||||
/// Create a `FuncWithContracts` value from the attribute-tokens of the
|
|
||||||
/// first contract and a parsed version of the function.
|
|
||||||
///
|
|
||||||
/// The initial contract is parsed from the tokens, others will be read from
|
|
||||||
/// parsed function.
|
|
||||||
pub(crate) fn new_with_initial_contract(
|
|
||||||
mut func: ItemFn,
|
|
||||||
cty: ContractType,
|
|
||||||
cmode: ContractMode,
|
|
||||||
ctoks: TokenStream,
|
|
||||||
) -> Self {
|
|
||||||
// add in the first attribute
|
|
||||||
let mut contracts: Vec<Contract> = {
|
|
||||||
let initial_contract = Contract::from_toks(cty, cmode, ctoks);
|
|
||||||
vec![initial_contract]
|
|
||||||
};
|
|
||||||
|
|
||||||
// find all other attributes
|
|
||||||
|
|
||||||
let contract_attrs = func
|
|
||||||
.attrs
|
|
||||||
.iter()
|
|
||||||
.filter_map(|a| {
|
|
||||||
let name = a.path().segments.last().unwrap().ident.to_string();
|
|
||||||
let (ty, mode) = ContractType::contract_type_and_mode(&name)?;
|
|
||||||
Some((ty, mode, a))
|
|
||||||
})
|
|
||||||
.map(|(ty, mode, a)| {
|
|
||||||
// the tts on attributes contains the out parenthesis, so some
|
|
||||||
// code might be mistakenly parsed as tuples, that's not good!
|
|
||||||
//
|
|
||||||
// this is a hack to get to the inner token stream.
|
|
||||||
use syn::Meta;
|
|
||||||
let toks = match &a.meta {
|
|
||||||
Meta::Path(_) => unreachable!(),
|
|
||||||
Meta::List(x) => x.tokens.clone(),
|
|
||||||
Meta::NameValue(x) => x.value.to_token_stream(),
|
|
||||||
};
|
|
||||||
Contract::from_toks(ty, mode, toks)
|
|
||||||
});
|
|
||||||
|
|
||||||
contracts.extend(contract_attrs);
|
|
||||||
|
|
||||||
// remove contract attributes
|
|
||||||
{
|
|
||||||
let attrs = std::mem::take(&mut func.attrs);
|
|
||||||
|
|
||||||
let other_attrs = attrs
|
|
||||||
.into_iter()
|
|
||||||
.filter(|attr| {
|
|
||||||
ContractType::contract_type_and_mode(
|
|
||||||
&attr.path().segments.last().unwrap().ident.to_string(),
|
|
||||||
)
|
|
||||||
.is_none()
|
|
||||||
})
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
func.attrs = other_attrs;
|
|
||||||
}
|
|
||||||
|
|
||||||
Self {
|
|
||||||
function: func,
|
|
||||||
contracts,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Generates the resulting tokens including all contract-checks
|
|
||||||
pub(crate) fn generate(mut self) -> TokenStream {
|
|
||||||
let doc_attrs = doc::generate_attributes(&self.contracts);
|
|
||||||
let olds = codegen::extract_old_calls(&mut self.contracts);
|
|
||||||
|
|
||||||
codegen::generate(self, doc_attrs, olds)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,187 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use proc_macro2::{Spacing, TokenStream, TokenTree};
|
|
||||||
use syn::{Expr, ExprLit, Lit};
|
|
||||||
|
|
||||||
/// Parse attributes into a list of expression and an optional description of
|
|
||||||
/// the assert
|
|
||||||
pub(crate) fn parse_attributes(
|
|
||||||
attrs: TokenStream,
|
|
||||||
) -> (Vec<Expr>, Vec<TokenStream>, Option<String>) {
|
|
||||||
let segments = segment_input(attrs);
|
|
||||||
let mut segments_stream: Vec<TokenStream> = segments
|
|
||||||
.iter()
|
|
||||||
.map(|x| x.iter().cloned().collect::<TokenStream>())
|
|
||||||
.collect();
|
|
||||||
let rewritten_segs: Vec<_> = segments.into_iter().map(rewrite).collect();
|
|
||||||
|
|
||||||
let mut conds: Vec<Expr> = vec![];
|
|
||||||
|
|
||||||
for seg in rewritten_segs {
|
|
||||||
let expr = match syn::parse2::<Expr>(seg) {
|
|
||||||
Ok(val) => val,
|
|
||||||
Err(err) => Expr::Verbatim(err.to_compile_error()),
|
|
||||||
};
|
|
||||||
conds.push(expr);
|
|
||||||
}
|
|
||||||
|
|
||||||
let desc = conds
|
|
||||||
.last()
|
|
||||||
.map(|expr| match expr {
|
|
||||||
Expr::Lit(ExprLit {
|
|
||||||
lit: Lit::Str(str), ..
|
|
||||||
}) => Some(str.value()),
|
|
||||||
_ => None,
|
|
||||||
})
|
|
||||||
.unwrap_or(None);
|
|
||||||
|
|
||||||
if desc.is_some() {
|
|
||||||
conds.pop();
|
|
||||||
segments_stream.pop();
|
|
||||||
}
|
|
||||||
|
|
||||||
(conds, segments_stream, desc)
|
|
||||||
}
|
|
||||||
|
|
||||||
// This function rewrites a list of TokenTrees so that the "pseudooperator" for
|
|
||||||
// implication `==>` gets transformed into an `if` expression.
|
|
||||||
//
|
|
||||||
// This has to happen on a TokenStream/Tree because it's not possible to easily
|
|
||||||
// add new syntax to the syn parsers without basically re-writing the whole
|
|
||||||
// expression parsing functions from scratch.
|
|
||||||
//
|
|
||||||
// The input gets classified into "before `==>` op" and "after `==>` op". Those
|
|
||||||
// two groups are then used to create an `if` that has implication semantics.
|
|
||||||
// However, because the input is only split based on the operator, no precedence
|
|
||||||
// is respected, including keywords such as `if`. This means the implication
|
|
||||||
// operator should only be used in grouped expressions.
|
|
||||||
// This also has the effect that implication is right-associative, which is the
|
|
||||||
// expected behaviour.
|
|
||||||
fn rewrite(segments: Vec<TokenTree>) -> proc_macro2::TokenStream {
|
|
||||||
let mut lhs = vec![];
|
|
||||||
let mut rhs: Option<_> = None;
|
|
||||||
let mut span: Option<_> = None;
|
|
||||||
|
|
||||||
let mut idx = 0;
|
|
||||||
|
|
||||||
'segment: while let Some(tt) = segments.get(idx) {
|
|
||||||
match tt {
|
|
||||||
TokenTree::Group(group) => {
|
|
||||||
let stream: Vec<_> = group.stream().into_iter().collect();
|
|
||||||
|
|
||||||
let new_stream: TokenStream =
|
|
||||||
rewrite(stream).into_iter().collect();
|
|
||||||
|
|
||||||
let mut new_group =
|
|
||||||
proc_macro2::Group::new(group.delimiter(), new_stream);
|
|
||||||
new_group.set_span(group.span());
|
|
||||||
|
|
||||||
lhs.push(TokenTree::Group(new_group));
|
|
||||||
idx += 1;
|
|
||||||
}
|
|
||||||
TokenTree::Ident(_) => {
|
|
||||||
lhs.push(tt.clone());
|
|
||||||
idx += 1;
|
|
||||||
}
|
|
||||||
TokenTree::Literal(_) => {
|
|
||||||
lhs.push(tt.clone());
|
|
||||||
idx += 1;
|
|
||||||
}
|
|
||||||
TokenTree::Punct(_) => {
|
|
||||||
let punct = |idx: usize, c: char, s: Spacing| -> bool {
|
|
||||||
let tt = if let Some(val) = segments.get(idx) {
|
|
||||||
val
|
|
||||||
} else {
|
|
||||||
return false;
|
|
||||||
};
|
|
||||||
|
|
||||||
if let TokenTree::Punct(p) = tt {
|
|
||||||
p.as_char() == c && p.spacing() == s
|
|
||||||
} else {
|
|
||||||
false
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
if punct(idx, '-', Spacing::Joint)
|
|
||||||
&& punct(idx + 1, '>', Spacing::Alone)
|
|
||||||
{
|
|
||||||
// found the implication
|
|
||||||
let rest = Vec::from(&segments[idx + 2..]);
|
|
||||||
let rhs_stream = rewrite(rest);
|
|
||||||
|
|
||||||
rhs = Some(rhs_stream);
|
|
||||||
span = Some(segments[idx + 1].span());
|
|
||||||
break 'segment;
|
|
||||||
} else {
|
|
||||||
// consume all so that =========> would not match with
|
|
||||||
// implication
|
|
||||||
'op: while let Some(tt) = segments.get(idx) {
|
|
||||||
match tt {
|
|
||||||
TokenTree::Punct(p) => {
|
|
||||||
if p.spacing() == Spacing::Alone {
|
|
||||||
// read this one but finish afterwards
|
|
||||||
lhs.push(tt.clone());
|
|
||||||
idx += 1;
|
|
||||||
break 'op;
|
|
||||||
} else {
|
|
||||||
// this punctuation is a joint-punctuation
|
|
||||||
// so needs to be read and then continue
|
|
||||||
lhs.push(tt.clone());
|
|
||||||
idx += 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
_ => {
|
|
||||||
// not a punktuation, so do not increase idx
|
|
||||||
break 'op;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
match (rhs, span) {
|
|
||||||
(None, None) => lhs.into_iter().collect(),
|
|
||||||
(None, Some(_)) => {
|
|
||||||
unreachable!("If there's a span there should be an implication")
|
|
||||||
}
|
|
||||||
(Some(_), None) => unreachable!("Invalid spans"),
|
|
||||||
(Some(rhs), Some(span)) => {
|
|
||||||
let lhs: TokenStream = lhs.into_iter().collect();
|
|
||||||
|
|
||||||
quote::quote_spanned! {
|
|
||||||
span =>
|
|
||||||
(!(#lhs) || #rhs)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// The tokenstream can contain multiple expressions to be checked, separated by
|
|
||||||
// a comma. This function "pulls" those expressions apart.
|
|
||||||
fn segment_input(tts: TokenStream) -> Vec<Vec<TokenTree>> {
|
|
||||||
let mut groups = vec![];
|
|
||||||
|
|
||||||
let mut group = vec![];
|
|
||||||
|
|
||||||
for tt in tts {
|
|
||||||
match tt {
|
|
||||||
TokenTree::Punct(p)
|
|
||||||
if p.as_char() == ',' && p.spacing() == Spacing::Alone =>
|
|
||||||
{
|
|
||||||
groups.push(group);
|
|
||||||
group = vec![];
|
|
||||||
}
|
|
||||||
t => group.push(t),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if !group.is_empty() {
|
|
||||||
groups.push(group);
|
|
||||||
}
|
|
||||||
|
|
||||||
groups
|
|
||||||
}
|
|
||||||
|
|
@ -1,21 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use crate::implementation::{ContractMode, ContractType, FuncWithContracts};
|
|
||||||
use proc_macro2::TokenStream;
|
|
||||||
use syn::ItemFn;
|
|
||||||
|
|
||||||
pub(crate) fn requires(
|
|
||||||
mode: ContractMode,
|
|
||||||
attr: TokenStream,
|
|
||||||
toks: TokenStream,
|
|
||||||
) -> TokenStream {
|
|
||||||
let ty = ContractType::Requires;
|
|
||||||
|
|
||||||
let func: ItemFn = syn::parse_quote!(#toks);
|
|
||||||
|
|
||||||
let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);
|
|
||||||
|
|
||||||
f.generate()
|
|
||||||
}
|
|
||||||
|
|
@ -1,302 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use crate::implementation::ContractType;
|
|
||||||
use proc_macro2::TokenStream;
|
|
||||||
use quote::ToTokens;
|
|
||||||
use syn::{
|
|
||||||
FnArg, ImplItem, ItemImpl, ItemTrait, Pat, TraitItem, TraitItemFn,
|
|
||||||
};
|
|
||||||
|
|
||||||
/// Name used for the "re-routed" method.
|
|
||||||
fn contract_method_impl_name(name: &str) -> String {
|
|
||||||
format!("__contracts_impl_{}", name)
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Modifies a trait item in a way that it includes contracts.
|
|
||||||
pub(crate) fn contract_trait_item_trait(
|
|
||||||
_attrs: TokenStream,
|
|
||||||
mut trait_: ItemTrait,
|
|
||||||
) -> TokenStream {
|
|
||||||
/// Just rename the method to have an internal, generated name.
|
|
||||||
fn create_method_rename(method: &TraitItemFn) -> TraitItemFn {
|
|
||||||
let mut m: TraitItemFn = (*method).clone();
|
|
||||||
|
|
||||||
// rename method and modify attributes
|
|
||||||
{
|
|
||||||
// remove any contracts attributes and rename
|
|
||||||
let name = m.sig.ident.to_string();
|
|
||||||
|
|
||||||
let new_name = contract_method_impl_name(&name);
|
|
||||||
|
|
||||||
let mut new_attrs = vec![];
|
|
||||||
new_attrs.push(syn::parse_quote!(#[doc(hidden)]));
|
|
||||||
new_attrs.push(syn::parse_quote!(#[doc = "This is an internal function that is not meant to be used directly!"]));
|
|
||||||
new_attrs.push(syn::parse_quote!(#[doc = "See the documentation of the `#[contract_trait]` attribute."]));
|
|
||||||
|
|
||||||
// add all existing non-contract attributes
|
|
||||||
new_attrs.extend(
|
|
||||||
m.attrs
|
|
||||||
.iter()
|
|
||||||
.filter(|a| {
|
|
||||||
let name =
|
|
||||||
a.path().segments.last().unwrap().ident.to_string();
|
|
||||||
|
|
||||||
ContractType::contract_type_and_mode(&name).is_none()
|
|
||||||
})
|
|
||||||
.cloned(),
|
|
||||||
);
|
|
||||||
|
|
||||||
m.attrs = new_attrs;
|
|
||||||
|
|
||||||
m.sig.ident = syn::Ident::new(&new_name, m.sig.ident.span());
|
|
||||||
}
|
|
||||||
|
|
||||||
m
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Create a wrapper function which has a default implementation and
|
|
||||||
/// includes contracts.
|
|
||||||
///
|
|
||||||
/// This new function forwards the call to the actual implementation.
|
|
||||||
fn create_method_wrapper(method: &TraitItemFn) -> TraitItemFn {
|
|
||||||
struct ArgInfo {
|
|
||||||
call_toks: proc_macro2::TokenStream,
|
|
||||||
}
|
|
||||||
|
|
||||||
// Calculate name and pattern tokens
|
|
||||||
fn arg_pat_info(pat: &Pat) -> ArgInfo {
|
|
||||||
match pat {
|
|
||||||
Pat::Ident(ident) => {
|
|
||||||
let toks = quote::quote! {
|
|
||||||
#ident
|
|
||||||
};
|
|
||||||
ArgInfo { call_toks: toks }
|
|
||||||
}
|
|
||||||
Pat::Tuple(tup) => {
|
|
||||||
let infos = tup.elems.iter().map(arg_pat_info);
|
|
||||||
|
|
||||||
let toks = {
|
|
||||||
let mut toks = proc_macro2::TokenStream::new();
|
|
||||||
|
|
||||||
for info in infos {
|
|
||||||
toks.extend(info.call_toks);
|
|
||||||
toks.extend(quote::quote!(,));
|
|
||||||
}
|
|
||||||
|
|
||||||
toks
|
|
||||||
};
|
|
||||||
|
|
||||||
ArgInfo {
|
|
||||||
call_toks: quote::quote!((#toks)),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Pat::TupleStruct(_tup) => unimplemented!(),
|
|
||||||
p => panic!("Unsupported pattern type: {:?}", p),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut m: TraitItemFn = (*method).clone();
|
|
||||||
|
|
||||||
let argument_data = m
|
|
||||||
.sig
|
|
||||||
.inputs
|
|
||||||
.clone()
|
|
||||||
.into_iter()
|
|
||||||
.map(|t: FnArg| match &t {
|
|
||||||
FnArg::Receiver(_) => quote::quote!(self),
|
|
||||||
FnArg::Typed(p) => {
|
|
||||||
let info = arg_pat_info(&p.pat);
|
|
||||||
|
|
||||||
info.call_toks
|
|
||||||
}
|
|
||||||
})
|
|
||||||
.collect::<Vec<_>>();
|
|
||||||
|
|
||||||
let arguments = {
|
|
||||||
let mut toks = proc_macro2::TokenStream::new();
|
|
||||||
|
|
||||||
for arg in argument_data {
|
|
||||||
toks.extend(arg);
|
|
||||||
toks.extend(quote::quote!(,));
|
|
||||||
}
|
|
||||||
|
|
||||||
toks
|
|
||||||
};
|
|
||||||
|
|
||||||
let body: TokenStream = {
|
|
||||||
let name = contract_method_impl_name(&m.sig.ident.to_string());
|
|
||||||
let name = syn::Ident::new(&name, m.sig.ident.span());
|
|
||||||
|
|
||||||
quote::quote! {
|
|
||||||
{
|
|
||||||
Self::#name(#arguments)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let mut attrs = vec![];
|
|
||||||
|
|
||||||
// keep the documentation and contracts of the original method
|
|
||||||
attrs.extend(
|
|
||||||
m.attrs
|
|
||||||
.iter()
|
|
||||||
.filter(|a| {
|
|
||||||
let name =
|
|
||||||
a.path().segments.last().unwrap().ident.to_string();
|
|
||||||
// is doc?
|
|
||||||
if name == "doc" {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
// is contract?
|
|
||||||
ContractType::contract_type_and_mode(&name).is_some()
|
|
||||||
})
|
|
||||||
.cloned(),
|
|
||||||
);
|
|
||||||
// always inline
|
|
||||||
attrs.push(syn::parse_quote!(#[inline(always)]));
|
|
||||||
|
|
||||||
m.attrs = attrs;
|
|
||||||
|
|
||||||
{
|
|
||||||
let block: syn::Block = syn::parse2(body).unwrap();
|
|
||||||
m.default = Some(block);
|
|
||||||
m.semi_token = None;
|
|
||||||
}
|
|
||||||
|
|
||||||
m
|
|
||||||
}
|
|
||||||
|
|
||||||
// create method wrappers and renamed items
|
|
||||||
let funcs = trait_
|
|
||||||
.items
|
|
||||||
.iter()
|
|
||||||
.filter_map(|item| {
|
|
||||||
if let TraitItem::Fn(m) = item {
|
|
||||||
let rename = create_method_rename(m);
|
|
||||||
let wrapper = create_method_wrapper(m);
|
|
||||||
|
|
||||||
Some(vec![
|
|
||||||
TraitItem::Fn(rename),
|
|
||||||
TraitItem::Fn(wrapper),
|
|
||||||
])
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
})
|
|
||||||
.flatten()
|
|
||||||
.collect::<Vec<_>>();
|
|
||||||
|
|
||||||
// remove all previous methods
|
|
||||||
trait_.items = trait_
|
|
||||||
.items
|
|
||||||
.into_iter()
|
|
||||||
.filter(|item| !matches!(item, TraitItem::Fn(_)))
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
// add back new methods
|
|
||||||
trait_.items.extend(funcs);
|
|
||||||
|
|
||||||
trait_.into_token_stream()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Rename all methods inside an `impl` to use the "internal implementation"
|
|
||||||
/// name.
|
|
||||||
pub(crate) fn contract_trait_item_impl(
|
|
||||||
_attrs: TokenStream,
|
|
||||||
impl_: ItemImpl,
|
|
||||||
) -> TokenStream {
|
|
||||||
let new_impl = {
|
|
||||||
let mut impl_: ItemImpl = impl_;
|
|
||||||
|
|
||||||
impl_.items.iter_mut().for_each(|it| {
|
|
||||||
if let ImplItem::Fn(method) = it {
|
|
||||||
let new_name =
|
|
||||||
contract_method_impl_name(&method.sig.ident.to_string());
|
|
||||||
let new_ident =
|
|
||||||
syn::Ident::new(&new_name, method.sig.ident.span());
|
|
||||||
|
|
||||||
method.sig.ident = new_ident;
|
|
||||||
}
|
|
||||||
});
|
|
||||||
|
|
||||||
impl_
|
|
||||||
};
|
|
||||||
|
|
||||||
new_impl.to_token_stream()
|
|
||||||
}
|
|
||||||
|
|
||||||
#[cfg(test)]
|
|
||||||
mod tests {
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn attributes_stay_on_trait_def() {
|
|
||||||
// attributes on functions should apply to the outer "wrapping" function
|
|
||||||
// only, the "internal" function should be hidden and be inlined.
|
|
||||||
|
|
||||||
let code = syn::parse_quote! {
|
|
||||||
trait Random {
|
|
||||||
/// Test!
|
|
||||||
#[aaa]
|
|
||||||
#[ensures((min..max).contains(ret))]
|
|
||||||
fn random_number(min: u8, max: u8) -> u8;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let expected = quote::quote! {
|
|
||||||
trait Random {
|
|
||||||
#[doc(hidden)]
|
|
||||||
#[doc = "This is an internal function that is not meant to be used directly!"]
|
|
||||||
#[doc = "See the documentation of the `#[contract_trait]` attribute."]
|
|
||||||
/// Test!
|
|
||||||
#[aaa]
|
|
||||||
fn __contracts_impl_random_number(min: u8, max: u8) -> u8;
|
|
||||||
|
|
||||||
/// Test!
|
|
||||||
#[ensures((min..max).contains(ret))]
|
|
||||||
#[inline(always)]
|
|
||||||
fn random_number(min: u8, max: u8) -> u8 {
|
|
||||||
Self::__contracts_impl_random_number(min, max,)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let generated =
|
|
||||||
super::contract_trait_item_trait(Default::default(), code);
|
|
||||||
|
|
||||||
assert_eq!(generated.to_string(), expected.to_string());
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn attributes_stay_on_trait_impl() {
|
|
||||||
// attributes on functions should apply to the outer "wrapping" function
|
|
||||||
// only, the "internal" function should be hidden and be inlined.
|
|
||||||
|
|
||||||
let code = syn::parse_quote! {
|
|
||||||
impl Random for AlwaysMin {
|
|
||||||
/// docs for this function!
|
|
||||||
#[no_panic]
|
|
||||||
fn random_number(min: u8, max: u8) -> u8 {
|
|
||||||
min
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let expected = quote::quote! {
|
|
||||||
impl Random for AlwaysMin {
|
|
||||||
/// docs for this function!
|
|
||||||
#[no_panic]
|
|
||||||
fn __contracts_impl_random_number(min: u8, max: u8) -> u8 {
|
|
||||||
min
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let generated =
|
|
||||||
super::contract_trait_item_impl(Default::default(), code);
|
|
||||||
|
|
||||||
assert_eq!(generated.to_string(), expected.to_string());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,450 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
//! A crate implementing ["Design by Contract"][dbc] via procedural macros.
|
|
||||||
//!
|
|
||||||
//! This crate is heavily inspired by the [`libhoare`] compiler plugin.
|
|
||||||
//!
|
|
||||||
//! The main use of this crate is to annotate functions and methods using
|
|
||||||
//! "contracts" in the form of [*pre-conditions* (`requires`)][precond],
|
|
||||||
//! [*post-conditions* (`ensures`)][postcond] and [*invariants*][invariant].
|
|
||||||
//!
|
|
||||||
//! Each "contract" annotation that is violated will cause an assertion failure.
|
|
||||||
//!
|
|
||||||
//! The attributes use "function call form" and can contain 1 or more conditions
|
|
||||||
//! to check.
|
|
||||||
//! If the last argument to an attribute is a string constant it will be
|
|
||||||
//! inserted into the assertion message.
|
|
||||||
//!
|
|
||||||
//! ## Example
|
|
||||||
//!
|
|
||||||
//! ```rust
|
|
||||||
//! # use contracts::*;
|
|
||||||
//! #[requires(x > 0, "x must be in the valid input range")]
|
|
||||||
//! #[ensures(ret.is_some() -> ret.unwrap() * ret.unwrap() == x)]
|
|
||||||
//! fn integer_sqrt(x: u64) -> Option<u64> {
|
|
||||||
//! // ...
|
|
||||||
//! # unimplemented!()
|
|
||||||
//! }
|
|
||||||
//! ```
|
|
||||||
//!
|
|
||||||
//! ```rust
|
|
||||||
//! # use std::collections::HashSet;
|
|
||||||
//! # use contracts::*;
|
|
||||||
//! pub struct Library {
|
|
||||||
//! available: HashSet<String>,
|
|
||||||
//! lent: HashSet<String>,
|
|
||||||
//! }
|
|
||||||
//!
|
|
||||||
//! impl Library {
|
|
||||||
//! fn book_exists(&self, book_id: &str) -> bool {
|
|
||||||
//! self.available.contains(book_id)
|
|
||||||
//! || self.lent.contains(book_id)
|
|
||||||
//! }
|
|
||||||
//!
|
|
||||||
//! #[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
|
|
||||||
//! #[debug_ensures(self.available.contains(book_id), "Book now available")]
|
|
||||||
//! #[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
//! #[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
|
|
||||||
//! pub fn add_book(&mut self, book_id: &str) {
|
|
||||||
//! self.available.insert(book_id.to_string());
|
|
||||||
//! }
|
|
||||||
//!
|
|
||||||
//! #[debug_requires(self.book_exists(book_id))]
|
|
||||||
//! #[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
|
|
||||||
//! #[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
|
|
||||||
//! #[debug_ensures(ret -> self.lent.contains(book_id))]
|
|
||||||
//! #[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
|
|
||||||
//! pub fn lend(&mut self, book_id: &str) -> bool {
|
|
||||||
//! if self.available.contains(book_id) {
|
|
||||||
//! self.available.remove(book_id);
|
|
||||||
//! self.lent.insert(book_id.to_string());
|
|
||||||
//! true
|
|
||||||
//! } else {
|
|
||||||
//! false
|
|
||||||
//! }
|
|
||||||
//! }
|
|
||||||
//!
|
|
||||||
//! #[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
|
|
||||||
//! #[ensures(self.lent.len() == old(self.lent.len()) - 1)]
|
|
||||||
//! #[ensures(self.available.len() == old(self.available.len()) + 1)]
|
|
||||||
//! #[debug_ensures(!self.lent.contains(book_id))]
|
|
||||||
//! #[debug_ensures(self.available.contains(book_id), "Book available again")]
|
|
||||||
//! pub fn return_book(&mut self, book_id: &str) {
|
|
||||||
//! self.lent.remove(book_id);
|
|
||||||
//! self.available.insert(book_id.to_string());
|
|
||||||
//! }
|
|
||||||
//! }
|
|
||||||
//! ```
|
|
||||||
//!
|
|
||||||
//! ## Attributes
|
|
||||||
//!
|
|
||||||
//! This crate exposes the `requires`, `ensures` and `invariant` attributes.
|
|
||||||
//!
|
|
||||||
//! - `requires` are checked before a function/method is executed.
|
|
||||||
//! - `ensures` are checked after a function/method ran to completion
|
|
||||||
//! - `invariant`s are checked both before *and* after a function/method ran.
|
|
||||||
//!
|
|
||||||
//! Additionally, all those attributes have versions with different "modes". See
|
|
||||||
//! [the Modes section](#modes) below.
|
|
||||||
//!
|
|
||||||
//! For `trait`s and trait `impl`s the `contract_trait` attribute can be used.
|
|
||||||
//!
|
|
||||||
//! ## Pseudo-functions and operators
|
|
||||||
//!
|
|
||||||
//! ### `old()` function
|
|
||||||
//!
|
|
||||||
//! One unique feature that this crate provides is an `old()` pseudo-function which
|
|
||||||
//! allows to perform checks using a value of a parameter before the function call
|
|
||||||
//! happened. This is only available in `ensures` attributes.
|
|
||||||
//!
|
|
||||||
//! ```rust
|
|
||||||
//! # use contracts::*;
|
|
||||||
//! #[ensures(*x == old(*x) + 1, "after the call `x` was incremented")]
|
|
||||||
//! fn incr(x: &mut usize) {
|
|
||||||
//! *x += 1;
|
|
||||||
//! }
|
|
||||||
//! ```
|
|
||||||
//!
|
|
||||||
//! ### `->` operator
|
|
||||||
//!
|
|
||||||
//! For more complex functions it can be useful to express behaviour using logical
|
|
||||||
//! implication. Because Rust does not feature an operator for implication, this
|
|
||||||
//! crate adds this operator for use in attributes.
|
|
||||||
//!
|
|
||||||
//! ```rust
|
|
||||||
//! # use contracts::*;
|
|
||||||
//! #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
|
|
||||||
//! fn geeting(person_name: Option<&str>) -> String {
|
|
||||||
//! let mut s = String::from("Hello");
|
|
||||||
//! if let Some(name) = person_name {
|
|
||||||
//! s.push(' ');
|
|
||||||
//! s.push_str(name);
|
|
||||||
//! }
|
|
||||||
//! s.push('!');
|
|
||||||
//! s
|
|
||||||
//! }
|
|
||||||
//! ```
|
|
||||||
//!
|
|
||||||
//! This operator is right-associative.
|
|
||||||
//!
|
|
||||||
//! **Note**: Because of the design of `syn`, it is tricky to add custom operators
|
|
||||||
//! to be parsed, so this crate performs a rewrite of the `TokenStream` instead.
|
|
||||||
//! The rewrite works by separating the expression into a part that's left of the
|
|
||||||
//! `->` operator and the rest on the right side. This means that
|
|
||||||
//! `if a -> b { c } else { d }` will not generate the expected code.
|
|
||||||
//! Explicit grouping using parenthesis or curly-brackets can be used to avoid this.
|
|
||||||
//!
|
|
||||||
//! ## Modes
|
|
||||||
//!
|
|
||||||
//! All the attributes (requires, ensures, invariant) have `debug_*` and `test_*` versions.
|
|
||||||
//!
|
|
||||||
//! - `debug_requires`/`debug_ensures`/`debug_invariant` use `debug_assert!`
|
|
||||||
//! internally rather than `assert!`
|
|
||||||
//! - `test_requires`/`test_ensures`/`test_invariant` guard the `assert!` with an
|
|
||||||
//! `if cfg!(test)`.
|
|
||||||
//! This should mostly be used for stating equivalence to "slow but obviously
|
|
||||||
//! correct" alternative implementations or checks.
|
|
||||||
//!
|
|
||||||
//! For example, a merge-sort implementation might look like this
|
|
||||||
//! ```rust
|
|
||||||
//! # use contracts::*;
|
|
||||||
//! # fn is_sorted<T>(x: T) -> bool { true }
|
|
||||||
//! #[test_ensures(is_sorted(input))]
|
|
||||||
//! fn merge_sort<T: Ord + Copy>(input: &mut [T]) {
|
|
||||||
//! // ...
|
|
||||||
//! }
|
|
||||||
//! ```
|
|
||||||
//!
|
|
||||||
//! ## Feature flags
|
|
||||||
//!
|
|
||||||
//! Following feature flags are available:
|
|
||||||
//! - `disable_contracts` - disables all checks and assertions.
|
|
||||||
//! - `override_debug` - changes all contracts (except `test_` ones) into
|
|
||||||
//! `debug_*` versions
|
|
||||||
//! - `override_log` - changes all contracts (except `test_` ones) into a
|
|
||||||
//! `log::error!()` call if the condition is violated.
|
|
||||||
//! No abortion happens.
|
|
||||||
//! - `mirai_assertions` - instead of regular assert! style macros, emit macros
|
|
||||||
//! used by the [MIRAI] static analyzer.
|
|
||||||
//!
|
|
||||||
//! [dbc]: https://en.wikipedia.org/wiki/Design_by_contract
|
|
||||||
//! [`libhoare`]: https://github.com/nrc/libhoare
|
|
||||||
//! [precond]: attr.requires.html
|
|
||||||
//! [postcond]: attr.ensures.html
|
|
||||||
//! [invariant]: attr.invariant.html
|
|
||||||
//! [MIRAI]: https://github.com/facebookexperimental/MIRAI
|
|
||||||
|
|
||||||
extern crate proc_macro;
|
|
||||||
|
|
||||||
mod implementation;
|
|
||||||
|
|
||||||
use implementation::ContractMode;
|
|
||||||
use proc_macro::TokenStream;
|
|
||||||
|
|
||||||
/// Pre-conditions are checked before the function body is run.
|
|
||||||
///
|
|
||||||
/// ## Example
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// #[requires(elems.len() >= 1)]
|
|
||||||
/// fn max<T: Ord + Copy>(elems: &[T]) -> T {
|
|
||||||
/// // ...
|
|
||||||
/// # unimplemented!()
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn requires(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::requires(ContractMode::Always, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`requires`], but uses `debug_assert!`.
|
|
||||||
///
|
|
||||||
/// [`requires`]: attr.requires.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn debug_requires(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::requires(ContractMode::Debug, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`requires`], but is only enabled in `#[cfg(test)]` environments.
|
|
||||||
///
|
|
||||||
/// [`requires`]: attr.requires.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn test_requires(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::requires(ContractMode::Test, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Post-conditions are checked after the function body is run.
|
|
||||||
///
|
|
||||||
/// The result of the function call is accessible in conditions using the `ret`
|
|
||||||
/// identifier.
|
|
||||||
///
|
|
||||||
/// A "pseudo-function" named `old` can be used to evaluate expressions in a
|
|
||||||
/// context *prior* to function execution.
|
|
||||||
/// This function takes only a single argument and the result of it will be
|
|
||||||
/// stored in a variable before the function is called. Because of this,
|
|
||||||
/// handling references might require special care.
|
|
||||||
///
|
|
||||||
/// ## Examples
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// #[ensures(ret > x)]
|
|
||||||
/// fn incr(x: usize) -> usize {
|
|
||||||
/// x + 1
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// #[ensures(*x == old(*x) + 1, "x is incremented")]
|
|
||||||
/// fn incr(x: &mut usize) {
|
|
||||||
/// *x += 1;
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn ensures(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::ensures(ContractMode::Always, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`ensures`], but uses `debug_assert!`.
|
|
||||||
///
|
|
||||||
/// [`ensures`]: attr.ensures.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn debug_ensures(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::ensures(ContractMode::Debug, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`ensures`], but is only enabled in `#[cfg(test)]` environments.
|
|
||||||
///
|
|
||||||
/// [`ensures`]: attr.ensures.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn test_ensures(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::ensures(ContractMode::Test, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Invariants are conditions that have to be maintained at the "interface
|
|
||||||
/// boundaries".
|
|
||||||
///
|
|
||||||
/// Invariants can be supplied to functions (and "methods"), as well as on
|
|
||||||
/// `impl` blocks.
|
|
||||||
///
|
|
||||||
/// When applied to an `impl`-block all methods taking `self` (either by value
|
|
||||||
/// or reference) will be checked for the invariant.
|
|
||||||
///
|
|
||||||
/// ## Example
|
|
||||||
///
|
|
||||||
/// On a function:
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// /// Update `num` to the next bigger even number.
|
|
||||||
/// #[invariant(*num % 2 == 0)]
|
|
||||||
/// fn advance_even(num: &mut usize) {
|
|
||||||
/// *num += 2;
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
///
|
|
||||||
/// On an `impl`-block:
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// struct EvenAdder {
|
|
||||||
/// count: usize,
|
|
||||||
/// }
|
|
||||||
///
|
|
||||||
/// #[invariant(self.count % 2 == 0)]
|
|
||||||
/// impl EvenAdder {
|
|
||||||
/// pub fn tell(&self) -> usize {
|
|
||||||
/// self.count
|
|
||||||
/// }
|
|
||||||
///
|
|
||||||
/// pub fn advance(&mut self) {
|
|
||||||
/// self.count += 2;
|
|
||||||
/// }
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn invariant(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Invariant attributes might apply to `impl` blocks as well, where the same
|
|
||||||
// level is simply replicated on all methods.
|
|
||||||
// Function expansions will resolve the actual mode themselves, so the
|
|
||||||
// actual "raw" mode is passed here
|
|
||||||
//
|
|
||||||
// TODO: update comment when implemented for traits
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
let mode = ContractMode::Always;
|
|
||||||
implementation::invariant(mode, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`invariant`], but uses `debug_assert!`.
|
|
||||||
///
|
|
||||||
/// [`invariant`]: attr.invariant.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn debug_invariant(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mode = ContractMode::Debug;
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::invariant(mode, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Same as [`invariant`], but is only enabled in `#[cfg(test)]` environments.
|
|
||||||
///
|
|
||||||
/// [`invariant`]: attr.invariant.html
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn test_invariant(attr: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mode = ContractMode::Test;
|
|
||||||
let attr = attr.into();
|
|
||||||
let toks = toks.into();
|
|
||||||
implementation::invariant(mode, attr, toks).into()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// A "contract_trait" is a trait which ensures all implementors respect all
|
|
||||||
/// provided contracts.
|
|
||||||
///
|
|
||||||
/// When this attribute is applied to a `trait` definition, the trait gets
|
|
||||||
/// modified so that all invocations of methods are checked.
|
|
||||||
///
|
|
||||||
/// When this attribute is applied to an `impl Trait for Type` item, the
|
|
||||||
/// implementation gets modified so it matches the trait definition.
|
|
||||||
///
|
|
||||||
/// **When the `#[contract_trait]` is not applied to either the trait or an
|
|
||||||
/// `impl` it will cause compile errors**.
|
|
||||||
///
|
|
||||||
/// ## Example
|
|
||||||
///
|
|
||||||
/// ```rust
|
|
||||||
/// # use contracts::*;
|
|
||||||
/// #[contract_trait]
|
|
||||||
/// trait MyRandom {
|
|
||||||
/// #[requires(min < max)]
|
|
||||||
/// #[ensures(min <= ret, ret <= max)]
|
|
||||||
/// fn gen(min: f64, max: f64) -> f64;
|
|
||||||
/// }
|
|
||||||
///
|
|
||||||
/// // Not a very useful random number generator, but a valid one!
|
|
||||||
/// struct AlwaysMax;
|
|
||||||
///
|
|
||||||
/// #[contract_trait]
|
|
||||||
/// impl MyRandom for AlwaysMax {
|
|
||||||
/// fn gen(min: f64, max: f64) -> f64 {
|
|
||||||
/// max
|
|
||||||
/// }
|
|
||||||
/// }
|
|
||||||
/// ```
|
|
||||||
#[proc_macro_attribute]
|
|
||||||
pub fn contract_trait(attrs: TokenStream, toks: TokenStream) -> TokenStream {
|
|
||||||
if cfg!(feature = "disable_contracts") {
|
|
||||||
return toks;
|
|
||||||
}
|
|
||||||
|
|
||||||
let attrs: proc_macro2::TokenStream = attrs.into();
|
|
||||||
let toks: proc_macro2::TokenStream = toks.into();
|
|
||||||
|
|
||||||
let item: syn::Item = syn::parse_quote!(#toks);
|
|
||||||
|
|
||||||
let tts = match item {
|
|
||||||
syn::Item::Trait(trait_) => implementation::contract_trait_item_trait(attrs, trait_),
|
|
||||||
syn::Item::Impl(impl_) => {
|
|
||||||
assert!(
|
|
||||||
impl_.trait_.is_some(),
|
|
||||||
"#[contract_trait] can only be applied to `trait` and `impl ... for` items"
|
|
||||||
);
|
|
||||||
implementation::contract_trait_item_impl(attrs, impl_)
|
|
||||||
}
|
|
||||||
_ => panic!("#[contract_trait] can only be applied to `trait` and `impl ... for` items"),
|
|
||||||
};
|
|
||||||
|
|
||||||
tts.into()
|
|
||||||
}
|
|
||||||
|
|
@ -1,169 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
//! Testing of simple functions.
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_a_thing() {
|
|
||||||
#[requires(x > 10, x < 20, "x must be in valid range")]
|
|
||||||
#[ensures(ret > x, "result will be bigger than input")]
|
|
||||||
fn a(x: usize) -> usize {
|
|
||||||
x + 1
|
|
||||||
}
|
|
||||||
|
|
||||||
a(15);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_sort() {
|
|
||||||
fn is_sorted(input: &[usize]) -> bool {
|
|
||||||
if input.len() < 2 {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
for i in 1..input.len() {
|
|
||||||
if input[i - 1] > input[i] {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
true
|
|
||||||
}
|
|
||||||
|
|
||||||
#[ensures(ret.len() == input.len())]
|
|
||||||
#[test_ensures(is_sorted(&ret))]
|
|
||||||
fn sort(input: &[usize]) -> Vec<usize> {
|
|
||||||
let mut vec = input.to_owned();
|
|
||||||
|
|
||||||
vec.sort_unstable();
|
|
||||||
|
|
||||||
vec
|
|
||||||
}
|
|
||||||
|
|
||||||
let input = vec![31, 234, 34, 0, 4234, 85];
|
|
||||||
|
|
||||||
sort(&input);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_invariant() {
|
|
||||||
#[invariant(*val <= 10)]
|
|
||||||
fn add_to_10(val: &mut usize) {
|
|
||||||
if *val >= 10 {
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
*val += 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut val = 8;
|
|
||||||
|
|
||||||
add_to_10(&mut val);
|
|
||||||
add_to_10(&mut val);
|
|
||||||
add_to_10(&mut val);
|
|
||||||
add_to_10(&mut val);
|
|
||||||
add_to_10(&mut val);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Post-condition of abs violated")]
|
|
||||||
fn test_early_return() {
|
|
||||||
// make sure that post-conditions are executed even if an early return happened.
|
|
||||||
|
|
||||||
#[ensures(ret >= 0)]
|
|
||||||
#[ensures(ret == x || ret == -x)]
|
|
||||||
#[ensures(ret * ret == x * x)]
|
|
||||||
fn abs(x: isize) -> isize {
|
|
||||||
if x < 0 {
|
|
||||||
// this implementation does not respect the contracts!
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
x
|
|
||||||
}
|
|
||||||
|
|
||||||
abs(-4);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_mut_ref_and_lifetimes() {
|
|
||||||
#[requires(i < s.len())]
|
|
||||||
#[ensures(*ret == 0)]
|
|
||||||
fn insert_zero<'a>(s: &'a mut [u8], i: usize) -> &'a mut u8 {
|
|
||||||
s[i] = 0;
|
|
||||||
&mut s[i]
|
|
||||||
}
|
|
||||||
|
|
||||||
insert_zero(&mut [4, 2], 1);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_pattern_match() {
|
|
||||||
#[ensures(ret > a && ret > b)]
|
|
||||||
fn add((a, b): (u8, u8)) -> u8 {
|
|
||||||
a.saturating_add(b)
|
|
||||||
}
|
|
||||||
|
|
||||||
assert_eq!(add((4, 2)), 6);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_impl_trait_return() {
|
|
||||||
// make sure that compiling functions that return existentially
|
|
||||||
// qualified types works properly.
|
|
||||||
|
|
||||||
#[requires(x >= 10)]
|
|
||||||
#[ensures(Clone::clone(&ret) == ret)]
|
|
||||||
#[allow(unused_variables)]
|
|
||||||
fn impl_test(x: isize) -> impl Clone + PartialEq + std::fmt::Debug {
|
|
||||||
"it worked"
|
|
||||||
}
|
|
||||||
|
|
||||||
let x = impl_test(200);
|
|
||||||
let y = x.clone();
|
|
||||||
assert_eq!(
|
|
||||||
format!("{:?} and {:?}", x, y),
|
|
||||||
r#""it worked" and "it worked""#
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_impl_trait_arg() {
|
|
||||||
#[requires(Clone::clone(&x) == x)]
|
|
||||||
#[ensures(Clone::clone(&ret) == ret)]
|
|
||||||
fn impl_test(x: impl Clone + PartialEq + std::fmt::Debug) -> &'static str {
|
|
||||||
"it worked"
|
|
||||||
}
|
|
||||||
|
|
||||||
let x = impl_test(200);
|
|
||||||
let y = Clone::clone(&x);
|
|
||||||
assert_eq!(
|
|
||||||
format!("{:?} and {:?}", x, y),
|
|
||||||
r#""it worked" and "it worked""#
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[deny(clippy::used_underscore_binding)]
|
|
||||||
fn test_unbound_parameters_clippy() {
|
|
||||||
#[requires(__y == 3)]
|
|
||||||
#[ensures(ret)]
|
|
||||||
fn param_test(_x: i32, __y: i32) -> bool {
|
|
||||||
true
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[deny(non_fmt_panics)]
|
|
||||||
fn test_braced_condition_expression_clippy() {
|
|
||||||
#[requires(if __y == 3 {
|
|
||||||
__y != 0
|
|
||||||
} else {
|
|
||||||
false
|
|
||||||
})]
|
|
||||||
fn param_test(_x: i32, __y: i32) {}
|
|
||||||
}
|
|
||||||
|
|
@ -1,82 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_ret_implication() {
|
|
||||||
#[ensures(do_thing -> ret.is_some(), "do_thing should cause a Some(_)")]
|
|
||||||
#[ensures(!do_thing -> ret.is_none(), "!do_thing should cause a None")]
|
|
||||||
fn perform_thing(do_thing: bool) -> Option<usize> {
|
|
||||||
if do_thing {
|
|
||||||
Some(12)
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
perform_thing(true);
|
|
||||||
perform_thing(false);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_ret_implication_old() {
|
|
||||||
#[ensures(old(*x) % 2 == 0 -> *x % 2 == 0)]
|
|
||||||
#[ensures(old(*x) % 2 == 1 -> *x % 2 == 1)]
|
|
||||||
fn incr(x: &mut usize) {
|
|
||||||
*x += 2;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut x = 0;
|
|
||||||
incr(&mut x);
|
|
||||||
|
|
||||||
let mut x = 1;
|
|
||||||
incr(&mut x);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_requires_implication() {
|
|
||||||
#[requires(!negative -> value >= 0)]
|
|
||||||
#[requires(negative -> value < 0)]
|
|
||||||
fn thing(negative: bool, value: isize) {}
|
|
||||||
|
|
||||||
thing(true, -123);
|
|
||||||
|
|
||||||
thing(false, 123);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Post")]
|
|
||||||
fn test_failing_implication() {
|
|
||||||
#[ensures(t -> ret)]
|
|
||||||
#[allow(unused_variables)]
|
|
||||||
fn only_true(t: bool) -> bool {
|
|
||||||
false // oops
|
|
||||||
}
|
|
||||||
|
|
||||||
only_true(true);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_nested_implication() {
|
|
||||||
#[ensures(a -> b -> ret.is_some())]
|
|
||||||
fn test(a: bool, b: bool) -> Option<usize> {
|
|
||||||
if a {
|
|
||||||
if b {
|
|
||||||
Some(9)
|
|
||||||
} else {
|
|
||||||
Some(3)
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
test(true, false);
|
|
||||||
test(false, true);
|
|
||||||
test(true, true);
|
|
||||||
}
|
|
||||||
|
|
@ -1,137 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
//! Testing of methods and `impl`-blocks.
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn methods() {
|
|
||||||
fn is_even(x: usize) -> bool {
|
|
||||||
x % 2 == 0
|
|
||||||
}
|
|
||||||
|
|
||||||
struct EvenAdder {
|
|
||||||
count: usize,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl EvenAdder {
|
|
||||||
#[invariant(is_even(self.count))]
|
|
||||||
#[ensures(self.count == old(self.count) + 2)]
|
|
||||||
fn next_even(&mut self) {
|
|
||||||
self.count += 2;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Manually express the invariant in terms of `ret` since `self.count` is mutably borrowed.
|
|
||||||
#[requires(is_even(self.count))]
|
|
||||||
#[ensures(is_even(*ret))]
|
|
||||||
#[ensures(*ret == old(self.count) + 2)]
|
|
||||||
fn next_even_and_get<'a>(&'a mut self) -> &'a mut usize {
|
|
||||||
self.count += 2;
|
|
||||||
&mut self.count
|
|
||||||
}
|
|
||||||
|
|
||||||
#[invariant(is_even(self.count))]
|
|
||||||
#[requires(self.count >= 2)]
|
|
||||||
#[ensures(self.count == old(self.count) - 2)]
|
|
||||||
fn prev_even(&mut self) {
|
|
||||||
self.count -= 2;
|
|
||||||
}
|
|
||||||
|
|
||||||
#[invariant(is_even(self.count))]
|
|
||||||
fn this_var_collision(&mut self) -> usize {
|
|
||||||
#[allow(unused_variables)]
|
|
||||||
let (this, this__) = (42, 42);
|
|
||||||
self.count
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut adder = EvenAdder { count: 0 };
|
|
||||||
|
|
||||||
adder.next_even();
|
|
||||||
adder.next_even();
|
|
||||||
|
|
||||||
adder.prev_even();
|
|
||||||
adder.prev_even();
|
|
||||||
|
|
||||||
assert_eq!(*adder.next_even_and_get(), 2);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn impl_invariant() {
|
|
||||||
fn is_even(x: usize) -> bool {
|
|
||||||
x % 2 == 0
|
|
||||||
}
|
|
||||||
|
|
||||||
struct EvenAdder {
|
|
||||||
count: usize,
|
|
||||||
}
|
|
||||||
|
|
||||||
#[invariant(is_even(self.count), "Count has to always be even")]
|
|
||||||
impl EvenAdder {
|
|
||||||
const fn step() -> usize {
|
|
||||||
2
|
|
||||||
}
|
|
||||||
|
|
||||||
fn new() -> Self {
|
|
||||||
EvenAdder { count: 0 }
|
|
||||||
}
|
|
||||||
|
|
||||||
#[ensures(self.count == old(self.count) + 2)]
|
|
||||||
fn next_even(&mut self) {
|
|
||||||
self.count += Self::step();
|
|
||||||
}
|
|
||||||
|
|
||||||
#[requires(self.count >= 2)]
|
|
||||||
#[ensures(self.count == old(self.count) - 2)]
|
|
||||||
fn prev_even(&mut self) {
|
|
||||||
self.count -= Self::step();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut adder = EvenAdder::new();
|
|
||||||
|
|
||||||
adder.next_even();
|
|
||||||
adder.next_even();
|
|
||||||
|
|
||||||
adder.prev_even();
|
|
||||||
adder.prev_even();
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_self_macro_hygiene() {
|
|
||||||
struct S {
|
|
||||||
value: i32,
|
|
||||||
}
|
|
||||||
|
|
||||||
// Use a macro to generate the function impl
|
|
||||||
// This requires strict hygiene of the `self` receiver
|
|
||||||
macro_rules! __impl {
|
|
||||||
(
|
|
||||||
$(#[$metas:meta])*
|
|
||||||
fn $function:ident(&mut $this:ident, $value:ident: $ty:ty)
|
|
||||||
$body:block
|
|
||||||
) => {
|
|
||||||
$(#[$metas])*
|
|
||||||
fn $function(&mut $this, $value: $ty)
|
|
||||||
$body
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
||||||
impl S {
|
|
||||||
__impl! {
|
|
||||||
#[ensures(self.value == old(value))]
|
|
||||||
fn set_value(&mut self, value: i32) {
|
|
||||||
self.value = value;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut s = S { value: 24 };
|
|
||||||
s.set_value(42);
|
|
||||||
assert_eq!(s.value, 42);
|
|
||||||
}
|
|
||||||
|
|
@ -1,24 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/.
|
|
||||||
*/
|
|
||||||
|
|
||||||
#[macro_export]
|
|
||||||
macro_rules! debug_checked_precondition {
|
|
||||||
($condition:expr, $($arg:tt)*) => ( debug_assert!($condition, $($arg)*); );
|
|
||||||
}
|
|
||||||
|
|
||||||
#[macro_export]
|
|
||||||
macro_rules! debug_checked_postcondition {
|
|
||||||
($condition:expr, $($arg:tt)*) => ( debug_assert!($condition, $($arg)*); );
|
|
||||||
}
|
|
||||||
|
|
||||||
#[macro_export]
|
|
||||||
macro_rules! checked_precondition {
|
|
||||||
($condition:expr, $($arg:tt)*) => ( assert!($condition, $($arg)*); );
|
|
||||||
}
|
|
||||||
|
|
||||||
#[macro_export]
|
|
||||||
macro_rules! checked_postcondition {
|
|
||||||
($condition:expr, $($arg:tt)*) => ( assert!($condition, $($arg)*); );
|
|
||||||
}
|
|
||||||
|
|
@ -1,42 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_old_simple() {
|
|
||||||
#[ensures(*x == old(*x) + 1, "x increments")]
|
|
||||||
fn incr(x: &mut usize) {
|
|
||||||
*x += 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut val = 0;
|
|
||||||
incr(&mut val);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn test_old_nested() {
|
|
||||||
#[ensures(*x == old(old(old(*x))) + 1, "x increments")]
|
|
||||||
fn incr(x: &mut usize) {
|
|
||||||
*x += 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut val = 0;
|
|
||||||
incr(&mut val);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Post-condition of incr violated")]
|
|
||||||
fn test_violation() {
|
|
||||||
#[ensures(*x == old(*x) + 1, "x increments")]
|
|
||||||
fn incr(x: &mut usize) {
|
|
||||||
*x += 0; // oops
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut val = 0;
|
|
||||||
incr(&mut val);
|
|
||||||
}
|
|
||||||
|
|
@ -1,147 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
//! Test implementing a `RangedInt` type.
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
use std::ops::{Add, Deref};
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[derive(Copy, Clone, Debug)]
|
|
||||||
pub struct Range {
|
|
||||||
min: usize,
|
|
||||||
max: usize,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Range {
|
|
||||||
#[requires(min < max)]
|
|
||||||
pub fn new(min: usize, max: usize) -> Self {
|
|
||||||
Range { min, max }
|
|
||||||
}
|
|
||||||
|
|
||||||
#[ensures(ret.min == self.min.min(other.min))]
|
|
||||||
#[ensures(ret.max == self.max.max(other.max))]
|
|
||||||
pub fn merge(self, other: Range) -> Range {
|
|
||||||
let min = self.min.min(other.min);
|
|
||||||
let max = self.max.max(other.max);
|
|
||||||
|
|
||||||
Range::new(min, max)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn contains(self, val: usize) -> bool {
|
|
||||||
self.min <= val && val <= self.max
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Copy, Clone, Debug)]
|
|
||||||
pub struct RangedInt {
|
|
||||||
range: Range,
|
|
||||||
value: usize,
|
|
||||||
}
|
|
||||||
|
|
||||||
#[invariant(self.range.contains(self.value))]
|
|
||||||
impl RangedInt {
|
|
||||||
#[requires(range.contains(val))]
|
|
||||||
pub fn new(range: Range, val: usize) -> Self {
|
|
||||||
RangedInt { range, value: val }
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn to_usize(self) -> usize {
|
|
||||||
self.value
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn range(self) -> Range {
|
|
||||||
self.range
|
|
||||||
}
|
|
||||||
|
|
||||||
#[ensures(ret.range.contains(ret.value))]
|
|
||||||
pub fn extend(self, range: Range) -> Self {
|
|
||||||
let new_range = self.range.merge(range);
|
|
||||||
|
|
||||||
RangedInt::new(new_range, self.value)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Add<Self> for RangedInt {
|
|
||||||
type Output = RangedInt;
|
|
||||||
|
|
||||||
#[requires(self.range.merge(rhs.range).contains(self.value + rhs.value))]
|
|
||||||
#[ensures(ret.range.contains(ret.value))]
|
|
||||||
#[ensures(ret.value == self.value + rhs.value)]
|
|
||||||
fn add(self, rhs: Self) -> Self::Output {
|
|
||||||
let mut new_ranged = self.extend(rhs.range);
|
|
||||||
|
|
||||||
new_ranged.value += rhs.value;
|
|
||||||
|
|
||||||
new_ranged
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Add<usize> for RangedInt {
|
|
||||||
type Output = RangedInt;
|
|
||||||
|
|
||||||
#[requires(self.range.contains(rhs))]
|
|
||||||
#[ensures(ret.value == self.value + rhs)]
|
|
||||||
fn add(self, rhs: usize) -> Self::Output {
|
|
||||||
let mut new = self;
|
|
||||||
new.value += rhs;
|
|
||||||
new
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Deref for RangedInt {
|
|
||||||
type Target = usize;
|
|
||||||
|
|
||||||
fn deref(&self) -> &Self::Target {
|
|
||||||
&self.value
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn ranged_int_add() {
|
|
||||||
let days = RangedInt::new(Range::new(0, 6), 0);
|
|
||||||
|
|
||||||
assert_eq!(*days, 0);
|
|
||||||
|
|
||||||
assert_eq!(*(days + 1), 1);
|
|
||||||
assert_eq!(*(days + 5), 5);
|
|
||||||
assert_eq!(*(days + 6), 6);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn ranged_int_add_reassign() {
|
|
||||||
let mut days = RangedInt::new(Range::new(0, 6), 0);
|
|
||||||
assert_eq!(*days, 0);
|
|
||||||
|
|
||||||
days = days + 3;
|
|
||||||
assert_eq!(*days, 3);
|
|
||||||
|
|
||||||
days = days + 2;
|
|
||||||
assert_eq!(*days, 5);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Pre-condition of add violated")]
|
|
||||||
fn ranged_overflow() {
|
|
||||||
let days = RangedInt::new(Range::new(0, 6), 0);
|
|
||||||
|
|
||||||
// cause overflow
|
|
||||||
let _ = days + 7;
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Pre-condition of new violated")]
|
|
||||||
fn construction_underflow() {
|
|
||||||
// value below of permitted range
|
|
||||||
RangedInt::new(Range::new(4, 6), 0);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic(expected = "Pre-condition of new violated")]
|
|
||||||
fn construction_overflow() {
|
|
||||||
// value above of permitted range
|
|
||||||
RangedInt::new(Range::new(0, 6), 8);
|
|
||||||
}
|
|
||||||
|
|
@ -1,79 +0,0 @@
|
||||||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
||||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
||||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
||||||
|
|
||||||
use contracts::*;
|
|
||||||
|
|
||||||
#[cfg(feature = "mirai_assertions")]
|
|
||||||
mod mirai_assertion_mocks;
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn adder_example() {
|
|
||||||
#[contract_trait]
|
|
||||||
trait Adder {
|
|
||||||
fn tell(&self) -> usize;
|
|
||||||
|
|
||||||
#[requires((self.tell() + val) < 20)]
|
|
||||||
fn add(&mut self, val: usize);
|
|
||||||
}
|
|
||||||
|
|
||||||
struct MyAdder(usize);
|
|
||||||
|
|
||||||
#[contract_trait]
|
|
||||||
impl Adder for MyAdder {
|
|
||||||
fn tell(&self) -> usize {
|
|
||||||
self.0
|
|
||||||
}
|
|
||||||
|
|
||||||
fn add(&mut self, val: usize) {
|
|
||||||
self.0 += val;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut add = MyAdder(0);
|
|
||||||
|
|
||||||
add.add(3);
|
|
||||||
add.add(16);
|
|
||||||
|
|
||||||
// this would violate the contract
|
|
||||||
// add.add(2);
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn interpolate_example() {
|
|
||||||
#[contract_trait]
|
|
||||||
trait Interpolate {
|
|
||||||
#[requires(0.0 <= val, val <= 1.0)]
|
|
||||||
#[requires(min < max)]
|
|
||||||
#[ensures(min <= ret, ret <= max)]
|
|
||||||
fn interpolate(min: f64, max: f64, val: f64) -> f64;
|
|
||||||
}
|
|
||||||
|
|
||||||
struct Linear;
|
|
||||||
|
|
||||||
#[contract_trait]
|
|
||||||
impl Interpolate for Linear {
|
|
||||||
fn interpolate(min: f64, max: f64, val: f64) -> f64 {
|
|
||||||
min + (val * (max - min))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
struct Quadratic;
|
|
||||||
|
|
||||||
#[contract_trait]
|
|
||||||
impl Interpolate for Quadratic {
|
|
||||||
fn interpolate(min: f64, max: f64, val: f64) -> f64 {
|
|
||||||
let val = val * val;
|
|
||||||
|
|
||||||
Linear::interpolate(min, max, val)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let min = 12.00;
|
|
||||||
let max = 24.00;
|
|
||||||
|
|
||||||
let val = 0.4;
|
|
||||||
|
|
||||||
Linear::interpolate(min, max, val);
|
|
||||||
Quadratic::interpolate(min, max, val);
|
|
||||||
}
|
|
||||||
Loading…
Reference in New Issue