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.

Sign up for GitHub

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

Jump to bottom

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
@nunoplopes nunoplopes mentioned this issue Jan 19, 2021
Open
@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
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
memory Memory Model
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Encode the basic refinement of escaped local blocks aqjune/alive2
3 participants
@LebedevRI @nunoplopes @aqjune