Skip to content

intptrcast (with many different seeds) does not explore all possible executions #866

@RalfJung

Description

@RalfJung

The following assertion is currently guaranteed to pass in Miri, no matter the seed:

fn main() {
  let ptr1 = Box::into_raw(Box::new(0)) as usize;
  let ptr2 = Box::into_raw(Box::new(0)) as usize;
  assert!(ptr2 > ptr1);
}

This is because we basically have a "bump allocator" as our implementation of int-to-ptr casts. Ideally, when exploring many seeds, all possible allocation patterns should arise; but at least we could try to find a way to be a bit less predictable than we currently are, so that failing the assertion above becomes a possibility.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-intptrcastArea: affects int2ptr and ptr2int castsC-enhancementCategory: a PR with an enhancement or an issue tracking an accepted enhancement

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions