viperproject / prusti-dev Goto Github PK

View Code? Open in Web Editor NEW

1.5K 18.0 98.0 1.29 GB

A static verifier for Rust, based on the Viper verification infrastructure.

Home Page: http://prusti.org

License: Other

Shell 0.02% Rust 99.33% Python 0.51% Dockerfile 0.05% Nix 0.08% C 0.01%

rust verification viper formal-verification

prusti-dev's Introduction

Prusti

Prusti is a prototype verifier for Rust that makes it possible to formally prove absence of bugs and correctness of code contracts. Internally, Prusti builds upon the Viper verification infrastructure.

By default Prusti verifies absence of integer overflows and panics, proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be disabled with a configuration flag, treating all integers as unbounded. In Prusti, the functional behaviour of functions and external libraries can be specified by using annotations, among which are preconditions, postconditions, and loop invariants. The tool checks them, reporting error messages when the code does not adhere to the provided specification.

Useful links

💻 VS Code extension to use Prusti from your IDE.
📖 User guide, containing installation instructions, a guided tutorial and a description of various verification features.
👩‍💻 Developer guide, intended for new contributors. If you want to help, check our good first issues.
📚 List of publications. To cite the Prusti verifier, please use this BibTeX entry.
📽️ Presentation of Prusti's research project. It includes a demo.
⚖️ License of the source code (Mozilla Public License Version 2.0, for code authored by us).
💬 Do you still have questions? Open an issue or contact us on the Zulip chat.

Getting Prusti

The easiest way to try out Prusti is by using the "Prusti Assistant" extension for VS Code. See the requirements and the troubleshooting section in its readme.

Alternatively, if you wish to use Prusti from the command line there are three options:

Download the precompiled binaries for Ubuntu, Windows, or macOS from a GitHub release.
Compile from the source code, by installing rustup, running ./x.py setup and then ./x.py build --release.
(unmaintained) Build a Docker image from this Dockerfile.

All three options provide the prusti-rustc and cargo-prusti programs that can be used analogously to, respectively, rustc and cargo build. For more detailed instructions, refer to the guides linked above.

Quick example

Take the following program:

/// A monotonically increasing discrete function, with domain [0, domain_size)
trait Function {
  fn domain_size(&self) -> usize;
  fn eval(&self, x: usize) -> i32;
}

/// Find the `x` s.t. `f(x) == target`
fn bisect<T: Function>(f: &T, target: i32) -> Option<usize> {
  let mut low = 0;
  let mut high = f.domain_size();
  while low < high {
    let mid = (low + high) / 2;
    let mid_val = f.eval(mid);
    if mid_val < target {
      low = mid + 1;
    } else if mid_val > target {
      high = mid;
    } else {
      return Some(mid)
    }
  }
  None
}

Run Prusti. You get the following error:

error: [Prusti: verification error] assertion might fail with "attempt to add with overflow"
  --> example.rs:12:15
   |
12 |     let mid = (low + high) / 2;
   |               ^^^^^^^^^^^^

Verification failed

Fix the buggy line with let mid = low + ((high - low) / 2);
Run Prusti. Now the bisect function verifies.

Congratulations! You just proved absence of panics and integer overflows in the bisect function. To additionally prove that the result is correct (i.e. such that f(x) == target), see this example.

prusti-dev's People

Contributors

Stargazers

Watchers

Forkers

karroffel alevy mario-bucev zeta1999 xldenis jorajeev corvinux sapphire-arches f4z3r juliand665 karlosss frececroka karenhong ckamueller eqfy aurel300 fabianwolff aakp10 yichaolemon elowis tillarnold shadow5tepper cedihegi kammola teymour-aldridge gavinleroy mabbamog isgasho dario23 rw zgrannan matklad definoob lukfried jmc-figueira ldy1998 maxwell-yang-2001 ani003 sledgehammervampire jyizheng plsyssec fibletype ejconlon emlaufer jonasalaif philippeitis repos-rust pointerbender spacejam vl0w kasraf pascal-huber jm4ier omar0tarek mlimbeck mohammadhossam zhoudongxu dewert99 rmehri01 markusdemedeiros jjurm pialex99 quinndiggity achyutha bornchanger gmh5225 srikwit hominee a-kenji gadiguibou oyelowo hiroki-chen mars-research meyerzinn frewsxcv patrick-6 jscissr jakuj jthomme1 simon-hrabec securecitizens dgateley dboures tv42 vfukala iq-scm floriangru binadamu-isiyoonekana wenhuizhang simon-hostettler janushannesarson jamestiotio pixelshot91 posticarus trktby nshyrei

prusti-dev's Issues

Failing crates in the top-500 test

There are a few crates on which cargo-prusti fails, as reported in the top-500 test.

Panic

'not yet implemented: TyParam(T/#0)', prusti-viper/src/encoder/type_encoder.rs:128:22

074_futures
111_num-complex
342_euclid
348_cgmath

Consistency error

No matching identifier equals$__$TY$__m_log$$Level$opensqu$0$closesqu$$beg$end$m_log$$LevelFilter$opensqu$0$closesqu$$beg$end$$bool$ found of type Function

002_log
423_h2

Unregistered verification error

[function.not.wellformed:insufficient.permission] Function might not be well-formed. There might be insufficient permission to access _arg.f$0.

341_winit

Timeout

033_unicode-normalization (see issue #77)

Passing two references as arguments triggers panic

This causes Prusti to panic:

use prusti_contracts::*;

struct Point { x: u32, y: u32 }

fn foo<'a, 'b>(p: &'a mut Point, q: &'b mut Point) -> &'a mut u32 {
    &mut p.x
}

fn main(){}

Variable not treated as read-only

The following program does not verify, but it should.

extern crate prusti_contracts;

#[pure]
#[requires="n <= 999999"]
fn closed_form(n: u64) -> u64 {
    n * (n + 1) / 2
}

#[requires="n <= 999999"]
#[ensures = "result == closed_form(n)"]
fn iter_form(n: u64) -> u64 {
    let mut i = 1;
    let mut acc = 0;
    // #[invariant = "n == old(n)"] // workaround
    #[invariant = "1 <= i && i <= n + 1"]
    #[invariant = "acc == closed_form(i - 1)"]
    while i <= n {
        acc += i;
        i += 1;
    }
    acc
}

A temporary workaround is to add n == old(n) to the loop invariant.

Panic when reassigning reference with explicit type information

This causes Prusti to panic:

fn test() {
    let p = 0;
    let q = 1;
    let mut x: &u32 = &p;
    x = &q;
}

When I remove the type annotation from x, it works. The generated MIR is actually different. With the type annotation, it looks like this:

_1 = const 0u32;
_2 = const 1u32;

// first assignment
_4 = &'2rv _1;
_3 = &'3rv (*_4);

// second assignment
_5 = &'4rv _2;
_3 = &'5rv (*_5);

Without, it looks like this:

_1 = const 0u32;
_2 = const 1u32;

// first assignment
_3 = &'2rv _1;

// second assignment
_4 = &'3rv _2;
_3 = &'4rv (*_4);

Provide links to the documentation in syntax/type error messages

We can expect that a large portion of our users have used some similar tool before and, therefore, have an intuition what constructs they should be able to use. However, it can be hard for them to find what is the correct syntax; for example, many tools use different syntax for quantifiers. The Rust compiler has a quite nice job here by giving suggestions and links to the documentation in syntax errors. We should do the same: for example, if we observe the keyword forall used incorrectly, we could emit a link to the documentation that explains how to use this construct.

Viper error: Unfolding u32(_3) might fail

The following program fails with "error: [Prusti internal error] unregistered verification error: [unfold.failed:insufficient.permission] Unfolding u32(_3) might fail. There might be insufficient permission to access u32(_3)."

#![feature(nll)]
extern crate prusti_contracts;

fn use_node(x: &mut u32) {}

fn conditional_borrowing(y: u32, z: u32) {
    let mut y = y;
    let mut z = z;
    let mut b = true;
    let mut x = &mut y;
    
    if b {
        x = &mut z;
    }

    b = false;
    use_node(x);
}

fn main() {}

Atom plugin?

Since some integration with VSCode was done, I wonder if the same can be done for Atom, and what modules would need to be integrated.

Avoid calling compute_definitely_initialized multiple times

compute_definitely_initialized is an expensive function, which is currently called from multiple places (LoopEncoder, PoloniusInfo, InitInfo). We should just do the call once, reusing the result.

Warn about non-pure function calls in specifications

Prusti should detect calls of non-pure functions in specifications, and generate a proper error message for them.

Currently, Prusti panics on programs like the following.

extern crate prusti_contracts;

// #[pure] // good: mark this function as pure
fn get_true() -> bool {
    true
}

#[requires="get_true()"] // bad: this contract calls a non-pure function
fn main(){
    assert!(true);
}

Clarify failing postcondition of trait method

In the following program Prusti identifies a verification error as expected: the method implementation A::bar does not specify a postcondition, so it gets by default the result > 10 from the trait definition, but the implementation returns 0. The error message currently points to the failing postcondition in the trait definition, but this is ambiguous because there are multiple types that implement that trait, and it's not immediately clear which of them is involved in the error.

The error message should use as primary span the fn baz() -> usize in the method implementation, excluding the method's body { .. } to keep the span short and readable.

extern crate prusti_contracts;

trait Foo {
    #[ensures="result > 10"] // Failing postcondition. The verification error is currently reported here.
    fn bar() -> usize;
}

struct A;

impl Foo for A {
    fn bar() -> usize { // Bad implementation. The verification error should be reported here.
        0
    }
}

struct B;

impl Foo for B {
    fn bar() -> usize { // Correct implementation
        100
    }
}

fn main(){}

Prusti panic involving mutable references and loops

This causes Prusti to enter unreachable code:

extern crate prusti_contracts;

fn walk(xs: &mut u32) {
    let ys = xs;
    while true {
        *ys;
    }
}

All four components (mutable reference, assignment, loop, dereference) seem to be important. The backtrace:

thread 'main' panicked at 'internal error: entered unreachable code', prusti-viper/src/encoder/foldunfold/branch_ctxt.rs:839:41
stack backtrace:
...
 6: std::panicking::begin_panic
 7: <core::iter::FlatMap<I, U, F> as core::iter::iterator::Iterator>::next
 8: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
 9: prusti_viper::encoder::foldunfold::branch_ctxt::BranchCtxt::obtain_permissions
10: <prusti_viper::encoder::foldunfold::FoldUnfold<'p, 'v, 'r, 'a, 'tcx> as prusti_viper::encoder::vir::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::branch_ctxt::BranchCtxt<'p>, alloc::vec::Vec<prusti_viper::encoder::foldunfold::action::Action>>>::replace_stmt
11: prusti_viper::encoder::foldunfold::add_fold_unfold
12: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
13: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
14: prusti_viper::verifier::Verifier::verify
15: prusti::verifier::verify
...

Update to latest

I've noticed prusti uses some fairly old versions of both dependencies (i.e. env_logger 0.5, while latest is 0.7) and rustc itself (1.28 nightly, while we are at 1.38 stable and 1.40 nightly). While the former is not that huge a deal, the latter restricts users to old language versions.

I understand that since prusti uses unstable, internal APIs, any update is bound to take time and effort. Just putting this here as a feature request/tracking issue.

Panic when calling a function that returns an Option of a reference

The program below causes Prusti to panic:

use prusti_contracts::*;

struct S(usize);

#[trusted]
fn foo(s: &S) -> Option<&S> { // succeeds for Option<S>
    None
}

fn bar(s: &S) {        
    let x = foo(s); // crashes
}

fn main(){}

The reported error message is the following:

thread 'main' panicked at 'assertion failed: `(left == right)`

Diff < left / right > :
<2
>1

Support domains

It would be useful to lift Viper's domains to Prusti. One of the main questions is the language design for that, for instance, to what extent we can build on existing Rust features. Instead of general domains, we might also want to provide a more limited feature such as ADTs.

Prusti for crypto?

In hacl-star/hacl-star#277 I describe the seed of a proposal to apply verification in Rust to verified crypto.

Project everest is a verified cryptographic library and associated tooling in F* that embeds a restricted set of C (Low*) and x64 assembly (Vale), reasons about registers and memory model, alongside symbolic execution and tries to ensure that a highly optimised and often opaque cryptographic implementation conforms to a spec, which can be written in a more transparent form.

Here is the state of crypto in Rust:

Rust is used extensively in the blockchain community for cryptographic implementation due to it's type safety and competitive performance with C++/C. A lot of new crypto (MPC, pairings, aggregated signatures, VDFs) is being implemented by this community. Just like with candidate post-quantum crypto, this presents an opportunity to test how verification applies to a wider subset of crypto.

I am wondering what the state of Prusti is, and what limitations might exist in pursuing such a project.

Crash when verifying unsupported types

This program

extern crate prusti_contracts;

#[requires="a != 0f64"]
#[ensures="a*result + b == 0f64"]
fn solve(a: f64, b: f64) -> f64 {
    -b/a
}

fn main() {
    solve(5f64, 2f64);
}

crashes with

thread 'main' panicked at 'not yet implemented: TyFloat(f64)', prusti-viper/src/encoder/type_encoder.rs:445:22

error: internal compiler error: unexpected panic

but the panic here is expected, since the type is not supported. Maybe a better error message can do it?

Possibility of verifying SYCL?

Is it possible the project may be extended to SYCL, the cross-platform parallel language standard (Khronos group) that is now being supported as flagship product by Intel through OneAPI and also has support throughout industry?

(for instance SYCL is integrated with full support as a backend to tensorflow, Xilinx is working on it too)

I ask because there seems to be an active attempt to verify "parallel and concurrent software" in vercors

Are there any particular reasons why Viper IR would be particularly suited to this task compared to other available options?

Prusti generating illegal Viper code when overflow checking is enabled

I have a Prusti.toml file with
CHECK_BINARY_OPERATIONS = true
Prusti then panics with the following program

extern crate prusti_contracts;

#[requires = "x > 0"]
fn int_sqrt(x: i32) -> i32 {
    let mut r = 0;

    #[invariant = "(r * r) <= x"]
    while (r + 1) * (r + 1) <= x {
        r += 1;
    }

    r
}

fn main() {}

Commenting out the definition of CHECK_BINARY_OPERATIONS in Prusti.toml makes the panic go away, but then it complains about overflow, which is also strange, as the default behavior should be not to check for overflow.

Failed initial build

When doing a make build, the build does not succeed due to Error: no class 'viper.silver.ast.NamedDomainAxiom'.

I am running the build on Ubuntu 16.04 (as described in the README), with all requirements and build steps mentioned inthe README being satisfied.

Any suggestions on how to fix this?

