## 3 Design
### Abstract Syntax Tree Analysis
#### 3.2.2 Prioritization of Symbolic Execution States
```
Input: Current execution state \(State_{current}\), Previously executed basic block information \(I_{previous}\) (Dictionary) Result: Successor execution states \(NewStates\) (List), priority of successor execution states \(Priority\), newly executed basic block information \(I_{new}\) (Dictionary)
1\(NewStates\), \(\texttt{expr}\leftarrow\texttt{SymbolicExecution}(State_{current})\);
2 ifGetStateAddr (\(State_{current}\)) in GetDictKeys(\(I_{previous}\)) then
3 PreviousStateInfo \(\leftarrow\) GetInfoByAddr (\(I_{previous}\), GetStateAddr (\(State_{current}\)));
4 ifStateInfoIsCritical(PreviousStateInfo)then
5 PositiveDirection \(\leftarrow\) GetPositiveDirection(PreviousStateInfo);
6 ifPositiveDirection == 'not sure'then
7 Priority \(\leftarrow\)Middle';
8
9 elseifPositiveDirection == '+'then
10 ifexpr > All(GetExprsByInfo(PreviousStateInfo))then
11 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Positive');
12 elseifexpr < All(GetExprsByInfo(PreviousStateInfo)) then
13 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Negative');
14
15 else
16 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Middle');
17
18
19 elseifPositiveDirection == '-'then
20 ifexpr < All(GetExprsByInfo(PreviousStateInfo))then
21 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Positive');
22
23 elseifexpr > All(GetExprsByInfo(PreviousStateInfo))then
24 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Negative');
25
26 else
27 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Middle');
28
29
30 end if
31
32 end if
33
34
35 else
36 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Non-critical');
37
38
39 else
40\(I_{new}\leftarrow\) SetInfoByAddr (\(I_{previous}\), GetStateAddr (\(State_{current}\)),expr);
41
42 Priority \(\leftarrow\) SetPriority(\(NewStates\), 'Not executed');
43
44
45 end if
46
47 forSuccessorState in NewStatesdo
48 ifStateSatisfiable(SuccessorState) == Falsethen
49 UnsatConstraint \(\leftarrow\) GetUnsatConstraintFromState(SuccessorState);
50 forStateAddr,Exprs in GetKeyValueFromDict(\(I_{previous}\))do
51 ifAny(Exprs) in GetChildrenAST(UnsatConstraint)then
52\(I_{new}\leftarrow\) MarkStateInfoAsCritical(\(I_{previous}\), StateAddr,Exprs);
53
54 end if
55
56 end if
57
58 end for
59
60 end for
61
62 end for
63
64 end for
```  
**Algorithm 1**Multi-priority scheduling algorithm  
```
Input: Current execution state \(State_{current}\), Previously executed basic block information \(I_{previous}\) (Dictionary) Result: Successor execution states \(NewStates\) (List), priority of successor execution states \(Priority\), newly executed basic block information \(I_{new}\) (Dictionary)
``` Input: Current execution state \(State_{current}\), Previously executed basic block information \(I_{previous}\) (Dictionary) Result: Successor execution states \(NewStates\) (List), priority of successor execution states \(Priority\), newly executed basic block information \(I_{new}\) (Dictionary) Result: Successor execution states \(Priority\), newly executed basic block information \  
The first task of the multi-priority scheduling algorithm is to prioritize the states for symbolic execution. After a state is symbolically executed, we first determine if the basic block where the state is located is being executed for the first time in line 2. If this is the first time the basic block is executed, we record the address and the expression generated during the execution into the \(I_{new}\) and set the priority as \"Not executed\" in lines 29 and 30. If not, we will determine if the expression generated at the previous same position is critical in lines 3 and 4. After that, we calculate the positive direction of the current position based on the previous state information of the same position in line 5. We decide the priority of the state based on whether the relationship between the newly generated expression and the previously generated expression matches the positive direction in lines 6 to 24. The result of the priority affects the current state's successor state.