KCTF_北冥神功

一道迷宫题，核心内容:

LABEL_11:
          v7 = (v4 + v5 / 6) % 6;               // v5为下标
          v8 = v5 + v4;
          count = v22;                          // 初始为0
          v20 = v7;
          v10 = 5 - v8 % 6;                     // 5-(v5+v4)%6
          for ( i = 0; ; i = 1 )                // 奇偶交替
          {
            switch ( v10 )
            {
              case 1:
                ++count;
                break;
              case 2:
                v17 = (I++ & 1) == 0;           // 偶数1,奇数0
                count += v17;
                break;
              case 3:
                v12 = (I++ & 1) != 0;           // 偶数0,奇数1
                count -= v12;
                break;
              case 4:
                --count;
                break;
              case 5:
                v19 = (I-- & 1) != 0;
                count -= v19;
                break;
              default:
                v18 = (I-- & 1) == 0;
                count += v18;
                break;
            }
            if ( count > 9 )
              break;
            if ( I > 8 )
              break;
            v13 = &aS_1[10 * I + count];
            if ( *v13 )
              break;
            *v13 = 1;
            if ( i == 1 )
            {
              ++v4;
              v22 = count;
              v3 = v25[v4];
              if ( v3 )
                goto LABEL_4;
              goto LABEL_19;
            }
            v10 = v20;
          }
        }
        else
        {
          while ( v24 != ++v5 )
          {
            if ( byte_4B7040[v5] == v3 )
              goto LABEL_11;
          }
        }
      }
    }

确定迷宫样子:10*9,并且会将走过的0转换成1:

S 0 1 0 0 1 0 0 1 1 
1 1 0 0 1 0 0 1 0 0 
0 0 1 0 1 1 1 1 1 0 
0 1 1 0 1 0 0 1 0 0 
0 0 1 0 0 1 0 0 1 1 
1 1 0 1 1 1 0 1 0 1 
0 0 1 1 1 1 0 1 0 1 
0 1 1 0 0 1 0 1 0 1 
0 0 0 1 0 0 1 1 0 0 

要打印Good job!，就需要迷宫中没有0，再看迷宫走法:

         for ( i = 0; ; i = 1 )                // 奇偶交替
          {
            switch ( v10 )
            {
              case 1:
                ++count;
                break;
              case 2:
                v17 = (I++ & 1) == 0;           // 偶数1,奇数0
                count += v17;
                break;
              case 3:
                v12 = (I++ & 1) != 0;           // 偶数0,奇数1
                count -= v12;
                break;
              case 4:
                --count;
                break;
              case 5:
                v19 = (I-- & 1) != 0;
                count -= v19;
                break;
              default:
                v18 = (I-- & 1) == 0;
                count += v18;
                break;
            }

很奇妙，刚开始看这里有点蒙，但是结合后面代码，确定个个数字之间代表的含义:

	1	2	3	4	5	0
奇数	右→	下↓	左下↙	左←	左上↖	上↑
偶数	右→	右下↘	下↓	左←	上↑	右上↗

获得走法:

1,2,3,4,3,2,1,2,3,4,3,2,1,1,0,1,2,1,0,0,5,0,5,4,3,4,5,0,5,0,1,2,1,0,1,2,1,2,3,4,3,2,2,3,2,1

逆推输入的值，很容易发现，两两一对，其中奇数位会影响到偶数位，而奇数位只受自己影响，可以根据这个条件，写解题脚本

from z3 import *
str_arr="0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"
odd=[1,3,3,1,3,3,1,0,2,0,5,5,3,5,5,1,1,1,1,3,3,2,2]
even=[2,4,2,2,4,2,1,1,1,0,0,4,4,0,0,2,0,2,2,4,2,3,1]
flag=[BitVec("%d" %i,8)for i in range(len(odd))]
s=Solver()
for i in range(len(odd)):
    s.add(5-(flag[i]+i)%6==odd[i])
    s.add((i+flag[i]/6)%6==even[i])
    s.add(flag[i]>=0,flag[i]<len(str_arr))
tmp=[]
if(s.check()==sat):
    m=s.model()
    for i in flag:
        tmp.append(m[i].as_long())
else:
    print("error")
for i in tmp:
    print(str_arr[i],end="")

获得flag:

GJ0V4LA4VKEVQZSVCNGJ00N