Click to expand the full build output

    Updating registry `https://github.com/rust-lang/crates.io-index`
    Updating git repository `https://github.com/fpoli/compiletest-rs.git`
 Downloading log v0.4.5
 Downloading jni v0.11.0
 Downloading uuid v0.7.1
 Downloading error-chain v0.12.0
 Downloading cfg-if v0.1.5
 Downloading combine v3.5.2
 Downloading cesu8 v1.1.0
 Downloading jni-sys v0.3.0
 Downloading backtrace v0.3.9
 Downloading backtrace-sys v0.1.24
 Downloading libc v0.2.43
 Downloading rustc-demangle v0.1.9
 Downloading cc v1.0.25
 Downloading byteorder v1.2.6
 Downloading memchr v2.1.0
 Downloading unreachable v1.0.0
 Downloading ascii v0.7.1
 Downloading either v1.5.0
 Downloading version_check v0.1.4
 Downloading void v1.0.2
 Downloading walkdir v2.2.5
 Downloading same-file v1.0.3
 Downloading rand v0.5.5
 Downloading rand_core v0.2.1
 Downloading env_logger v0.5.13
 Downloading humantime v1.1.1
 Downloading atty v0.2.11
 Downloading termcolor v1.0.4
 Downloading regex v1.0.5
 Downloading quick-error v1.2.2
 Downloading utf8-ranges v1.0.1
 Downloading thread_local v0.3.6
 Downloading aho-corasick v0.6.8
 Downloading regex-syntax v0.6.2
 Downloading lazy_static v1.1.0
 Downloading ucd-util v0.1.1
 Downloading reqwest v0.9.2
 Downloading tempdir v0.3.7
 Downloading tokio v0.1.8
 Downloading serde_urlencoded v0.5.3
 Downloading mime v0.3.9
 Downloading encoding_rs v0.8.6
 Downloading mime_guess v2.0.0-alpha.6
 Downloading native-tls v0.2.1
 Downloading base64 v0.9.3
 Downloading serde_json v1.0.32
 Downloading serde v1.0.80
 Downloading futures v0.1.24
 Downloading tokio-io v0.1.8
 Downloading http v0.1.13
 Downloading libflate v0.1.18
 Downloading url v1.7.1
 Downloading hyper v0.12.11
 Downloading bytes v0.4.10
 Downloading hyper-tls v0.3.0
 Downloading tokio-codec v0.1.0
 Downloading tokio-current-thread v0.1.1
 Downloading tokio-uds v0.2.1
 Downloading mio v0.6.16
 Downloading tokio-udp v0.1.2
 Downloading tokio-executor v0.1.4
 Downloading tokio-timer v0.2.6
 Downloading tokio-threadpool v0.1.6
 Downloading tokio-tcp v0.1.1
 Downloading tokio-reactor v0.1.5
 Downloading tokio-fs v0.1.3
 Downloading iovec v0.1.2
 Downloading mio-uds v0.6.7
 Downloading slab v0.4.1
 Downloading net2 v0.2.33
 Downloading lazycell v1.2.0
 Downloading parking_lot v0.6.4
 Downloading num_cpus v1.8.0
 Downloading crossbeam-utils v0.5.0
 Downloading lock_api v0.1.3
 Downloading parking_lot_core v0.3.1
 Downloading owning_ref v0.3.3
 Downloading scopeguard v0.3.3
 Downloading stable_deref_trait v1.1.1
 Downloading smallvec v0.6.5
 Downloading rustc_version v0.2.3
 Downloading semver v0.9.0
 Downloading semver-parser v0.7.0
 Downloading crossbeam-deque v0.6.1
 Downloading crossbeam-epoch v0.5.2
 Downloading arrayvec v0.4.7
 Downloading memoffset v0.2.1
 Downloading nodrop v0.1.12
 Downloading itoa v0.4.3
 Downloading dtoa v0.4.3
 Downloading idna v0.1.5
 Downloading matches v0.1.8
 Downloading percent-encoding v1.0.1
 Downloading unicode-bidi v0.3.4
 Downloading unicode-normalization v0.1.7
 Downloading unicase v2.1.0
 Downloading unicase v1.4.2
 Downloading phf v0.7.23
 Downloading phf_shared v0.7.23
 Downloading siphasher v0.2.3
 Downloading phf_codegen v0.7.23
 Downloading phf_generator v0.7.23
 Downloading openssl v0.10.12
 Downloading openssl-sys v0.9.36
 Downloading openssl-probe v0.1.2
 Downloading foreign-types v0.3.2
 Downloading bitflags v1.0.4
 Downloading foreign-types-shared v0.1.1
 Downloading pkg-config v0.3.14
 Downloading safemem v0.3.0
 Downloading ryu v0.2.6
 Downloading fnv v1.0.6
 Downloading adler32 v1.0.3
 Downloading crc v1.8.1
 Downloading build_const v0.2.1
 Downloading h2 v0.1.12
 Downloading httparse v1.3.2
 Downloading want v0.0.6
 Downloading futures-cpupool v0.1.8
 Downloading time v0.1.40
 Downloading indexmap v1.0.1
 Downloading string v0.1.1
 Downloading try-lock v0.2.2
 Downloading rand v0.4.3
 Downloading remove_dir_all v0.5.1
 Downloading polonius-engine v0.5.0
 Downloading serde_derive v1.0.80
 Downloading csv v1.0.1
 Downloading polonius v0.2.0
 Downloading config v0.9.1
 Downloading rustc-hash v1.0.1
 Downloading datafrog v0.1.0
 Downloading quote v0.6.8
 Downloading syn v0.15.4
 Downloading proc-macro2 v0.4.19
 Downloading unicode-xid v0.1.0
 Downloading csv-core v0.1.4
 Downloading histo v0.1.0
 Downloading clap v2.32.0
 Downloading failure v0.1.2
 Downloading polonius-parser v0.1.0
 Downloading structopt v0.2.10
 Downloading streaming-stats v0.1.29
 Downloading num-traits v0.2.6
 Downloading strsim v0.7.0
 Downloading ansi_term v0.11.0
 Downloading textwrap v0.10.0
 Downloading vec_map v0.8.1
 Downloading unicode-width v0.1.5
 Downloading failure_derive v0.1.2
 Downloading syn v0.14.9
 Downloading synstructure v0.9.0
 Downloading lalrpop-util v0.15.2
 Downloading lalrpop v0.15.2
 Downloading regex-syntax v0.4.2
 Downloading regex v0.2.11
 Downloading digest v0.7.5
 Downloading diff v0.1.11
 Downloading string_cache v0.7.3
 Downloading atty v0.1.2
 Downloading ascii-canvas v1.0.0
 Downloading ena v0.5.0
 Downloading sha2 v0.7.1
 Downloading term v0.4.6
 Downloading bit-set v0.4.0
 Downloading docopt v0.8.3
 Downloading itertools v0.7.8
 Downloading petgraph v0.4.13
 Downloading regex-syntax v0.5.6
 Downloading generic-array v0.9.0
 Downloading typenum v1.10.0
 Downloading string_cache_shared v0.3.0
 Downloading precomputed-hash v0.1.1
 Downloading new_debug_unreachable v1.0.1
 Downloading string_cache_codegen v0.4.1
 Downloading quote v0.5.2
 Downloading proc-macro2 v0.3.8
 Downloading winapi v0.2.8
 Downloading kernel32-sys v0.2.2
 Downloading winapi-build v0.1.1
 Downloading block-buffer v0.3.3
 Downloading fake-simd v0.1.2
 Downloading byte-tools v0.2.0
 Downloading arrayref v0.3.5
 Downloading bit-vec v0.4.4
 Downloading strsim v0.6.0
 Downloading fixedbitset v0.1.9
 Downloading ordermap v0.3.5
 Downloading lalrpop-snap v0.15.2
 Downloading structopt-derive v0.2.10
 Downloading yaml-rust v0.4.2
 Downloading nom v4.0.0
 Downloading rust-ini v0.12.2
 Downloading toml v0.4.7
 Downloading serde-hjson v0.8.1
 Downloading linked-hash-map v0.5.1
 Downloading regex v0.1.80
 Downloading serde v0.8.23
 Downloading linked-hash-map v0.3.0
 Downloading lazy_static v0.2.11
 Downloading num-traits v0.1.43
 Downloading aho-corasick v0.5.3
 Downloading utf8-ranges v0.1.3
 Downloading memchr v0.1.11
 Downloading regex-syntax v0.3.9
 Downloading thread_local v0.2.7
 Downloading thread-id v2.0.0
 Downloading serde_test v0.8.23
 Downloading num-rational v0.2.1
 Downloading pretty_assertions v0.5.1
 Downloading num-integer v0.1.39
 Downloading num-bigint v0.2.0
 Downloading difference v2.0.0
 Downloading chrono v0.4.6
   Compiling version_check v0.1.4
   Compiling siphasher v0.2.3
   Compiling semver-parser v0.7.0
   Compiling unicode-xid v0.1.0
   Compiling libc v0.2.43
   Compiling rand_core v0.2.1
   Compiling void v1.0.2
   Compiling string_cache_shared v0.3.0
   Compiling winapi-build v0.1.1
   Compiling nodrop v0.1.12
   Compiling cfg-if v0.1.5
   Compiling proc-macro2 v0.4.19
   Compiling serde v1.0.80
   Compiling stable_deref_trait v1.1.1
   Compiling regex v0.2.11
   Compiling ucd-util v0.1.1
   Compiling byteorder v1.2.6
   Compiling typenum v1.10.0
   Compiling memoffset v0.2.1
   Compiling winapi v0.2.8
   Compiling crossbeam-utils v0.5.0
   Compiling scopeguard v0.3.3
   Compiling bit-vec v0.4.4
   Compiling either v1.5.0
   Compiling lazycell v1.2.0
   Compiling slab v0.4.1
   Compiling fixedbitset v0.1.9
   Compiling futures v0.1.24
   Compiling pkg-config v0.3.14
   Compiling term v0.4.6
   Compiling utf8-ranges v1.0.1
   Compiling cc v1.0.25
   Compiling ordermap v0.3.5
   Compiling precomputed-hash v0.1.1
   Compiling diff v0.1.11
   Compiling ena v0.5.0
   Compiling lalrpop-util v0.15.2
   Compiling regex-syntax v0.4.2
   Compiling matches v0.1.8
   Compiling build_const v0.2.1
   Compiling same-file v1.0.3
   Compiling foreign-types-shared v0.1.1
   Compiling byte-tools v0.2.0
   Compiling openssl v0.10.12
   Compiling arrayref v0.3.5
   Compiling fnv v1.0.6
   Compiling itoa v0.4.3
   Compiling httparse v1.3.2
   Compiling string v0.1.1
   Compiling fake-simd v0.1.2
   Compiling try-lock v0.2.2
   Compiling indexmap v1.0.1
   Compiling strsim v0.6.0
   Compiling native-tls v0.2.1
   Compiling rustc-demangle v0.1.9
   Compiling unicode-normalization v0.1.7
   Compiling bitflags v1.0.4
   Compiling ryu v0.2.6
   Compiling percent-encoding v1.0.1
   Compiling ascii v0.7.1
   Compiling num-traits v0.2.6
   Compiling openssl-probe v0.1.2
   Compiling regex v1.0.5
   Compiling unicode-width v0.1.5
   Compiling adler32 v1.0.3
   Compiling jni-sys v0.3.0
   Compiling cesu8 v1.1.0
   Compiling quick-error v1.2.2
   Compiling dtoa v0.4.3
   Compiling safemem v0.3.0
   Compiling failure_derive v0.1.2
   Compiling serde v0.8.23
   Compiling ansi_term v0.11.0
   Compiling strsim v0.7.0
   Compiling remove_dir_all v0.5.1
   Compiling vec_map v0.8.1
   Compiling utf8-ranges v0.1.3
   Compiling termcolor v1.0.4
   Compiling regex-syntax v0.3.9
   Compiling linked-hash-map v0.5.1
   Compiling datafrog v0.1.0
   Compiling num-integer v0.1.39
   Compiling lazy_static v0.2.11
   Compiling rust-ini v0.12.2
   Compiling num-bigint v0.2.0
   Compiling num-rational v0.2.1
   Compiling difference v2.0.0
   Compiling prusti-contracts v0.1.0 (file:///prusti-dev/prusti-contracts)
   Compiling proc-macro2 v0.3.8
   Compiling unicase v1.4.2
   Compiling memchr v2.1.0
   Compiling lazy_static v1.1.0
   Compiling unicase v2.1.0
   Compiling semver v0.9.0
   Compiling unreachable v1.0.0
   Compiling arrayvec v0.4.7
   Compiling log v0.4.5
   Compiling encoding_rs v0.8.6
   Compiling kernel32-sys v0.2.2
   Compiling rand v0.5.5
   Compiling iovec v0.1.2
   Compiling net2 v0.2.33
   Compiling num_cpus v1.8.0
   Compiling time v0.1.40
   Compiling memchr v0.1.11
   Compiling atty v0.2.11
   Compiling rand v0.4.3
   Compiling owning_ref v0.3.3
   Compiling regex-syntax v0.5.6
   Compiling regex-syntax v0.6.2
   Compiling rustc-hash v1.0.1
   Compiling itertools v0.7.8
   Compiling bit-set v0.4.0
   Compiling petgraph v0.4.13
   Compiling ascii-canvas v1.0.0
   Compiling tokio-executor v0.1.4
   Compiling openssl-sys v0.9.36
   Compiling backtrace-sys v0.1.24
   Compiling unicode-bidi v0.3.4
   Compiling crc v1.8.1
   Compiling foreign-types v0.3.2
   Compiling walkdir v2.2.5
   Compiling block-buffer v0.3.3
   Compiling textwrap v0.10.0
   Compiling humantime v1.1.1
   Compiling base64 v0.9.3
   Compiling yaml-rust v0.4.2
   Compiling serde_test v0.8.23
   Compiling pretty_assertions v0.5.1
   Compiling quote v0.5.2
   Compiling rustc_version v0.2.3
   Compiling smallvec v0.6.5
   Compiling new_debug_unreachable v1.0.1
   Compiling want v0.0.6
   Compiling bytes v0.4.10
   Compiling mio v0.6.16
   Compiling futures-cpupool v0.1.8
   Compiling uuid v0.7.1
   Compiling aho-corasick v0.5.3
   Compiling lock_api v0.1.3
   Compiling tempdir v0.3.7
   Compiling polonius-engine v0.5.0
   Compiling tokio-current-thread v0.1.1
   Compiling tokio-timer v0.2.6
   Compiling idna v0.1.5
   Compiling jni v0.11.0
   Compiling clap v2.32.0
   Compiling linked-hash-map v0.3.0
   Compiling parking_lot_core v0.3.1
   Compiling tokio-io v0.1.8
   Compiling http v0.1.13
   Compiling mio-uds v0.6.7
   Compiling generic-array v0.9.0
   Compiling quote v0.6.8
   Compiling url v1.7.1
   Compiling streaming-stats v0.1.29
   Compiling num-traits v0.1.43
   Compiling phf_shared v0.7.23
   Compiling thread_local v0.3.6
   Compiling crossbeam-epoch v0.5.2
   Compiling aho-corasick v0.6.8
   Compiling combine v3.5.2
   Compiling nom v4.0.0
   Compiling csv-core v0.1.4
   Compiling atty v0.1.2
   Compiling thread-id v2.0.0
   Compiling mime v0.3.9
   Compiling tokio-codec v0.1.0
   Compiling digest v0.7.5
   Compiling backtrace v0.3.9
   Compiling libflate v0.1.18
   Compiling syn v0.15.4
   Compiling syn v0.14.9
   Compiling serde_json v1.0.32
   Compiling toml v0.4.7
   Compiling histo v0.1.0
   Compiling phf_generator v0.7.23
   Compiling phf v0.7.23
   Compiling chrono v0.4.6
   Compiling crossbeam-deque v0.6.1
   Compiling serde_urlencoded v0.5.3
   Compiling h2 v0.1.12
   Compiling thread_local v0.2.7
   Compiling csv v1.0.1
   Compiling sha2 v0.7.1
   Compiling error-chain v0.12.0
   Compiling serde_derive v1.0.80
   Compiling synstructure v0.9.0
   Compiling structopt-derive v0.2.10
   Compiling string_cache_codegen v0.4.1
   Compiling phf_codegen v0.7.23
   Compiling prusti v0.1.0 (file:///prusti-dev/prusti)
   Compiling tokio-threadpool v0.1.6
   Compiling regex v0.1.80
   Compiling parking_lot v0.6.4
   Compiling env_logger v0.5.13
   Compiling string_cache v0.7.3
   Compiling mime_guess v2.0.0-alpha.6
   Compiling structopt v0.2.10
   Compiling tokio-fs v0.1.3
   Compiling tokio-reactor v0.1.5
   Compiling serde-hjson v0.8.1
   Compiling docopt v0.8.3
   Compiling jni-gen v0.1.0 (file:///prusti-dev/jni-gen)
   Compiling tokio-udp v0.1.2
   Compiling tokio-tcp v0.1.1
   Compiling tokio-uds v0.2.1
   Compiling failure v0.1.2
   Compiling config v0.9.1
   Compiling tokio v0.1.8
   Compiling lalrpop-snap v0.15.2
   Compiling hyper v0.12.11
   Compiling hyper-tls v0.3.0
   Compiling reqwest v0.9.2
   Compiling viper-sys v0.1.0 (file:///prusti-dev/viper-sys)
   Compiling systest v0.1.0 (file:///prusti-dev/jni-gen/systest)
error: failed to run custom build command for `viper-sys v0.1.0 (file:///prusti-dev/viper-sys)`
process didn't exit successfully: `/prusti-dev/target/debug/build/viper-sys-b2f7008154f8e25e/build-script-build` (exit code: 101)
--- stdout
cargo:rerun-if-changed=build.rs
cargo:rerun-if-env-changed=VIPER_HOME
cargo:rerun-if-changed=/usr/lib/viper/
cargo:rerun-if-changed=/usr/lib/viper/viper.silicon-1.1-SNAPSHOT.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-http-spray-json_2.12-10.1.8.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.ssl-config-core_2.12-0.3.7.jar
cargo:rerun-if-changed=/usr/lib/viper/commons-io.commons-io-2.6.jar
cargo:rerun-if-changed=/usr/lib/viper/com.google.guava.guava-27.0-jre.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.scala-logging.scala-logging_2.12-3.9.0.jar
cargo:rerun-if-changed=/usr/lib/viper/ch.qos.logback.logback-classic-1.2.3.jar
cargo:rerun-if-changed=/usr/lib/viper/ch.qos.logback.logback-core-1.2.3.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scala-lang.scala-library-2.12.7.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.config-1.3.3.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-http-core_2.12-10.1.8.jar
cargo:rerun-if-changed=/usr/lib/viper/io.spray.spray-json_2.12-1.3.5.jar
cargo:rerun-if-changed=/usr/lib/viper/Alloy-5.0.0.1.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-protobuf_2.12-2.5.22.jar
cargo:rerun-if-changed=/usr/lib/viper/com.lihaoyi.sourcecode_2.12-0.1.4.jar
cargo:rerun-if-changed=/usr/lib/viper/org.apache.commons.commons-pool2-2.6.0.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scalactic.scalactic_2.12-3.0.5.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-http_2.12-10.1.8.jar
cargo:rerun-if-changed=/usr/lib/viper/org.slf4j.slf4j-api-1.7.25.jar
cargo:rerun-if-changed=/usr/lib/viper/common.common-0.1.0-SNAPSHOT.jar
cargo:rerun-if-changed=/usr/lib/viper/com.lihaoyi.fastparse_2.12-1.0.0.jar
cargo:rerun-if-changed=/usr/lib/viper/com.google.guava.failureaccess-1.0.jar
cargo:rerun-if-changed=/usr/lib/viper/org.rogach.scallop_2.12-3.1.3.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scala-lang.modules.scala-java8-compat_2.12-0.8.0.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-stream_2.12-2.5.22.jar
cargo:rerun-if-changed=/usr/lib/viper/viper.silver-0.1-SNAPSHOT.jar
cargo:rerun-if-changed=/usr/lib/viper/com.google.errorprone.error_prone_annotations-2.2.0.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scala-lang.modules.scala-parser-combinators_2.12-1.1.1.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-parsing_2.12-10.1.8.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scala-lang.scala-reflect-2.12.7.jar
cargo:rerun-if-changed=/usr/lib/viper/viper.viperserver-1.1-SNAPSHOT.jar
cargo:rerun-if-changed=/usr/lib/viper/com.lihaoyi.fastparse-utils_2.12-1.0.0.jar
cargo:rerun-if-changed=/usr/lib/viper/org.scala-lang.modules.scala-xml_2.12-1.0.6.jar
cargo:rerun-if-changed=/usr/lib/viper/com.typesafe.akka.akka-actor_2.12-2.5.22.jar
cargo:rerun-if-changed=/usr/lib/viper/org.jgrapht.jgrapht-core-1.2.0.jar
cargo:rerun-if-changed=/usr/lib/viper/com.google.j2objc.j2objc-annotations-1.1.jar
cargo:rerun-if-changed=/usr/lib/viper/org.codehaus.mojo.animal-sniffer-annotations-1.17.jar
cargo:rerun-if-changed=/usr/lib/viper/com.google.guava.listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar
cargo:rerun-if-changed=/usr/lib/viper/org.reactivestreams.reactive-streams-1.0.2.jar
cargo:rerun-if-changed=/usr/lib/viper/viper.carbon-1.0-SNAPSHOT.jar

--- stderr
Exception in thread "Thread-0" java.lang.NoClassDefFoundError: viper/silver/ast/NamedDomainAxiom
Caused by: java.lang.ClassNotFoundException: viper.silver.ast.NamedDomainAxiom
	at java.net.URLClassLoader.findClass(URLClassLoader.java:382)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:419)
	at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:352)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:352)
thread 'main' panicked at 'Error: no class 'viper.silver.ast.NamedDomainAxiom'
Caused by: Java exception was thrown
', viper-sys/build.rs:621:13
note: Run with `RUST_BACKTRACE=1` for a backtrace.

warning: build failed, waiting for other jobs to finish...
error: build failed

Prusti attributes do not work across crates

Describe the error
Attributes such as #[pure] or #[requires] are not taken into consideration across multiple crates.

To Reproduce
Unpack the attached .zip file and run cargo-prusti and observe that the #[pure] annotation is assumed to be missing even when it's there.

Alternatively, this is pretty easy to set up manually.

Create a cargo workspace or have two (or more) empty crates available. (at least one of them as a lib-crate)
add the necessary declarations (extern crate prusti_contracts) and have one crate depend on a lib-crate by modifying the Cargo.toml.
Add a function to the lib crate with any prusti-attributes (#[pure], #[requires] and #[ensures] have been tested)
Use the function from the lib crate inside the "consumer" crate in a way that demonstrates if the attributes are respected (using #[pure] function inside of a pre/post-condition, violating the #[requires]-clause or assert!-ing on #[ensures] properties)
Run cargo-prusti and observe that those attributes do not have the desired effect (not marked as #[pure], no #[requires]-violation found or assert! fails)

Expected behavior
Attributes should work across crate boundaries just as they work within a single crate.

Reproduction project or code sample
pure-across-crates.zip

// crate producer
extern crate prusti_contracts;

#[pure]
pub fn five() -> usize {
    5
}

// crate consumer
extern crate prusti_contracts;
extern crate producer;

use producer::five;

#[requires="five() == 5"]
pub fn _test() {}

Software configuration:
Using fpoli/prusti-artefact docker image from 09 July 2019

Missing error messages for unmet Prusti requirements

When compiling Prusti, many things can go wrong. For example:

the JVM is not installed
JAVA_HOME is not set or cannot be found
libjvm.so cannot be found in JAVA_HOME
VIPER_HOME is not set
VIPER_HOME does not contain the Viper jars
the Viper jars don't contain the expected classes

For each of these cases, we should make sure that the compiler reports a helpful error message.

Snapshot equality between empty tuples

Two crates are failing the top-20 test. The error message is

thread 'main' panicked at 'not yet implemented: TyTuple([])', prusti-viper/src/encoder/snapshot_encoder.rs:129:18

I think it's because those crates use empty tuples.

@cmatheja Would it be easy to encode that empty tuples are always equal? The following program outputs true.

fn main() {
    println!("{}", () == ()); // true
}

Carbon cannot verify some loops

Hello!
As far as I've understood, BeginFrame and EndFrame are used in the context of loops, as a way to frame out and frame in currently held permissions. I have noticed that when such a statement is encountered, the effect of framing is applied to the state of Prusti, but not reflected in the emitted code. That is, no inhale and exhale are emitted.

prusti-dev/prusti-viper/src/encoder/foldunfold/mod.rs

Lines 807 to 810 in 134f9f5

 // 5. Apply effect of statement on state 

 debug!("[step.5] replace_stmt: {}", stmt); 

 bctxt.apply_stmt(&stmt); 

 stmts.push(stmt.clone());

I think this would explain why the following program does not verify when using Carbon (Viper file can be found here):

extern crate prusti_contracts;

// ERROR: Unfolding bool(_1) might fail. 
// There might be insufficient permission to access bool(_1). ([email protected])
fn whileok() {
    let mut ok = true;
    while ok {}
}

fn main() {}

In particular, if we look at the following lines of the Viper program:
https://gist.github.com/mario-bucev/b7fb55a6b6bb0d7c8981889bb41f30e4#file-whileok-vpr-L95-L109
we note that inhale acc(bool(_1), read$()) comes from the loop permission invariant, but the fact that we unfold bool(_1) with write is due to the framing in of the permissions (so we get back full permissions, in that case, write).

I don't know if this is an intended behavior, so I am creating this issue.

Thanks :)

Static function used in trait contract is encoded twice to Viper

The following code snippet produces two identical encodings of static_pure in the Viper code. Prusti then panics due to a consistency error in Viper.

Breaking Code

extern crate prusti_contracts;

#[pure]
fn static_pure(val: i32) -> i32 {
    val
}

trait Answer {
    #[ensures="result == static_pure(arg)"]
    fn produce_answer(&self, arg: i32) -> i32;
}

struct DeepThought {}

impl Answer for DeepThought {
    fn produce_answer(&self, arg: i32) -> i32 { arg }
}

fn main() {
    let dt = DeepThought {};
    let val1 = static_pure(42);
    let val2 = dt.produce_answer(42);
    assert!(val1 == val2);
}

Note that produce_answer needs to be defined as a trait function. Implementing it directly on DeepThought does not create the erroneous behaviour. Moreover, the main function needs to be populated as such; removing any statement other than the assert will remove the error.

Prusti Log

  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  |  Hash:  ccf572597ff91ca6c7c
 |      /\   |  \ \__/ .__/  |       /\   |  Build: 2020-04-24 10:57:06

 INFO 2020-04-29T10:21:52Z: prusti::compiler_calls: Parsing of annotations successful (0.0 seconds)
 INFO 2020-04-29T10:21:52Z: prusti::compiler_calls: Type-checking of annotations successful (0.0 seconds)
Verification of 3 items...
 INFO 2020-04-29T10:21:52Z: viper::viper: Using JVM OpenJDK 64-Bit Server VM, Java 11.0.7
 INFO 2020-04-29T10:21:52Z: prusti::verifier: JVM startup (0.3 seconds)
 INFO 2020-04-29T10:21:52Z: viper::verification_context: Using Z3 path: '/usr/bin/viper-z3'
 INFO 2020-04-29T10:21:52Z: viper::verifier: Using backend Silicon version <unknown-build-version>
 INFO 2020-04-29T10:21:53Z: prusti::verifier: Verifier startup (1.62 seconds)
 INFO 2020-04-29T10:21:53Z: prusti_viper::verifier: Received 3 items to be verified:
 INFO 2020-04-29T10:21:53Z: prusti_viper::verifier:  - code::static_pure from code.rs:4:1: 6:2 (code::static_pure[0])
 INFO 2020-04-29T10:21:53Z: prusti_viper::verifier:  - code::main from code.rs:19:1: 24:2 (code::main[0])
 INFO 2020-04-29T10:21:53Z: prusti_viper::verifier:  - <DeepThought as Answer>::produce_answer from code.rs:16:5: 16:54 (code::{{impl}}[0]::produce_answer[0])
 INFO 2020-04-29T10:21:53Z: prusti_viper::encoder::encoder: Encoding: code::static_pure from code.rs:4:1: 6:2 (code::static_pure[0])
 INFO 2020-04-29T10:21:53Z: prusti_viper::encoder::encoder: Encoding: code::main from code.rs:19:1: 24:2 (code::main[0])
 INFO 2020-04-29T10:21:54Z: prusti_viper::encoder::encoder: Encoding: code::static_pure from code.rs:4:1: 6:2 (code::static_pure[0])
 INFO 2020-04-29T10:21:54Z: prusti_viper::encoder::encoder: Encoding: code::static_pure from code.rs:4:1: 6:2 (code::static_pure[0])
 INFO 2020-04-29T10:21:54Z: prusti_viper::encoder::encoder: Encoding: <DeepThought as Answer>::produce_answer from code.rs:16:5: 16:54 (code::{{impl}}[0]::produce_answer[0])
 INFO 2020-04-29T10:21:54Z: prusti_viper::encoder::encoder: Encoding: code::static_pure from code.rs:4:1: 6:2 (code::static_pure[0])
 INFO 2020-04-29T10:21:54Z: prusti_viper::verifier: Encoding to Viper successful (0.15 seconds)
 INFO 2020-04-29T10:21:54Z: prusti_viper::verifier: Viper encoding uses 0 domains, 8 fields, 3 functions, 16 predicates, 5 methods
 INFO 2020-04-29T10:21:54Z: prusti_viper::verifier: Dumping Viper program to '"viper_program"'
 INFO 2020-04-29T10:21:54Z: prusti_viper::verifier: Construction of JVM objects successful (0.40 seconds)
ERROR 2020-04-29T10:21:54Z: viper::verifier: The provided Viper program has 1 consistency errors.
ERROR 2020-04-29T10:21:54Z: viper::verifier: Consistency error: Duplicate identifier m_code$$static_pure$opensqu$0$closesqu$__$TY$__$int$$$int$ found. (<no position>)
thread 'main' panicked at 'Consistency errors. The encoded Viper program is incorrect.', viper/src/verifier.rs:145:13
note: Run with `RUST_BACKTRACE=1` for a backtrace.

error: internal compiler error: unexpected panic

note: the compiler or Prusti unexpectedly panicked.

note: possible reasons include the usage of Rust features that are not supported by Prusti.

note: we would appreciate a bug report for Prusti: <https://github.com/viperproject/prusti-dev/issues>

note: Prusti hash ccf572597ff91ca6c7c built on 2020-04-24 10:57:06

note: rustc <unknown> running on x86_64-unknown-linux-gnu

I am running Prusti inside an ubuntu:bionic docker container.

Add support for quantifying over copy types

Currently, Prusti allows quantification only over primitive types. However, once we have snapshots as part of #53, we could support quantification over Copy types by quantifying over snapshots.

Set toolchain from cargo-prusti

It would be nice to automatically set the RUST_TOOLCHAIN environment variable in the cargo-prusti binary.

Invariants on types behave in unexpected ways.

When using invariants on types, one would imagine the invariant to hold in all visible states. However, it seems that those invariants are only checked at function boundaries that involve the type. Therefore, performing an operation that is based on the invariant right after construction cannot be verified.

extern crate prusti_contracts;

#[invariant="self.0 >= 0"]
struct MyTuple(i32);

fn main() {
    let mut s = MyTuple(-1);        // no error is raised
    s.0 = -200;                     // still no error raised
    assert!(s.0 >= 0);              // error: "asserted expression might not hold"
}

The preceding example provides an error only on the assert!, the only statement that should actually verify. However, it doesn't complain about the object being in an invalid state, neither after construction, nor after direct modification.

Branching re-borrow causes permission error

This can be verified:

extern crate prusti_contracts;

struct Point { x: u32, y: u32 }

fn f1<'a>(p: &'a mut Point) -> &'a mut u32 {
	if p.x == 0 {
		&mut p.x
	} else {
		&mut p.x
	}
}

This fails with an internal encoding error:

extern crate prusti_contracts;

struct Point { x: u32, y: u32 }

fn f1<'a>(p: &'a mut Point) -> &'a mut u32 {
	if p.x == 0 {
		&mut p.y
	} else {
		&mut p.x
	}
}

The error is internal encoding error - unregistered verification error: [unfold.failed:insufficient.permission] Unfolding u32(old[post](_1.val_ref).f$x) might fail. There might be insufficient permission to access old[post](_1.val_ref).f$x. (<no position>)

The problem seems to be that the predicates are not folded/unfolded correctly. I managed to get it to work by inserting/removing some folds/unfolds manually. The file main-fail.rs.vpr is the Viper encoding generated by Prusti and the file main-succeed.rs.vpr contains my modifications.

Returning pair of references triggers panic

This causes Prusti to panic:

use prusti_contracts::*;

struct Point { x: u32, y: u32 }

fn foo(p: &mut Point) -> (&mut u32, &mut u32) {
    (&mut p.x, &mut p.y)
}

fn main(){}

Create a proper notion of equality for Prusti

We want a way to express that two objects have the same byte representation and use this notion for equality for pure functions (if a and b are equal, then f(a) and f(b) are equal for any pure function f).

Trait refinement verifies contracts are legal but then doesn't use them

According to the source code, contract refinement on trait methods should be supported with pre-condition weakening and post-condition strengthening. This is enforced in the sense that it is checked that the pre-/post-condition on the implementation is weaker/stronger respectively, but the verification does not take these contracts into account:

extern crate prusti_contracts;

trait Answer {
    #[requires="_arg == 1"]
    #[ensures="result >= - 100 && result <= 100"]
    fn produce_answer(&self, _arg: i32) -> i32;
}

struct DeepThought {}

impl Answer for DeepThought {
    #[requires="true"]
    #[ensures="result == 42"]
    fn produce_answer(&self, _arg: i32) -> i32 { 42 }
}

fn test(dt: &DeepThought) {
    let answer = dt.produce_answer(40);

    assert!(answer == 42);
}

fn main() {
    let dt = DeepThought {};
    test(&dt);
}

The code above doesn't verify as it complains that the call to produce_answer doesn't have 1 as an argument. Even if this is changed, it doesn't verify with "the asserted expression might not hold", implying the post-condition is also not taken into account.

Warn about misplaced loop invariant

Placing the invariant annotation inside the loop causes Prusti to panick or misbehave. Prusti should detect this case and generate a proper error message.

For example, on the following program Prusti incorrectly reports a verification error for the assertion:

extern crate prusti_contracts;

fn main(){
    let mut i = 0;
    // #[invariant="0 <= i && i <= 10"] // good
    while i < 10 {
        #[invariant="0 <= i && i <= 10"] // bad
        i += 1;
    }
    assert!(i == 10) // Prusti is expected to prove that this always holds
}

Compiler or Prusti unexpectedly panicked

The enclosed log was generated when trying to verify an iterative version of a function that computes the sum of the first n integers. My installed system verifies the code in the Fibbonacci example, so the installation does something.

John

sum_of_ints.log
sum_of_ints.rs.txt

cargo-prusti on 033_unicode-normalization uses too much memory

Running cargo-prusti on the crate 033_unicode-normalization uses too much memory.

The reason is probably that PathCtxt now has its own copy of EventLog.
When cloning EventLog, we should at least share the immutable entries of EventLog::prejoin_actions.

Failing test on the top-20 crates

The test that runs Prusti on the top-20 crates (see here) recently started failing.

Probably, the whitelist produced by cargo-filter and consumed by Prusti is no longer stable between compiler runs. One option is to skip unsupported functions on the fly while running Prusti, without relying on the on-disk whitelist.

[Documentation] dead links in the book

Hi ! I was interested in understanding how Prusti works. In particular, how you link the the rust compiler and MIR.

I built the book in design, but the link given for the documentation of the patched Rust compiler is dead.
I realise it was written two years ago, but is there any chance you still have that documentation somewhere ? Even in raw format :)

Thank you !

Prusti tries to generate code for trait function without a body

Prusti complains about the following program

extern crate prusti_contracts;

