prusti-dev
prusti-dev copied to clipboard
viperproject
Support for library contracts
Summary: Automatically import specifications from dependency crates and inline them when respective functions or types are referenced in the current crate.
This eliminates the need for #[extern_spec] blocks for declarations in other crates as long as the crates are compiled in the same cargo session.
With the proposed changes, the following verifies:
prusti-tests/tests/cargo_verify/library_contracts_test/src/main.rs:
extern crate prusti_contracts;
extern crate library_contracts_lib;
use library_contracts_lib::Opt;
// Demonstrating library contracts: the following specification is imported
// and thus the #[extern_spec] block is not needed
/*
use prusti_contracts::*;
#[extern_spec]
impl<T> Opt<T> {
#[ensures(matches!(*self, Opt::OSome(_)) == result)]
fn is_some(&self) -> bool;
}
*/
fn main() {
let a = Opt::OSome(42);
let b = Opt::ONone::<i32>;
assert!(a.is_some() == true);
assert!(b.is_some() == false);
}
Closes #2
TO-DO:
- [x] Load specs only from dependency crates instead of loading all compiled crates
- [x] Ensure that serialized specs are usable across subsequent builds
@jjurm also try changing the CLEAR_CROSS_CRATE flag to see what it does, I have no idea but maybe it'll help with the recompilation issue?
If you have time, could you also try to fix the crash I've introduced now - I didn't have time now before going on holiday
By the way, will this functionality also work for items that are both in core and std? For example, the method core::mem::swap is also re-exported as std::mem::swap by the standard library. If an #[extern_spec] is defined for one of these paths, will it also automatically work for the other? This is handy for #![no_std] crates that are verified with Prusti, which typically import everything from the core::* namespace instead of from the std::* namespace.
@Pointerbender This discussion is starting to overlap quite a bit with @juliand665's thesis. (Also for that reason @jjurm the solution in this PR does not yet have to be perfect.) Our plan is indeed to support both core and std, maybe in addition to some third-party libraries. For more info, see the project description.
As you say, std re-rexports many modules from core, e.g. here for Option. Because extern specs bind to a method by its DefId, then the methods of option are the one and the same, no matter what path you used to access them.
Ooof... this should be ready to merge now if CI checks pass. If you want, we can discuss a bit before then @Aurel300?
Generally looks good! I wish it wasn't a PR that combined so many changes:
- support cross-crate specs;
- refactor build process for loading
prusti-contractsand core/std specs; - refactor
Environmentinto separate parts (+ adapt rest of codebase).
Although you documented MIN_PRUSTI_VERSION, I think we should document the contracts feature/crate more thoroughly in the user guide, as there are probably some pitfalls. We can push that onto another PR though, since this one is large and will easily get into conflicts.
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "Published by a pub.dev verified publisher"){kind=small}