diff options
Diffstat (limited to 'stp/c_interface')
| -rw-r--r-- | stp/c_interface/Makefile | 19 | ||||
| -rw-r--r-- | stp/c_interface/c_interface.cpp | 1548 | ||||
| -rw-r--r-- | stp/c_interface/c_interface.h | 401 | ||||
| -rw-r--r-- | stp/c_interface/fdstream.h | 186 |
4 files changed, 0 insertions, 2154 deletions
diff --git a/stp/c_interface/Makefile b/stp/c_interface/Makefile deleted file mode 100644 index 29b9006b..00000000 --- a/stp/c_interface/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -#===-- stp/c_interface/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_c_interface -DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 - -include $(LEVEL)/Makefile.common - -# HACK: Force -Wno-deprecated for ext container use. -CXX.Flags += -Wno-deprecated diff --git a/stp/c_interface/c_interface.cpp b/stp/c_interface/c_interface.cpp deleted file mode 100644 index 52c4df21..00000000 --- a/stp/c_interface/c_interface.cpp +++ /dev/null @@ -1,1548 +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 "c_interface.h" - -#include <cstdlib> -#include <cassert> -#include <ostream> -#include <iostream> -#include "fdstream.h" -#include "../AST/AST.h" - -//These typedefs lower the effort of using the keyboard to type (too -//many overloaded meanings of the word type) -typedef BEEV::ASTNode node; -typedef BEEV::ASTNode* nodestar; -typedef BEEV::BeevMgr* bmstar; -typedef BEEV::ASTVec nodelist; -typedef BEEV::CompleteCounterExample* CompleteCEStar; -BEEV::ASTVec *decls = NULL; -//vector<BEEV::ASTNode *> created_exprs; -bool cinterface_exprdelete_on = false; - -void vc_setFlags(char c) { - std::string helpstring = "Usage: stp [-option] [infile]\n\n"; - helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; - helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; - helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; - helpstring += "-s : print function statistics\n"; - helpstring += "-v : print nodes \n"; - helpstring += "-c : construct counterexample\n"; - helpstring += "-d : check counterexample\n"; - helpstring += "-p : print counterexample\n"; - helpstring += "-h : help\n"; - - switch(c) { - case 'a' : - BEEV::optimize = false; - BEEV::wordlevel_solve = false; - break; - case 'b': - BEEV::print_STPinput_back = true; - break; - case 'c': - BEEV::construct_counterexample = true; - break; - case 'd': - BEEV::construct_counterexample = true; - BEEV::check_counterexample = true; - break; - case 'e': - BEEV::variable_activity_optimize = true; - break; - case 'f': - BEEV::smtlib_parser_enable = true; - break; - case 'h': - cout << helpstring; - BEEV::FatalError(""); - break; - case 'l' : - BEEV::linear_search = true; - break; - case 'n': - BEEV::print_output = true; - break; - case 'p': - BEEV::print_counterexample = true; - break; - case 'q': - BEEV::print_arrayval_declaredorder = true; - break; - case 'r': - BEEV::arrayread_refinement = false; - break; - case 's' : - BEEV::stats = true; - break; - case 'u': - BEEV::arraywrite_refinement = true; - break; - case 'v' : - BEEV::print_nodes = true; - break; - case 'w': - BEEV::wordlevel_solve = false; - break; - case 'x': - cinterface_exprdelete_on = true; - break; - case 'z': - BEEV::print_sat_varorder = true; - break; - default: - std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n"; - s += helpstring; - BEEV::FatalError(s.c_str()); - break; - } -} - -//Create a validity Checker. This is the global BeevMgr -VC vc_createValidityChecker(void) { - vc_setFlags('d'); -#ifdef NATIVE_C_ARITH -#else - CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); - if(0 != c) { - cout << CONSTANTBV::BitVector_Error(c) << endl; - return 0; - } -#endif - bmstar bm = new BEEV::BeevMgr(); - decls = new BEEV::ASTVec(); - //created_exprs.clear(); - return (VC)bm; -} - -// Expr I/O -void vc_printExpr(VC vc, Expr e) { - //do not print in lisp mode - //bmstar b = (bmstar)vc; - BEEV::ASTNode q = (*(nodestar)e); - // b->Begin_RemoveWrites = true; - // BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false); - // b->Begin_RemoveWrites = false; - q.PL_Print(cout); -} - -void vc_printExprFile(VC vc, Expr e, int fd) { - fdostream os(fd); - ((nodestar)e)->PL_Print(os); - //os.flush(); -} - -static void vc_printVarDeclsToStream(VC vc, ostream &os) { - for(BEEV::ASTVec::iterator i = decls->begin(),iend=decls->end();i!=iend;i++) { - node a = *i; - switch(a.GetType()) { - case BEEV::BITVECTOR_TYPE: - a.PL_Print(os); - os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl; - break; - case BEEV::ARRAY_TYPE: - a.PL_Print(os); - os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF "; - os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl; - break; - case BEEV::BOOLEAN_TYPE: - a.PL_Print(os); - os << " : BOOLEAN;" << endl; - break; - default: - BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a); - break; - } - } -} - -void vc_printVarDecls(VC vc) { - vc_printVarDeclsToStream(vc, cout); -} - -static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) { - bmstar b = (bmstar)vc; - BEEV::ASTVec v = b->GetAsserts(); - for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { - b->Begin_RemoveWrites = true; - BEEV::ASTNode q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(*i,false) : *i; - q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(q,false) : q; - b->Begin_RemoveWrites = false; - os << "ASSERT( "; - q.PL_Print(os); - os << ");" << endl; - } -} - -void vc_printAsserts(VC vc, int simplify_print) { - vc_printAssertsToStream(vc, cout, simplify_print); -} - -void vc_printQueryStateToBuffer(VC vc, Expr e, char **buf, unsigned long *len, int simplify_print){ - assert(vc); - assert(e); - assert(buf); - assert(len); - bmstar b = (bmstar)vc; - - // formate the state of the query - stringstream os; - vc_printVarDeclsToStream(vc, os); - os << "%----------------------------------------------------" << endl; - vc_printAssertsToStream(vc, os, simplify_print); - os << "%----------------------------------------------------" << endl; - os << "QUERY( "; - b->Begin_RemoveWrites = true; - BEEV::ASTNode q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(*((nodestar)e),false) : *(nodestar)e; - b->Begin_RemoveWrites = false; - q.PL_Print(os); - os << " );" << endl; - - // convert to a c buffer - string s = os.str(); - const char *cstr = s.c_str(); - unsigned long size = s.size() + 1; // number of chars + terminating null - *buf = (char *)malloc(size); - if (!(*buf)) { - fprintf(stderr, "malloc(%lu) failed.", size); - assert(*buf); - } - *len = size; - memcpy(*buf, cstr, size); -} - -void vc_printCounterExampleToBuffer(VC vc, char **buf, unsigned long *len) { - assert(vc); - assert(buf); - assert(len); - bmstar b = (bmstar)vc; - - // formate the state of the query - std::ostringstream os; - BEEV::print_counterexample = true; - os << "COUNTEREXAMPLE BEGIN: \n"; - b->PrintCounterExample(true,os); - os << "COUNTEREXAMPLE END: \n"; - - // convert to a c buffer - string s = os.str(); - const char *cstr = s.c_str(); - unsigned long size = s.size() + 1; // number of chars + terminating null - *buf = (char *)malloc(size); - if (!(*buf)) { - fprintf(stderr, "malloc(%lu) failed.", size); - assert(*buf); - } - *len = size; - memcpy(*buf, cstr, size); -} - -void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len) { - stringstream os; - //bmstar b = (bmstar)vc; - BEEV::ASTNode q = *((nodestar)e); - // b->Begin_RemoveWrites = true; - // BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false); - // b->Begin_RemoveWrites = false; - q.PL_Print(os); - //((nodestar)e)->PL_Print(os); - string s = os.str(); - const char * cstr = s.c_str(); - unsigned long size = s.size() + 1; // number of chars + terminating null - *buf = (char *)malloc(size); - *len = size; - memcpy(*buf, cstr, size); -} - -void vc_printQuery(VC vc){ - ostream& os = std::cout; - bmstar b = (bmstar)vc; - os << "QUERY("; - //b->Begin_RemoveWrites = true; - //BEEV::ASTNode q = b->SimplifyFormula_TopLevel(b->GetQuery(),false); - BEEV::ASTNode q = b->GetQuery(); - //b->Begin_RemoveWrites = false; - q.PL_Print(os); - // b->GetQuery().PL_Print(os); - os << ");" << endl; -} - -///////////////////////////////////////////////////////////////////////////// -// Array-related methods // -///////////////////////////////////////////////////////////////////////////// -//! Create an array type -Type vc_arrayType(VC vc, Type typeIndex, Type typeData) { - bmstar b = (bmstar)vc; - nodestar ti = (nodestar)typeIndex; - nodestar td = (nodestar)typeData; - - if(!(ti->GetKind() == BEEV::BITVECTOR && (*ti)[0].GetKind() == BEEV::BVCONST)) - BEEV::FatalError("Tyring to build array whose indextype i is not a BITVECTOR, where i = ",*ti); - if(!(td->GetKind() == BEEV::BITVECTOR && (*td)[0].GetKind() == BEEV::BVCONST)) - BEEV::FatalError("Trying to build an array whose valuetype v is not a BITVECTOR. where a = ",*td); - nodestar output = new node(b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0])); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return (Type)output; -} - -//! Create an expression for the value of array at the given index -Expr vc_readExpr(VC vc, Expr array, Expr index) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)array; - nodestar i = (nodestar)index; - - b->BVTypeCheck(*a); - b->BVTypeCheck(*i); - node o = b->CreateTerm(BEEV::READ,a->GetValueWidth(),*a,*i); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -// //! Array update; equivalent to "array WITH [index] := newValue" -Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)array; - nodestar i = (nodestar)index; - nodestar n = (nodestar)newValue; - - b->BVTypeCheck(*a); - b->BVTypeCheck(*i); - b->BVTypeCheck(*n); - node o = b->CreateTerm(BEEV::WRITE,a->GetValueWidth(),*a,*i,*n); - o.SetIndexWidth(a->GetIndexWidth()); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -///////////////////////////////////////////////////////////////////////////// -// Context-related methods // -///////////////////////////////////////////////////////////////////////////// -//! Assert a new formula in the current context. -/*! The formula must have Boolean type. */ -void vc_assertFormula(VC vc, Expr e) { - nodestar a = (nodestar)e; - bmstar b = (bmstar)vc; - - if(!BEEV::is_Form_kind(a->GetKind())) - BEEV::FatalError("Trying to assert a NON formula: ",*a); - - b->BVTypeCheck(*a); - b->AddAssert(*a); -} - -//! Check validity of e in the current context. -/*! If the result is true, then the resulting context is the same as - * the starting context. If the result is false, then the resulting - * context is a context in which e is false. e must have Boolean - * type. */ -int vc_query(VC vc, Expr e) { - nodestar a = (nodestar)e; - bmstar b = (bmstar)vc; - - if(!BEEV::is_Form_kind(a->GetKind())) - BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a); - - b->BVTypeCheck(*a); - b->AddQuery(*a); - - const BEEV::ASTVec v = b->GetAsserts(); - node o; - if(!v.empty()) { - if(v.size()==1) - return b->TopLevelSAT(v[0],*a); - else - return b->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a); - } - else - return b->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a); -} - -void vc_push(VC vc) { - bmstar b = (bmstar)vc; - b->ClearAllCaches(); - b->Push(); -} - -void vc_pop(VC vc) { - bmstar b = (bmstar)vc; - b->Pop(); -} - -void vc_printCounterExample(VC vc) { - bmstar b = (bmstar)vc; - BEEV::print_counterexample = true; - cout << "COUNTEREXAMPLE BEGIN: \n"; - b->PrintCounterExample(true); - cout << "COUNTEREXAMPLE END: \n"; -} - -// //! Return the counterexample after a failed query. -// /*! This method should only be called after a query which returns -// * false. It will try to return the simplest possible set of -// * assertions which are sufficient to make the queried expression -// * false. The caller is responsible for freeing the array when -// * finished with it. -// */ - -Expr vc_getCounterExample(VC vc, Expr e) { - nodestar a = (nodestar)e; - bmstar b = (bmstar)vc; - - bool t = false; - if(b->CounterExampleSize()) - t = true; - nodestar output = new node(b->GetCounterExample(t, *a)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -int vc_counterexample_size(VC vc) { - bmstar b = (bmstar)vc; - return b->CounterExampleSize(); -} - -WholeCounterExample vc_getWholeCounterExample(VC vc) { - bmstar b = (bmstar)vc; - CompleteCEStar c = - new BEEV::CompleteCounterExample(b->GetCompleteCounterExample(), b); - return c; -} - -Expr vc_getTermFromCounterExample(VC vc, Expr e, CompleteCEStar cc) { - //bmstar b = (bmstar)vc; - nodestar n = (nodestar)e; - CompleteCEStar c = (CompleteCEStar)cc; - - nodestar output = new node(c->GetCounterExample(*n)); - return output; -} - -int vc_getBVLength(VC vc, Expr ex) { - nodestar e = (nodestar)ex; - - if(BEEV::BITVECTOR_TYPE != e->GetType()) { - BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector"); - } - - return e->GetValueWidth(); -} // end of vc_getBVLength - -///////////////////////////////////////////////////////////////////////////// -// Expr Creation methods // -///////////////////////////////////////////////////////////////////////////// -//! Create a variable with a given name and type -/*! The type cannot be a function type. */ -Expr vc_varExpr1(VC vc, char* name, - int indexwidth, int valuewidth) { - bmstar b = (bmstar)vc; - - node o = b->CreateSymbol(name); - o.SetIndexWidth(indexwidth); - o.SetValueWidth(valuewidth); - - nodestar output = new node(o); - ////if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->BVTypeCheck(*output); - - //store the decls in a vector for printing purposes - decls->push_back(o); - return output; -} - -Expr vc_varExpr(VC vc, char * name, Type type) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)type; - - node o = b->CreateSymbol(name); - switch(a->GetKind()) { - case BEEV::BITVECTOR: - o.SetIndexWidth(0); - o.SetValueWidth(GetUnsignedConst((*a)[0])); - break; - case BEEV::ARRAY: - o.SetIndexWidth(GetUnsignedConst((*a)[0])); - o.SetValueWidth(GetUnsignedConst((*a)[1])); - break; - case BEEV::BOOLEAN: - o.SetIndexWidth(0); - o.SetValueWidth(0); - break; - default: - BEEV::FatalError("CInterface: vc_varExpr: Unsupported type",*a); - break; - } - nodestar output = new node(o); - ////if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->BVTypeCheck(*output); - - //store the decls in a vector for printing purposes - decls->push_back(o); - return output; -} - -//! Create an equality expression. The two children must have the -//same type. -Expr vc_eqExpr(VC vc, Expr ccc0, Expr ccc1) { - bmstar b = (bmstar)vc; - - nodestar a = (nodestar)ccc0; - nodestar aa = (nodestar)ccc1; - b->BVTypeCheck(*a); - b->BVTypeCheck(*aa); - node o = b->CreateNode(BEEV::EQ,*a,*aa); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_boolType(VC vc) { - bmstar b = (bmstar)vc; - - node o = b->CreateNode(BEEV::BOOLEAN); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -///////////////////////////////////////////////////////////////////////////// -// BOOLEAN EXPR Creation methods // -///////////////////////////////////////////////////////////////////////////// -// The following functions create Boolean expressions. The children -// provided as arguments must be of type Boolean. -Expr vc_trueExpr(VC vc) { - bmstar b = (bmstar)vc; - node c = b->CreateNode(BEEV::TRUE); - - nodestar d = new node(c); - //if(cinterface_exprdelete_on) created_exprs.push_back(d); - return d; -} - -Expr vc_falseExpr(VC vc) { - bmstar b = (bmstar)vc; - node c = b->CreateNode(BEEV::FALSE); - - nodestar d = new node(c); - //if(cinterface_exprdelete_on) created_exprs.push_back(d); - return d; -} - -Expr vc_notExpr(VC vc, Expr ccc) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - - node o = b->CreateNode(BEEV::NOT,*a); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_andExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - node o = b->CreateNode(BEEV::AND,*l,*r); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_orExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - node o = b->CreateNode(BEEV::OR,*l,*r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_andExprN(VC vc, Expr* cc, int n) { - bmstar b = (bmstar)vc; - nodestar * c = (nodestar *)cc; - nodelist d; - - for(int i =0; i < n; i++) - d.push_back(*c[i]); - - node o = b->CreateNode(BEEV::AND,d); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - - -Expr vc_orExprN(VC vc, Expr* cc, int n) { - bmstar b = (bmstar)vc; - nodestar * c = (nodestar *)cc; - nodelist d; - - for(int i =0; i < n; i++) - d.push_back(*c[i]); - - node o = b->CreateNode(BEEV::OR,d); - b->BVTypeCheck(o); - - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){ - bmstar b = (bmstar)vc; - nodestar c = (nodestar)cond; - nodestar t = (nodestar)thenpart; - nodestar e = (nodestar)elsepart; - - b->BVTypeCheck(*c); - b->BVTypeCheck(*t); - b->BVTypeCheck(*e); - node o; - //if the user asks for a formula then produce a formula, else - //prodcue a term - if(BEEV::BOOLEAN_TYPE == t->GetType()) - o = b->CreateNode(BEEV::ITE,*c,*t,*e); - else { - o = b->CreateTerm(BEEV::ITE,t->GetValueWidth(),*c,*t,*e); - o.SetIndexWidth(t->GetIndexWidth()); - } - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_impliesExpr(VC vc, Expr antecedent, Expr consequent){ - bmstar b = (bmstar)vc; - nodestar c = (nodestar)antecedent; - nodestar t = (nodestar)consequent; - - b->BVTypeCheck(*c); - b->BVTypeCheck(*t); - node o; - - o = b->CreateNode(BEEV::IMPLIES,*c,*t); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_iffExpr(VC vc, Expr e0, Expr e1){ - bmstar b = (bmstar)vc; - nodestar c = (nodestar)e0; - nodestar t = (nodestar)e1; - - b->BVTypeCheck(*c); - b->BVTypeCheck(*t); - node o; - - o = b->CreateNode(BEEV::IFF,*c,*t); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_boolToBVExpr(VC vc, Expr form) { - bmstar b = (bmstar)vc; - nodestar c = (nodestar)form; - - b->BVTypeCheck(*c); - if(!is_Form_kind(c->GetKind())) - BEEV::FatalError("CInterface: vc_BoolToBVExpr: You have input a NON formula:",*c); - - node o; - node one = b->CreateOneConst(1); - node zero = b->CreateZeroConst(1); - o = b->CreateTerm(BEEV::ITE,1,*c,one,zero); - - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -///////////////////////////////////////////////////////////////////////////// -// BITVECTOR EXPR Creation methods // -///////////////////////////////////////////////////////////////////////////// -Type vc_bvType(VC vc, int num_bits) { - bmstar b = (bmstar)vc; - - if(!(0 < num_bits)) - BEEV::FatalError("CInterface: number of bits in a bvtype must be a positive integer:", - b->CreateNode(BEEV::UNDEFINED)); - - node e = b->CreateBVConst(32, num_bits); - nodestar output = new node(b->CreateNode(BEEV::BITVECTOR,e)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Type vc_bv32Type(VC vc) { - return vc_bvType(vc,32); -} - - -Expr vc_bvConstExprFromStr(VC vc, char* binary_repr) { - bmstar b = (bmstar)vc; - - node n = b->CreateBVConst(binary_repr,2); - b->BVTypeCheck(n); - nodestar output = new node(n); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvConstExprFromInt(VC vc, - int n_bits, - unsigned int value) { - bmstar b = (bmstar)vc; - - unsigned long long int v = (unsigned long long int)value; - node n = b->CreateBVConst(n_bits, v); - b->BVTypeCheck(n); - nodestar output = new node(n); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvConstExprFromLL(VC vc, - int n_bits, - unsigned long long value) { - bmstar b = (bmstar)vc; - - node n = b->CreateBVConst(n_bits, value); - b->BVTypeCheck(n); - nodestar output = new node(n); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvConcatExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = - b->CreateTerm(BEEV::BVCONCAT, - l->GetValueWidth()+ r->GetValueWidth(),*l,*r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right){ - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVPLUS,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - - -Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right) { - return vc_bvPlusExpr(vc, 32, left, right); -} - - -Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVSUB,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - - -Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right) { - return vc_bvMinusExpr(vc, 32, left, right); -} - - -Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVMULT,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVDIV,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVMOD,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::SBVDIV,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::SBVMOD,n_bits, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bv32MultExpr(VC vc, Expr left, Expr right) { - return vc_bvMultExpr(vc, 32, left, right); -} - - -// unsigned comparators -Expr vc_bvLtExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVLT, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvLeExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVLE, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvGtExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVGT, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvGeExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVGE, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -// signed comparators -Expr vc_sbvLtExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVSLT, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_sbvLeExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVSLE, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_sbvGtExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVSGT, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_sbvGeExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateNode(BEEV::BVSGE, *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvUMinusExpr(VC vc, Expr ccc) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - b->BVTypeCheck(*a); - - node o = b->CreateTerm(BEEV::BVUMINUS, a->GetValueWidth(), *a); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -// bitwise operations: these are terms not formulas -Expr vc_bvAndExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVAND, (*l).GetValueWidth(), *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvOrExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVOR, (*l).GetValueWidth(), *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvXorExpr(VC vc, Expr left, Expr right) { - bmstar b = (bmstar)vc; - nodestar l = (nodestar)left; - nodestar r = (nodestar)right; - - b->BVTypeCheck(*l); - b->BVTypeCheck(*r); - node o = b->CreateTerm(BEEV::BVXOR, (*l).GetValueWidth(), *l, *r); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvNotExpr(VC vc, Expr ccc) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - - b->BVTypeCheck(*a); - node o = b->CreateTerm(BEEV::BVNEG, a->GetValueWidth(), *a); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - b->BVTypeCheck(*a); - - //convert leftshift to bvconcat - if(0 != sh_amt) { - node len = b->CreateBVConst(sh_amt, 0); - node o = b->CreateTerm(BEEV::BVCONCAT, a->GetValueWidth() + sh_amt, *a, len); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; - } - else - return a; -} - -Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - b->BVTypeCheck(*a); - - unsigned int w = a->GetValueWidth(); - //the amount by which you are rightshifting - //is less-than/equal-to the length of input - //bitvector - if(0 < (unsigned)sh_amt && (unsigned)sh_amt <= w) { - node len = b->CreateBVConst(sh_amt, 0); - node hi = b->CreateBVConst(32,w-1); - node low = b->CreateBVConst(32,sh_amt); - node extract = b->CreateTerm(BEEV::BVEXTRACT,w-sh_amt,*a,hi,low); - - node n = b->CreateTerm(BEEV::BVCONCAT, w,len, extract); - b->BVTypeCheck(n); - nodestar output = new node(n); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; - } - else if(sh_amt == 0) - return a; - else { - if(0== w) - BEEV::FatalError("CInterface: vc_bvRightShiftExpr: cannot have a bitvector of length 0:",*a); - nodestar output = new node(b->CreateBVConst(w,0)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; - } -} - -/* Same as vc_bvLeftShift only that the answer in 32 bits long */ -Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child) { - return vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, sh_amt, child), 31, 0); -} - -/* Same as vc_bvRightShift only that the answer in 32 bits long */ -Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child) { - return vc_bvExtract(vc, vc_bvRightShiftExpr(vc, sh_amt, child), 31, 0); -} - - -Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child) { - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, 32, count)); - thenpart = vc_bvExtract(vc, - vc_bvLeftShiftExpr(vc, count, child), - 31, 0); - - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } - else - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - return ite; -} - -Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) { - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, rhs, - vc_bvConstExprFromInt(vc, 32, 1 << count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - } - return ite; -} - -Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child) { - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, 32, count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - } - return ite; -} - -Expr vc_bvExtract(VC vc, Expr ccc, int hi_num, int low_num) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - b->BVTypeCheck(*a); - - node hi = b->CreateBVConst(32,hi_num); - node low = b->CreateBVConst(32,low_num); - node o = b->CreateTerm(BEEV::BVEXTRACT,hi_num-low_num+1,*a,hi,low); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvBoolExtract(VC vc, Expr ccc, int bit_num) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - b->BVTypeCheck(*a); - - node bit = b->CreateBVConst(32,bit_num); - //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit); - node zero = b->CreateBVConst(1,0); - node oo = b->CreateTerm(BEEV::BVEXTRACT,1,*a,bit,bit); - node o = b->CreateNode(BEEV::EQ,oo,zero); - b->BVTypeCheck(o); - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -Expr vc_bvSignExtend(VC vc, Expr ccc, int nbits) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)ccc; - - //width of the expr which is being sign extended. nbits is the - //resulting length of the signextended expr - b->BVTypeCheck(*a); - - unsigned exprlen = a->GetValueWidth(); - unsigned outputlen = nbits; - node n; - if(exprlen >= outputlen) { - //extract - node hi = b->CreateBVConst(32,outputlen-1); - node low = b->CreateBVConst(32,0); - n = b->CreateTerm(BEEV::BVEXTRACT,nbits,*a,hi,low); - b->BVTypeCheck(n); - } - else { - //sign extend - BEEV::ASTNode width = b->CreateBVConst(32,nbits); - n = b->CreateTerm(BEEV::BVSX,nbits,*a, width); - } - - b->BVTypeCheck(n); - nodestar output = new node(n); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; -} - -//! Return an int from a constant bitvector expression -int getBVInt(Expr e) { - //bmstar b = (bmstar)vc; - nodestar a = (nodestar)e; - - if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("CInterface: getBVInt: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); - return (int)GetUnsignedConst(*a); -} - -//! Return an unsigned int from a constant bitvector expression -unsigned int getBVUnsigned(Expr e) { - //bmstar b = (bmstar)vc; - nodestar a = (nodestar)e; - - if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); - return (unsigned int)GetUnsignedConst(*a); -} - -//! Return an unsigned long long int from a constant bitvector expression -unsigned long long int getBVUnsignedLongLong(Expr e) { - //bmstar b = (bmstar)vc; - nodestar a = (nodestar)e; - - if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); -#ifdef NATIVE_C_ARITH - return (unsigned long long int)a->GetBVConst(); -#else - unsigned* bv = a->GetBVConst(); - - char * str_bv = (char *)CONSTANTBV::BitVector_to_Bin(bv); - unsigned long long int tmp = strtoull(str_bv,NULL,2); - CONSTANTBV::BitVector_Dispose((unsigned char *)str_bv); - return tmp; -#endif -} - - -Expr vc_simplify(VC vc, Expr e) { - bmstar b = (bmstar)vc; - nodestar a = (nodestar)e; - - if(BEEV::BOOLEAN_TYPE == a->GetType()) { - nodestar output = new node(b->SimplifyFormula_TopLevel(*a,false)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = true; - output = new node(b->SimplifyFormula_TopLevel(*output,false)); - b->Begin_RemoveWrites = false; - return output; - } - else { - nodestar output = new node(b->SimplifyTerm(*a)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = true; - output = new node(b->SimplifyTerm(*output)); - b->Begin_RemoveWrites = false; - return output; - } -} - -/* C pointer support: C interface to support C memory arrays in CVCL */ -Expr vc_bvCreateMemoryArray(VC vc, char * arrayName) { - Type bv8 = vc_bvType(vc,8); - Type bv32 = vc_bvType(vc,32); - - Type malloced_mem0 = vc_arrayType(vc,bv32,bv8); - return vc_varExpr(vc, arrayName, malloced_mem0); -} - -Expr vc_bvReadMemoryArray(VC vc, - Expr array, - Expr byteIndex, int numOfBytes) { - if(!(numOfBytes > 0)) - BEEV::FatalError("numOfBytes must be greater than 0"); - - if(numOfBytes == 1) - return vc_readExpr(vc,array,byteIndex); - else { - int count = 1; - Expr a = vc_readExpr(vc,array,byteIndex); - while(--numOfBytes > 0) { - Expr b = vc_readExpr(vc,array, - /*vc_simplify(vc, */ - vc_bvPlusExpr(vc, 32, - byteIndex, - vc_bvConstExprFromInt(vc,32,count)))/*)*/; - a = vc_bvConcatExpr(vc,b,a); - count++; - } - return a; - } -} - -Expr vc_bvWriteToMemoryArray(VC vc, - Expr array, Expr byteIndex, - Expr element, int numOfBytes) { - if(!(numOfBytes > 0)) - BEEV::FatalError("numOfBytes must be greater than 0"); - - int newBitsPerElem = numOfBytes*8; - if(numOfBytes == 1) - return vc_writeExpr(vc, array, byteIndex, element); - else { - int count = 1; - int hi = newBitsPerElem - 1; - int low = newBitsPerElem - 8; - int low_elem = 0; - int hi_elem = low_elem + 7; - Expr c = vc_bvExtract(vc, element, hi_elem, low_elem); - Expr newarray = vc_writeExpr(vc, array, byteIndex, c); - while(--numOfBytes > 0) { - hi = low-1; - low = low-8; - - low_elem = low_elem + 8; - hi_elem = low_elem + 7; - - c = vc_bvExtract(vc, element, hi_elem, low_elem); - newarray = - vc_writeExpr(vc, newarray, - vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)), - c); - count++; - } - return newarray; - } -} - -Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value){ - return vc_bvConstExprFromInt(vc, 32, value); -} - - -#if 0 -static char *val_to_binary_str(unsigned nbits, unsigned long long val) { - char s[65]; - - assert(nbits < sizeof s); - strcpy(s, ""); - while(nbits-- > 0) { - if((val >> nbits) & 1) - strcat(s, "1"); - else - strcat(s, "0"); - } - return strdup(s); -} -#endif - -char* exprString(Expr e){ - stringstream ss; - ((nodestar)e)->PL_Print(ss,0); - string s = ss.str(); - char *copy = strdup(s.c_str()); - return copy; -} - -char* typeString(Type t){ - stringstream ss; - ((nodestar)t)->PL_Print(ss,0); - - string s = ss.str(); - char *copy = strdup(s.c_str()); - return copy; -} - -Expr getChild(Expr e, int i){ - nodestar a = (nodestar)e; - - BEEV::ASTVec c = a->GetChildren(); - if ((unsigned)i < c.size()) { - BEEV::ASTNode o = c[i]; - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; - } - else - BEEV::FatalError("getChild: Error accessing childNode in expression: ",*a); - return a; -} - -void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg)) { - BEEV::vc_error_hdlr = error_hdlr; -} - - -int vc_getHashQueryStateToBuffer(VC vc, Expr query) { - assert(vc); - assert(query); - bmstar b = (bmstar)vc; - nodestar qry = (nodestar)query; - BEEV::ASTVec v = b->GetAsserts(); - BEEV::ASTNode out = b->CreateNode(BEEV::AND,b->CreateNode(BEEV::NOT,*qry),v); - return out.Hash(); -} - -Type vc_getType(VC vc, Expr ex) { - nodestar e = (nodestar)ex; - - switch(e->GetType()) { - case BEEV::BOOLEAN_TYPE: - return vc_boolType(vc); - break; - case BEEV::BITVECTOR_TYPE: - return vc_bvType(vc,e->GetValueWidth()); - break; - case BEEV::ARRAY_TYPE: { - Type typeindex = vc_bvType(vc,e->GetIndexWidth()); - Type typedata = vc_bvType(vc,e->GetValueWidth()); - return vc_arrayType(vc,typeindex,typedata); - break; - } - default: - BEEV::FatalError("c_interface: vc_GetType: expression with bad typing: please check your expression construction"); - return vc_boolType(vc); - break; - } -}// end of vc_gettype() - -//!if e is TRUE then return 1; if e is FALSE then return 0; otherwise -//return -1 -int vc_isBool(Expr e) { - nodestar input = (nodestar)e; - if(BEEV::TRUE == input->GetKind()) { - return 1; - } - - if(BEEV::FALSE == input->GetKind()) { - return 0; - } - - return -1; -} - -void vc_Destroy(VC vc) { - bmstar b = (bmstar)vc; - // for(std::vector<BEEV::ASTNode *>::iterator it=created_exprs.begin(), - // itend=created_exprs.end();it!=itend;it++) { - // BEEV::ASTNode * aaa = *it; - // delete aaa; - // } - delete decls; - delete b; -} - -void vc_DeleteExpr(Expr e) { - nodestar input = (nodestar)e; - //bmstar b = (bmstar)vc; - delete input; -} - -exprkind_t getExprKind(Expr e) { - nodestar input = (nodestar)e; - return (exprkind_t)(input->GetKind()); -} - -int getDegree (Expr e) { - nodestar input = (nodestar)e; - return input->Degree(); -} - -int getBVLength(Expr ex) { - nodestar e = (nodestar)ex; - - if(BEEV::BITVECTOR_TYPE != e->GetType()) { - BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector"); - } - - return e->GetValueWidth(); -} - -type_t getType (Expr ex) { - nodestar e = (nodestar)ex; - - return (type_t)(e->GetType()); -} - -int getVWidth (Expr ex) { - nodestar e = (nodestar)ex; - - return e->GetValueWidth(); -} - -int getIWidth (Expr ex) { - nodestar e = (nodestar)ex; - - return e->GetIndexWidth(); -} - -void vc_printCounterExampleFile(VC vc, int fd) { - fdostream os(fd); - bmstar b = (bmstar)vc; - BEEV::print_counterexample = true; - os << "COUNTEREXAMPLE BEGIN: \n"; - b->PrintCounterExample(true, os); - os << "COUNTEREXAMPLE END: \n"; -} - -const char* exprName(Expr e){ - return ((nodestar)e)->GetName(); -} - -int getExprID (Expr ex) { - BEEV::ASTNode q = (*(nodestar)ex); - - return q.GetNodeNum(); -} diff --git a/stp/c_interface/c_interface.h b/stp/c_interface/c_interface.h deleted file mode 100644 index a2fa8cd7..00000000 --- a/stp/c_interface/c_interface.h +++ /dev/null @@ -1,401 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * 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. - ********************************************************************/ -// -*- c++ -*- -#ifndef _cvcl__include__c_interface_h_ -#define _cvcl__include__c_interface_h_ - -#ifdef __cplusplus -extern "C" { -#endif - -#ifdef STP_STRONG_TYPING -#else - //This gives absolutely no pointer typing at compile-time. Most C - //users prefer this over stronger typing. User is the king. A - //stronger typed interface is in the works. - typedef void* VC; - typedef void* Expr; - typedef void* Type; - typedef void* WholeCounterExample; -#endif - - // o : optimizations - // c : check counterexample - // p : print counterexample - // h : help - // s : stats - // v : print nodes - void vc_setFlags(char c); - - //! Flags can be NULL - VC vc_createValidityChecker(void); - - // Basic types - Type vc_boolType(VC vc); - - //! Create an array type - Type vc_arrayType(VC vc, Type typeIndex, Type typeData); - - ///////////////////////////////////////////////////////////////////////////// - // Expr manipulation methods // - ///////////////////////////////////////////////////////////////////////////// - - //! Create a variable with a given name and type - /*! The type cannot be a function type. The var name can contain - only variables, numerals and underscore. If you use any other - symbol, you will get a segfault. */ - Expr vc_varExpr(VC vc, char * name, Type type); - - //The var name can contain only variables, numerals and - //underscore. If you use any other symbol, you will get a segfault. - Expr vc_varExpr1(VC vc, char* name, - int indexwidth, int valuewidth); - - //! Get the expression and type associated with a name. - /*! If there is no such Expr, a NULL Expr is returned. */ - //Expr vc_lookupVar(VC vc, char* name, Type* type); - - //! Get the type of the Expr. - Type vc_getType(VC vc, Expr e); - - int vc_getBVLength(VC vc, Expr e); - - //! Create an equality expression. The two children must have the same type. - Expr vc_eqExpr(VC vc, Expr child0, Expr child1); - - // Boolean expressions - - // The following functions create Boolean expressions. The children - // provided as arguments must be of type Boolean (except for the - // function vc_iteExpr(). In the case of vc_iteExpr() the - // conditional must always be Boolean, but the ifthenpart - // (resp. elsepart) can be bit-vector or Boolean type. But, the - // ifthenpart and elsepart must be both of the same type) - Expr vc_trueExpr(VC vc); - Expr vc_falseExpr(VC vc); - Expr vc_notExpr(VC vc, Expr child); - Expr vc_andExpr(VC vc, Expr left, Expr right); - Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes); - Expr vc_orExpr(VC vc, Expr left, Expr right); - Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes); - Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc); - Expr vc_iffExpr(VC vc, Expr left, Expr right); - //The output type of vc_iteExpr can be Boolean (formula-level ite) - //or bit-vector (word-level ite) - Expr vc_iteExpr(VC vc, Expr conditional, Expr ifthenpart, Expr elsepart); - - //Boolean to single bit BV Expression - Expr vc_boolToBVExpr(VC vc, Expr form); - - // Arrays - - //! Create an expression for the value of array at the given index - Expr vc_readExpr(VC vc, Expr array, Expr index); - - //! Array update; equivalent to "array WITH [index] := newValue" - Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue); - - // Expr I/O - //! Expr vc_parseExpr(VC vc, char* s); - - //! Prints 'e' to stdout. - void vc_printExpr(VC vc, Expr e); - - //! Prints 'e' into an open file descriptor 'fd' - void vc_printExprFile(VC vc, Expr e, int fd); - - //! Prints state of 'vc' into malloc'd buffer '*buf' and stores the - // length into '*len'. It is the responsibility of the caller to - // free the buffer. - //void vc_printStateToBuffer(VC vc, char **buf, unsigned long *len); - - //! Prints 'e' to malloc'd buffer '*buf'. Sets '*len' to the length of - // the buffer. It is the responsibility of the caller to free the buffer. - void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len); - - //! Prints counterexample to stdout. - void vc_printCounterExample(VC vc); - - //! Prints variable declarations to stdout. - void vc_printVarDecls(VC vc); - - //! Prints asserts to stdout. The flag simplify_print must be set to - //"1" if you wish simplification to occur dring printing. It must be - //set to "0" otherwise - void vc_printAsserts(VC vc, int simplify_print); - - //! Prints the state of the query to malloc'd buffer '*buf' and - //stores ! the length of the buffer to '*len'. It is the - //responsibility of the caller to free the buffer. The flag - //simplify_print must be set to "1" if you wish simplification to - //occur dring printing. It must be set to "0" otherwise - void vc_printQueryStateToBuffer(VC vc, Expr e, - char **buf, unsigned long *len, int simplify_print); - - //! Similar to vc_printQueryStateToBuffer() - void vc_printCounterExampleToBuffer(VC vc, char **buf,unsigned long *len); - - //! Prints query to stdout. - void vc_printQuery(VC vc); - - ///////////////////////////////////////////////////////////////////////////// - // Context-related methods // - ///////////////////////////////////////////////////////////////////////////// - - //! Assert a new formula in the current context. - /*! The formula must have Boolean type. */ - void vc_assertFormula(VC vc, Expr e); - - //! Simplify e with respect to the current context - Expr vc_simplify(VC vc, Expr e); - - //! Check validity of e in the current context. e must be a FORMULA - // - //if returned 0 then input is INVALID. - // - //if returned 1 then input is VALID - // - //if returned 2 then ERROR - int vc_query(VC vc, Expr e); - - //! Return the counterexample after a failed query. - Expr vc_getCounterExample(VC vc, Expr e); - - //! get size of counterexample, i.e. the number of variables/array - //locations in the counterexample. - int vc_counterexample_size(VC vc); - - //! Checkpoint the current context and increase the scope level - void vc_push(VC vc); - - //! Restore the current context to its state at the last checkpoint - void vc_pop(VC vc); - - //! Return an int from a constant bitvector expression - int getBVInt(Expr e); - //! Return an unsigned int from a constant bitvector expression - unsigned int getBVUnsigned(Expr e); - //! Return an unsigned long long int from a constant bitvector expressions - unsigned long long int getBVUnsignedLongLong(Expr e); - - /**************************/ - /* BIT VECTOR OPERATIONS */ - /**************************/ - Type vc_bvType(VC vc, int no_bits); - Type vc_bv32Type(VC vc); - - Expr vc_bvConstExprFromStr(VC vc, char* binary_repr); - Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value); - Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value); - Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); - - Expr vc_bvConcatExpr(VC vc, Expr left, Expr right); - Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right); - Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right); - Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right); - Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right); - Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right); - Expr vc_bv32MultExpr(VC vc, Expr left, Expr right); - // left divided by right i.e. left/right - Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right); - // left modulo right i.e. left%right - Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right); - // signed left divided by right i.e. left/right - Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right); - // signed left modulo right i.e. left%right - Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right); - - Expr vc_bvLtExpr(VC vc, Expr left, Expr right); - Expr vc_bvLeExpr(VC vc, Expr left, Expr right); - Expr vc_bvGtExpr(VC vc, Expr left, Expr right); - Expr vc_bvGeExpr(VC vc, Expr left, Expr right); - - Expr vc_sbvLtExpr(VC vc, Expr left, Expr right); - Expr vc_sbvLeExpr(VC vc, Expr left, Expr right); - Expr vc_sbvGtExpr(VC vc, Expr left, Expr right); - Expr vc_sbvGeExpr(VC vc, Expr left, Expr right); - - Expr vc_bvUMinusExpr(VC vc, Expr child); - - // bitwise operations: these are terms not formulas - Expr vc_bvAndExpr(VC vc, Expr left, Expr right); - Expr vc_bvOrExpr(VC vc, Expr left, Expr right); - Expr vc_bvXorExpr(VC vc, Expr left, Expr right); - Expr vc_bvNotExpr(VC vc, Expr child); - - Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child); - Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child); - /* Same as vc_bvLeftShift only that the answer in 32 bits long */ - Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child); - /* Same as vc_bvRightShift only that the answer in 32 bits long */ - Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child); - Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child); - Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child); - Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs); - - Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no); - - //accepts a bitvector and position, and returns a boolean - //corresponding to that position. More precisely, it return the - //equation (x[bit_no:bit_no] = 0) - //FIXME = 1 ? - Expr vc_bvBoolExtract(VC vc, Expr x, int bit_no); - Expr vc_bvSignExtend(VC vc, Expr child, int nbits); - - /*C pointer support: C interface to support C memory arrays in CVCL */ - Expr vc_bvCreateMemoryArray(VC vc, char * arrayName); - Expr vc_bvReadMemoryArray(VC vc, - Expr array, Expr byteIndex, int numOfBytes); - Expr vc_bvWriteToMemoryArray(VC vc, - Expr array, Expr byteIndex, - Expr element, int numOfBytes); - Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); - - // return a string representation of the Expr e. The caller is responsible - // for deallocating the string with free() - char* exprString(Expr e); - - // return a string representation of the Type t. The caller is responsible - // for deallocating the string with free() - char* typeString(Type t); - - Expr getChild(Expr e, int i); - - //1.if input expr is TRUE then the function returns 1; - // - //2.if input expr is FALSE then function returns 0; - // - //3.otherwise the function returns -1 - int vc_isBool(Expr e); - - /* Register the given error handler to be called for each fatal error.*/ - void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg)); - - int vc_getHashQueryStateToBuffer(VC vc, Expr query); - - //destroys the STP instance, and removes all the created expressions - void vc_Destroy(VC vc); - - //deletes the expression e - void vc_DeleteExpr(Expr e); - - //Get the whole counterexample from the current context - WholeCounterExample vc_getWholeCounterExample(VC vc); - - //Get the value of a term expression from the CounterExample - Expr vc_getTermFromCounterExample(VC vc, Expr e, WholeCounterExample c); - - //Kinds of Expr - enum exprkind_t{ - 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 - }; - - // type of expression - enum type_t { - BOOLEAN_TYPE = 0, - BITVECTOR_TYPE, - ARRAY_TYPE, - UNKNOWN_TYPE - }; - - // get the kind of the expression - exprkind_t getExprKind (Expr e); - - // get the number of children nodes - int getDegree (Expr e); - - // get the bv length - int getBVLength(Expr e); - - // get expression type - type_t getType (Expr e); - - // get value bit width - int getVWidth (Expr e); - - // get index bit width - int getIWidth (Expr e); - - // Prints counterexample to an open file descriptor 'fd' - void vc_printCounterExampleFile(VC vc, int fd); - - // get name of expression. must be a variable. - const char* exprName(Expr e); - - // get the node ID of an Expr. - int getExprID (Expr ex); - -#ifdef __cplusplus -} -#endif - -#endif - - diff --git a/stp/c_interface/fdstream.h b/stp/c_interface/fdstream.h deleted file mode 100644 index 2cff613c..00000000 --- a/stp/c_interface/fdstream.h +++ /dev/null @@ -1,186 +0,0 @@ -/*! @brief The following code declares classes to read from and write to - * file descriptore or file handles. - * - * See - * http://www.josuttis.com/cppcode - * for details and the latest version. - * - * - open: - * - integrating BUFSIZ on some systems? - * - optimized reading of multiple characters - * - stream for reading AND writing - * - i18n - * - * (C) Copyright Nicolai M. Josuttis 2001. - * Permission to copy, use, modify, sell and distribute this software - * is granted provided this copyright notice appears in all copies. - * This software is provided "as is" without express or implied - * warranty, and with no claim as to its suitability for any purpose. - * - * Version: Jul 28, 2002 - * History: - * Jul 28, 2002: bugfix memcpy() => memmove() - * fdinbuf::underflow(): cast for return statements - * Aug 05, 2001: first public version - */ -#ifndef BOOST_FDSTREAM_HPP -#define BOOST_FDSTREAM_HPP - -#include <istream> -#include <ostream> -#include <streambuf> - - -// for EOF: -#include <cstdio> -// for memmove(): -#include <cstring> - - -// low-level read and write functions -#ifdef _MSC_VER -# include <io.h> -#else -# include <unistd.h> -//extern "C" { -// int write (int fd, const char* buf, int num); -// int read (int fd, char* buf, int num); -//} -#endif - - -// BEGIN namespace BOOST -namespace std { - - -/************************************************************ - * fdostream - * - a stream that writes on a file descriptor - ************************************************************/ - - -class fdoutbuf : public std::streambuf { - protected: - int fd; // file descriptor - public: - // constructor - fdoutbuf (int _fd) : fd(_fd) { - } - protected: - // write one character - virtual int_type overflow (int_type c) { - if (c != EOF) { - char z = c; - if (write (fd, &z, 1) != 1) { - return EOF; - } - } - return c; - } - // write multiple characters - virtual - std::streamsize xsputn (const char* s, - std::streamsize num) { - return write(fd,s,num); - } -}; - -class fdostream : public std::ostream { - protected: - fdoutbuf buf; - public: - fdostream (int fd) : std::ostream(0), buf(fd) { - rdbuf(&buf); - } -}; - - -/************************************************************ - * fdistream - * - a stream that reads on a file descriptor - ************************************************************/ - -class fdinbuf : public std::streambuf { - protected: - int fd; // file descriptor - protected: - /* data buffer: - * - at most, pbSize characters in putback area plus - * - at most, bufSize characters in ordinary read buffer - */ - static const int pbSize = 4; // size of putback area - static const int bufSize = 1024; // size of the data buffer - char buffer[bufSize+pbSize]; // data buffer - - public: - /* constructor - * - initialize file descriptor - * - initialize empty data buffer - * - no putback area - * => force underflow() - */ - fdinbuf (int _fd) : fd(_fd) { - setg (buffer+pbSize, // beginning of putback area - buffer+pbSize, // read position - buffer+pbSize); // end position - } - - protected: - // insert new characters into the buffer - virtual int_type underflow () { -#ifndef _MSC_VER - using std::memmove; -#endif - - // is read position before end of buffer? - if (gptr() < egptr()) { - return traits_type::to_int_type(*gptr()); - } - - /* process size of putback area - * - use number of characters read - * - but at most size of putback area - */ - int numPutback; - numPutback = gptr() - eback(); - if (numPutback > pbSize) { - numPutback = pbSize; - } - - /* copy up to pbSize characters previously read into - * the putback area - */ - memmove (buffer+(pbSize-numPutback), gptr()-numPutback, - numPutback); - - // read at most bufSize new characters - int num; - num = read (fd, buffer+pbSize, bufSize); - if (num <= 0) { - // ERROR or EOF - return EOF; - } - - // reset buffer pointers - setg (buffer+(pbSize-numPutback), // beginning of putback area - buffer+pbSize, // read position - buffer+pbSize+num); // end of buffer - - // return next character - return traits_type::to_int_type(*gptr()); - } -}; - -class fdistream : public std::istream { - protected: - fdinbuf buf; - public: - fdistream (int fd) : std::istream(0), buf(fd) { - rdbuf(&buf); - } -}; - - -} // END namespace boost - -#endif /*BOOST_FDSTREAM_HPP*/ |