diff options
Diffstat (limited to 'stp/c_interface')
| -rw-r--r-- | stp/c_interface/Makefile | 13 | ||||
| -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, 2148 insertions, 0 deletions
diff --git a/stp/c_interface/Makefile b/stp/c_interface/Makefile new file mode 100644 index 00000000..cf6b09d1 --- /dev/null +++ b/stp/c_interface/Makefile @@ -0,0 +1,13 @@ +include ../Makefile.common + +SRCS = c_interface.cpp +OBJS = $(SRCS:.cpp=.o) + +libcinterface.a: $(OBJS) + $(AR) rc $@ $^ + $(RANLIB) $@ + +clean: + rm -rf *.o *~ *.a .#* + +c_interface.o: c_interface.h diff --git a/stp/c_interface/c_interface.cpp b/stp/c_interface/c_interface.cpp new file mode 100644 index 00000000..f4e53114 --- /dev/null +++ b/stp/c_interface/c_interface.cpp @@ -0,0 +1,1548 @@ +/******************************************************************** + * 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(0 <= (unsigned)i && (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 new file mode 100644 index 00000000..a2fa8cd7 --- /dev/null +++ b/stp/c_interface/c_interface.h @@ -0,0 +1,401 @@ +/******************************************************************** + * 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 new file mode 100644 index 00000000..2cff613c --- /dev/null +++ b/stp/c_interface/fdstream.h @@ -0,0 +1,186 @@ +/*! @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*/ |