'make clean' does not make clean enough #2909
Comments
|
Not 0.6, regrettably. |
|
Nominating for milestone 5, production-ready |
|
just a bug, removing milestone/nomination. |
|
Still relevant. Fix is probably to use relative paths? |
|
Part of #8058 |
|
I just ran this today, and everything appeared to work just fine for me. @gwillen, do you remember what the problem it was that you were seeing? Otherwise I'm tempted to close this because I think that @pnkfelix's recent improvements to the Makefiles might have fixed this (or possibly just reorganization at some point during the last year) |
|
If you tell me this is likely fixed, I'll believe you. I haven't tried it in ages. Thanks for looking into it. |
|
Cool, closing this for now on the grounds that I couldn't reproduce this. Certainly feel free to reopen if the issue crops up again! |
RalfJung
pushed a commit
to RalfJung/rust
that referenced
this issue
Aug 6, 2023
…883, r=RalfJung Rewrite miri script in rust This is a sketch of a rewrite of miri script in Rust. It does not include changes made in rust-lang/miri#2908 yet. Environment variables are not properly propagated yet, which is something I plan to address. This PR is mostly a heads-up about the ongoing effort and it's state. It's definitely not the cleanest code I've seen in my life, but my first goal was feature/interface parity. I will iterate on it a bit before marking it as ready. I wonder though how this should be integrated/tested. Are you aware of anyone using `./miri` in their scripts? I guess we should keep existing `miri` script in place and let it run miri-script package directly? CI should probably `cargo check` this package as well. Fixes rust-lang#2883
celinval
pushed a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
Extends the function contract functionality with a `modifies` clause. The design is different from rust-lang#2594 but serves a similar purpose. The `modifies` clause allows the user to specify which parts of a structure a function may assign to. Essentially refining the `mut` annotation. We allow arbitrary (side-effect free) expressions in the `modifies` clause. The expressions are evaluated as part of the preconditions and passed to the function-under-verification as additional arguments. CBMC is then instructed to check that those locations are assigned. Aliasing means that this also adds the location in the original structure to the write set. Each expression must return a pointer to a value that implements `Arbitrary`. On replacement we then simply assign `*ptr = kani::any()`, relying again on aliasing to update the original structure. Additional tests for the new functionality are provided. Resolves rust-lang#2594 ## Open Questions ### API divergence from CBMC (accepted) The current design goes roughly as follows: We start with a `modifies` annotation on a function ```rs #[modifies(obj.some_expr())] fn target(obj: ...) { ... } ``` And from this we generate code to the effect of (simplified here) ```rs fn target_check(obj: ...) { // Undo the lifetime entanglements let modified_1 = std::mem::transmute::<&'a _, &'b _>(obj.some_expr()); target_wrapper(obj, modified_1); } #[cbmc::assigns(*modified_1)] fn target_wrapper(obj: ..., modified_1: &impl kani::Arbitrary) { ... } ``` Unlike CBMC we expect `obj.some_expr()` to be of a **pointer type** (`*const`, `*mut`, `&mut` or `&`) that points to the object which is target of the modification. So if we had a `t : &mut T` that was modified, CBMC would expect its assigns clause to say `*t`, but we expect `t` (no dereference). The reason is that the code we generate uses the workaround of creating an alias to whichever part of `obj` is modified and registers the alias with CBMC (thereby registering the original also). If we generated code where the right side of `let modified_1 =` is not of pointer type, then the object is moved to the stack and the aliasing destroyed. The open questions is whether we are happy with this change in API. (Yes) ### Test cases when expressions are used in the clause. With more complex expressions in the modifies clause it becomes hard to define good test cases because they reference generated code as in this case: ```rs #[kani::requires(**ptr < 100)] #[kani::modifies(ptr.as_ref())] fn modify(ptr: &mut Box<u32>) { *ptr.as_mut() += 1; } ``` This passes (as it should) and when commenting out the `modifies` clause we get this error: ``` Check 56: modify_wrapper_895c4e.assigns.2 - Status: FAILURE - Description: "Check that *var_2 is assignable" - Location: assigns_expr_pass.rs:8:5 in function modify_wrapper_895c4e ``` The information in this error is very non-specific, hard to read and brittle. How should we define robust "expected" test cases for such errors? ### Corner Cases / Future Improvements - rust-lang#2907 - rust-lang#2908 - rust-lang#2909 ## TODOs - [ ] Test Cases where the clause contains - [x] `Rc` + (`RefCell` or `unsafe`) (see rust-lang#2907) - [x] Fields - [x] Statement expressions - [x] `Vec` (see rust-lang#2909) - [ ] Fat pointers - [ ] update contracts documentation - [x] Make sure the wrapper arguments are unique. - [x] Ensure `nondet-static-exclude` always uses the correct filepath (relative or absolute) - [ ] Test case for multiple `modifies` clauses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
) CBMC's symbolic execution by default turns `while(true) {}` loops into `assume(false)` to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops. Resolves: rust-lang#2909
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
If I check out the repo, ./configure, and build rustc; then move the repo to a different directory, make clean, ./configure, and build rustc again, it should work. It doesn't.
Workaround: instead of doing 'make clean', rm .gitignore, then git clean -df (removing everything that's not part of the repo), then git checkout .gitignore.
The text was updated successfully, but these errors were encountered: