From 0f00902ed2feba8795855e9f99c9051b1dec905f Mon Sep 17 00:00:00 2001 From: pgbovine Date: Wed, 4 Feb 2009 17:58:43 +0000 Subject: [PATCH] added functionality for converting CVC to C code git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@57 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 495 ++++++++++++++++++++++++++++++++++++ AST/AST.h | 33 ++- README | 1 + c-api-tests/cvc-to-c.cpp | 28 ++ c_interface/c_interface.cpp | 38 ++- c_interface/c_interface.h | 3 + 6 files changed, 586 insertions(+), 12 deletions(-) create mode 100644 c-api-tests/cvc-to-c.cpp diff --git a/AST/AST.cpp b/AST/AST.cpp index 2ecff2f..f607c1e 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -8,6 +8,9 @@ // -*- c++ -*- #include "AST.h" + +#include + namespace BEEV { //some global variables that are set through commandline options. it //is best that these variables remain global. Default values set @@ -682,6 +685,498 @@ namespace BEEV { } } //end of PL_Print1() + + // printer for C code (copied from PL_Print()) + // TODO: this does not fully implement printing of all of the STP + // language - FatalError calls inserted for unimplemented + // functionality, e.g.,: + // FatalError("C_Print1: printing not implemented for this kind: ",*this); + + //two pass algorithm: + // + //1. In the first pass, letize this Node, N: i.e. if a node + //1. appears more than once in N, then record this fact. + // + //2. In the second pass print a "global let" and then print N + //2. as follows: Every occurence of a node occuring more than + //2. once is replaced with the corresponding let variable. + ostream& ASTNode::C_Print(ostream &os, + int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + LetizeNode(); + + unsigned int lower, upper, num_bytes = 0; + + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if(0 < bm.NodeLetVarMap.size()) { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); + + // start a new block to create new static scope + os << "{" << endl; + + for(;it!=itend;it++) { + + // see if it's a BVEXTRACT, and if so, whether it's multi-byte + if (it->second.GetKind() == BVEXTRACT) { + upper = GetUnsignedConst(it->second.GetChildren()[1]); + lower = GetUnsignedConst(it->second.GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + assert(num_bytes > 0); + } + + //print the let var first + if (num_bytes > 1) { + // for multi-byte assignment, use 'memcpy' and array notation + os << "unsigned char "; + it->first.C_Print1(os,indentation,false); + os << "[" << num_bytes << "]; "; + os << "memcpy("; + it->first.C_Print1(os,indentation,false); + os << ", "; + //print the expr + it->second.C_Print1(os,indentation,false); + os << ", " << num_bytes << ");"; + } + else { + // for single-byte assignment, use '=' + os << "unsigned char "; + it->first.C_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.C_Print1(os,indentation,false); + os << ";" << endl; + } + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << endl << "stp_assert "; + C_Print1(os,indentation, true); + + os << ";" << endl << "}"; + } + else { + os << "stp_assert "; + C_Print1(os,indentation, false); + os << ";"; + } + //os << " )"; + //os << " "; + + return os; + } //end of C_Print() + + // helper function for printing C code (copied from PL_Print1()) + void ASTNode::C_Print1(ostream& os, + int indentation, + bool letize) const { + + unsigned int upper, lower, num_bytes; + Kind LHSkind, RHSkind; + + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!IsDefined()) { + os << ""; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) { + (bm.NodeLetVarMap1[*this]).C_Print1(os,indentation,letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) { + (bm.NodeLetVarMap[*this]).C_Print1(os,indentation,letize); + return; + } + + //otherwise print it normally + Kind kind = GetKind(); + const ASTVec &c = GetChildren(); + switch(kind) { + case BVGETBIT: + FatalError("C_Print1: printing not implemented for this kind: ",*this); + c[0].C_Print1(os,indentation,letize); + os << "{"; + c[1].C_Print1(os,indentation,letize); + os << "}"; + break; + case BITVECTOR: + FatalError("C_Print1: printing not implemented for this kind: ",*this); + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + FatalError("C_Print1: printing not implemented for this kind: ",*this); + os << "BOOLEAN"; + break; + case FALSE: + os << "0"; + break; + case TRUE: + os << "1"; + break; + case BVCONST: + case SYMBOL: + // print in C friendly format: + _int_node_ptr->nodeprint(os, true); + break; + case READ: + c[0].C_Print1(os, indentation,letize); + os << "["; + c[1].C_Print1(os,indentation,letize); + os << "]"; + break; + case WRITE: + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " WITH ["; + c[1].C_Print1(os,indentation,letize); + os << "] := "; + c[2].C_Print1(os,indentation,letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + c[0].C_Print1(os,indentation,letize); + os << ")"; + break; + case NOT: + os << "!("; + c[0].C_Print1(os,indentation,letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + c[0].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVCONCAT: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " @ "; + c[1].C_Print1(os,indentation,letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " | "; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVAND: + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " & "; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVEXTRACT: + + // we only accept indices that are byte-aligned + // (e.g., [15:8], [23:16]) + // and round down to byte indices rather than bit indices + upper = GetUnsignedConst(c[1]); + lower = GetUnsignedConst(c[2]); + assert(upper > lower); + assert(lower % 8 == 0); + assert((upper + 1) % 8 == 0); + num_bytes = (upper - lower + 1) / 8; + assert (num_bytes > 0); + + // for multi-byte extraction, use the ADDRESS + if (num_bytes > 1) { + os << "&"; + c[0].C_Print1(os,indentation,letize); + os << "[" << lower / 8 << "]"; + } + // for single-byte extraction, use the VALUE + else { + c[0].C_Print1(os,indentation,letize); + os << "[" << lower / 8 << "]"; + } + + break; + case BVLEFTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " >> "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVMULT: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVREM: + case BVDIV: + case BVMOD: + os << kind << "("; + os << this->GetValueWidth(); + for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) { + os << ", " << endl; + it->C_Print1(os,indentation,letize); + } + os << ")" << endl; + break; + case ITE: + os << "if ("; + c[0].C_Print1(os,indentation,letize); + os << ")" << endl; + os << "{"; + c[1].C_Print1(os,indentation,letize); + os << endl << "} else {"; + c[2].C_Print1(os,indentation,letize); + os << endl << "}"; + break; + case BVLT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + c[0].C_Print1(os,indentation,letize); + os << " < "; + os << "(unsigned char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVLE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + c[0].C_Print1(os,indentation,letize); + os << " <= "; + os << "(unsigned char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVGT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + c[0].C_Print1(os,indentation,letize); + os << " > "; + os << "(unsigned char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVGE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + c[0].C_Print1(os,indentation,letize); + os << " >= "; + os << "(unsigned char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + break; + case BVSLT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + c[0].C_Print1(os,indentation,letize); + os << " < "; + os << "(signed char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVSLE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + c[0].C_Print1(os,indentation,letize); + os << " <= "; + os << "(signed char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVSGT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + c[0].C_Print1(os,indentation,letize); + os << " > "; + os << "(signed char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case BVSGE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + c[0].C_Print1(os,indentation,letize); + os << " >= "; + os << "(signed char)"; + c[1].C_Print1(os,indentation,letize); + os << ")"; + break; + case EQ: + // tricky tricky ... if it's a single-byte comparison, + // simply do ==, but if it's multi-byte, must do memcmp + LHSkind = c[0].GetKind(); + RHSkind = c[1].GetKind(); + + num_bytes = 0; + + // try to figure out whether it's a single-byte or multi-byte + // comparison + if (LHSkind == BVEXTRACT) { + upper = GetUnsignedConst(c[0].GetChildren()[1]); + lower = GetUnsignedConst(c[0].GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + } + else if (RHSkind == BVEXTRACT) { + upper = GetUnsignedConst(c[1].GetChildren()[1]); + lower = GetUnsignedConst(c[1].GetChildren()[2]); + num_bytes = (upper - lower + 1) / 8; + } + + if (num_bytes > 1) { + os << "(memcmp("; + c[0].C_Print1(os,indentation,letize); + os << ", "; + c[1].C_Print1(os,indentation,letize); + os << ", "; + os << num_bytes; + os << ") == 0)"; + } + else if (num_bytes == 1) { + os << "("; + c[0].C_Print1(os,indentation,letize); + os << " == "; + c[1].C_Print1(os,indentation,letize); + os << ")"; + } + else { + FatalError("C_Print1: ugh problem in implementing =="); + } + + break; + case NEQ: + c[0].C_Print1(os,indentation,letize); + os << " != "; + c[1].C_Print1(os,indentation,letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: { + os << "("; + c[0].C_Print1(os,indentation,letize); + ASTVec::const_iterator it=c.begin(); + ASTVec::const_iterator itend=c.end(); + + it++; + for(;it!=itend;it++) { + switch (kind) { + case AND: + os << " && "; + break; + case OR: + os << " || "; + break; + case NAND: + FatalError("unsupported boolean type in C_Print1"); + break; + case NOR: + FatalError("unsupported boolean type in C_Print1"); + break; + case XOR: + FatalError("unsupported boolean type in C_Print1"); + break; + default: + FatalError("unsupported boolean type in C_Print1"); + } + it->C_Print1(os,indentation,letize); + } + os << ")"; + break; + } + case IFF: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + os << "("; + os << "("; + c[0].C_Print1(os,indentation,letize); + os << ")"; + os << " <=> "; + os << "("; + c[1].C_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + os << "("; + os << "("; + c[0].C_Print1(os,indentation,letize); + os << ")"; + os << " => "; + os << "("; + c[1].C_Print1(os,indentation,letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features + + os << kind << "("; + c[0].C_Print1(os,indentation,letize); + os << ","; + os << this->GetValueWidth(); + os << ")" << endl; + break; + default: + //remember to use LispPrinter here. Otherwise this function will + //go into an infinite loop. Recall that "<<" is overloaded to + //the lisp printer. FatalError uses lispprinter + FatalError("C_Print1: printing not implemented for this kind: ",*this); + break; + } + } //end of C_Print1() + + //////////////////////////////////////////////////////////////// // BeevMgr members //////////////////////////////////////////////////////////////// diff --git a/AST/AST.h b/AST/AST.h index 56dde97..adcce5e 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -295,6 +295,11 @@ namespace BEEV { void PL_Print1(ostream &os, int indentation = 0, bool b = false) const; + // C code printer + ostream& C_Print(ostream &os, int indentation = 0) const; + void C_Print1(ostream &os, int indentation = 0, bool b = false) const; + + //Construct let variables for shared subterms void LetizeNode(void) const; @@ -461,7 +466,8 @@ namespace BEEV { virtual ~ASTInternal(); // Abstract virtual print function for internal node. - virtual void nodeprint(ostream& os) { os << "*"; }; + // (c_friendly is for printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) { os << "*"; }; }; //End of Class ASTInternal // FIXME: Should children be only in interior node type? @@ -506,7 +512,8 @@ namespace BEEV { // Returns kinds. "lispprinter" handles printing of parenthesis // and childnodes. - virtual void nodeprint(ostream& os) { + // (c_friendly is for printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) { os << _kind_names[_kind]; } public: @@ -574,7 +581,8 @@ namespace BEEV { const char * const GetName() const{return _name;} // Print function for symbol -- return name */ - virtual void nodeprint(ostream& os) { os << _name;} + // (c_friendly is for printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) { os << _name;} // Call this when deleting a node that has been stored in the // the unique table @@ -652,16 +660,27 @@ namespace BEEV { virtual void CleanUp(); // Print function for bvconst -- return _bvconst value in bin format - virtual void nodeprint(ostream& os) { + // (c_friendly is for printing hex. numbers that C compilers will accept) + virtual void nodeprint(ostream& os, bool c_friendly = false) { unsigned char *res; const char *prefix; if (_value_width%4 == 0) { res = CONSTANTBV::BitVector_to_Hex(_bvconst); - prefix = "0hex"; + if (c_friendly) { + prefix = "0x"; + } + else { + prefix = "0hex"; + } } else { res = CONSTANTBV::BitVector_to_Bin(_bvconst); - prefix = "0bin"; + if (c_friendly) { + prefix = "0b"; + } + else { + prefix = "0bin"; + } } if (NULL == res) { os << "nodeprint: BVCONST : could not convert to string" << _bvconst; @@ -774,7 +793,7 @@ namespace BEEV { } // Print function for bvconst -- return _bvconst value in binary format - virtual void nodeprint(ostream& os) { + virtual void nodeprint(ostream& os, bool c_friendly = false) { string s = "0bin"; unsigned long long int bitmask = 0x8000000000000000LL; bitmask = bitmask >> (64-_value_width); diff --git a/README b/README index 7aa371d..ae2a16e 100644 --- a/README +++ b/README @@ -22,6 +22,7 @@ Others Who Have Contributed Some Code David L. Dill, Stanford University, Stanford, CA, USA (Nov - Dec, 2005) Michael Katelman, University of Illinois, Urbana-Champaign, USA (July - Oct, 2008) Tim King, Stanford University, Stanford, CA, USA (July - Sep, 2007) +Philip Guo, Stanford University, Stanford, CA, USA (Dec 2008, Jan 2009) Makefiles and configuration scripts diff --git a/c-api-tests/cvc-to-c.cpp b/c-api-tests/cvc-to-c.cpp new file mode 100644 index 0000000..1b0db4f --- /dev/null +++ b/c-api-tests/cvc-to-c.cpp @@ -0,0 +1,28 @@ +/* + +Take a .cvc file specified by argv[1] and transform to C code + +g++ -I$HOME/stp/c_interface cvc-to-c.cpp -L$HOME/stp/lib -lstp -o cvc-to-c + +*/ + +#include "c_interface.h" +#include + +using namespace std; + +int main(int argc, char** argv) { + VC vc = vc_createValidityChecker(); + + //vc_setFlags('n'); + //vc_setFlags('d'); + //vc_setFlags('p'); + + Expr c = vc_parseExpr(vc, argv[1]); + + vc_printExprCCode(vc, c); + + vc_Destroy(vc); + return 0; +} + diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp index 631179c..5182680 100644 --- a/c_interface/c_interface.cpp +++ b/c_interface/c_interface.cpp @@ -26,7 +26,7 @@ bool cinterface_exprdelete_on = false; /* GLOBAL FUNCTION: parser */ -extern int yyparse(); +extern int cvcparse(); void vc_setFlags(char c) { std::string helpstring = "Usage: stp [-option] [infile]\n\n"; @@ -134,6 +134,34 @@ void vc_printExpr(VC vc, Expr e) { q.PL_Print(cout); } +// prints Expr 'e' to stdout as C code +void vc_printExprCCode(VC vc, Expr e) { + BEEV::ASTNode q = (*(nodestar)e); + + // print variable declarations + BEEV::ASTVec declsFromParser = (nodelist)BEEV::globalBeevMgr_for_parser->_special_print_set; + + for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) { + if(BEEV::BITVECTOR_TYPE == it->GetType()) { + const char* name = it->GetName(); + unsigned int bitWidth = it->GetValueWidth(); + assert(bitWidth % 8 == 0); + unsigned int byteWidth = bitWidth / 8; + cout << "unsigned char " << name << "[" << byteWidth << "];" << endl; + } + else { + // vc_printExprCCode: unsupported decl. type + assert(0); + } + } + + cout << endl; + + // print constraints and assert + q.C_Print(cout); +} + + void vc_printExprFile(VC vc, Expr e, int fd) { fdostream os(fd); ((nodestar)e)->PL_Print(os); @@ -1409,11 +1437,11 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) { Expr vc_parseExpr(VC vc, char* infile) { bmstar b = (bmstar)vc; - extern FILE* yyin; + extern FILE* cvcin; const char * prog = "stp"; - yyin = fopen(infile,"r"); - if(yyin == NULL) { + cvcin = fopen(infile,"r"); + if(cvcin == NULL) { fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); BEEV::FatalError(""); } @@ -1426,7 +1454,7 @@ Expr vc_parseExpr(VC vc, char* infile) { return 0; } - yyparse(); + cvcparse(); nodelist aaa = b->GetAsserts(); node o = b->CreateNode(BEEV::AND,aaa); diff --git a/c_interface/c_interface.h b/c_interface/c_interface.h index b6a1e78..35afbd6 100644 --- a/c_interface/c_interface.h +++ b/c_interface/c_interface.h @@ -117,6 +117,9 @@ extern "C" { //! Prints 'e' to stdout. void vc_printExpr(VC vc, Expr e); + //! Prints 'e' to stdout as C code + void vc_printExprCCode(VC vc, Expr e); + //! Prints 'e' into an open file descriptor 'fd' void vc_printExprFile(VC vc, Expr e, int fd); -- 2.47.3