diff --git a/src/goto-cc/xml_binaries/read_goto_object.cpp b/src/goto-cc/xml_binaries/read_goto_object.cpp deleted file mode 100644 index 24dde49bec9..00000000000 --- a/src/goto-cc/xml_binaries/read_goto_object.cpp +++ /dev/null @@ -1,135 +0,0 @@ -/*******************************************************************\ - -Module: Read goto object files. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Read goto object files. - -#include "read_goto_object.h" - -#include -#include -#include -#include - -#define XML_VERSION "1.4" - -#include - -#include "xml_goto_function_hashing.h" -#include "xml_irep_hashing.h" -#include "xml_symbol_hashing.h" - -/// reads a goto object xml file back into a symbol and a function table -/// \par parameters: input stream, symbol_table, functions -/// \return true on error, false otherwise -bool read_goto_object( - std::istream &in, - const std::string &filename, - symbol_tablet &symbol_table, - goto_functionst &functions, - message_handlert &message_handler) -{ - messaget message(message_handler); - - xml_parser.clear(); - xml_parser.filename = filename; - xml_parser.in = ∈ - xml_parser.set_message_handler(message_handler); - - if(xml_parser.parse()) - return true; - - xmlt &top = xml_parser.parse_tree.element; - - if(top.get_attribute("version")!=XML_VERSION) - { - message.error() << - "The input was compiled with a different version of " - "goto-cc, please recompile." << messaget::eom; - return true; - } - - xml_irep_convertt::ireps_containert ic; - xml_irep_convertt irepconverter(ic); - xml_symbol_convertt symbolconverter(ic); - xml_goto_function_convertt gfconverter(ic); - - if(top.name.substr(0, 11)=="goto-object") - { - for(xmlt::elementst::const_iterator - sec_it=top.elements.begin(); - sec_it != top.elements.end(); - sec_it++) - { - xmlt sec = *sec_it; - if(sec.name=="irep_hash_map") - { - for(xmlt::elementst::const_iterator - irep_it = sec.elements.begin(); - irep_it != sec.elements.end(); - irep_it++) - { - irept i; - irepconverter.convert(*irep_it, i); - irepconverter.insert(irep_it->get_attribute("id"), i); - } - } - else if(sec.name=="symbols") - { - for(xmlt::elementst::const_iterator - sym_it = sec.elements.begin(); - sym_it != sec.elements.end(); - sym_it++) - { - symbolt symbol; - symbolconverter.convert(*sym_it, symbol); - // std::cout << "Adding Symbol: " << symbol.name << '\n'; - if(!symbol.is_type && - symbol.type.id()=="code") - { - // makes sure there is an empty function - // for this symbol. if we got code for it, - // it will be added later on. - functions.function_map[symbol.name].type= - to_code_type(symbol.type); - } - symbol_table.add(symbol); - } - } - else if(sec.name=="functions") - { - for(xmlt::elementst::const_iterator - fun_it = sec.elements.begin(); - fun_it != sec.elements.end(); - fun_it++) - { - std::string fname = fun_it->get_attribute("name"); - // std::cout << "Adding function body: " << fname << '\n'; - goto_functionst::goto_functiont &f = functions.function_map[fname]; - gfconverter.convert(*fun_it, f); - } - } - else - { - message.error() << "Unknown Section '" << sec.name - << "' in object file." << messaget::eom; - return true; - } - } - } - else - { - message.error() << "no goto-object" << messaget::eom; - return true; - } - - xml_parser.clear(); - return false; -} diff --git a/src/goto-cc/xml_binaries/read_goto_object.h b/src/goto-cc/xml_binaries/read_goto_object.h deleted file mode 100644 index 36981051008..00000000000 --- a/src/goto-cc/xml_binaries/read_goto_object.h +++ /dev/null @@ -1,28 +0,0 @@ -/*******************************************************************\ - -Module: Read goto object files. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Read goto object files. - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_READ_GOTO_OBJECT_H -#define CPROVER_GOTO_CC_XML_BINARIES_READ_GOTO_OBJECT_H - -#include -#include -#include - -bool read_goto_object( - std::istream &in, - const std::string &filename, - symbol_tablet &symbol_table, - goto_functionst &functions, - message_handlert &msg_hndlr); - -#endif // CPROVER_GOTO_CC_XML_BINARIES_READ_GOTO_OBJECT_H diff --git a/src/goto-cc/xml_binaries/xml_goto_function.cpp b/src/goto-cc/xml_binaries/xml_goto_function.cpp deleted file mode 100644 index 7475a990a4b..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_function.cpp +++ /dev/null @@ -1,38 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto functions to xml structures and back. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto functions to xml structures and back. - -#include "xml_goto_function.h" - -#include - -#include "xml_goto_program.h" - -/// takes a goto_function and creates an according xml structure -/// \par parameters: goto_function and an xml node -/// \return none -void convert(const goto_functionst::goto_functiont &function, xmlt &xml) -{ - if(function.body_available) - convert(function.body, xml); -} - -/// constructs the goto_function according to the information in the xml -/// structure. -/// \par parameters: xml structure and a goto_function to fill -/// \return none -void convert(const xmlt &xml, goto_functionst::goto_functiont &function) -{ - function.body.clear(); - convert(xml, function.body); - // don't forget to fix the functions type via the symbol table! -} diff --git a/src/goto-cc/xml_binaries/xml_goto_function.h b/src/goto-cc/xml_binaries/xml_goto_function.h deleted file mode 100644 index b15722976b8..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_function.h +++ /dev/null @@ -1,23 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto functions into xml structures and back - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto functions into xml structures and back - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_H - -#include -#include - -void convert(const xmlt&, goto_functionst::goto_functiont&); -void convert(const goto_functionst::goto_functiont&, xmlt&); - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_H diff --git a/src/goto-cc/xml_binaries/xml_goto_function_hashing.cpp b/src/goto-cc/xml_binaries/xml_goto_function_hashing.cpp deleted file mode 100644 index a0a2f428dab..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_function_hashing.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto functions to xml structures and back (with irep - hashing) - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto functions to xml structures and back (with irep hashing) - -#include "xml_goto_function_hashing.h" - -#include "xml_goto_program_hashing.h" - -/// takes a goto_function and creates an according xml structure -/// \par parameters: goto_function and an xml node -/// \return none -void xml_goto_function_convertt::convert( - const goto_functionst::goto_functiont &function, - xmlt &xml) -{ - xml_goto_program_convertt gpconverter(ireps_container); - if(function.body_available) - gpconverter.convert(function.body, xml); -} - -/// constructs the goto_function according to the information in the xml -/// structure. -/// \par parameters: xml structure and a goto_function to fill -/// \return none -void xml_goto_function_convertt::convert( - const xmlt &xml, - goto_functionst::goto_functiont &function) -{ - xml_goto_program_convertt gpconverter(ireps_container); - function.body.clear(); - gpconverter.convert(xml, function.body); - // don't forget to fix the functions type via the symbol table! -} diff --git a/src/goto-cc/xml_binaries/xml_goto_function_hashing.h b/src/goto-cc/xml_binaries/xml_goto_function_hashing.h deleted file mode 100644 index e558a702c68..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_function_hashing.h +++ /dev/null @@ -1,38 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto functions into xml structures and back (with irep - hashing). - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto functions into xml structures and back (with irep hashing). - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_HASHING_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_HASHING_H - -#include -#include - -#include "xml_irep_hashing.h" - -class xml_goto_function_convertt -{ -private: - xml_irep_convertt::ireps_containert &ireps_container; - -public: - explicit xml_goto_function_convertt(xml_irep_convertt::ireps_containert &ic): - ireps_container(ic) - { - } - - void convert(const xmlt&, goto_functionst::goto_functiont&); - void convert(const goto_functionst::goto_functiont&, xmlt&); -}; - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_FUNCTION_HASHING_H diff --git a/src/goto-cc/xml_binaries/xml_goto_program.cpp b/src/goto-cc/xml_binaries/xml_goto_program.cpp deleted file mode 100644 index 1f12fcff98f..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_program.cpp +++ /dev/null @@ -1,405 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto programs to xml structures and back. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto programs to xml structures and back. - -#include "xml_goto_program.h" - -#include -#include - -#include - -/// constructs the xml structure according to the goto program and the namespace -/// into the given xml object. -/// \par parameters: goto program, namespace and an xml structure to fill -/// \return none -void convert(const goto_programt &goto_program, - xmlt &xml) -{ - std::stringstream tmp; - // std::cout << "TNO: " << goto_program.target_numbers.size() << '\n'; - - for(const auto &inst : goto_program.instructions) - { - xmlt &ins=xml.new_element("instruction"); - - if(!inst.location.is_nil()) - { - convert(inst.location, ins.new_element("location")); - } - - if(!inst.labels.empty()) - { - xmlt &lbl=ins.new_element("labels"); - for(goto_programt::instructiont::labelst::const_iterator - l_it=inst.labels.begin(); - l_it!=inst.labels.end(); - l_it++) - { - lbl.new_element("label").set_attribute("name", id2string(*l_it)); - } - } - - - if(inst.target_number!=0) - { - // std::cout << "Targetlabel found!\n"; - tmp.str(""); - tmp << inst.target_number; - ins.set_attribute("targetlabel", tmp.str()); - } - - switch(inst.type) - { - case GOTO: - { - ins.name="goto"; - if(!inst.guard.is_true()) - { - xmlt &g=ins.new_element("guard"); - convert(inst.guard, g); - } - xmlt &tgt=ins.new_element("targets"); - for(goto_programt::instructiont::targetst::const_iterator - gt_it=inst.targets.begin(); - gt_it!=inst.targets.end(); - gt_it++) - { - tmp.str(""); - tmp << (*gt_it)->target_number; - tgt.new_element("target").data=tmp.str(); - } - break; - } - - case ASSUME: - { - ins.name="assume"; - xmlt &g=ins.new_element("guard"); - convert(inst.guard, g); - - const irep_idt &comment=inst.location.get("comment"); - - if(comment!="") - ins.new_element("comment").data=id2string(comment); - - break; - } - - case ASSERT: - { - ins.name="assert"; - xmlt &g=ins.new_element("guard"); - convert(inst.guard, g); - const irep_idt &comment=inst.location.get("comment"); - - if(comment!="") - ins.new_element("comment").data=id2string(comment); - - break; - } - - case SKIP: - ins.name="skip"; - break; - - case END_FUNCTION: - ins.name="end_function"; - break; - - case LOCATION: - ins.name="location"; - break; - - case DEAD: - ins.name="dead"; - break; - - case ATOMIC_BEGIN: - ins.name="atomic_begin"; - break; - - case ATOMIC_END: - ins.name="atomic_end"; - break; - - case RETURN: - { - ins.name="return"; - xmlt &c=ins.new_element("code"); - convert(inst.code, c); - break; - } - - case OTHER: - { - ins.name="instruction"; - xmlt &c=ins.new_element("code"); - convert(inst.code, c); - break; - } - - case ASSIGN: - { - ins.name="assign"; - xmlt &c=ins.new_element("code"); - convert(inst.code, c); - break; - } - - case FUNCTION_CALL: - { - ins.name="functioncall"; - xmlt &c=ins.new_element("code"); - convert(inst.code, c); - break; - } - - case START_THREAD: - { - ins.name="thread_start"; - xmlt &tgt=ins.new_element("targets"); - if(inst.targets.size()==1) - { - tmp.str(""); - tmp << inst.targets.front()->target_number; - tgt.new_element("target").data=tmp.str(); - } - break; - } - - case END_THREAD: - ins.name="thread_end"; - break; - - default: - ins.name="unknown"; - break; - } - - if(inst.function!="") - { - xmlt &fnc=ins.new_element("function"); - fnc.data=id2string(inst.function); - } - } -} - -/// constructs the goto program according to the xml structure and the namespace -/// into the given goto program object. -/// \par parameters: an xml structure, namespace, function symbol -/// and a goto program to fill -/// \return none -void convert(const xmlt &xml, goto_programt &goto_program) -{ - goto_program.clear(); - goto_programt::instructionst &instructions = goto_program.instructions; - - xmlt::elementst::const_iterator it = xml.elements.begin(); - for(; it != xml.elements.end(); it++) - { - goto_programt::targett inst = goto_program.add_instruction(); - inst->targets.clear(); - - if(it->name=="goto") - { - inst->type = GOTO; - } - else if(it->name=="assume") - { - inst->type = ASSUME; - } - else if(it->name=="assert") - { - inst->type = ASSERT; - } - else if(it->name=="skip") - { - inst->type = SKIP; - } - else if(it->name=="end_function") - { - inst->type = END_FUNCTION; - } - else if(it->name=="location") - { - inst->type = LOCATION; - } - else if(it->name=="dead") - { - inst->type = DEAD; - } - else if(it->name=="atomic_begin") - { - inst->type = ATOMIC_BEGIN; - } - else if(it->name=="atomic_end") - { - inst->type = ATOMIC_END; - } - else if(it->name=="return") - { - inst->make_return(); - } - else if(it->name=="instruction") // OTHER - { - inst->make_other(); - } - else if(it->name=="assign") - { - inst->make_other(); - inst->type=ASSIGN; - } - else if(it->name=="functioncall") - { - inst->make_other(); - inst->type=FUNCTION_CALL; - } - else if(it->name=="thread_start") - { - inst->type = START_THREAD; - } - else if(it->name=="thread_end") - { - inst->type = END_THREAD; - } - else - { - std::cout << "Unknown instruction type encountered (" << it->name - << ")\n"; - return; - } - - xmlt::elementst::const_iterator eit = it->elements.begin(); - for(; eit != it->elements.end(); eit++) - { - if(eit->name=="location") - { - convert(*eit, inst->location); - } - else if(eit->name=="variables") - { - } - else if(eit->name=="labels") - { - xmlt::elementst::const_iterator lit = eit->elements.begin(); - for(; lit != eit->elements.end(); lit++) - { - if(lit->name=="label") - { - std::string ls = lit->get_attribute("name"); - inst->labels.push_back(ls); - } - else - { - std::cout << "Unknown node in labels section.\n"; - return; - } - } - } - else if(eit->name=="guard") - { - inst->guard.remove("value"); - convert(*eit, inst->guard); - } - else if(eit->name=="code") - { - convert(*eit, inst->code); - } - else if(eit->name=="targets") - { - // Don't do anything here, we'll need a second run for that - } - else if(eit->name=="comment") - { - inst->location.set("comment", eit->data); - } - else if(eit->name=="function") - { - inst->function = eit->data; - } - } - } - - // assign line numbers - goto_program.compute_location_numbers(); - - // second run, for targets - goto_programt::targett ins_it = instructions.begin(); - it = xml.elements.begin(); - for(; it != xml.elements.end() && ins_it!=instructions.end(); it++) - { - xmlt::elementst::const_iterator eit = it->elements.begin(); - for(; eit != it->elements.end(); eit++) - { - if(eit->name=="targets") - { - xmlt::elementst::const_iterator tit = eit->elements.begin(); - for(; tit != eit->elements.end(); tit++) - { - if(tit->name=="target") - { - goto_programt::targett tins = - find_instruction(xml, instructions, tit->data); - if(tins != instructions.end()) - { - // Here we insert the iterators that somehow seem - // to be strange afterwards (see line 87) - ins_it->targets.push_back(tins); - } - else - { - std::cout << "Warning: instruction not found when " - "resolving target links.\n"; - } - } - else - { - std::cout << "Unknown node in targets section.\n"; - return; - } - } - } - } - ins_it++; - } - - // resolve links - goto_program.update(); - - // std::cout << "TNI: " << goto_program.target_numbers.size() << '\n'; -} - -/// finds the index of the instruction labelled with the given target label in -/// the given xml-program -/// \par parameters: a target label string, the instructions list and an xml -/// program -/// \return iterator to the found instruction or .end() -goto_programt::targett -find_instruction( - const xmlt &xml, - goto_programt::instructionst &instructions, - const irep_idt &label) -{ - goto_programt::targett ins_it=instructions.begin(); - xmlt::elementst::const_iterator it=xml.elements.begin(); - - for(; it != xml.elements.end() && ins_it!=instructions.end(); it++) - { - if(label==it->get_attribute("targetlabel")) - return ins_it; - - ins_it++; - } - - return instructions.end(); -} diff --git a/src/goto-cc/xml_binaries/xml_goto_program.h b/src/goto-cc/xml_binaries/xml_goto_program.h deleted file mode 100644 index cd5cb4e6c17..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_program.h +++ /dev/null @@ -1,33 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto programs into xml structures and back - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto programs into xml structures and back - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_H - -#include -#include - -void convert( - const goto_programt&, - xmlt&); - -void convert( - const xmlt&, - goto_programt&); - -goto_programt::targett find_instruction( - const xmlt &, - goto_programt::instructionst &, - const irep_idt &); - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_H diff --git a/src/goto-cc/xml_binaries/xml_goto_program_hashing.cpp b/src/goto-cc/xml_binaries/xml_goto_program_hashing.cpp deleted file mode 100644 index 129f90dd9d6..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_program_hashing.cpp +++ /dev/null @@ -1,403 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto programs to xml structures and back (with irep - hashing) - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto programs to xml structures and back (with irep hashing) - -#include "xml_goto_program_hashing.h" - -#include -#include - -#include "xml_irep_hashing.h" - -/// constructs the xml structure according to the goto program and the namespace -/// into the given xml object. -/// \par parameters: goto program and an xml structure to fill -/// \return none -void xml_goto_program_convertt::convert( - const goto_programt &goto_program, - xmlt &xml) -{ - std::stringstream tmp; - // std::cout << "TNO: " << goto_program.target_numbers.size() << '\n'; - - for(const auto &inst : goto_program.instructions) - { - xmlt &ins=xml.new_element("instruction"); - if(!inst.location.is_nil()) - { - irepconverter.reference_convert( - inst.location, ins.new_element("location")); - } - - if(!inst.labels.empty()) - { - xmlt &lbl=ins.new_element("labels"); - for(goto_programt::instructiont::labelst::const_iterator - l_it=inst.labels.begin(); - l_it!=inst.labels.end(); - l_it++) - { - lbl.new_element("label").set_attribute("name", id2string(*l_it)); - } - } - - - if(inst.target_number!=0) - { - // std::cout << "Targetlabel found!\n"; - tmp.str(""); - tmp << inst.target_number; - ins.set_attribute("targetlabel", tmp.str()); - } - - switch(inst.type) - { - case GOTO: - { - ins.name="goto"; - if(!inst.guard.is_true()) - { - xmlt &g=ins.new_element("guard"); - irepconverter.reference_convert(inst.guard, g); - } - xmlt &tgt=ins.new_element("targets"); - for(goto_programt::instructiont::targetst::const_iterator - gt_it=inst.targets.begin(); - gt_it!=inst.targets.end(); - gt_it++) - { - tmp.str(""); - tmp << (*gt_it)->target_number; - tgt.new_element("target").data=tmp.str(); - } - break; - } - - case ASSUME: - { - ins.name="assume"; - xmlt &g=ins.new_element("guard"); - irepconverter.reference_convert(inst.guard, g); - const irep_idt &comment=inst.location.get("comment"); - if(comment!="") - ins.new_element("comment").data=id2string(comment); - break; - } - - case ASSERT: - { - ins.name="assert"; - xmlt &g=ins.new_element("guard"); - irepconverter.reference_convert(inst.guard, g); - const irep_idt &comment=inst.location.get("comment"); - if(comment!="") - ins.new_element("comment").data=id2string(comment); - break; - } - - case SKIP: - ins.name="skip"; - break; - - case END_FUNCTION: - ins.name="end_function"; - break; - - case LOCATION: - ins.name="location"; - break; - - case DEAD: - ins.name="dead"; - break; - - case ATOMIC_BEGIN: - ins.name="atomic_begin"; - break; - - case ATOMIC_END: - ins.name="atomic_end"; - break; - - case RETURN: - { - ins.name="return"; - xmlt &c=ins.new_element("code"); - irepconverter.reference_convert(inst.code, c); - break; - } - - case OTHER: - { - ins.name="instruction"; - xmlt &c=ins.new_element("code"); - irepconverter.reference_convert(inst.code, c); - break; - } - - case ASSIGN: - { - ins.name="assign"; - xmlt &c=ins.new_element("code"); - irepconverter.reference_convert(inst.code, c); - break; - } - - case FUNCTION_CALL: - { - ins.name="functioncall"; - xmlt &c=ins.new_element("code"); - irepconverter.reference_convert(inst.code, c); - break; - } - - case START_THREAD: - { - ins.name="thread_start"; - xmlt &tgt=ins.new_element("targets"); - if(inst.targets.size()==1) - { - tmp.str(""); - tmp << inst.targets.front()->target_number; - tgt.new_element("target").data=tmp.str(); - } - break; - } - - case END_THREAD: - ins.name="thread_end"; - break; - - default: - ins.name="unknown"; - break; - } - - if(inst.function!="") - { - xmlt &fnc=ins.new_element("function"); - fnc.data=id2string(inst.function); - } - } -} - -/// constructs the goto program according to the xml structure and the namespace -/// into the given goto program object. -/// \par parameters: an xml structure and a goto program to fill -/// \return none -void xml_goto_program_convertt::convert( - const xmlt &xml, - goto_programt &goto_program) -{ - goto_program.clear(); - goto_programt::instructionst &instructions=goto_program.instructions; - - for(const auto &element : xml.elements) - { - goto_programt::targett inst=goto_program.add_instruction(); - inst->targets.clear(); - - if(element.name=="goto") - { - inst->type=GOTO; - } - else if(element.name=="assume") - { - inst->type=ASSUME; - } - else if(element.name=="assert") - { - inst->type=ASSERT; - } - else if(element.name=="skip") - { - inst->type=SKIP; - } - else if(element.name=="end_function") - { - inst->type=END_FUNCTION; - } - else if(element.name=="location") - { - inst->type=LOCATION; - } - else if(element.name=="dead") - { - inst->type=DEAD; - } - else if(element.name=="atomic_begin") - { - inst->type=ATOMIC_BEGIN; - } - else if(element.name=="atomic_end") - { - inst->type=ATOMIC_END; - } - else if(element.name=="return") - { - inst->make_return(); - } - else if(element.name=="instruction") // OTHER - { - inst->make_other(); - } - else if(element.name=="assign") // OTHER - { - inst->make_other(); - inst->type=ASSIGN; - } - else if(element.name=="functioncall") // OTHER - { - inst->make_other(); - inst->type=FUNCTION_CALL; - } - else if(element.name=="thread_start") - { - inst->type=START_THREAD; - } - else if(element.name=="thread_end") - { - inst->type=END_THREAD; - } - else - { - std::cout << "Unknown instruction type encountered (" - << element.name << ")\n"; - return; - } - - xmlt::elementst::const_iterator eit=element.elements.begin(); - for(const auto &sub : element.elements) - { - if(sub.name=="location") - { - irepconverter.convert(*eit, inst->location); - irepconverter.resolve_references(inst->location); - } - else if(sub.name=="variables") - { - } - else if(sub.name=="labels") - { - xmlt::elementst::const_iterator lit=sub.elements.begin(); - for(; lit != sub.elements.end(); lit++) - { - if(lit->name=="label") - { - std::string ls=lit->get_attribute("name"); - inst->labels.push_back(ls); - } - else - { - std::cout << "Unknown node in labels section.\n"; - return; - } - } - } - else if(sub.name=="guard") - { - inst->guard.remove("value"); - irepconverter.convert(*eit, inst->guard); - irepconverter.resolve_references(inst->guard); - } - else if(sub.name=="code") - { - irepconverter.convert(*eit, inst->code); - irepconverter.resolve_references(inst->code); - } - else if(sub.name=="targets") - { - // Don't do anything here, we'll need a second run for that - } - else if(sub.name=="comment") - { - inst->location.set("comment", sub.data); - } - else if(sub.name=="function") - { - inst->function=sub.data; - } - } - } - - // assign line numbers - goto_program.compute_location_numbers(); - - // second run, for targets - goto_programt::targett ins_it=instructions.begin(); - for(const auto &element : xml.elements) - { - if(ins_it==instructions.end()) - break; - - for(const auto &sub : element.elements) - { - if(sub.name=="targets") - { - for(const auto &t : sub.elements) - { - if(t.name=="target") - { - goto_programt::targett tins = - find_instruction(xml, instructions, t.data); - if(tins!=instructions.end()) - { - // Here we insert the iterators that somehow seem - // to be strange afterwards (see line 87) - ins_it->targets.push_back(tins); - } - else - { - std::cout << "Warning: instruction not found when " - "resolving target links.\n"; - } - } - else - { - std::cout << "Unknown node in targets section.\n"; - return; - } - } - } - } - ins_it++; - } - - // resolve links - goto_program.update(); - - // std::cout << "TNI: " << goto_program.target_numbers.size() << '\n'; -} - -/// finds the index of the instruction labelled with the given target label in -/// the given xml-program -/// \par parameters: a target label string, the instructions list and an xml -/// program -/// \return iterator to the found instruction or .end() -goto_programt::targett xml_goto_program_convertt::find_instruction( - const xmlt &xml, - goto_programt::instructionst &instructions, - const std::string &label) -{ - goto_programt::targett ins_it=instructions.begin(); - for(const auto &element : xml.elements) - { - if(ins_it==instructions.end()) - break; - - if(label==element.get_attribute("targetlabel")) - return ins_it; - ins_it++; - } - return instructions.end(); -} diff --git a/src/goto-cc/xml_binaries/xml_goto_program_hashing.h b/src/goto-cc/xml_binaries/xml_goto_program_hashing.h deleted file mode 100644 index 63622775799..00000000000 --- a/src/goto-cc/xml_binaries/xml_goto_program_hashing.h +++ /dev/null @@ -1,43 +0,0 @@ -/*******************************************************************\ - -Module: Convert goto programs into xml structures and back (with - irep hashing) - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// Convert goto programs into xml structures and back (with irep hashing) - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_HASHING_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_HASHING_H - -#include -#include - -#include "xml_irep_hashing.h" - -class xml_goto_program_convertt -{ -private: - xml_irep_convertt irepconverter; - -public: - explicit xml_goto_program_convertt(xml_irep_convertt::ireps_containert &ic): - irepconverter(ic) - { - } - - void convert(const goto_programt&, xmlt&); - void convert(const xmlt&, goto_programt&); - - goto_programt::targett find_instruction( - const xmlt &, - goto_programt::instructionst &, - const std::string &); -}; - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_GOTO_PROGRAM_HASHING_H diff --git a/src/goto-cc/xml_binaries/xml_irep_hashing.cpp b/src/goto-cc/xml_binaries/xml_irep_hashing.cpp deleted file mode 100644 index 312a076befe..00000000000 --- a/src/goto-cc/xml_binaries/xml_irep_hashing.cpp +++ /dev/null @@ -1,294 +0,0 @@ -/*******************************************************************\ - -Module: XML-irep conversions with hashing - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// XML-irep conversions with hashing - -#include "xml_irep_hashing.h" - -#include -#include - -#include "string_hash.h" - -void xml_irep_convertt::convert( - const irept &irep, - xmlt &xml) -{ - if(irep.id()!="nil") - xml.new_element("id").data=irep.id_string(); - - forall_irep(it, irep.get_sub()) - { - xmlt &x_sub=xml.new_element("s"); - reference_convert(*it, x_sub); - } - - forall_named_irep(it, irep.get_named_sub()) - { - xmlt &x_nsub=xml.new_element("ns"); - x_nsub.set_attribute("n", name2string(it->first)); - reference_convert(it->second, x_nsub); - } - - forall_named_irep(it, irep.get_comments()) - { - xmlt &x_com=xml.new_element("c"); - x_com.set_attribute("n", name2string(it->first)); - reference_convert(it->second, x_com); - } -} - -void xml_irep_convertt::convert( - const xmlt &xml, - irept &irep) -{ - irep.id("nil"); - xmlt::elementst::const_iterator it=xml.elements.begin(); - for(; it != xml.elements.end(); it++) - { - if(it->name=="R") - { - irep.id("__REFERENCE__"); - irep.set("REF", it->data); - } - else if(it->name=="id") - { - irep.id(it->data); - } - else if(it->name=="ns") - { - irept r; - convert(*it, r); - std::string named_name=it->get_attribute("n"); - irep.move_to_named_sub(named_name, r); - } - else if(it->name=="s") - { - irept r; - convert(*it, r); - irep.move_to_sub(r); - } - else if(it->name=="c") - { - irept r; - convert(*it, r); - std::string named_name=it->get_attribute("n"); - irep.move_to_named_sub(named_name, r); - } - else - { - // Should not happen - std::cout << "Unknown sub found (" << it->name << "); malformed xml?\n"; - } - } -} - -void xml_irep_convertt::reference_convert( - const irept &irep, - xmlt &xml) -{ - xmlt &ir=xml.new_element("R"); - - ireps_containert::content_containert::const_iterator fi= - find_irep_by_content(irep); - if(fi==ireps_container.content_container.end()) - { - unsigned id=ireps_container.id_replace_map[add_with_childs(irep)]; - ir.data=long_to_string(id); - } - else - { - ir.data= - long_to_string(ireps_container.id_replace_map[fi->second]); - } -} - -unsigned long xml_irep_convertt::add_with_childs(const irept &iwi) -{ - unsigned long id=insert((unsigned long)&iwi, iwi); - if(id!=(unsigned long)&iwi) - return id; - - forall_irep(it, iwi.get_sub()) - { - ireps_containert::content_containert::const_iterator fi= - find_irep_by_content(*it); - if(fi==ireps_container.content_container.end()) - { - add_with_childs(*it); - } - } - forall_named_irep(it, iwi.get_named_sub()) - { - ireps_containert::content_containert::const_iterator fi= - find_irep_by_content(it->second); - if(fi==ireps_container.content_container.end()) - { - add_with_childs(it->second); - } - } - forall_named_irep(it, iwi.get_comments()) - { - ireps_containert::content_containert::const_iterator fi= - find_irep_by_content(it->second); - if(fi==ireps_container.content_container.end()) - { - add_with_childs(it->second); - } - } - return id; -} - -/// resolves references to ireps from an irep after reading an irep hash map -/// into memory. -/// \return none -void xml_irep_convertt::resolve_references(const irept &cur) -{ - if(cur.id() == "__REFERENCE__") - { - unsigned long id=string_to_long(cur.get_string("REF")); - ireps_containert::id_containert::const_iterator itr=find_irep_by_id(id); - if(itr==ireps_container.id_container.end()) - { - std::cout << "Warning: can't resolve irep reference (sub " - << cur.get("REF") << ")\n"; - } - else - { - irept &curX=const_cast(cur); - curX=itr->second; - } - } - - forall_irep(iti, cur.get_sub()) - resolve_references(*iti); - - forall_named_irep(iti, cur.get_named_sub()) - resolve_references(iti->second); - - forall_named_irep(iti, cur.get_comments()) - resolve_references(iti->second); -} - -/// converts the hash value to a readable string -/// \par parameters: an irep pointer -/// \return a new string -std::string xml_irep_convertt::long_to_string(const unsigned long l) -{ - std::stringstream s; - s << std::hex << l; - return s.str(); -} - -/// converts the string to an unsigned long that used to give a pointer to an -/// irep in an old compilation -/// \par parameters: a string -/// \return an unsigned long -unsigned long xml_irep_convertt::string_to_long(const std::string &s) -{ - std::stringstream ss(s); - unsigned long res=0; - ss >> std::hex >> res; - return res; -} - -/// finds an irep in the ireps hash set by its id -/// \par parameters: an id -/// \return an iterator into the ireps hash set -xml_irep_convertt::ireps_containert::id_containert::const_iterator - xml_irep_convertt::find_irep_by_id(const unsigned int id) -{ - return ireps_container.id_container.find(id); -} - -/// finds an irep in the ireps hash set by checking contents -/// \par parameters: an irep -/// \return an iterator into the ireps hash set -xml_irep_convertt::ireps_containert::content_containert::const_iterator - xml_irep_convertt::find_irep_by_content(const irept &irep) -{ - return ireps_container.content_container.find(irep); -} - -/// inserts an irep into the hashtable -/// \par parameters: an unsigned long and an irep -/// \return true on success, false otherwise -unsigned long xml_irep_convertt::insert( - unsigned long id, - const irept &i) -{ - ireps_containert::content_containert::const_iterator sit; - sit=find_irep_by_content(i); - if(sit==ireps_container.content_container.end()) - { - ireps_container.content_container.insert( - std::pair(i, id)); - - if(ireps_container.id_container.insert( - std::pair(id, i)).second) - { - ireps_container.id_replace_map[id] = - ireps_container.id_container.size(); - } - - return id; - } - else - { - return sit->second; - } -} - -/// inserts an irep into the hashtable -/// \par parameters: a string and an irep -/// \return true on success, false otherwise -unsigned long xml_irep_convertt::insert( - const std::string &id, - const irept &i) -{ - return insert(string_to_long(id), i); -} - -/// converts the current hash map of ireps into the given xml structure -/// \par parameters: an xml node -/// \return nothing -void xml_irep_convertt::convert_map(xmlt &xml) -{ - ireps_containert::id_containert::iterator hit= - ireps_container.id_container.begin(); - for(; hit!=ireps_container.id_container.end(); hit++) - { - xmlt &xmlhe=xml.new_element("irep"); - xmlhe.set_attribute( - "id", - long_to_string(ireps_container.id_replace_map[hit->first])); - convert(hit->second, xmlhe); - } -} - -/// converts the current hash map of ireps into xml nodes and outputs them to -/// the stream -/// \par parameters: an output stream -/// \return nothing -void xml_irep_convertt::output_map(std::ostream &out, unsigned indent) -{ - ireps_containert::id_containert::iterator hit= - ireps_container.id_container.begin(); - for(; hit!=ireps_container.id_container.end(); hit++) - { - xmlt xmlhe("irep"); - xmlhe.set_attribute( - "id", - long_to_string(ireps_container.id_replace_map[hit->first])); - convert(hit->second, xmlhe); - xmlhe.output(out, indent); - } -} diff --git a/src/goto-cc/xml_binaries/xml_irep_hashing.h b/src/goto-cc/xml_binaries/xml_irep_hashing.h deleted file mode 100644 index 2391580a61b..00000000000 --- a/src/goto-cc/xml_binaries/xml_irep_hashing.h +++ /dev/null @@ -1,116 +0,0 @@ -/*******************************************************************\ - -Module: XML-irep conversions with hashing - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// XML-irep conversions with hashing - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_IREP_HASHING_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_IREP_HASHING_H - -#include -#include - -class xml_irep_convertt -{ -private: - // NOLINTNEXTLINE(readability/identifiers) - struct ul_hash - { - unsigned short operator()(const unsigned long l) const - { - return (l &0xFFFF); - } - }; - - // NOLINTNEXTLINE(readability/identifiers) - struct ul_eq - { - bool operator()(const unsigned long l, const unsigned long r) const - { - return (l==r); - } - }; - - // NOLINTNEXTLINE(readability/identifiers) - struct irep_full_hash - { - size_t operator()(const irept &i) const - { - return i.full_hash(); - } - }; - - // NOLINTNEXTLINE(readability/identifiers) - struct irep_content_eq - { - bool operator()(const irept &l, const irept &r) const - { - return l.full_eq(l, r); - } - }; - -public: - struct ireps_containert - { - typedef std::unordered_map - id_containert; - id_containert id_container; - - typedef std::unordered_map - content_containert; - content_containert content_container; - - typedef std::map id_replace_mapt; - id_replace_mapt id_replace_map; - - void clear() - { - id_container.clear(); - content_container.clear(); - id_replace_map.clear(); - } - }; - - explicit xml_irep_convertt(ireps_containert &ic):ireps_container(ic) - { - }; - - unsigned long insert(unsigned long, const irept&); - unsigned long insert(const std::string&, const irept&); - - void convert(const irept &irep, xmlt &xml); - void convert(const xmlt &xml, irept &irep); - void reference_convert(const irept &irep, xmlt &xml); - void resolve_references(const irept &cur); - - void convert_map(xmlt &xml); - void output_map(std::ostream &out, unsigned indent); - - void clear() - { - ireps_container.clear(); - } - -private: - ireps_containert &ireps_container; - - ireps_containert::id_containert::const_iterator - find_irep_by_id(const unsigned int); - ireps_containert::content_containert::const_iterator - find_irep_by_content(const irept &irep); - - std::string long_to_string(const unsigned long); - unsigned long string_to_long(const std::string &); - - unsigned long add_with_childs(const irept&); -}; - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_IREP_HASHING_H diff --git a/src/goto-cc/xml_binaries/xml_symbol.cpp b/src/goto-cc/xml_binaries/xml_symbol.cpp deleted file mode 100644 index 0fa7acd8069..00000000000 --- a/src/goto-cc/xml_binaries/xml_symbol.cpp +++ /dev/null @@ -1,128 +0,0 @@ -/*******************************************************************\ - -Module: Compile and link source and object files. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Compile and link source and object files. - -#include "xml_symbol.h" - -#include "xml_irep.h" - -/// converts a symbol to an xml symbol node -/// \par parameters: a symbol and an xml node -/// \return none -void convert(const symbolt &sym, xmlt &root) -{ - xmlt &xmlsym = root.new_element("symbol"); - xmlsym.set_attribute("name", id2string(sym.name)); - - xmlt &xmltype = xmlsym.new_element("type"); - convert(sym.type, xmltype); - - xmlt &xmlval = xmlsym.new_element("value"); - if(!sym.is_type && sym.type.id() == "code" && !sym.value.is_nil()) - xmlval.data = "compiled"; // only for implemented functions - else - convert(sym.value, xmlval); - - xmlt &flags = xmlsym.new_element("flags"); - - flags.set_attribute_bool("lvalue", sym.is_lvalue); - flags.set_attribute_bool("static_lifetime", sym.is_static_lifetime); - flags.set_attribute_bool("file_local", sym.is_file_local); - flags.set_attribute_bool("theorem", sym.is_property); - flags.set_attribute_bool("thread_local", sym.is_thread_local); - flags.set_attribute_bool("type", sym.is_type); - flags.set_attribute_bool("extern", sym.is_extern); - flags.set_attribute_bool("input", sym.is_input); - flags.set_attribute_bool("output", sym.is_output); - flags.set_attribute_bool("macro", sym.is_macro); - // flags.set_attribute_bool("actual", sym.is_actual); - // flags.set_attribute_bool("binding", sym.binding); - // flags.set_attribute_bool("free_var", sym.free_var); - flags.set_attribute_bool("statevar", sym.is_state_var); - - xmlt &mode = flags.new_element("mode"); - mode.data = id2string(sym.mode); - - flags.new_element("base_name").data=id2string(sym.base_name); - flags.new_element("module").data=id2string(sym.module); - - if(!sym.pretty_name.empty()) - flags.new_element("pretty_name").data=id2string(sym.pretty_name); - - xmlt &xmlloc = xmlsym.new_element("location"); - convert(sym.location, xmlloc); - xmlloc.name = "location"; // convert overwrote this -} - -/// converts an xml symbol node to a symbol -/// \par parameters: an xml node and a symbol -/// \return none -void convert(const xmlt &xmlsym, symbolt &symbol) -{ - symbol.name=xmlsym.get_attribute("name"); - - for(xmlt::elementst::const_iterator - it=xmlsym.elements.begin(); - it!=xmlsym.elements.end(); - it++) - { - if(it->name=="type") - { - convert(*it, symbol.type); - } - else if(it->name=="value") - { - if(it->data=="compiled") - { - symbol.value.id("code"); - } - else - { - convert(*it, symbol.value); - } - } - else if(it->name=="flags") - { - symbol.is_lvalue = it->get_attribute_bool("lvalue"); - symbol.is_static_lifetime = it->get_attribute_bool("static_lifetime"); - symbol.is_file_local = it->get_attribute_bool("file_local"); - symbol.is_property = it->get_attribute_bool("theorem"); - symbol.is_thread_local = it->get_attribute_bool("thread_local"); - symbol.is_type = it->get_attribute_bool("type"); - symbol.is_extern = it->get_attribute_bool("extern"); - symbol.is_input = it->get_attribute_bool("input"); - symbol.is_output = it->get_attribute_bool("output"); - symbol.is_macro = it->get_attribute_bool("macro"); - // symbol.is_actual = it->get_attribute_bool("actual"); - // symbol.binding = it->get_attribute_bool("binding"); - // symbol.free_var = it->get_attribute_bool("free_var"); - symbol.is_state_var = it->get_attribute_bool("statevar"); - - for(xmlt::elementst::const_iterator - fit=it->elements.begin(); - fit!=it->elements.end(); - fit++) - { - if(fit->name=="mode") - symbol.mode=fit->data; - else if(fit->name=="base_name") - symbol.base_name=fit->data; - else if(fit->name=="module") - symbol.module=fit->data; - } - } - else if(it->name=="location") - { - convert(*it, symbol.location); - } - } -} diff --git a/src/goto-cc/xml_binaries/xml_symbol.h b/src/goto-cc/xml_binaries/xml_symbol.h deleted file mode 100644 index 0044cf98000..00000000000 --- a/src/goto-cc/xml_binaries/xml_symbol.h +++ /dev/null @@ -1,23 +0,0 @@ -/*******************************************************************\ - -Module: Converts symbols to xml structures and back. - -Author: CM Wintersteiger - -Date: June 2006 - -\*******************************************************************/ - -/// \file -/// Converts symbols to xml structures and back. - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_H - -#include -#include - -void convert(const symbolt &, xmlt &); -void convert(const xmlt &, symbolt &); - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_H diff --git a/src/goto-cc/xml_binaries/xml_symbol_hashing.cpp b/src/goto-cc/xml_binaries/xml_symbol_hashing.cpp deleted file mode 100644 index e666487df76..00000000000 --- a/src/goto-cc/xml_binaries/xml_symbol_hashing.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/*******************************************************************\ - -Module: XML-symbol conversions with irep hashing - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// XML-symbol conversions with irep hashing - -#include "xml_irep_hashing.h" - -#include "xml_symbol_hashing.h" - -/// converts a symbol to an xml symbol node -/// \par parameters: a symbol and an xml node -/// \return none -void xml_symbol_convertt::convert(const symbolt &sym, xmlt &root) -{ - xmlt &xmlsym = root.new_element("symbol"); - irepcache.push_back(irept()); - sym.to_irep(irepcache.back()); - irepconverter.reference_convert(irepcache.back(), xmlsym); -} - -/// converts an xml symbol node to a symbol -/// \par parameters: an xml node and a symbol -/// \return none -void xml_symbol_convertt::convert(const xmlt &xmlsym, symbolt &symbol) -{ - irept t; - - irepconverter.convert(xmlsym, t); - irepconverter.resolve_references(t); - symbol.from_irep(t); -} diff --git a/src/goto-cc/xml_binaries/xml_symbol_hashing.h b/src/goto-cc/xml_binaries/xml_symbol_hashing.h deleted file mode 100644 index bb5f3e9a060..00000000000 --- a/src/goto-cc/xml_binaries/xml_symbol_hashing.h +++ /dev/null @@ -1,38 +0,0 @@ -/*******************************************************************\ - -Module: XML-symbol conversions with irep hashing - -Author: CM Wintersteiger - -Date: July 2006 - -\*******************************************************************/ - -/// \file -/// XML-symbol conversions with irep hashing - -#ifndef CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_HASHING_H -#define CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_HASHING_H - -#include -#include - -#include "xml_irep_hashing.h" - -class xml_symbol_convertt -{ -private: - xml_irep_convertt irepconverter; - std::list irepcache; - -public: - explicit xml_symbol_convertt(xml_irep_convertt::ireps_containert &ic): - irepconverter(ic) - { - } - - void convert(const symbolt &, xmlt &); - void convert(const xmlt &, symbolt &); -}; - -#endif // CPROVER_GOTO_CC_XML_BINARIES_XML_SYMBOL_HASHING_H diff --git a/src/goto-instrument/accelerate/linearize.cpp b/src/goto-instrument/accelerate/linearize.cpp deleted file mode 100644 index 87c4db589cb..00000000000 --- a/src/goto-instrument/accelerate/linearize.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/*******************************************************************\ - -Module: Loop Acceleration - -Author: Matt Lewis - -\*******************************************************************/ - -/// \file -/// Loop Acceleration - -#include "linearize.h" - -#include - -bool linearize(symex_target_equationt &equation, linear_recurrencet &recurrence) -{ -} diff --git a/src/goto-instrument/accelerate/linearize.h b/src/goto-instrument/accelerate/linearize.h deleted file mode 100644 index 90192ce1dfe..00000000000 --- a/src/goto-instrument/accelerate/linearize.h +++ /dev/null @@ -1,41 +0,0 @@ -/*******************************************************************\ - -Module: Loop Acceleration - -Author: Matt Lewis - -\*******************************************************************/ - -/// \file -/// Loop Acceleration - -#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H -#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H - -#include - -#include -#include - -#include "Eigen/Eigen" - -/* - * The idea here is that a linear_recurrencet describes a linear recurrence in - * the following way: - * - * vars' = matrix * vars; - * - * i.e. the next value of the vars vector is calculated by applying the matrix - * to the current vars vector. - */ -struct linear_recurrencet -{ - Eigen::MatrixXd matrix; - std::vector vars; -}; - -bool linearize( - symex_target_equationt &equation, - linear_recurrencet &recurrence); - -#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H diff --git a/src/java_bytecode/java_bytecode_vtable.cpp b/src/java_bytecode/java_bytecode_vtable.cpp deleted file mode 100644 index 68da4c6b494..00000000000 --- a/src/java_bytecode/java_bytecode_vtable.cpp +++ /dev/null @@ -1,449 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "java_bytecode_vtable.h" - -#include -#include - -#include -#include -#include -#include -#include -#include - -const char ID_virtual_name[]="virtual_name"; - -class is_virtual_name_equalt -{ - const irep_idt &virtual_name; -public: - explicit is_virtual_name_equalt(const class_typet::methodt &method): - virtual_name(method.get(ID_virtual_name)) - { - } - - bool operator()(const class_typet::methodt &method) const - { - return virtual_name==method.get(ID_virtual_name); - } -}; - -class is_name_equalt -{ - const irep_idt &name; - -public: - explicit is_name_equalt(const irep_idt &name): - name(name) - { - } - - bool operator()(const class_typet::componentt &component) const - { - return name==component.get_name(); - } -}; - -class java_bytecode_vtable_factoryt -{ - symbol_tablet &symbol_table; - const std::string &module; - const namespacet ns; - -public: - bool has_error; - - java_bytecode_vtable_factoryt( - symbol_tablet &symbol_table, - const std::string &module): - symbol_table(symbol_table), - module(module), - ns(symbol_table), - has_error(false) - { - } - - symbolt &get_vt_type_symbol(const class_typet &class_type) - { - const std::string &class_name(id2string(class_type.get(ID_name))); - return symbol_table.lookup(vtnamest::get_type(class_name)); - } - - void create_vtable_symbol(symbolt &result, const class_typet &class_type) - { - const std::string &class_name=id2string(class_type.get(ID_name)); - const std::string &base_class_name=id2string(class_type.get(ID_base_name)); - const symbolt &type_symbol(get_vt_type_symbol(class_type)); - result.name=vtnamest::get_table(class_name); - result.base_name=vtnamest::get_table_base(base_class_name); - result.pretty_name=result.base_name; - result.mode=type_symbol.mode; - result.module=module; - result.location=type_symbol.location; - result.type=symbol_typet(type_symbol.name); - result.is_lvalue=true; - result.is_state_var=true; - result.is_static_lifetime=true; - } - - bool has_component(const class_typet &vtable_type, const irep_idt &ifc_name) - { - const class_typet::componentst &comps(vtable_type.components()); - const is_name_equalt pred(ifc_name); - return std::find_if(comps.begin(), comps.end(), pred)!=comps.end(); - } - - void add_vtable_entry(struct_exprt &vtable_value, - const class_typet &interface, const class_typet &implementor, - const class_typet::methodt &implementation) - { - const class_typet::methodst &methods(interface.methods()); - const is_virtual_name_equalt pred(implementation); - const class_typet::methodst::const_iterator ifc_method( - std::find_if(methods.begin(), methods.end(), pred)); - assert(methods.end()!=ifc_method); - symbolt &vtable_type_symbol(get_vt_type_symbol(implementor)); - class_typet &vtable_type(to_class_type(vtable_type_symbol.type)); - const irep_idt &ifc_name(ifc_method->get_name()); - if(has_component(vtable_type, ifc_name)) - return; - - struct_typet::componentt entry_component; - entry_component.set_name(ifc_name); - entry_component.set_base_name(ifc_method->get_base_name()); - entry_component.type()=pointer_type(implementation.type()); - vtable_type.components().push_back(entry_component); - - const irep_idt &impl_name(implementation.get_name()); - const symbol_exprt impl_symbol(impl_name, implementation.type()); - const address_of_exprt impl_ref(impl_symbol); - vtable_value.copy_to_operands(impl_ref); - } - - const class_typet &get_class_type(const irept &base) - { - const typet &type(static_cast(base.find(ID_type))); - const symbol_typet &symbol_type(to_symbol_type(type)); - const irep_idt &base_class_name(symbol_type.get_identifier()); - assert(symbol_table.has_symbol(base_class_name)); - const symbolt &base_class_symbol(ns.lookup(base_class_name)); - return to_class_type(base_class_symbol.type); - } - - bool has_method(const irept &base, const class_typet::methodt &method) - { - const typet &type(static_cast(base.find(ID_type))); - const symbol_typet &symbol_type(to_symbol_type(type)); - const irep_idt &base_class_name(symbol_type.get_identifier()); - if(!symbol_table.has_symbol(base_class_name)) - return false; - const symbolt &base_class_symbol(ns.lookup(base_class_name)); - const class_typet &base_class_type(to_class_type(base_class_symbol.type)); - const class_typet::methodst &methods(base_class_type.methods()); - const is_virtual_name_equalt pred(method); - return std::find_if(methods.begin(), methods.end(), pred)!=methods.end(); - } - - void extract_types( - std::vector &result, - const irept::subt &types, - const class_typet::methodt &method) - { - for(irept::subt::const_iterator it=types.begin(); - it!=types.end(); ++it) - { - if(!has_method(*it, method)) - continue; - result.push_back(get_class_type(*it)); - } - } - - bool is_virtual(const class_typet::methodt &method) - { - return method.get_bool(ID_is_virtual) - && !method.get_bool(ID_constructor); - } - - void create_base_vtable_entries( - struct_exprt &vtable_value, - const class_typet &class_type, - const class_typet::methodt &method) - { - if(!is_virtual(method)) - return; - std::vector bases; - extract_types(bases, class_type.bases(), method); - // extract_types(bases, class_type.find(ID_interfaces).get_sub(), method); - for(const std::vector::value_type &b : bases) - add_vtable_entry(vtable_value, b, class_type, method); - } - - void create_vtable_entry(struct_exprt &vtable_value, - const class_typet &class_type, const class_typet::methodt &method) - { - if(!is_virtual(method)) - return; - add_vtable_entry(vtable_value, class_type, class_type, method); - } - - void set_vtable_value(symbolt &vtable_symbol, const class_typet &class_type, - struct_exprt &vtable_value) - { - const std::string &class_name(id2string(class_type.get(ID_name))); - const irep_idt vttype(vtnamest::get_type(class_name)); - vtable_value.type()=symbol_typet(vttype); - vtable_symbol.value=vtable_value; - } - - bool is_class_with_vt(const symbolt &symbol) - { - if(!symbol.is_type || ID_struct!=symbol.type.id()) - return false; - const class_typet &class_type(to_class_type(symbol.type)); - const std::string &class_name(id2string(class_type.get(ID_name))); - return symbol_table.has_symbol(vtnamest::get_type(class_name)); - } - - void operator()(const irep_idt &symbol_name) - { - const symbolt &symbol=symbol_table.lookup(symbol_name); - if(!is_class_with_vt(symbol)) - return; - const class_typet &class_type(to_class_type(symbol.type)); - const std::string &class_name(id2string(symbol_name)); - if(symbol_table.has_symbol(vtnamest::get_table(class_name))) - return; - symbolt vtable_symbol; - create_vtable_symbol(vtable_symbol, class_type); - const class_typet::methodst &methods(class_type.methods()); - struct_exprt vtable_value; - for(const class_typet::methodst::value_type &m : methods) - create_base_vtable_entries(vtable_value, class_type, m); - for(const class_typet::methodst::value_type &m : methods) - create_vtable_entry(vtable_value, class_type, m); - set_vtable_value(vtable_symbol, class_type, vtable_value); - assert(!symbol_table.add(vtable_symbol)); - } -}; - - -/******************************************************************* - - Function: java_bytecode_vtable - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool java_bytecode_vtable( - symbol_tablet &symbol_table, - const std::string &module) -{ - const symbol_tablet::symbolst &symbols(symbol_table.symbols); - std::vector names; - names.reserve(symbols.size()); - std::transform(symbols.begin(), symbols.end(), std::back_inserter(names), - [](const std::pair &entry) - { return entry.first;}); - java_bytecode_vtable_factoryt factory(symbol_table, module); - std::for_each(names.begin(), names.end(), factory); - return factory.has_error; -} - -static void create_vtable_type( - const irep_idt &vt_name, - symbol_tablet &symbol_table, - const symbolt &class_symbol) -{ - symbolt vt_symb_type; - vt_symb_type.name=vt_name; - vt_symb_type.base_name=vtnamest::get_type_base( - id2string(class_symbol.base_name)); - vt_symb_type.pretty_name=vt_symb_type.base_name; - vt_symb_type.mode=class_symbol.mode; - vt_symb_type.module=class_symbol.module; - vt_symb_type.location=class_symbol.location; - vt_symb_type.type=struct_typet(); - vt_symb_type.type.set(ID_name, vt_symb_type.name); - vt_symb_type.is_type=true; - assert(!symbol_table.add(vt_symb_type)); -} - -#define ID_vtable_pointer "@vtable_pointer" - -static void add_vtable_pointer_member( - const irep_idt &vt_name, - symbolt &class_symbol) -{ - struct_typet::componentt comp; - - comp.type()=pointer_type(symbol_typet(vt_name)); - comp.set_name(ID_vtable_pointer); - comp.set_base_name(ID_vtable_pointer); - comp.set_pretty_name(ID_vtable_pointer); - comp.set("is_vtptr", true); - - struct_typet &class_type=to_struct_type(class_symbol.type); - class_type.components().push_back(comp); -} - -/******************************************************************* - - Function: create_vtable_symbol - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void create_vtable_symbol( - symbol_tablet &symbol_table, - const symbolt &class_symbol) -{ - const irep_idt vttype= - vtnamest::get_type(id2string(class_symbol.name)); - - if(!symbol_table.has_symbol(vttype)) - create_vtable_type(vttype, symbol_table, class_symbol); -} - -/******************************************************************* - - Function: has_vtable_info - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool has_vtable_info( - const symbol_tablet &symbol_table, - const symbolt &class_symbol) -{ - return - symbol_table.has_symbol(vtnamest::get_type(id2string(class_symbol.name))) && - to_struct_union_type(class_symbol.type).has_component(ID_vtable_pointer); -} - -/******************************************************************* - - Function: create_vtable_pointer - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void create_vtable_pointer(symbolt &class_symbol) -{ - const irep_idt vttype= - vtnamest::get_type(id2string(class_symbol.name)); - - add_vtable_pointer_member(vttype, class_symbol); -} - -/******************************************************************* - - Function: get_virtual_name - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void set_virtual_name(class_typet::methodt &method) -{ - const std::string &name(id2string(method.get(ID_name))); - const std::string::size_type vname_start(name.find_last_of('.') + 1); - std::string virtual_name(name.substr(vname_start)); - method.set(ID_virtual_name, virtual_name); -} - -static exprt get_ref( - const exprt &this_obj, - const symbol_typet &target_type) -{ - const typet &type(this_obj.type()); - const irep_idt &type_id(type.id()); - if(ID_symbol==type_id) - return get_ref(address_of_exprt(this_obj), target_type); - assert(ID_pointer==type_id); - const typecast_exprt cast(this_obj, pointer_type(target_type)); - return dereference_exprt(cast, target_type); -} - -static std::string get_full_class_name(const std::string &name) -{ - const bool has_prefix(name.find("java::")!=std::string::npos); - const std::string::size_type offset= - has_prefix ? std::string("java::").size() : 0; - const std::string::size_type end(name.find_first_of(':', offset)); - const std::string::size_type last_sep(name.rfind('.', end)); - return name.substr(0, last_sep); -} - -/******************************************************************* - - Function: make_vtable_function - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt make_vtable_function( - const exprt &func, - const exprt &this_obj) -{ - const irep_idt &func_name(func.get(ID_identifier)); - const std::string class_id(get_full_class_name(id2string(func_name))); - - // TODO: Handle unavailable models! - if(class_id.find("java.")!=std::string::npos) - { - // When translating a single java_bytecode_parse_treet, we don't know - // which classes will eventually be available yet. If we could provide - // access to the class loader here, we know which classes have been - // loaded successfully. For classes which have not been loaded, returning - // "func" is equivalent to an unimplemented function. - return func; - } - - const symbol_typet vtable_type(vtnamest::get_type(class_id)); - const pointer_typet vt_ptr_type=pointer_type(vtable_type); - const symbol_typet target_type(class_id); - const exprt this_ref(get_ref(this_obj, target_type)); - const typet ref_type(this_ref.type()); - const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type); - const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast? - const pointer_typet func_ptr_type=pointer_type(func.type()); - const member_exprt func_ptr(vtable, func_name, func_ptr_type); - const dereference_exprt virtual_func(func_ptr, func.type()); - return virtual_func; -} diff --git a/src/java_bytecode/java_bytecode_vtable.h b/src/java_bytecode/java_bytecode_vtable.h deleted file mode 100644 index 44a7f35bf1b..00000000000 --- a/src/java_bytecode/java_bytecode_vtable.h +++ /dev/null @@ -1,37 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H -#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H - -#include - -void create_vtable_pointer( - class symbolt &class_symbol); - -void create_vtable_symbol( - symbol_tablet &symbol_table, - const class symbolt &class_symbol); - -bool has_vtable_info( - const symbol_tablet &symbol_table, - const symbolt &class_symbol); - -exprt make_vtable_function( - const exprt &function, - const exprt &this_obj); - -void set_virtual_name( - class_typet::methodt &method); - -bool java_bytecode_vtable( - symbol_tablet &symbol_table, - const std::string &module); - -#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_VTABLE_H diff --git a/src/solvers/Makefile b/src/solvers/Makefile index b7b9c5b43d9..a3e7219db4d 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -69,6 +69,13 @@ ifneq ($(LINGELING),) CP_CXXFLAGS += -DHAVE_LINGELING endif +ifneq ($(LIMMAT),) + LIMMAT_SRC=sat/satcheck_limmat.cpp + LIMMAT_INCLUDE=-I $(LIMMAT) + LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT) + CP_CXXFLAGS += -DHAVE_LIMMAT +endif + SRC = $(BOOLEFORCE_SRC) \ $(CHAFF_SRC) \ $(CUDD_SRC) \ @@ -80,6 +87,7 @@ SRC = $(BOOLEFORCE_SRC) \ $(PRECOSAT_SRC) \ $(SMVSAT_SRC) \ $(SQUOLEM2_SRC) \ + $(LIMMAT_SRC) \ cvc/cvc_conv.cpp \ cvc/cvc_dec.cpp \ flattening/arrays.cpp \ @@ -138,6 +146,7 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/pointer_logic.cpp \ floatbv/float_bv.cpp \ floatbv/float_utils.cpp \ + floatbv/float_approximation.cpp \ miniBDD/miniBDD.cpp \ prop/aig.cpp \ prop/aig_prop.cpp \ diff --git a/src/solvers/cvc/cvc_prop.cpp b/src/solvers/cvc/cvc_prop.cpp deleted file mode 100644 index 7a02bd65335..00000000000 --- a/src/solvers/cvc/cvc_prop.cpp +++ /dev/null @@ -1,307 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "cvc_prop.h" - -#include -#include - -explicit cvc_propt::cvc_propt(std::ostream &_out):out(_out) -{ - _no_variables=0; -} - -cvc_propt::~cvc_propt() -{ -} - -void cvc_propt::land(literalt a, literalt b, literalt o) -{ - out << "%% land\n"; - out << "ASSERT (" << cvc_literal(a) << " AND " - << cvc_literal(b) << ") <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::lor(literalt a, literalt b, literalt o) -{ - out << "%% lor\n"; - out << "ASSERT (" << cvc_literal(a) << " OR " - << cvc_literal(b) << ") <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::lxor(literalt a, literalt b, literalt o) -{ - out << "%% lxor\n"; - out << "ASSERT (" << cvc_literal(a) << " XOR " - << cvc_literal(b) << ") <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::lnand(literalt a, literalt b, literalt o) -{ - out << "%% lnand\n"; - out << "ASSERT (NOT (" << cvc_literal(a) << " AND " - << cvc_literal(b) << ")) <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::lnor(literalt a, literalt b, literalt o) -{ - out << "%% lnor\n"; - out << "ASSERT (NOT (" << cvc_literal(a) << " OR " - << cvc_literal(b) << ")) <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::lequal(literalt a, literalt b, literalt o) -{ - out << "%% lequal\n"; - out << "ASSERT (" << cvc_literal(a) << " <=> " - << cvc_literal(b) << ") <=> " << cvc_literal(o) - << ";\n\n"; -} - -void cvc_propt::limplies(literalt a, literalt b, literalt o) -{ - out << "%% limplies\n"; - out << "ASSERT (" << cvc_literal(a) << " => " - << cvc_literal(b) << ") <=> " << cvc_literal(o) - << ";\n\n"; -} - -literalt cvc_propt::land(const bvt &bv) -{ - out << "%% land\n"; - - literalt literal=def_cvc_literal(); - - forall_literals(it, bv) - { - if(it!=bv.begin()) - out << " AND "; - out << cvc_literal(*it); - } - - out << ";\n\n"; - - return literal; -} - -literalt cvc_propt::lor(const bvt &bv) -{ - out << "%% lor\n"; - - literalt literal=def_cvc_literal(); - - forall_literals(it, bv) - { - if(it!=bv.begin()) - out << " OR "; - out << cvc_literal(*it); - } - - out << ";\n\n"; - - return literal; -} - -literalt cvc_propt::lxor(const bvt &bv) -{ - if(bv.empty()) - return const_literal(false); - if(bv.size()==1) - return bv[0]; - if(bv.size()==2) - return lxor(bv[0], bv[1]); - - literalt literal=const_literal(false); - - forall_literals(it, bv) - literal=lxor(*it, literal); - - return literal; -} - -literalt cvc_propt::land(literalt a, literalt b) -{ - if(a==const_literal(true)) - return b; - if(b==const_literal(true)) - return a; - if(a==const_literal(false)) - return const_literal(false); - if(b==const_literal(false)) - return const_literal(false); - if(a==b) - return a; - - out << "%% land\n"; - - literalt o=def_cvc_literal(); - - out << cvc_literal(a) << " AND " << cvc_literal(b) << ";\n\n"; - - return o; -} - -literalt cvc_propt::lor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return const_literal(true); - if(b==const_literal(true)) - return const_literal(true); - if(a==b) - return a; - - out << "%% lor\n"; - - literalt o=def_cvc_literal(); - - out << cvc_literal(a) << " OR " << cvc_literal(b) << ";\n\n"; - - return o; -} - -literalt cvc_propt::lxor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - out << "%% lxor\n"; - - literalt o=def_cvc_literal(); - - out << cvc_literal(a) << " XOR " << cvc_literal(b) << ";\n\n"; - - return o; -} - -literalt cvc_propt::lnand(literalt a, literalt b) -{ - return !land(a, b); -} - -literalt cvc_propt::lnor(literalt a, literalt b) -{ - return !lor(a, b); -} - -literalt cvc_propt::lequal(literalt a, literalt b) -{ - return !lxor(a, b); -} - -literalt cvc_propt::limplies(literalt a, literalt b) -{ - return lor(!a, b); -} - -literalt cvc_propt::lselect(literalt a, literalt b, literalt c) -{ - if(a==const_literal(true)) - return b; - if(a==const_literal(false)) - return c; - if(b==c) - return b; - - out << "%% lselect\n"; - - literalt o=def_cvc_literal(); - - out << "IF " << cvc_literal(a) << " THEN " - << cvc_literal(b) << " ELSE " - << cvc_literal(c) << " ENDIF;\n\n"; - - return o; -} - -literalt cvc_propt::new_variable() -{ - out << "l" << _no_variables << ": BOOLEAN;\n"; - literalt l; - l.set(_no_variables, false); - _no_variables++; - return l; -} - -literalt cvc_propt::def_cvc_literal() -{ - out << "l" << _no_variables << ": BOOLEAN = "; - literalt l; - l.set(_no_variables, false); - _no_variables++; - return l; -} - -void cvc_propt::lcnf(const bvt &bv) -{ - if(bv.empty()) - return; - bvt new_bv; - - std::set s; - - new_bv.reserve(bv.size()); - - for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++) - { - if(s.insert(*it).second) - new_bv.push_back(*it); - - if(s.find(!*it)!=s.end()) - return; // clause satisfied - - assert(it->var_no()<_no_variables); - } - - assert(!new_bv.empty()); - - out << "%% lcnf\n"; - out << "ASSERT "; - - for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++) - { - if(it!=new_bv.begin()) - out << " OR "; - out << cvc_literal(*it); - } - - out << ";\n\n"; -} - -std::string cvc_propt::cvc_literal(literalt l) -{ - if(l==const_literal(false)) - return "FALSE"; - else if(l==const_literal(true)) - return "TRUE"; - - if(l.sign()) - return "(NOT l"+std::to_string(l.var_no())+")"; - - return "l"+std::to_string(l.var_no()); -} - -propt::resultt cvc_propt::prop_solve() -{ - out << "QUERY FALSE;\n"; - return P_ERROR; -} diff --git a/src/solvers/cvc/cvc_prop.h b/src/solvers/cvc/cvc_prop.h deleted file mode 100644 index 82786e0a2bb..00000000000 --- a/src/solvers/cvc/cvc_prop.h +++ /dev/null @@ -1,88 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_CVC_CVC_PROP_H -#define CPROVER_SOLVERS_CVC_CVC_PROP_H - -#include - -#include - -#include - -class cvc_propt:virtual public propt -{ -public: - explicit cvc_propt(std::ostream &_out); - virtual ~cvc_propt(); - - virtual void land(literalt a, literalt b, literalt o); - virtual void lor(literalt a, literalt b, literalt o); - virtual void lxor(literalt a, literalt b, literalt o); - virtual void lnand(literalt a, literalt b, literalt o); - virtual void lnor(literalt a, literalt b, literalt o); - virtual void lequal(literalt a, literalt b, literalt o); - virtual void limplies(literalt a, literalt b, literalt o); - - virtual literalt land(literalt a, literalt b); - virtual literalt lor(literalt a, literalt b); - virtual literalt land(const bvt &bv); - virtual literalt lor(const bvt &bv); - virtual literalt lxor(const bvt &bv); - virtual literalt lxor(literalt a, literalt b); - virtual literalt lnand(literalt a, literalt b); - virtual literalt lnor(literalt a, literalt b); - virtual literalt lequal(literalt a, literalt b); - virtual literalt limplies(literalt a, literalt b); - virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c - virtual literalt new_variable(); - virtual size_t no_variables() const { return _no_variables; } - virtual void set_no_variables(size_t no) { assert(false); } - - virtual void lcnf(const bvt &bv); - - virtual const std::string solver_text() - { return "CVC"; } - - virtual tvt l_get(literalt literal) const - { - unsigned v=literal.var_no(); - if(v>=assignment.size()) - return tvt(tvt::tv_enumt::TV_UNKNOWN); - tvt r=assignment[v]; - return literal.sign()?!r:r; - } - - virtual propt::resultt prop_solve(); - - friend class cvc_convt; - friend class cvc_dect; - - virtual void clear() - { - assignment.clear(); - } - - void reset_assignment() - { - assignment.clear(); - assignment.resize(no_variables(), tvt(tvt::tv_enumt::TV_UNKNOWN)); - } - -protected: - unsigned _no_variables; - std::ostream &out; - - std::string cvc_literal(literalt l); - literalt def_cvc_literal(); - - std::vector assignment; -}; - -#endif // CPROVER_SOLVERS_CVC_CVC_PROP_H diff --git a/src/solvers/dplib/dplib_conv.cpp b/src/solvers/dplib/dplib_conv.cpp deleted file mode 100644 index a87cd0c25a2..00000000000 --- a/src/solvers/dplib/dplib_conv.cpp +++ /dev/null @@ -1,1170 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "dplib_conv.h" - -#include -#include - -#include -#include -#include -#include -#include -#include -#include - -#include - -std::string dplib_convt::bin_zero(unsigned bits) -{ - assert(bits!=0); - std::string result="0bin"; - while(bits!=0) { result+='0'; bits--; } - return result; -} - -std::string dplib_convt::dplib_pointer_type() -{ - assert(config.ansi_c.pointer_width!=0); - return "[# object: INT, offset: BITVECTOR("+ - std::to_string(config.ansi_c.pointer_width)+") #]"; -} - -std::string dplib_convt::array_index_type() -{ - return std::string("SIGNED [")+std::to_string(32)+"]"; -} - -typet dplib_convt::gen_array_index_type() -{ - typet t(ID_signedbv); - t.set(ID_width, 32); - return t; -} - -std::string dplib_convt::array_index(unsigned i) -{ - return "0bin"+integer2binary(i, config.ansi_c.int_width); -} - -void dplib_convt::convert_array_index(const exprt &expr) -{ - if(expr.type()==gen_array_index_type()) - { - convert_dplib_expr(expr); - } - else - { - exprt tmp(ID_typecast, gen_array_index_type()); - tmp.copy_to_operands(expr); - convert_dplib_expr(tmp); - } -} - -void dplib_convt::convert_address_of_rec(const exprt &expr) -{ - if(expr.id()==ID_symbol || - expr.id()==ID_constant || - expr.id()==ID_string_constant) - { - dplib_prop.out - << "(# object:=" - << pointer_logic.add_object(expr) - << ", offset:=" - << bin_zero(config.ansi_c.pointer_width) << " #)"; - } - else if(expr.id()==ID_index) - { - if(expr.operands().size()!=2) - throw "index takes two operands"; - - const exprt &array=expr.op0(); - const exprt &index=expr.op1(); - - if(index.is_zero()) - { - if(array.type().id()==ID_pointer) - convert_dplib_expr(array); - else if(array.type().id()==ID_array) - convert_address_of_rec(array); - else - assert(false); - } - else - { - dplib_prop.out << "(LET P: "; - dplib_prop.out << dplib_pointer_type(); - dplib_prop.out << " = "; - - if(array.type().id()==ID_pointer) - convert_dplib_expr(array); - else if(array.type().id()==ID_array) - convert_address_of_rec(array); - else - assert(false); - - dplib_prop.out << " IN P WITH .offset:=BVPLUS(" - << config.ansi_c.pointer_width - << ", P.offset, "; - convert_dplib_expr(index); - dplib_prop.out << "))"; - } - } - else if(expr.id()==ID_member) - { - if(expr.operands().size()!=1) - throw "member takes one operand"; - - const exprt &struct_op=expr.op0(); - - dplib_prop.out << "(LET P: "; - dplib_prop.out << dplib_pointer_type(); - dplib_prop.out << " = "; - - convert_address_of_rec(struct_op); - - const irep_idt &component_name= - to_member_expr(expr).get_component_name(); - - mp_integer offset=member_offset(ns, - to_struct_type(struct_op.type()), component_name); - assert(offset>=0); - - typet index_type(ID_unsignedbv); - index_type.set(ID_width, config.ansi_c.pointer_width); - - exprt index=from_integer(offset, index_type); - - dplib_prop.out << " IN P WITH .offset:=BVPLUS(" - << config.ansi_c.pointer_width - << ", P.offset, "; - convert_dplib_expr(index); - dplib_prop.out << "))"; - } - else - throw "don't know how to take address of: "+expr.id_string(); -} - -literalt dplib_convt::convert_rest(const exprt &expr) -{ - // dplib_prop.out << "%% E: " << expr << '\n'; - - literalt l=prop.new_variable(); - - find_symbols(expr); - - if(expr.id()==ID_equal || expr.id()==ID_notequal) - { - assert(expr.operands().size()==2); - - dplib_prop.out << "ASSERT " << dplib_prop.dplib_literal(l) << " <=> ("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ((expr.id()==ID_equal)?"=":"/="); - convert_dplib_expr(expr.op1()); - dplib_prop.out << ");\n"; - } - - return l; -} - -void dplib_convt::convert_identifier(const std::string &identifier) -{ - for(std::string::const_iterator - it=identifier.begin(); - it!=identifier.end(); - it++) - { - char ch=*it; - - if(isalnum(ch) || ch=='$' || ch=='?') - dplib_prop.out << ch; - else if(ch==':') - { - std::string::const_iterator next_it(it); - next_it++; - if(next_it!=identifier.end() && *next_it==':') - { - dplib_prop.out << "__"; - it=next_it; - } - else - { - dplib_prop.out << '_'; - dplib_prop.out << int(ch); - dplib_prop.out << '_'; - } - } - else - { - dplib_prop.out << '_'; - dplib_prop.out << int(ch); - dplib_prop.out << '_'; - } - } -} - -void dplib_convt::convert_as_bv(const exprt &expr) -{ - if(expr.type().id()==ID_bool) - { - dplib_prop.out << "IF "; - convert_dplib_expr(expr); - dplib_prop.out << " THEN 0bin1 ELSE 0bin0 ENDIF"; - } - else - convert_dplib_expr(expr); -} - -void dplib_convt::convert_array_value(const exprt &expr) -{ - convert_as_bv(expr); -} - -void dplib_convt::convert_dplib_expr(const exprt &expr) -{ - if(expr.id()==ID_symbol) - { - convert_identifier(expr.get_string(ID_identifier)); - } - else if(expr.id()==ID_nondet_symbol) - { - convert_identifier("nondet$"+expr.get_string(ID_identifier)); - } - else if(expr.id()==ID_typecast) - { - assert(expr.operands().size()==1); - const exprt &op=expr.op0(); - - if(expr.type().id()==ID_bool) - { - if(op.type().id()==ID_signedbv || - op.type().id()==ID_unsignedbv || - op.type().id()==ID_pointer) - { - convert_dplib_expr(op); - dplib_prop.out << "/="; - convert_dplib_expr(from_integer(0, op.type())); - } - else - { - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast1 "+op.type().id_string()+" -> bool"; - } - } - else if(expr.type().id()==ID_signedbv || - expr.type().id()==ID_unsignedbv) - { - unsigned to_width= - unsafe_string2unsigned(id2string(expr.type().get(ID_width))); - - if(op.type().id()==ID_signedbv) - { - unsigned from_width= - unsafe_string2unsigned(id2string(op.type().get(ID_width))); - - if(from_width==to_width) - convert_dplib_expr(op); - else if(from_width1) - { - dplib_prop.out << "(0bin"; - - for(unsigned i=1; i "+expr.type().id_string(); - } - } - else if(expr.type().id()==ID_pointer) - { - if(op.type().id()==ID_pointer) - { - convert_dplib_expr(op); - } - else - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast3 "+op.type().id_string()+" -> pointer"; - } - else - // NOLINTNEXTLINE(readability/throw) - throw "TODO typecast4 ? -> "+expr.type().id_string(); - } - else if(expr.id()==ID_struct) - { - dplib_prop.out << "(# "; - - const struct_typet &struct_type=to_struct_type(expr.type()); - - const struct_typet::componentst &components= - struct_type.components(); - - assert(components.size()==expr.operands().size()); - - unsigned i=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++, i++) - { - if(i!=0) - dplib_prop.out << ", "; - dplib_prop.out << it->get(ID_name); - dplib_prop.out << ":="; - convert_dplib_expr(expr.operands()[i]); - } - - dplib_prop.out << " #)"; - } - else if(expr.id()==ID_constant) - { - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv || - expr.type().id()==ID_bv) - { - dplib_prop.out << "0bin" << expr.get(ID_value); - } - else if(expr.type().id()==ID_pointer) - { - const irep_idt &value=expr.get(ID_value); - - if(value=="NULL") - { - dplib_prop.out << "(# object:=" - << pointer_logic.get_null_object() - << ", offset:=" - << bin_zero(config.ansi_c.pointer_width) << " #)"; - } - else - throw "unknown pointer constant: "+id2string(value); - } - else if(expr.type().id()==ID_bool) - { - if(expr.is_true()) - dplib_prop.out << "TRUE"; - else if(expr.is_false()) - dplib_prop.out << "FALSE"; - else - throw "unknown boolean constant"; - } - else if(expr.type().id()==ID_array) - { - dplib_prop.out << "ARRAY (i: " << array_index_type() << "):"; - - assert(!expr.operands().empty()); - - unsigned i=0; - forall_operands(it, expr) - { - if(i==0) - dplib_prop.out << "\n IF "; - else - dplib_prop.out << "\n ELSIF "; - - dplib_prop.out << "i=" << array_index(i) << " THEN "; - convert_array_value(*it); - i++; - } - - dplib_prop.out << "\n ELSE "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << "\n ENDIF"; - } - else if(expr.type().id()==ID_integer || - expr.type().id()==ID_natural || - expr.type().id()==ID_range) - { - dplib_prop.out << expr.get(ID_value); - } - else - throw "unknown constant: "+expr.type().id_string(); - } - else if(expr.id()==ID_concatenation || - expr.id()==ID_bitand || - expr.id()==ID_bitor) - { - dplib_prop.out << "("; - - forall_operands(it, expr) - { - if(it!=expr.operands().begin()) - { - if(expr.id()==ID_concatenation) - dplib_prop.out << " @ "; - else if(expr.id()==ID_bitand) - dplib_prop.out << " & "; - else if(expr.id()==ID_bitor) - dplib_prop.out << " | "; - } - - convert_as_bv(*it); - } - - dplib_prop.out << ")"; - } - else if(expr.id()==ID_bitxor) - { - assert(!expr.operands().empty()); - - if(expr.operands().size()==1) - { - convert_dplib_expr(expr.op0()); - } - else if(expr.operands().size()==2) - { - dplib_prop.out << "BVXOR("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - { - assert(expr.operands().size()>=3); - - exprt tmp(expr); - tmp.operands().resize(tmp.operands().size()-1); - - dplib_prop.out << "BVXOR("; - convert_dplib_expr(tmp); - dplib_prop.out << ", "; - convert_dplib_expr(expr.operands().back()); - dplib_prop.out << ")"; - } - } - else if(expr.id()==ID_bitnand) - { - assert(expr.operands().size()==2); - - dplib_prop.out << "BVNAND("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else if(expr.id()==ID_bitnot) - { - assert(expr.operands().size()==1); - dplib_prop.out << "~("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")"; - } - else if(expr.id()==ID_unary_minus) - { - assert(expr.operands().size()==1); - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - dplib_prop.out << "BVUMINUS("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")"; - } - else - throw "unsupported type for unary-: "+expr.type().id_string(); - } - else if(expr.id()==ID_if) - { - assert(expr.operands().size()==3); - dplib_prop.out << "IF "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << " THEN "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << " ELSE "; - convert_dplib_expr(expr.op2()); - dplib_prop.out << " ENDIF"; - } - else if(expr.id()==ID_and || - expr.id()==ID_or || - expr.id()==ID_xor) - { - assert(expr.type().id()==ID_bool); - - if(expr.operands().size()>=2) - { - forall_operands(it, expr) - { - if(it!=expr.operands().begin()) - { - if(expr.id()==ID_and) - dplib_prop.out << " AND "; - else if(expr.id()==ID_or) - dplib_prop.out << " OR "; - else if(expr.id()==ID_xor) - dplib_prop.out << " XOR "; - } - - dplib_prop.out << "("; - convert_dplib_expr(*it); - dplib_prop.out << ")"; - } - } - else if(expr.operands().size()==1) - { - convert_dplib_expr(expr.op0()); - } - else - assert(false); - } - else if(expr.id()==ID_not) - { - assert(expr.operands().size()==1); - dplib_prop.out << "NOT ("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")"; - } - else if(expr.id()==ID_equal || - expr.id()==ID_notequal) - { - assert(expr.operands().size()==2); - assert(expr.op0().type()==expr.op1().type()); - - if(expr.op0().type().id()==ID_bool) - { - if(expr.id()==ID_notequal) - dplib_prop.out << "NOT ("; - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ") <=> ("; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - if(expr.id()==ID_notequal) - dplib_prop.out << ")"; - } - else - { - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")"; - dplib_prop.out << (expr.id()==ID_equal?"=":"/="); - dplib_prop.out << "("; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - } - else if(expr.id()==ID_le || - expr.id()==ID_lt || - expr.id()==ID_ge || - expr.id()==ID_gt) - { - assert(expr.operands().size()==2); - - const typet &op_type=expr.op0().type(); - - if(op_type.id()==ID_unsignedbv) - { - if(expr.id()==ID_le) - dplib_prop.out << "BVLE"; - else if(expr.id()==ID_lt) - dplib_prop.out << "BVLT"; - else if(expr.id()==ID_ge) - dplib_prop.out << "BVGE"; - else if(expr.id()==ID_gt) - dplib_prop.out << "BVGT"; - - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else if(op_type.id()==ID_signedbv) - { - if(expr.id()==ID_le) - dplib_prop.out << "SBVLE"; - else if(expr.id()==ID_lt) - dplib_prop.out << "SBVLT"; - else if(expr.id()==ID_ge) - dplib_prop.out << "SBVGE"; - else if(expr.id()==ID_gt) - dplib_prop.out << "SBVGT"; - - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw - "unsupported type for "+expr.id_string()+": "+expr.type().id_string(); - } - else if(expr.id()==ID_plus) - { - if(expr.operands().size()>=2) - { - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - dplib_prop.out << "BVPLUS(" << expr.type().get(ID_width); - - forall_operands(it, expr) - { - dplib_prop.out << ", "; - convert_dplib_expr(*it); - } - - dplib_prop.out << ")"; - } - else if(expr.type().id()==ID_pointer) - { - if(expr.operands().size()!=2) - throw "pointer arithmetic with more than two operands"; - - const exprt *p, *i; - - if(expr.op0().type().id()==ID_pointer) - { - p=&expr.op0(); - i=&expr.op1(); - } - else if(expr.op1().type().id()==ID_pointer) - { - p=&expr.op1(); - i=&expr.op0(); - } - else - throw "unexpected mixture in pointer arithmetic"; - - dplib_prop.out << "(LET P: " << dplib_pointer_type() << " = "; - convert_dplib_expr(*p); - dplib_prop.out << " IN P WITH .offset:=BVPLUS(" - << config.ansi_c.pointer_width - << ", P.offset, "; - convert_dplib_expr(*i); - dplib_prop.out << "))"; - } - else - throw "unsupported type for +: "+expr.type().id_string(); - } - else if(expr.operands().size()==1) - { - convert_dplib_expr(expr.op0()); - } - else - assert(false); - } - else if(expr.id()==ID_minus) - { - if(expr.operands().size()==2) - { - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - dplib_prop.out << "BVSUB(" << expr.type().get(ID_width) << ", "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw "unsupported type for -: "+expr.type().id_string(); - } - else if(expr.operands().size()==1) - { - convert_dplib_expr(expr.op0()); - } - else - assert(false); - } - else if(expr.id()==ID_div) - { - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - if(expr.type().id()==ID_unsignedbv) - dplib_prop.out << "BVDIV"; - else - dplib_prop.out << "SBVDIV"; - - dplib_prop.out << "(" << expr.type().get(ID_width) << ", "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw "unsupported type for /: "+expr.type().id_string(); - } - else if(expr.id()==ID_mod) - { - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - if(expr.type().id()==ID_unsignedbv) - dplib_prop.out << "BVMOD"; - else - dplib_prop.out << "SBVMOD"; - - dplib_prop.out << "(" << expr.type().get(ID_width) << ", "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw "unsupported type for mod: "+expr.type().id_string(); - } - else if(expr.id()==ID_mult) - { - if(expr.operands().size()==2) - { - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - dplib_prop.out << "BVMULT(" << expr.type().get(ID_width) << ", "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw "unsupported type for *: "+expr.type().id_string(); - } - else if(expr.operands().size()==1) - { - convert_dplib_expr(expr.op0()); - } - else - assert(false); - } - else if(expr.id()==ID_address_of || - expr.id()=="reference_to") - { - assert(expr.operands().size()==1); - assert(expr.type().id()==ID_pointer); - convert_address_of_rec(expr.op0()); - } - else if(expr.id()==ID_array_of) - { - assert(expr.type().id()==ID_array); - assert(expr.operands().size()==1); - dplib_prop.out << "(ARRAY (i: " << array_index_type() << "): "; - convert_array_value(expr.op0()); - dplib_prop.out << ")"; - } - else if(expr.id()==ID_index) - { - assert(expr.operands().size()==2); - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")["; - convert_array_index(expr.op1()); - dplib_prop.out << "]"; - } - else if(expr.id()==ID_ashr || - expr.id()==ID_lshr || - expr.id()==ID_shl) - { - assert(expr.operands().size()==2); - - if(expr.type().id()==ID_unsignedbv || - expr.type().id()==ID_signedbv) - { - if(expr.id()==ID_ashr) - dplib_prop.out << "BVASHR"; - else if(expr.id()==ID_lshr) - dplib_prop.out << "BVLSHR"; - else if(expr.id()==ID_shl) - dplib_prop.out << "BVSHL"; - else - assert(false); - - dplib_prop.out << "(" << expr.type().get(ID_width) << ", "; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ", "; - convert_dplib_expr(expr.op1()); - dplib_prop.out << ")"; - } - else - throw - "unsupported type for "+expr.id_string()+": "+expr.type().id_string(); - } - else if(expr.id()==ID_with) - { - assert(expr.operands().size()>=1); - dplib_prop.out << "("; - convert_dplib_expr(expr.op0()); - dplib_prop.out << ")"; - - for(unsigned i=1; i s_set; - - ::find_symbols(expr.op1(), s_set); - - if(s_set.find(identifier)==s_set.end()) - { - id.type=expr.op0().type(); - - find_symbols(expr.op1()); - - convert_identifier(id2string(identifier)); - dplib_prop.out << ": "; - convert_dplib_type(expr.op0().type()); - dplib_prop.out << " = "; - convert_dplib_expr(expr.op1()); - - dplib_prop.out << ";\n\n"; - return; - } - } - } - } - - find_symbols(expr); - - dplib_prop.out << "AXIOM "; - - if(!value) - dplib_prop.out << "! ("; - - convert_dplib_expr(expr); - - if(!value) - dplib_prop.out << ")"; - - dplib_prop.out << ";\n\n"; -} - -void dplib_convt::find_symbols(const exprt &expr) -{ - find_symbols(expr.type()); - - forall_operands(it, expr) - find_symbols(*it); - - if(expr.id()==ID_symbol) - { - if(expr.type().id()==ID_code) - return; - - const irep_idt &identifier=expr.get(ID_identifier); - - identifiert &id=identifier_map[identifier]; - - if(id.type.is_nil()) - { - id.type=expr.type(); - - convert_identifier(id2string(identifier)); - dplib_prop.out << ": "; - convert_dplib_type(expr.type()); - dplib_prop.out << ";\n"; - } - } - else if(expr.id()==ID_nondet_symbol) - { - if(expr.type().id()==ID_code) - return; - - const irep_idt identifier="nondet$"+expr.get_string(ID_identifier); - - identifiert &id=identifier_map[identifier]; - - if(id.type.is_nil()) - { - id.type=expr.type(); - - convert_identifier(id2string(identifier)); - dplib_prop.out << ": "; - convert_dplib_type(expr.type()); - dplib_prop.out << ";\n"; - } - } -} - -void dplib_convt::convert_dplib_type(const typet &type) -{ - if(type.id()==ID_array) - { - const array_typet &array_type=to_array_type(type); - - dplib_prop.out << "ARRAY " << array_index_type() - << " OF "; - - if(array_type.subtype().id()==ID_bool) - dplib_prop.out << "BITVECTOR(1)"; - else - convert_dplib_type(array_type.subtype()); - } - else if(type.id()==ID_bool) - { - dplib_prop.out << "boolean"; - } - else if(type.id()==ID_struct || - type.id()==ID_union) - { - const struct_typet &struct_type=to_struct_type(type); - - dplib_prop.out << "[#"; - - const struct_typet::componentst &components= - struct_type.components(); - - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) - { - if(it!=components.begin()) - dplib_prop.out << ","; - dplib_prop.out << " "; - dplib_prop.out << it->get(ID_name); - dplib_prop.out << ": "; - convert_dplib_type(it->type()); - } - - dplib_prop.out << " #]"; - } - else if(type.id()==ID_pointer || - type.id()==ID_reference) - { - dplib_prop.out << dplib_pointer_type(); - } - else if(type.id()==ID_integer) - { - dplib_prop.out << "int"; - } - else if(type.id()==ID_signedbv) - { - unsigned width=to_signedbv_type(type).get_width(); - - if(width==0) - throw "zero-width vector type: "+type.id_string(); - - dplib_prop.out << "signed[" << width << "]"; - } - else if(type.id()==ID_unsignedbv) - { - unsigned width=to_unsignedbv_type(type).get_width(); - - if(width==0) - throw "zero-width vector type: "+type.id_string(); - - dplib_prop.out << "unsigned[" << width << "]"; - } - else if(type.id()==ID_bv) - { - unsigned width=to_bv_type(type).get_width(); - - if(width==0) - throw "zero-width vector type: "+type.id_string(); - - dplib_prop.out << "bv[" << width << "]"; - } - else - throw "unsupported type: "+type.id_string(); -} - -void dplib_convt::find_symbols(const typet &type) -{ - if(type.id()==ID_array) - { - const array_typet &array_type=to_array_type(type); - find_symbols(array_type.size()); - } - else if(type.id()==ID_struct || - type.id()==ID_union) - { - } -} diff --git a/src/solvers/dplib/dplib_conv.h b/src/solvers/dplib/dplib_conv.h deleted file mode 100644 index 74034d6c1e2..00000000000 --- a/src/solvers/dplib/dplib_conv.h +++ /dev/null @@ -1,73 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H -#define CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H - - -#include -#include - -#include "dplib_prop.h" - -class dplib_convt:public prop_convt -{ -public: - dplib_convt( - const namespacet &_ns, - std::ostream &_out): - prop_convt(_ns), - out(_out), - pointer_logic(_ns) { } - - virtual ~dplib_convt() { } - -protected: - std::ostream &out; - - virtual literalt convert_rest(const exprt &expr); - virtual void convert_dplib_expr(const exprt &expr); - virtual void convert_dplib_type(const typet &type); - virtual void set_to(const exprt &expr, bool value); - virtual void convert_address_of_rec(const exprt &expr); - - pointer_logict pointer_logic; - -private: - void convert_identifier(const std::string &identifier); - void find_symbols(const exprt &expr); - void find_symbols(const typet &type); - void convert_array_value(const exprt &expr); - void convert_as_bv(const exprt &expr); - void convert_array_index(const exprt &expr); - static typet gen_array_index_type(); - static std::string bin_zero(unsigned bits); - static std::string array_index_type(); - static std::string array_index(unsigned i); - static std::string dplib_pointer_type(); - - struct identifiert - { - typet type; - exprt value; - - identifiert() - { - type.make_nil(); - value.make_nil(); - } - }; - - typedef std::unordered_map - identifier_mapt; - - identifier_mapt identifier_map; -}; - -#endif // CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H diff --git a/src/solvers/dplib/dplib_dec.cpp b/src/solvers/dplib/dplib_dec.cpp deleted file mode 100644 index 111805276ba..00000000000 --- a/src/solvers/dplib/dplib_dec.cpp +++ /dev/null @@ -1,159 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "dplib_dec.h" - -#include -#include - -#if defined(__linux__) || \ - defined(__FreeBSD_kernel__) || \ - defined(__GNU__) || \ - defined(__unix__) || \ - defined(__CYGWIN__) || \ - defined(__MACH__) -#include -#endif - -#ifdef _WIN32 -#include -#define getpid _getpid -#endif - -#include -#include - -dplib_temp_filet::dplib_temp_filet() -{ - temp_out_filename="dplib_dec_out_"+std::to_string(getpid())+".tmp"; - - temp_out.open( - temp_out_filename.c_str(), - std::ios_base::out | std::ios_base::trunc); -} - -dplib_temp_filet::~dplib_temp_filet() -{ - temp_out.close(); - - if(temp_out_filename!="") - unlink(temp_out_filename.c_str()); - - if(temp_result_filename!="") - unlink(temp_result_filename.c_str()); -} - -decision_proceduret::resultt dplib_dect::dec_solve() -{ - dplib_prop.out << "QUERY FALSE;\n"; - dplib_prop.out << "COUNTERMODEL;\n"; - - post_process(); - - temp_out.close(); - - temp_result_filename= - "dplib_dec_result_"+std::to_string(getpid())+".tmp"; - - std::string command= - "dplibl "+temp_out_filename+" > "+temp_result_filename+" 2>&1"; - - int res=system(command.c_str()); - assert(0 == res); - - status("Reading result from CVCL"); - - return read_dplib_result(); -} - -void dplib_dect::read_assert(std::istream &in, std::string &line) -{ - // strip ASSERT - line=std::string(line, strlen("ASSERT "), std::string::npos); - if(line=="") - return; - - // bit-vector - if(line[0]=='(') - { - // get identifier - std::string::size_type pos= - line.find(' '); - - std::string identifier=std::string(line, 1, pos-1); - - // get value - if(!std::getline(in, line)) - return; - - // skip spaces - pos=0; - while(pos" << identifier << "< = >" << value << "<\n"; - #endif - } - else - { - // boolean - tvt value=tvt(true); - - if(has_prefix(line, "NOT ")) - { - line=std::string(line, strlen("NOT "), std::string::npos); - value=tvt(false); - } - - if(line=="") - return; - - if(line[0]=='l') - { - unsigned number=unsafe_str2unsigned(line.c_str()+1); - assert(number - -#include "dplib_conv.h" - -class dplib_temp_filet -{ -public: - dplib_temp_filet(); - ~dplib_temp_filet(); - -protected: - std::ofstream temp_out; - std::string temp_out_filename, temp_result_filename; -}; - -class dplib_dect:protected dplib_temp_filet, public dplib_convt -{ -public: - explicit dplib_dect(const namespacet &_ns): - dplib_convt(_ns, temp_out) - { - } - - virtual resultt dec_solve(); - -protected: - resultt read_dplib_result(); - void read_assert(std::istream &in, std::string &line); -}; - -#endif // CPROVER_SOLVERS_DPLIB_DPLIB_DEC_H diff --git a/src/solvers/dplib/dplib_prop.cpp b/src/solvers/dplib/dplib_prop.cpp deleted file mode 100644 index a0111b3b8fc..00000000000 --- a/src/solvers/dplib/dplib_prop.cpp +++ /dev/null @@ -1,305 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "dplib_prop.h" - -#include - -#include - -dplib_propt::dplib_propt(std::ostream &_out):out(_out) -{ - // we skip index 0 - _no_variables=1; -} - -void dplib_propt::land(literalt a, literalt b, literalt o) -{ - out << "// land\n"; - out << "AXIOM (" << dplib_literal(a) << " & " - << dplib_literal(b) << ") <=> " << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::lor(literalt a, literalt b, literalt o) -{ - out << "// lor\n"; - out << "AXIOM (" << dplib_literal(a) << " | " - << dplib_literal(b) << ") <=> " << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::lxor(literalt a, literalt b, literalt o) -{ - out << "// lxor\n"; - out << "AXIOM (" << dplib_literal(a) << " <=> " - << dplib_literal(b) << ") <=> !" << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::lnand(literalt a, literalt b, literalt o) -{ - out << "// lnand\n"; - out << "AXIOM (" << dplib_literal(a) << " & " - << dplib_literal(b) << ") <=> !" << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::lnor(literalt a, literalt b, literalt o) -{ - out << "// lnor\n"; - out << "AXIOM (" << dplib_literal(a) << " | " - << dplib_literal(b) << ") <=> !" << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::lequal(literalt a, literalt b, literalt o) -{ - out << "// lequal\n"; - out << "AXIOM (" << dplib_literal(a) << " <=> " - << dplib_literal(b) << ") <=> " << dplib_literal(o) - << ";\n\n"; -} - -void dplib_propt::limplies(literalt a, literalt b, literalt o) -{ - out << "// limplies\n"; - out << "AXIOM (" << dplib_literal(a) << " => " - << dplib_literal(b) << ") <=> " << dplib_literal(o) - << ";\n\n"; -} - -literalt dplib_propt::land(const bvt &bv) -{ - out << "// land\n"; - - literalt literal=def_dplib_literal(); - - forall_literals(it, bv) - { - if(it!=bv.begin()) - out << " & "; - out << dplib_literal(*it); - } - - out << "\n\n"; - - return literal; -} - -literalt dplib_propt::lor(const bvt &bv) -{ - out << "// lor\n"; - - literalt literal=def_dplib_literal(); - - forall_literals(it, bv) - { - if(it!=bv.begin()) - out << " | "; - out << dplib_literal(*it); - } - - out << "\n\n"; - - return literal; -} - -literalt dplib_propt::lxor(const bvt &bv) -{ - if(bv.empty()) - return const_literal(false); - if(bv.size()==1) - return bv[0]; - if(bv.size()==2) - return lxor(bv[0], bv[1]); - - literalt literal=const_literal(false); - - forall_literals(it, bv) - literal=lxor(*it, literal); - - return literal; -} - -literalt dplib_propt::land(literalt a, literalt b) -{ - if(a==const_literal(true)) - return b; - if(b==const_literal(true)) - return a; - if(a==const_literal(false)) - return const_literal(false); - if(b==const_literal(false)) - return const_literal(false); - if(a==b) - return a; - - literalt o=def_dplib_literal(); - out << dplib_literal(a) << " & " << dplib_literal(b) - << ";\n\n"; - - return o; -} - -literalt dplib_propt::lor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return const_literal(true); - if(b==const_literal(true)) - return const_literal(true); - if(a==b) - return a; - - literalt o=def_dplib_literal(); - out << dplib_literal(a) << " | " << dplib_literal(b) - << ";\n\n"; - - return o; -} - -literalt dplib_propt::lxor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - literalt o=def_dplib_literal(); - out << "!(" << dplib_literal(a) << " <-> " << dplib_literal(b) - << ");\n\n"; - - return o; -} - -literalt dplib_propt::lnand(literalt a, literalt b) -{ - return !land(a, b); -} - -literalt dplib_propt::lnor(literalt a, literalt b) -{ - return !lor(a, b); -} - -literalt dplib_propt::lequal(literalt a, literalt b) -{ - return !lxor(a, b); -} - -literalt dplib_propt::limplies(literalt a, literalt b) -{ - return lor(!a, b); -} - -literalt dplib_propt::lselect(literalt a, literalt b, literalt c) -{ - if(a==const_literal(true)) - return b; - if(a==const_literal(false)) - return c; - if(b==c) - return b; - - out << "// lselect\n"; - - literalt o=def_dplib_literal(); - - out << "IF " << dplib_literal(a) << " THEN " - << dplib_literal(b) << " ELSE " - << dplib_literal(c) << " ENDIF;\n\n"; - - return o; -} - -literalt dplib_propt::new_variable() -{ - _no_variables++; - out << "l" << _no_variables << ": boolean;\n"; - literalt l; - l.set(_no_variables, false); - return l; -} - -literalt dplib_propt::def_dplib_literal() -{ - _no_variables++; - out << "l" << _no_variables << ": boolean = "; - literalt l; - l.set(_no_variables, false); - return l; -} - -void dplib_propt::lcnf(const bvt &bv) -{ - if(bv.empty()) - return; - bvt new_bv; - - std::set s; - - new_bv.reserve(bv.size()); - - for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++) - { - if(s.insert(*it).second) - new_bv.push_back(*it); - - if(s.find(!*it)!=s.end()) - return; // clause satisfied - - assert(it->var_no()<=_no_variables); - } - - assert(!new_bv.empty()); - - out << "// lcnf\n"; - out << "AXIOM "; - - for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++) - { - if(it!=new_bv.begin()) - out << " | "; - out << dplib_literal(*it); - } - - out << ";\n\n"; -} - -std::string dplib_propt::dplib_literal(literalt l) -{ - if(l==const_literal(false)) - return "FALSE"; - else if(l==const_literal(true)) - return "TRUE"; - - if(l.sign()) - return "(NOT l"+std::to_string(l.var_no())+")"; - - return "l"+std::to_string(l.var_no()); -} - -void dplib_propt::finish() -{ - // we want satisfiability - out << "THEOREM false;\n"; -} - -propt::resultt dplib_propt::prop_solve() -{ - finish(); - return P_ERROR; -} diff --git a/src/solvers/dplib/dplib_prop.h b/src/solvers/dplib/dplib_prop.h deleted file mode 100644 index 89441646093..00000000000 --- a/src/solvers/dplib/dplib_prop.h +++ /dev/null @@ -1,91 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H -#define CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H - -#include - -#include - -#include - -class dplib_propt:virtual public propt -{ -public: - explicit dplib_propt(std::ostream &_out); - virtual ~dplib_propt() { } - - virtual void land(literalt a, literalt b, literalt o); - virtual void lor(literalt a, literalt b, literalt o); - virtual void lxor(literalt a, literalt b, literalt o); - virtual void lnand(literalt a, literalt b, literalt o); - virtual void lnor(literalt a, literalt b, literalt o); - virtual void lequal(literalt a, literalt b, literalt o); - virtual void limplies(literalt a, literalt b, literalt o); - - virtual literalt land(literalt a, literalt b); - virtual literalt lor(literalt a, literalt b); - virtual literalt land(const bvt &bv); - virtual literalt lor(const bvt &bv); - virtual literalt lxor(const bvt &bv); - virtual literalt lxor(literalt a, literalt b); - virtual literalt lnand(literalt a, literalt b); - virtual literalt lnor(literalt a, literalt b); - virtual literalt lequal(literalt a, literalt b); - virtual literalt limplies(literalt a, literalt b); - virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c - virtual literalt new_variable(); - virtual size_t no_variables() const { return _no_variables; } - virtual void set_no_variables(size_t no) { assert(false); } - // virtual unsigned no_clauses()=0; - - virtual void lcnf(const bvt &bv); - - virtual const std::string solver_text() - { return "DPLIB"; } - - virtual tvt l_get(literalt literal) const - { - unsigned v=literal.var_no(); - if(v>=assignment.size()) - return tvt::unknown(); - tvt r=assignment[v]; - return literal.sign()?!r:r; - } - - virtual propt::resultt prop_solve(); - - friend class dplib_convt; - friend class dplib_dect; - - virtual void clear() - { - assignment.clear(); - } - - void reset_assignment() - { - assignment.clear(); - assignment.resize(no_variables(), tvt::unknown()); - } - -protected: - unsigned _no_variables; - std::ostream &out; - - std::string dplib_literal(literalt l); - literalt def_dplib_literal(); - - std::vector assignment; - - void finish(); -}; - -#endif // CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H diff --git a/src/solvers/floatbv/float_approximation.cpp b/src/solvers/floatbv/float_approximation.cpp index 6a70b5f5091..2c73e517999 100644 --- a/src/solvers/floatbv/float_approximation.cpp +++ b/src/solvers/floatbv/float_approximation.cpp @@ -42,7 +42,7 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent) if(over_approximate) shifted_fraction=overapproximating_left_shift(fraction, i); else - shifted_fraction=bv_utils.shift(fraction, bv_utilst::LEFT, i); + shifted_fraction=bv_utils.shift(fraction, bv_utilst::shiftt::LEFT, i); bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction); diff --git a/src/solvers/floatbv/float_approximation.h b/src/solvers/floatbv/float_approximation.h index daaaac8c7f3..a3193126465 100644 --- a/src/solvers/floatbv/float_approximation.h +++ b/src/solvers/floatbv/float_approximation.h @@ -12,7 +12,7 @@ Module: Floating Point with under/over-approximation #ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_APPROXIMATION_H #define CPROVER_SOLVERS_FLOATBV_FLOAT_APPROXIMATION_H -#include +#include "float_utils.h" class float_approximationt:public float_utilst { diff --git a/src/solvers/smt1/smt1_prop.cpp b/src/solvers/smt1/smt1_prop.cpp deleted file mode 100644 index 481d0d289c5..00000000000 --- a/src/solvers/smt1/smt1_prop.cpp +++ /dev/null @@ -1,297 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -Revisions: Roberto Bruttomesso, roberto.bruttomesso@unisi.ch - -\*******************************************************************/ - -#include "smt1_prop.h" - -#include - -smt1_propt::smt1_propt( - const std::string &benchmark, - const std::string &source, - const std::string &logic, - std::ostream &_out):out(_out) -{ - out << "(benchmark " << benchmark << "\n"; - out << ":source { " << source << " }" << "\n"; - out << ":status unknown" << "\n"; - out << ":logic " << logic << " ; SMT1" << "\n"; - _no_variables=0; -} - -smt1_propt::~smt1_propt() -{ -} - -void smt1_propt::finalize() -{ - out << "\n"; - out << ":formula true" << "\n"; - out << ") ; benchmark" << "\n"; -} - -literalt smt1_propt::land(const bvt &bv) -{ - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; land" << "\n"; - out << " (iff " << smt1_literal(l) << " (and"; - - forall_literals(it, bv) - out << " " << smt1_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::lor(const bvt &bv) -{ - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; lor" << "\n"; - out << " (iff " << smt1_literal(l) << " (or"; - - forall_literals(it, bv) - out << " " << smt1_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::lxor(const bvt &bv) -{ - if(bv.empty()) - return const_literal(false); - if(bv.size()==1) - return bv[0]; - - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; lxor" << "\n"; - out << " (iff " << smt1_literal(l) << " (xor"; - - forall_literals(it, bv) - out << " " << smt1_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::land(literalt a, literalt b) -{ - if(a==const_literal(true)) - return b; - if(b==const_literal(true)) - return a; - if(a==const_literal(false)) - return const_literal(false); - if(b==const_literal(false)) - return const_literal(false); - if(a==b) - return a; - - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; land" << "\n"; - out << " (iff " << smt1_literal(l) << " (and"; - out << " " << smt1_literal(a); - out << " " << smt1_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::lor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return const_literal(true); - if(b==const_literal(true)) - return const_literal(true); - if(a==b) - return a; - - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; lor" << "\n"; - out << " (iff " << smt1_literal(l) << " (or"; - out << " " << smt1_literal(a); - out << " " << smt1_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::lxor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; lxor" << "\n"; - out << " (iff " << smt1_literal(l) << " (xor"; - out << " " << smt1_literal(a); - out << " " << smt1_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt1_propt::lnand(literalt a, literalt b) -{ - return !land(a, b); -} - -literalt smt1_propt::lnor(literalt a, literalt b) -{ - return !lor(a, b); -} - -literalt smt1_propt::lequal(literalt a, literalt b) -{ - return !lxor(a, b); -} - -literalt smt1_propt::limplies(literalt a, literalt b) -{ - return lor(!a, b); -} - -literalt smt1_propt::lselect(literalt a, literalt b, literalt c) -{ - if(a==const_literal(true)) - return b; - if(a==const_literal(false)) - return c; - if(b==c) - return b; - - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - out << "\n"; - - literalt l=new_variable(); - - out << ":assumption ; lselect" << "\n"; - out << " (iff " << smt1_literal(l) << "(if_then_else " - << smt1_literal(a) << " " << smt1_literal(b) << " " - << smt1_literal(c) << ")" << "\n"; - - return l; -} - -literalt smt1_propt::new_variable() -{ - literalt l; - l.set(_no_variables, false); - _no_variables++; - - out << ":extrapreds((" << smt1_literal(l) << "))" << "\n"; - - return l; -} - -void smt1_propt::lcnf(const bvt &bv) -{ - out << "\n"; - out << ":assumption ; lcnf" << "\n"; - out << " "; - - if(bv.empty()) - out << "false ; the empty clause"; - else if(bv.size()==1) - out << smt1_literal(bv.front()); - else - { - out << "(or"; - - for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++) - out << " " << smt1_literal(*it); - - out << ")"; - } - - out << "\n"; -} - -std::string smt1_propt::smt1_literal(literalt l) -{ - if(l==const_literal(false)) - return "false"; - else if(l==const_literal(true)) - return "true"; - - std::string v="B"+std::to_string(l.var_no()); - - if(l.sign()) - return "(not "+v+")"; - - return v; -} - -tvt smt1_propt::l_get(literalt literal) const -{ - if(literal.is_true()) - return tvt(true); - if(literal.is_false()) - return tvt(false); - - unsigned v=literal.var_no(); - if(v>=assignment.size()) - return tvt(tvt::tv_enumt::TV_UNKNOWN); - tvt r=assignment[v]; - return literal.sign()?!r:r; -} - -void smt1_propt::set_assignment(literalt literal, bool value) -{ - if(literal.is_true() || literal.is_false()) - return; - - unsigned v=literal.var_no(); - assert(v - -#include - -#include - -class smt1_propt:public propt -{ -public: - smt1_propt( - const std::string &_benchmark, - const std::string &_source, - const std::string &_logic, - std::ostream &_out); - virtual ~smt1_propt(); - - virtual literalt land(literalt a, literalt b); - virtual literalt lor(literalt a, literalt b); - virtual literalt land(const bvt &bv); - virtual literalt lor(const bvt &bv); - virtual literalt lxor(const bvt &bv); - virtual literalt lxor(literalt a, literalt b); - virtual literalt lnand(literalt a, literalt b); - virtual literalt lnor(literalt a, literalt b); - virtual literalt lequal(literalt a, literalt b); - virtual literalt limplies(literalt a, literalt b); - virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c - - virtual literalt new_variable(); - virtual size_t no_variables() const { return _no_variables; } - virtual void set_no_variables(size_t no) { assert(false); } - - virtual void lcnf(const bvt &bv); - - virtual const std::string solver_text() - { return "SMT"; } - - virtual tvt l_get(literalt literal) const; - virtual void set_assignment(literalt a, bool value); - - virtual propt::resultt prop_solve(); - - virtual void clear() - { - assignment.clear(); - } - - virtual void reset_assignment() - { - assignment.clear(); - assignment.resize(no_variables(), tvt(tvt::tv_enumt::TV_UNKNOWN)); - } - - friend class smt1_convt; - friend class smt1_dect; - - void finalize(); - -protected: - size_t _no_variables; - std::ostream &out; - - std::string smt1_literal(literalt l); - literalt def_smt1_literal(); - - std::vector assignment; -}; - -#endif // CPROVER_SOLVERS_SMT1_SMT1_PROP_H diff --git a/src/solvers/smt2/smt2_prop.cpp b/src/solvers/smt2/smt2_prop.cpp deleted file mode 100644 index d6810e5d0c0..00000000000 --- a/src/solvers/smt2/smt2_prop.cpp +++ /dev/null @@ -1,334 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "smt2_prop.h" - -#include - -smt2_propt::smt2_propt( - const std::string &benchmark, - const std::string &source, - const std::string &logic, - bool _core_enabled, - std::ostream &_out): - out(_out), - core_enabled(_core_enabled) -{ - out << "; SMT 2" << "\n"; - - out << "(set-info :source \"" << source << "\")" << "\n"; - out << "(set-option :produce-models true)" << "\n"; - - if(core_enabled) - { - out << "(set-option :produce-unsat-cores true)" << "\n"; - } - - out << "(set-logic " << logic << ")" << "\n"; - - _no_variables=0; -} - -smt2_propt::~smt2_propt() -{ -} - -void smt2_propt::finalize() -{ - out << "\n"; - out << "(check-sat)" << "\n"; - out << "\n"; - - for(smt2_identifierst::const_iterator - it=smt2_identifiers.begin(); - it!=smt2_identifiers.end(); - it++) - out << "(get-value (" << *it << "))" << "\n"; - - out << "\n"; - - if(core_enabled) - out << "(get-unsat-core)" << "\n"; - - out << "; end of SMT2 file" << "\n"; -} - -literalt smt2_propt::land(const bvt &bv) -{ - out << "\n"; - - literalt l=define_new_variable(); - - out << "; land" << "\n"; - out << " (and"; - - forall_literals(it, bv) - out << " " << smt2_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::lor(const bvt &bv) -{ - out << "\n"; - - literalt l=define_new_variable(); - - out << "; lor" << "\n"; - out << " (or"; - - forall_literals(it, bv) - out << " " << smt2_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::lxor(const bvt &bv) -{ - if(bv.empty()) - return const_literal(false); - if(bv.size()==1) - return bv[0]; - - out << "\n"; - - literalt l=define_new_variable(); - - out << "; lxor" << "\n"; - out << " (xor"; - - forall_literals(it, bv) - out << " " << smt2_literal(*it); - - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::land(literalt a, literalt b) -{ - if(a==const_literal(true)) - return b; - if(b==const_literal(true)) - return a; - if(a==const_literal(false)) - return const_literal(false); - if(b==const_literal(false)) - return const_literal(false); - if(a==b) - return a; - - out << "\n"; - - literalt l=define_new_variable(); - - out << "; land" << "\n"; - out << " (and"; - out << " " << smt2_literal(a); - out << " " << smt2_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::lor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return const_literal(true); - if(b==const_literal(true)) - return const_literal(true); - if(a==b) - return a; - - out << "\n"; - - literalt l=define_new_variable(); - - out << "; lor" << "\n"; - out << " (or"; - out << " " << smt2_literal(a); - out << " " << smt2_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::lxor(literalt a, literalt b) -{ - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - out << "\n"; - - literalt l=new_variable(); - - out << "; lxor" << "\n"; - out << " (xor"; - out << " " << smt2_literal(a); - out << " " << smt2_literal(b); - out << "))" << "\n"; - - return l; -} - -literalt smt2_propt::lnand(literalt a, literalt b) -{ - return !land(a, b); -} - -literalt smt2_propt::lnor(literalt a, literalt b) -{ - return !lor(a, b); -} - -literalt smt2_propt::lequal(literalt a, literalt b) -{ - return !lxor(a, b); -} - -literalt smt2_propt::limplies(literalt a, literalt b) -{ - return lor(!a, b); -} - -literalt smt2_propt::lselect(literalt a, literalt b, literalt c) -{ - if(a==const_literal(true)) - return b; - if(a==const_literal(false)) - return c; - if(b==c) - return b; - - if(a==const_literal(false)) - return b; - if(b==const_literal(false)) - return a; - if(a==const_literal(true)) - return !b; - if(b==const_literal(true)) - return !a; - - out << "\n"; - - literalt l=define_new_variable(); - - out << "; lselect" << "\n"; - out << " (if_then_else " - << smt2_literal(a) << " " << smt2_literal(b) << " " - << smt2_literal(c) << "))" << "\n"; - - return l; -} - -literalt smt2_propt::new_variable() -{ - literalt l; - l.set(_no_variables, false); - _no_variables++; - - out << "(declare-fun " << smt2_literal(l) << " () Bool)" << "\n"; - - return l; -} - -literalt smt2_propt::define_new_variable() -{ - literalt l; - l.set(_no_variables, false); - _no_variables++; - - out << "(define-fun " << smt2_literal(l) << " () Bool "; - // The command is continued elsewhere, and the - // closing parenthesis is missing! - - return l; -} - -void smt2_propt::lcnf(const bvt &bv) -{ - out << "\n"; - out << "(assert ; lcnf" << "\n"; - out << " "; - - if(bv.empty()) - out << "false"; - else if(bv.size()==1) - out << smt2_literal(bv.front()); - else - { - out << "(or"; - - for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++) - out << " " << smt2_literal(*it); - - out << ")"; - } - - out << ")" << "\n"; -} - -std::string smt2_propt::smt2_literal(literalt l) -{ - if(l==const_literal(false)) - return "false"; - else if(l==const_literal(true)) - return "true"; - - std::string v="B"+std::to_string(l.var_no()); - - smt2_identifiers.insert(v); - - if(l.sign()) - return "(not "+v+")"; - - return v; -} - -tvt smt2_propt::l_get(literalt literal) const -{ - if(literal.is_true()) - return tvt(true); - if(literal.is_false()) - return tvt(false); - - unsigned v=literal.var_no(); - if(v>=assignment.size()) - return tvt(tvt::tv_enumt::TV_UNKNOWN); - tvt r=assignment[v]; - return literal.sign()?!r:r; -} - -void smt2_propt::set_assignment(literalt literal, bool value) -{ - if(literal.is_true() || literal.is_false()) - return; - - unsigned v=literal.var_no(); - assert(v -#include - -#include - -#include - -class smt2_propt:public propt -{ -public: - smt2_propt( - const std::string &_benchmark, - const std::string &_source, - const std::string &_logic, - bool _core_enabled, - std::ostream &_out); - virtual ~smt2_propt(); - - virtual literalt land(literalt a, literalt b); - virtual literalt lor(literalt a, literalt b); - virtual literalt land(const bvt &bv); - virtual literalt lor(const bvt &bv); - virtual literalt lxor(const bvt &bv); - virtual literalt lxor(literalt a, literalt b); - virtual literalt lnand(literalt a, literalt b); - virtual literalt lnor(literalt a, literalt b); - virtual literalt lequal(literalt a, literalt b); - virtual literalt limplies(literalt a, literalt b); - virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c - - virtual literalt new_variable(); - virtual size_t no_variables() const { return _no_variables; } - virtual void set_no_variables(size_t no) { assert(false); } - - virtual void lcnf(const bvt &bv); - - virtual const std::string solver_text() - { return "SMT"; } - - virtual tvt l_get(literalt literal) const; - virtual void set_assignment(literalt a, bool value); - - virtual propt::resultt prop_solve(); - - virtual void clear() - { - assignment.clear(); - } - - virtual void reset_assignment() - { - assignment.clear(); - assignment.resize(no_variables(), tvt(tvt::tv_enumt::TV_UNKNOWN)); - } - - friend class smt2_convt; - friend class smt2_dect; - - void finalize(); - -protected: - size_t _no_variables; - std::ostream &out; - - std::string smt2_literal(literalt l); - literalt def_smt2_literal(); - - std::vector assignment; - - literalt define_new_variable(); - - typedef std::set smt2_identifierst; - smt2_identifierst smt2_identifiers; - - bool core_enabled; -}; - -#endif // CPROVER_SOLVERS_SMT2_SMT2_PROP_H