Commit 4d1dc5d4 authored by Cristian Cadar's avatar Cristian Cadar Committed by Daniel Liew
Browse files

Forgot to remove the actual stp directory.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8
parent a98690d5
This diff is collapsed.
This diff is collapsed.
// Generated automatically by genkinds.h from ASTKind.kinds Sun Apr 4 19:39:09 2010.
// Do not edit
namespace BEEV {
const char * _kind_names[] = {
"UNDEFINED",
"SYMBOL",
"BVCONST",
"BVNEG",
"BVCONCAT",
"BVOR",
"BVAND",
"BVXOR",
"BVNAND",
"BVNOR",
"BVXNOR",
"BVEXTRACT",
"BVLEFTSHIFT",
"BVRIGHTSHIFT",
"BVSRSHIFT",
"BVVARSHIFT",
"BVPLUS",
"BVSUB",
"BVUMINUS",
"BVMULTINVERSE",
"BVMULT",
"BVDIV",
"BVMOD",
"SBVDIV",
"SBVMOD",
"BVSX",
"BOOLVEC",
"ITE",
"BVGETBIT",
"BVLT",
"BVLE",
"BVGT",
"BVGE",
"BVSLT",
"BVSLE",
"BVSGT",
"BVSGE",
"EQ",
"NEQ",
"FALSE",
"TRUE",
"NOT",
"AND",
"OR",
"NAND",
"NOR",
"XOR",
"IFF",
"IMPLIES",
"READ",
"WRITE",
"ARRAY",
"BITVECTOR",
"BOOLEAN",
};
unsigned char _kind_categories[] = {
0,
3,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
3,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
2,
1,
1,
0,
0,
0,
};
} // end namespace
// -*- c++ -*-
#ifndef TESTKINDS_H
#define TESTKINDS_H
// Generated automatically by genkinds.pl from ASTKind.kinds Sun Apr 4 19:39:09 2010.
// Do not edit
namespace BEEV {
typedef enum {
UNDEFINED,
SYMBOL,
BVCONST,
BVNEG,
BVCONCAT,
BVOR,
BVAND,
BVXOR,
BVNAND,
BVNOR,
BVXNOR,
BVEXTRACT,
BVLEFTSHIFT,
BVRIGHTSHIFT,
BVSRSHIFT,
BVVARSHIFT,
BVPLUS,
BVSUB,
BVUMINUS,
BVMULTINVERSE,
BVMULT,
BVDIV,
BVMOD,
SBVDIV,
SBVMOD,
BVSX,
BOOLVEC,
ITE,
BVGETBIT,
BVLT,
BVLE,
BVGT,
BVGE,
BVSLT,
BVSLE,
BVSGT,
BVSGE,
EQ,
NEQ,
FALSE,
TRUE,
NOT,
AND,
OR,
NAND,
NOR,
XOR,
IFF,
IMPLIES,
READ,
WRITE,
ARRAY,
BITVECTOR,
BOOLEAN
} Kind;
extern unsigned char _kind_categories[];
inline bool is_Term_kind(Kind k) { return (_kind_categories[k] & 1); }
inline bool is_Form_kind(Kind k) { return (_kind_categories[k] & 2); }
extern const char *_kind_names[];
/** Prints symbolic name of kind */
inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }
} // end namespace
#endif
#Please refer LICENSE FILE in the home directory for licensing information
# name minkids maxkids cat1 cat2 ...
Categories: Term Form
# Leaf nodes.
UNDEFINED 0 0
SYMBOL 0 0 Term Form
# These always produce terms
BVCONST 0 0 Term
BVNEG 1 1 Term
BVCONCAT 2 - Term
BVOR 1 - Term
BVAND 1 - Term
BVXOR 1 - Term
BVNAND 1 - Term
BVNOR 1 - Term
BVXNOR 1 - Term
BVEXTRACT 3 3 Term
BVLEFTSHIFT 3 3 Term
BVRIGHTSHIFT 3 3 Term
BVSRSHIFT 3 3 Term
BVVARSHIFT 3 3 Term
BVPLUS 1 - Term
BVSUB 2 2 Term
BVUMINUS 1 1 Term
BVMULTINVERSE 1 1 Term
BVMULT 1 - Term
BVDIV 2 2 Term
BVMOD 2 2 Term
SBVDIV 2 2 Term
SBVMOD 2 2 Term
BVSX 1 1 Term
BOOLVEC 0 - Term
# Formula OR term, depending on context
ITE 3 3 Term Form
# These produce formulas.
BVGETBIT 2 2 Form
BVLT 2 2 Form
BVLE 2 2 Form
BVGT 2 2 Form
BVGE 2 2 Form
BVSLT 2 2 Form
BVSLE 2 2 Form
BVSGT 2 2 Form
BVSGE 2 2 Form
EQ 2 2 Form
NEQ 2 2 Form
FALSE 0 0 Form
TRUE 0 0 Form
NOT 1 1 Form
AND 1 - Form
OR 1 - Form
NAND 1 - Form
NOR 1 - Form
XOR 1 - Form
IFF 1 - Form
IMPLIES 2 2 Form
# array operations
READ 2 2 Term
WRITE 3 3 Term
#Types: These kinds are used only in the API. Once processed inside
#the API, they are never used again in the system
ARRAY 0 0
BITVECTOR 0 0
BOOLEAN 0 0
/********************************************************************
* AUTHORS: Vijay Ganesh, David L. Dill
*
* BEGIN DATE: November, 2005
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
// -*- c++ -*-
#include "ASTUtil.h"
#include <ostream>
namespace BEEV {
ostream &operator<<(ostream &os, const Spacer &sp) {
// Instead of wrapping lines with hundreds of spaces, prints
// a "+" at the beginning of the line for each wrap-around.
// so lines print like: +14+ (XOR ...
int blanks = sp._spaces % 60;
int wraps = sp._spaces / 60;
if (wraps > 0) {
os << "+" << wraps;
}
for (int i = 0; i < blanks; i++)
os << " ";
return os;
}
//this function accepts the name of a function (as a char *), and
//records some stats about it. if the input is "print_func_stats",
//the function will then print the stats that it has collected.
void CountersAndStats(const char * functionname) {
if(!stats)
return;
static function_counters s;
if(!strcmp(functionname,"print_func_stats")) {
cout << endl;
for(hash_map<const char*,int,hash<const char*>,eqstr>::iterator it=s.begin(),itend=s.end();
it!=itend;it++)
cout << "Number of times the function: " << it->first << ": is called: " << it->second << endl;
return;
}
s[functionname] += 1;
}
} // end of namespace
/********************************************************************
* AUTHORS: Vijay Ganesh, David L. Dill
*
* BEGIN DATE: November, 2005
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
// -*- c++ -*-
#ifndef ASTUTIL_H
#define ASTUTIL_H
#include <cstring>
#include <iostream>
#include <vector>
#ifdef EXT_HASH_MAP
#include <ext/hash_set>
#include <ext/hash_map>
#else
#include <hash_set>
#include <hash_map>
#endif
using namespace std;
namespace BEEV {
#ifdef EXT_HASH_MAP
using namespace __gnu_cxx;
#endif
//some global variables that are set through commandline options. it
//is best that these variables remain global. Default values set
//here
//
//collect statistics on certain functions
extern bool stats;
//print DAG nodes
extern bool print_nodes;
//tentative global var to allow for variable activity optimization
//in the SAT solver. deprecated.
extern bool variable_activity_optimize;
//run STP in optimized mode
extern bool optimize;
//do sat refinement, i.e. underconstraint the problem, and feed to
//SAT. if this works, great. else, add a set of suitable constraints
//to re-constraint the problem correctly, and call SAT again, until
//all constraints have been added.
extern bool arrayread_refinement;
//switch to control write refinements
extern bool arraywrite_refinement;
//check the counterexample against the original input to STP
extern bool check_counterexample;
//construct the counterexample in terms of original variable based
//on the counterexample returned by SAT solver
extern bool construct_counterexample;
extern bool print_counterexample;
//if this option is true then print the way dawson wants using a
//different printer. do not use this printer.
extern bool print_arrayval_declaredorder;
//flag to decide whether to print "valid/invalid" or not
extern bool print_output;
//do linear search in the array values of an input array. experimental
extern bool linear_search;
//print the variable order chosen by the sat solver while it is
//solving.
extern bool print_sat_varorder;
//turn on word level bitvector solver
extern bool wordlevel_solve;
//XOR flattening optimizations.
extern bool xor_flatten;
//this flag indicates that the BVSolver() succeeded
extern bool toplevel_solved;
//the smtlib parser has been turned on
extern bool smtlib_parser_enable;
//print the input back
extern bool print_STPinput_back;
extern void (*vc_error_hdlr)(const char* err_msg);
/*Spacer class is basically just an int, but the new class allows
overloading of << with a special definition that prints the int as
that many spaces. */
class Spacer {
public:
int _spaces;
Spacer(int spaces) { _spaces = spaces; }
friend ostream& operator<<(ostream& os, const Spacer &ind);
};
inline Spacer spaces(int width) {
Spacer sp(width);
return sp;
}
struct eqstr {
bool operator()(const char* s1, const char* s2) const {
return strcmp(s1, s2) == 0;
}
};
typedef hash_map<const char*,int,
hash<const char *>,eqstr> function_counters;
void CountersAndStats(const char * functionname);
//global function which accepts an integer and looks up the
//corresponding ASTNode and prints a char* of that ASTNode
void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
int decision, int polarity=0);
} // end namespace.
#endif
This diff is collapsed.
#===-- stp/AST/Makefile ------------------------------------*- Makefile -*--===#
#
# The KLEE Symbolic Virtual Machine
#
# This file is distributed under the University of Illinois Open Source
# License. See LICENSE.TXT for details.
#
#===------------------------------------------------------------------------===#
LEVEL=../..
LIBRARYNAME=stp_AST
DONT_BUILD_RELINKED=1
BUILD_ARCHIVE=1
include $(LEVEL)/Makefile.common
# HACK: Force -Wno-deprecated for ext container use.
CXX.Flags += -Wno-deprecated
/********************************************************************
* AUTHORS: Vijay Ganesh, David L. Dill
*
* BEGIN DATE: November, 2005
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
// -*- c++ -*-
// STLport debug checking, if we use STLport threads flag is to get
// rid of link errors, since iostreams compiles with threads. alloc
// and uninitialized are extra checks Later on, if used with Purify or
// Valgrind, may want to set flags to prevent reporting of false
// leaks. For some reason, _STLP_THREADS works on the command line
// but not here (?)
#define _STLP_THREADS
#define _STLP_DEBUG 1
#define _STLP_DEBUG_LEVEL _STLP_STANDARD_DBG_LEVEL
#define _STLP_DEBUG_ALLOC 1
#define _STLP_DEBUG_UNINITIALIZED 1
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
#!/usr/bin/perl -w
#AUTHORS: Vijay Ganesh, David L. Dill BEGIN DATE: November, 2005
#LICENSE: Please view LICENSE file in the home dir of this Program
#given a file containing kind names, one per line produces .h and .cpp
#files for the kinds.
#globals
@kindnames = ();
$minkids = 0;
$maxkids = 0;
@cat_bits = ();
@category_names = ();
%cat_index = ();
$now = localtime time;
sub read_kind_defs {
open(KFILE, "< ASTKind.kinds") || die "Cannot open .kinds file: $!\n";
@kindlines = <KFILE>;
close(KFILE)
}
# create lists of things indexed by kinds.
sub split_fields {
my $kind_cat_bits;
# matches anything with three whitespace-delimited alphanumeric fields,
# followed by rest of line. Automatically ignores lines beginning with '#' and blank lines.
for (@kindlines) {
if (/Categories:\s+(.*)/) {
@category_names = split(/\s+/, $1);
$i = 0;
for (@category_names) {
$cat_index{$_} = $i++;
# print "cat_index{$_} = $i\n";
}
}
elsif (/^(\w+)\s+(\w+)\s+(\w+|-)\s+(.*)/) {
push(@kindnames, $1);
push(@minkids, $2);
push(@maxkids, $3);
@kind_cats = split(/\s+/, $4);
# build a bit vector of categories.
$kind_cat_bits = 0;
for (@kind_cats) {
$kind_cat_bits |= (1 << int($cat_index{$_}));
}
push(@cat_bits, $kind_cat_bits);
}
}
}
sub gen_h_file {
open(HFILE, "> ASTKind.h") || die "Cannot open .h file: $!\n";
print HFILE
"// -*- c++ -*-\n",
"#ifndef TESTKINDS_H\n",
"#define TESTKINDS_H\n",
"// Generated automatically by genkinds.pl from ASTKind.kinds $now.\n",
"// Do not edit\n",
"namespace BEEV {\n typedef enum {\n";
for (@kindnames) {
print HFILE " $_,\n";
}
print HFILE
"} Kind;\n\n",
"extern unsigned char _kind_categories[];\n\n";
# For category named "cat", generate functions "bool is_cat_kind(k);"
for (@category_names) {
my $catname = $_;
my $kind_cat_bit = (1 << int($cat_index{$catname}));
print HFILE "inline bool is_", $catname, "_kind(Kind k) { return (_kind_categories[k] & $kind_cat_bit); }\n\n"
}
print HFILE
"extern const char *_kind_names[];\n\n",
"/** Prints symbolic name of kind */\n",
"inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n",
"\n\n",
"} // end namespace\n",
"\n\n#endif\n";
close(HFILE);
}
# generate the .cpp file
sub gen_cpp_file {
open(CPPFILE, "> ASTKind.cpp") || die "Cannot open .h file: $!\n";
print CPPFILE
"// Generated automatically by genkinds.h from ASTKind.kinds $now.\n",
"// Do not edit\n",
"namespace BEEV {\n",
"const char * _kind_names[] = {\n";
for (@kindnames) {
print CPPFILE " \"$_\",\n";
}
print CPPFILE "};\n\n";
# category bits
print CPPFILE
"unsigned char _kind_categories[] = {\n";
for (@cat_bits) {
print CPPFILE " $_,\n";
}
print CPPFILE
"};\n",
"\n} // end namespace\n";
close(CPPFILE);
}
&read_kind_defs;
&split_fields;
&gen_h_file;
&gen_cpp_file;
1. To install STP perform the following steps on your Unix/GNU-Linux/MacOS X commandline:
./configure --with-prefix=$HOME (or another installation directory)
make clean
make
make install
2. To test the system after installation:
make regressall
\ No newline at end of file
/*****************************************************************************/
/* AUTHORS: Vijay Ganesh, David L. Dill DATE: Nov 2005 */
/*****************************************************************************/
/* Copyright (C) 2005 by the Board of Trustees of Leland Stanford */
/* Junior University. */
/* */
/* License to use, copy, modify, sell and/or distribute this software */
/* and its documentation for any purpose is hereby granted without */
/* royalty, subject to the terms and conditions defined in the \ref */
/* LICENSE file provided with this distribution. In particular: */
/* */
/* - The above copyright notice and this permission notice must appear */
/* in all copies of the software and related documentation. */
/* */
/* - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, */
/* EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. */
/*****************************************************************************/
#===-- stp/Makefile ----------------------------------------*- Makefile -*--===#
#