In enumerator.cpp, compareFunctions or constantSynthesis will be invoked according to whether the sketch contains any constant:
if (!HaveC) {
AliveEngine AE(TLI);
Good = AE.compareFunctions(*Src, *Tgt);
} else {
AliveEngine AE(TLI);
Good = AE.constantSynthesis(*Src, *Tgt, ConstantResults);
}
However, we find that their tolerance to poison is different.
Considering Example 3 in the paper:
%0 = shufflevector <32 x i8> %x, poison, <3, 7, 11, 15, 19, 23, 27, 31>
%1 = lshr %0, <6, 6, 6, 6, 6, 6, 6, 6>
%2 = zext 8 x i8> %1 to <8 x i32>
ret <8 x i32> %2
=>
%0 = bitcast <32 x i8> %x to <8 x i32>
%1 = call @llvm.x86.avx2.psrli.d(<8 x i32> %0, 30)
ret <8 x i32> %1
Minotaur can successfully generate this rewrite by constantSynthesis:
define <8 x i32> @cut.256.257(<32 x i8> %__n3, i16 %__n4, i32 %_reservedc_99) {
#0:
%__n0 = shufflevector <32 x i8> %__n3, <32 x i8> poison, 3, 7, 11, 15, 19, 23, 27, 31
%__n1 = lshr <8 x i8> %__n0, { 6, 6, 6, 6, 6, 6, 6, 6 }
%__n2 = zext <8 x i8> %__n1 to <8 x i32>
ret <8 x i32> %__n2
}
=>
define <8 x i32> @cut.256(<32 x i8> %__n3, i16 %__n4, i32 %_reservedc_99) {
#0:
%#1 = bitcast <32 x i8> %__n3 to <8 x i32>
%intr = x86_avx2_psrli_d <8 x i32> %#1, i32 %_reservedc_99
ret <8 x i32> %intr
}
;result
i32 %_reservedc_99 = #x0000001e (30)
However, when I proceed to check whether they are really equivalent using compareFunctions:
define <8 x i32> @cut.256.257(<32 x i8> %__n3, i16 %__n4, i32 %_reservedc_99) {
#0:
%__n0 = shufflevector <32 x i8> %__n3, <32 x i8> poison, 3, 7, 11, 15, 19, 23, 27, 31
%__n1 = lshr <8 x i8> %__n0, { 6, 6, 6, 6, 6, 6, 6, 6 }
%__n2 = zext <8 x i8> %__n1 to <8 x i32>
ret <8 x i32> %__n2
}
=>
define <8 x i32> @cut.256(<32 x i8> %__n3, i16 %__n4, i32 %_reservedc_99) {
#0:
%#1 = bitcast <32 x i8> %__n3 to <8 x i32>
%intr = x86_avx2_psrli_d <8 x i32> %#1, i32 30
ret <8 x i32> %intr
}
Alive2 provides a counterexample about poison values:
ERROR: Target is more poisonous than source
Example:
<32 x i8> %__n3 = < #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), poison, #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3) >
i16 %__n4 = poison
i32 %_reservedc_99 = poison
Source:
<8 x i8> %__n0 = < #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3), #x03 (3) >
<8 x i8> %__n1 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
<8 x i32> %__n2 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >
Target:
<8 x i32> %#1 = < #x03030303 (50529027), poison, #x03030303 (50529027), #x03030303 (50529027), #x03030303 (50529027), #x03030303 (50529027), #x03030303 (50529027), #x03030303 (50529027) >
<8 x i32> %intr = < #x00000000 (0), poison, #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >
Source value: < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >
Target value: < #x00000000 (0), poison, #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >
I am a little confused with this inconsistency. Considering this example, I wonder whether this optimization should be treated as correct.
In enumerator.cpp,
compareFunctionsorconstantSynthesiswill be invoked according to whether the sketch contains any constant:However, we find that their tolerance to
poisonis different.Considering Example 3 in the paper:
Minotaur can successfully generate this rewrite by
constantSynthesis:However, when I proceed to check whether they are really equivalent using
compareFunctions:Alive2 provides a counterexample about poison values:
I am a little confused with this inconsistency. Considering this example, I wonder whether this optimization should be treated as correct.