Closed regehr closed 5 months ago
it says "ERROR: Target's return value is more undefined" but then the CEX shows src and tgt returning the same thing
regehr@ohm:~/test/results/179$ cat src.ll ; ModuleID = 'M2' source_filename = "M2" target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128" target triple = "aarch64-linux-gnu" define <8 x i16> @f(<8 x i16> %0, <8 x i16> %1) { %3 = zext <8 x i16> %0 to <8 x i33> %4 = zext <8 x i16> %1 to <8 x i33> %5 = mul <8 x i33> %3, %4 %6 = lshr <8 x i33> %5, <i33 16, i33 16, i33 16, i33 16, i33 16, i33 16, i33 16, i33 16> %7 = trunc <8 x i33> %6 to <8 x i16> ret <8 x i16> %7 } regehr@ohm:~/test/results/179$ cat tgt.ll ; ModuleID = 'M2' source_filename = "M2" target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128" target triple = "aarch64-linux-gnu" @.LCPI0_0 = local_unnamed_addr constant [16 x i8] c"\00\01\04\05\10\11\14\15 !$%0145", align 16 declare void @llvm.assert(i1) define <8 x i16> @f(<8 x i16> %0, <8 x i16> %1) local_unnamed_addr { arm_tv_entry: %bc = bitcast <8 x i16> %0 to <2 x i64> %a6_1 = extractelement <2 x i64> %bc, i64 0 %a6_7 = bitcast i64 %a6_1 to <4 x i16> %a6_9 = zext <4 x i16> %a6_7 to <4 x i32> %a6_12 = bitcast <4 x i32> %a6_9 to i128 %bc26 = bitcast <8 x i16> %1 to <2 x i64> %a7_1 = extractelement <2 x i64> %bc26, i64 0 %a7_7 = bitcast i64 %a7_1 to <4 x i16> %a7_9 = zext <4 x i16> %a7_7 to <4 x i32> %a7_12 = bitcast <4 x i32> %a7_9 to i128 %a10_2 = lshr i128 %a6_12, 64 %a10_3 = lshr i128 %a7_12, 64 %a10_4 = bitcast i128 %a10_2 to <4 x i32> %a10_5 = bitcast i128 %a10_3 to <4 x i32> %a10_6 = zext <4 x i32> %a10_4 to <4 x i64> %a10_7 = zext <4 x i32> %a10_5 to <4 x i64> %a10_8 = mul nuw <4 x i64> %a10_7, %a10_6 %bc27 = bitcast <4 x i64> %a10_8 to <2 x i128> %a10_10 = extractelement <2 x i128> %bc27, i64 0 %2 = mul nuw <4 x i32> %a7_9, %a6_9 %a14_1 = bitcast i128 %a10_10 to <2 x i64> %a14_428 = lshr i128 %a10_10, 16 %a14_5 = trunc i128 %a14_428 to i32 %a14_6 = insertelement <2 x i32> poison, i32 %a14_5, i64 0 %a14_7 = extractelement <2 x i64> %a14_1, i64 1 %a14_9 = lshr i64 %a14_7, 16 %a14_10 = trunc i64 %a14_9 to i32 %a14_11 = insertelement <2 x i32> %a14_6, i32 %a14_10, i64 1 %a14_12 = bitcast <2 x i32> %a14_11 to i64 %a14_13 = zext i64 %a14_12 to i128 %a15_2 = extractelement <4 x i32> %2, i64 0 %a15_4 = lshr i32 %a15_2, 16 %a15_6 = insertelement <2 x i32> poison, i32 %a15_4, i64 0 %a15_7 = extractelement <4 x i32> %2, i64 1 %a15_9 = lshr i32 %a15_7, 16 %a15_11 = insertelement <2 x i32> %a15_6, i32 %a15_9, i64 1 %a15_12 = bitcast <2 x i32> %a15_11 to i64 %a15_13 = zext nneg i64 %a15_12 to i128 %a17_1 = bitcast i128 %a15_13 to <16 x i8> %a17_3 = bitcast i128 %a14_13 to <16 x i8> %a17_12 = trunc i64 %a15_12 to i8 %a17_27 = insertelement <16 x i8> <i8 poison, i8 poison, i8 poison, i8 poison, i8 poison, i8 poison, i8 poison, i8 poison, i8 undef, i8 undef, i8 undef, i8 undef, i8 undef, i8 undef, i8 undef, i8 undef>, i8 %a17_12, i64 0 %a17_30 = extractelement <16 x i8> %a17_1, i64 1 %a17_45 = insertelement <16 x i8> %a17_27, i8 %a17_30, i64 1 %a17_48 = extractelement <16 x i8> %a17_1, i64 4 %a17_63 = insertelement <16 x i8> %a17_45, i8 %a17_48, i64 2 %a17_66 = extractelement <16 x i8> %a17_1, i64 5 %a17_81 = insertelement <16 x i8> %a17_63, i8 %a17_66, i64 3 %a17_87 = trunc i64 %a14_12 to i8 %a17_99 = insertelement <16 x i8> %a17_81, i8 %a17_87, i64 4 %a17_153 = shufflevector <16 x i8> %a17_99, <16 x i8> %a17_3, <16 x i32> <i32 0, i32 1, i32 2, i32 3, i32 4, i32 17, i32 20, i32 21, i32 8, i32 9, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15> tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) tail call void @llvm.assert(i1 true) %a18_23 = bitcast <16 x i8> %a17_153 to <8 x i16> ret <8 x i16> %a18_23 } regehr@ohm:~/test/results/179$ ~/alive2-regehr/build/alive-tv src.ll tgt.ll --disable-poison-input --disable-undef-input ---------------------------------------- define <8 x i16> @f(<8 x i16> %#0, <8 x i16> %#1) { #2: %#3 = zext <8 x i16> %#0 to <8 x i33> %#4 = zext <8 x i16> %#1 to <8 x i33> %#5 = mul <8 x i33> %#3, %#4 %#6 = lshr <8 x i33> %#5, { 16, 16, 16, 16, 16, 16, 16, 16 } %#7 = trunc <8 x i33> %#6 to <8 x i16> ret <8 x i16> %#7 } => define <8 x i16> @f(<8 x i16> %#0, <8 x i16> %#1) { arm_tv_entry: %bc = bitcast <8 x i16> %#0 to <2 x i64> %a6_1 = extractelement <2 x i64> %bc, i64 0 %a6_7 = bitcast i64 %a6_1 to <4 x i16> %a6_9 = zext <4 x i16> %a6_7 to <4 x i32> %a6_12 = bitcast <4 x i32> %a6_9 to i128 %bc26 = bitcast <8 x i16> %#1 to <2 x i64> %a7_1 = extractelement <2 x i64> %bc26, i64 0 %a7_7 = bitcast i64 %a7_1 to <4 x i16> %a7_9 = zext <4 x i16> %a7_7 to <4 x i32> %a7_12 = bitcast <4 x i32> %a7_9 to i128 %a10_2 = lshr i128 %a6_12, 64 %a10_3 = lshr i128 %a7_12, 64 %a10_4 = bitcast i128 %a10_2 to <4 x i32> %a10_5 = bitcast i128 %a10_3 to <4 x i32> %a10_6 = zext <4 x i32> %a10_4 to <4 x i64> %a10_7 = zext <4 x i32> %a10_5 to <4 x i64> %a10_8 = mul nuw <4 x i64> %a10_7, %a10_6 %bc27 = bitcast <4 x i64> %a10_8 to <2 x i128> %a10_10 = extractelement <2 x i128> %bc27, i64 0 %#2 = mul nuw <4 x i32> %a7_9, %a6_9 %a14_1 = bitcast i128 %a10_10 to <2 x i64> %a14_428 = lshr i128 %a10_10, 16 %a14_5 = trunc i128 %a14_428 to i32 %a14_6 = insertelement <2 x i32> poison, i32 %a14_5, i64 0 %a14_7 = extractelement <2 x i64> %a14_1, i64 1 %a14_9 = lshr i64 %a14_7, 16 %a14_10 = trunc i64 %a14_9 to i32 %a14_11 = insertelement <2 x i32> %a14_6, i32 %a14_10, i64 1 %a14_12 = bitcast <2 x i32> %a14_11 to i64 %a14_13 = zext i64 %a14_12 to i128 %a15_2 = extractelement <4 x i32> %#2, i64 0 %a15_4 = lshr i32 %a15_2, 16 %a15_6 = insertelement <2 x i32> poison, i32 %a15_4, i64 0 %a15_7 = extractelement <4 x i32> %#2, i64 1 %a15_9 = lshr i32 %a15_7, 16 %a15_11 = insertelement <2 x i32> %a15_6, i32 %a15_9, i64 1 %a15_12 = bitcast <2 x i32> %a15_11 to i64 %a15_13 = zext nneg i64 %a15_12 to i128 %a17_1 = bitcast i128 %a15_13 to <16 x i8> %a17_3 = bitcast i128 %a14_13 to <16 x i8> %a17_12 = trunc i64 %a15_12 to i8 %a17_27 = insertelement <16 x i8> { poison, poison, poison, poison, poison, poison, poison, poison, undef, undef, undef, undef, undef, undef, undef, undef }, i8 %a17_12, i64 0 %a17_30 = extractelement <16 x i8> %a17_1, i64 1 %a17_45 = insertelement <16 x i8> %a17_27, i8 %a17_30, i64 1 %a17_48 = extractelement <16 x i8> %a17_1, i64 4 %a17_63 = insertelement <16 x i8> %a17_45, i8 %a17_48, i64 2 %a17_66 = extractelement <16 x i8> %a17_1, i64 5 %a17_81 = insertelement <16 x i8> %a17_63, i8 %a17_66, i64 3 %a17_87 = trunc i64 %a14_12 to i8 %a17_99 = insertelement <16 x i8> %a17_81, i8 %a17_87, i64 4 %a17_153 = shufflevector <16 x i8> %a17_99, <16 x i8> %a17_3, 0, 1, 2, 3, 4, 17, 20, 21, 8, 9, 10, 11, 12, 13, 14, 15 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 assume i1 1 %a18_23 = bitcast <16 x i8> %a17_153 to <8 x i16> ret <8 x i16> %a18_23 } Transformation doesn't verify! ERROR: Target's return value is more undefined Example: <8 x i16> %#0 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > <8 x i16> %#1 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > Source: <8 x i33> %#3 = < #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0) > <8 x i33> %#4 = < #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0) > <8 x i33> %#5 = < #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0) > <8 x i33> %#6 = < #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0), #x000000000 (0) > <8 x i16> %#7 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > Target: <2 x i64> %bc = < #x0000000000000000 (0), #x0000000000000000 (0) > i64 %a6_1 = #x0000000000000000 (0) <4 x i16> %a6_7 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > <4 x i32> %a6_9 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) > i128 %a6_12 = #x00000000000000000000000000000000 (0) <2 x i64> %bc26 = < #x0000000000000000 (0), #x0000000000000000 (0) > i64 %a7_1 = #x0000000000000000 (0) <4 x i16> %a7_7 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > <4 x i32> %a7_9 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) > i128 %a7_12 = #x00000000000000000000000000000000 (0) i128 %a10_2 = #x00000000000000000000000000000000 (0) i128 %a10_3 = #x00000000000000000000000000000000 (0) <4 x i32> %a10_4 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) > <4 x i32> %a10_5 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) > <4 x i64> %a10_6 = < #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0) > <4 x i64> %a10_7 = < #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0) > <4 x i64> %a10_8 = < #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0), #x0000000000000000 (0) > <2 x i128> %bc27 = < #x00000000000000000000000000000000 (0), #x00000000000000000000000000000000 (0) > i128 %a10_10 = #x00000000000000000000000000000000 (0) <4 x i32> %#2 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) > <2 x i64> %a14_1 = < #x0000000000000000 (0), #x0000000000000000 (0) > i128 %a14_428 = #x00000000000000000000000000000000 (0) i32 %a14_5 = #x00000000 (0) <2 x i32> %a14_6 = < #x00000000 (0), poison > i64 %a14_7 = #x0000000000000000 (0) i64 %a14_9 = #x0000000000000000 (0) i32 %a14_10 = #x00000000 (0) <2 x i32> %a14_11 = < #x00000000 (0), #x00000000 (0) > i64 %a14_12 = #x0000000000000000 (0) i128 %a14_13 = #x00000000000000000000000000000000 (0) i32 %a15_2 = #x00000000 (0) i32 %a15_4 = #x00000000 (0) <2 x i32> %a15_6 = < #x00000000 (0), poison > i32 %a15_7 = #x00000000 (0) i32 %a15_9 = #x00000000 (0) <2 x i32> %a15_11 = < #x00000000 (0), #x00000000 (0) > i64 %a15_12 = #x0000000000000000 (0) i128 %a15_13 = #x00000000000000000000000000000000 (0) <16 x i8> %a17_1 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > <16 x i8> %a17_3 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > i8 %a17_12 = #x00 (0) <16 x i8> %a17_27 = < #x00 (0), poison, poison, poison, poison, poison, poison, poison, #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > i8 %a17_30 = #x00 (0) <16 x i8> %a17_45 = < #x00 (0), #x00 (0), poison, poison, poison, poison, poison, poison, #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > i8 %a17_48 = #x00 (0) <16 x i8> %a17_63 = < #x00 (0), #x00 (0), #x00 (0), poison, poison, poison, poison, poison, #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > i8 %a17_66 = #x00 (0) <16 x i8> %a17_81 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), poison, poison, poison, poison, #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > i8 %a17_87 = #x00 (0) <16 x i8> %a17_99 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), poison, poison, poison, #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > <16 x i8> %a17_153 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > <8 x i16> %a18_23 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > Source value: < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > Target value: < #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) > Summary: 0 correct transformations 1 incorrect transformations 0 failed-to-prove transformations 0 Alive2 errors regehr@ohm:~/test/results/179$
This is a dup of #129.
nunoplopes
commented
5 months ago nunoplopes
commented
5 months ago
it says "ERROR: Target's return value is more undefined" but then the CEX shows src and tgt returning the same thing