From cee7c16c2afdb2a086c7c684d99d3375e001f163 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 16:11:40 +0000 Subject: [PATCH 01/11] Refactored out output_instruction so could use an instruction This allows the function to be called without using an iterator (useful if using ranged based for loop and more accurate - there is no reason this function shuold be able to, for instance, advance the iterator). --- src/goto-programs/goto_program.cpp | 96 ++++++++++++++++++++---------- src/goto-programs/goto_program.h | 6 ++ 2 files changed, 72 insertions(+), 30 deletions(-) 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 From aa5de8e25eddd87ca242090c0cc62b8c924700ab Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 16:13:29 +0000 Subject: [PATCH 02/11] First pass implementing json output of GOTO program Uses the normal output for showing the instruction. Addes some additional meta data for each instruction. --- src/goto-programs/show_goto_functions.cpp | 33 +++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 99cdc36d84c..35951430157 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -10,6 +10,7 @@ Author: Peter Schrammel #include #include +#include #include #include #include @@ -67,6 +68,38 @@ void show_goto_functions( bool is_internal=(has_prefix(id2string(it->first), CPROVER_PREFIX) || it->first==ID__start); json_function["isInternal"]=jsont::json_boolean(is_internal); + + if(it->second.body_available()) + { + json_arrayt json_instruction_array=json_arrayt(); + + for(const goto_programt::instructiont &instruction : + it->second.body.instructions) + { + json_objectt instruction_entry=json_objectt(); + + std::ostringstream instruction_id_builder; + instruction_id_builder << instruction.type; + + instruction_entry["instructionId"]= + json_stringt(instruction_id_builder.str()); + + instruction_entry["sourceLocation"]= + json(instruction.code.source_location()); + + std::ostringstream instruction_builder; + it->second.body.output_instruction( + ns, it->first, instruction_builder, instruction); + + instruction_entry["instruction"]= + json_stringt(instruction_builder.str()); + + + json_instruction_array.push_back(instruction_entry); + } + + json_function["instructions"] = json_instruction_array; + } } json_objectt json_result; json_result["functions"]=json_functions; From 832cc0cd84a069799f6f7cb93187bc3991ecfd95 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 17:52:27 +0000 Subject: [PATCH 03/11] Moved the JSON printing logic into its own class. Also used a range based for in place of forall_goto_functions. I believe auto is appropriate here as the type would be goto_functionst::function_mapt::value_type which doesn't tell you anything and is harder to read. --- src/goto-programs/Makefile | 1 + src/goto-programs/show_goto_functions.cpp | 51 +-------- .../show_goto_functions_json.cpp | 108 ++++++++++++++++++ src/goto-programs/show_goto_functions_json.h | 26 +++++ 4 files changed, 138 insertions(+), 48 deletions(-) create mode 100644 src/goto-programs/show_goto_functions_json.cpp create mode 100644 src/goto-programs/show_goto_functions_json.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 326e6e8bce3..4f953bfbfe5 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -18,6 +18,7 @@ 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 \ remove_static_init_loops.cpp remove_instanceof.cpp INCLUDES= -I .. diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 35951430157..a6f98e265d5 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -16,6 +16,7 @@ Author: Peter Schrammel #include #include +#include #include "show_goto_functions.h" #include "goto_functions.h" @@ -56,54 +57,8 @@ void show_goto_functions( 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); - - if(it->second.body_available()) - { - json_arrayt json_instruction_array=json_arrayt(); - - for(const goto_programt::instructiont &instruction : - it->second.body.instructions) - { - json_objectt instruction_entry=json_objectt(); - - std::ostringstream instruction_id_builder; - instruction_id_builder << instruction.type; - - instruction_entry["instructionId"]= - json_stringt(instruction_id_builder.str()); - - instruction_entry["sourceLocation"]= - json(instruction.code.source_location()); - - std::ostringstream instruction_builder; - it->second.body.output_instruction( - ns, it->first, instruction_builder, instruction); - - instruction_entry["instruction"]= - json_stringt(instruction_builder.str()); - - - json_instruction_array.push_back(instruction_entry); - } - - json_function["instructions"] = json_instruction_array; - } - } - 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.show_goto_functions(goto_functions); } 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..613dc4ff9a1 --- /dev/null +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -0,0 +1,108 @@ +/*******************************************************************\ + +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::show_goto_functions + + Inputs: + goto_functions - the goto functions that make up the program + + Outputs: + + Purpose: Walks through all of the functions in the program and outputs + JSON + +\*******************************************************************/ + +void show_goto_functions_jsont::show_goto_functions( + const goto_functionst &goto_functions) +{ + json_arrayt json_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; + + 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(); + + std::ostringstream instruction_id_builder; + instruction_id_builder << instruction.type; + + instruction_entry["instructionId"]= + json_stringt(instruction_id_builder.str()); + + 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()); + + json_instruction_array.push_back(instruction_entry); + } + + json_function["instructions"]=json_instruction_array; + } + } + json_objectt json_result; + json_result["functions"]=json_functions; + + // Should this actually be through a message handler + std::cout << ",\n" << json_result; +} 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..296ce0bbe4c --- /dev/null +++ b/src/goto-programs/show_goto_functions_json.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: Goto Program + +Author: Thomas Kiley + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H +#define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H + +class goto_functionst; +class namespacet; + +class show_goto_functions_jsont +{ +public: + explicit show_goto_functions_jsont(const namespacet &ns); + + void show_goto_functions(const goto_functionst &goto_functions); + +private: + const namespacet &ns; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H From 22708a632e625b4bb2b066f9aab2d709a34431b3 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 18:05:48 +0000 Subject: [PATCH 04/11] Only show source location if there is one --- src/goto-programs/show_goto_functions_json.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 613dc4ff9a1..a9361659144 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -84,8 +84,11 @@ void show_goto_functions_jsont::show_goto_functions( instruction_entry["instructionId"]= json_stringt(instruction_id_builder.str()); - instruction_entry["sourceLocation"]= - json(instruction.code.source_location()); + if(instruction.code.source_location().is_not_nil()) + { + instruction_entry["sourceLocation"]= + json(instruction.code.source_location()); + } std::ostringstream instruction_builder; function.body.output_instruction( From 11a4231926ebcb8ecb28112572b1695583be8d9d Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 18 Jan 2017 12:24:14 +0000 Subject: [PATCH 05/11] Made show_goto_functions provide options to directly return the object Can either be used to print to a specific ostream or just return the json object. This mirrors the interface of the output function more accurately. --- src/goto-programs/show_goto_functions.cpp | 2 +- .../show_goto_functions_json.cpp | 40 ++++++++++++++++--- src/goto-programs/show_goto_functions_json.h | 6 ++- 3 files changed, 40 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index a6f98e265d5..0db9f574c6f 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -58,7 +58,7 @@ void show_goto_functions( case ui_message_handlert::JSON_UI: { show_goto_functions_jsont json_show_functions(ns); - json_show_functions.show_goto_functions(goto_functions); + json_show_functions.print_goto_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 index a9361659144..f4a9fde8d2a 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -9,7 +9,6 @@ Author: Thomas Kiley #include #include -#include #include #include #include @@ -46,12 +45,12 @@ Function: show_goto_functions_jsont::show_goto_functions Outputs: - Purpose: Walks through all of the functions in the program and outputs - JSON + Purpose: Walks through all of the functions in the program and returns + a JSON object representing all their functions \*******************************************************************/ -void show_goto_functions_jsont::show_goto_functions( +json_objectt show_goto_functions_jsont::get_goto_functions( const goto_functionst &goto_functions) { json_arrayt json_functions; @@ -105,7 +104,36 @@ void show_goto_functions_jsont::show_goto_functions( } json_objectt json_result; json_result["functions"]=json_functions; + return json_result; +} + +/*******************************************************************\ + +Function: show_goto_functions_jsont::print_goto_functions - // Should this actually be through a message handler - std::cout << ",\n" << json_result; + 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::print_goto_functions( + const goto_functionst &goto_functions, + std::ostream &out, + bool append) +{ + const json_objectt &function_output=get_goto_functions(goto_functions); + if(append) + { + out << ",\n"; + } + out << get_goto_functions(goto_functions); } diff --git a/src/goto-programs/show_goto_functions_json.h b/src/goto-programs/show_goto_functions_json.h index 296ce0bbe4c..70ca6126d27 100644 --- a/src/goto-programs/show_goto_functions_json.h +++ b/src/goto-programs/show_goto_functions_json.h @@ -9,6 +9,8 @@ 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; @@ -17,7 +19,9 @@ class show_goto_functions_jsont public: explicit show_goto_functions_jsont(const namespacet &ns); - void show_goto_functions(const goto_functionst &goto_functions); + json_objectt get_goto_functions(const goto_functionst &goto_functions); + void print_goto_functions( + const goto_functionst &goto_functions, std::ostream &out, bool append=true); private: const namespacet &ns; From c333716aafdb509fa58bd8194bf4a9abaacb9438 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 19 Jan 2017 13:52:19 +0000 Subject: [PATCH 06/11] Basic implementation for the XML class Produces an XML version of the show-goto-functions flag (i.e. when running a tool with the --xml-ui flag). --- src/goto-programs/Makefile | 1 + src/goto-programs/show_goto_functions.cpp | 12 +- .../show_goto_functions_json.cpp | 1 - src/goto-programs/show_goto_functions_xml.cpp | 148 ++++++++++++++++++ src/goto-programs/show_goto_functions_xml.h | 30 ++++ 5 files changed, 182 insertions(+), 10 deletions(-) create mode 100644 src/goto-programs/show_goto_functions_xml.cpp create mode 100644 src/goto-programs/show_goto_functions_xml.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 4f953bfbfe5..d8cb835e4a8 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -19,6 +19,7 @@ SRC = goto_convert.cpp goto_convert_function_call.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/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 0db9f574c6f..2dad1bfd4f6 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -17,6 +17,7 @@ Author: Peter Schrammel #include #include +#include #include "show_goto_functions.h" #include "goto_functions.h" @@ -43,15 +44,8 @@ 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.print_goto_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 index f4a9fde8d2a..0a8214dd2f2 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -130,7 +130,6 @@ void show_goto_functions_jsont::print_goto_functions( std::ostream &out, bool append) { - const json_objectt &function_output=get_goto_functions(goto_functions); if(append) { out << ",\n"; 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..f62ec4bd440 --- /dev/null +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -0,0 +1,148 @@ +/*******************************************************************\ + +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::show_goto_functions + + 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::get_goto_functions( + 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"); + + std::ostringstream instruction_id_builder; + instruction_id_builder << instruction.type; + + instruction_entry.set_attribute( + "instruction_id", instruction_id_builder.str()); + + 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::print_goto_functions + + 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::print_goto_functions( + const goto_functionst &goto_functions, + std::ostream &out, + bool append) +{ + if(append) + { + out << "\n"; + } + out << get_goto_functions(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..98192e8eb0b --- /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 get_goto_functions(const goto_functionst &goto_functions); + void print_goto_functions( + const goto_functionst &goto_functions, std::ostream &out, bool append=true); + +private: + const namespacet &ns; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H From a92d8f87d83d6c5d6c460421317be5ca26bf3d58 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 19 Jan 2017 14:53:26 +0000 Subject: [PATCH 07/11] Added a to_string method to instructions This way if you are not using an ostream you don't have to create one just to get the string. Replaced uses in show_goto_function_json and show_goto_functions_xml Since this isn't performance critical we use std::string as makes the result connect more cleanly to external APIs like the JSON and XML libraries. --- src/goto-programs/goto_program_template.h | 9 +++++++++ src/goto-programs/show_goto_functions_json.cpp | 5 +---- src/goto-programs/show_goto_functions_xml.cpp | 5 +---- 3 files changed, 11 insertions(+), 8 deletions(-) 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_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 0a8214dd2f2..e23d42da7a6 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -77,11 +77,8 @@ json_objectt show_goto_functions_jsont::get_goto_functions( { json_objectt instruction_entry=json_objectt(); - std::ostringstream instruction_id_builder; - instruction_id_builder << instruction.type; - instruction_entry["instructionId"]= - json_stringt(instruction_id_builder.str()); + json_stringt(instruction.to_string()); if(instruction.code.source_location().is_not_nil()) { diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index f62ec4bd440..3e651bcdee9 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -91,11 +91,8 @@ xmlt show_goto_functions_xmlt::get_goto_functions( { xmlt &instruction_entry=xml_instructions.new_element("instruction"); - std::ostringstream instruction_id_builder; - instruction_id_builder << instruction.type; - instruction_entry.set_attribute( - "instruction_id", instruction_id_builder.str()); + "instruction_id", instruction.to_string()); if(instruction.code.source_location().is_not_nil()) { From 8644218a6f5584282d310f7440531db3bf65829b Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 25 Jan 2017 14:14:07 +0000 Subject: [PATCH 08/11] Wrote an irep to JSON converter Use this converter in the show_goto_functions_json to provide more information. --- .../show_goto_functions_json.cpp | 12 ++ src/util/Makefile | 2 +- src/util/json_irep.cpp | 133 ++++++++++++++++++ src/util/json_irep.h | 36 +++++ 4 files changed, 182 insertions(+), 1 deletion(-) create mode 100644 src/util/json_irep.cpp create mode 100644 src/util/json_irep.h diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index e23d42da7a6..f6d125f503f 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -10,6 +10,7 @@ Author: Thomas Kiley #include #include +#include #include #include @@ -54,6 +55,7 @@ json_objectt show_goto_functions_jsont::get_goto_functions( 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; @@ -93,6 +95,16 @@ json_objectt show_goto_functions_jsont::get_goto_functions( instruction_entry["instruction"]= json_stringt(instruction_builder.str()); + 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; + json_instruction_array.push_back(instruction_entry); } 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 From efca2625a90d672e5fc51e14b874ee420e3f64fb Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 25 Jan 2017 14:48:34 +0000 Subject: [PATCH 09/11] Added guard to the output --- src/goto-programs/show_goto_functions_json.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index f6d125f503f..e9568cf9d73 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -105,6 +105,16 @@ json_objectt show_goto_functions_jsont::get_goto_functions( 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); } From 4f54e00b6f19dcaa17bba4b5b1f6ca319d560295 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 25 Jan 2017 14:52:48 +0000 Subject: [PATCH 10/11] Only print the operands if there are some Some instructions have no operands, to keep the JSON legible we omit the empty array. --- src/goto-programs/show_goto_functions_json.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index e9568cf9d73..bf384dca9c2 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -95,16 +95,19 @@ json_objectt show_goto_functions_jsont::get_goto_functions( instruction_entry["instruction"]= json_stringt(instruction_builder.str()); - json_arrayt operand_array; - for(const exprt &operand : instruction.code.operands()) + if(instruction.code.operands().size()>0) { - json_objectt operand_object; - no_comments_irep_converter.convert_from_irep(operand, operand_object); - operand_array.push_back(operand_object); + 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; } - instruction_entry["operands"]=operand_array; - if(!instruction.guard.is_true()) { json_objectt guard_object; From 5550c08597e1bd90e7a8168124c5faa52ffda9cc Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 8 Feb 2017 09:57:36 +0000 Subject: [PATCH 11/11] Made the json and xml show functions class use operator() --- src/goto-programs/show_goto_functions.cpp | 4 ++-- src/goto-programs/show_goto_functions_json.cpp | 10 +++++----- src/goto-programs/show_goto_functions_json.h | 4 ++-- src/goto-programs/show_goto_functions_xml.cpp | 10 +++++----- src/goto-programs/show_goto_functions_xml.h | 4 ++-- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 2dad1bfd4f6..83eb3434717 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -45,14 +45,14 @@ void show_goto_functions( case ui_message_handlert::XML_UI: { show_goto_functions_xmlt xml_show_functions(ns); - xml_show_functions.print_goto_functions(goto_functions, std::cout); + xml_show_functions(goto_functions, std::cout); } break; case ui_message_handlert::JSON_UI: { show_goto_functions_jsont json_show_functions(ns); - json_show_functions.print_goto_functions(goto_functions, std::cout); + 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 index bf384dca9c2..1f61e30d2f6 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -39,7 +39,7 @@ show_goto_functions_jsont::show_goto_functions_jsont(const namespacet &ns): /*******************************************************************\ -Function: show_goto_functions_jsont::show_goto_functions +Function: show_goto_functions_jsont::convert Inputs: goto_functions - the goto functions that make up the program @@ -51,7 +51,7 @@ Function: show_goto_functions_jsont::show_goto_functions \*******************************************************************/ -json_objectt show_goto_functions_jsont::get_goto_functions( +json_objectt show_goto_functions_jsont::convert( const goto_functionst &goto_functions) { json_arrayt json_functions; @@ -131,7 +131,7 @@ json_objectt show_goto_functions_jsont::get_goto_functions( /*******************************************************************\ -Function: show_goto_functions_jsont::print_goto_functions +Function: show_goto_functions_jsont::operator() Inputs: goto_functions - the goto functions that make up the program @@ -147,7 +147,7 @@ Function: show_goto_functions_jsont::print_goto_functions \*******************************************************************/ -void show_goto_functions_jsont::print_goto_functions( +void show_goto_functions_jsont::operator()( const goto_functionst &goto_functions, std::ostream &out, bool append) @@ -156,5 +156,5 @@ void show_goto_functions_jsont::print_goto_functions( { out << ",\n"; } - out << get_goto_functions(goto_functions); + out << convert(goto_functions); } diff --git a/src/goto-programs/show_goto_functions_json.h b/src/goto-programs/show_goto_functions_json.h index 70ca6126d27..b6313247f43 100644 --- a/src/goto-programs/show_goto_functions_json.h +++ b/src/goto-programs/show_goto_functions_json.h @@ -19,8 +19,8 @@ class show_goto_functions_jsont public: explicit show_goto_functions_jsont(const namespacet &ns); - json_objectt get_goto_functions(const goto_functionst &goto_functions); - void print_goto_functions( + json_objectt convert(const goto_functionst &goto_functions); + void operator()( const goto_functionst &goto_functions, std::ostream &out, bool append=true); private: diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index 3e651bcdee9..a5d1c9d5dd4 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -40,7 +40,7 @@ show_goto_functions_xmlt::show_goto_functions_xmlt(const namespacet &ns): /*******************************************************************\ -Function: show_goto_functions_xmlt::show_goto_functions +Function: show_goto_functions_xmlt::convert Inputs: goto_functions - the goto functions that make up the program @@ -66,7 +66,7 @@ Function: show_goto_functions_xmlt::show_goto_functions \*******************************************************************/ -xmlt show_goto_functions_xmlt::get_goto_functions( +xmlt show_goto_functions_xmlt::convert( const goto_functionst &goto_functions) { xmlt xml_functions=xmlt("functions"); @@ -116,7 +116,7 @@ xmlt show_goto_functions_xmlt::get_goto_functions( /*******************************************************************\ -Function: show_goto_functions_xmlt::print_goto_functions +Function: show_goto_functions_xmlt::operator() Inputs: goto_functions - the goto functions that make up the program @@ -132,7 +132,7 @@ Function: show_goto_functions_xmlt::print_goto_functions \*******************************************************************/ -void show_goto_functions_xmlt::print_goto_functions( +void show_goto_functions_xmlt::operator()( const goto_functionst &goto_functions, std::ostream &out, bool append) @@ -141,5 +141,5 @@ void show_goto_functions_xmlt::print_goto_functions( { out << "\n"; } - out << get_goto_functions(goto_functions); + out << convert(goto_functions); } diff --git a/src/goto-programs/show_goto_functions_xml.h b/src/goto-programs/show_goto_functions_xml.h index 98192e8eb0b..6e170b5f32d 100644 --- a/src/goto-programs/show_goto_functions_xml.h +++ b/src/goto-programs/show_goto_functions_xml.h @@ -19,8 +19,8 @@ class show_goto_functions_xmlt public: explicit show_goto_functions_xmlt(const namespacet &ns); - xmlt get_goto_functions(const goto_functionst &goto_functions); - void print_goto_functions( + xmlt convert(const goto_functionst &goto_functions); + void operator()( const goto_functionst &goto_functions, std::ostream &out, bool append=true); private: