Skip to content
New issue

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

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

Already on GitHub? # to your account

Comparison of bytes of allocas given to function arguments #435

Open
LebedevRI opened this issue Jun 22, 2020 · 7 comments · May be fixed by #753
Open

Comparison of bytes of allocas given to function arguments #435

LebedevRI opened this issue Jun 22, 2020 · 7 comments · May be fixed by #753
Labels
memory Memory Model

Comments

@LebedevRI
Copy link
Contributor

This code seems to not roundtrip to itself:

void use(char&);

void loop() {
    char storage[16] = {};
    for(char& c : storage) use(c);
}

https://godbolt.org/z/UPbp51

----------------------------------------
define void @_Z4loopv() {
%entry:
  %storage = alloca i64 16, align 16, dead
  %0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
  start_lifetime * %0
  memset * %0 align 16, i8 0, i64 16
  %add.ptr = gep inbounds * %storage, 16 x i64 0, 1 x i64 16
  br label %for.body

%for.body:
  %__begin1.09 = phi * [ %0, %entry ], [ %incdec.ptr, %for.body ]
  call void @_Z3useRc(nonnull dereferenceable(1) * %__begin1.09)
  %incdec.ptr = gep inbounds * %__begin1.09, 1 x i64 1
  %cmp = icmp eq * %incdec.ptr, %add.ptr
  br i1 %cmp, label %for.cond.cleanup, label %for.body

%for.cond.cleanup:
  free * %0 unconstrained
  ret void
}
=>
define void @_Z4loopv() {
%entry:
  %storage = alloca i64 16, align 16, dead
  %0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
  start_lifetime * %0
  memset * %0 align 16, i8 0, i64 16
  %add.ptr = gep inbounds * %storage, 16 x i64 0, 1 x i64 16
  br label %for.body

%for.body:
  %__begin1.09 = phi * [ %0, %entry ], [ %incdec.ptr, %for.body ]
  call void @_Z3useRc(nonnull dereferenceable(1) * %__begin1.09)
  %incdec.ptr = gep inbounds * %__begin1.09, 1 x i64 1
  %cmp = icmp eq * %incdec.ptr, %add.ptr
  br i1 %cmp, label %for.cond.cleanup, label %for.body

%for.cond.cleanup:
  free * %0 unconstrained
  ret void
}
ERROR: Precondition is always false

Summary:
  0 correct transformations
  0 incorrect transformations
  1 Alive2 errors

I wanted to play around and see what alive2 things about different memsets,
in particular dropping overflowing memset (should fail, but again fails with
ERROR: Precondition is always false), clamping overflowing memset (should pass,
but again fails with ERROR: Precondition is always false), etc.

@aqjune
Copy link
Member

aqjune commented Jun 22, 2020

Hi,
Alive2 deals with a loop by unrolling it constant times (actually only once currently, and making a nice unroller is our future goal). In this case, it has a loop that iterates 16 times, which is more than the number of unroll count, making Alive2 raise 'precondition is false'.
For an equivalent test, you can try https://godbolt.org/z/GZtUG2 instead.

@LebedevRI
Copy link
Contributor Author

Aha, okay, thank you. But then, i'm having trouble doing mental gymnastics to understand
why the following refinement is correct? Am i simply using a wrong sink?

https://godbolt.org/z/8cdF77

----------------------------------------
define void @src(i32 %i, i8 %c) {
%entry:
  %storage = alloca i64 16, align 16, dead
  %0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
  start_lifetime * %0
  memset * %0 align 16, i8 %c, i64 16
  %idxprom = sext i32 %i to i64
  %arrayidx = gep inbounds * %storage, 16 x i64 0, 1 x i64 %idxprom
  call void @_Z3useRc(nonnull dereferenceable(1) * %arrayidx)
  free * %0 unconstrained
  ret void
}
=>
define void @tgt(i32 %i, i8 %c) {
%entry:
  %storage = alloca i64 16, align 16, dead
  %0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
  start_lifetime * %0
  memset * %0 align 16, i8 0, i64 0
  %idxprom = sext i32 %i to i64
  %arrayidx = gep inbounds * %storage, 16 x i64 0, 1 x i64 %idxprom
  call void @_Z3useRc(nonnull dereferenceable(1) * %arrayidx)
  free * %0 unconstrained
  ret void
}
Transformation seems to be correct!

test.ll.txt

@aqjune
Copy link
Member

aqjune commented Jun 22, 2020

It is because Alive2 does not implement comparison of bytes of allocas given to function arguments yet, sorry :)
This feature should be added soon - I'm currently working on it. This is important for reproducing a few bugzilla reports as well.
I'll leave a comment here after the feature is added.

@LebedevRI
Copy link
Contributor Author

Thank you!

@LebedevRI LebedevRI changed the title ERROR: Precondition is always false Comparison of bytes of allocas given to function arguments Jun 22, 2020
@nunoplopes nunoplopes added the memory Memory Model label Jan 19, 2021
@aqjune
Copy link
Member

aqjune commented Oct 10, 2021

@nunoplopes Would it be good if I implement this functionality? :)

Instead of creating a patch for whole escaped block mapping encoding, I'd like to start with a simple patch that only checks the bytes of the given allocas only.

@nunoplopes
Copy link
Member

sure! should I take over #746 then?

@aqjune
Copy link
Member

aqjune commented Oct 10, 2021

Yes, I am afraid that I won't have time for #746 in the near future. :( I am sorry about it.
The escaped local block thing is something I promised to carry back to the main branch.
I will make a patch for this soon.

@aqjune aqjune linked a pull request Oct 10, 2021 that will close this issue
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
memory Memory Model
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants