summarize

题目要求输入 a~f 六个正整数

通过观察和带入值尝试，发现这些函数的实现都是基本运算

_BOOL8 __fastcall sub_40137B(
        unsigned int a1,
        unsigned int a2,
        unsigned int a3,
        unsigned int a4,
        unsigned int a5,
        unsigned int a6)
{
  unsigned int v7; // eax
  int v8; // ebx
  unsigned int v9; // eax
  unsigned int v10; // ebx
  unsigned int v11; // eax
  unsigned int v12; // eax
  unsigned int v18; // [rsp+20h] [rbp-30h]
  unsigned int v19; // [rsp+24h] [rbp-2Ch]
  unsigned int v20; // [rsp+28h] [rbp-28h]
  unsigned int v21; // [rsp+2Ch] [rbp-24h]
  unsigned int v22; // [rsp+30h] [rbp-20h]
  unsigned int v23; // [rsp+34h] [rbp-1Ch]
  unsigned int v24; // [rsp+38h] [rbp-18h]
  unsigned int v25; // [rsp+3Ch] [rbp-14h]

  if ( a1 <= 100000000 || a2 <= 0x5F5E100 || a3 <= 0x5F5E100 || a4 <= 0x5F5E100 || a5 <= 0x5F5E100 || a6 <= 0x5F5E100 )
    return 0LL;
  if ( a1 > 999999999 || a2 > 0x3B9AC9FF || a3 > 0x3B9AC9FF || a4 > 0x3B9AC9FF || a5 > 0x3B9AC9FF || a6 > 0x3B9AC9FF )
    return 0LL;
  v7 = sub(a1, a2);
  v18 = add(v7, a3) % 0x10AE961;
  v19 = add(a1, a2) % 0x1093A1D;
  v8 = mul(2u, a2);
  v9 = mul(3u, a1);
  v10 = sub(v9, v8);
  v20 = v10 % xor(a1, a4);
  v11 = add(a3, a1);
  v21 = and(a2, v11) % 0x6E22;
  v22 = add(a2, a4) % a1;
  v12 = add(a4, a6);
  v23 = xor(a3, v12) % 0x1CE628;
  v24 = sub(a5, a6) % 0x1172502;
  v25 = add(a5, a6) % 0x2E16F83;
  return v18 == 4139449
      && v19 == 9166034
      && v20 == 556569677
      && v21 == 12734
      && v22 == 540591164
      && v23 == 1279714
      && v24 == 17026895
      && v25 == 23769303;
}

至此，我们可以写出z3-solver脚本

from z3 import *
s = Solver()
x = [BitVec(f"x{i}", 32) for i in range(6)]

for i in x:
    s.add(i > 100000001, i <= 999999999)

a1,a2,a3,a4,a5,a6=x[0],x[1],x[2],x[3],x[4],x[5]
sub = lambda a1,a2 : a1 - a2
add = lambda a1,a2 : a1 + a2
mul = lambda a1,a2 : a1 * a2
xor = lambda a1,a2 : a1 ^ a2
_and = lambda a1,a2 : a1 & a2

v7 = sub(a1, a2)
v18 = add(v7, a3) % 0x10AE961
v19 = add(a1, a2) % 0x1093A1D
v8 = mul(2, a2)
v9 = mul(3, a1)
v10 = sub(v9, v8)
v20 = v10 % xor(a1, a4)
v11 = add(a3, a1)
v21 = _and(a2, v11) % 0x6E22
v22 = add(a2, a4) % a1
v12 = add(a4, a6)
v23 = xor(a3, v12) % 0x1CE628
v24 = sub(a5, a6) % 0x1172502
v25 = add(a5, a6) % 0x2E16F83;v18 = (v7 + a3) % 0x10AE961
v19 = (a1 + a2) % 0x1093A1D
s.add(v18 == 4139449)
s.add(v19 == 9166034)
s.add(v20 == 556569677)
s.add(v21 == 12734)
s.add(v22 == 540591164)
s.add(v23 == 1279714)
s.add(v24 == 17026895)
s.add(v25 == 23769303)
print(s.check())
m = s.model()
for i in x:
    print(hex(m[i].as_long())[2:], end='')
# 2a142dd72e87fa9c1456a32d1bc4f77739975e5fcf5c6c0
# uiuctf{2a142dd72e87fa9c1456a32d1bc4f77739975e5fcf5c6c0}

附，运算符优先级（从上到下依次降低）：

~
* /
+ -
<< >>
^
&
|