Let's just start with a topic. If I encounter new errors in subsequent topics, I'll update the article
I made a mistake and told me my QQ 935797872
I. Preparations
Catalog
Generate a puzzle solver called flag, notice there's a capitalization'S'
Declare the type of a single unknown parameter
An array as a parameter is important and saves time
x.add() Add constraints to solve problems
Check for solutions and output
Problem with parameter settings
I made a mistake and told me my QQ 935797872
You are going to download z3!
First go to Baidu and download Z3 from the command line, then you know how to install z3. It looks like pip install z3-solver... Or go to Baidu
Okay, you can install it directly from the cmd window. If the download is slow, quit. Try changing your phone hotspot
pip install z3-solver
Then you can use it directly from vscode, I don't like pycharm,vscode is good, and you have to remember that z3 must be Python 3.8 and once, your Python 3.9 has nothing to do with it
2. Basic Grammar
Introduce header file
from z3 import*
Generate a puzzle solver called flag, notice there's a capitalization'S'
from z3 import* flag=Solver()
Declare the type of a single unknown parameter
x = Int('x')
x,y=Ints('x y') #Here's an Ints
s= BitVec('s',8)
s1,s2 = BitVec('s1 s2',8)
'''Here 8 is the parameter 8 bit Of,That is, the parameter size is 1 byte byte,Write 16,Is 2 bytes,8 or 16,See how the title requires unknown numbers'''We often use BitVec variables, which are the only operations that can be bitwise, that is, those
> <* | & ~ ^ BitVec's variable type is required for operation
An array as a parameter is important and saves time
s= [BitVec('%d'%i,8) for i in range(18)]
s= [BitVec('s[%d]'%i,8) for i in range(18)]The%d should be similar to the c language, and the 16 and 8 are bit 1
This is where we define an array s of length 18, so we use s[1],s[2]...
For the second, it means that you will have one more s[i] in the output of your answer, such as the second, below
[s[1] = 90, s[3] = 123, s[8] = 105, s[0] = 70, s[11] = 103, s[2] = 81, s[12] = 95, s[17] = 125, s[6] = 95, s[10] = 110, s[14] = 105, s[4] = 90, s[5] = 97, s[15] = 65, s[7] = 74, s[9] = 97, s[13] = 77, s[16] = 78]
For the first writing, the output looks like this
[70, 90, 81, 123, 90, 97, 95, 74, 105, 97, 110, 103, 95, 77, 105, 65, 78, 125]
x.add() Add constraints to solve problems
s.add(cmp[j]==table[(s[i]>>2)^0x34])
It is worth noting that add() can only contain judgement statements, not assignment statements.
Check for solutions and output
if x.check() == sat:
flag_result = solver.model()
print(flag_result)
else:
print("no flag_result!")Here sat means satisface satisfies
check()
To detect the solution,
model()
When there is a solution, the intersection of the solutions, unless there is only one solution
Talk about the considerations
Ignore Constraints
v3 = (unsigned __int8)(flag >> 7) >> 4;
This is how z3 (handles u int9) takes &0xff
v3 =(((s[i] >> 7)&0xff) >> 4)&0xff
Problem with parameter settings
Such as 16bit and 8bit
ascill range not considered
for i in range(18):
....
x.add(s[i]>=20)
x.add(s[i]<=127)Talk about output techniques
We often encounter output solutions that are out of order, like the following
[s[1] = 90, s[3] = 123, s[8] = 105, s[0] = 70, s[11] = 103, s[2] = 81, s[12] = 95, s[17] = 125, s[6] = 95, s[10] = 110, s[14] = 105, s[4] = 90, s[5] = 97, s[15] = 65, s[7] = 74, s[9] = 97, s[13] = 77, s[16] = 78]
We want it to output in order
Declare another array, and he writes it sequentially to the flag array
head
s= [BitVec('%d'%i,8) for i in range(18)]
tail
Declare an array first
flag=[]
if x.check() == sat:
ans = x.model()
for i in s:
flag.append(ans[i])