trait Val {
    #[pure]
    fn value(&self) -> i32;
}

struct Foo<T> {
    x: T,
}

impl<T: Val> Foo<T> {
    fn get(&self) -> i32 {
        self.x.value()
    }
}

with the error
librustc_mir/build/mod.rs:40: can't build MIR for DefId(0/0:5 ~ test[8787]::Val[0]::value[0])
It appears to be trying to generate code for the empty value function in the trait.

Prusti panic involving multiple dereferences in conditional

This causes Prusti to panic:

fn find(b: &mut bool) -> &mut bool {
    if *b { b }
    else if *b { b }
    else { b }
}

The backtrace:

thread 'main' panicked at 'internal error: entered unreachable code: Invalid addition: write + write', prusti-viper/src/encoder/vir/ast/common.rs:101:18
stack backtrace:
...
 7: std::panicking::begin_panic_fmt
             at libstd/panicking.rs:413
 8: prusti_viper::encoder::foldunfold::state::State::restore_dropped_perm
 9: prusti_viper::encoder::foldunfold::FoldUnfold::process_expire_borrows
10: <prusti_viper::encoder::foldunfold::FoldUnfold<'p, 'v, 'r, 'a, 'tcx> as prusti_viper::encoder::vir::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::branch_ctxt::BranchCtxt<'p>, alloc::vec::Vec<prusti_viper::encoder::foldunfold::action::Action>>>::replace_stmt
11: <prusti_viper::encoder::foldunfold::FoldUnfold<'p, 'v, 'r, 'a, 'tcx> as prusti_viper::encoder::vir::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::branch_ctxt::BranchCtxt<'p>, alloc::vec::Vec<prusti_viper::encoder::foldunfold::action::Action>>>::replace_stmt
12: prusti_viper::encoder::foldunfold::add_fold_unfold
13: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
14: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
15: prusti_viper::verifier::Verifier::verify
16: prusti::verifier::verify
...

Incorrect `old[l](...)` in Viper encoding of a re-borrowing function

The following program fails to verify with an internal encoding error:

extern crate prusti_contracts;

struct Point {
	x: u32,
	y: u32
}

fn foo<'a>(p: &'a mut Point) -> &'a u32 {
    &p.x
}

fn main() {
}

The Viper encoding packages a magic wand to trade the returned &u32 reference for the original &mut Point reference passed as an argument. The following inhale inside the package statement fails because of missing permission to access old[post](_1.val_ref).f$x:

inhale acc(u32(old[post](_1.val_ref).f$x), write - read$())

The necessary permission would actually be available, but is not selected to be part of the magic wand's footprint. Manually adding it to the footprint with an assert acc(old[post](_1.val_ref).f$x) inside the package statement resolves the problem.

Relevant files:

The Rust program triggering the issue: main.rs
The Viper encoding of this program that fails to verify: main.rs.vpr
In case it's helpful, a simplified version of the Viper encoding that fails to verify for the same reason: main-clean.rs.vpr

Support existential quantifiers

This should be a really small change.

Support quantifiers inside pure functions

When pure functions are used to abbreviate recurring assertions (e.g. invariants that are conjoined to many pre- and postconditions), it would be useful if one could write (pure) assertions, in particular, quantifiers in their bodies.

There are various alternative designs (e.g., using postconditions of abstract functions, using macros), but those have subtle implications for triggering. So we need to explore what the best option is. We might even have to change Viper to avoid matching loops.

Test Prusti on a collection of crates

We would need a way to run Prusti (cargo-prusti) on multiple test crates. This would allow to have regression tests for issues like #2 and #528.

Ideally, the test suite should check that the position and message of the reported errors matches the expected one, as compiletest-rs does.

Malformed cfg value or key/value pair with cargo-prusti

After PR #48, cargo-prusti fails with "error: malformed cfg value or key/value pair: lib___.rlib".

That PR runs the compiler twice, to collect type system information that are not available in the parse phase of the second run. The preliminar run probably has some side effects (stdout messages? file system changes?) that break cargo.

The error is not catched by the CI tests because they don't yet run cargo-prusti (see also: #3).

"not yet implemented: action fold" error

The following program makes Prusti crash with

thread 'main' panicked at 'not yet implemented: action fold acc(m_20200615_225658$$Locator$opensqu$0$closesqu$$_beg_$_end_:None(_16.val_ref), read)', prusti-viper/src/encoder/foldunfold/action.rs:44:17

The error happens during the encoding of the delete method. Deleting or changing the contract of remove (called by delete) makes the crash disappear.

Actions to close this issue:

Make Prusti report the error without crashing, pointing to the method that was being encoded.
Make Prusti verify the given program.

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: MIT-0

// This version will compile with prusti-rustc but uses various partially
// supported features. Attempting to verify anything might crash Prusti.

extern crate prusti_contracts;

use std::collections::HashMap;
use std::hash::Hash;

#[derive(Copy, Clone, PartialEq, Eq, Hash)]
pub struct Locator(usize);

const NUM_PAGES: usize = 512usize;

#[derive(Clone)]
pub struct Page<T>
    where T: Clone
{
    data: T,
    next:  Option<usize>,
}

// PRUSTI START: trusted wrappers
#[derive(Clone)] // partially supported due to internal usage of raw pointers
pub struct VecWrapper<T> 
    where T: Clone
{
    v: Vec<T>,
}

impl<T> VecWrapper<T>
    where T: Clone
{
   
}

pub struct HashMapLocatorWrapper
{
    m: HashMap<Locator, Locator>,
}

impl HashMapLocatorWrapper
{

    //Option<&Locator>
    #[trusted]
    pub fn get(&self, k: &Locator) -> Option<Locator>{
        unimplemented!()
    }


    #[trusted]
    #[pure]
    pub fn contains_kv(&self, k: &Locator, v: usize) -> bool {
       unimplemented!()
    }


    #[trusted]
    //#[ensures="old(self.contains_kv(k,0)) == false ==> self.existsZero() == true"] // original
    #[ensures="old(self.contains_kv(k, 0))"] // minimized
    pub fn remove(&mut self, k: &Locator) -> Option<Locator> {
        //self.m.remove(k)
        unimplemented!()
    }

