Test Failure: Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll

Test source: git

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i8(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i8 2, i8 10
  %ptr.slide = gep ptr %obj, 1 x i8 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
Transformation seems to be correct! (syntactically equal)

-- 3. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i8(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i8 2, i8 10
  %ptr.slide = gep ptr %obj, 1 x i8 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
=>
define i32 @possible_out_of_bounds_gep_i8(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %res = select i1 %c1, i32 3, i32 0
  ret i32 %res
}
Transformation seems to be correct!

-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i16(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i16 2, i16 10
  %ptr.slide = gep ptr %obj, 1 x i16 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
Transformation seems to be correct! (syntactically equal)

-- 7. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i16(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i16 2, i16 10
  %ptr.slide = gep ptr %obj, 1 x i16 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
=>
define i32 @possible_out_of_bounds_gep_i16(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %res = select i1 %c1, i32 3, i32 0
  ret i32 %res
}
Transformation seems to be correct!

-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i32(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i32 2, i32 10
  %ptr.slide = gep ptr %obj, 1 x i32 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
Transformation seems to be correct! (syntactically equal)

-- 11. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i32(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %offset = select i1 %c0, i32 2, i32 10
  %ptr.slide = gep ptr %obj, 1 x i32 %offset
  %objsize_max = objectsize ptr %ptr.slide, i1 0, i1 1
  %objsize_min = objectsize ptr %ptr.slide, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
=>
define i32 @possible_out_of_bounds_gep_i32(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %res = select i1 %c1, i32 3, i32 0
  ret i32 %res
}
Transformation seems to be correct!

-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i16_sroa(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %.sroa.gep = gep ptr %obj, 1 x i16 2
  %.sroa.gep1 = gep ptr %obj, 1 x i16 10
  %offset.sroa.sel = select i1 %c0, ptr %.sroa.gep, ptr %.sroa.gep1
  %objsize_max = objectsize ptr %offset.sroa.sel, i1 0, i1 1
  %objsize_min = objectsize ptr %offset.sroa.sel, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
Transformation seems to be correct! (syntactically equal)

-- 15. LowerConstantIntrinsicsPass

----------------------------------------
define i32 @possible_out_of_bounds_gep_i16_sroa(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %.sroa.gep = gep ptr %obj, 1 x i16 2
  %.sroa.gep1 = gep ptr %obj, 1 x i16 10
  %offset.sroa.sel = select i1 %c0, ptr %.sroa.gep, ptr %.sroa.gep1
  %objsize_max = objectsize ptr %offset.sroa.sel, i1 0, i1 1
  %objsize_min = objectsize ptr %offset.sroa.sel, i1 1, i1 1
  %res = select i1 %c1, i32 %objsize_max, i32 %objsize_min
  ret i32 %res
}
=>
define i32 @possible_out_of_bounds_gep_i16_sroa(i1 %c0, i1 %c1) {
entry:
  %obj = alloca i64 5, align 1
  %res = select i1 %c1, i32 3, i32 65531
  ret i32 %res
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch

Example:
i1 %c0 = #x1 (1)
i1 %c1 = #x0 (0)

Source:
ptr %obj = pointer(local, block_id=0, offset=0) / Address=#x03
ptr %.sroa.gep = pointer(local, block_id=0, offset=2) / Address=#x05
ptr %.sroa.gep1 = pointer(local, block_id=0, offset=10) / Address=#x0d
ptr %offset.sroa.sel = pointer(local, block_id=0, offset=2) / Address=#x05
i32 %objsize_max = #x00000004 (4)
i32 %objsize_min = #x00000000 (0)
i32 %res = #x00000000 (0)

SOURCE MEMORY STATE
===================
LOCAL BLOCKS:
Block 0 >	size: 5	align: 1	alloc type: 1	alive: true	address: #x03

Target:
ptr %obj = pointer(local, block_id=0, offset=0) / Address=#x04
i32 %res = #x0000fffb (65531)

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 0 >	size: 5	align: 1	alloc type: 1	alive: true	address: #x04
Source value: #x00000000 (0)
Target value: #x0000fffb (65531)

Pass: LowerConstantIntrinsicsPass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-passes=lower-constant-intrinsics' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'

Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_t2LWdKia_fVjf.bc"

------------------- SMT STATS -------------------
Num queries: 45
Num invalid: 0
Num skips:   0
Num trivial: 24 (34.8%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     28 (62.2%)
Num UNSAT:   17 (37.8%)
Alive2: Transform doesn't verify; aborting!

stderr:

Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll' FAILED ********************
Exit Code: 2

Command Output (stdout):
--
# RUN: at line 2
/home/nlopes/alive2/build/opt-alive.sh -passes=lower-constant-intrinsics -S < /bitbucket/nlopes/llvm/llvm/test/Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll
# executed command: /home/nlopes/alive2/build/opt-alive.sh -passes=lower-constant-intrinsics -S
# .---command stderr------------
# `-----------------------------
# error: command failed with exit status: 1
# executed command: /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll
# .---command stderr------------
# | FileCheck error: '<stdin>' is empty.
# | FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LowerConstantIntrinsics/builtin-object-size-idxsize.ll
# `-----------------------------
# error: command failed with exit status: 2

--

<-- Back