/******************************************************************** * AUTHORS: Vijay Ganesh, David L. Dill * * BEGIN DATE: November, 2005 * * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ // -*- c++ -*- #include "AST.h" namespace BEEV { //some global variables that are set through commandline options. it //is best that these variables remain global. Default values set //here // //collect statistics on certain functions bool stats = false; //print DAG nodes bool print_nodes = false; //tentative global var to allow for variable activity optimization //in the SAT solver. deprecated. bool variable_activity_optimize = false; //run STP in optimized mode bool optimize = true; //do sat refinement, i.e. underconstraint the problem, and feed to //SAT. if this works, great. else, add a set of suitable constraints //to re-constraint the problem correctly, and call SAT again, until //all constraints have been added. bool arrayread_refinement = true; //flag to control write refinement bool arraywrite_refinement = true; //check the counterexample against the original input to STP bool check_counterexample = false; //construct the counterexample in terms of original variable based //on the counterexample returned by SAT solver bool construct_counterexample = true; bool print_counterexample = false; //if this option is true then print the way dawson wants using a //different printer. do not use this printer. bool print_arrayval_declaredorder = false; //flag to decide whether to print "valid/invalid" or not bool print_output = false; //do linear search in the array values of an input array. experimental bool linear_search = false; //print the variable order chosen by the sat solver while it is //solving. bool print_sat_varorder = false; //turn on word level bitvector solver bool wordlevel_solve = true; //turn off XOR flattening bool xor_flatten = false; //the smtlib parser has been turned on bool smtlib_parser_enable = false; //print the input back bool print_STPinput_back = false; //global BEEVMGR for the parser BeevMgr * globalBeevMgr_for_parser; void (*vc_error_hdlr)(const char* err_msg) = NULL; /** This is reusable empty vector, for representing empty children arrays */ ASTVec _empty_ASTVec; //////////////////////////////////////////////////////////////// // ASTInternal members //////////////////////////////////////////////////////////////// /** Trivial but virtual destructor */ ASTInternal::~ASTInternal() { } //////////////////////////////////////////////////////////////// // ASTInterior members //////////////////////////////////////////////////////////////// /** Copy constructor */ // ASTInterior::ASTInterior(const ASTInterior &int_node) // { // _kind = int_node._kind; // _children = int_node._children; // } /** Trivial but virtual destructor */ ASTInterior::~ASTInterior() { } // FIXME: Darn it! I think this ends up copying the children twice! /** Either return an old node or create it if it doesn't exist. Note that nodes are physically allocated in the hash table. */ // There is an inelegance here that I don't know how to solve. I'd // like to heap allocate and do some other initialization on keys only // if they aren't in the hash table. It would be great if the // "insert" method took a "creator" class so that I could do that // between when it notices that the key is not there and when it // inserts it. Alternatively, it would be great if I could insert the // temporary key and replace it if it actually got inserted. But STL // hash_set doesn't have the creator feature and paternalistically // declares that keys are immutable, even though (it seems to me) that // they could be mutated if the hash value and eq values did not // change. ASTInterior *BeevMgr::LookupOrCreateInterior(ASTInterior *n_ptr) { ASTInteriorSet::iterator it; if ((it = _interior_unique_table.find(n_ptr)) == _interior_unique_table.end()) { // Make a new ASTInterior node // We want (NOT alpha) always to have alpha.nodenum + 1. if (n_ptr->GetKind() == NOT) { n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum()+1); } else { n_ptr->SetNodeNum(NewNodeNum()); } pair p = _interior_unique_table.insert(n_ptr); return *(p.first); } else // Delete the temporary node, and return the found node. delete n_ptr; return *it; } size_t ASTInterior::ASTInteriorHasher::operator() (const ASTInterior *int_node_ptr) const { //size_t hashval = 0; size_t hashval = ((size_t) int_node_ptr->GetKind()); const ASTVec &ch = int_node_ptr->GetChildren(); ASTVec::const_iterator iend = ch.end(); for (ASTVec::const_iterator i = ch.begin(); i != iend; i++) { //Using "One at a time hash" by Bob Jenkins hashval += i->Hash(); hashval += (hashval << 10); hashval ^= (hashval >> 6); } hashval += (hashval << 3); hashval ^= (hashval >> 11); hashval += (hashval << 15); return hashval; //return hashval += ((size_t) int_node_ptr->GetKind()); } void ASTInterior::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; _bm._interior_unique_table.erase(this); delete this; } //////////////////////////////////////////////////////////////// // ASTNode members //////////////////////////////////////////////////////////////// //ASTNode constructors are inlined in AST.h bool ASTNode::IsAlreadyPrinted() const { BeevMgr &bm = GetBeevMgr(); return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end()); } void ASTNode::MarkAlreadyPrinted() const { // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class? BeevMgr &bm = GetBeevMgr(); bm.AlreadyPrintedSet.insert(*this); } // Get the name from a symbol (char *). It's an error if kind != SYMBOL const char * const ASTNode::GetName() const { if (GetKind() != SYMBOL) FatalError("GetName: Called GetName on a non-symbol: ", *this); return ((ASTSymbol *) _int_node_ptr)->GetName(); } // Print in lisp format ostream &ASTNode::LispPrint(ostream &os, int indentation) const { // Clear the PrintMap BeevMgr& bm = GetBeevMgr(); bm.AlreadyPrintedSet.clear(); return LispPrint_indent(os, indentation); } // Print newline and indentation, then print the thing. ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const { os << endl << spaces(indentation); LispPrint1(os, indentation); return os; } /** Internal function to print in lisp format. Assume newline and indentation printed already before first line. Recursive calls will have newline & indent, though */ ostream &ASTNode::LispPrint1(ostream &os, int indentation) const { if (!IsDefined()) { os << ""; return os; } Kind kind = GetKind(); // FIXME: figure out how to avoid symbols with same names as kinds. // if (kind == READ) { // const ASTVec &children = GetChildren(); // children[0].LispPrint1(os, indentation); // os << "[" << children[1] << "]"; // } else if(kind == BVGETBIT) { const ASTVec &children = GetChildren(); // child 0 is a symbol. Print without the NodeNum. os << GetNodeNum() << ":"; children[0]._int_node_ptr->nodeprint(os); //os << "{" << children[1].GetBVConst() << "}"; os << "{"; children[1]._int_node_ptr->nodeprint(os); os << "}"; } else if (kind == NOT) { const ASTVec &children = GetChildren(); os << GetNodeNum() << ":"; os << "(NOT "; children[0].LispPrint1(os, indentation); os << ")"; } else if (Degree() == 0) { // Symbol or a kind with no children print as index:NAME if shared, // even if they have been printed before. os << GetNodeNum() << ":"; _int_node_ptr->nodeprint(os); // os << "(" << _int_node_ptr->_ref_count << ")"; // os << "{" << GetValueWidth() << "}"; } else if (IsAlreadyPrinted()) { // print non-symbols as "[index]" if seen before. os << "[" << GetNodeNum() << "]"; // << "(" << _int_node_ptr->_ref_count << ")"; } else { MarkAlreadyPrinted(); const ASTVec &children = GetChildren(); os << GetNodeNum() << ":" //<< "(" << _int_node_ptr->_ref_count << ")" << "(" << kind << " "; // os << "{" << GetValueWidth() << "}"; ASTVec::const_iterator iend = children.end(); for (ASTVec::const_iterator i = children.begin(); i != iend; i++) { i->LispPrint_indent(os, indentation+2); } os << ")"; } return os; } //print in PRESENTATION LANGUAGE // //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::PL_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.PL_Print1(os,indentation,false); os << " = "; //print the expr it->second.PL_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.PL_Print1(os,indentation,false); os << " = "; //print the expr it->second.PL_Print1(os,indentation,false); //update the second map for proper printing of LET bm.NodeLetVarMap1[it->second] = it->first; } os << " IN " << endl; PL_Print1(os,indentation, true); os << ") "; } else PL_Print1(os,indentation, false); //os << " )"; os << " "; return os; } //end of PL_Print() //traverse "*this", and construct "let variables" for terms that //occur more than once in "*this". void ASTNode::LetizeNode(void) const { Kind kind = this->GetKind(); if(kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE) return; //FIXME: this is ugly. BeevMgr& bm = GetBeevMgr(); const ASTVec &c = this->GetChildren(); for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++){ ASTNode ccc = *it; if(bm.PLPrintNodeSet.find(ccc) == bm.PLPrintNodeSet.end()){ //If branch: if *it is not in NodeSet then, // //1. add it to NodeSet // //2. Letize its childNodes //FIXME: Fetching BeevMgr is annoying. Can we put this in //some kind of a printer class bm.PLPrintNodeSet.insert(ccc); //debugging //cerr << ccc; ccc.LetizeNode(); } else{ Kind k = ccc.GetKind(); if(k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE) continue; //0. Else branch: Node has been seen before // //1. Check if the node has a corresponding letvar in the //1. NodeLetVarMap. // //2. if no, then create a new var and add it to the //2. NodeLetVarMap if(bm.NodeLetVarMap.find(ccc) == bm.NodeLetVarMap.end()) { //Create a new symbol. Get some name. if it conflicts with a //declared name, too bad. int sz = bm.NodeLetVarMap.size(); ostringstream oss; oss << "let_k_" << sz; ASTNode CurrentSymbol = bm.CreateSymbol(oss.str().c_str()); CurrentSymbol.SetValueWidth(this->GetValueWidth()); CurrentSymbol.SetIndexWidth(this->GetIndexWidth()); /* If for some reason the variable being created here is * already declared by the user then the printed output will * not be a legal input to the system. too bad. I refuse to * check for this. [Vijay is the author of this comment.] */ bm.NodeLetVarMap[ccc] = CurrentSymbol; std::pair node_letvar_pair(CurrentSymbol,ccc); bm.NodeLetVarVec.push_back(node_letvar_pair); } } } } //end of LetizeNode() void ASTNode::PL_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]).PL_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]).PL_Print1(os,indentation,letize); return; } //otherwise print it normally Kind kind = GetKind(); const ASTVec &c = GetChildren(); switch(kind) { case BVGETBIT: c[0].PL_Print1(os,indentation,letize); os << "{"; c[1].PL_Print1(os,indentation,letize); os << "}"; break; case BITVECTOR: os << "BITVECTOR("; unsigned char * str; str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); os << str << ")"; CONSTANTBV::BitVector_Dispose(str); break; case BOOLEAN: os << "BOOLEAN"; break; case FALSE: case TRUE: os << kind; break; case BVCONST: case SYMBOL: _int_node_ptr->nodeprint(os); break; case READ: c[0].PL_Print1(os, indentation,letize); os << "["; c[1].PL_Print1(os,indentation,letize); os << "]"; break; case WRITE: os << "("; c[0].PL_Print1(os,indentation,letize); os << " WITH ["; c[1].PL_Print1(os,indentation,letize); os << "] := "; c[2].PL_Print1(os,indentation,letize); os << ")"; os << endl; break; case BVUMINUS: os << kind << "( "; c[0].PL_Print1(os,indentation,letize); os << ")"; break; case NOT: os << "NOT("; c[0].PL_Print1(os,indentation,letize); os << ") " << endl; break; case BVNEG: os << " ~("; c[0].PL_Print1(os,indentation,letize); os << ")"; break; case BVCONCAT: os << "("; c[0].PL_Print1(os,indentation,letize); os << " @ "; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case BVOR: os << "("; c[0].PL_Print1(os,indentation,letize); os << " | "; c[1].PL_Print1(os,indentation,letize); os << ")"; break; case BVAND: os << "("; c[0].PL_Print1(os,indentation,letize); os << " & "; c[1].PL_Print1(os,indentation,letize); os << ")"; break; case BVEXTRACT: c[0].PL_Print1(os,indentation,letize); os << "["; os << GetUnsignedConst(c[1]); os << ":"; os << GetUnsignedConst(c[2]); os << "]"; break; case BVLEFTSHIFT: os << "("; c[0].PL_Print1(os,indentation,letize); os << " << "; os << GetUnsignedConst(c[1]); os << ")"; break; case BVRIGHTSHIFT: os << "("; c[0].PL_Print1(os,indentation,letize); os << " >> "; os << GetUnsignedConst(c[1]); os << ")"; break; case BVMULT: case BVSUB: case BVPLUS: case SBVDIV: case SBVMOD: 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->PL_Print1(os,indentation,letize); } os << ")" << endl; break; case ITE: os << "IF("; c[0].PL_Print1(os,indentation,letize); os << ")" << endl; os << "THEN "; c[1].PL_Print1(os,indentation,letize); os << endl << "ELSE "; c[2].PL_Print1(os,indentation,letize); os << endl << "ENDIF"; break; case BVLT: case BVLE: case BVGT: case BVGE: case BVXOR: case BVNAND: case BVNOR: case BVXNOR: os << kind << "("; c[0].PL_Print1(os,indentation,letize); os << ","; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case BVSLT: os << "SBVLT" << "("; c[0].PL_Print1(os,indentation,letize); os << ","; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case BVSLE: os << "SBVLE" << "("; c[0].PL_Print1(os,indentation,letize); os << ","; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case BVSGT: os << "SBVGT" << "("; c[0].PL_Print1(os,indentation,letize); os << ","; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case BVSGE: os << "SBVGE" << "("; c[0].PL_Print1(os,indentation,letize); os << ","; c[1].PL_Print1(os,indentation,letize); os << ")" << endl; break; case EQ: c[0].PL_Print1(os,indentation,letize); os << " = "; c[1].PL_Print1(os,indentation,letize); os << endl; break; case NEQ: c[0].PL_Print1(os,indentation,letize); os << " /= "; c[1].PL_Print1(os,indentation,letize); os << endl; break; case AND: case OR: case NAND: case NOR: case XOR: { os << "("; c[0].PL_Print1(os,indentation,letize); ASTVec::const_iterator it=c.begin(); ASTVec::const_iterator itend=c.end(); it++; for(;it!=itend;it++) { os << " " << kind << " "; it->PL_Print1(os,indentation,letize); os << endl; } os << ")"; break; } case IFF: os << "("; os << "("; c[0].PL_Print1(os,indentation,letize); os << ")"; os << " <=> "; os << "("; c[1].PL_Print1(os,indentation,letize); os << ")"; os << ")"; os << endl; break; case IMPLIES: os << "("; os << "("; c[0].PL_Print1(os,indentation,letize); os << ")"; os << " => "; os << "("; c[1].PL_Print1(os,indentation,letize); os << ")"; os << ")"; os << endl; break; case BVSX: os << kind << "("; c[0].PL_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("PL_Print1: printing not implemented for this kind: ",*this); break; } } //end of PL_Print1() //////////////////////////////////////////////////////////////// // BeevMgr members //////////////////////////////////////////////////////////////// ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children) { // create a new node. Children will be modified. ASTInterior *n_ptr = new ASTInterior(kind, *this); // insert all of children at end of new_children. ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); return n; } ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind, *this); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); return n; } ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind, *this); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); front_children.push_back(child1); ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); return n; } ASTNode BeevMgr::CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec & back_children) { ASTInterior *n_ptr = new ASTInterior(kind, *this); ASTVec &front_children = n_ptr->_children; front_children.push_back(child0); front_children.push_back(child1); front_children.push_back(child2); ASTNode n(CreateInteriorNode(kind, n_ptr, back_children)); return n; } ASTInterior *BeevMgr::CreateInteriorNode(Kind kind, // children array of this node will be modified. ASTInterior *n_ptr, const ASTVec & back_children) { // insert back_children at end of front_children ASTVec &front_children = n_ptr->_children; front_children.insert(front_children.end(), back_children.begin(), back_children.end()); // check for undefined nodes. ASTVec::const_iterator it_end = front_children.end(); for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++) { if (it->IsNull()) FatalError("CreateInteriorNode: Undefined childnode in CreateInteriorNode: ", ASTUndefined); } return LookupOrCreateInterior(n_ptr); } /** Trivial but virtual destructor */ ASTSymbol::~ASTSymbol() {} ostream &operator<<(ostream &os, const ASTNodeMap &nmap) { ASTNodeMap::const_iterator iend = nmap.end(); for (ASTNodeMap::const_iterator i = nmap.begin(); i!=iend; i++) { os << "Key: " << i->first << endl; os << "Value: " << i->second << endl; } return os; } //////////////////////////////////////////////////////////////// // BeevMgr member functions to create ASTSymbol and ASTBVConst //////////////////////////////////////////////////////////////// ASTNode BeevMgr::CreateSymbol(const char * const name) { ASTSymbol temp_sym(name, *this); ASTNode n(LookupOrCreateSymbol(temp_sym)); return n; } #ifndef NATIVE_C_ARITH //Create a ASTBVConst node ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst){ if(width > (sizeof(unsigned long long int)<<3) || width <= 0) FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); CBV bv = CONSTANTBV::BitVector_Create(width, true); unsigned long c_val = (0x00000000ffffffffLL) & bvconst; unsigned int copied = 0; // sizeof(unsigned long) returns the number of bytes in unsigned // long. In order to convert it to bits, we need to shift left by // 3. Hence, sizeof(unsigned long) << 3 //The algo below works as follows: It starts by copying the //lower-order bits of the input "bvconst" in chunks of size = //number of bits in unsigned long. The variable "copied" keeps //track of the number of chunks copied so far while(copied + (sizeof(unsigned long)<<3) < width){ CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val); bvconst = bvconst >> (sizeof(unsigned long) << 3); c_val = (0x00000000ffffffffLL) & bvconst; copied += sizeof(unsigned long) << 3; } CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val); return CreateBVConst(bv,width); } //Create a ASTBVConst node from std::string ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) { size_t width = strlen((const char *)strval); if(!(2 == base || 10 == base || 16 == base)){ FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base); } //FIXME Tim: Earlier versions of the code assume that the length of //binary strings is 32 bits. if(10 == base) width = 32; if(16 == base) width = width * 4; //checking if the input is in the correct format CBV bv = CONSTANTBV::BitVector_Create(width,true); CONSTANTBV::ErrCode e; if(2 == base){ e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*)strval); }else if(10 == base){ e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*)strval); }else if(16 == base){ e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*)strval); }else{ e = CONSTANTBV::ErrCode_Pars; } if(0 != e) { cerr << "CreateBVConst: " << BitVector_Error(e); FatalError("",ASTUndefined); } //FIXME return CreateBVConst(bv, width); } //FIXME Code currently assumes that it will destroy the bitvector passed to it ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width){ ASTBVConst temp_bvconst(bv, width, *this); ASTNode n(LookupOrCreateBVConst(temp_bvconst)); CONSTANTBV::BitVector_Destroy(bv); return n; } ASTNode BeevMgr::CreateZeroConst(unsigned width) { CBV z = CONSTANTBV::BitVector_Create(width, true); return CreateBVConst(z, width); } ASTNode BeevMgr::CreateOneConst(unsigned width) { CBV o = CONSTANTBV::BitVector_Create(width, true); CONSTANTBV::BitVector_increment(o); return CreateBVConst(o,width); } ASTNode BeevMgr::CreateTwoConst(unsigned width) { CBV two = CONSTANTBV::BitVector_Create(width, true); CONSTANTBV::BitVector_increment(two); CONSTANTBV::BitVector_increment(two); return CreateBVConst(two,width); } ASTNode BeevMgr::CreateMaxConst(unsigned width) { CBV max = CONSTANTBV::BitVector_Create(width, false); CONSTANTBV::BitVector_Fill(max); return CreateBVConst(max,width); } //To ensure unique BVConst nodes, lookup the node in unique-table //before creating a new one. ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { ASTBVConst *s_ptr = &s; // it's a temporary key. // Do an explicit lookup to see if we need to create a copy of the string. ASTBVConstSet::const_iterator it; if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { // Make a new ASTBVConst with duplicated string (can't assign // _name because it's const). Can cast the iterator to // non-const -- carefully. ASTBVConst * s_copy = new ASTBVConst(s); s_copy->SetNodeNum(NewNodeNum()); pair p = _bvconst_unique_table.insert(s_copy); return *p.first; } else{ // return symbol found in table. return *it; } } // Inline because we need to wait until unique_table is defined void ASTBVConst::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; _bm._bvconst_unique_table.erase(this); delete this; } // Get the value of bvconst from a bvconst. It's an error if kind != BVCONST CBV const ASTNode::GetBVConst() const { if(GetKind() != BVCONST) FatalError("GetBVConst: non bitvector-constant: ",*this); return ((ASTBVConst *) _int_node_ptr)->GetBVConst(); } #else //Create a ASTBVConst node ASTNode BeevMgr::CreateBVConst(const unsigned int width, const unsigned long long int bvconst) { if(width > 64 || width <= 0) FatalError("Fatal Error: CreateBVConst: trying to create a bvconst of width:", ASTUndefined, width); //64 bit mask unsigned long long int mask = 0xffffffffffffffffLL; mask = mask >> (64 - width); unsigned long long int bv = bvconst; bv = bv & mask; ASTBVConst temp_bvconst(bv, *this); temp_bvconst._value_width = width; ASTNode n(LookupOrCreateBVConst(temp_bvconst)); n.SetValueWidth(width); n.SetIndexWidth(0); return n; } //Create a ASTBVConst node from std::string ASTNode BeevMgr::CreateBVConst(const char* strval, int base) { if(!(base == 2 || base == 16 || base == 10)) FatalError("CreateBVConst: This base is not supported: ", ASTUndefined, base); if(10 != base) { unsigned int width = (base == 2) ? strlen(strval) : strlen(strval)*4; unsigned long long int val = strtoull(strval, NULL, base); ASTNode bvcon = CreateBVConst(width, val); return bvcon; } else { //this is an ugly hack to accomodate SMTLIB format //restrictions. SMTLIB format represents bitvector constants in //base 10 (what a terrible idea, but i have no choice but to //support it), and make an implicit assumption that the length //is 32 (another terrible idea). unsigned width = 32; unsigned long long int val = strtoull(strval, NULL, base); ASTNode bvcon = CreateBVConst(width, val); return bvcon; } } //To ensure unique BVConst nodes, lookup the node in unique-table //before creating a new one. ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s) { ASTBVConst *s_ptr = &s; // it's a temporary key. // Do an explicit lookup to see if we need to create a copy of the // string. ASTBVConstSet::const_iterator it; if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { // Make a new ASTBVConst. Can cast the iterator to non-const -- // carefully. unsigned int width = s_ptr->_value_width; ASTBVConst * s_ptr1 = new ASTBVConst(s_ptr->GetBVConst(), *this); s_ptr1->SetNodeNum(NewNodeNum()); s_ptr1->_value_width = width; pair p = _bvconst_unique_table.insert(s_ptr1); return *p.first; } else // return BVConst found in table. return *it; } // Inline because we need to wait until unique_table is defined void ASTBVConst::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; _bm._bvconst_unique_table.erase(this); delete this; } // Get the value of bvconst from a bvconst. It's an error if kind // != BVCONST unsigned long long int ASTNode::GetBVConst() const { if(GetKind() != BVCONST) FatalError("GetBVConst: non bitvector-constant: ", *this); return ((ASTBVConstTmp *) _int_node_ptr)->GetBVConst(); } ASTNode BeevMgr::CreateZeroConst(unsigned width) { return CreateBVConst(width,0); } ASTNode BeevMgr::CreateOneConst(unsigned width) { return CreateBVConst(width,1); } ASTNode BeevMgr::CreateTwoConst(unsigned width) { return CreateBVConst(width,2); } ASTNode BeevMgr::CreateMaxConst(unsigned width) { std::string s; s.insert(s.end(),width,'1'); return CreateBVConst(s.c_str(),2); } #endif // FIXME: _name is now a constant field, and this assigns to it // because it tries not to copy the string unless it needs to. How // do I avoid copying children in ASTInterior? Perhaps I don't! // Note: There seems to be a limitation of hash_set, in that insert // returns a const iterator to the value. That prevents us from // modifying the name (in a hash-preserving way) after the symbol is // inserted. FIXME: Is there a way to do this with insert? Need a // function to make a new object in the middle of insert. Read STL // documentation. ASTSymbol *BeevMgr::LookupOrCreateSymbol(ASTSymbol& s) { ASTSymbol *s_ptr = &s; // it's a temporary key. // Do an explicit lookup to see if we need to create a copy of the string. ASTSymbolSet::const_iterator it; if ((it = _symbol_unique_table.find(s_ptr)) == _symbol_unique_table.end()) { // Make a new ASTSymbol with duplicated string (can't assign // _name because it's const). Can cast the iterator to // non-const -- carefully. //std::string strname(s_ptr->GetName()); ASTSymbol * s_ptr1 = new ASTSymbol(strdup(s_ptr->GetName()), *this); s_ptr1->SetNodeNum(NewNodeNum()); s_ptr1->_value_width = s_ptr->_value_width; pair p = _symbol_unique_table.insert(s_ptr1); return *p.first; } else // return symbol found in table. return *it; } bool BeevMgr::LookupSymbol(ASTSymbol& s) { ASTSymbol* s_ptr = &s; // it's a temporary key. if(_symbol_unique_table.find(s_ptr) == _symbol_unique_table.end()) return false; else return true; } // Inline because we need to wait until unique_table is defined void ASTSymbol::CleanUp() { // cout << "Deleting node " << this->GetNodeNum() << endl; _bm._symbol_unique_table.erase(this); //FIXME This is a HUGE free to invoke. //TEST IT! free((char*) this->_name); delete this; } //////////////////////////////////////////////////////////////// // // IO manipulators for Lisp format printing of AST. // //////////////////////////////////////////////////////////////// // FIXME: Additional controls // * Print node numbers (addresses/nums) // * Printlength limit // * Printdepth limit /** Print a vector of ASTNodes in lisp format */ ostream &LispPrintVec(ostream &os, const ASTVec &v, int indentation) { // Print the children ASTVec::const_iterator iend = v.end(); for (ASTVec::const_iterator i = v.begin(); i != iend; i++) { i->LispPrint_indent(os, indentation); } return os; } // FIXME: Made non-ref in the hope that it would work better. void lp(ASTNode node) { cout << lisp(node) << endl; } void lpvec(const ASTVec &vec) { vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); LispPrintVec(cout, vec, 0); cout << endl; } // Copy constructor. Maintain _ref_count ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) { #ifndef SMTLIB if (n._int_node_ptr) { n._int_node_ptr->IncRef(); } #endif } /* FUNCTION: Typechecker for terms and formulas * * TypeChecker: Assumes that the immediate Children of the input * ASTNode have been typechecked. This function is suitable in * scenarios like where you are building the ASTNode Tree, and you * typecheck as you go along. It is not suitable as a general * typechecker */ void BeevMgr::BVTypeCheck(const ASTNode& n) { Kind k = n.GetKind(); //The children of bitvector terms are in turn bitvectors. ASTVec v = n.GetChildren(); if(is_Term_kind(k)) { switch(k) { case BVCONST: if(BITVECTOR_TYPE != n.GetType()) FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); break; case SYMBOL: return; case ITE: if(BOOLEAN_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType() && BITVECTOR_TYPE != n[2].GetType()) FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n); if(n[1].GetValueWidth() != n[2].GetValueWidth()) FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); if(n[1].GetIndexWidth() != n[2].GetIndexWidth()) FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n); break; case READ: if(n[0].GetIndexWidth() != n[1].GetValueWidth()) { cerr << "Length of indexwidth of array: " << n[0] << " is : " << n[0].GetIndexWidth() << endl; cerr << "Length of the actual index is: " << n[1] << " is : " << n[1].GetValueWidth() << endl; FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); } break; case WRITE: if(n[0].GetIndexWidth() != n[1].GetValueWidth()) FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n",n); if(n[0].GetValueWidth() != n[2].GetValueWidth()) FatalError("BVTypeCheck: valuewidth of array != length of actual value in the term t = \n",n); break; case BVOR: case BVAND: case BVXOR: case BVNOR: case BVNAND: case BVXNOR: case BVPLUS: case BVMULT: case BVDIV: case BVMOD: case BVSUB: { if(!(v.size() >= 2)) FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must have atleast two arguments\n",n); unsigned int width = n.GetValueWidth(); for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++){ if(width != it->GetValueWidth()) { cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith operators must be of equal length\n"; cerr << n << endl; cerr << "width of term:" << width << endl; cerr << "width of offending operand:" << it->GetValueWidth() << endl; FatalError("BVTypeCheck:Offending operand:\n",*it); } if(BITVECTOR_TYPE != it->GetType()) FatalError("BVTypeCheck: ChildNodes of bitvector-terms must be bitvectors\n",n); } break; } case BVSX: //in BVSX(n[0],len), the length of the BVSX term must be //greater than the length of n[0] if(n[0].GetValueWidth() >= n.GetValueWidth()) { FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n); } break; default: for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++) if(BITVECTOR_TYPE != it->GetType()) { cerr << "The type is: " << it->GetType() << endl; FatalError("BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n",n); } break; } switch(k) { case BVCONCAT: if(n.Degree() != 2) FatalError("BVTypeCheck: should have exactly 2 args\n",n); if(n.GetValueWidth() != n[0].GetValueWidth() + n[1].GetValueWidth()) FatalError("BVTypeCheck:BVCONCAT: lengths do not add up\n",n); break; case BVUMINUS: case BVNEG: if(n.Degree() != 1) FatalError("BVTypeCheck: should have exactly 1 args\n",n); break; case BVEXTRACT: if(n.Degree() != 3) FatalError("BVTypeCheck: should have exactly 3 args\n",n); if(!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind())) FatalError("BVTypeCheck: indices should be BVCONST\n",n); if(n.GetValueWidth() != GetUnsignedConst(n[1])- GetUnsignedConst(n[2])+1) FatalError("BVTypeCheck: length mismatch\n",n); break; case BVLEFTSHIFT: case BVRIGHTSHIFT: if(n.Degree() != 2) FatalError("BVTypeCheck: should have exactly 2 args\n",n); break; //case BVVARSHIFT: //case BVSRSHIFT: break; default: break; } } else { if(!(is_Form_kind(k) && BOOLEAN_TYPE == n.GetType())) FatalError("BVTypeCheck: not a formula:",n); switch(k){ case TRUE: case FALSE: case SYMBOL: return; case EQ: case NEQ: if(!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth())) { cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl; cerr << "valuewidth of rhs of EQ: " << n[1].GetValueWidth() << endl; cerr << "indexwidth of lhs of EQ: " << n[0].GetIndexWidth() << endl; cerr << "indexwidth of rhs of EQ: " << n[1].GetIndexWidth() << endl; FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); } break; case BVLT: case BVLE: case BVGT: case BVGE: case BVSLT: case BVSLE: case BVSGT: case BVSGE: if(BITVECTOR_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType()) FatalError("BVTypeCheck: terms in atomic formulas must be bitvectors",n); if(n[0].GetValueWidth() != n[1].GetValueWidth()) FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); if(n[0].GetIndexWidth() != n[1].GetIndexWidth()) FatalError("BVTypeCheck: terms in atomic formulas must be of equal length",n); break; case NOT: if(1 != n.Degree()) FatalError("BVTypeCheck: NOT formula can have exactly one childNode",n); break; case AND: case OR: case XOR: case NAND: case NOR: if(2 > n.Degree()) FatalError("BVTypeCheck: AND/OR/XOR/NAND/NOR: must have atleast 2 ChildNodes",n); break; case IFF: case IMPLIES: if(2 != n.Degree()) FatalError("BVTypeCheck:IFF/IMPLIES must have exactly 2 ChildNodes",n); break; case ITE: if(3 != n.Degree()) FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes",n); break; default: FatalError("BVTypeCheck: Unrecognized kind: ",ASTUndefined); break; } } } //End of TypeCheck function //add an assertion to the current logical context void BeevMgr::AddAssert(const ASTNode& assert) { if(!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) { FatalError("AddAssert:Trying to assert a non-formula:",assert); } ASTVec * v; //if the stack of ASTVec is not empty, then take the top ASTVec //and add the input assert to it if(!_asserts.empty()) { v = _asserts.back(); //v->push_back(TransformFormula(assert)); v->push_back(assert); } else { //else create a logical context, and add it to the top of the //stack v = new ASTVec(); //v->push_back(TransformFormula(assert)); v->push_back(assert); _asserts.push_back(v); } } void BeevMgr::Push(void) { ASTVec * v; v = new ASTVec(); _asserts.push_back(v); } void BeevMgr::Pop(void) { if(!_asserts.empty()) { ASTVec * c = _asserts.back(); //by calling the clear function we ensure that the ref count is //decremented for the ASTNodes stored in c c->clear(); delete c; _asserts.pop_back(); } } void BeevMgr::AddQuery(const ASTNode& q) { //_current_query = TransformFormula(q); //cerr << "\nThe current query is: " << q << endl; _current_query = q; } const ASTNode BeevMgr::PopQuery() { ASTNode q = _current_query; _current_query = ASTTrue; return q; } const ASTNode BeevMgr::GetQuery() { return _current_query; } const ASTVec BeevMgr::GetAsserts(void) { vector::iterator it = _asserts.begin(); vector::iterator itend = _asserts.end(); ASTVec v; for(;it!=itend;it++) { if(!(*it)->empty()) v.insert(v.end(),(*it)->begin(),(*it)->end()); } return v; } //Create a new variable of ValueWidth 'n' ASTNode BeevMgr::NewArrayVar(unsigned int index, unsigned int value) { std:: string c("v"); char d[32]; sprintf(d,"%d",_symbol_count++); std::string ccc(d); c += "_writearray_" + ccc; ASTNode CurrentSymbol = CreateSymbol(c.c_str()); CurrentSymbol.SetValueWidth(value); CurrentSymbol.SetIndexWidth(index); return CurrentSymbol; } //end of NewArrayVar() //Create a new variable of ValueWidth 'n' ASTNode BeevMgr::NewVar(unsigned int value) { std:: string c("v"); char d[32]; sprintf(d,"%d",_symbol_count++); std::string ccc(d); c += "_new_stp_var_" + ccc; ASTNode CurrentSymbol = CreateSymbol(c.c_str()); CurrentSymbol.SetValueWidth(value); CurrentSymbol.SetIndexWidth(0); _introduced_symbols.insert(CurrentSymbol); return CurrentSymbol; } //end of NewVar() //prints statistics for the ASTNode void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a){ if(!stats) return; StatInfoSet.clear(); //print node size: cout << endl << "Printing: " << c; if(print_nodes) { //a.PL_Print(cout,0); //cout << endl; cout << a << endl; } cout << "Node size is: "; cout << NodeSize(a) << endl << endl; } unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) { if(clearStatInfo) StatInfoSet.clear(); ASTNodeSet::iterator it; if((it = StatInfoSet.find(a)) != StatInfoSet.end()) //has already been counted return 0; //record that you have seen this node already StatInfoSet.insert(a); //leaf node has a size of 1 if(a.Degree() == 0) return 1; unsigned newn = 1; ASTVec c = a.GetChildren(); for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) newn += NodeSize(*it); return newn; } void BeevMgr::ClearAllTables(void) { //clear all tables before calling toplevelsat _ASTNode_to_SATVar.clear(); _SATVar_to_AST.clear(); for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { delete it->second; } _ASTNode_to_Bitvector.clear(); /* OLD Destructor * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { ivec->second.clear(); }*/ /*What should I do here? For ASTNodes? * for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { ivec->second.clear(); }*/ BBTermMemo.clear(); BBFormMemo.clear(); NodeLetVarMap.clear(); NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); AlreadyPrintedSet.clear(); SimplifyMap.clear(); SimplifyNegMap.clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); TransformMap.clear(); _letid_expr_map.clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); StatInfoSet.clear(); // for(std::vector::iterator it=_asserts.begin(), // itend=_asserts.end();it!=itend;it++) { // (*it)->clear(); // } _asserts.clear(); for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset!=iset_end;iset++) { iset->second.clear(); } _arrayname_readindices.clear(); _interior_unique_table.clear(); _symbol_unique_table.clear(); _bvconst_unique_table.clear(); } void BeevMgr::ClearAllCaches(void) { //clear all tables before calling toplevelsat _ASTNode_to_SATVar.clear(); _SATVar_to_AST.clear(); for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { delete it->second; } _ASTNode_to_Bitvector.clear(); /*OLD destructor * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { ivec->second.clear(); }*/ /*What should I do here? *for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { ivec->second.clear(); }*/ BBTermMemo.clear(); BBFormMemo.clear(); NodeLetVarMap.clear(); NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); AlreadyPrintedSet.clear(); SimplifyMap.clear(); SimplifyNegMap.clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); TransformMap.clear(); _letid_expr_map.clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); StatInfoSet.clear(); for(ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset!=iset_end;iset++) { iset->second.clear(); } _arrayname_readindices.clear(); //_interior_unique_table.clear(); //_symbol_unique_table.clear(); //_bvconst_unique_table.clear(); } void BeevMgr::CopySolverMap_To_CounterExample(void) { if(!SolverMap.empty()) { CounterExampleMap.insert(SolverMap.begin(),SolverMap.end()); } } void FatalError(const char * str, const ASTNode& a, int w) { if(a.GetKind() != UNDEFINED) { cerr << "Fatal Error: " << str << endl << a << endl; cerr << w << endl; } else { cerr << "Fatal Error: " << str << endl; cerr << w << endl; } if (vc_error_hdlr) vc_error_hdlr(str); exit(-1); //assert(0); } void FatalError(const char * str) { cerr << "Fatal Error: " << str << endl; if (vc_error_hdlr) vc_error_hdlr(str); exit(-1); //assert(0); } //Variable Order Printer: A global function which converts a MINISAT //var into a ASTNODE var. It then prints this var along with //variable order dcisions taken by MINISAT. void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision_level, int polarity) { BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; cout << spaces(decision_level); if(polarity) { cout << "!"; } vv.PL_Print(cout,0); cout << endl; } void SortByExprNum(ASTVec& v) { sort(v.begin(), v.end(), exprless); } bool isAtomic(Kind kind) { if(TRUE == kind || FALSE == kind || EQ == kind || NEQ == kind || BVLT == kind || BVLE == kind || BVGT == kind || BVGE == kind || BVSLT == kind || BVSLE == kind || BVSGT == kind || BVSGE == kind || SYMBOL == kind || BVGETBIT == kind) return true; return false; } BeevMgr::~BeevMgr() { ClearAllTables(); } }; // end namespace