Skip to content

Commit

Permalink
analyze: add HEAP and STACK permissions (#1147)
Browse files Browse the repository at this point in the history
This adds new pointer permissions that track whether a pointer may point
to the heap or to the stack. (Statics are counted as stack, since like
stack variables, we can't use `Box<T>` for pointers to them.)

As usual for forward-dataflow permissions in our framework, the
definitions are a little tricky:
* `HEAP` means "points to the heap, or is null" - in other words, this
pointer definitely doesn't point to the stack.
* `STACK` means "points to the stack, or is null" - in other words, this
pointer definitely doesn't point to the heap.
* `HEAP | STACK` means the pointer must be null, since null is the only
pointer in the intersection of those two sets. In other words, the
pointer points neither to the heap nor to the stack.
* Having neither flag means the pointer could point anywhere.
  • Loading branch information
spernsteiner authored Nov 22, 2024
2 parents 5c27c04 + a632901 commit 644d80b
Show file tree
Hide file tree
Showing 17 changed files with 152 additions and 98 deletions.
20 changes: 17 additions & 3 deletions c2rust-analyze/src/analyze.rs
Original file line number Diff line number Diff line change
Expand Up @@ -696,7 +696,7 @@ fn run(tcx: TyCtxt) {
let l = acx.local_tys.push(lty);
assert_eq!(local, l);

let ptr = acx.new_pointer(PointerInfo::empty());
let ptr = acx.new_pointer(PointerInfo::ADDR_OF_LOCAL);
let l = acx.addr_of_local.push(ptr);
assert_eq!(local, l);
}
Expand Down Expand Up @@ -890,8 +890,12 @@ fn run(tcx: TyCtxt) {
// don't want to rewrite those
gacx.foreign_mentioned_tys = foreign_mentioned_tys(tcx);

const INITIAL_PERMS: PermissionSet =
PermissionSet::union_all([PermissionSet::UNIQUE, PermissionSet::NON_NULL]);
const INITIAL_PERMS: PermissionSet = PermissionSet::union_all([
PermissionSet::UNIQUE,
PermissionSet::NON_NULL,
PermissionSet::HEAP,
PermissionSet::STACK,
]);
const INITIAL_FLAGS: FlagSet = FlagSet::empty();

let mut gasn = GlobalAssignment::new(gacx.num_pointers(), INITIAL_PERMS, INITIAL_FLAGS);
Expand All @@ -901,6 +905,11 @@ fn run(tcx: TyCtxt) {
if should_make_fixed(info) {
gasn.flags[ptr].insert(FlagSet::FIXED);
}
if info.contains(PointerInfo::ADDR_OF_LOCAL) {
// `addr_of_local` is always a stack pointer, though it should be rare for the
// `ADDR_OF_LOCAL` flag to appear on a global `PointerId`.
gasn.perms[ptr].remove(PermissionSet::HEAP);
}
}

mark_foreign_fixed(&mut gacx, &mut gasn, tcx);
Expand Down Expand Up @@ -928,6 +937,11 @@ fn run(tcx: TyCtxt) {
if should_make_fixed(info) {
lasn.flags[ptr].insert(FlagSet::FIXED);
}
if info.contains(PointerInfo::ADDR_OF_LOCAL) {
// `addr_of_local` is always a stack pointer. This will be propagated
// automatically through dataflow whenever the address of the local is taken.
lasn.perms[ptr].remove(PermissionSet::HEAP);
}
}

info.lasn.set(lasn);
Expand Down
35 changes: 31 additions & 4 deletions c2rust-analyze/src/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,20 @@ bitflags! {
/// [`_.is_null()`]: core::ptr::is_null
/// [`_.is_some()`]: Option::is_some
const NON_NULL = 0x0080;

/// This pointer points to the heap (or is null).
///
/// `HEAP` and `STACK` form a four-element lattice. `HEAP` means definitely heap, `STACK`
/// means definitely stack, neither means it could be either (top), and both means the
/// pointer is either definitely null or comes from an unknown source (bottom).
const HEAP = 0x0100;

/// This pointer points to the stack or to static memory (or is null).
///
/// Currently we distinguish stack/static vs heap, but don't distinguish stack vs static.
/// The reason is that heap pointers can be rewritten to `Box<T>`, but stack and static
/// pointers both cannot.
const STACK = 0x0200;
}
}

Expand Down Expand Up @@ -167,7 +181,11 @@ impl PermissionSet {
/// The permissions for a (byte-)string literal.
//
// `union_all` is used here since it's a `const fn`, unlike `BitOr::bitor`.
pub const STRING_LITERAL: Self = Self::union_all([Self::READ, Self::OFFSET_ADD]);
pub const STRING_LITERAL: Self = Self::union_all([Self::READ, Self::OFFSET_ADD, Self::STACK]);

/// Negative permissions for a (byte-)string literal. These permissions should be absent from
/// all string literals, contrary to the defaults for most pointers.
pub const STRING_LITERAL_NEGATIVE: Self = Self::union_all([Self::HEAP]);
}

bitflags! {
Expand Down Expand Up @@ -296,6 +314,9 @@ bitflags! {
/// This `PointerId` has at least one local declaration that is not a temporary reference
/// arising from an `&x` or `&mut x` expression in the source.
const NOT_TEMPORARY_REF = 0x0004;

/// This `PointerId` appeared as the `addr_of_local` `PointerId` for at least one local.
const ADDR_OF_LOCAL = 0x0008;
}
}

Expand Down Expand Up @@ -447,9 +468,15 @@ impl<'a, 'tcx> AnalysisCtxt<'_, 'tcx> {

pub fn string_literal_perms(
&'a self,
) -> impl Iterator<Item = (PointerId, PermissionSet)> + PhantomLifetime<'tcx> + 'a {
self.string_literal_tys()
.map(|lty| (lty.label, PermissionSet::STRING_LITERAL))
) -> impl Iterator<Item = (PointerId, PermissionSet, PermissionSet)> + PhantomLifetime<'tcx> + 'a
{
self.string_literal_tys().map(|lty| {
(
lty.label,
PermissionSet::STRING_LITERAL,
PermissionSet::STRING_LITERAL_NEGATIVE,
)
})
}

pub fn check_string_literal_perms(&self, asn: &Assignment) {
Expand Down
5 changes: 4 additions & 1 deletion c2rust-analyze/src/dataflow/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,10 @@ impl DataflowConstraints {
// Permissions that should be propagated "down": if the superset (`b`)
// doesn't have it, then the subset (`a`) should have it removed.
#[allow(bad_style)]
let PROPAGATE_DOWN = PermissionSet::UNIQUE | PermissionSet::NON_NULL;
let PROPAGATE_DOWN = PermissionSet::UNIQUE
| PermissionSet::NON_NULL
| PermissionSet::HEAP
| PermissionSet::STACK;
// Permissions that should be propagated "up": if the subset (`a`) has it,
// then the superset (`b`) should be given it.
#[allow(bad_style)]
Expand Down
12 changes: 11 additions & 1 deletion c2rust-analyze/src/dataflow/type_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -491,6 +491,11 @@ impl<'tcx> TypeChecker<'tcx, '_> {

Callee::Malloc | Callee::Calloc => {
self.visit_place(destination, Mutability::Mut);

// The output of `malloc` is known not to be a stack pointer.
let pl_lty = self.acx.type_of(destination);
self.constraints
.add_no_perms(pl_lty.label, PermissionSet::STACK);
}
Callee::Realloc => {
let out_ptr = destination;
Expand All @@ -507,6 +512,10 @@ impl<'tcx> TypeChecker<'tcx, '_> {
let perms = PermissionSet::FREE;
self.constraints.add_all_perms(rv_lty.label, perms);

// Output loses the STACK permission.
self.constraints
.add_no_perms(pl_lty.label, PermissionSet::STACK);

// unify inner-most pointer types
self.do_equivalence_nested(pl_lty, rv_lty);
}
Expand Down Expand Up @@ -723,8 +732,9 @@ pub fn visit<'tcx>(
equiv_constraints: Vec::new(),
};

for (ptr, perms) in acx.string_literal_perms() {
for (ptr, perms, neg_perms) in acx.string_literal_perms() {
tc.constraints.add_all_perms(ptr, perms);
tc.constraints.add_no_perms(ptr, neg_perms);
}

for (bb, bb_data) in mir.basic_blocks().iter_enumerated() {
Expand Down
12 changes: 6 additions & 6 deletions c2rust-analyze/tests/filecheck/alias1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,23 +2,23 @@ use std::ptr;

// CHECK-LABEL: final labeling for "alias1_good"
pub unsafe fn alias1_good() {
// CHECK-DAG: ([[@LINE+1]]: mut x): addr_of = READ | WRITE | UNIQUE | NON_NULL,
// CHECK-DAG: ([[@LINE+1]]: mut x): addr_of = READ | WRITE | UNIQUE | NON_NULL | STACK,
let mut x = 0;
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL | STACK#
let p = ptr::addr_of_mut!(x);
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | STACK#
let q = ptr::addr_of_mut!(x);
*q = 1;
}

// CHECK-LABEL: final labeling for "alias1_bad"
pub unsafe fn alias1_bad() {
// CHECK-DAG: ([[@LINE+2]]: mut x): addr_of = READ | WRITE | NON_NULL,
// CHECK-DAG: ([[@LINE+2]]: mut x): addr_of = READ | WRITE | NON_NULL | STACK,
// CHECK-DAG: ([[@LINE+1]]: mut x): addr_of flags = CELL,
let mut x = 0;
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL | STACK#
let p = ptr::addr_of_mut!(x);
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = NON_NULL | STACK#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
let q = ptr::addr_of_mut!(x);
*p = 1;
Expand Down
24 changes: 12 additions & 12 deletions c2rust-analyze/tests/filecheck/alias2.rs
Original file line number Diff line number Diff line change
@@ -1,43 +1,43 @@
use std::ptr;

// CHECK-LABEL: final labeling for "alias2_copy_good"
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK#
pub unsafe fn alias2_copy_good(x: *mut i32) {
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL | HEAP | STACK#
let p = x;
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK#
let q = x;
*q = 1;
}

// CHECK-LABEL: final labeling for "alias2_addr_of_good"
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK#
pub unsafe fn alias2_addr_of_good(x: *mut i32) {
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL | HEAP | STACK#
let p = ptr::addr_of_mut!(*x);
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK#
let q = ptr::addr_of_mut!(*x);
*q = 1;
}

// CHECK-LABEL: final labeling for "alias2_copy_bad"
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
pub unsafe fn alias2_copy_bad(x: *mut i32) {
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
let p = x;
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL | HEAP | STACK#
let q = x;
*p = 1;
}

// CHECK-LABEL: final labeling for "alias2_addr_of_bad"
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
pub unsafe fn alias2_addr_of_bad(x: *mut i32) {
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
let p = ptr::addr_of_mut!(*x);
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL | HEAP | STACK#
let q = ptr::addr_of_mut!(*x);
*p = 1;
}
Expand Down
12 changes: 6 additions & 6 deletions c2rust-analyze/tests/filecheck/alias3.rs
Original file line number Diff line number Diff line change
@@ -1,26 +1,26 @@
use std::ptr;

// CHECK-LABEL: final labeling for "alias3_copy_bad1"
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
pub unsafe fn alias3_copy_bad1(x: *mut i32) {
// CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type flags = CELL#
let p = x;
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
let q = x;
*q = *p;
}

// CHECK-LABEL: final labeling for "alias3_copy_bad2"
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
pub unsafe fn alias3_copy_bad2(x: *mut i32) {
// CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type flags = CELL#
let p = x;
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | NON_NULL#
// CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | NON_NULL | HEAP | STACK#
// CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
let q = x;
*p = *q;
Expand Down
24 changes: 12 additions & 12 deletions c2rust-analyze/tests/filecheck/alloc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,53 +26,53 @@ extern "C" {

// CHECK-LABEL: final labeling for "malloc_and_free1"
pub unsafe extern "C" fn malloc_and_free1(mut cnt: libc::c_int) {
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL, type = READ | UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL | STACK, type = READ | UNIQUE | FREE | NON_NULL | HEAP#
let mut i = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
// Perform an access to constrain the pointee type. Without a pointee type, some rewrites will
// be skipped.
let x = *i;
// CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL | HEAP#
free(i as *mut libc::c_void);
}

// CHECK-LABEL: final labeling for "malloc_and_free2"
pub unsafe extern "C" fn malloc_and_free2(mut cnt: libc::c_int) {
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | FREE | NON_NULL | HEAP#
let mut i = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
if !i.is_null() {
// CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | NON_NULL | HEAP#
let mut b = i;
*b = 2;
// CHECK-DAG: ([[@LINE+1]]: i): {{.*}}type = UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: i): {{.*}}type = UNIQUE | FREE | NON_NULL | HEAP#
free(i as *mut libc::c_void);
}
}

// CHECK-LABEL: final labeling for "malloc_and_free3"
pub unsafe extern "C" fn malloc_and_free3(mut cnt: libc::c_int) {
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | FREE | NON_NULL | HEAP#
let mut i: *mut i32 = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
// CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | FREE | NON_NULL | HEAP#
let mut b: *mut i32 = i;
*b = 2;
// CHECK-DAG: ([[@LINE+1]]: b): {{.*}}type = UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: b): {{.*}}type = UNIQUE | FREE | NON_NULL | HEAP#
free(b as *mut libc::c_void);
}

// CHECK-LABEL: final labeling for "calloc_and_free1"
pub unsafe extern "C" fn calloc_and_free1(mut cnt: libc::c_int) {
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL, type = READ | UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: mut i): addr_of = UNIQUE | NON_NULL | STACK, type = READ | UNIQUE | FREE | NON_NULL | HEAP#
let mut i = calloc(1, ::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
// Perform an access to constrain the pointee type. Without a pointee type, some rewrites will
// be skipped.
let x = *i;
// CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL#
// CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL | HEAP#
free(i as *mut libc::c_void);
}

// CHECK-LABEL: final labeling for "realloc1"
unsafe extern "C" fn realloc1(n: libc::c_ulong) {
// CHECK-DAG: ([[@LINE+1]]: mut buf): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | FREE | NON_NULL
// CHECK-DAG: ([[@LINE+1]]: mut buf): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | FREE | NON_NULL | HEAP
let mut buf: *mut i32 = malloc(2 * std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
let mut len = 0;
let mut capacity = 2;
Expand All @@ -82,7 +82,7 @@ unsafe extern "C" fn realloc1(n: libc::c_ulong) {
while i < n {
if len == capacity {
capacity *= 2;
// CHECK-DAG: ([[@LINE+2]]: buf{{.*}}): addr_of = UNIQUE | NON_NULL, type = UNIQUE | OFFSET_ADD | OFFSET_SUB | FREE | NON_NULL
// CHECK-DAG: ([[@LINE+2]]: buf{{.*}}): addr_of = UNIQUE | NON_NULL | STACK, type = UNIQUE | OFFSET_ADD | OFFSET_SUB | FREE | NON_NULL | HEAP
buf = realloc(
buf as *mut libc::c_void,
(capacity * std::mem::size_of::<i32>()) as libc::c_ulong,
Expand Down
2 changes: 1 addition & 1 deletion c2rust-analyze/tests/filecheck/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

// CHECK-LABEL: final labeling for "null_ptr"
pub unsafe fn null_ptr() {
// CHECK-DAG: ([[@LINE+3]]: s): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE#
// CHECK-DAG: ([[@LINE+3]]: s): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | HEAP | STACK#
// CHECK-LABEL: type assignment for "null_ptr":
// CHECK-DAG: ([[@LINE+1]]: s): std::option::Option<&mut S>
let s = 0 as *mut S;
Expand Down
6 changes: 3 additions & 3 deletions c2rust-analyze/tests/filecheck/fields.rs
Original file line number Diff line number Diff line change
Expand Up @@ -60,15 +60,15 @@ struct HypoWrapper {
// CHECK-DAG: assign Label { origin: Some(Origin([[P_REF_A_ORIGIN]]))

// CHECK-LABEL: final labeling for "_field_access"
// CHECK-DAG: ([[@LINE+3]]: ppd): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL
// CHECK-DAG: ([[@LINE+3]]: ppd): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK
// CHECK-DAG: ([[@LINE+2]]: ra): &'d mut A<'d>
// CHECK-DAG: ([[@LINE+1]]: ppd): &mut &mut Data
unsafe fn _field_access<'d, 'a: 'd, T: Clone + Copy>(ra: &'d mut A<'d>, ppd: *mut *mut Data<'d>) {
// CHECK-DAG: ([[@LINE+2]]: rd): addr_of = UNIQUE | NON_NULL, type = READ | UNIQUE | NON_NULL
// CHECK-DAG: ([[@LINE+2]]: rd): addr_of = UNIQUE | NON_NULL | STACK, type = READ | UNIQUE | NON_NULL | HEAP | STACK
// CHECK-DAG: ([[@LINE+1]]: rd): &Data
let rd = (*(**ppd).a.pra).rd;

// CHECK-DAG: ([[@LINE+2]]: pi): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL
// CHECK-DAG: ([[@LINE+2]]: pi): addr_of = UNIQUE | NON_NULL | STACK, type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK
// CHECK-DAG: ([[@LINE+1]]: pi): &mut i32
let pi = rd.pi;
*pi = 3;
Expand Down
8 changes: 4 additions & 4 deletions c2rust-analyze/tests/filecheck/foreign.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ extern "C" {

type Alias = Bar;

// CHECK-DAG: br: ({{.*}}) perms = UNIQUE | NON_NULL, flags = FIXED
// CHECK-DAG: bz: ({{.*}}) perms = UNIQUE | NON_NULL, flags = FIXED
// CHECK-DAG: x: ({{.*}}) perms = UNIQUE | NON_NULL, flags = FIXED
// CHECK-DAG: y: ({{.*}}) perms = UNIQUE | NON_NULL, flags = FIXED
// CHECK-DAG: br: ({{.*}}) perms = UNIQUE | NON_NULL | HEAP | STACK, flags = FIXED
// CHECK-DAG: bz: ({{.*}}) perms = UNIQUE | NON_NULL | HEAP | STACK, flags = FIXED
// CHECK-DAG: x: ({{.*}}) perms = UNIQUE | NON_NULL | HEAP | STACK, flags = FIXED
// CHECK-DAG: y: ({{.*}}) perms = UNIQUE | NON_NULL | HEAP | STACK, flags = FIXED
// CHECK-DAG: "s": addr_of flags = FIXED
// CHECK-DAG: "STATIC_PTR": addr_of flags = FIXED, type flags = FIXED#{{.*}}

Expand Down
Loading

0 comments on commit 644d80b

Please sign in to comment.