    #[trusted]
    #[pure]
    pub fn existsZero(&self) -> bool{
        unimplemented!()
    }

}
// PRUSTI END


struct Disk<T>
    where T:Clone
{
    pages: VecWrapper<Page<T>>,
}

impl<T> Disk<T>
    where T: Clone
{
    //#[requires="p < self.pages.len()"]
    fn read(&self, p: usize) -> Page<T> {
        unimplemented!()
    }
}

pub struct KeyStore<T>
    where T: Clone
{
    disk: Disk<T>,
    predecessor: HashMapLocatorWrapper,
}

impl<T> KeyStore<T>
    where T: Eq + Hash + Clone
{
    // The crash happens during the encoding of this method:
    pub fn delete(&mut self, locator: Locator) {
        if let Some(loc) = self.predecessor.get(&locator) {
            let this_page = self.disk.read(locator.0);
            self.predecessor.remove(&locator);
        }
    }
}

fn main() {}

Temporary borrows in condition to break out of loop causes panic

Temporary borrows such as used by pattern matching that wrap a break statement inside a loop cause Prusti to panic.

Rust Code

#![allow(path_statements)]
fn main () {
    loop {
        if let Some(_) = get_a_number() {
            1;
        } else {
            break;
        }
    }
}

fn get_a_number() -> Option<u32> {
        Some(5)
}

Note that changing the condition to something like if get_a_number().is_some(), does not exhibit the problem. Changing the break statement to anything else (even continue) also does not exhibit the problem.

Prusti log

  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  |  Hash:  ccf572597ff91ca6c7c
 |      /\   |  \ \__/ .__/  |       /\   |  Build: 2020-04-24 10:57:06

 INFO 2020-05-02T13:43:41Z: prusti::compiler_calls: Parsing of annotations successful (0.0 seconds)
 INFO 2020-05-02T13:43:41Z: prusti::compiler_calls: Type-checking of annotations successful (0.0 seconds)
Verification of 2 items...
 INFO 2020-05-02T13:43:41Z: viper::viper: Using JVM OpenJDK 64-Bit Server VM, Java 11.0.7
 INFO 2020-05-02T13:43:41Z: prusti::verifier: JVM startup (0.4 seconds)
 INFO 2020-05-02T13:43:41Z: viper::verification_context: Using Z3 path: '/usr/bin/viper-z3'
 INFO 2020-05-02T13:43:41Z: viper::verifier: Using backend Silicon version <unknown-build-version>
 INFO 2020-05-02T13:43:43Z: prusti::verifier: Verifier startup (1.67 seconds)
 INFO 2020-05-02T13:43:43Z: prusti_viper::verifier: Received 2 items to be verified:
 INFO 2020-05-02T13:43:43Z: prusti_viper::verifier:  - code::main from code.rs:2:1: 10:2 (code::main[0])
 INFO 2020-05-02T13:43:43Z: prusti_viper::verifier:  - code::get_a_number from code.rs:12:1: 14:2 (code::get_a_number[0])
warning: [Prusti] this is partially supported, because it causes abrupt loop terminations
 --> code.rs:4:16
  |
4 |         if let Some(_) = get_a_number() {
  |                ^^^^^^^

 INFO 2020-05-02T13:43:43Z: prusti_viper::encoder::encoder: Encoding: code::main from code.rs:2:1: 10:2 (code::main[0])
thread 'main' panicked at 'assertion failed: !self.loop_magic_wands.is_empty()', prusti-interface/src/environment/polonius_info.rs:1177:17
note: Run with `RUST_BACKTRACE=1` for a backtrace.

error: internal compiler error: unexpected panic

note: the compiler or Prusti unexpectedly panicked.

note: possible reasons include the usage of Rust features that are not supported by Prusti.

note: we would appreciate a bug report for Prusti: <https://github.com/viperproject/prusti-dev/issues>

note: Prusti hash ccf572597ff91ca6c7c built on 2020-04-24 10:57:06

note: rustc <unknown> running on x86_64-unknown-linux-gnu

I am running Prusti inside an ubuntu:bionic docker container.

Support for maps

It seems useful to add support for maps to Prusti (and Viper). The key question is whether there are triggering issues (and of course what the Prusti language design should be).

Syntax error in pledges silently ignored

This fails to verify:

extern crate prusti_contracts;

struct Point { x: u32, y: u32 }

#[ensures="after_expiry<result>(
	p.x == before_expiry(*result)
	p.y == 0
)"]
fn f1<'a>(p: &'a mut Point) -> &'a mut u32 {
	p.y = 0;
	&mut p.x
}

#[ensures="after_expiry<result>(
	p.x == before_expiry(*result) &&
	p.y == 0
)"]
fn f2<'a>(p: &'a mut Point) -> &'a mut u32 {
	f1(p)
}

fn main() {
}

Prusti's output is:

error: [Prusti] pledge in the postcondition might not hold.
  --> main.rs:16:2
   |
16 |     p.y == 0
   |     ^^^^^^^^
   |
note: the error originates here
  --> main.rs:18:1
   |
18 | / fn f2<'a>(p: &'a mut Point) -> &'a mut u32 {
19 | |     f1(p)
20 | | }
   | |_^

Verification failed
error: aborting due to previous error

I'd say the postcondition of f1 has a syntax error -- there should be a && after the first line of the pledge, like this:

#[ensures="after_expiry<result>(
	p.x == before_expiry(*result) &&
	p.y == 0
)"]

(With this updated postcondition, verification succeeds.) The issue is that Prusti silently drops the second conjunct if the conjuction is missing. If I remove f2 in the initial program, Prusti does not report an error.

Unimplemented: Inhale the predicate rooted at dst_field

This program

use prusti_contracts::*;
use std::collections::HashSet;
use std::hash::Hash;
use std::cmp::Eq;

struct SetWrapper<T: Hash + Eq> {
    set: HashSet<T>
}

impl<T: Hash + Eq> SetWrapper<T> {
    #[pure]
    #[trusted]
    pub fn contains(&self, value: &T) -> bool {
        self.set.contains(value)
    }

    #[ensures(self.contains(&value))]
    pub fn insert(&mut self, value: T) {
        self.set.insert(value);
    }

    #[ensures(!self.contains(&value))]
    pub fn remove(&mut self, value: &T) -> bool {
        self.set.remove(value)
    }
}

fn test() {
    let mut set = SetWrapper { set: HashSet::new() };
    set.insert(1);
    set.insert(2);
    set.insert(3);
    set.remove(&3);
    set.remove(&2);
    set.remove(&1);
    set.remove(&1);
}

fn main() {}

crashes with

thread 'main' panicked at 'not yet implemented: Inhale the predicate rooted at dst_field.', prusti-viper/src/encoder/procedure_encoder.rs:3973:25

Support for pure functions that return Copy types

Currently, Prusti only supports pure functions that return integers or booleans. It should be possible to use the same mechanism applied in checking equality of structs (see #53 ) to also support pure functions that return copyable types.

Support for loops

Pull request #46 prepared the ground to support break/return/continue statements in loops and loop conditions with side effects.

Still to do:

Havoc all the Viper local variables modified in the loop, at the point where the loop invariant is enforced.
Modify the computation of Viper permissions such that it computes them at the point where the loop invariant is enforced, and not at the loop head of the CFG.
Add more tests.
Remove from prusti-filter the warnings/errors regarding complex loop guards or abrupt loop termination.
After modifying prusti-filter, check the top-500-crates test and open new issues for the failing crates.
Update the status table in the wiki.

	// 5. Apply effect of statement on state
	debug!("[step.5] replace_stmt: {}", stmt);
	bctxt.apply_stmt(&stmt);
	stmts.push(stmt.clone());

viperproject / prusti-dev Goto Github PK

prusti-dev's Introduction

Prusti

Useful links

Getting Prusti

Quick example

prusti-dev's People

Contributors

Stargazers

Watchers

Forkers

prusti-dev's Issues

Panic

Consistency error

Unregistered verification error

Timeout

Breaking Code

Prusti Log

Rust Code

Prusti log

Recommend Projects

Recommend Topics

Recommend Org