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

Add a flag to disable counterexamples with type punning through memory #1035

Open
nunoplopes opened this issue May 9, 2024 · 1 comment
Open
Labels
enhancement New feature or request memory Memory Model

Comments

@nunoplopes
Copy link
Member

So we don't get counterexamples with loads being poison.
We have something similar in place for the asm mode already. Can likely reuse that code.

for @regehr

@nunoplopes nunoplopes added enhancement New feature or request memory Memory Model labels May 9, 2024
@regehr
Copy link
Contributor

regehr commented May 9, 2024

just as a random example I get a lot of stuff like this where (if I understand correctly) a byte containing pointer data poisons the results

https://alive2.llvm.org/ce/z/i3P8Ad

define void @f(ptr %0, ptr %1) {
  %3 = load i32, ptr %0, align 8
  %4 = load i16, ptr %0, align 1
  %5 = insertelement <8 x i16> zeroinitializer, i16 %4, i64 0
  %6 = bitcast <8 x i16> %5 to <4 x i32>
  %7 = insertelement <4 x i32> zeroinitializer, i32 %3, i64 0
  %8 = shufflevector <4 x i32> %6, <4 x i32> %7, <4 x i32> <i32 0, i32 4, i32 1, i32 5>
  store <4 x i32> %8, ptr %0, align 4
  ret void
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request memory Memory Model
Projects
None yet
Development

No branches or pull requests

2 participants