doc init

Author: QiongwenXu

doc/main.tex

@@ -0,0 +1,332 @@
+\documentclass{article}
+\usepackage[utf8]{inputenc}
+\usepackage{algorithm}
+\usepackage{algorithmic}
+\usepackage{amsmath}
+\usepackage{bm}
+\usepackage{listings}
+\usepackage[usenames,dvipsnames]{xcolor}
+\title{smtGen}
+\author{qx51 }
+\date{October 2019}
+\renewcommand{\algorithmicrequire}{ \textbf{Input:}} %Use Input in the format of Algorithm
+\renewcommand{\algorithmicensure}{ \textbf{Output:}} %UseOutput in the format of Algorithm
+
+\definecolor{mygreen}{rgb}{0,0.6,0}
+\definecolor{mygray}{rgb}{0.5,0.5,0.5}
+\definecolor{mymauve}{rgb}{0.58,0,0.82}
+\lstset{ %
+backgroundcolor=\color{white},      % choose the background color
+basicstyle=\footnotesize\ttfamily,  % size of fonts used for the code
+columns=fullflexible,
+tabsize=4,
+breaklines=true,               % automatic line breaking only at whitespace
+captionpos=b,                  % sets the caption-position to bottom
+commentstyle=\color{mygreen},  % comment style
+escapeinside={\%*}{*)},        % if you want to add LaTeX within your code
+keywordstyle=\color{blue},     % keyword style
+stringstyle=\color{mymauve}\ttfamily,  % string literal style
+frame=single,
+rulesepcolor=\color{red!20!green!20!blue!20},
+% identifierstyle=\color{red},
+language=c++,
+}
+
+\begin{document}
+
+\section{Algorithm for program SMT}
+\subsection{Definition}
+
+Some definitions are made in order to make the algorithm easier understood.
+\begin{enumerate}
+\item $F_{i}$ is SMT formula for the basic block $i$.
+\item $r_{i\_j\_k}$ represents the register value, where $i$ is the register ID, $j$ is the basic block ID, $k$ is the version ID (i.e., the number of update times in this block). $k$ starts from $0$ and each update in this basic block will increase $k$ by 1. For example, $r_{0\_0\_1}$ is the value that represents $r_1$ in basic block 0 (i.e., the starting basic block), and $r_1$ has been updated once in basic block 0. $j$ ensures that each basic block has its own register version, and $k$ ensures that different values of the same register can be differed in the same basic block.
+\item $f_{pl}$ is the formula of program logic for the current basic block.
+\item $IV = \{iv_0, iv_1, ... \}$ is the initial value set for all basic blocks. Each item $iv_i = \langle iv_{i\_0}, iv_{i\_1}, ... \rangle = \langle r_{0\_\bm{i}\_k_0}, r_{1\_\bm{i}\_k_1}, ...\rangle$ represents the initial values of all registers \textbf{\textit{generated}} by basic block $i$.
+
+\item $f_{iv}$ is the formula representing the logic that initial values of register from the last basic block $b_1$ are fed to the register values in current basic block $b_2$, that is,
+\begin{equation}
+\begin{aligned}
+f_{iv} &= \bigwedge_{i} r_{i\_b_1\_k_i} == r_{i\_b_2\_0} \\
+&= \bigwedge_{i} iv_{b_1\_i} == r_{i\_b_2\_0}
+\end{aligned}
+\end{equation}
+\item $C = \{c_{b_{i_1}\rightarrow b_{j_1}}, c_{b_{i_2}\rightarrow b_{j_2}}, ...\}$ is the initial path condition formulas set for all edges. Each item $c_{b_i\rightarrow b_j}$ is a path condition formula generated by the basic block $b_i$ for the basic block $b_j$. 
+The post path condition $C_b$ for the basic block $b$ is
+\begin{equation}
+C_b = \bigcup_i \{c_{parents}\wedge c_{instEnd\_case_i}\}
+\end{equation}
+where $c_{parents} = \bigvee_{p} c_{p\rightarrow b}$
+\end{enumerate}
+
+\subsection{Target SMT formula}
+SMT formula for the program (do not take pre-condition or post-condition into consideration here) is 
+
+\begin{equation}
+\begin{aligned}
+F &= \bigwedge_i F_{i} \\
+  &= \bigwedge_i \bigwedge_j c_{j\rightarrow i}\rightarrow f_{iv\_i} \wedge f_{pl\_i}
+\end{aligned}
+\end{equation}
+
+\begin{algorithm}
+\begin{algorithmic}[1]
+\caption{SMT\_Prog}
+\label{alg:smt_prog}
+% \REQUIRE $instLst$, $instLstLen$, $inputRegLst$
+\REQUIRE $instLst$, $instLstLen$
+\ENSURE $F$, $outputRegLst$
+\STATE // Sort basic blocks by Topological\_Sorting
+\STATE // $B = \langle b_0, b_1, ...\rangle$ is set of basic blocks, $b_0$ is the start basic block
+\STATE // $InB = \langle inb_0, inb_1, ...\rangle$ is set of incoming edges for each basic block
+\STATE // $OutB = \langle outb_0, outb_1, ...\rangle$ is set of outgoing edges for each basic block
+\STATE // $InB$ and $OutB$ are from $cfg$
+\STATE $cfg \Leftarrow Gen\_Cfg(instLst, instLstLen)$
+\STATE $B \Leftarrow Topological\_Sorting(cfg)$
+\STATE
+\STATE // Process Basic Block 0
+\STATE $f_{pl} \Leftarrow Gen\_Block\_Prog\_Logic(0,instLst[start:end])$
+% \STATE $f_{iv} \Leftarrow \bigwedge_{i=1}^{i=NumOfReg} inputRegLst_i ==  r_{i\_0\_0}$
+% \STATE $F_0 \Leftarrow true \rightarrow (f_{iv} \wedge f_{pl})$
+\STATE $F_0 \Leftarrow f_{pl}$
+\STATE $iv_0 \Leftarrow Get\_Cur\_Reg\_Val(0)$
+\STATE $IV \Leftarrow \{iv_0\}$
+\STATE $C \Leftarrow Gen\_Path\_Cond\_For\_Next\_Blocks(0, instLst[end], inb_0, outb_0)$
+
+\STATE
+\STATE // Process Basic Block $1 \rightarrow (len-1)$
+\FOR{$i=1$ to $len(B)-1$}
+\STATE $f_{pl} \Leftarrow Gen\_Block\_Prog\_Logic(i,instLst[start:end])$
+\STATE $F_i \Leftarrow true$
+\FOR{each last block $b$ in $inb_{\bm{i}}$}
+\STATE $f_{iv} \Leftarrow \bigwedge_{j=1}^{j=NumOfReg} iv_{b_\_j} ==  r_{j_\_i_\_0}$
+\STATE $F_i \Leftarrow F_i \wedge (c_{b \rightarrow i} \rightarrow (f_{iv} \wedge f_{pl}))$
+\ENDFOR
+\STATE $iv_i \Leftarrow Get\_Cur\_Reg\_Val(i)$
+\STATE $IV \Leftarrow IV \cup \{iv_i\}$
+\STATE $C_{out\_i} \Leftarrow Gen\_Path\_Cond\_For\_Next\_Blocks(i, instLst[end], inb_i, outb_i)$
+\STATE $C \Leftarrow C \cup C_{out_\_i}$
+\ENDFOR
+\STATE
+\FOR{$i=0$ to $len(B)-1$}
+\STATE $F \Leftarrow F \wedge F_i$
+\ENDFOR
+\STATE
+\STATE initialize $outputRegLst$
+\FOR{$i=0$ to $NumOfReg-1$}
+\STATE $outputRegLst_i \Leftarrow iv_{(instLstLen-1)\_i}$
+\ENDFOR
+\RETURN $outputRegLst_i$
+\end{algorithmic}
+\end{algorithm}
+
+\begin{algorithm}
+\begin{algorithmic}[1]
+\caption{Gen\_Block\_Prog\_Logic}
+\REQUIRE Basic Block ID $b$, $instLst$
+\ENSURE $f_{pl}$
+\STATE $f_{pl} \Leftarrow true$
+\FOR{$i=1$ to $len(instLst)$}
+\IF{type of instruction is not $JMP$ or $END$}
+\STATE $f_{pl} \Leftarrow f_{pl} \wedge f_{instruction_\_i}$
+\ENDIF
+\ENDFOR
+\RETURN $f_{pl}$
+\end{algorithmic}
+\end{algorithm}
+
+\begin{algorithm}
+\begin{algorithmic}[1]
+\caption{Get\_Cur\_Reg\_Val}
+\REQUIRE Basic Block ID $b$, $R_b$
+\ENSURE $iv_b$
+\STATE $iv_{b} \Leftarrow\emptyset$
+\FOR{$i=0$ to $(NumberOfRegisters-1)$}
+\STATE //$R$ stores the current values of all register for the basic blocks
+\STATE $iv_{b} \Leftarrow iv_{b} \cup \{R_{b\_i}\}$ 
+\ENDFOR
+\RETURN $iv_{b}$
+\end{algorithmic}
+\end{algorithm}
+
+\begin{algorithm}
+\begin{algorithmic}[1]
+\caption{Gen\_Path\_Cond\_For\_Next\_Blocks}
+\REQUIRE Basic Block ID $b$, $instEnd$, $inBlocks$, $outBlocks$
+\ENSURE $C_{out}$
+\STATE $c_{in} \Leftarrow true$
+\FOR{each last block $b_{i}$ in $inBlocks$}
+\STATE $c_{in} \Leftarrow c_{in} \vee c_{b_i \rightarrow b}$
+\ENDFOR
+\STATE $C_{out} \Leftarrow \emptyset$
+\STATE $c_{instEnd} \Leftarrow Parse Instruction(instEnd)$
+\FOR{each last block $c$ in $c_{instEnd}$}
+\STATE $C_{out} \Leftarrow C_{out} \cup \{c_{in} \wedge c\}$
+\ENDFOR
+\RETURN $C_{out}$
+\end{algorithmic}
+\end{algorithm}
+
+\subsection{Example}
+\begin{enumerate}
+\item Instructions:
+\begin{lstlisting}
+inst(MOVXC, 2, 15),   // 0 mov r2, 15
+inst(JMPGT, 0, 2, 2), // 1 if r0 <= r2 no jmp else jmp to 4
+inst(ADDXY, 0, 1),    // 2 add r0, r1
+inst(RETX, 2),        // 3 ret r2
+inst(ADDXY, 2, 1),    // 4 add r2, r1
+inst(RETX, 0),        // 5 else ret r0
+\end{lstlisting}
+\item Instructions $\rightarrow$ CFG \\
+CFG:\\
+nodes: 0[0:1] 1[2:3] 2[4:5] \\
+edges: 0 $\rightarrow$ 1 0 $\rightarrow$ 2 
+\item List by topological Sorting \\
+$B = \langle 0, 1, 2 \rangle$ \\
+$InB = \langle \langle\rangle, \langle 0 \rangle, \langle 0 \rangle \rangle$ \\
+$OutB = \langle \langle 1, 2 \rangle, \langle\rangle, \langle  \rangle \rangle$
+\item Process Node 0 \\
+$f_{pl} = (r_{2\_0\_1} == 15)$\\
+$iv_0 = \langle r_{0\_0\_0},r_{1\_0\_0},r_{2\_0\_1}\rangle$ \\
+$IV = \{iv_0\}$\\
+$F_0 = (r_{2\_0\_1} == 15)$ \\
+$C_{out\_0} = \{ c_{0\rightarrow 1}=(r_0 > r_2), c_{0\rightarrow 2}=\neg(r_0 > r_2)\}$ \\
+$C = C_{out\_0}$
+\item Process Node 1 \\
+$f_{pl} = (r_{0\_1\_1} == r_{0\_1\_0} + r_{1\_1\_0})$\\
+$iv_1 = \langle r_{0\_1\_1},r_{1\_1\_0},r_{2\_1\_0}\rangle$\\ 
+$IV = \{iv_0, iv_1\}$\\
+$f_{iv} = \bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_1\_0})$\\
+$F_1 = c_{0\rightarrow 1} \rightarrow f_{iv} \wedge f_{pl} = (r_0 > r_2)\rightarrow (\bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_1\_0}) \wedge (r_{0\_1\_1} == r_{0\_1\_0} + r_{1\_1\_0}))$ \\
+$C_{out\_1} = \emptyset$ \\
+$C = C_{out\_0}$ 
+\item Process Node 2 \\
+$f_{pl} = (r_{2\_2\_1} == r_{2\_2\_0} + r_{1\_2\_0})$\\
+$iv_1 = \langle r_{0\_2\_0},r_{1\_2\_0},r_{2\_2\_1}\rangle$\\ 
+$IV = \{iv_0, iv_1, iv_2\}$\\
+$f_{iv} = \bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_2\_0})$\\
+$F_2 = c_{0\rightarrow 2} \rightarrow f_{iv} \wedge f_{pl} = \neg(r_0 > r_2)\rightarrow (\bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_2\_0})\wedge (r_{2\_2\_1} == r_{2\_2\_0} + r_{1\_2\_0}))$ \\
+$C_{out\_2} = \emptyset$ \\
+$C = C_{out\_0}$ 
+\item Generate $F$ \\
+$F = F_0 \wedge F_1 \wedge F_2$ \\
+where \\
+$F_0 = true\rightarrow  (true \wedge (r_{2\_0\_1} == 15))$ \\
+$F_1 = (r_0 > r_2)\rightarrow (\bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_1\_0}) \wedge (r_{0\_1\_1} == r_{0\_1\_0} + r_{1\_1\_0}))$ \\
+$F_2 = \neg(r_0 > r_2)\rightarrow (\bigwedge_{i=1}^{i=3} (iv_{0\_i} == r_{i\_2\_0})\wedge (r_{2\_2\_1} == r_{2\_2\_0} + r_{1\_2\_0}))$ 
+\end{enumerate}
+
+\section{Algorithm for equivalence check}
+\subsection{Definition}
+\begin{enumerate}
+\item Since there are two programs, a new dimension, program ID, should be added into register value $r_{i\_j\_k}$ to ensure that each program has it own register value version. Then $r_{i\_j\_k}$ extends to $\bm{r_{i\_j\_k\_p}}$, where $p$ is the program ID.
+\item Equivalence check formula
+\begin{equation}
+F = F_{pre_1} \wedge F_{pre_2} \wedge F_1 \wedge F_2 \rightarrow F_{post}
+\end{equation}
+where \\
+$F_{pre_i}$, $F_i$, $F_{post}$ are the pre-conditon, program logic, post-condition FOL formulas of program $i$, that is,
+\begin{equation}
+F_{pre_i} = (r_{0\_*\_*\_i})\wedge (\bigwedge_{j = 1}^{j = NumOfReg-1} r_{j\_*\_*\_i} == 0) 
+\end{equation}
+
+\begin{equation}
+\begin{aligned}
+F_{i} &= (\bigwedge_{j=0}^{j=NumOfInstLst-1} f_{inst\_j}) \wedge (F_{output}) \\
+&= (\bigwedge_{j=0}^{j=NumOfInstLst-1} f_{inst\_j}) \wedge (\bigwedge_{r_k = reg[ret_k]} (c \rightarrow r_k == output_i))
+\end{aligned}
+\end{equation}
+
+\begin{equation}
+F_{post} = (output_1 == output_2)
+\end{equation}
+\end{enumerate}
+
+\subsection{Algorithm}
+\begin{algorithm}
+\begin{algorithmic}[1]
+\caption{Equivalence\_Check}
+\REQUIRE $input$, $instLst_1$, $len_1$, $instLst_2$, $len_2$
+\ENSURE $isEqual$
+\STATE // pre-condition formula: $input_1 == input_2$
+\STATE $F_{pre_1} \Leftarrow true$
+\STATE $F_{pre_2} \Leftarrow true$
+\FOR{each value $\bm{rv}$ of register $\bm{i}$ in $input$}
+\STATE $F_{pre_1} \Leftarrow F_{pre_1} \wedge (rv == r_{i\_0\_0\_1})$
+\STATE $F_{pre_2} \Leftarrow F_{pre_2} \wedge (rv == r_{i\_0\_0\_2})$
+\ENDFOR{}
+\STATE // program logic formula: $F_1$, $F_2$
+\STATE $F_1, output_1 \Leftarrow SMT\_Prog(instLst_1, len_1)$
+\STATE $F_2, output_2 \Leftarrow SMT\_Prog(instLst_2, len_2)$
+\STATE // post-condition formula: $output_1 == output_2$
+\STATE $F_{post} \Leftarrow true$
+\FOR{$i=0$ to $len(output_1)$} 
+\STATE $F_{post} \Leftarrow F_{post} \wedge (output_{1\_i} == output_{2\_i})$
+\ENDFOR
+\STATE $F \Leftarrow F_{pre_1} \wedge F_{pre_2} \wedge F_1 \wedge F_2 \rightarrow F_{post} $
+\STATE $isEqual \Leftarrow Is\_Unsat(\neg F)$
+\RETURN $isEqual$
+\end{algorithmic}
+\end{algorithm}
+
+\section{Test set}
+\subsection{Program equivalence}
+\begin{enumerate}
+\item no branch
+\item branch: use more arithmetic and jmp instructions 
+\subitem with RET, 
+\subitem without RET
+\item illegal input
+\end{enumerate}
+\subsection{Specification check} 
+
+\begin{enumerate}
+\item Instruction specification: the range of register ID,...; \\done by candidate program generator?\\
+Now it is done by candidate program generator.
+\item Invalid instruction reach: Jmp instruction check; has done\\ 
+End instruction check  $\rightarrow$ Is the program is always ended with \textbf{RETs}? \\
+For now, only with registers, if no RET, return $r_0$  
+\item No loop
+\end{enumerate}
+
+\section{Data structure}
+\begin{lstlisting}[caption={}]
+class node {
+private:
+public:
+	unsigned int _start = 0; // start intruction ID
+	unsigned int _end = 0;   // end instruction ID
+};
+
+class graph {
+private:
+	vector<node> nodes;
+	vector<vector<unsigned int> > nodesIn;
+	vector<vector<unsigned int> > nodesOut;
+public:
+};
+
+class progSmt {
+private:
+	// f[i] is program logic FOL formula F of basic block i
+	vector<expr> f;
+	// postRegVal[i] is post register values of basic block i,
+	// which are initial values for NEXT basic blocks
+	vector<vector<expr> > postRegVal;
+	// pathCon[i] stores pre path conditions of basic block i
+	// There is a corresponding relationship between pathCon and g.nodesIn
+	// more specifically, pathCon[i][j] stores the pre path condition from basic block g.nodesIn[i][j] to i
+	vector<vector<expr> > pathCon;
+	// program FOL formula
+	expr smt = stringToExpr("true");
+	// program output FOL formula
+	expr smtOutput = stringToExpr("true");
+	// return the SMT for the given program
+	expr smtProg(inst* program, int length, smtVar* sv);
+	// return SMT for the given instruction
+	expr smtInst(smtVar* sv, inst* in);
+public:
+};
+\end{lstlisting}
+\end{document}