From f5f7b24633703ba30a3688d319827f0d1a2329ec Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 7 Mar 2017 10:23:23 +0000 Subject: [PATCH 01/15] const_hash for irep and dstring --- src/util/dstring.h | 10 ++++++++++ src/util/irep.cpp | 41 +++++++++++++++++++++++++++++++++++++++++ src/util/irep.h | 1 + 3 files changed, 52 insertions(+) diff --git a/src/util/dstring.h b/src/util/dstring.h index 9fdfd1ecddd..ef29e485428 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -123,6 +123,16 @@ class dstringt return out << as_string(); } + friend size_t hash_string(const dstring &s) + { + return s.hash(); + } + + friend size_t const_hash_string(const dstring &s) + { + return hash_string(string_container.get_string(s.no)); + } + // non-standard unsigned get_no() const diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 886f8ce9d7b..0879f2cefc6 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -923,6 +923,47 @@ std::size_t irept::full_hash() const /*******************************************************************\ +Function: irept::const_hash + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::size_t irept::const_hash() const +{ + const irept::subt &sub=get_sub(); + const irept::named_subt &named_sub=get_named_sub(); + const irept::named_subt &comments=get_comments(); + + std::size_t result=const_hash_string(id()); + + forall_irep(it, sub) result=hash_combine(result, it->full_hash()); + + forall_named_irep(it, named_sub) + { + result=hash_combine(result, const_hash_string(it->first)); + result=hash_combine(result, it->second.full_hash()); + } + + forall_named_irep(it, comments) + { + result=hash_combine(result, const_hash_string(it->first)); + result=hash_combine(result, it->second.full_hash()); + } + + result=hash_finalize( + result, + named_sub.size()+sub.size()+comments.size()); + + return result; +} + +/*******************************************************************\ + Function: indent Inputs: diff --git a/src/util/irep.h b/src/util/irep.h index af0b68ac26e..55359787e22 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -252,6 +252,7 @@ class irept std::size_t hash() const; std::size_t full_hash() const; + std::size_t const_hash() const; bool full_eq(const irept &other) const; From 23287ed4e7f8e88cd0991f6f5a9708c91cd17567 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 7 Mar 2017 10:32:20 +0000 Subject: [PATCH 02/15] goto-template const_hash --- src/goto-programs/goto_program_template.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 77161fcb4d8..7f9813de0fd 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include typedef enum { @@ -263,6 +264,11 @@ class goto_program_templatet instruction_id_builder << type; return instruction_id_builder.str(); } + + std::size_t const_hash() const + { + return hash_combine(code.const_hash(),guard.const_hash()); + } }; typedef std::list instructionst; From 456088a83d0972862d8e34a5af987343adb3d491 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 7 Mar 2017 13:14:32 +0000 Subject: [PATCH 03/15] fixed missing and duplicate errors caused on merge --- src/util/dstring.h | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/util/dstring.h b/src/util/dstring.h index ef29e485428..6d47e565557 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -123,16 +123,6 @@ class dstringt return out << as_string(); } - friend size_t hash_string(const dstring &s) - { - return s.hash(); - } - - friend size_t const_hash_string(const dstring &s) - { - return hash_string(string_container.get_string(s.no)); - } - // non-standard unsigned get_no() const @@ -168,6 +158,12 @@ inline size_t hash_string(const dstringt &s) return s.hash(); } +inline size_t const_hash_string(const dstringt &s) +{ + return hash_string(string_container.get_string(s.get_no())); +} + + inline std::ostream &operator<<(std::ostream &out, const dstringt &a) { return a.operator<<(out); From ddc580d1624db8c4c9085e1c67206043f4a54aaf Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 8 Mar 2017 06:19:57 -0800 Subject: [PATCH 04/15] Minor change that exposes some typedefs and internal variables --- src/analyses/dependence_graph.h | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index f82d6f369ec..721bc5fccab 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -69,6 +69,7 @@ struct dep_nodet:public graph_nodet class dep_graph_domaint:public ai_domain_baset { public: + typedef std::set depst; typedef grapht::node_indext node_indext; dep_graph_domaint(): @@ -111,6 +112,16 @@ class dep_graph_domaint:public ai_domain_baset data_deps.clear(); } + const depst& get_control_deps() + { + return control_deps; + } + + const depst& get_data_deps() + { + return data_deps; + } + void make_entry() final { make_top(); @@ -131,7 +142,6 @@ class dep_graph_domaint:public ai_domain_baset tvt has_values; node_indext node_id; - typedef std::set depst; depst control_deps, data_deps; void control_dependencies( From 928865f3ab4b442b211d1b2c0a653b30c602860e Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 9 Mar 2017 08:48:08 -0800 Subject: [PATCH 05/15] Variable instrumentation code. --- src/langapi/language_ui.cpp | 204 ++++++++++++++++++++++++++++++++++++ src/langapi/language_ui.h | 15 +++ src/util/source_location.h | 10 ++ 3 files changed, 229 insertions(+) diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 95b5d104a4f..1885247b122 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -14,6 +14,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include +#include +#include #include "language_ui.h" #include "mode.h" @@ -345,3 +348,204 @@ void language_uit::show_symbol_table_plain( out << '\n' << std::flush; } } + +/*******************************************************************\ + +Function: language_uit::list_extended_symbols + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void language_uit::list_extended_symbols( + const namespacet ns, + const std::string symbol, + const typet type, + std::unique_ptr &p, + std::ostream &out) +{ + if (type.id()==ID_array) + { + const exprt &size_expr=static_cast(type.find(ID_size)); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + for(unsigned int i=0;iget_name(); + list_extended_symbols(ns,buffer.str(),ns.follow(it->type()),p,out); + } + } + else + { + std::string type_str; + p->from_type(type, type_str, ns); + out << "{&" << symbol << "," << type_str << "};" << std::endl; + } +} + + + +/*******************************************************************\ + +Function: language_uit::build_array_from_static_symbol_table + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +unsigned language_uit::build_array_from_static_symbol_table( + std::ostream &address_out, + std::ostream &type_out) +{ + unsigned count = 0; + std::stringstream types; + std::stringstream addresses; + const namespacet ns(symbol_table); + + std::set symbols; + forall_symbols(it, symbol_table.symbols) + symbols.insert(id2string(it->first)); + + for(const std::string &id : symbols) + { + const symbolt &symbol=ns.lookup(id); + languaget *ptr; + if(symbol.mode=="") + ptr=get_default_language(); + else + { + ptr=get_language_from_mode(symbol.mode); + if(ptr == nullptr) + throw "symbol "+id2string(symbol.name)+" has unknown mode"; + } + + std::unique_ptr p(ptr); + std::string type_str; + std::string value_str; + + if(symbol.type.is_not_nil()) + p->from_type(symbol.type, type_str, ns); + + if(symbol.value.is_not_nil()) + p->from_expr(symbol.value, value_str, ns); + + if((symbol.is_static_lifetime) && (!symbol.location.is_built_in())) + { + const typet type = ns.follow(symbol.type); + std::stringstream buffer; + buffer << symbol.base_name; + build_entry(ns,type,p,buffer.str(),addresses,types,count); + } + continue; + } + if(count > 0) + { + address_out << "void* __input_addresses[] = {" + << addresses.str() + << "};"; + type_out << "int __input_type[] = {" + << types.str() + << "};"; + } + else + { + address_out << "static void* __input_addresses = 0;"; + type_out << "static int* __input_type = 0;"; + } + return count; +} + +/*******************************************************************\ + +Function: language_uit::build_entry + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void language_uit::build_entry(const namespacet ns, + const typet type, + std::unique_ptr &p, + const std::string name, + std::ostream &addresses, + std::ostream &types, + unsigned &count) +{ + if (type.id() == ID_array) + { + const exprt &size_expr=static_cast(type.find(ID_size)); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + for(unsigned int i=0;iget_name(); + build_entry(ns,ns.follow(type.subtype()),p, + buffer.str(),addresses,types,count); + } + } + else + { + if(name == "argc") + return; + std::string type_str; + p->from_type(type, type_str, ns); + if(count != 0) + { + types << ","; + addresses << ","; + } + addresses << "&" << name; + static const std::unordered_map type_map + = {{"unsigned int",0},{"signed int",1}, + {"char",2},{"unsigned long int", 3},{"signed long long int",4}, + {"unsigned long long int",5},{"float",6},{"double",7}, + {"signed char",2},{"unsigned char",8},{"signed short int",9}, + {"unsigned short int",10},{"signed long int",11}}; + auto it = type_map.find(type_str); + if(it == type_map.end()) + //used for debugging. + types << type_str; + else + types << it->second; + count += 1; + } +} diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 90c1de3e5cb..92bf2184953 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include +#include class cmdlinet; @@ -40,6 +42,19 @@ class language_uit:public messaget virtual void show_symbol_table(bool brief=false); virtual void show_symbol_table_plain(std::ostream &out, bool brief); virtual void show_symbol_table_xml_ui(bool brief); + virtual unsigned build_array_from_static_symbol_table( + std::ostream &address_out,std::ostream &type_out); + + virtual void build_entry(const namespacet ns, + typet type, + std::unique_ptr &p, + const std::string name, + std::ostream &addresses, + std::ostream &types, + unsigned &count); + + void list_extended_symbols(const namespacet ns,const std::string symbol, + const typet type,std::unique_ptr &p,std::ostream &out); typedef ui_message_handlert::uit uit; diff --git a/src/util/source_location.h b/src/util/source_location.h index b24befcb8c4..2f8881cd469 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -138,6 +138,16 @@ class source_locationt:public irept return get_bool(ID_hide); } + inline bool is_built_in() const + { + std::string file=get_file().c_str(); + std::string built_in=""; + std::string built_in2=""; + bool is_built_in=!file.compare(0,built_in.length(),built_in); + is_built_in|=!file.compare(0,built_in2.length(),built_in2); + return is_built_in; + } + static const source_locationt &nil() { return static_cast(get_nil_irep()); From 611c905c67ad53d63a0be64f13e9534e5f2c7496 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 9 Mar 2017 08:48:57 -0800 Subject: [PATCH 06/15] Tracking progression of coverage. --- src/cbmc/bmc_cover.cpp | 2 +- src/solvers/prop/cover_goals.cpp | 1 + src/solvers/prop/cover_goals.h | 22 ++++++++++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 5fb282778f5..c7af3185a83 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -459,7 +459,7 @@ bool bmc_covert::operator()() for(const auto &test : tests) std::cout << get_test(test.goto_trace) << '\n'; } - + cover_goals.print_goals_stats(std::cout); return false; } diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 699177b25ad..8741ea1ea65 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -50,6 +50,7 @@ void cover_goalst::mark() prop_conv.l_get(g.condition).is_true()) { g.status=goalt::statust::COVERED; + g.seconds=(current_time()-start_time); _number_covered++; // notify observers diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index afb93c9e534..b7840a5df6c 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_PROP_COVER_GOALS_H #include +#include #include "prop_conv.h" @@ -29,6 +30,7 @@ class cover_goalst:public messaget explicit cover_goalst(prop_convt &_prop_conv): prop_conv(_prop_conv) { + start_time=current_time(); } virtual ~cover_goalst(); @@ -41,6 +43,7 @@ class cover_goalst:public messaget struct goalt { literalt condition; + time_periodt seconds; enum class statust { UNKNOWN, COVERED, UNCOVERED, ERROR } status; goalt():status(statust::UNKNOWN) @@ -91,7 +94,26 @@ class cover_goalst:public messaget observers.push_back(&o); } + inline void print_goals_stats(std::ostream &out) + { + out << '\n'; + out <<"**#START" << '\n'; + out << "block-id,hit-count,time(s)" << '\n'; + for(std::list::const_iterator + g_it=goals.begin(); + g_it!=goals.end(); + g_it++) + { + if(g_it->status == goalt::statust::COVERED) + { + out << "0,0," << g_it->seconds << '\n'; + } + } + out <<"#END" << '\n'; + } + protected: + absolute_timet start_time; std::size_t _number_covered; unsigned _iterations; prop_convt &prop_conv; From def160b7c34f69bd0ea8bebaf6ad676b09ee4b37 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Mon, 13 Mar 2017 05:08:09 -0700 Subject: [PATCH 07/15] Simplified and removed C-specific instrumentation code from language_ui.cpp --- src/langapi/language_ui.cpp | 141 ++++++------------------------------ src/langapi/language_ui.h | 22 +++--- 2 files changed, 32 insertions(+), 131 deletions(-) diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 1885247b122..91f7951ad7c 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -349,84 +349,26 @@ void language_uit::show_symbol_table_plain( } } -/*******************************************************************\ - -Function: language_uit::list_extended_symbols - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void language_uit::list_extended_symbols( - const namespacet ns, - const std::string symbol, - const typet type, - std::unique_ptr &p, - std::ostream &out) -{ - if (type.id()==ID_array) - { - const exprt &size_expr=static_cast(type.find(ID_size)); - mp_integer mp_count; - to_integer(size_expr, mp_count); - unsigned count=integer2unsigned(mp_count); - for(unsigned int i=0;iget_name(); - list_extended_symbols(ns,buffer.str(),ns.follow(it->type()),p,out); - } - } - else - { - std::string type_str; - p->from_type(type, type_str, ns); - out << "{&" << symbol << "," << type_str << "};" << std::endl; - } -} - - - /*******************************************************************\ Function: language_uit::build_array_from_static_symbol_table - Inputs: + Inputs: out - maps variable names to types + + Outputs: N/A - Outputs: - - Purpose: + Purpose: builds a list of static variables and maps them to types \*******************************************************************/ -unsigned language_uit::build_array_from_static_symbol_table( - std::ostream &address_out, - std::ostream &type_out) +void language_uit::build_array_from_static_symbol_table( + std::map& out) { - unsigned count = 0; - std::stringstream types; - std::stringstream addresses; const namespacet ns(symbol_table); std::set symbols; forall_symbols(it, symbol_table.symbols) symbols.insert(id2string(it->first)); - + for(const std::string &id : symbols) { const symbolt &symbol=ns.lookup(id); @@ -439,7 +381,7 @@ unsigned language_uit::build_array_from_static_symbol_table( if(ptr == nullptr) throw "symbol "+id2string(symbol.name)+" has unknown mode"; } - + std::unique_ptr p(ptr); std::string type_str; std::string value_str; @@ -449,53 +391,36 @@ unsigned language_uit::build_array_from_static_symbol_table( if(symbol.value.is_not_nil()) p->from_expr(symbol.value, value_str, ns); - + if((symbol.is_static_lifetime) && (!symbol.location.is_built_in())) { const typet type = ns.follow(symbol.type); - std::stringstream buffer; - buffer << symbol.base_name; - build_entry(ns,type,p,buffer.str(),addresses,types,count); + std::stringstream buffer; + buffer << symbol.base_name; + build_entry(ns,type,p,buffer.str(),out); } - continue; - } - if(count > 0) - { - address_out << "void* __input_addresses[] = {" - << addresses.str() - << "};"; - type_out << "int __input_type[] = {" - << types.str() - << "};"; - } - else - { - address_out << "static void* __input_addresses = 0;"; - type_out << "static int* __input_type = 0;"; } - return count; } /*******************************************************************\ Function: language_uit::build_entry - Inputs: + Inputs: - Outputs: + Outputs: N/A - Purpose: + Purpose: Retrieves the names and types of static variable + Recursively handles arrays and structures \*******************************************************************/ void language_uit::build_entry(const namespacet ns, const typet type, std::unique_ptr &p, const std::string name, - std::ostream &addresses, - std::ostream &types, - unsigned &count) + std::map &out) { - if (type.id() == ID_array) + if(type.id() == ID_array) { const exprt &size_expr=static_cast(type.find(ID_size)); mp_integer mp_count; @@ -505,11 +430,10 @@ void language_uit::build_entry(const namespacet ns, { std::stringstream buffer; buffer << name << "[" << i << "]"; - build_entry(ns,ns.follow(type.subtype()),p, - buffer.str(),addresses,types,count); + build_entry(ns,ns.follow(type.subtype()),p,buffer.str(),out); } } - else if (type.id() == ID_struct) + else if(type.id() == ID_struct) { const struct_typet &struct_type=to_struct_type(type); const struct_typet::componentst &components=struct_type.components(); @@ -518,34 +442,13 @@ void language_uit::build_entry(const namespacet ns, { std::stringstream buffer; buffer << name << "." << it->get_name(); - build_entry(ns,ns.follow(type.subtype()),p, - buffer.str(),addresses,types,count); + build_entry(ns,ns.follow(type.subtype()),p,buffer.str(),out); } } else { - if(name == "argc") - return; std::string type_str; p->from_type(type, type_str, ns); - if(count != 0) - { - types << ","; - addresses << ","; - } - addresses << "&" << name; - static const std::unordered_map type_map - = {{"unsigned int",0},{"signed int",1}, - {"char",2},{"unsigned long int", 3},{"signed long long int",4}, - {"unsigned long long int",5},{"float",6},{"double",7}, - {"signed char",2},{"unsigned char",8},{"signed short int",9}, - {"unsigned short int",10},{"signed long int",11}}; - auto it = type_map.find(type_str); - if(it == type_map.end()) - //used for debugging. - types << type_str; - else - types << it->second; - count += 1; + out.insert({name,type_str}); } } diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 92bf2184953..57ca05a2628 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include +#include #include class cmdlinet; @@ -42,19 +44,15 @@ class language_uit:public messaget virtual void show_symbol_table(bool brief=false); virtual void show_symbol_table_plain(std::ostream &out, bool brief); virtual void show_symbol_table_xml_ui(bool brief); - virtual unsigned build_array_from_static_symbol_table( - std::ostream &address_out,std::ostream &type_out); - - virtual void build_entry(const namespacet ns, - typet type, + + virtual void build_array_from_static_symbol_table( + std::map& out); + virtual void build_entry( + const namespacet ns, + const typet type, std::unique_ptr &p, - const std::string name, - std::ostream &addresses, - std::ostream &types, - unsigned &count); - - void list_extended_symbols(const namespacet ns,const std::string symbol, - const typet type,std::unique_ptr &p,std::ostream &out); + const std::string name, + std::map& out); typedef ui_message_handlert::uit uit; From 14fde02f087b29ab250245c168b6f0d23f08359b Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 14 Mar 2017 02:55:56 -0700 Subject: [PATCH 08/15] Printing of coverage goals has been removed from bmc_cover.cpp --- src/cbmc/bmc_cover.cpp | 2 +- src/solvers/prop/cover_goals.h | 18 ------------------ 2 files changed, 1 insertion(+), 19 deletions(-) diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index c7af3185a83..5fb282778f5 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -459,7 +459,7 @@ bool bmc_covert::operator()() for(const auto &test : tests) std::cout << get_test(test.goto_trace) << '\n'; } - cover_goals.print_goals_stats(std::cout); + return false; } diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index b7840a5df6c..7711100a600 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -94,24 +94,6 @@ class cover_goalst:public messaget observers.push_back(&o); } - inline void print_goals_stats(std::ostream &out) - { - out << '\n'; - out <<"**#START" << '\n'; - out << "block-id,hit-count,time(s)" << '\n'; - for(std::list::const_iterator - g_it=goals.begin(); - g_it!=goals.end(); - g_it++) - { - if(g_it->status == goalt::statust::COVERED) - { - out << "0,0," << g_it->seconds << '\n'; - } - } - out <<"#END" << '\n'; - } - protected: absolute_timet start_time; std::size_t _number_covered; From 09565f7418e96bbe80f702970f09e0617a879a21 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 14 Mar 2017 03:35:34 -0700 Subject: [PATCH 09/15] CPPLINT conformance --- src/goto-programs/goto_program_template.h | 2 +- src/langapi/language_ui.cpp | 20 ++++++++++---------- src/langapi/language_ui.h | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 7f9813de0fd..423ff6c1e59 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -267,7 +267,7 @@ class goto_program_templatet std::size_t const_hash() const { - return hash_combine(code.const_hash(),guard.const_hash()); + return hash_combine(code.const_hash(), guard.const_hash()); } }; diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 91f7951ad7c..9b8aee7d59a 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -378,7 +378,7 @@ void language_uit::build_array_from_static_symbol_table( else { ptr=get_language_from_mode(symbol.mode); - if(ptr == nullptr) + if(ptr == nullptr) throw "symbol "+id2string(symbol.name)+" has unknown mode"; } @@ -397,7 +397,7 @@ void language_uit::build_array_from_static_symbol_table( const typet type = ns.follow(symbol.type); std::stringstream buffer; buffer << symbol.base_name; - build_entry(ns,type,p,buffer.str(),out); + build_entry(ns, type, p, buffer.str(), out); } } } @@ -415,10 +415,10 @@ Function: language_uit::build_entry \*******************************************************************/ void language_uit::build_entry(const namespacet ns, - const typet type, + const typet type, std::unique_ptr &p, - const std::string name, - std::map &out) + const std::string name, + std::map &out) { if(type.id() == ID_array) { @@ -426,11 +426,11 @@ void language_uit::build_entry(const namespacet ns, mp_integer mp_count; to_integer(size_expr, mp_count); unsigned count=integer2unsigned(mp_count); - for(unsigned int i=0;iget_name(); - build_entry(ns,ns.follow(type.subtype()),p,buffer.str(),out); + build_entry(ns, ns.follow(type.subtype()), p, buffer.str(), out); } } else { std::string type_str; p->from_type(type, type_str, ns); - out.insert({name,type_str}); + out.insert({name, type_str}); } } diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 57ca05a2628..5e5ce80e2dc 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -44,9 +44,9 @@ class language_uit:public messaget virtual void show_symbol_table(bool brief=false); virtual void show_symbol_table_plain(std::ostream &out, bool brief); virtual void show_symbol_table_xml_ui(bool brief); - + virtual void build_array_from_static_symbol_table( - std::map& out); + std::map& out); virtual void build_entry( const namespacet ns, const typet type, From 7d6191bbe42e6bbd5e09251ab363493e1a2b0f48 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 15 Mar 2017 06:58:01 -0700 Subject: [PATCH 10/15] Removed changes to langapi, minor changes to util/source_location as requested by reviewer --- src/langapi/language_ui.cpp | 107 ----------------------------------- src/langapi/language_ui.h | 13 ----- src/util/source_location.cpp | 23 ++++++++ src/util/source_location.h | 10 +--- 4 files changed, 24 insertions(+), 129 deletions(-) diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 9b8aee7d59a..95b5d104a4f 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -14,9 +14,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include -#include -#include #include "language_ui.h" #include "mode.h" @@ -348,107 +345,3 @@ void language_uit::show_symbol_table_plain( out << '\n' << std::flush; } } - -/*******************************************************************\ - -Function: language_uit::build_array_from_static_symbol_table - - Inputs: out - maps variable names to types - - Outputs: N/A - - Purpose: builds a list of static variables and maps them to types - -\*******************************************************************/ -void language_uit::build_array_from_static_symbol_table( - std::map& out) -{ - const namespacet ns(symbol_table); - - std::set symbols; - forall_symbols(it, symbol_table.symbols) - symbols.insert(id2string(it->first)); - - for(const std::string &id : symbols) - { - const symbolt &symbol=ns.lookup(id); - languaget *ptr; - if(symbol.mode=="") - ptr=get_default_language(); - else - { - ptr=get_language_from_mode(symbol.mode); - if(ptr == nullptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - } - - std::unique_ptr p(ptr); - std::string type_str; - std::string value_str; - - if(symbol.type.is_not_nil()) - p->from_type(symbol.type, type_str, ns); - - if(symbol.value.is_not_nil()) - p->from_expr(symbol.value, value_str, ns); - - if((symbol.is_static_lifetime) && (!symbol.location.is_built_in())) - { - const typet type = ns.follow(symbol.type); - std::stringstream buffer; - buffer << symbol.base_name; - build_entry(ns, type, p, buffer.str(), out); - } - } -} - -/*******************************************************************\ - -Function: language_uit::build_entry - - Inputs: - - Outputs: N/A - - Purpose: Retrieves the names and types of static variable - Recursively handles arrays and structures - -\*******************************************************************/ -void language_uit::build_entry(const namespacet ns, - const typet type, - std::unique_ptr &p, - const std::string name, - std::map &out) -{ - if(type.id() == ID_array) - { - const exprt &size_expr=static_cast(type.find(ID_size)); - mp_integer mp_count; - to_integer(size_expr, mp_count); - unsigned count=integer2unsigned(mp_count); - for(unsigned int i=0; iget_name(); - build_entry(ns, ns.follow(type.subtype()), p, buffer.str(), out); - } - } - else - { - std::string type_str; - p->from_type(type, type_str, ns); - out.insert({name, type_str}); - } -} diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 5e5ce80e2dc..90c1de3e5cb 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -13,10 +13,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include -#include -#include -#include class cmdlinet; @@ -45,15 +41,6 @@ class language_uit:public messaget virtual void show_symbol_table_plain(std::ostream &out, bool brief); virtual void show_symbol_table_xml_ui(bool brief); - virtual void build_array_from_static_symbol_table( - std::map& out); - virtual void build_entry( - const namespacet ns, - const typet type, - std::unique_ptr &p, - const std::string name, - std::map& out); - typedef ui_message_handlert::uit uit; uit get_ui() diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 7583b40b496..33adde7e6c0 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" #include "file_util.h" +#include "prefix.h" /*******************************************************************\ @@ -93,3 +94,25 @@ std::ostream &operator << ( out << source_location.as_string(); return out; } + +/*******************************************************************\ + +Function: is_build_in + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool source_locationt::is_built_in() const +{ + std::string file=get_file().c_str(); + std::string built_in=""; + std::string built_in2=""; + bool is_built_in=has_prefix(file, built_in); + is_built_in|=has_prefix(file, built_in2); + return is_built_in; +} diff --git a/src/util/source_location.h b/src/util/source_location.h index 2f8881cd469..f33f093d874 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -138,15 +138,7 @@ class source_locationt:public irept return get_bool(ID_hide); } - inline bool is_built_in() const - { - std::string file=get_file().c_str(); - std::string built_in=""; - std::string built_in2=""; - bool is_built_in=!file.compare(0,built_in.length(),built_in); - is_built_in|=!file.compare(0,built_in2.length(),built_in2); - return is_built_in; - } + bool is_built_in() const; static const source_locationt &nil() { From d5691f6dbfd9d4d5cb1c081e33e5e8700d6203cc Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 15 Mar 2017 09:07:46 -0700 Subject: [PATCH 11/15] Renamed const_hash to stable_hash for clarity. Stable hash is used when there is a need to identify goto-program hashes across commits (of the target software). This is useful for example in differential analysis where we record hash-tagged information from an analysis and need it relate it to a new analysis (done after some changes to the code). The traditional hash function cannot be used for such use-cases as the ID can change across commits. --- src/goto-programs/goto_program_template.h | 4 ++-- src/util/dstring.h | 2 +- src/util/irep.cpp | 14 ++++++++------ src/util/irep.h | 2 +- 4 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 423ff6c1e59..04acf436238 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -265,9 +265,9 @@ class goto_program_templatet return instruction_id_builder.str(); } - std::size_t const_hash() const + std::size_t stable_hash() const { - return hash_combine(code.const_hash(), guard.const_hash()); + return hash_combine(code.stable_hash(), guard.stable_hash()); } }; diff --git a/src/util/dstring.h b/src/util/dstring.h index 6d47e565557..01ea5de0567 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -158,7 +158,7 @@ inline size_t hash_string(const dstringt &s) return s.hash(); } -inline size_t const_hash_string(const dstringt &s) +inline size_t stable_hash_string(const dstringt &s) { return hash_string(string_container.get_string(s.get_no())); } diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 0879f2cefc6..cb4fd16f03c 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -923,35 +923,37 @@ std::size_t irept::full_hash() const /*******************************************************************\ -Function: irept::const_hash +Function: irept::stable_hash Inputs: Outputs: - Purpose: + Purpose: Stable hash, hashes the actual content of the string. + Can be used to identify hashes across commits + (of the target software) \*******************************************************************/ -std::size_t irept::const_hash() const +std::size_t irept::stable_hash() const { const irept::subt &sub=get_sub(); const irept::named_subt &named_sub=get_named_sub(); const irept::named_subt &comments=get_comments(); - std::size_t result=const_hash_string(id()); + std::size_t result=stable_hash_string(id()); forall_irep(it, sub) result=hash_combine(result, it->full_hash()); forall_named_irep(it, named_sub) { - result=hash_combine(result, const_hash_string(it->first)); + result=hash_combine(result, stable_hash_string(it->first)); result=hash_combine(result, it->second.full_hash()); } forall_named_irep(it, comments) { - result=hash_combine(result, const_hash_string(it->first)); + result=hash_combine(result, stable_hash_string(it->first)); result=hash_combine(result, it->second.full_hash()); } diff --git a/src/util/irep.h b/src/util/irep.h index 55359787e22..cbf3e067995 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -252,7 +252,7 @@ class irept std::size_t hash() const; std::size_t full_hash() const; - std::size_t const_hash() const; + std::size_t stable_hash() const; bool full_eq(const irept &other) const; From 3ceed49723a228b15bfaaceea47bc152a3c4d5c6 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 3 May 2017 03:49:21 -0700 Subject: [PATCH 12/15] Removed 'is_built_in' function. --- src/util/source_location.cpp | 22 ---------------------- src/util/source_location.h | 2 -- 2 files changed, 24 deletions(-) diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 33adde7e6c0..2b0f700d9b7 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -94,25 +94,3 @@ std::ostream &operator << ( out << source_location.as_string(); return out; } - -/*******************************************************************\ - -Function: is_build_in - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool source_locationt::is_built_in() const -{ - std::string file=get_file().c_str(); - std::string built_in=""; - std::string built_in2=""; - bool is_built_in=has_prefix(file, built_in); - is_built_in|=has_prefix(file, built_in2); - return is_built_in; -} diff --git a/src/util/source_location.h b/src/util/source_location.h index f33f093d874..b24befcb8c4 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -138,8 +138,6 @@ class source_locationt:public irept return get_bool(ID_hide); } - bool is_built_in() const; - static const source_locationt &nil() { return static_cast(get_nil_irep()); From d0a5d31854bfa2b4c4dac31636e199d497eae6be Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 3 May 2017 05:52:33 -0700 Subject: [PATCH 13/15] Removed unnecessary include directive. --- src/util/source_location.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 2b0f700d9b7..7583b40b496 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" #include "file_util.h" -#include "prefix.h" /*******************************************************************\ From 3c33f6687a808fe03a4e7014440d689d29f2801e Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 4 May 2017 07:00:51 -0700 Subject: [PATCH 14/15] Removed extra blank line. --- src/util/dstring.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/dstring.h b/src/util/dstring.h index 01ea5de0567..d38ec3c9057 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -163,7 +163,6 @@ inline size_t stable_hash_string(const dstringt &s) return hash_string(string_container.get_string(s.get_no())); } - inline std::ostream &operator<<(std::ostream &out, const dstringt &a) { return a.operator<<(out); From 27da466d3c7dab407d7cc009550ac64bf5c0f7d9 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 4 May 2017 16:07:48 +0100 Subject: [PATCH 15/15] Fix to comment in stable_hash --- src/util/irep.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/irep.cpp b/src/util/irep.cpp index cb4fd16f03c..aceca40fc57 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -929,7 +929,7 @@ Function: irept::stable_hash Outputs: - Purpose: Stable hash, hashes the actual content of the string. + Purpose: Stable hash, hashes the actual content of all contained strings. Can be used to identify hashes across commits (of the target software)