Skip to content

Failure in solve fuzzer #9242

Description

@alexreinking

Description

We hit a fuzz failure in the CI for #9241

Reproducing case

Seed: 12497262138497136136
solve_expression produced a non-equivalent result:
  a0 = 32
  a1 = 3
  a2 = 3
  a3 = -30
  a4 = 3
  variable being solved: a2
  original: ((int32(uint1(int32(uint1(int32(uint32(a1))) || uint1(select(255 >= (244 ^ 68), a3, 65)))) || uint1(max(185 + 42, 202))) + (75 % 76)) < (int32(uint8(-1_i8))*select(103 <= int32(true || true), max(a3, select(shift_right(a2, 194 % 32) <= (int32(uint1(a0) || true) | a1), select(57 <= int32(211_u32), int32(true && true), select(207 < 250, a4, 203)), select(101 > 246, a3, 187))), select(int32((uint32)absd(int32(89_i64)/select(118 != 138, a2, 12), 244)) == int32((219_i64 ^ 147_i64) ^ 126_i64), ~(a3) & 237, 124)))) -> true
  solved:   (select(103 <= int32(true), max(select(shift_right(a2, 194 % 32) <= (int32(uint1(a0) || true) | a1), select(57 <= int32(211_u32), int32(true), select(207 < 250, a4, 203)), select(101 > 246, a3, 187)), a3), select(int32((uint32)absd(int32(89_i64)/select(118 != 138, a2, 12), 244)) == int32((219_i64 ^ 147_i64) ^ 126_i64), ~(a3) & 237, 124)) < (0 - (int32(uint1(int32(uint1(int32(uint32(a1))) || uint1(select(255 >= (244 ^ 68), a3, 65)))) || uint1(227)) + (75 % 76)))) -> false
Failing comparison (C++):
Expr expr_0 = Variable::make(Type(Type::Int, 32, 1), "a1");
Expr expr_1 = Cast::make(Type(Type::UInt, 32, 1), expr_0);
Expr expr_2 = Cast::make(Type(Type::Int, 32, 1), expr_1);
Expr expr_3 = Cast::make(Type(Type::UInt, 1, 1), expr_2);
Expr expr_4 = IntImm::make(Type(Type::Int, 32, 1), 255);
Expr expr_5 = IntImm::make(Type(Type::Int, 32, 1), 244);
Expr expr_6 = IntImm::make(Type(Type::Int, 32, 1), 68);
Expr expr_7 = Call::make(Type(Type::Int, 32, 1), "bitwise_xor", {expr_5, expr_6}, Call::CallType::PureIntrinsic);
Expr expr_8 = GE::make(expr_4, expr_7);
Expr expr_9 = Variable::make(Type(Type::Int, 32, 1), "a3");
Expr expr_10 = IntImm::make(Type(Type::Int, 32, 1), 65);
Expr expr_11 = Select::make(expr_8, expr_9, expr_10);
Expr expr_12 = Cast::make(Type(Type::UInt, 1, 1), expr_11);
Expr expr_13 = Or::make(expr_3, expr_12);
Expr expr_14 = Cast::make(Type(Type::Int, 32, 1), expr_13);
Expr expr_15 = Cast::make(Type(Type::UInt, 1, 1), expr_14);
Expr expr_16 = IntImm::make(Type(Type::Int, 32, 1), 185);
Expr expr_17 = IntImm::make(Type(Type::Int, 32, 1), 42);
Expr expr_18 = Add::make(expr_16, expr_17);
Expr expr_19 = IntImm::make(Type(Type::Int, 32, 1), 202);
Expr expr_20 = Max::make(expr_18, expr_19);
Expr expr_21 = Cast::make(Type(Type::UInt, 1, 1), expr_20);
Expr expr_22 = Or::make(expr_15, expr_21);
Expr expr_23 = Cast::make(Type(Type::Int, 32, 1), expr_22);
Expr expr_24 = IntImm::make(Type(Type::Int, 32, 1), 75);
Expr expr_25 = IntImm::make(Type(Type::Int, 32, 1), 76);
Expr expr_76 = IntImm::make(Type(Type::Int, 32, 1), 118);
Expr expr_77 = IntImm::make(Type(Type::Int, 32, 1), 138);
Expr expr_78 = NE::make(expr_76, expr_77);
Expr expr_79 = Variable::make(Type(Type::Int, 32, 1), "a2");
Expr expr_80 = IntImm::make(Type(Type::Int, 32, 1), 12);
Expr expr_81 = Select::make(expr_78, expr_79, expr_80);
Expr expr_82 = Div::make(expr_75, expr_81);
Expr expr_83 = IntImm::make(Type(Type::Int, 32, 1), 244);
Expr expr_84 = Call::make(Type(Type::UInt, 32, 1), "absd", {expr_82, expr_83}, Call::CallType::PureIntrinsic);
Expr expr_85 = Cast::make(Type(Type::Int, 32, 1), expr_84);
Expr expr_86 = IntImm::make(Type(Type::Int, 64, 1), 219);
Expr expr_87 = IntImm::make(Type(Type::Int, 64, 1), 147);
Expr expr_88 = Call::make(Type(Type::Int, 64, 1), "bitwise_xor", {expr_86, expr_87}, Call::CallType::PureIntrinsic);
Expr expr_89 = IntImm::make(Type(Type::Int, 64, 1), 126);
Expr expr_90 = Call::make(Type(Type::Int, 64, 1), "bitwise_xor", {expr_88, expr_89}, Call::CallType::PureIntrinsic);
Expr expr_91 = Cast::make(Type(Type::Int, 32, 1), expr_90);
Expr expr_92 = EQ::make(expr_85, expr_91);
Expr expr_93 = Variable::make(Type(Type::Int, 32, 1), "a3");
Expr expr_94 = Call::make(Type(Type::Int, 32, 1), "bitwise_not", {expr_93}, Call::CallType::PureIntrinsic);
Expr expr_95 = IntImm::make(Type(Type::Int, 32, 1), 237);
Expr expr_96 = Call::make(Type(Type::Int, 32, 1), "bitwise_and", {expr_94, expr_95}, Call::CallType::PureIntrinsic);
Expr expr_97 = IntImm::make(Type(Type::Int, 32, 1), 124);
Expr expr_98 = Select::make(expr_92, expr_96, expr_97);
Expr expr_99 = Select::make(expr_36, expr_73, expr_98);
Expr expr_100 = Mul::make(expr_30, expr_99);
Expr expr_101 = LT::make(expr_27, expr_100);
Expr final_expr = expr_101;
  solving for "a2"

How did you get Halide?

None

Halide version

No response

Halide commit (if known)

No response

Target

No response

Operating system

No response

Additional context

No response

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions