LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:sign_analysis_of_expressions_and_programs [2008/05/07 01:08]
vkuncak
sav08:sign_analysis_of_expressions_and_programs [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== Sign Analysis of Expressions and Programs ====== ====== Sign Analysis of Expressions and Programs ======
 +
  
 ===== Sign Analysis of Expressions ===== ===== Sign Analysis of Expressions =====
Line 6: Line 7:
  
 What is (quickly) the sign of What is (quickly) the sign of
-\[+\begin{equation*}
   (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))   (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))
-\]+\end{equation*}
 Why? Why?
 ++++| ++++|
-\[+\begin{equation*}
    (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos    (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos
-\]+\end{equation*}
 ++++ ++++
  
 What is (quickly) the sign of What is (quickly) the sign of
-\[+\begin{equation*}
     (28166461706 + (723497 \times (- 38931))) \times 42     (28166461706 + (723497 \times (- 38931))) \times 42
-\]+\end{equation*}
 ++++| ++++|
-\[+\begin{equation*}
    (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top    (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top
-\]+\end{equation*}
 ++++ ++++
  
Line 32: Line 33:
 Abstract domain: $A = \{ neg, nul, pos, \top \}$ Abstract domain: $A = \{ neg, nul, pos, \top \}$
  
-Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:+Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:\\ 
 +\\ 
 +$\begin{tabular}{ |c |c |c |c |c |c |} 
 +\hline \oplus & neg & nul & pos & \top \\ 
 +\hline ​ neg & neg & neg & \top & \top \\ 
 +\hline ​ nul & neg & nul & pos & \top \\ 
 +\hline pos & \top & pos & pos & \top \\ 
 +\hline \top & \top & \top & \top & \top \\ \hline 
 +\end{tabular} 
 +$\\ 
 +\\ 
 +$\begin{tabular}{ |c |c |c |c |c |c |} 
 +\hline \otimes & neg & nul & pos & \top \\ 
 +\hline ​ neg & pos & nul & neg & \top \\ 
 +\hline ​ nul & nul & nul & nul & nul \\ 
 +\hline pos & neg & nul & pos & \top \\ 
 +\hline \top & \top & nul & \top & \top \\ \hline 
 +\end{tabular} 
 +
  
 ===== Sign Analysis of Programs ===== ===== Sign Analysis of Programs =====
Line 52: Line 72:
 </​code>​ </​code>​
  
-Abstract state: map each variable to element of $A$.+Abstract state: map each variable to element of $A$. Here we have $|A|^3$ possible states.
  
   * computation over control-flow graph   * computation over control-flow graph