diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 326e6e8bce3..d8cb835e4a8 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -18,6 +18,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ graphml_witness.cpp remove_virtual_functions.cpp \ class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ + show_goto_functions_json.cpp \ + show_goto_functions_xml.cpp \ remove_static_init_loops.cpp remove_instanceof.cpp INCLUDES= -I .. diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 82f59d7988a..f5e9999114d 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -19,10 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com Function: goto_programt::output_instruction Inputs: + ns - the namespace to resolve the expressions in + identifier - the identifier used to find a symbol to identify the + source language + out - the stream to write the goto string to + it - an iterator pointing to the instruction to convert - Outputs: + Outputs: See below. - Purpose: + Purpose: See below. \*******************************************************************/ @@ -32,51 +37,81 @@ std::ostream& goto_programt::output_instruction( std::ostream& out, instructionst::const_iterator it) const { - out << " // " << it->location_number << " "; + return output_instruction(ns, identifier, out, *it); +} + +/*******************************************************************\ + +Function: goto_programt::output_instruction + + Inputs: + ns - the namespace to resolve the expressions in + identifier - the identifier used to find a symbol to identify the + source language + out - the stream to write the goto string to + instruction - the instruction to convert - if(!it->source_location.is_nil()) - out << it->source_location.as_string(); + Outputs: Appends to out a two line representation of the instruction + + Purpose: Writes to out a two line string representation of the specific + instruction. It is of the format: + // {location} file {source file} line {line in source file} + {representation of the instruction} + +\*******************************************************************/ + +std::ostream &goto_programt::output_instruction( + const namespacet &ns, + const irep_idt &identifier, + std::ostream &out, + const goto_program_templatet::instructiont &instruction) const +{ + out << " // " << instruction.location_number << " "; + + if(!instruction.source_location.is_nil()) + out << instruction.source_location.as_string(); else out << "no location"; out << "\n"; - if(!it->labels.empty()) + if(!instruction.labels.empty()) { out << " // Labels:"; - for(const auto &label : it->labels) + for(const auto &label : instruction.labels) out << " " << label; out << '\n'; } - if(it->is_target()) - out << std::setw(6) << it->target_number << ": "; + if(instruction.is_target()) + out << std::setw(6) << instruction.target_number << ": "; else out << " "; - switch(it->type) + switch(instruction.type) { case NO_INSTRUCTION_TYPE: out << "NO INSTRUCTION TYPE SET" << '\n'; break; case GOTO: - if(!it->guard.is_true()) + if(!instruction.guard.is_true()) { out << "IF " - << from_expr(ns, identifier, it->guard) + << from_expr(ns, identifier, instruction.guard) << " THEN "; } out << "GOTO "; for(instructiont::targetst::const_iterator - gt_it=it->targets.begin(); - gt_it!=it->targets.end(); + gt_it=instruction.targets.begin(); + gt_it!=instruction.targets.end(); gt_it++) { - if(gt_it!=it->targets.begin()) out << ", "; + if(gt_it!=instruction.targets.begin()) + out << ", "; out << (*gt_it)->target_number; } @@ -89,20 +124,20 @@ std::ostream& goto_programt::output_instruction( case DEAD: case FUNCTION_CALL: case ASSIGN: - out << from_expr(ns, identifier, it->code) << '\n'; + out << from_expr(ns, identifier, instruction.code) << '\n'; break; case ASSUME: case ASSERT: - if(it->is_assume()) + if(instruction.is_assume()) out << "ASSUME "; else out << "ASSERT "; { - out << from_expr(ns, identifier, it->guard); + out << from_expr(ns, identifier, instruction.guard); - const irep_idt &comment=it->source_location.get_comment(); + const irep_idt &comment=instruction.source_location.get_comment(); if(comment!="") out << " // " << comment; } @@ -126,34 +161,35 @@ std::ostream& goto_programt::output_instruction( { const irept::subt &exception_list= - it->code.find(ID_exception_list).get_sub(); + instruction.code.find(ID_exception_list).get_sub(); for(const auto &ex : exception_list) out << " " << ex.id(); } - if(it->code.operands().size()==1) - out << ": " << from_expr(ns, identifier, it->code.op0()); + if(instruction.code.operands().size()==1) + out << ": " << from_expr(ns, identifier, instruction.code.op0()); out << '\n'; break; case CATCH: - if(!it->targets.empty()) + if(!instruction.targets.empty()) { out << "CATCH-PUSH "; unsigned i=0; const irept::subt &exception_list= - it->code.find(ID_exception_list).get_sub(); - assert(it->targets.size()==exception_list.size()); + instruction.code.find(ID_exception_list).get_sub(); + assert(instruction.targets.size()==exception_list.size()); for(instructiont::targetst::const_iterator - gt_it=it->targets.begin(); - gt_it!=it->targets.end(); + gt_it=instruction.targets.begin(); + gt_it!=instruction.targets.end(); gt_it++, i++) { - if(gt_it!=it->targets.begin()) out << ", "; + if(gt_it!=instruction.targets.begin()) + out << ", "; out << exception_list[i].id() << "->" << (*gt_it)->target_number; } @@ -175,8 +211,8 @@ std::ostream& goto_programt::output_instruction( case START_THREAD: out << "START THREAD "; - if(it->targets.size()==1) - out << it->targets.front()->target_number; + if(instruction.targets.size()==1) + out << instruction.targets.front()->target_number; out << '\n'; break; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 1098582ee2f..e3c7c5528c6 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -28,6 +28,12 @@ class goto_programt:public goto_program_templatet std::ostream &out, instructionst::const_iterator it) const; + std::ostream &output_instruction( + const class namespacet &ns, + const irep_idt &identifier, + std::ostream &out, + const instructiont &instruction) const; + goto_programt() { } // get the variables in decl statements diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index e8ae0f7eeb3..8dd62262e33 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include @@ -240,6 +242,13 @@ class goto_program_templatet return false; } + + std::string to_string() const + { + std::ostringstream instruction_id_builder; + instruction_id_builder << type; + return instruction_id_builder.str(); + } }; typedef std::list instructionst; diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 99cdc36d84c..83eb3434717 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -10,11 +10,14 @@ Author: Peter Schrammel #include #include +#include #include #include #include #include +#include +#include #include "show_goto_functions.h" #include "goto_functions.h" @@ -41,36 +44,15 @@ void show_goto_functions( { case ui_message_handlert::XML_UI: { - //This only prints the list of functions - xmlt xml_functions("functions"); - forall_goto_functions(it, goto_functions) - { - xmlt &xml_function=xml_functions.new_element("function"); - xml_function.set_attribute("name", id2string(it->first)); - } - - std::cout << xml_functions << std::endl; + show_goto_functions_xmlt xml_show_functions(ns); + xml_show_functions(goto_functions, std::cout); } break; case ui_message_handlert::JSON_UI: { - //This only prints the list of functions - json_arrayt json_functions; - forall_goto_functions(it, goto_functions) - { - json_objectt &json_function= - json_functions.push_back(jsont()).make_object(); - json_function["name"]=json_stringt(id2string(it->first)); - json_function["isBodyAvailable"]= - jsont::json_boolean(it->second.body_available()); - bool is_internal=(has_prefix(id2string(it->first), CPROVER_PREFIX) || - it->first==ID__start); - json_function["isInternal"]=jsont::json_boolean(is_internal); - } - json_objectt json_result; - json_result["functions"]=json_functions; - std::cout << ",\n" << json_result; + show_goto_functions_jsont json_show_functions(ns); + json_show_functions(goto_functions, std::cout); } break; diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp new file mode 100644 index 00000000000..1f61e30d2f6 --- /dev/null +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -0,0 +1,160 @@ +/*******************************************************************\ + +Module: Goto Program + +Author: Thomas Kiley + +\*******************************************************************/ + +#include +#include + +#include +#include +#include +#include + +#include + +#include "goto_functions.h" +#include "goto_model.h" +#include "show_goto_functions_json.h" + +/*******************************************************************\ + +Function: show_goto_functions_jsont::show_goto_functions_jsont + + Inputs: + ns - the namespace to use to resolve names with + + Outputs: + + Purpose: For outputing the GOTO program in a readable JSON format. + +\*******************************************************************/ + +show_goto_functions_jsont::show_goto_functions_jsont(const namespacet &ns): + ns(ns) +{} + +/*******************************************************************\ + +Function: show_goto_functions_jsont::convert + + Inputs: + goto_functions - the goto functions that make up the program + + Outputs: + + Purpose: Walks through all of the functions in the program and returns + a JSON object representing all their functions + +\*******************************************************************/ + +json_objectt show_goto_functions_jsont::convert( + const goto_functionst &goto_functions) +{ + json_arrayt json_functions; + const json_irept no_comments_irep_converter(false); + for(const auto &function_entry : goto_functions.function_map) + { + const irep_idt &function_name=function_entry.first; + const goto_functionst::goto_functiont &function=function_entry.second; + + json_objectt &json_function= + json_functions.push_back(jsont()).make_object(); + json_function["name"]=json_stringt(id2string(function_name)); + json_function["isBodyAvailable"]= + jsont::json_boolean(function.body_available()); + bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) || + function_name==ID__start); + json_function["isInternal"]=jsont::json_boolean(is_internal); + + if(function.body_available()) + { + json_arrayt json_instruction_array=json_arrayt(); + + for(const goto_programt::instructiont &instruction : + function.body.instructions) + { + json_objectt instruction_entry=json_objectt(); + + instruction_entry["instructionId"]= + json_stringt(instruction.to_string()); + + if(instruction.code.source_location().is_not_nil()) + { + instruction_entry["sourceLocation"]= + json(instruction.code.source_location()); + } + + std::ostringstream instruction_builder; + function.body.output_instruction( + ns, function_name, instruction_builder, instruction); + + instruction_entry["instruction"]= + json_stringt(instruction_builder.str()); + + if(instruction.code.operands().size()>0) + { + json_arrayt operand_array; + for(const exprt &operand : instruction.code.operands()) + { + json_objectt operand_object; + no_comments_irep_converter.convert_from_irep( + operand, operand_object); + operand_array.push_back(operand_object); + } + instruction_entry["operands"]=operand_array; + } + + if(!instruction.guard.is_true()) + { + json_objectt guard_object; + no_comments_irep_converter.convert_from_irep( + instruction.guard, + guard_object); + + instruction_entry["guard"]=guard_object; + } + + json_instruction_array.push_back(instruction_entry); + } + + json_function["instructions"]=json_instruction_array; + } + } + json_objectt json_result; + json_result["functions"]=json_functions; + return json_result; +} + +/*******************************************************************\ + +Function: show_goto_functions_jsont::operator() + + Inputs: + goto_functions - the goto functions that make up the program + out - the stream to write the object to + append - should a command and newline be appended to the stream + before writing the JSON object. Defaults to true + + Outputs: + + Purpose: Print the json object generated by + show_goto_functions_jsont::show_goto_functions to the provided + stream (e.g. std::cout) + +\*******************************************************************/ + +void show_goto_functions_jsont::operator()( + const goto_functionst &goto_functions, + std::ostream &out, + bool append) +{ + if(append) + { + out << ",\n"; + } + out << convert(goto_functions); +} diff --git a/src/goto-programs/show_goto_functions_json.h b/src/goto-programs/show_goto_functions_json.h new file mode 100644 index 00000000000..b6313247f43 --- /dev/null +++ b/src/goto-programs/show_goto_functions_json.h @@ -0,0 +1,30 @@ +/*******************************************************************\ + +Module: Goto Program + +Author: Thomas Kiley + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H +#define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H + +#include + +class goto_functionst; +class namespacet; + +class show_goto_functions_jsont +{ +public: + explicit show_goto_functions_jsont(const namespacet &ns); + + json_objectt convert(const goto_functionst &goto_functions); + void operator()( + const goto_functionst &goto_functions, std::ostream &out, bool append=true); + +private: + const namespacet &ns; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp new file mode 100644 index 00000000000..a5d1c9d5dd4 --- /dev/null +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -0,0 +1,145 @@ +/*******************************************************************\ + +Module: Goto Program + +Author: Thomas Kiley + +\*******************************************************************/ + +#include +#include + + +#include +#include +#include + +#include + +#include "goto_functions.h" +#include "goto_model.h" + +#include "show_goto_functions_xml.h" + +/*******************************************************************\ + +Function: show_goto_functions_xmlt::show_goto_functions_xmlt + + Inputs: + ns - the namespace to use to resolve names with + + Outputs: + + Purpose: For outputing the GOTO program in a readable xml format. + +\*******************************************************************/ + +show_goto_functions_xmlt::show_goto_functions_xmlt(const namespacet &ns): + ns(ns) +{} + +/*******************************************************************\ + +Function: show_goto_functions_xmlt::convert + + Inputs: + goto_functions - the goto functions that make up the program + + Outputs: + + Purpose: Walks through all of the functions in the program and returns + an xml object representing all their functions. Produces output + like this: + + + + + + + // 34 file main.c line 1 + s = { 'a', 'b', 'c', 0 }; + + + + + + +\*******************************************************************/ + +xmlt show_goto_functions_xmlt::convert( + const goto_functionst &goto_functions) +{ + xmlt xml_functions=xmlt("functions"); + for(const auto &function_entry : goto_functions.function_map) + { + const irep_idt &function_name=function_entry.first; + const goto_functionst::goto_functiont &function=function_entry.second; + + xmlt &xml_function=xml_functions.new_element("function"); + xml_function.set_attribute("name", id2string(function_name)); + xml_function.set_attribute_bool( + "is_body_available", function.body_available()); + bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) || + function_name==ID__start); + xml_function.set_attribute_bool("is_internal", is_internal); + + if(function.body_available()) + { + xmlt &xml_instructions=xml_function.new_element("instructions"); + for(const goto_programt::instructiont &instruction : + function.body.instructions) + { + xmlt &instruction_entry=xml_instructions.new_element("instruction"); + + instruction_entry.set_attribute( + "instruction_id", instruction.to_string()); + + if(instruction.code.source_location().is_not_nil()) + { + instruction_entry.new_element( + xml(instruction.code.source_location())); + } + + std::ostringstream instruction_builder; + function.body.output_instruction( + ns, function_name, instruction_builder, instruction); + + xmlt &instruction_value= + instruction_entry.new_element("instruction_value"); + instruction_value.data=instruction_builder.str(); + instruction_value.elements.clear(); + } + } + } + return xml_functions; +} + +/*******************************************************************\ + +Function: show_goto_functions_xmlt::operator() + + Inputs: + goto_functions - the goto functions that make up the program + out - the stream to write the object to + append - should a command and newline be appended to the stream + before writing the xml object. Defaults to true + + Outputs: + + Purpose: Print the xml object generated by + show_goto_functions_xmlt::show_goto_functions to the provided + stream (e.g. std::cout) + +\*******************************************************************/ + +void show_goto_functions_xmlt::operator()( + const goto_functionst &goto_functions, + std::ostream &out, + bool append) +{ + if(append) + { + out << "\n"; + } + out << convert(goto_functions); +} diff --git a/src/goto-programs/show_goto_functions_xml.h b/src/goto-programs/show_goto_functions_xml.h new file mode 100644 index 00000000000..6e170b5f32d --- /dev/null +++ b/src/goto-programs/show_goto_functions_xml.h @@ -0,0 +1,30 @@ +/*******************************************************************\ + +Module: Goto Program + +Author: Thomas Kiley + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H +#define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H + +#include + +class goto_functionst; +class namespacet; + +class show_goto_functions_xmlt +{ +public: + explicit show_goto_functions_xmlt(const namespacet &ns); + + xmlt convert(const goto_functionst &goto_functions); + void operator()( + const goto_functionst &goto_functions, std::ostream &out, bool append=true); + +private: + const namespacet &ns; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H diff --git a/src/util/Makefile b/src/util/Makefile index 237236f5230..6cc42a18fb8 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -21,7 +21,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.cpp \ irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \ memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ - ssa_expr.cpp json_expr.cpp \ + ssa_expr.cpp json_irep.cpp json_expr.cpp \ string_utils.cpp INCLUDES= -I .. diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp new file mode 100644 index 00000000000..7a3d1a8f2bc --- /dev/null +++ b/src/util/json_irep.cpp @@ -0,0 +1,133 @@ +/*******************************************************************\ + +Module: Util + +Author: Thomas Kiley, thomas.kiley@diffblue.com + +\*******************************************************************/ + +#include "irep.h" +#include "json.h" +#include "json_irep.h" + +/*******************************************************************\ + +Function: json_irept::json_irept + + Inputs: + include_comments - when generating the JSON, should the comments + sub tree be included. + + Outputs: + + Purpose: To convert to JSON from an irep structure by recurssively + generating JSON for the different sub trees. + +\*******************************************************************/ + +json_irept::json_irept(bool include_comments): + include_comments(include_comments) +{} + +/*******************************************************************\ + +Function: json_irept::convert_from_irep + + Inputs: + irep - The irep structure to turn into json + json - The json object to be filled up. + + Outputs: + + Purpose: To convert to JSON from an irep structure by recurssively + generating JSON for the different sub trees. + +\*******************************************************************/ + +void json_irept::convert_from_irep(const irept &irep, jsont &json) const +{ + json_objectt &irep_object=json.make_object(); + if(irep.id()!=ID_nil) + irep_object["id"]=json_stringt(irep.id_string()); + + convert_sub_tree("sub", irep.get_sub(), irep_object); + convert_named_sub_tree("namedSub", irep.get_named_sub(), irep_object); + if(include_comments) + { + convert_named_sub_tree("comment", irep.get_comments(), irep_object); + } +} + +/*******************************************************************\ + +Function: json_irept::convert_sub_tree + + Inputs: + sub_tree_id - the name to give the subtree in the parent object + sub_trees - the list of subtrees to parse + parent - the parent JSON object who should be added to + + Outputs: + + Purpose: To convert to JSON from a list of ireps that are in an + unlabelled subtree. The parent JSON object will get a key + called sub_tree_id and the value shall be an array of JSON + objects generated from each of the sub trees + +\*******************************************************************/ + +void json_irept::convert_sub_tree( + const std::string &sub_tree_id, + const irept::subt &sub_trees, + json_objectt &parent) const +{ + if(sub_trees.size()>0) + { + json_arrayt sub_objects; + for(const irept &sub_tree : sub_trees) + { + json_objectt sub_object; + convert_from_irep(sub_tree, sub_object); + sub_objects.push_back(sub_object); + } + parent[sub_tree_id]=sub_objects; + } +} + +/*******************************************************************\ + +Function: json_irept::convert_named_sub_tree + + Inputs: + sub_tree_id - the name to give the subtree in the parent object + sub_trees - the map of subtrees to parse + parent - the parent JSON object who should be added to + + Outputs: + + Purpose: To convert to JSON from a map of ireps that are in a + named subtree. The parent JSON object will get a key + called sub_tree_id and the value shall be a JSON object + whose keys shall be the name of the sub tree and the value + will be the object generated from the sub tree. + +\*******************************************************************/ + +void json_irept::convert_named_sub_tree( + const std::string &sub_tree_id, + const irept::named_subt &sub_trees, + json_objectt &parent) const +{ + if(sub_trees.size()>0) + { + json_objectt sub_objects; + for(const auto &sub_tree : sub_trees) + { + json_objectt sub_object; + convert_from_irep(sub_tree.second, sub_object); + sub_objects[id2string(sub_tree.first)]=sub_object; + } + parent[sub_tree_id]=sub_objects; + } +} + diff --git a/src/util/json_irep.h b/src/util/json_irep.h new file mode 100644 index 00000000000..749917cb34b --- /dev/null +++ b/src/util/json_irep.h @@ -0,0 +1,36 @@ +/*******************************************************************\ + +Module: Util + +Author: Thomas Kiley, thomas.kiley@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_JSON_IREP_H +#define CPROVER_UTIL_JSON_IREP_H + +#include +class jsont; +class json_objectt; + +class json_irept +{ +public: + explicit json_irept(bool include_comments); + void convert_from_irep(const irept &irep, jsont &json) const; + +private: + void convert_sub_tree( + const std::string &sub_tree_id, + const irept::subt &sub_trees, + json_objectt &parent) const; + + void convert_named_sub_tree( + const std::string &sub_tree_id, + const irept::named_subt &sub_trees, + json_objectt &parent) const; + + bool include_comments; +}; + +#endif // CPROVER_UTIL_JSON_IREP_H