souper doesn't exploit assume() about souper HOT 22 OPEN

Looks like probably a phase ordering problem: Souper finds the optimization after the C code above is optimized using only SROA and inlining.

from souper.

I would guess that SROA doesn't have any effect, as there are no aggregates in the code. That inlining is needed makes sense, because we're not doing interprocedural analysis, and inlining will not happen by default at the lowest optimisation level.

from souper.

SROA is the new mem2reg.

from souper.

I'll review the output of opt -print-after-all when I get a chance, but my guess is that Souper isn't running until some pass has already eliminated the unreachable instructions. It might be InstCombine that does this, for example.

from souper.

Ok, I think I'm simply confused on how to reproduce this. How should I invoke Souper?

from souper.

If by "reproduce this" you mean "reproduce Souper failing to optimize the code to return 1" then you should run something like:

sclang -c -O2 foo.c

from souper.

The problem seems to be that even before the instruction combiner and inliner are called for the first time, assume has been transformed from:

define internal void @assume(i32 %x) #1 {
entry:
  %x.addr = alloca i32, align 4
  store i32 %x, i32* %x.addr, align 4, !tbaa !2
  %0 = load i32* %x.addr, align 4, !tbaa !2
  %tobool = icmp ne i32 %0, 0
  br i1 %tobool, label %if.end, label %if.then

if.then:                                          ; preds = %entry
  unreachable

if.end:                                           ; preds = %entry
  ret void
}

into (CFG simpification)

define internal void @assume(i32 %x) #1 {
entry:
  %x.addr = alloca i32, align 4
  store i32 %x, i32* %x.addr, align 4, !tbaa !2
  ret void
}

into (SROA)

define internal void @assume(i32 %x) #1 {
entry:
  ret void
}

So, yes, the unreachable branch is being dropped.

from souper.

Ok, thanks! Perhaps what is called for here is a command-line flag to the Souper pass that causes it to run early? It has to run after SROA and inlining and ideally after stuff like adce and constant propagation, but before CFG simplify and probably also before InstCombine.

from souper.

Alternatively, replace the implementation of assume by

static inline void assume (int x) {
  __builtin_assume(x);
}

and support the llvm.assume intrinsic. However, you might have had more in mind than supporting an assume function?

from souper.

I hadn't heard of __builtin_assume(), is it new? Last I heard, LLVM's story was to use "unreachable" for this purpose. Yes, let's certainly use this new thing if it works better.

from souper.

I just took a look at @llvm.assume, it seems to stick around through all of the optimization passes, I guess it is elided only in the backend. Yes, we should definitely modify Souper to generate the appropriate path condition when it sees this intrinsic!

from souper.

That would be awesome! I can't wait to play around with assume() to see how often it could be used in, say, libstdc++, to help optimization. I hope that at least /some/ of all those class invariants and function preconditions that currently only live in comments or asserts could be exploited by Souper. :)

from souper.

I thought I give this a go, but it's apparent slightly trivial than I thought. Starting from:

define i32 @add1(i32 %x, i32 %y) #0 {
entry:
  %and.i = and i32 %x, 1
  %tobool.i7 = icmp ne i32 %and.i, 0
  tail call void @llvm.assume(i1 %tobool.i7) #1
  %and.i6 = and i32 %y, 1
  %tobool.i = icmp ne i32 %and.i6, 0
  tail call void @llvm.assume(i1 %tobool.i) #1
  %add = add nsw i32 %y, %x
  %and.i5 = and i32 %add, 1
  %0 = xor i32 %and.i5, 1
  ret i32 %0
}

What I thought was that I could generate something like:

%0:i32 = var
%1:i32 = and 1:i32, %0
%2:i1 = ne 0:i32, %1
pc %2 1:i1
%3:i32 = var
%4:i32 = and 1:i32, %3
%5:i1 = ne 0:i32, %4
pc %5 1:i1
%6:i32 = addnsw %0, %3
%7:i32 = and 1:i32, %6
%8:i32 = xor 1:i32, %7
infer %8

Which would then give me the proper replacement. However, what I get is %tobool.i7 and %tobool.i being replaced by true in the IR, but the return value stays as it is. I suspect I'm missing something fundamental here.

from souper.

Jeroen, can you explain your implementation strategy? I agree that extracting a path condition from an @llvm.assume is the right idea.

from souper.

My first attempt is here jeroenk/souper@720bdf1

Adding a few lines to ExprBuilder::addPathConditions

from souper.

I think your patch is correct, and that it does the right thing when we run standalone Souper. In the context of the pass, it isn't working -- Souper is generating the correct path conditions but then doing the wrong optimizations. I'll have more time to look at this later today hopefully.

from souper.

Basically it looks like a phase ordering bug -- something we haven't seen before.

from souper.

Interesting.

I should learn to give all the details. I was running Souper as an opt pass:
opt -load libsouperPass.dylib -souper -z3-path=/path/to/z3 test.bc
As far as I can tell, it seems that this implies that it's only running Souper followed by two verification passes. Wouldn't that indicate that it's something else than a phase ordering problem?

from souper.

Probably so. I'll try to help get to the bottom of this a bit later.

from souper.

Duh, so inference for integers of width larger than 1 is disabled by default in the pass. Enabling this does the trick.

from souper.

Before I turn this in a pull request, I think I need two things:

• Some test cases (obviously)
• Disabling replacements of instructions that (in)directly feed into assume instructions.

At least the direct ones need to be disabled, otherwise the added path condition will always the replace the assume(%v) with an assume(true). And, this is not very useful for any other passes that may want to use the assume.

from souper.

Jeroen, I think your second item will probably fix the phase ordering problem I saw easier.

from souper.