diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs index 9f81e5ce66..dc22282551 100644 --- a/c2rust-analyze/src/analyze.rs +++ b/c2rust-analyze/src/analyze.rs @@ -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); } @@ -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); @@ -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); @@ -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); diff --git a/c2rust-analyze/src/context.rs b/c2rust-analyze/src/context.rs index 231c403f0d..3423fbf4c3 100644 --- a/c2rust-analyze/src/context.rs +++ b/c2rust-analyze/src/context.rs @@ -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`, but stack and static + /// pointers both cannot. + const STACK = 0x0200; } } @@ -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! { @@ -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; } } @@ -447,9 +468,15 @@ impl<'a, 'tcx> AnalysisCtxt<'_, 'tcx> { pub fn string_literal_perms( &'a self, - ) -> impl Iterator + PhantomLifetime<'tcx> + 'a { - self.string_literal_tys() - .map(|lty| (lty.label, PermissionSet::STRING_LITERAL)) + ) -> impl Iterator + 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) { diff --git a/c2rust-analyze/src/dataflow/mod.rs b/c2rust-analyze/src/dataflow/mod.rs index 27dada6dcc..fa7224a91b 100644 --- a/c2rust-analyze/src/dataflow/mod.rs +++ b/c2rust-analyze/src/dataflow/mod.rs @@ -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)] diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs index 2cca9f0658..9120747ead 100644 --- a/c2rust-analyze/src/dataflow/type_check.rs +++ b/c2rust-analyze/src/dataflow/type_check.rs @@ -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; @@ -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); } @@ -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() { diff --git a/c2rust-analyze/tests/filecheck/alias1.rs b/c2rust-analyze/tests/filecheck/alias1.rs index a68907447a..36a65f03e5 100644 --- a/c2rust-analyze/tests/filecheck/alias1.rs +++ b/c2rust-analyze/tests/filecheck/alias1.rs @@ -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; diff --git a/c2rust-analyze/tests/filecheck/alias2.rs b/c2rust-analyze/tests/filecheck/alias2.rs index daa16e419f..55742ca356 100644 --- a/c2rust-analyze/tests/filecheck/alias2.rs +++ b/c2rust-analyze/tests/filecheck/alias2.rs @@ -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; } diff --git a/c2rust-analyze/tests/filecheck/alias3.rs b/c2rust-analyze/tests/filecheck/alias3.rs index d15324f205..073d44fde3 100644 --- a/c2rust-analyze/tests/filecheck/alias3.rs +++ b/c2rust-analyze/tests/filecheck/alias3.rs @@ -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; diff --git a/c2rust-analyze/tests/filecheck/alloc.rs b/c2rust-analyze/tests/filecheck/alloc.rs index 8a30d884f3..58f4058a2a 100644 --- a/c2rust-analyze/tests/filecheck/alloc.rs +++ b/c2rust-analyze/tests/filecheck/alloc.rs @@ -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::() 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::() 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::() 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::() 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::() as libc::c_ulong) as *mut i32; let mut len = 0; let mut capacity = 2; @@ -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::()) as libc::c_ulong, diff --git a/c2rust-analyze/tests/filecheck/cast.rs b/c2rust-analyze/tests/filecheck/cast.rs index 523fbe58d4..d0d342042a 100644 --- a/c2rust-analyze/tests/filecheck/cast.rs +++ b/c2rust-analyze/tests/filecheck/cast.rs @@ -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; diff --git a/c2rust-analyze/tests/filecheck/fields.rs b/c2rust-analyze/tests/filecheck/fields.rs index 563df5003a..f187f295cc 100644 --- a/c2rust-analyze/tests/filecheck/fields.rs +++ b/c2rust-analyze/tests/filecheck/fields.rs @@ -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; diff --git a/c2rust-analyze/tests/filecheck/foreign.rs b/c2rust-analyze/tests/filecheck/foreign.rs index bb60121a58..59b668dc02 100644 --- a/c2rust-analyze/tests/filecheck/foreign.rs +++ b/c2rust-analyze/tests/filecheck/foreign.rs @@ -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#{{.*}} diff --git a/c2rust-analyze/tests/filecheck/insertion_sort.rs b/c2rust-analyze/tests/filecheck/insertion_sort.rs index 59049d89f7..98be54c8f4 100644 --- a/c2rust-analyze/tests/filecheck/insertion_sort.rs +++ b/c2rust-analyze/tests/filecheck/insertion_sort.rs @@ -6,26 +6,26 @@ extern crate libc; #[no_mangle] // CHECK-LABEL: final labeling for "insertion_sort" -// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe extern "C" fn insertion_sort(n: libc::c_int, p: *mut libc::c_int) { let mut i: libc::c_int = 1 as libc::c_int; while i < n { - // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p.offset(i as isize)): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p.offset(i as isize)): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# let tmp: libc::c_int = *p.offset(i as isize); let mut j: libc::c_int = i; - // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p.offset{{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p.offset{{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# while j > 0 as libc::c_int && *p.offset((j - 1 as libc::c_int) as isize) > tmp { - // CHECK-DAG: ([[@LINE+4]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+3]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+2]]: p.offset((j {{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p.offset(j {{.*}}): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+4]]: p): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+3]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+2]]: p.offset((j {{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p.offset(j {{.*}}): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK# *p.offset(j as isize) = *p.offset((j - 1 as libc::c_int) as isize); j -= 1 } - // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p.offset(j {{.*}}): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p.offset(j {{.*}}): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK# *p.offset(j as isize) = tmp; i += 1 } diff --git a/c2rust-analyze/tests/filecheck/known_fn.rs b/c2rust-analyze/tests/filecheck/known_fn.rs index 1f3d071baa..19a8347edb 100644 --- a/c2rust-analyze/tests/filecheck/known_fn.rs +++ b/c2rust-analyze/tests/filecheck/known_fn.rs @@ -9,7 +9,7 @@ extern "C" { // CHECK-LABEL: final labeling for "known_fn" pub fn known_fn() { - // CHECK-DAG: ([[@LINE+3]]: path): addr_of = UNIQUE | NON_NULL, type = READ | UNIQUE | OFFSET_ADD | NON_NULL# + // CHECK-DAG: ([[@LINE+3]]: path): addr_of = UNIQUE | NON_NULL | STACK, type = READ | UNIQUE | OFFSET_ADD | NON_NULL | STACK# // CHECK-LABEL: type assignment for "known_fn": // CHECK-DAG: ([[@LINE+1]]: path): &[i8] let path = b".\0" as *const u8 as *const c_char; diff --git a/c2rust-analyze/tests/filecheck/non_null.rs b/c2rust-analyze/tests/filecheck/non_null.rs index 2d067c31b2..06d1da8b20 100644 --- a/c2rust-analyze/tests/filecheck/non_null.rs +++ b/c2rust-analyze/tests/filecheck/non_null.rs @@ -3,7 +3,7 @@ use std::ptr; // CHECK-LABEL: final labeling for "f" fn f(cond: bool) { let x = 1_i32; - // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE# + // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE | STACK# let mut y = ptr::addr_of!(x); if cond { y = ptr::null(); @@ -13,7 +13,7 @@ fn f(cond: bool) { // CHECK-LABEL: final labeling for "g" fn g(cond: bool) { let x = 1_i32; - // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL# + // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL | STACK# let y = ptr::addr_of!(x); if cond { let z = ptr::null::(); @@ -23,9 +23,9 @@ fn g(cond: bool) { // CHECK-LABEL: final labeling for "h" fn h(cond: bool) { let x = 1_i32; - // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL# + // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL | STACK# let y = ptr::addr_of!(x); - // CHECK: ([[@LINE+1]]: z): {{.*}}, type = UNIQUE# + // CHECK: ([[@LINE+1]]: z): {{.*}}, type = UNIQUE | STACK# let z = if cond { y } else { @@ -38,7 +38,7 @@ fn h(cond: bool) { // CHECK-LABEL: final labeling for "f_zero" fn f_zero(cond: bool) { let x = 1_i32; - // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE# + // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE | STACK# let mut y = ptr::addr_of!(x); if cond { y = 0 as *const _; diff --git a/c2rust-analyze/tests/filecheck/non_null_force.rs b/c2rust-analyze/tests/filecheck/non_null_force.rs index a6757f5813..0d25f9f955 100644 --- a/c2rust-analyze/tests/filecheck/non_null_force.rs +++ b/c2rust-analyze/tests/filecheck/non_null_force.rs @@ -9,32 +9,32 @@ use std::ptr; // CHECK-LABEL: final labeling for "f" fn f(cond: bool) { let x = 1_i32; - // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = (empty)# + // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = 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 = (empty)# + // CHECK: ([[@LINE+1]]: y): {{.*}}, type = 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# +// CHECK: ([[@LINE+2]]: p): {{.*}}, type = 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 = (empty)# + // CHECK: ([[@LINE+1]]: mut q): {{.*}}, type = 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 = (empty)# + // CHECK: ([[@LINE+1]]: r): {{.*}}, type = STACK# let r = q; } diff --git a/c2rust-analyze/tests/filecheck/offset1.rs b/c2rust-analyze/tests/filecheck/offset1.rs index 80576bfe34..ce97836193 100644 --- a/c2rust-analyze/tests/filecheck/offset1.rs +++ b/c2rust-analyze/tests/filecheck/offset1.rs @@ -1,18 +1,18 @@ use std::ptr; // CHECK-LABEL: final labeling for "offset1_const" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset1_const(x: *mut i32) -> i32 { - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: x.offset(1)): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: x.offset(1)): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# *x.offset(1) } // CHECK-LABEL: final labeling for "offset1_unknown" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset1_unknown(x: *mut i32, off: isize) -> i32 { - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: x.offset(off)): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: x.offset(off)): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# *x.offset(off) } @@ -23,18 +23,18 @@ pub unsafe fn offset1_usize(x: *mut i32, off: usize) -> i32 { */ // CHECK-LABEL: final labeling for "offset1_immut" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset1_immut(x: *const i32, off: isize) -> i32 { - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: x.offset(off)): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: x.offset(off)): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# *x.offset(off) } // CHECK-LABEL: final labeling for "offset1_double" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset1_double(x: *mut i32, off: isize) -> i32 { - // CHECK-DAG: ([[@LINE+3]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+2]]: x.offset(off)): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: x.offset{{.*}}...{{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+3]]: x): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+2]]: x.offset(off)): {{.*}}type = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: x.offset{{.*}}...{{.*}}): {{.*}}type = READ | UNIQUE | NON_NULL | HEAP | STACK# *x.offset(off).offset(off) } diff --git a/c2rust-analyze/tests/filecheck/offset2.rs b/c2rust-analyze/tests/filecheck/offset2.rs index 160c559a5c..f9298cc9f5 100644 --- a/c2rust-analyze/tests/filecheck/offset2.rs +++ b/c2rust-analyze/tests/filecheck/offset2.rs @@ -1,25 +1,25 @@ use std::ptr; // CHECK-LABEL: final labeling for "offset2_good" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset2_good(x: *mut i32, off: isize) { - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL | HEAP | STACK# let p = x.offset(off); - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL | HEAP | STACK# let q = x.offset(off); *q = 1; } // CHECK-LABEL: final labeling for "offset2_bad" -// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | OFFSET_ADD | OFFSET_SUB | NON_NULL# +// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# pub unsafe fn offset2_bad(x: *mut i32, off: isize) { - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL | HEAP | STACK# let p = x.offset(off); - // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = OFFSET_ADD | OFFSET_SUB | NON_NULL# - // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL# + // CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = OFFSET_ADD | OFFSET_SUB | NON_NULL | HEAP | STACK# + // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL | HEAP | STACK# let q = x.offset(off); *p = 1; }