alivetoolkit / alive2 Goto Github PK
View Code? Open in Web Editor NEWAutomatic verification of LLVM optimizations
License: MIT License
alive2's Issues
Printing counterexamples with `undef` vars always yields undef
Not sure how to solve this... evaluation of registers with undef prints bogus values:
----------------------------------------
%res = usub_sat i8 undef, %y
ret i8 %res
=>
ret undef
ERROR: Value mismatch
Example:
i8 %y = #xe9 (233, -23)
Source:
i8 %res = undef # expression is (ite (bvule undef_3 #xe9) #x00 (bvadd #x17 undef_3))
Negative tests for malloc/free
I'll add negative tests (XFAIL) for malloc/free, updating lit if needed.
Check Z3's unknown reason
We always declare it as timeout, but it might not be the case.
ir/type.cpp:129:3: runtime error: execution reached an unreachable program point
Name: zz
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, i8 %X
%Y = extractvalue i8 %X, 0
%Z = extractvalue i8 %X, 1
=>
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, i8 %X
%Y = i8 0
%Z = i1 false
$ ./alive -root-only /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
----------------------------------------
Name: zz
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, %X
%Y = extractvalue i8 %X, 0
%Z = extractvalue i8 %X, 1
=>
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, %X
%Y = i8 0
%Z = i1 0
../ir/type.cpp:129:3: runtime error: execution reached an unreachable program point
#0 0x61a949 in IR::Type::getAsStructType() const /home/lebedevri/src/alive2/build-Clang-release/../ir/type.cpp:129:3
#1 0x54b37b in IR::ExtractValue::getTypeConstraints(IR::Function const&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/instr.cpp:581:21
#2 0x4f9fa9 in IR::BasicBlock::getTypeConstraints(IR::Function const&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/function.cpp:15:12
#3 0x4fc019 in IR::Function::getTypeConstraints() const /home/lebedevri/src/alive2/build-Clang-release/../ir/function.cpp:53:14
#4 0x688eca in tools::TransformVerify::getTypings() const /home/lebedevri/src/alive2/build-Clang-release/../tools/transform.cpp:314:18
#5 0x44594a in main /home/lebedevri/src/alive2/build-Clang-release/../tools/alive.cpp:107:25
#6 0x7fcda823409a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409a)
#7 0x39a029 in _start (/home/lebedevri/src/alive2/build-Clang-release/alive+0x39a029)
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior ../ir/type.cpp:129:3 in
Aborted
Should alive2 be added to oss-fuzz?
Simple transform times out
Getting this with latest alive2 on OS X.
Johns-MacBook-Pro:build johnregehr$ ./alive foo2.opt
Processing foo2.opt..
----------------------------------------
%a = add i64 %b, %b
=>
%a = shl %b, 1
ERROR: Timeout
Johns-MacBook-Pro:build johnregehr$ ./alive foo3.opt
Processing foo3.opt..
----------------------------------------
%a = add i65 %b, %b
=>
%a = shl %b, 1
Doesn't type check!
Johns-MacBook-Pro:build johnregehr$
smt/expr.cpp:716:40: runtime error: negation of 1 cannot be represented in type 'unsigned long long'
----------------------------------------
Name: zz
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 1, %undef0
%Y = extractvalue {i8, i1} %X, 0
%Z = extractvalue {i8, i1} %X, 1
%YisZero = icmp eq %Y, 0
%ZisZero = icmp eq %Z, 0
%Zero = and i1 %YisZero, %ZisZero
ret i1 %Zero
=>
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 1, %undef0
%Y = i8 0
%Z = i1 0
%YisZero = i1 1
%ZisZero = i1 1
%Zero = i1 1
ret i1 %Zero
../smt/expr.cpp:716:40: runtime error: negation of 1 cannot be represented in type 'unsigned long long'
#0 0x656a19 in auto smt::expr::operator&(smt::expr const&) const::$_7::operator()<smt::expr const, smt::expr const>(smt::expr const&, smt::expr const&) const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:716:40
#1 0x65646b in smt::expr::operator&(smt::expr const&) const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:738:18
#2 0x5322c4 in IR::BinOp::toSMT(IR::State&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/instr.cpp:226:13
#3 0x5bdede in IR::State::exec(IR::Value const&) /home/lebedevri/src/alive2/build-Clang-release/../ir/state.cpp:23:16
#4 0x6c4d7a in util::sym_exec(IR::State&) /home/lebedevri/src/alive2/build-Clang-release/../util/symexec.cpp:33:20
#5 0x6847ce in tools::TransformVerify::verify() const /home/lebedevri/src/alive2/build-Clang-release/../tools/transform.cpp:246:5
#6 0x445a85 in main /home/lebedevri/src/alive2/build-Clang-release/../tools/alive.cpp:118:30
#7 0x7f2cc119c09a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409a)
#8 0x39a029 in _start (/home/lebedevri/src/alive2/build-Clang-release/alive+0x39a029)
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior ../smt/expr.cpp:716:40 in
ERROR: Value mismatch for i8 %Y
Example:
i8 %a = ?
i8 %undef0 = #x00 (0)
{i8, i1} %X = { #x01 (1, -255), #x0 (0) }
Source value: #x01 (1, -255)
Target value: #x00 (0)
Add support for optimization of known library functions
I have these two .ll files, the second one is the optimized version of the first.
; ModuleID = './FicE/2581362695652647725/263564.bc'
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-musl"
; Function Attrs: noinline nounwind sspstrong uwtable
define i32 @bla(i8 signext) #0 align 2 {
%2 = sext i8 %0 to i32
%3 = call i32 @isdigit(i32 %2) #2
%4 = icmp ne i32 %3, 0
br i1 %4, label %5, label %8
5: ; preds = %1
%6 = sext i8 %0 to i32
%7 = sub i32 %6, 48
br label %30
8: ; preds = %1
%9 = sext i8 %0 to i32
%10 = icmp sge i32 %9, 97
br i1 %10, label %11, label %18
11: ; preds = %8
%12 = sext i8 %0 to i32
%13 = icmp sle i32 %12, 102
br i1 %13, label %14, label %18
14: ; preds = %11
%15 = sext i8 %0 to i32
%16 = sub i32 %15, 97
%17 = add i32 %16, 10
br label %29
18: ; preds = %11, %8
%19 = sext i8 %0 to i32
%20 = icmp sge i32 %19, 65
br i1 %20, label %21, label %28
21: ; preds = %18
%22 = sext i8 %0 to i32
%23 = icmp sle i32 %22, 70
br i1 %23, label %24, label %28
24: ; preds = %21
%25 = sext i8 %0 to i32
%26 = sub i32 %25, 65
%27 = add i32 %26, 10
br label %28
28: ; preds = %24, %21, %18
%.0 = phi i32 [ %27, %24 ], [ 0, %21 ], [ 0, %18 ]
br label %29
29: ; preds = %28, %14
%.1 = phi i32 [ %17, %14 ], [ %.0, %28 ]
br label %30
30: ; preds = %29, %5
%.2 = phi i32 [ %7, %5 ], [ %.1, %29 ]
ret i32 %.2
}
; Function Attrs: nounwind readonly
declare i32 @isdigit(i32) #1
attributes #0 = { noinline nounwind sspstrong uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="4" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { nounwind readonly "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="4" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #2 = { nounwind readonly }
; ModuleID = 'foo.ll'
source_filename = "foo.ll"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-musl"
; Function Attrs: noinline nounwind sspstrong uwtable
define i32 @bla(i8 signext) #0 align 2 {
%2 = sext i8 %0 to i32
%isdigittmp = add nsw i32 %2, -48
%isdigit = icmp ult i32 %isdigittmp, 10
br i1 %isdigit, label %.thread1, label %3
3: ; preds = %1
%4 = icmp sgt i8 %0, 96
br i1 %4, label %5, label %8
5: ; preds = %3
%6 = icmp slt i8 %0, 103
%7 = add nsw i32 %2, -87
%spec.select = select i1 %6, i32 %7, i32 0
ret i32 %spec.select
8: ; preds = %3
%.off = add i8 %0, -65
%9 = icmp ult i8 %.off, 6
%10 = add nsw i32 %2, -55
%spec.select2 = select i1 %9, i32 %10, i32 0
ret i32 %spec.select2
.thread1: ; preds = %1
ret i32 %isdigittmp
}
; Function Attrs: nounwind readonly
declare i32 @isdigit(i32) #1
attributes #0 = { noinline nounwind sspstrong uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="4" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { nounwind readonly "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="4" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
here's what alive-tv says:
regehr@john-home:~/wllvm$ ~/alive2/build/alive-tv --disable-poison-input --disable-undef-input foo.ll foo2.ll
----------------------------------------
define i32 @bla(i8 %0) {
%1:
%12 = sext i8 %0 to i32
%13 = call i32 @isdigit(i32 %12)
%14 = icmp ne i32 %13, 0
br i1 %14, label %2, label %3
%2:
%15 = sext i8 %0 to i32
%16 = sub i32 %15, 48
br label %11
%3:
%17 = sext i8 %0 to i32
%18 = icmp sge i32 %17, 97
br i1 %18, label %4, label %6
%4:
%19 = sext i8 %0 to i32
%20 = icmp sle i32 %19, 102
br i1 %20, label %5, label %6
%5:
%21 = sext i8 %0 to i32
%22 = sub i32 %21, 97
%23 = add i32 %22, 10
br label %10
%6:
%24 = sext i8 %0 to i32
%25 = icmp sge i32 %24, 65
br i1 %25, label %7, label %9
%7:
%26 = sext i8 %0 to i32
%27 = icmp sle i32 %26, 70
br i1 %27, label %8, label %9
%8:
%28 = sext i8 %0 to i32
%29 = sub i32 %28, 65
%30 = add i32 %29, 10
br label %9
%9:
%.0 = phi i32 [ %30, %8 ], [ 0, %7 ], [ 0, %6 ]
br label %10
%10:
%.1 = phi i32 [ %23, %5 ], [ %.0, %9 ]
br label %11
%11:
%.2 = phi i32 [ %16, %2 ], [ %.1, %10 ]
ret i32 %.2
}
=>
define i32 @bla(i8 %0) {
%1:
%5 = sext i8 %0 to i32
%isdigittmp = add nsw i32 %5, 4294967248
%isdigit = icmp ult i32 %isdigittmp, 10
br i1 %isdigit, label %.thread1, label %2
%2:
%6 = icmp sgt i8 %0, 96
br i1 %6, label %3, label %4
%3:
%7 = icmp slt i8 %0, 103
%8 = add nsw i32 %5, 4294967209
%spec.select = select i1 %7, i32 %8, i32 0
ret i32 %spec.select
%4:
%.off = add i8 %0, 191
%9 = icmp ult i8 %.off, 6
%10 = add nsw i32 %5, 4294967241
%spec.select2 = select i1 %9, i32 %10, i32 0
ret i32 %spec.select2
%.thread1:
ret i32 %isdigittmp
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
i8 %0 = #x62 (98)
Source:
i32 %12 = #x00000062 (98)
i32 %13 = #x00000200 (512)
i1 %14 = #x1 (0)
i32 %15 = #x00000062 (98)
i32 %16 = #x00000032 (50)
i32 %17 = #x00000062 (98)
i1 %18 = #x1 (0)
i32 %19 = #x00000062 (98)
i1 %20 = #x1 (0)
i32 %21 = #x00000062 (98)
i32 %22 = #x00000001 (1, -4294967295)
i32 %23 = #x0000000b (11, -4294967285)
i32 %24 = #x00000062 (98)
i1 %25 = #x1 (0)
i32 %26 = #x00000062 (98)
i1 %27 = #x0 (00)
i32 %28 = #x00000062 (98)
i32 %29 = #x00000021 (33, -4294967263)
i32 %30 = #x0000002b (43, -4294967253)
i32 %.0 = #x0000002b (43, -4294967253)
i32 %.1 = #x0000000b (11, -4294967285)
i32 %.2 = #x00000032 (50)
Target:
i32 %5 = #x00000062 (98)
i32 %isdigittmp = #x00000032 (50)
i1 %isdigit = #x0 (00)
i1 %6 = #x1 (0)
i1 %7 = #x1 (0)
i32 %8 = #x0000000b (11, -4294967285)
i32 %spec.select = #x0000000b (11, -4294967285)
i8 %.off = #x21 (33, -223)
i1 %9 = #x0 (00)
i32 %10 = #x0000002b (43, -4294967253)
i32 %spec.select2 = #x00000000 (0)
Source value: #x00000032 (50)
Target value: #x0000000b (11, -4294967285)
now the confusing thing is that if I supply this main:
int bla(int);
#include <stdio.h>
int main(void) {
printf("%d\n", bla(98));
return 0;
}
and run it against the original function, it says that the function emits 11, not 50, as alive claims. so I suspect that perhaps something's wrong with alive here maybe.
the other confusing thing is that alive seems to be saying that isdigit() returns 200. I suppose that happens because it's modeled using a UF that can return anything? in this case the result of isdigit() is only compared against 0, so the actual value doesn't matter, but in other cases we could end up getting false positives by returning an out-of-contract value.
also notice that the optimized code doesn't contain the call to isdigit(), I suppose due to SimplifyLibCalls.
anyway I haven't yet fully traced through why alive thinks the original function returns 50 instead of 11 but wanted to post this in the meantime.
we should test LLVM integration
We should have testing for alive-tv and the tv opt plugin. This isn't too hard, @regehr will work on it at some point. We should also have CI do this, which requires CI to have access to an LLVM compiled with RTTI/EH, which seems to mean that we have to build our own LLVM. This isn't too difficult via docker, and I have this working, but what I haven't done is figured out how to integrate tests that run in a custom docker image with the other tests in our .travis.yml.
Refinement of function calls is incomplete
We need to support fn(poison) -> fn(42). Right now it will error out.
Add support for void functions
Compiling against latest LLVM I'm getting a lot of these. Haven't looked into it yet beyond this.
FAIL: LLVM :: Transforms/ADCE/2017-08-21-DomTree-deletions.ll (111 of 4565)
******************** TEST 'LLVM :: Transforms/ADCE/2017-08-21-DomTree-deletions.ll' FAILED ********************
Script:
--
: 'RUN: at line 1'; /home/regehr/opt-alive.sh < /home/regehr/llvm/test/Transforms/ADCE/2017-08-21-DomTree-deletions.ll -adce | /home/regehr/llvm/build/bin/llvm-dis
: 'RUN: at line 2'; /home/regehr/opt-alive.sh < /home/regehr/llvm/test/Transforms/ADCE/2017-08-21-DomTree-deletions.ll -adce -verify-dom-info | /home/regehr/llvm/build/bin/llvm-dis
--
Exit Code: 1
Command Output (stderr):
--
+ : 'RUN: at line 1'
+ /home/regehr/llvm/build/bin/llvm-dis
+ /home/regehr/opt-alive.sh -adce
opt: /home/regehr/llvm-install/include/llvm/IR/Instructions.h:2991: llvm::Value* llvm::ReturnInst::getOperand(unsigned int) const: Assertion `i_nocapture < OperandTraits<ReturnInst>::operands(this) && "getOperand() out of range!"' failed.
Stack dump:
0. Program arguments: /home/regehr/llvm/build/bin/opt -load=/home/regehr/alive2/build/tv/tv.so -tv -adce -tv
1. Running pass 'Function Pass Manager' on module '<stdin>'.
2. Running pass 'Translation Validator' on function '@foo'
#0 0x0000000003c14f49 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:494:11
#1 0x0000000003c150f9 PrintStackTraceSignalHandler(void*) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:558:1
#2 0x0000000003c13236 llvm::sys::RunSignalHandlers() /home/regehr/llvm/build/../lib/Support/Signals.cpp:67:5
#3 0x0000000003c1580b SignalHandler(int) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:357:1
#4 0x00007fa82bab1890 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12890)
#5 0x00007fa82a55ae97 gsignal /build/glibc-OTsEL5/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
#6 0x00007fa82a55c801 abort /build/glibc-OTsEL5/glibc-2.27/stdlib/abort.c:81:0
#7 0x00007fa82a54c39a __assert_fail_base /build/glibc-OTsEL5/glibc-2.27/assert/assert.c:89:0
#8 0x00007fa82a54c412 (/lib/x86_64-linux-gnu/libc.so.6+0x30412)
#9 0x00007fa82a2e7e7b visitReturnInst /home/regehr/alive2/build/../tv/tv.cpp:252:0
#10 0x00007fa82a2e7e7b visitRet /home/regehr/llvm-install/include/llvm/IR/Instruction.def:127:0
#11 0x00007fa82a2e7e7b llvm::InstVisitor<(anonymous namespace)::llvm2alive, std::unique_ptr<IR::Instr, std::default_delete<IR::Instr> > >::visit(llvm::Instruction&) /home/regehr/llvm-install/include/llvm/IR/Instruction.def:127:0
#12 0x00007fa82a2eb089 run /home/regehr/alive2/build/../tv/tv.cpp:423:0
#13 0x00007fa82a2eb089 (anonymous namespace)::TVPass::runOnFunction(llvm::Function&) /home/regehr/alive2/build/../tv/tv.cpp:448:0
#14 0x00000000031dc3e8 llvm::FPPassManager::runOnFunction(llvm::Function&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1643:27
#15 0x00000000031dc875 llvm::FPPassManager::runOnModule(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1678:16
#16 0x00000000031dd02d (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1743:27
#17 0x00000000031dcb05 llvm::legacy::PassManagerImpl::run(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1856:16
#18 0x00000000031dd701 llvm::legacy::PassManager::run(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1887:3
#19 0x0000000000d8d74a main /home/regehr/llvm/build/../tools/opt/opt.cpp:862:12
#20 0x00007fa82a53db97 __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:344:0
#21 0x0000000000d419aa _start (/home/regehr/llvm/build/bin/opt+0xd419aa)
/home/regehr/opt-alive.sh: line 2: 21533 Aborted timeout 60 $HOME/llvm/build/bin/opt -load=$HOME/alive2/build/tv/tv.so -tv $@ -tv
/home/regehr/llvm/build/bin/llvm-dis: error: Invalid bitcode signature
--
Counter-proofing
I'm not sure how generally useful could that be done, but it it would be interesting
to have something opposite to Pre:conditions (#45).
E.g. i'm currently trying to generalize this proof:
Name: one truncation - the values being shifted should be 0 or 1, or the original widest input should be losslessly truncatable, or the other input should have at most lowest bit set
Pre: C1+C2 u< 64 && ( C11 == 0 || C22 == 0 || C11 == 1 || C22 == 1 || (countLeadingZeros(C11) u>= (64-32)) || (countLeadingZeros(C22) u>= (32-1)) )
%C1_64 = zext i8 C1 to i64
%C2_32 = zext i8 C2 to i32
%old_shift_of_x = lshr i64 C11, %C1_64
%old_shift_of_y = shl i32 C22, %C2_32
%old_trunc_of_shift_of_x = trunc i64 %old_shift_of_x to i32
%old_masked = and i32 %old_trunc_of_shift_of_x, %old_shift_of_y
%r = icmp ne i32 %old_masked, 0
=>
%C1_64 = zext i8 C1 to i64
%C2_64 = zext i8 C2 to i64
%new_shamt = add i64 %C1_64, %C2_64
%new_y_wide = zext i32 C22 to i64
%new_shift = shl i64 %new_y_wide, %new_shamt
%new_masked = and i64 %new_shift, C11
%r = icmp ne i64 %new_masked, 0
https://rise4fun.com/Alive/BFF (for https://bugs.llvm.org/show_bug.cgi?id=42399)
How can i tell if there is some other condition where the fold is valid that i didn't think of?
Granted, i'm not sure alive will generalize and pretty-print the preconditions for me,
that would be awesome, but might be a bit too much to ask for :)
memory model doesn't understand values stored through argument pointers
regehr@john-home:~$ ~/alive2/build/alive-tv foo1.ll foo2.ll
----------------------------------------
define void @foo(* %0) {
%1:
store i32 3, * %0, align 4
ret void void
}
=>
define void @foo(* %0) {
%1:
store i32 4, * %0, align 4
ret void void
}
Transformation seems to be correct!
Predicate support incomplete
Just a tracking issue.
prettyprint negative zero
this is for @zhengyangl. I think it would be very nice if we printed -0 instead of 0 for #x80000000
Johns-MacBook-Pro:alive2 johnregehr$ ~/alive2/build/alive-tv f2a.ll f2b.ll
----------------------------------------
define float @f1(float %0) {
%1:
%2 = fadd float %0, 0.000000
ret float %2
}
=>
define float @f1(float %0) {
%1:
ret float %0
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
float %0 = #x80000000 (0)
Source:
float %2 = #x00000000 (0)
Target:
Source value: #x00000000 (0)
Target value: #x80000000 (0)
Johns-MacBook-Pro:alive2 johnregehr$
Add support for call instructions
This might because of my old z3 version though..
$ php scripts/run.php /tmp/test.ll.bz2 "instcombine" ~/src/alive2/build-Clang-Sanitize/alive /build/llvm-build-GCC-release/bin/opt
Processing /tmp/test.ll.alive.opt..
Parse error in line: 9: expected token: ARROW, got: IDENTIFIER
$ bzcat /tmp/test.ll.bz2
; ============================================================================ ;
; One-use tests. We don't care about multi-uses here.
; ============================================================================ ;
declare void @use8(i8)
define i1 @oneuse0(i8 %x) {
; CHECK-LABEL: @oneuse0(
; CHECK-NEXT: [[TMP0:%.*]] = and i8 [[X:%.*]], 3
; CHECK-NEXT: call void @use8(i8 [[TMP0]])
; CHECK-NEXT: [[TMP1:%.*]] = icmp slt i8 [[X]], 4
; CHECK-NEXT: ret i1 [[TMP1]]
;
%tmp0 = and i8 %x, 3
call void @use8(i8 %tmp0)
%ret = icmp sge i8 %tmp0, %x
ret i1 %ret
}
$ cat /tmp/test.ll.alive.opt
Name: oneuse0
; CHECK-LABEL: @oneuse0(
; CHECK-NEXT: [[TMP0:%.*]] = and i8 [[X:%.*]], 3
; CHECK-NEXT: call void @use8(i8 [[TMP0]])
; CHECK-NEXT: [[TMP1:%.*]] = icmp slt i8 [[X]], 4
; CHECK-NEXT: ret i1 [[TMP1]]
;
%tmp0 = and i8 %x, 3
call void @use8(i8 %tmp0)
%ret = icmp sge i8 %tmp0, %x
ret i1 %ret
=>
%tmp0 = and i8 %x, 3
call void @use8(i8 %tmp0)
%1 = icmp slt i8 %x, 4
ret i1 %1
util/compiler.cpp:50:26: runtime error: passing zero to clz(), which is not a valid argument
Name: zz
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, i8 %ARG
%Y = extractvalue %X, 0
%Z = extractvalue %X, 1
=>
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, i8 %ARG
%Y = udiv i8 %b, 0
%Z = 0
~$ ./src/alive2/build-Clang-release/alive /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
----------------------------------------
Name: zz
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, %ARG
%Y = extractvalue {i8, i1} %X, 0
%Z = extractvalue {i8, i1} %X, 1
=>
%undef0 = udiv i8 %a, 0
%X = uadd_overflow i8 %undef0, %ARG
%Y = udiv i8 %b, 0
%Z = 0
../util/compiler.cpp:50:26: runtime error: passing zero to clz(), which is not a valid argument
#0 0x6bb794 in util::num_leading_zeros(unsigned long) /home/lebedevri/src/alive2/build-Clang-release/../util/compiler.cpp:50:10
#1 0x647c8b in smt::expr::min_leading_zeros() const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:335:12
#2 0x64e482 in smt::expr::add_no_uoverflow(smt::expr const&) const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:515:7
#3 0x533091 in IR::BinOp::toSMT(IR::State&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/instr.cpp:254:26
#4 0x5bdf3e in IR::State::exec(IR::Value const&) /home/lebedevri/src/alive2/build-Clang-release/../ir/state.cpp:23:16
#5 0x6c4d9a in util::sym_exec(IR::State&) /home/lebedevri/src/alive2/build-Clang-release/../util/symexec.cpp:33:20
#6 0x68482e in tools::TransformVerify::verify() const /home/lebedevri/src/alive2/build-Clang-release/../tools/transform.cpp:246:5
#7 0x445ab5 in main /home/lebedevri/src/alive2/build-Clang-release/../tools/alive.cpp:118:30
#8 0x7fafffc5c09a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409a)
#9 0x39a029 in _start (/home/lebedevri/src/alive2/build-Clang-release/alive+0x39a029)
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior ../util/compiler.cpp:50:26 in
../util/compiler.cpp:50: runtime error: passing zero to clz(), which is not a valid argument
#0 0x6bb794 in util::num_leading_zeros(unsigned long) /home/lebedevri/src/alive2/build-Clang-release/../util/compiler.cpp:50:10
#1 0x647c8b in smt::expr::min_leading_zeros() const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:335:12
#2 0x64e482 in smt::expr::add_no_uoverflow(smt::expr const&) const /home/lebedevri/src/alive2/build-Clang-release/../smt/expr.cpp:515:7
#3 0x533091 in IR::BinOp::toSMT(IR::State&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/instr.cpp:254:26
#4 0x5bdf3e in IR::State::exec(IR::Value const&) /home/lebedevri/src/alive2/build-Clang-release/../ir/state.cpp:23:16
#5 0x6c4d9a in util::sym_exec(IR::State&) /home/lebedevri/src/alive2/build-Clang-release/../util/symexec.cpp:33:20
#6 0x68483f in tools::TransformVerify::verify() const /home/lebedevri/src/alive2/build-Clang-release/../tools/transform.cpp:247:5
#7 0x445ab5 in main /home/lebedevri/src/alive2/build-Clang-release/../tools/alive.cpp:118:30
#8 0x7fafffc5c09a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409a)
#9 0x39a029 in _start (/home/lebedevri/src/alive2/build-Clang-release/alive+0x39a029)
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior ../util/compiler.cpp:50 in
ERROR: Target is more poisonous than source for i8 %Y
Example:
i8 %a = undef
i8 %ARG = undef
i8 %undef0 = #x00 (0)
{i8, i1} %X = ?
Source value: ?
Target value: poison
sanitizer errors
I get this puzzling error when running an alive2 build using -fsanitize=address,undefined
$ ./alive ../tests/unit/add-error.opt
==6828==ERROR: AddressSanitizer failed to allocate 0xdfff0001000 (15392894357504) bytes at address 2008fff7000 (errno: 12)
==6828==ReserveShadowMemoryRange failed while trying to map 0xdfff0001000 bytes. Perhaps you're using ulimit -v
Aborted
$
Alignment check when bytes is zero
When bytes is zero, any pointer is dereferenceable in this implementations.
However, alignment must be checked if bytes is zero in LLVM Language Reference.
If “len” is 0, the pointers may be NULL or dangling. However, they must still be appropriately aligned.
Because giving alignment for memcpy and memset instructions is not implemented, I can't check it.
Though, in my opinion, we have to modify the code.
extractvalue printing/lexing issues
Given
Name: res is undef
%X = umul_overflow i8 %a, undef
%Op = extractvalue %X, 0
%Ov = extractvalue %X, 1
=>
%X = umul_overflow i8 %a, undef
%Op = undef
%Ov = 0
it is printed as:
$ ~/src/alive2/build-Clang-release/alive -smt-to:100000 /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
----------------------------------------
Name: res is undef
%X = umul_overflow i8 %a, undef
%Op = extractvalue {i8, i1} %X, 0
%Ov = extractvalue {i8, i1} %X, 1
=>
%X = umul_overflow i8 %a, undef
%Op = undef
%Ov = 0
<...>
But if you copy %Op = extractvalue {i8, i1} %X, 0 back into the test.opt
$ ~/src/alive2/build-Clang-release/alive -smt-to:100000 /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
Parse error in line: 3: [Lex] couldn't parse: '{i8, i1} %X, 0
'
So i think it should either not print {i8, i1}, or not fail to lex it.
function calls can't be dropped (unless readonly)
Johns-MacBook-Pro:build johnregehr$ cat foo1.ll
declare i32 @getc(%struct.__sFILE* nocapture) local_unnamed_addr #1
%struct.__sFILE = type { i8*, i32, i32, i16, i16, %struct.__sbuf, i32, i8*, i32 (i8*)*, i32 (i8*, i8*, i32)*, i64 (i8*, i64, i32)*, i32 (i8*, i8*, i32)*, %struct.__sbuf, %struct.__sFILEX*, i32, [3 x i8], [1 x i8], %struct.__sbuf, i32, i64 }
%struct.__sFILEX = type opaque
%struct.__sbuf = type { i8*, i32 }
define i32 @foo(%struct.__sFILE* nocapture) {
%2 = tail call i32 @getc(%struct.__sFILE* %0)
ret i32 3
}
Johns-MacBook-Pro:build johnregehr$ cat foo2.ll
declare i32 @getc(%struct.__sFILE* nocapture) local_unnamed_addr #1
%struct.__sFILE = type { i8*, i32, i32, i16, i16, %struct.__sbuf, i32, i8*, i32 (i8*)*, i32 (i8*, i8*, i32)*, i64 (i8*, i64, i32)*, i32 (i8*, i8*, i32)*, %struct.__sbuf, %struct.__sFILEX*, i32, [3 x i8], [1 x i8], %struct.__sbuf, i32, i64 }
%struct.__sFILEX = type opaque
%struct.__sbuf = type { i8*, i32 }
define i32 @foo(%struct.__sFILE* nocapture) {
ret i32 3
}
Johns-MacBook-Pro:build johnregehr$ ./alive-tv foo1.ll foo2.ll
----------------------------------------
define i32 @foo(* %0) {
%1:
%2 = call i32 @getc(* %0)
ret i32 3
}
=>
define i32 @foo(* %0) {
%1:
ret i32 3
}
Transformation seems to be correct!
saturating math undef handling
(retranslating from https://reviews.llvm.org/D63060#1535589 / #63)
...
We are correct that saturating subtraction from undef is undef?
$ ./alive /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
----------------------------------------
Name: form usub_sat
%sub = sub i8 %x, %y
%cmp = icmp uge i8 %x, %y
%res = select i1 %cmp, i8 %sub, i8 0
=>
%sub = sub i8 %x, %y
%cmp = icmp uge i8 %x, %y
%res = usub_sat i8 %x, %y
Done: 1
Optimization is correct!
----------------------------------------
Name: unfold usub_sat
%res = usub_sat i8 %x, %y
=>
%sub = sub i8 %x, %y
%cmp = icmp uge i8 %x, %y
%res = select i1 %cmp, i8 %sub, i8 0
ERROR: Value mismatch for i8 %res
Example:
i8 %x = undef
i8 %y = #x91 (145, -111)
i8 %sub = undef
i1 %cmp = undef
Source value: undef
Target value: #x83 (131, -125)
Interaction between precondition and undef inputs
Logging here since I don't have time today to look into this:
There's an interaction of preconditions taking input registers which can be undef. See example below.
Alive1 didn't have this problem because inputs were never undef.
Pre: WillNotOverflowSignedAdd(%x, %y)
%r = add i4 %x, %y
=>
%r = add nsw %x, %y
ERROR: Target is more poisonous than source for i4 %r
Example:
i4 %x = undef
i4 %y = undef
Source value: undef
Target value: poison
With -disable-undef-input it goes through:
----------------------------------------
Pre: WillNotOverflowSignedAdd(%x, %y)
%r = add i4 %x, %y
=>
%r = add nsw %x, %y
Done: 1
Optimization is correct!
Handle more metadata
- Function arguments / formals
- Call arguments
free(null) should be no-op
free(null) should be no-op, but this is not implemented because there is no notion of null pointer in alive2 yet.
crash when checking buggy transformation with wide integers
regehr@john-home:~/alive2/build$ ./alive -root-only foo.opt
Processing foo.opt..
----------------------------------------
%nx = add i65 %x, -1
%r = add i65 %nx, 3
ret i65 %r
=>
%r = i65 %x
ret i65 %r
alive: ../tools/transform.cpp:41: void print_varval(std::ostream&, const smt::Model&, const IR::Value*, const IR::StateValue&): Assertion `e.isUInt(n)' failed.
Aborted
regehr@john-home:~/alive2/build$
Can disable_undef_input (and similar) be made a property of TransformVerify?
I have to mix several verify calls where disable_undef_input is true for speed, and a last one where it is false to make sure the transformation generated by Souper is sound.
Changing global state for this seems like a bad idea.
Should I submit a PR that makes this an option when constructing a TransformVerify object?
(Maybe a TransformVerifyOpts struct?)
Improve printing of counterexamples with struct typed vars
%a = sadd_overflow i8 1, 1
%b = extractvalue %a, 1
=>
%a = sadd_overflow i8 1, 1
%b = 1
ERROR: Value mismatch for i1 %b
Example:
{i8, i1} %a = #x004 (4)
Source value: #x0 (00)
Target value: #x1 (0)
Should create hidden return instructions for -root-only
When there's no return statement at all, e.g.:
%a = add %x, %y
=>
%a = 0
Function argument and newly allocated block should not alias
TV report file name problem
after a TV run with logging to file enabled, we end up with lots of files called something like
<stdin>_2776131420.txt
not sure yet what's the best solution.
Add support for C++'s new operators
It is not clear whether
p = malloc()
delete p
and
p = new X()
free(p)
is okay in LLVM IR. This should be clarified.
Missing instruction copying to target in Alive parser
e.g.
%a = add %x, %y
%r = mul %a, 2
=>
%r = shl %a, 1
Diagnose new input in target
Should error out when new inputs are introduced in target.
uadd_overflow with undef
From https://reviews.llvm.org/D63065#1545052:
$ ./src/alive2/build-Clang-release/alive -root-only /tmp/test.opt
OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
Processing /tmp/test.opt..
----------------------------------------
Name: uadd_overflow
%X = uadd_overflow i8 %a, undef
%Op = extractvalue {i8, i1} %X, 0
%Ov = extractvalue {i8, i1} %X, 1
%OpIsZero = icmp eq %Op, 0
%NoOverflow = icmp eq %Ov, 0
%Zero = and i1 %OpIsZero, %NoOverflow
ret i1 %Zero
=>
ret i1 1
Done: 1
Optimization is correct!
I don't understand why this optimization is correct. If %a is 1, then I don't see any choice of undef for which both the result is 0 and there is no overflow.
Root checking doesn't handle possible multiple users
Alive2 accepts the following, but shouldn't since there might be multiple users:
%x = freeze i4 undef
=>
%x = undef
Alive misses BB domain on jump if target BB has been seen before
I'm investigating this TV failure from Transforms/CorrelatedValuePropagation/range.ll
alive seems to be telling us that the original function returns 0 when %c==8, but I don't think this makes sense. rather, %cmp == 0, causing us to go return 1.
declare i1 @test6(i32 %c) {
%0:
%cmp = icmp ule i32 %c, 7
br i1 %cmp, label %if.then, label %if.end
%if.then:
switch i32 %c, label %if.end [
i32 6, label %sw.bb
i32 8, label %sw.bb
]
%if.end:
ret i1 1
%sw.bb:
%cmp2 = icmp eq i32 %c, 6
ret i1 %cmp2
}
=>
declare i1 @test6(i32 %c) {
%0:
%cmp = icmp ule i32 %c, 7
br i1 %cmp, label %if.then, label %if.end
%if.then:
%cond = icmp eq i32 %c, 6
br i1 %cond, label %sw.bb, label %if.end
%if.end:
ret i1 1
%sw.bb:
ret i1 1
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
i32 %c = 0x8 (8)
Source:
i1 %cmp = 0x0 (0)
i1 %cmp2 = 0x0 (0)
Target:
i1 %cmp = 0x0 (0)
i1 %cond = 0x0 (0)
Source value: 0x0 (0)
Target value: 0x1 (1, -1)
LLVM ERROR: Alive2: Transform doesn't verify; aborting!
Does select based on undef result in undef?
Come up in https://reviews.llvm.org/D63060
----------------------------------------
%sat = usub_sat i8 %a, %b
%res = add i8 %sat, %b
=>
%sat = usub_sat i8 %a, %b
%t0 = icmp ult i8 %a, %b
%res = select i1 %t0, i8 %b, i8 %a
ERROR: Value mismatch for i8 %res
Example:
i8 %a = undef
i8 %b = #x10 (16)
i8 %sat = undef
i1 %t0 = undef
Source value: undef
Target value: #x02 (2)
So we're selecting based on %t0, which is undef.
The result should be undef, too, right?
CC @nikic.
Add lit test support for opt plugin & alive-tv
Required for e.g. #88 because the parser doesn't have support for load/store, etc yet.
missing pred in icmp should fail to parse
----------------------------------------
Name: zz
%r = icmp i4 %o1, %y
=>
%r = icmp eq i4 %o1, %y
Done: 1
Optimization is correct!
----------------------------------------
Name: z2
%r = icmp i4 %o1, %y
=>
%r = icmp ne i4 %o1, %y
Done: 1
Optimization is correct!
errors from UBsan
UBSan catches a problem triggered by a few Alive2 test cases
$ ./alive ../tests/unit/add-error.opt
Processing ../tests/unit/add-error.opt..
----------------------------------------
%x = shl i16 %i, 1
=>
%x = add %i, %i
/home/regehr/alive2/ir/function.h:64:44: runtime error: reference binding to null pointer of type 'const IR::Type'
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior /home/regehr/alive2/ir/function.h:64:44 in
AddressSanitizer:DEADLYSIGNAL
=================================================================
==7748==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x0000005ac20f bp 0x7fffb4762250 sp 0x7fffb4761e40 T0)
==7748==The signal is caused by a READ memory access.
==7748==Hint: address points to the zero page.
#0 0x5ac20e (/home/regehr/alive2/build/alive+0x5ac20e)
#1 0x501725 (/home/regehr/alive2/build/alive+0x501725)
#2 0x7fd93e05ab96 (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
#3 0x425f69 (/home/regehr/alive2/build/alive+0x425f69)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/home/regehr/alive2/build/alive+0x5ac20e)
==7748==ABORTING
something weird with poison and range metadata
here's a test that's just making sure that instcombine adds the appropriate range metadata for a ctpop call. alive is saying that source is more defined than target, but then %res ends up being poison both before and after, so I'm not sure what's going on but at the very least the printed output is confusing to read.
anyhow (regardless of the actual problem with this test case) it does seem like inserting fake icmp/and instructions may lead to UB problems and that we may need a separate flavor of instruction here that simply adds constraints without UB-related entanglements.
declare i1 @test4(i8 %arg) {
%0:
%cnt = ctpop i8 %arg
%res = icmp eq i8 %cnt, 2
ret i1 %res
}
=>
declare i1 @test4(i8 %arg) {
%0:
%cnt = ctpop i8 %arg
$range_l$0%cnt = icmp sge i8 %cnt, 0
$range_h$0%cnt = icmp slt i8 %cnt, 9
$range$0%cnt = and i1 $range_l$0%cnt, $range_h$0%cnt
assume i1 $range$0%cnt
%res = icmp eq i8 %cnt, 2
ret i1 %res
}
Transformation doesn't verify!
ERROR: Source is more defined than target
Example:
i8 %arg = poison
Source:
i8 %cnt = poison
i1 %res = poison
Target:
i8 %cnt = poison
LLVM ERROR: Alive2: Transform doesn't verify; aborting!
FileCheck error: '-' is empty.
FileCheck command line: /home/regehr/llvm/build/bin/FileCheck /home/regehr/llvm/test/Transforms/InstCombine/ctpop.ll
Check timeouts
I seem to be very successful in making alive2 do not what it is supposed to just by manually coming up with tests :/
Name: zz
%X = uadd_overflow i8 undef, i8 %ARG
%Y = extractvalue %X, 0
%Z = extractvalue %X, 1
=>
%X = uadd_overflow i8 undef, i8 %ARG
%Y = 0
%Z = 0
ERROR: Timeout
enhancement: TV dashboard
Nuno and I discussed this briefly; I'd like to use this space to iron out a few details and then I'll start working on code.
The goal is to make it easy for people to see the results of a translation validation run, whether it is over the LLVM test suite or some other collection of LLVM IR.
There are maybe three steps:
-
Run Alive2 TV on some test cases using a special command line option that causes it to emit extra details about its run. This could go to its stderr stream or it could write a bunch of special files, I'm not sure which makes more sense.
-
Run a not-yet-implemented script which has two outputs. First, a web page showing the results of the TV run, with links to test cases, details, etc. Second, a CSV file (or similar) describing the outcome of each test case. I don't think it's worth interacting with a database or anything heavyweight here.
-
Optionally, run another not-yet-implemented script that diffs two (or more?)
TV runs using the CSV summary files. This script emits a web page that describes all of the test cases that had a different outcome across the input runs.
If I'm the only one working on this I'd prefer to work in Perl, which I find much easier and more concise than Python. But if that seems like a bad idea I can muddle along in Python. Let me know what you think about all this.
UB not tracked data-flow-wise
$ ./third_party/alive2/build/alive /tmp/test.opt
Processing /tmp/test.opt..
----------------------------------------
Name: undef
%r = udiv i8 %x, 0
=>
%r = i8 undef
ERROR: Value mismatch for i8 %r
Example:
i8 %x = undef
Source value: #x00 (0)
Target value: #xff (255, -1)
Experiment Z3's ackermannization with arrays
As of today, Z3's akermannization supports arrays (Z3Prover/z3@000e485). Let's test the performance of that. It should now remove all UFs, though lambdas and quantifiers are still left, so no fast SAT yet.
support FP intrinsics
another one for @zhengyangl: support sin, cos, sqrt, powi, and all of the rest of these as alive instructions
IR::Phi::toSMT()-related crashes in TV
alive2 master + llvm master
$ ./bin/llvm-lit -s -Dopt="/tmp/opt-alive.sh" ../llvm/test/Transforms/InstSimplify/phi.ll -v -v -vv
FAIL: LLVM :: Transforms/InstSimplify/phi.ll (1 of 1)
******************** TEST 'LLVM :: Transforms/InstSimplify/phi.ll' FAILED ********************
Script:
--
: 'RUN: at line 2'; /tmp/opt-alive.sh < /build/llvm/test/Transforms/InstSimplify/phi.ll -instsimplify -S | /build/llvm-build-Clang-release/bin/FileCheck /build/llvm/test/Transforms/InstSimplify/phi.ll
--
Exit Code: 2
Command Output (stderr):
--
+ : 'RUN: at line 2'
+ /tmp/opt-alive.sh -instsimplify -S
+ /build/llvm-build-Clang-release/bin/FileCheck /build/llvm/test/Transforms/InstSimplify/phi.ll
----------------------------------------
define i1 @test1(i32 %x) {
%0:
br i1 1, label %a, label %b
%a:
%aa = or i32 %x, 10
br label %c
%b:
%bb = or i32 %x, 10
br label %c
%c:
%cc = phi i32 [ %bb, %b ], [ %aa, %a ]
%d = urem i32 %cc, 2
%e = icmp eq i32 %d, 0
ret i1 %e
}
=>
define i1 @test1(i32 %x) {
%0:
br i1 1, label %a, label %b
%a:
%aa = or i32 %x, 10
br label %c
%b:
%bb = or i32 %x, 10
br label %c
%c:
%cc = phi i32 [ %bb, %b ], [ %aa, %a ]
%d = urem i32 %cc, 2
%e = icmp eq i32 %d, 0
ret i1 %e
}
terminate called after throwing an instance of 'std::out_of_range'
what(): _Map_base::at
Stack dump:
0. Program arguments: /build/llvm-build-Clang-release/bin/opt -load=/home/lebedevri/src/alive2/build-Clang-release/tv/tv.so -tv -instsimplify -S -tv
1. Running pass 'Function Pass Manager' on module '<stdin>'.
2. Running pass 'Translation Validator' on function '@test1'
#0 0x00000000026869b9 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /build/llvm/lib/Support/Unix/Signals.inc:494:13
#1 0x00000000026869b9 PrintStackTraceSignalHandler(void*) /build/llvm/lib/Support/Unix/Signals.inc:557:0
#2 0x00000000026842a8 llvm::sys::RunSignalHandlers() /build/llvm/lib/Support/Signals.cpp:69:18
#3 0x0000000002686cf6 SignalHandler(int) /build/llvm/lib/Support/Unix/Signals.inc:357:1
#4 0x00007f9021bd26e0 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x126e0)
#5 0x00007f90214978bb gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x378bb)
#6 0x00007f9021482535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
#7 0x00007f90216d4983 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8c983)
#8 0x00007f90216da8e6 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x928e6)
#9 0x00007f90216da921 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x92921)
#10 0x00007f90216dab54 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x92b54)
#11 0x00007f90216d686b (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8e86b)
#12 0x00007f902141bf09 std::__detail::_Map_base<IR::Value const*, std::pair<IR::Value const* const, unsigned int>, std::allocator<std::pair<IR::Value const* const, unsigned int> >, std::__detail::_Select1st, std::equal_to<IR::Value const*>, std::hash<IR::Value const*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true>, true>::at(IR::Value const* const&) /usr/lib64/gcc/x86_64-linux-gnu/8/../../../../include/c++/8/bits/hashtable_policy.h:761:14
#13 0x00007f9021413208 std::unordered_map<IR::Value const*, unsigned int, std::hash<IR::Value const*>, std::equal_to<IR::Value const*>, std::allocator<std::pair<IR::Value const* const, unsigned int> > >::at(IR::Value const* const&) /usr/lib64/gcc/x86_64-linux-gnu/8/../../../../include/c++/8/bits/unordered_map.h:991:9
#14 0x00007f90214117ba IR::State::operator[](IR::Value const&) /home/lebedevri/src/alive2/build-Clang-release/../ir/state.cpp:43:32
#15 0x00007f902140e473 IR::Phi::toSMT(IR::State&) const /home/lebedevri/src/alive2/build-Clang-release/../ir/instr.cpp:553:14
#16 0x00007f9021411539 IR::State::exec(IR::Value const&) /home/lebedevri/src/alive2/build-Clang-release/../ir/state.cpp:30:16
#17 0x00007f902143ccdd util::sym_exec(IR::State&) /home/lebedevri/src/alive2/build-Clang-release/../util/symexec.cpp:33:20
#18 0x00007f9021430648 tools::TransformVerify::verify() const /home/lebedevri/src/alive2/build-Clang-release/../tools/transform.cpp:223:5
#19 0x00007f90213d3828 (anonymous namespace)::TVPass::runOnFunction(llvm::Function&) /home/lebedevri/src/alive2/build-Clang-release/../tv/tv.cpp:513:32
#20 0x0000000001fbd2e7 llvm::FPPassManager::runOnFunction(llvm::Function&) /build/llvm/lib/IR/LegacyPassManager.cpp:1643:27
#21 0x0000000001fbd663 llvm::FPPassManager::runOnModule(llvm::Module&) /build/llvm/lib/IR/LegacyPassManager.cpp:1678:13
#22 0x0000000001fbdca1 (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /build/llvm/lib/IR/LegacyPassManager.cpp:0:0
#23 0x0000000001fbdca1 llvm::legacy::PassManagerImpl::run(llvm::Module&) /build/llvm/lib/IR/LegacyPassManager.cpp:1856:0
#24 0x00000000013b77dc main /build/llvm/tools/opt/opt.cpp:862:12
#25 0x00007f902148409b __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409b)
#26 0x000000000139702a _start (/build/llvm-build-Clang-release/bin/opt+0x139702a)
/tmp/opt-alive.sh: line 3: 31045 Aborted timeout 60 /build/llvm-build-Clang-release/bin/opt -load=/home/lebedevri/src/alive2/build-Clang-release/tv/tv.so -tv $@ -tv
FileCheck error: '-' is empty.
FileCheck command line: /build/llvm-build-Clang-release/bin/FileCheck /build/llvm/test/Transforms/InstSimplify/phi.ll
--
********************
Testing Time: 0.22s
********************
Failing Tests (1):
LLVM :: Transforms/InstSimplify/phi.ll
Unexpected Failures: 1
CI Broken
counterexample printing broken with undefs triggering poison
define i32 @f_var2(i32 %arg, i32 %arg1) {
%tmp = and i32 %arg, 1
%tmp2 = icmp eq i32 %tmp, 0
%tmp3 = lshr i32 %arg, %arg1
%tmp4 = and i32 %tmp3, 1
%tmp5 = select i1 %tmp2, i32 %tmp4, i32 1
ret i32 %tmp5
}
=>
define i32 @f_var2(i32 %arg, i32 %arg1) {
%1 = shl i32 1, %arg1
%2 = or i32 %1, 1
%3 = and i32 %2, %arg
%4 = icmp ne i32 %3, 0
%tmp5 = zext i1 %4 to i32
ret i32 %tmp5
}
Transformation doesn't verify!
ERROR: Target is more poisonous than source
Example:
i32 %arg = #x00000001 (1, -4294967295)
i32 %arg1 = undef
Target:
i32 %1 = #x00000001 (1, -4294967295) <-- should be poison
i32 %2 = #x00000001 (1, -4294967295)
i32 %3 = #x00000001 (1, -4294967295)
i1 %4 = #x1 (0)
i32 %tmp5 = #x00000001 (1, -4294967295)
Source value: #x00000001 (1, -4294967295)
Target value: poison
crashes in tv
regehr@john-home:~/alive2/build$ ~/llvm/build/bin/llvm-lit -vv -Dopt="$HOME/alive2/build/opt-alive.sh" $HOME/llvm/test/Transforms/AggressiveInstCombine/rotate.ll
-- Testing: 1 tests, single process --
FAIL: LLVM :: Transforms/AggressiveInstCombine/rotate.ll (1 of 1)
******************** TEST 'LLVM :: Transforms/AggressiveInstCombine/rotate.ll' FAILED ********************
Script:
--
: 'RUN: at line 2'; /home/regehr/alive2/build/opt-alive.sh < /home/regehr/llvm/test/Transforms/AggressiveInstCombine/rotate.ll -aggressive-instcombine -S | /home/regehr/llvm/build/bin/FileCheck /home/regehr/llvm/test/Transforms/AggressiveInstCombine/rotate.ll
--
Exit Code: 2
Command Output (stderr):
--
+ : 'RUN: at line 2'
+ /home/regehr/alive2/build/opt-alive.sh -aggressive-instcombine -S
+ /home/regehr/llvm/build/bin/FileCheck /home/regehr/llvm/test/Transforms/AggressiveInstCombine/rotate.ll
Unsupported instruction: %0 = call i32 @llvm.fshl.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshl.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshl.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshl.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshr.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshr.i32(i32 %a, i32 %a, i32 %b)
Unsupported instruction: %0 = call i32 @llvm.fshr.i32(i32 %a, i32 %a, i32 %b)
----------------------------------------
define i12 @could_be_rotr_weird_type(i12 %a, i12 %b) {
%entry:
%cmp = icmp eq i12 %b, 0
br i1 %cmp, label %end, label %rotbb
%end:
%cond = phi i12 [ %a, %entry ], [ %or, %rotbb ]
ret i12 %cond
%rotbb:
%sub = sub i12 12, %b
%shl = shl i12 %a, %sub
%shr = lshr i12 %a, %b
%or = or i12 %shl, %shr
br label %end
}
=>
define i12 @could_be_rotr_weird_type(i12 %a, i12 %b) {
%entry:
%cmp = icmp eq i12 %b, 0
br i1 %cmp, label %end, label %rotbb
%end:
%cond = phi i12 [ %a, %entry ], [ %or, %rotbb ]
ret i12 %cond
%rotbb:
%sub = sub i12 12, %b
%shl = shl i12 %a, %sub
%shr = lshr i12 %a, %b
%or = or i12 %shl, %shr
br label %end
}
terminate called after throwing an instance of 'std::out_of_range'
what(): _Map_base::at
Stack dump:
0. Program arguments: /home/regehr/llvm/build/bin/opt -load=/home/regehr/alive2/build/tv/tv.so -tv -aggressive-instcombine -S -tv
1. Running pass 'Function Pass Manager' on module '<stdin>'.
2. Running pass 'Translation Validator' on function '@could_be_rotr_weird_type'
#0 0x0000000003c16e29 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:494:11
#1 0x0000000003c16fd9 PrintStackTraceSignalHandler(void*) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:558:1
#2 0x0000000003c15266 llvm::sys::RunSignalHandlers() /home/regehr/llvm/build/../lib/Support/Signals.cpp:67:5
#3 0x0000000003c176eb SignalHandler(int) /home/regehr/llvm/build/../lib/Support/Unix/Signals.inc:357:1
#4 0x00007f0919362890 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12890)
#5 0x00007f0917e0be97 gsignal /build/glibc-OTsEL5/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
#6 0x00007f0917e0d801 abort /build/glibc-OTsEL5/glibc-2.27/stdlib/abort.c:81:0
#7 0x00007f09184628b7 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8c8b7)
#8 0x00007f0918468a06 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x92a06)
#9 0x00007f0918468a41 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x92a41)
#10 0x00007f0918468c74 (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x92c74)
#11 0x00007f091846478f (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x8e78f)
#12 0x00007f091973fee9 (/home/regehr/alive2/build/tv/tv.so+0x3eee9)
#13 0x00007f091973df38 IR::State::operator[](IR::Value const&) /home/regehr/alive2/build/../ir/state.cpp:43:0
#14 0x00007f091973a914 IR::Phi::toSMT(IR::State&) const /home/regehr/alive2/build/../ir/instr.cpp:509:0
#15 0x00007f091973f19a IR::State::exec(IR::Value const&) /home/regehr/alive2/build/../ir/state.cpp:31:0
#16 0x00007f0919750b53 util::sym_exec(IR::State&) /home/regehr/alive2/build/../util/symexec.cpp:33:0
#17 0x00007f091974e7ca tools::TransformVerify::verify() const /home/regehr/alive2/build/../tools/transform.cpp:224:0
#18 0x00007f091973152f (anonymous namespace)::TVPass::runOnFunction(llvm::Function&) /home/regehr/alive2/build/../tv/tv.cpp:489:0
#19 0x00000000031e1908 llvm::FPPassManager::runOnFunction(llvm::Function&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1643:27
#20 0x00000000031e1d95 llvm::FPPassManager::runOnModule(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1678:16
#21 0x00000000031e254d (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1743:27
#22 0x00000000031e2025 llvm::legacy::PassManagerImpl::run(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1856:16
#23 0x00000000031e2c21 llvm::legacy::PassManager::run(llvm::Module&) /home/regehr/llvm/build/../lib/IR/LegacyPassManager.cpp:1887:3
#24 0x0000000000da132a main /home/regehr/llvm/build/../tools/opt/opt.cpp:862:12
#25 0x00007f0917deeb97 __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:344:0
#26 0x0000000000d5596a _start (/home/regehr/llvm/build/bin/opt+0xd5596a)
/home/regehr/alive2/build/opt-alive.sh: line 2: 11223 Aborted timeout 60 $HOME/llvm/build/bin/opt -load=$HOME/alive2/build/tv/tv.so -tv $@ -tv
FileCheck error: '-' is empty.
FileCheck command line: /home/regehr/llvm/build/bin/FileCheck /home/regehr/llvm/test/Transforms/AggressiveInstCombine/rotate.ll
--
********************
Testing Time: 3.42s
********************
Failing Tests (1):
LLVM :: Transforms/AggressiveInstCombine/rotate.ll
Unexpected Failures: 1
regehr@john-home:~/alive2/build$
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.