From 4e5ac5633cf20fa583e07fd52e41249b9a5198a3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 12:08:11 +0100 Subject: [PATCH 1/3] Revert "vcd" This reverts commit 52f73798d0dd206d087aff087d83269256a9f6ff. --- src/goto-programs/Makefile | 1 - src/goto-programs/vcd_goto_trace.cpp | 153 --------------------------- src/goto-programs/vcd_goto_trace.h | 28 ----- 3 files changed, 182 deletions(-) delete mode 100644 src/goto-programs/vcd_goto_trace.cpp delete mode 100644 src/goto-programs/vcd_goto_trace.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 18a9129e7be..639d1d52d52 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -68,7 +68,6 @@ SRC = add_malloc_may_fail_variable_initializations.cpp \ structured_trace_util.cpp \ system_library_symbols.cpp \ validate_goto_model.cpp \ - vcd_goto_trace.cpp \ wp.cpp \ write_goto_binary.cpp \ xml_expr.cpp \ diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp deleted file mode 100644 index d06308abd23..00000000000 --- a/src/goto-programs/vcd_goto_trace.cpp +++ /dev/null @@ -1,153 +0,0 @@ -/*******************************************************************\ - -Module: Traces of GOTO Programs in VCD (Value Change Dump) Format - -Author: Daniel Kroening - -Date: June 2011 - -\*******************************************************************/ - -/// \file -/// Traces of GOTO Programs in VCD (Value Change Dump) Format - -#include "vcd_goto_trace.h" - -#include - -#include -#include -#include - -std::string as_vcd_binary( - const exprt &expr, - const namespacet &ns) -{ - const typet &type = expr.type(); - - if(expr.id()==ID_constant) - { - if(type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_bv || - type.id()==ID_fixedbv || - type.id()==ID_floatbv || - type.id()==ID_pointer) - return expr.get_string(ID_value); - } - else if(expr.id()==ID_array) - { - std::string result; - - forall_operands(it, expr) - result+=as_vcd_binary(*it, ns); - - return result; - } - else if(expr.id()==ID_struct) - { - std::string result; - - forall_operands(it, expr) - result+=as_vcd_binary(*it, ns); - - return result; - } - else if(expr.id()==ID_union) - { - return as_vcd_binary(to_union_expr(expr).op(), ns); - } - - // build "xxx" - - const auto width = pointer_offset_bits(type, ns); - - if(width.has_value()) - return std::string(numeric_cast_v(*width), 'x'); - else - return ""; -} - -void output_vcd( - const namespacet &ns, - const goto_tracet &goto_trace, - std::ostream &out) -{ - time_t t; - time(&t); - out << "$date\n " << ctime(&t) << "$end" << "\n"; - - // this is pretty arbitrary - out << "$timescale 1 ns $end" << "\n"; - - // we first collect all variables that are assigned - - numberingt n; - - for(const auto &step : goto_trace.steps) - { - if(step.is_assignment()) - { - auto lhs_object=step.get_lhs_object(); - if(lhs_object.has_value()) - { - irep_idt identifier=lhs_object->get_identifier(); - const typet &type=lhs_object->type(); - - const auto number=n.number(identifier); - - const auto width = pointer_offset_bits(type, ns); - - if(width.has_value() && (*width) >= 1) - out << "$var reg " << (*width) << " V" << number << " " << identifier - << " $end" - << "\n"; - } - } - } - - // end of header - out << "$enddefinitions $end" << "\n"; - - unsigned timestamp=0; - - for(const auto &step : goto_trace.steps) - { - if(step.is_assignment()) - { - auto lhs_object = step.get_lhs_object(); - if(lhs_object.has_value()) - { - irep_idt identifier = lhs_object->get_identifier(); - const typet &type = lhs_object->type(); - - out << '#' << timestamp << "\n"; - timestamp++; - - const auto number = n.number(identifier); - - // booleans are special in VCD - if(type.id() == ID_bool) - { - if(step.full_lhs_value.is_true()) - out << "1" - << "V" << number << "\n"; - else if(step.full_lhs_value.is_false()) - out << "0" - << "V" << number << "\n"; - else - out << "x" - << "V" << number << "\n"; - } - else - { - std::string binary = as_vcd_binary(step.full_lhs_value, ns); - - if(!binary.empty()) - out << "b" << binary << " V" << number << " " - << "\n"; - } - } - } - } -} diff --git a/src/goto-programs/vcd_goto_trace.h b/src/goto-programs/vcd_goto_trace.h deleted file mode 100644 index 0f7990b92bd..00000000000 --- a/src/goto-programs/vcd_goto_trace.h +++ /dev/null @@ -1,28 +0,0 @@ -/*******************************************************************\ - -Module: Traces of GOTO Programs in VCD (Value Change Dump) Format - -Author: Daniel Kroening - -Date: June 2011 - -\*******************************************************************/ - -/// \file -/// Traces of GOTO Programs in VCD (Value Change Dump) Format - -#ifndef CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H -#define CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H - -#include - -#include - -#include "goto_trace.h" - -void output_vcd( - const namespacet &ns, - const goto_tracet &goto_trace, - std::ostream &out); - -#endif // CPROVER_GOTO_PROGRAMS_VCD_GOTO_TRACE_H From dcd3b4c7b203406686e20baf2a8ecfe056ad53df Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:26:57 +0100 Subject: [PATCH 2/3] Remove unused preprocessor.h --- src/util/preprocessor.h | 43 ----------------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 src/util/preprocessor.h diff --git a/src/util/preprocessor.h b/src/util/preprocessor.h deleted file mode 100644 index 64919612319..00000000000 --- a/src/util/preprocessor.h +++ /dev/null @@ -1,43 +0,0 @@ -/*******************************************************************\ - -Module: Preprocessing Base Class - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Preprocessing Base Class - -#ifndef CPROVER_UTIL_PREPROCESSOR_H -#define CPROVER_UTIL_PREPROCESSOR_H - -#include -#include - -#include "message.h" - -class preprocessort:public messaget -{ -public: - preprocessort( - std::istream &_in, - std::ostream &_out, - message_handlert &_message_handler, - const std::string &_filename): - messaget(_message_handler), - in(_in), out(_out), - filename(_filename) - { - } - - virtual ~preprocessort() { } - - std::istream ∈ - std::ostream &out; - std::string filename; - - virtual void preprocessor()=0; -}; - -#endif // CPROVER_UTIL_PREPROCESSOR_H From b414951115d21f57a7c01c812434f42ad13d7b89 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 May 2018 12:39:09 +0100 Subject: [PATCH 3/3] Remove EBMC-specific find_macros and get_module These are not of general use and cannot be tested in this repository. --- src/util/Makefile | 2 - src/util/find_macros.cpp | 64 ------------------- src/util/find_macros.h | 27 -------- src/util/get_module.cpp | 130 --------------------------------------- src/util/get_module.h | 26 -------- src/util/irep_ids.def | 1 - 6 files changed, 250 deletions(-) delete mode 100644 src/util/find_macros.cpp delete mode 100644 src/util/find_macros.h delete mode 100644 src/util/get_module.cpp delete mode 100644 src/util/get_module.h diff --git a/src/util/Makefile b/src/util/Makefile index d50c5b54322..29bdb6c7897 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -17,7 +17,6 @@ SRC = allocate_objects.cpp \ expr_util.cpp \ exception_utils.cpp \ file_util.cpp \ - find_macros.cpp \ find_symbols.cpp \ fixedbv.cpp \ format_constant.cpp \ @@ -26,7 +25,6 @@ SRC = allocate_objects.cpp \ format_type.cpp \ fresh_symbol.cpp \ get_base_name.cpp \ - get_module.cpp \ identifier.cpp \ ieee_float.cpp \ interval_union.cpp \ diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp deleted file mode 100644 index c78f856eb7c..00000000000 --- a/src/util/find_macros.cpp +++ /dev/null @@ -1,64 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "find_macros.h" - -#include - -#include "namespace.h" -#include "std_expr.h" -#include "symbol.h" - -void find_macros( - const exprt &src, - const namespacet &ns, - find_macros_sett &dest) -{ - std::stack stack; - - // use stack, these may be nested deeply - stack.push(&src); - - while(!stack.empty()) - { - const exprt &e=*stack.top(); - stack.pop(); - - if(e.id() == ID_symbol) - { - const irep_idt &identifier = to_symbol_expr(e).get_identifier(); - - const symbolt &symbol = ns.lookup(identifier); - - if(symbol.is_macro) - { - // inserted? - if(dest.insert(identifier).second) - stack.push(&symbol.value); - } - } - else if(e.id() == ID_next_symbol) - { - const irep_idt &identifier=e.get(ID_identifier); - - const symbolt &symbol=ns.lookup(identifier); - - if(symbol.is_macro) - { - // inserted? - if(dest.insert(identifier).second) - stack.push(&symbol.value); - } - } - else - { - forall_operands(it, e) - stack.push(&(*it)); - } - } -} diff --git a/src/util/find_macros.h b/src/util/find_macros.h deleted file mode 100644 index 654f72b0c21..00000000000 --- a/src/util/find_macros.h +++ /dev/null @@ -1,27 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_UTIL_FIND_MACROS_H -#define CPROVER_UTIL_FIND_MACROS_H - -#include - -#include "irep.h" - -class exprt; -class namespacet; - -typedef std::unordered_set find_macros_sett; - -void find_macros( - const exprt &src, - const namespacet &ns, - find_macros_sett &dest); - -#endif // CPROVER_UTIL_FIND_MACROS_H diff --git a/src/util/get_module.cpp b/src/util/get_module.cpp deleted file mode 100644 index f3df545efeb..00000000000 --- a/src/util/get_module.cpp +++ /dev/null @@ -1,130 +0,0 @@ -/*******************************************************************\ - -Module: Find module symbol using name - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Find module symbol using name - -#include "get_module.h" - -#include -#include - -#include "message.h" -#include "symbol_table.h" - -typedef std::list symbolptr_listt; - -#define forall_symbolptr_list(it, list) \ - for(symbolptr_listt::const_iterator it=(list).begin(); \ - it!=(list).end(); ++it) - -#define Forall_symbolptr_list(it, list) \ - for(symbolptr_listt::iterator it=(list).begin(); \ - it!=(list).end(); ++it) - -const symbolt &get_module_by_name( - const symbol_tablet &symbol_table, - const std::string &module, - message_handlert &message_handler) -{ - symbolptr_listt symbolptr_list; - messaget message(message_handler); - - forall_symbol_base_map(it, symbol_table.symbol_base_map, module) - { - symbol_tablet::symbolst::const_iterator it2= - symbol_table.symbols.find(it->second); - - if(it2==symbol_table.symbols.end()) - continue; - - const symbolt &s=it2->second; - - if(s.is_type || s.type.id()!=ID_module) - continue; - - symbolptr_list.push_back(&s); - } - - if(symbolptr_list.empty()) - { - message.error() << "module '" << module << "' not found" << messaget::eom; - throw 0; - } - else if(symbolptr_list.size()>=2) - { - message.error() << "module '" << module << "' does not uniquely resolve:\n"; - - forall_symbolptr_list(it, symbolptr_list) - message.error() << " " << (*it)->name << '\n'; - - message.error() << messaget::eom; - throw 0; - } - - // symbolptr_list has exactly one element - - return *symbolptr_list.front(); -} - -const symbolt &get_module( - const symbol_tablet &symbol_table, - const std::string &module, - message_handlert &message_handler) -{ - if(!module.empty()) - return get_module_by_name(symbol_table, module, message_handler); - - symbolptr_listt symbolptr_list, main_symbolptr_list; - messaget message(message_handler); - - for(const auto &symbol_pair : symbol_table.symbols) - { - const symbolt &s = symbol_pair.second; - - if(s.type.id()!=ID_module) - continue; - - // this is our default - if(s.base_name==ID_main) - return get_module_by_name(symbol_table, "main", message_handler); - - symbolptr_list.push_back(&s); - } - - if(symbolptr_list.empty()) - { - message.error() << "no module found" << messaget::eom; - throw 0; - } - else if(symbolptr_list.size()>=2) - { - // sorted alphabetically - std::set modules; - - forall_symbolptr_list(it, symbolptr_list) - modules.insert(id2string((*it)->pretty_name)); - - message.error() << "multiple modules found, please select one:\n"; - - for(const auto &s_it : modules) - message.error() << " " << s_it << '\n'; - - message.error() << messaget::eom; - throw 0; - } - - // symbolptr_list has exactly one element - - const symbolt &symbol=*symbolptr_list.front(); - - message.status() << "Using module '" << symbol.pretty_name << "'" - << messaget::eom; - - return symbol; -} diff --git a/src/util/get_module.h b/src/util/get_module.h deleted file mode 100644 index 73eda37dfbb..00000000000 --- a/src/util/get_module.h +++ /dev/null @@ -1,26 +0,0 @@ -/*******************************************************************\ - -Module: Find module symbol using name - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Find module symbol using name - -#ifndef CPROVER_UTIL_GET_MODULE_H -#define CPROVER_UTIL_GET_MODULE_H - -#include - -class symbol_tablet; -class message_handlert; -class symbolt; - -const symbolt &get_module( - const symbol_tablet &symbol_table, - const std::string &module, - message_handlert &message_handler); - -#endif // CPROVER_UTIL_GET_MODULE_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b7748d7c67c..746501c3a19 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -145,7 +145,6 @@ IREP_ID_ONE(merged_type) IREP_ID_ONE(range) IREP_ID_ONE(from) IREP_ID_ONE(to) -IREP_ID_ONE(module) IREP_ID_ONE(parameter) IREP_ID_ONE(component_name) IREP_ID_ONE(component_number)