Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for some operations on raw pointers #1217

Open
Armael opened this issue Nov 4, 2024 · 0 comments
Open

Support for some operations on raw pointers #1217

Armael opened this issue Nov 4, 2024 · 0 comments

Comments

@Armael
Copy link
Contributor

Armael commented Nov 4, 2024

Trying to write the following test on top of #1169 currently fails, because operations (such as ==) on raw pointers are not currently supported:

extern crate creusot_contracts;
use creusot_contracts::*;

#[trusted]
fn make_ptrs() -> (*const i32, *const i32) {
    (Box::into_raw(Box::new(42)), Box::into_raw(Box::new(12)))
}

pub fn test() {
    let (p, q) = make_ptrs();

    if p == std::ptr::null() {
        proof_assert!(p@ == 0);
    } else {
        proof_assert!(p@ != 0);
    }

    if p == q {
        proof_assert!(p == q);
        proof_assert!(p@ == q@);
    }

    if std::ptr::addr_eq(p, q) {
        proof_assert!(p@ == q@);
    }

    let null1: *const i32 = std::ptr::null();
    let null2: *const i32 = std::ptr::null();
    proof_assert!(null1@ == null2@ && null1@ == 0);
}
thread 'rustc' panicked at creusot/src/backend/program.rs:1202:14:
internal error: entered unreachable code: non-primitive type for binary operation Eq *const i32
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Copy-pasting some notes from @xldenis on steps to take to solve the issue:

  • stop using opaque_ptr as the type for all pointers. We need ptr 't or maybe even mut_ptr 't and const_ptr 't. These need to be added in prelude.coma and backend/ty.rs must be updated accordingly (this should be an easy first step)
  • handle pointer equality in MIR. Primitive types use BinOp::Eq in MIR, but here we probably want to use PartialEq::eq instead.

Something that doesn't appear in this test but would be useful to handle as well are pointer->pointer casts between *mut and *const.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant