From: trevor_hansen Date: Thu, 16 Jul 2009 06:24:43 +0000 (+0000) Subject: Move printers to a new namespace. Create a DOT graph format printer. Add extra warnin... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=68412288127d350baca54136b9313267c9e2c6db;p=francis%2Fstp.git Move printers to a new namespace. Create a DOT graph format printer. Add extra warnings during compilation. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@82 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/AST/AST.cpp b/AST/AST.cpp index 5d88742..1b7b705 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -155,6 +155,11 @@ namespace BEEV { return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end()); } + void ASTNode::nodeprint(ostream& os, bool c_friendly) const + { + _int_node_ptr->nodeprint(os, c_friendly); + } + void ASTNode::MarkAlreadyPrinted() const { // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class? BeevMgr &bm = GetBeevMgr(); @@ -685,669 +690,6 @@ namespace BEEV { } } //end of PL_Print1() - - // copied from Presentation Langauge printer. - ostream& ASTNode::SMTLIB_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(); - - //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(); - - os << "(LET "; - //print the let var first - it->first.SMTLIB_Print1(os,indentation,false); - os << " = "; - //print the expr - it->second.SMTLIB_Print1(os,indentation,false); - - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - - for(it++;it!=itend;it++) { - os << "," << endl; - //print the let var first - it->first.SMTLIB_Print1(os,indentation,false); - os << " = "; - //print the expr - it->second.SMTLIB_Print1(os,indentation,false); - - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - } - - os << " IN " << endl; - SMTLIB_Print1(os,indentation, true); - os << ") "; - } - else - SMTLIB_Print1(os,indentation, false); - return os; - } - - - - - -void ASTNode::SMTLIB_Print1(ostream& os, - int indentation, - bool letize) const -{ - //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]).SMTLIB_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]).SMTLIB_Print1(os,indentation,letize); - return; - } - - //otherwise print it normally - Kind kind = GetKind(); - const ASTVec &c = GetChildren(); - switch(kind) - { - case BITVECTOR: // Not sure how this is differen to a BVCONST?? - {os << "bv"; - unsigned char * str; - str = CONSTANTBV::BitVector_to_Dec(c[0].GetBVConst()); - os << str << "[" << c[0].GetValueWidth() << "]"; - CONSTANTBV::BitVector_Dispose(str); - } - break; - case BVCONST: - { - os << "bv"; - unsigned char * str; - str = CONSTANTBV::BitVector_to_Dec(GetBVConst()); - os << str << "[" << GetValueWidth() << "]"; - CONSTANTBV::BitVector_Dispose(str); - } - break; - case SYMBOL: - _int_node_ptr->nodeprint(os); - break; - case FALSE: - os << "false"; - break; - case TRUE: - os << "true"; - break; - case BVEXTRACT: - { - unsigned int upper = GetUnsignedConst(c[1]); - unsigned int lower = GetUnsignedConst(c[2]); - assert(upper > lower); - os << "(extract[" << upper << ":" << lower << "] "; - c[0].SMTLIB_Print1(os,indentation,letize); - os << ")"; - } - default: - { - os << "(" << functionToSMTLIBName(kind); - - ASTVec::const_iterator iend = c.end(); - for (ASTVec::const_iterator i = c.begin(); i != iend; i++) - { - os << " "; - i->SMTLIB_Print1(os,0,letize); - } - - os << ")"; - } - } -} - -string ASTNode::functionToSMTLIBName(const Kind k) const -{ - switch(k) - { - case AND: - case OR: - case NAND: - case NOR: - case XOR: - case BVAND: - case BVNEG: - case ITE: - case BVOR: - case NOT: - return _kind_names[k]; - - case BVMULT: return "bvmul"; - case WRITE: return "store"; - case EQ: return "="; - case BVCONCAT: return "concat"; - - default: - FatalError(_kind_names[k]); - } -} - - // 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 14d3a39..a368d4e 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -123,8 +123,6 @@ namespace BEEV { return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr); } - string functionToSMTLIBName(const Kind k) const; - public: //Check if it points to a null node bool IsNull () const { return _int_node_ptr == NULL; } @@ -185,6 +183,10 @@ namespace BEEV { bool IsAlreadyPrinted() const; void MarkAlreadyPrinted() const; + // delegates to the ASTInternal node. + void nodeprint(ostream& os, bool c_friendly = false) const; + + public: // Default constructor. This gets used when declaring an ASTVec // of a given size, in the hash table, etc. For faster @@ -297,14 +299,6 @@ 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; - - ostream& SMTLIB_Print(ostream &os, int indentation) const; - void SMTLIB_Print1(ostream& os, int indentation, bool letize) const; - - //Construct let variables for shared subterms void LetizeNode(void) const; diff --git a/AST/Makefile b/AST/Makefile index 9e31bd9..aa2f5c9 100644 --- a/AST/Makefile +++ b/AST/Makefile @@ -1,7 +1,7 @@ include ../Makefile.common #SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp -SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp +SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp OBJS = $(SRCS:.cpp=.o) CFLAGS += -I../sat/mtl -I../sat/core @@ -29,6 +29,7 @@ ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl clean: rm -rf *.o *~ bbtest asttest cnftest *.a ASTKind.h ASTKind.cpp .#* + rm -rf outputer/*.o depend: makedepend -Y -- $(CFLAGS) -- $(SRCS) diff --git a/AST/printer/CPrinter.cpp b/AST/printer/CPrinter.cpp new file mode 100644 index 0000000..482c72a --- /dev/null +++ b/AST/printer/CPrinter.cpp @@ -0,0 +1,496 @@ +#include "printers.h" + +namespace printer { + +using std::string; +using namespace BEEV; + + +// 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); + +// helper function for printing C code (copied from PL_Print1()) +void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize) { + + unsigned int upper, lower, num_bytes; + Kind LHSkind, RHSkind; + + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) { + os << ""; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = n.GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) { + C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) { + C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + return; + } + + //otherwise print it normally + Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) { + case BVGETBIT: + FatalError("C_Print1: printing not implemented for this kind: ", n); + C_Print1(os, c[0], indentation, letize); + os << "{"; + C_Print1(os, c[1], indentation, letize); + os << "}"; + break; + case BITVECTOR: + FatalError("C_Print1: printing not implemented for this kind: ", n); + 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: ", n); + os << "BOOLEAN"; + break; + case FALSE: + os << "0"; + break; + case TRUE: + os << "1"; + break; + case BVCONST: + case SYMBOL: + // print in C friendly format: + n.nodeprint(os, true); + break; + case READ: + C_Print1(os, c[0], indentation, letize); + os << "["; + C_Print1(os, c[1], indentation, letize); + os << "]"; + break; + case WRITE: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " WITH ["; + C_Print1(os, c[1], indentation, letize); + os << "] := "; + C_Print1(os, c[2], indentation, letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + C_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case NOT: + os << "!("; + C_Print1(os, c[0], indentation, letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + C_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case BVCONCAT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os,c[0], indentation, letize); + os << " @ "; + C_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " | "; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVAND: + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " & "; + C_Print1(os, c[1], 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_Print1(os, c[0], indentation, letize); + os << "[" << lower / 8 << "]"; + } + // for single-byte extraction, use the VALUE + else { + C_Print1(os, c[0], indentation, letize); + os << "[" << lower / 8 << "]"; + } + + break; + case BVLEFTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + C_Print1(os,c[0], 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 << n.GetValueWidth(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { + os << ", " << endl; + C_Print1(os, *it, indentation, letize); + } + os << ")" << endl; + break; + case ITE: + os << "if ("; + C_Print1(os, c[0], indentation, letize); + os << ")" << endl; + os << "{"; + C_Print1(os, c[1], indentation, letize); + os << endl << "} else {"; + C_Print1(os, c[2], indentation, letize); + os << endl << "}"; + break; + case BVLT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " < "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVLE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " <= "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVGT: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " > "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVGE: + // convert to UNSIGNED before doing comparison! + os << "((unsigned char)"; + C_Print1(os, c[0], indentation, letize); + os << " >= "; + os << "(unsigned char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + break; + case BVSLT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " < "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSLE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " <= "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSGT: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " > "; + os << "(signed char)"; + C_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVSGE: + // convert to SIGNED before doing comparison! + os << "((signed char)"; + C_Print1(os, c[0], indentation, letize); + os << " >= "; + os << "(signed char)"; + C_Print1(os, c[1], 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_Print1(os,c[0], indentation, letize); + os << ", "; + C_Print1(os, c[1], indentation, letize); + os << ", "; + os << num_bytes; + os << ") == 0)"; + } + else if (num_bytes == 1) { + os << "("; + C_Print1(os, c[0], indentation, letize); + os << " == "; + C_Print1(os, c[1], indentation, letize); + os << ")"; + } + else { + FatalError("C_Print1: ugh problem in implementing =="); + } + + break; + case NEQ: + C_Print1(os, c[0], indentation, letize); + os << " != "; + C_Print1(os, c[1], indentation, letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: { + os << "("; + C_Print1(os, c[0], 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"); + } + C_Print1(os, *it, indentation, letize); + } + os << ")"; + break; + } + case IFF: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + os << "("; + C_Print1(os,c[0], indentation, letize); + os << ")"; + os << " <=> "; + os << "("; + C_Print1(os,c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + os << "("; + os << "("; + C_Print1(os, c[0],indentation, letize); + os << ")"; + os << " => "; + os << "("; + C_Print1(os, c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features + + os << kind << "("; + C_Print1(os, c[0],indentation, letize); + os << ","; + os << n.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: ", n); + break; + } +} //end of C_Print1() + + +//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& C_Print(ostream &os, const ASTNode n, int indentation) { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + n.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 "; + C_Print1(os, it->first,indentation, false); + os << "[" << num_bytes << "]; "; + os << "memcpy("; + C_Print1(os,it->first, indentation, false); + os << ", "; + //print the expr + C_Print1(os,it->second, indentation, false); + os << ", " << num_bytes << ");"; + } + else { + // for single-byte assignment, use '=' + os << "unsigned char "; + C_Print1(os, it->first,indentation, false); + os << " = "; + //print the expr + C_Print1(os, it->second,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, n, indentation, true); + + os << ";" << endl << "}"; + } + else { + os << "stp_assert "; + C_Print1(os, n, indentation, false); + os << ";"; + } + //os << " )"; + //os << " "; + + return os; +} //end of C_Print() +} diff --git a/AST/printer/SMTLIBPrinter.cpp b/AST/printer/SMTLIBPrinter.cpp new file mode 100644 index 0000000..c041677 --- /dev/null +++ b/AST/printer/SMTLIBPrinter.cpp @@ -0,0 +1,244 @@ +#include "printers.h" + +namespace printer { + +using std::string; +using namespace BEEV; + +string functionToSMTLIBName(const BEEV::Kind k); +void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + +void outputBitVec(const ASTNode n, ostream& os) { + Kind k = n.GetKind(); + const ASTVec &c = n.GetChildren(); + ASTNode op; + + if (BITVECTOR == k) { + op = c[0]; + } + else if (BVCONST == k) { + op = n; + } + else + FatalError("nsadfsdaf"); + + // CONSTANTBV::BitVector_to_Dec returns a signed representation by default. + // Prepend with zero to convert to unsigned. + + os << "bv"; + CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst()); + unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign); + CONSTANTBV::BitVector_Destroy(unsign); + os << str << "[" << op.GetValueWidth() << "]"; + CONSTANTBV::BitVector_Dispose(str); +} + +void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize) { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) { + os << ""; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = n.GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) { + SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) { + SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize); + return; + } + + //otherwise print it normally + Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) { + case BITVECTOR: + case BVCONST: + outputBitVec(n, os); + break; + + case SYMBOL: + n.nodeprint(os); + break; + case FALSE: + os << "false"; + break; + case TRUE: + os << "true"; + break; + + case BVSX: + case BVZX: { + unsigned int amount = GetUnsignedConst(c[1]); + if (BVZX == kind) + os << "(zero_extend["; + else + os << "(sign_extend["; + + os << amount << "]"; + SMTLIB_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + case BVEXTRACT: { + unsigned int upper = GetUnsignedConst(c[1]); + unsigned int lower = GetUnsignedConst(c[2]); + assert(upper >= lower); + os << "(extract[" << upper << ":" << lower << "] "; + SMTLIB_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + default: { + os << "(" << functionToSMTLIBName(kind); + + ASTVec::const_iterator iend = c.end(); + for (ASTVec::const_iterator i = c.begin(); i != iend; i++) { + os << " "; + SMTLIB_Print1(os, *i, 0, letize); + } + + os << ")"; + } + } +} + +// copied from Presentation Langauge printer. +ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) { + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + n.LetizeNode(); + + //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(); + + os << "(LET "; + //print the let var first + SMTLIB_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + SMTLIB_Print1(os, it->second, indentation, false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + + for (it++; it != itend; it++) { + os << "," << endl; + //print the let var first + SMTLIB_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + SMTLIB_Print1(os, it->second, indentation, false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << " IN " << endl; + SMTLIB_Print1(os, n, indentation, true); + os << ") "; + } + else + SMTLIB_Print1(os, n, indentation, false); + + os << endl; + return os; +} + +string functionToSMTLIBName(const Kind k) { + switch (k) { + case AND: + case BVAND: + case BVNAND: + case BVNOR: + case BVOR: + case BVSGE: + case BVSGT: + case BVSLE: + case BVSLT: + case BVSUB: + case BVXOR: + case ITE: + case NAND: + case NOR: + case NOT: + case OR: + case XOR: + case IFF: + return _kind_names[k]; + + case BVCONCAT: + return "concat"; + case BVDIV: + return "bvudiv"; + case BVGT: + return "bvugt"; + case BVGE: + return "bvuge"; + case BVLE: + return "bvule"; + case BVLEFTSHIFT: + return "bvshl"; + case BVLT: + return "bvult"; + case BVMOD: + return "bvurem"; + case BVMULT: + return "bvmul"; + case BVNEG: + return "bvnot"; // CONFUSSSSINNG. (1/2) + case BVPLUS: + return "bvadd"; + case BVRIGHTSHIFT: + return "bvlshr"; // logical + case BVSRSHIFT: + return "bvashr"; // arithmetic. + case BVUMINUS: + return "bvneg"; // CONFUSSSSINNG. (2/2) + case EQ: + return "="; + case READ: + return "select"; + case WRITE: + return "store"; + case SBVDIV: + return "bvsdiv"; + case SBVREM: + return "bvsrem"; + + default: { + cerr << "Unknown name when outputting:"; + FatalError(_kind_names[k]); + return ""; // to quieten compiler/ + } + } +} + +} diff --git a/AST/printer/dotPrinter.cpp b/AST/printer/dotPrinter.cpp new file mode 100644 index 0000000..0ffd9f2 --- /dev/null +++ b/AST/printer/dotPrinter.cpp @@ -0,0 +1,72 @@ +#include "printers.h" + +/* + * Outputs in DOT graph format. Can be layed out by the dotty/neato tools. + */ + +namespace printer { + +using std::string; +using namespace BEEV; + +void outputBitVec(const ASTNode n, ostream& os); + +void Dot_Print1(ostream &os, const ASTNode n, hash_set *alreadyOutput) { + + // check if this node has already been printed. If so return. + if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) + return; + + alreadyOutput->insert(n.GetNodeNum()); + + os << "n" << n.GetNodeNum() << "[label =\""; + switch(n.GetKind()) + { + case SYMBOL: + n.nodeprint(os); + break; + + case BITVECTOR: + case BVCONST: + outputBitVec(n, os); + break; + + default: + os << _kind_names[n.GetKind()]; + } + + + os << "\"];" << endl; + + + // print the edges to each child. + ASTVec ch = n.GetChildren(); + ASTVec::iterator itend = ch.end(); + int i =0; + for(ASTVec::iterator it = ch.begin(); it < itend; it++) + { + os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl; + } + + // print each of the children. + for(ASTVec::iterator it = ch.begin(); it < itend; it++) + { + Dot_Print1(os, *it, alreadyOutput); + } +} + +ostream& Dot_Print(ostream &os, const ASTNode n) { + + os << "digraph G{" << endl; + + // create hashmap to hold integers (node numbers). + hash_set alreadyOutput; + + Dot_Print1(os, n, &alreadyOutput); + + os << "}" << endl; + + return os; +} + +} diff --git a/AST/printer/printers.h b/AST/printer/printers.h new file mode 100644 index 0000000..fb99658 --- /dev/null +++ b/AST/printer/printers.h @@ -0,0 +1,17 @@ +#ifndef PRINTERS_H_ +#define PRINTERS_H_ + +#include "../AST.h" +#include "../ASTUtil.h" +#include "../ASTKind.h" + + +namespace printer +{ + + ostream& Dot_Print(ostream &os, const BEEV::ASTNode n); + ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation=0); + ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation=0); +} + +#endif /* PRINTERS_H_ */ diff --git a/Makefile.common b/Makefile.common index 3200510..d160e62 100644 --- a/Makefile.common +++ b/Makefile.common @@ -43,7 +43,7 @@ else CFLAGS = $(CFLAGS_BASE) endif -CXXFLAGS = $(CFLAGS) -Wall -DEXT_HASH_MAP -Wno-deprecated +CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated #CXXFLAGS = $(CFLAGS) -Wall -DTR1_UNORDERED_MAP #CXXFLAGS = $(CFLAGS) -Wall #LDFLAGS= -lstdc++ diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp index 32be6ec..75292ea 100644 --- a/c_interface/c_interface.cpp +++ b/c_interface/c_interface.cpp @@ -12,6 +12,7 @@ #include #include "fdstream.h" #include "../AST/AST.h" +#include "../AST/printer/printers.h" //These typedefs lower the effort of using the keyboard to type (too //many overloaded meanings of the word type) @@ -137,7 +138,7 @@ void vc_printExpr(VC vc, Expr e) { char * vc_printSMTLIB(VC vc, Expr e) { stringstream ss; - ((nodestar)e)->SMTLIB_Print(ss,0); + printer::SMTLIB_Print(ss,*((nodestar)e), 0); string s = ss.str(); char *copy = strdup(s.c_str()); return copy; @@ -168,7 +169,7 @@ void vc_printExprCCode(VC vc, Expr e) { cout << endl; // print constraints and assert - q.C_Print(cout); + printer::C_Print(cout,q); }