<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<style>BODY, P, DIV, H1, H2, H3, H4, H5, H6, ADDRESS, OL, UL, LI, TITLE, TD, OPTION, SELECT
{
font-family: Verdana
}
BODY, P, DIV, ADDRESS, OL, UL, LI, TITLE, TD, OPTION, SELECT
{
font-size: 10.0pt;
margin-top:0pt;
margin-bottom:0pt;
}
BODY, P
{
margin-left:0pt;
margin-right:0pt;
}
BODY
{
background: white;
margin: 6px;
padding: 0px;
}
h6 { font-size: 10pt }
h5 { font-size: 11pt }
h4 { font-size: 12pt }
h3 { font-size: 13pt }
h2 { font-size: 14pt }
h1 { font-size: 16pt }
blockquote { padding: 10px; border: 1px #DDDDDD dashed }
a img { border: 0; }
table.zeroBorder {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
table.zeroBorder th {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
table.zeroBorder td {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
.hiddenStyle {
visibility: hidden;
position: absolute;
z-Index: 1;
paddingRight: 0;
background: white
}
.misspell { background-image: url('/images/misspell.gif'); background-repeat: repeat-x; background-position: bottom }
@media screen {
.pb { border-top: 1px dashed #C0C0C0; border-bottom: 1px dashed #C0C0C0 }
.writely-comment { font-size: 9pt; line-height: 1.4em; padding: 1px; border: 1px dashed #C0C0C0 }
}
@media print {
.pb { border-top: 0px; border-bottom: 0px }
.writely-comment { display: none }
}
@media screen,print {
.pb { height: 1px }
}
</style>
<title>STP Documentation</title>
</head>
<body revision="ddvbwkf4_12dp5n4m:8">
<h2 style="text-align: center; color: rgb(153, 0, 0);"><big><big> <font
size="5"><big><big>STP</big></big></font>
</big></big></h2>
<div style="text-align: center; color: rgb(153, 0, 0);">
<h2><font style="color: rgb(153, 0, 0);" size="5">A Decision Procedure
for
Bitvectors and Arrays</font></h2>
</div>
<table style="text-align: left;" border="0" cellpadding="10"
cellspacing="20">
<tbody>
<tr>
<td style="vertical-align: top; text-align: left;">
<h4><a href="stp.html">STP Main Page</a></h4>
<h4><a href="stp-papers.html">STP Papers</a></h4>
<h4><a href="stp-tools.html">Tools Using STP<br>
</a></h4>
<h4><a href="stp-docs.html">STP_Documentation</a></h4>
<br>
</td>
<td style="vertical-align: top;">
<h2 style="color: rgb(102, 102, 0);">Input Language of STP</h2>
<h3>Introduction</h3>
<p>STP is an efficient decision procedure for the validity (or
satisfiability) of formulas from a quantifier-free many-sorted theory
of fixed-width bitvectors and (non-extensional) one-dimensional arrays.
The functions in STP's input language include concatenation,
extraction, left/right shift, sign-extension, unary minus, addition,
multiplication, (signed) modulo/division, bitwise Boolean operations,
if-then-else terms, and array reads and writes. The predicates in the
language include equality and (signed) comparators between bitvector
terms.<br>
<br>
The basic architecture of STP essentially follows the idea of
word-level preprocessing followed by translation to SAT (We use
MINISAT). In particular, we introduce several new heuristics for the
preprocessing step, including abstraction-refinement in the context of
arrays, a new bitvector linear arithmetic equation solver, and some
interesting simplifications. These heuristics help us acheive several
magnitudes of order performance over other tools, and also over
straight-forward translation to SAT. STP has been heavily tested on
thousands of examples sourced from various real-world applications such
as program analysis and bug-finding tools like EXE, and equivalence
checking tools and theorem-provers. <br>
</p>
<h3>The Input Langauge<br>
</h3>
<h4 style="margin-left: 40px;">Declarations<br>
</h4>
<div style="margin-left: 40px;">Bit-vector expressions (or terms)
are
constructed out of bit-vector
constants, bit-vector variables and the functions listed below. In STP
all variables have to declared before the point of use. An example
declaration of a bit-vector variable of length, say 32, is as follows: </div>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">x : BITVECTOR(32);<br></pre>
</div>
<p style="margin-left: 40px;">An example of an array declaration
is as
follows:</p>
<pre style="margin-left: 40px;" class="fragment">x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);<br><br></pre>
<h4 style="margin-left: 40px;">Functions
and Terms<br>
</h4>
<p style="margin-left: 40px;">Bit-vector variables (or terms) of
length
0 are not allowed.
Bit-vector
constants can be represented in binary or hexadecimal format. The
rightmost bit is called the least significant bit (LSB), and the
leftmost bit is the most significant bit(MSB). The index of the LSB is
0, and the index of the MSB is n-1 for an n-bit constant. This
convention naturally extends to all bit-vector expressions. Following
are some examples of bit-vector constants:</p>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">0bin0000111101010000, and the corresponding hex representation is 0hex0f50.<br></pre>
</div>
<p style="margin-left: 40px;">The Bit-vector implementation in
STP
supports a very large number
of functions and predicates. The functions are categorized into
word-level functions, bitwise functions, and arithmetic functions. Let
t1,t2,...,tm denote some arbitrary bitvector terms<span
style="font-family: mon;"><span style="font-weight: bold;">. </span></span></p>
<p style="margin-left: 40px;"><span style="font-family: mon;"><span
style="font-weight: bold;"></span></span><span
style="font-weight: bold;">The word level functions are:</span><br>
</p>
<div style="margin-left: 40px;" class="fragment">
<table style="text-align: left; width: 680px; height: 316px;"
border="1" cellpadding="2" cellspacing="2">
<tbody>
<tr>
<td style="vertical-align: top;">Name<br>
</td>
<td style="vertical-align: top;">Symbol<br>
</td>
<td style="vertical-align: top;">Example<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Concatenation<br>
</td>
<td style="vertical-align: top;">@<br>
</td>
<td style="vertical-align: top;">t1@t2@...@tm<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Extraction<br>
</td>
<td style="vertical-align: top;">[i:j]<br>
</td>
<td style="vertical-align: top;">x[31:26]<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">left shift<br>
</td>
<td style="vertical-align: top;"><<<br>
</td>
<td style="vertical-align: top;">0bin0011 << 3 =
0bin0011000<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">right shift<br>
</td>
<td style="vertical-align: top;">>><br>
</td>
<td style="vertical-align: top;">x[24:17] >> 5,
another
example: 0bin1000 >> 3 = 0bin0001</td>
</tr>
<tr>
<td style="vertical-align: top;">sign extension<br>
</td>
<td style="vertical-align: top;">BVSX(bv,n)<br>
</td>
<td style="vertical-align: top;">BVSX(0bin100, 5) =
0bin11100</td>
</tr>
<tr>
<td style="vertical-align: top;">Array READ<br>
</td>
<td style="vertical-align: top;">[index]<br>
</td>
<td style="vertical-align: top;">x_arr[t1]<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Array WRITE<br>
</td>
<td style="vertical-align: top;">WITH<br>
</td>
<td style="vertical-align: top;">x_arr WITH [index] := value<br>
</td>
</tr>
</tbody>
</table>
</div>
<ul style="margin-left: 40px;">
<li>For extraction terms, say t[i:j], n > i >= j >= 0,
where
n is the length of t.</li>
<li>For Left shift terms, t << k is equal to k 0's
appended to
t. The length of t << k is n+k.</li>
<li>for
Right shift terms, say t >> k, the term is equal to the bitvector
obtained by k 0's followed by t[n-1:k]. The length of t >> k is n.</li>
</ul>
<div style="margin-left: 40px;"><span style="font-weight: bold;">The
bitwise functions are:</span><br style="font-weight: bold;">
</div>
<br>
<div style="margin-left: 40px;">
<table style="text-align: left; width: 684px; height: 242px;"
border="1" cellpadding="2" cellspacing="2">
<tbody>
<tr>
<td style="vertical-align: top;">Name<br>
</td>
<td style="vertical-align: top;">Symbol<br>
</td>
<td style="vertical-align: top;">Example<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise AND<br>
</td>
<td style="vertical-align: top;">&<br>
</td>
<td style="vertical-align: top;">t1 & t2 & ...
& tm<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise OR<br>
</td>
<td style="vertical-align: top;">|<br>
</td>
<td style="vertical-align: top;">t1 | t2 | t3 | ... | tm<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise NOT<br>
</td>
<td style="vertical-align: top;">~<br>
</td>
<td style="vertical-align: top;">~t1<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise XOR<br>
</td>
<td style="vertical-align: top;">BVXOR<br>
</td>
<td style="vertical-align: top;">BVXOR(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise NAND<br>
</td>
<td style="vertical-align: top;">BVNAND<br>
</td>
<td style="vertical-align: top;">BVNAND(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise NOR<br>
</td>
<td style="vertical-align: top;">BVNOR<br>
</td>
<td style="vertical-align: top;">BVNOR(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitwise XNOR<br>
</td>
<td style="vertical-align: top;">BVXNOR<br>
</td>
<td style="vertical-align: top;">BVXNOR(t1,t2)<br>
</td>
</tr>
</tbody>
</table>
<br>
<ul>
<li>It is required that all the arguments of bitwise functions
have
the same length</li>
</ul>
<span style="font-weight: bold;">The arithmetic functions are:<br>
</span>
<table style="text-align: left; width: 692px; height: 314px;"
border="1" cellpadding="2" cellspacing="2">
<tbody>
<tr>
<td style="vertical-align: top;">Name<br>
</td>
<td style="vertical-align: top;">Symbol<br>
</td>
<td style="vertical-align: top;">Example<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector Add<br>
</td>
<td style="vertical-align: top;">BVPLUS<br>
</td>
<td style="vertical-align: top;">BVPLUS(n,t1,t2,...,tm)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector Mult<br>
</td>
<td style="vertical-align: top;">BVMULT<br>
</td>
<td style="vertical-align: top;">BVMULT(n,t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector subtract<br>
</td>
<td style="vertical-align: top;">BVSUB<br>
</td>
<td style="vertical-align: top;">BVSUB(n,t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector Unary Minus<br>
</td>
<td style="vertical-align: top;">BVUMINUS<br>
</td>
<td style="vertical-align: top;">BVUMINUS(t1)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector Div<br>
</td>
<td style="vertical-align: top;">BVDIV<br>
</td>
<td style="vertical-align: top;">BVDIV(n,t1,t2), where t1
is the
dividend and t2 is the divisor<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Bitvector Div<br>
</td>
<td style="vertical-align: top;">SBVDIV<br>
</td>
<td style="vertical-align: top;">SBVDIV(n,t1,t2), where t1
is the
dividend and t2 is the divisor</td>
</tr>
<tr>
<td style="vertical-align: top;">Bitvector Modulo<br>
</td>
<td style="vertical-align: top;">BVMOD<br>
</td>
<td style="vertical-align: top;">BVMOD(n,t1,t2), where t1
is the
dividend and t2 is the divisor</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Bitvector Modulo<br>
</td>
<td style="vertical-align: top;">SBVREM<br>
</td>
<td style="vertical-align: top;">SBVREM(n,t1,t2), where t1
is the
dividend and t2 is the divisor</td>
</tr>
</tbody>
</table>
<span style="font-weight: bold;"></span></div>
<ul style="margin-left: 40px;">
<li>the number of output bits has to specified (except unary
minus).</li>
<li>Inputs t1,t2 ...,tm must be of the same length<br>
</li>
<li>BVUMINUS(t) is a short-hand for BVPLUS(n,~t,0bin1), where n
is
the length of t.</li>
<li>Bitvector subtraction (BVSUB(n,t1,t2)) is a short-hand for
BVPLUS(n,t1,BVUMINUS(t2))</li>
</ul>
<p style="margin-left: 40px;">STP also supports conditional terms
(IF cond THEN t1 ELSE t2
ENDIF), where cond is boolean term, t1 and t2 can be bitvector terms.
This allows us to simulate multiplexors. An example is:</p>
<div class="fragment">
<pre style="margin-left: 40px;" class="fragment">x,y : BITVECTOR(1);<br>QUERY(x = IF 0bin0=x THEN y ELSE BVUMINUS(y));<br></pre>
</div>
<h4 style="margin-left: 40px;">Predicates<br>
</h4>
<div class="fragment">
<div style="margin-left: 40px;">Following are the predicates
supported
by STP:<br>
</div>
<div style="margin-left: 40px;"><br>
</div>
<table
style="text-align: left; width: 676px; height: 390px; margin-left: 40px;"
border="1" cellpadding="2" cellspacing="2">
<tbody>
<tr>
<td style="vertical-align: top;">Name<br>
</td>
<td style="vertical-align: top;">Symbol<br>
</td>
<td style="vertical-align: top;">Example<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Equality<br>
</td>
<td style="vertical-align: top;">=<br>
</td>
<td style="vertical-align: top;">t1=t2<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Less Than<br>
</td>
<td style="vertical-align: top;">BVLT<br>
</td>
<td style="vertical-align: top;">BVLT(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Greater Than<br>
</td>
<td style="vertical-align: top;">BVGT<br>
</td>
<td style="vertical-align: top;">BVGT(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Less Than Or Equal To<br>
</td>
<td style="vertical-align: top;">BVLE<br>
</td>
<td style="vertical-align: top;">BVLE(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Greater Than Or Equal To<br>
</td>
<td style="vertical-align: top;">BVGE<br>
</td>
<td style="vertical-align: top;">BVGE(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;"><br>
</td>
<td style="vertical-align: top;"><br>
</td>
<td style="vertical-align: top;"><br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Less Than<br>
</td>
<td style="vertical-align: top;">SBVLT<br>
</td>
<td style="vertical-align: top;">SBVLT(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Greater Than<br>
</td>
<td style="vertical-align: top;">SBVGT<br>
</td>
<td style="vertical-align: top;">SBVGT(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Less Than Or Equal
To<br>
</td>
<td style="vertical-align: top;">SBVLE<br>
</td>
<td style="vertical-align: top;">SBVLE(t1,t2)<br>
</td>
</tr>
<tr>
<td style="vertical-align: top;">Signed Greater Than Or
Equal To<br>
</td>
<td style="vertical-align: top;">SBVGE<br>
</td>
<td style="vertical-align: top;">SBVGE(t1,t2)<br>
</td>
</tr>
</tbody>
</table>
<div style="margin-left: 40px;">
<ul>
<li>STP requires that in atomic formulas such
as x=y, x and y are expressions of the same length. STP accepts Boolean
combination of atomic formulas.</li>
</ul>
</div>
<h3>Some
Examples</h3>
</div>
<p style="margin-left: 40px;"><span style="font-weight: bold;">Example
1</span>
illustrates the use of arithmetic, word-level and bitwise
NOT operations:</p>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">x : BITVECTOR(5);<br>y : BITVECTOR(4);<br>yy : BITVECTOR(3);<br>QUERY(<br> BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) <br>);<br></pre>
</div>
<p style="margin-left: 40px;"><span style="font-weight: bold;">Example
2 </span>illustrates the use of arithmetic, word-level and
multiplexor terms:</p>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">bv : BITVECTOR(10);<br>a : BOOLEAN;<br>QUERY(<br>0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] <br>AND <br>0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)=(IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]<br>);<br></pre>
</div>
<p style="margin-left: 40px;"><span style="font-weight: bold;">Example
3</span>
illustrates the use of bitwise operations:</p>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">x, y, z, t, q : BITVECTOR(1024);<br><br>ASSERT(x=~x);<br>ASSERT(x&y&t&z&q = x);<br>ASSERT(x|y = t);<br>ASSERT(BVXOR(x,~x)=t);<br>QUERY(FALSE);<br></pre>
</div>
<p style="margin-left: 40px;"><span style="font-weight: bold;">Example
4</span>
illustrates the use of predicates and all the arithmetic
operations:</p>
<div style="margin-left: 40px;" class="fragment">
<pre class="fragment">x, y : BITVECTOR(4);<br><br>ASSERT(x=0hex5);<br>ASSERT(y = 0bin0101);<br>QUERY(<br>BVMULT(8,x,y)=BVMULT(8,y,x)<br>AND<br>NOT(BVLT(x,y))<br>AND<br>BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))<br>AND <br>x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1))<br>);<br></pre>
</div>
<p style="margin-left: 40px;"><span style="font-weight: bold;">Example
5</span>
illustrates the use of shift functions</p>
<div class="fragment">
<pre style="margin-left: 40px;" class="fragment">x, y : BITVECTOR(8);<br>z, t : BITVECTOR(12);<br><br>ASSERT(x=0hexff);<br>ASSERT(z=0hexff0);<br>QUERY(z = x << 4);<br>QUERY((z >> 4)[7:0] = x);<br><br></pre>
</div>
<p>For invalid inputs, the COUNTEREXAMPLE command can be used to
generate
appropriate counterexamples. The generated counter example is
essentially a bitwise assignment to the variables in the input.</p>
<div style="margin-left: 40px;"> </div>
</td>
</tr>
</tbody>
</table>
<a href="#stp"></a><br>
</body>
</html>
distrib
>
Fedora
>
14
>
x86_64
>
media
>
os
>
by-pkgid
>
e4284596e3656e403aa4a54f4fcd0ae3
>
files
>
9
