-
Notifications
You must be signed in to change notification settings - Fork 246
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
analyze: misc fixes for lighttpd buffer (part 1/2) (#1178)
Various small fixes for lighttpd's `buffer` module: * In `rewrite::expr::mir_op`, skip generating casts for `Deref` projections on `FIXED` pointers * In borrowck, don't treat `StorageLive`/`StorageDead` as uses (which would invalidate loans) * In `rewrite::ty::HirTyVisitor`, add a missing `walk_stmt` call. This was causing type rewrites to be skipped in some places. * In `rewrite::expr::mir_op`, add a conversion from `&[T]` to `&T` before dereferencing if needed. This can happen in cases like `p.offset(...); x = *p;` because `*p` uses `p` directly, which has the `OFFSET` permission due to the previous `p.offset()` call, instead of copying `p` into a temporary, which would not need the `OFFSET` permission. * In `GlobalAnalysisCtxt::fn_analysis_invalid`, ignore the flag `DontRewriteFnReason::REWRITE_INVALID`, since rewriting errors don't affect the validity of the analysis results.
- Loading branch information
Showing
9 changed files
with
165 additions
and
40 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
use std::ptr; | ||
|
||
// CHECK-LABEL: final labeling for "move_mut1" | ||
pub unsafe fn move_mut1(mut x: i32) -> i32 { | ||
// CHECK-DAG: ([[@LINE+1]]: q): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | NON_NULL | STACK# | ||
let q: *mut i32 = { | ||
// CHECK-DAG: ([[@LINE+1]]: p): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | NON_NULL | STACK# | ||
let p: *mut i32 = ptr::addr_of_mut!(x); | ||
*p = 1; | ||
// This produces a move from `p` into `q`. c2rust-analyze interprets this as a reborrow, | ||
// which gets invalidated at the end of `p`'s lifetime. Currently we work around this by | ||
// ignoring `StorageLive` and `StorageDead`, so they don't invalidate any borrows. | ||
p | ||
}; | ||
*q = 2; | ||
*q | ||
} | ||
|
||
// Safe version of `move_mut1`. This can be run through `rustc -Z nll-facts` to produce Polonius | ||
// facts from the reference implementation for comparison. | ||
// CHECK-LABEL: final labeling for "move_mut1_safe" | ||
pub fn move_mut1_safe(mut x: i32) -> i32 { | ||
let q: &mut i32 = { | ||
let p: &mut i32 = &mut x; | ||
*p = 1; | ||
p | ||
}; | ||
*q = 2; | ||
*q | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,40 +1,37 @@ | ||
#![feature(register_tool)] | ||
#![register_tool(c2rust_analyze_test)] | ||
|
||
// TODO: All the pointers here are currently inferred to be non-`UNIQUE`, even though the access | ||
// patterns look fine. | ||
|
||
use std::ptr; | ||
|
||
// CHECK-LABEL: final labeling for "f" | ||
fn f(cond: bool) { | ||
let x = 1_i32; | ||
// CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = STACK# | ||
// CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE | STACK# | ||
let mut y = ptr::addr_of!(x); | ||
if cond { | ||
y = 0 as *const _; | ||
} | ||
// The expression `y` is considered nullable even though it's passed for argument `p` of `g`, | ||
// which is forced to be `NON_NULL`. | ||
// CHECK: ([[@LINE+1]]: y): {{.*}}, type = STACK# | ||
// CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | STACK# | ||
g(cond, y); | ||
} | ||
|
||
// CHECK-LABEL: final labeling for "g" | ||
// `p` should be non-null, as it's forced to be by the attribute. This emulates the "unsound" PDG | ||
// case, where a variable is forced to stay `NON_NULL` even though a null possibly flows into it. | ||
// CHECK: ([[@LINE+2]]: p): {{.*}}, type = NON_NULL | STACK# | ||
// CHECK: ([[@LINE+2]]: p): {{.*}}, type = UNIQUE | NON_NULL | STACK# | ||
#[c2rust_analyze_test::force_non_null_args] | ||
fn g(cond: bool, p: *const i32) { | ||
// `q` is not forced to be `NON_NULL`, so it should be inferred nullable due to the null | ||
// assignment below. | ||
// CHECK: ([[@LINE+1]]: mut q): {{.*}}, type = STACK# | ||
// CHECK: ([[@LINE+1]]: mut q): {{.*}}, type = UNIQUE | STACK# | ||
let mut q = p; | ||
if cond { | ||
q = 0 as *const _; | ||
} | ||
// `r` is derived from `q` (and is not forced), so it should also be nullable. | ||
// CHECK: ([[@LINE+1]]: r): {{.*}}, type = STACK# | ||
// CHECK: ([[@LINE+1]]: r): {{.*}}, type = UNIQUE | STACK# | ||
let r = q; | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
|
||
// Test dereferencing a pointer that has OFFSET permissions. This requires inserting a cast from | ||
// `&mut [T]` to `&mut T`. | ||
// CHECK-LABEL: fn offset_deref | ||
pub unsafe fn offset_deref(x: *mut i32, off: isize) -> *mut i32 { | ||
// CHECK: *&mut (x)[0] = 0; | ||
*x = 0; | ||
// CHECK: *&mut (&mut (x)[((1) as usize) ..])[0] = 1; | ||
*x.offset(1) = 1; | ||
// CHECK: {{.*}}x{{.*}} | ||
x | ||
} |