STP Documentation

From: vijay_ganesh Date: Tue, 11 Aug 2009 17:22:08 +0000 (+0000) Subject: git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1d40fd024506e5b7b444b6f48c243351522e2304;p=francis%2Fstp.git git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@110 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/web/stp-docs.html b/web/stp-docs.html deleted file mode 100644 index fa97ef6..0000000 --- a/web/stp-docs.html +++ /dev/null @@ -1,587 +0,0 @@ - - - - - - STP Documentation - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

- - - - - - - -

STP Main Page

STP Papers

Tools Using STP
-

STP_Documentation

-
-

Input Language of STP

Introduction

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.
-
-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.
-

The Input Langauge
-

Declarations
-

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:

x : BITVECTOR(32);

An example of an array declaration -is as -follows:

x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);

Functions -and Terms
-

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:

0bin0000111101010000, and the corresponding hex representation is 0hex0f50.

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.

The word level functions are:
-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Name -	Symbol -	Example -
Concatenation -	@ -	t1@t2@...@tm -
Extraction -	[i:j] -	x[31:26] -
left shift -	<< -	0bin0011 << 3 = -0bin0011000 -
right shift -	>> -	x[24:17] >> 5, -another -example: 0bin1000 >> 3 = 0bin0001
sign extension -	BVSX(bv,n) -	BVSX(0bin100, 5) = -0bin11100
Array READ -	[index] -	x_arr[t1] -
Array WRITE -	WITH -	x_arr WITH [index] := value -

For extraction terms, say t[i:j], n > i >= j >= 0, -where -n is the length of t.
For Left shift terms, t << k is equal to k 0's -appended to -t. The length of t << k is n+k.
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.

The -bitwise functions are:
-

-
-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Name -	Symbol -	Example -
Bitwise AND -	& -	t1 & t2 & ... -& tm -
Bitwise OR -	\| -	t1 \| t2 \| t3 \| ... \| tm -
Bitwise NOT -	~ -	~t1 -
Bitwise XOR -	BVXOR -	BVXOR(t1,t2) -
Bitwise NAND -	BVNAND -	BVNAND(t1,t2) -
Bitwise NOR -	BVNOR -	BVNOR(t1,t2) -
Bitwise XNOR -	BVXNOR -	BVXNOR(t1,t2) -

-
-

It is required that all the arguments of bitwise functions -have -the same length

- The arithmetic functions are:
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Name -	Symbol -	Example -
Bitvector Add -	BVPLUS -	BVPLUS(n,t1,t2,...,tm) -
Bitvector Mult -	BVMULT -	BVMULT(n,t1,t2) -
Bitvector subtract -	BVSUB -	BVSUB(n,t1,t2) -
Bitvector Unary Minus -	BVUMINUS -	BVUMINUS(t1) -
Bitvector Div -	BVDIV -	BVDIV(n,t1,t2), where t1 -is the -dividend and t2 is the divisor -
Signed Bitvector Div -	SBVDIV -	SBVDIV(n,t1,t2), where t1 -is the -dividend and t2 is the divisor
Bitvector Modulo -	BVMOD -	BVMOD(n,t1,t2), where t1 -is the -dividend and t2 is the divisor
Signed Bitvector Modulo -	SBVREM -	SBVREM(n,t1,t2), where t1 -is the -dividend and t2 is the divisor

the number of output bits has to specified (except unary -minus).
Inputs t1,t2 ...,tm must be of the same length
-
BVUMINUS(t) is a short-hand for BVPLUS(n,~t,0bin1), where n -is -the length of t.
Bitvector subtraction (BVSUB(n,t1,t2)) is a short-hand for -BVPLUS(n,t1,BVUMINUS(t2))

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:

x,y : BITVECTOR(1);
QUERY(x = IF 0bin0=x THEN y ELSE BVUMINUS(y));

Predicates
-

Following are the predicates -supported -by STP:
-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Name -	Symbol -	Example -
Equality -	= -	t1=t2 -
Less Than -	BVLT -	BVLT(t1,t2) -
Greater Than -	BVGT -	BVGT(t1,t2) -
Less Than Or Equal To -	BVLE -	BVLE(t1,t2) -
Greater Than Or Equal To -	BVGE -	BVGE(t1,t2) -
-	-	-
Signed Less Than -	SBVLT -	SBVLT(t1,t2) -
Signed Greater Than -	SBVGT -	SBVGT(t1,t2) -
Signed Less Than Or Equal -To -	SBVLE -	SBVLE(t1,t2) -
Signed Greater Than Or -Equal To -	SBVGE -	SBVGE(t1,t2) -

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.

Some -Examples

Example -1 -illustrates the use of arithmetic, word-level and bitwise -NOT operations:

x : BITVECTOR(5);
y : BITVECTOR(4);
yy : BITVECTOR(3);
QUERY(
 BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2]))   
);

Example -2 illustrates the use of arithmetic, word-level and -multiplexor terms:

bv : BITVECTOR(10);
a : BOOLEAN;
QUERY(
0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] 
AND 
0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)=(IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]
);

Example -3 -illustrates the use of bitwise operations:

x, y, z, t, q : BITVECTOR(1024);

ASSERT(x=~x);
ASSERT(x&y&t&z&q = x);
ASSERT(x|y = t);
ASSERT(BVXOR(x,~x)=t);
QUERY(FALSE);

Example -4 -illustrates the use of predicates and all the arithmetic -operations:

x, y : BITVECTOR(4);

ASSERT(x=0hex5);
ASSERT(y = 0bin0101);
QUERY(
BVMULT(8,x,y)=BVMULT(8,y,x)
AND
NOT(BVLT(x,y))
AND
BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
AND 
x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1))
);

Example -5 -illustrates the use of shift functions

x, y : BITVECTOR(8);
z, t : BITVECTOR(12);

ASSERT(x=0hexff);
ASSERT(z=0hexff0);
QUERY(z = x << 4);
QUERY((z >> 4)[7:0] = x);

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.

-
- - diff --git a/web/stp-papers.html b/web/stp-papers.html deleted file mode 100644 index e256e88..0000000 --- a/web/stp-papers.html +++ /dev/null @@ -1,118 +0,0 @@ - - - - - - STP Papers - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

- - - - - - - -

STP Main Page

STP Papers

Tools Using STP
-

STP_Documentation

-
-

STP Papers

A Decision Procedure for Bit-Vectors and Arrays by Vijay -Ganesh -and David L. Dill. In Proceedings of Computer Aided Verification 2007 -(CAV 2007), Berlin, Germany, July 2007 (pdf) (bib)

-
-

EXE: Automatically Generating Inputs of Death by Cristian -Cadar, -Vijay Ganesh, Peter Pawlowski, Dawson Engler, David Dill. In -Proceedings of ACM Conference on Computer and Communications Security -2006 (CCS 2006), Alexandria, Virginia, October, 2006 (pdf) -(bib)

-
-

-
- - diff --git a/web/stp-tools.html b/web/stp-tools.html deleted file mode 100644 index fcd15f5..0000000 --- a/web/stp-tools.html +++ /dev/null @@ -1,212 +0,0 @@ - - - - - - Tools Using STP - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

- - - - - - - -

STP Main Page

STP Papers

Tools Using STP
-

STP_Documentation

Projects that use STP

Bug Finding and Symbolic -Execution Tools

-
- -

EXE is a bug -finding tool that reads your C program and tries to automatically crash -it. EXE has been used to find bugs in TCP/IP Filters, Berkeley Packet -Filter, Linux Disks, PCRE library. This work is being done by -Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Prof. Dawson Engler and -Prof. David Dill at Stanford -University
-

-
-

MINESWEEPER -is a tool that automatically analyzes certain malicious behavior in -unix utilities and malware. This work is being done by Jim Newsome, -David -Brumley, Prof. Dawn Song and others at Carnegie -Mellon University (CMU)
-

-
-

CATCHCONV is a bug finding tool that tries to find bugs -due to -type mismatch in C programs. This work is being done by David Molnar -and Prof. David Wagner at University -of -California, Berkeley

-
-

Backward path-sensitive analysis of C programs to find -bugs by -Tim Leek from MIT Lincoln Labs

-
-

Bug finding in Verilog -code by a major microprocessor company

-
-

JPF-SE -is a symbolic execution extension to the Java PathFinder -model checker by Saswat Anand, Corina Pasareanu and Willem Visser from NASA Ames Research Center
-

-
-

Formal Verification Tools

-
- -

In conjunction with ACL2 to formally -verify implementation of encryption algorithms in Java by Eric W. Smith -and Prof. David Dill at Stanford -University
-

-
-

Formal verification of Parallel Transaction Architecture -by -Jacob -Chang and Prof. David Dill at Stanford -University
-

-
-

Tools For Finding Security -Exploits

-
-

REPLAYER is a -tool that replays an application dialog between two hosts in order to -find security exploits by Jim Newsome, David Brumley, Prof. Dawn Song -and others at Carnegie Mellon -University (CMU)

-
- - diff --git a/web/stp.html b/web/stp.html deleted file mode 100644 index c5345c7..0000000 --- a/web/stp.html +++ /dev/null @@ -1,124 +0,0 @@ - - - - - - STP - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

- - - - - - - -

Download

STP (accepts CVCL format) -: -Linux binary and library (last updated April 25, 2007)
STP.smt (accepts SMT format) -: -Linux binary
The c_interface.h file
The c_interface testcases -file
WARNING: PLEASE DO `ulimit -s unlimited` BEFORE RUNNING -STP. -OTHERWISE, THE YACC PARSER WILL SEGFAULT ON BIG EXAMPLES

STP Examples

These examples -were used for the CAV 2007 paper
-

Authors
-

-Vijay Ganesh and David L. Dill
- -

-
- - diff --git a/web/template.html b/web/template.html deleted file mode 100644 index 7bf534c..0000000 --- a/web/template.html +++ /dev/null @@ -1,100 +0,0 @@ - - - - - - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

- - - - - - - -

STP -

A Decision Procedure -for -Bitvectors and Arrays

Input Language of STP

Introduction

The Input Langauge -

Declarations -

Functions -and Terms -

Predicates -

Some -Examples

STP -

A Decision Procedure -for -Bitvectors and Arrays

STP Papers

STP -

A Decision Procedure -for -Bitvectors and Arrays

Projects that use STP

STP -

A Decision Procedure -for -Bitvectors and Arrays

Download

STP Examples

Authors -

STP -

A Decision Procedure -for -Bitvectors and Arrays

The Input Langauge
-

Declarations
-

Functions -and Terms
-

Predicates
-

Authors
-