From a1d59d28fc930ac9ec1986dae66c7a98e7d6987a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 15 Aug 2018 09:46:16 +0100 Subject: [PATCH] remove clobber --- .travis.yml | 1 - CMakeLists.txt | 2 - src/CMakeLists.txt | 1 - src/Makefile | 1 - src/clobber/CMakeLists.txt | 31 -- src/clobber/Makefile | 41 --- src/clobber/README.md | 6 - src/clobber/clobber_main.cpp | 28 -- src/clobber/clobber_parse_options.cpp | 413 -------------------------- src/clobber/clobber_parse_options.h | 71 ----- src/clobber/module_dependencies.txt | 10 - 11 files changed, 605 deletions(-) delete mode 100644 src/clobber/CMakeLists.txt delete mode 100644 src/clobber/Makefile delete mode 100644 src/clobber/README.md delete mode 100644 src/clobber/clobber_main.cpp delete mode 100644 src/clobber/clobber_parse_options.cpp delete mode 100644 src/clobber/clobber_parse_options.h delete mode 100644 src/clobber/module_dependencies.txt diff --git a/.travis.yml b/.travis.yml index 61b5957538..6bf16937ca 100644 --- a/.travis.yml +++ b/.travis.yml @@ -352,7 +352,6 @@ install: - make -C src/ansi-c library_check - make -C src/cpp library_check - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 - - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 script: diff --git a/CMakeLists.txt b/CMakeLists.txt index 6256bea09f..0f62152230 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -52,8 +52,6 @@ set_target_properties( big-int cbmc cbmc-lib - clobber - clobber-lib cpp driver goto-analyzer diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8c07a24b12..8e87949943 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -96,7 +96,6 @@ add_subdirectory(pointer-analysis) add_subdirectory(solvers) add_subdirectory(util) add_subdirectory(xmllang) -add_subdirectory(clobber) add_subdirectory(cbmc) add_subdirectory(goto-cc) diff --git a/src/Makefile b/src/Makefile index 7220b6fcb7..8797575357 100644 --- a/src/Makefile +++ b/src/Makefile @@ -3,7 +3,6 @@ DIRS = analyses \ assembler \ big-int \ cbmc \ - clobber \ cpp \ goto-analyzer \ goto-cc \ diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt deleted file mode 100644 index de48db53b9..0000000000 --- a/src/clobber/CMakeLists.txt +++ /dev/null @@ -1,31 +0,0 @@ -# Library -file(GLOB_RECURSE sources "*.cpp" "*.h") -list(REMOVE_ITEM sources - ${CMAKE_CURRENT_SOURCE_DIR}/clobber_main.cpp -) -add_library(clobber-lib ${sources}) - -generic_includes(clobber-lib) - -target_link_libraries(clobber-lib - ansi-c - cpp - linking - big-int - goto-programs - analyses - langapi - xml - assembler - solvers - util - goto-symex - pointer-analysis - goto-instrument-lib -) - -add_if_library(clobber-lib bv_refinement) - -# Executable -add_executable(clobber clobber_main.cpp) -target_link_libraries(clobber clobber-lib) diff --git a/src/clobber/Makefile b/src/clobber/Makefile deleted file mode 100644 index 459cae23cd..0000000000 --- a/src/clobber/Makefile +++ /dev/null @@ -1,41 +0,0 @@ -SRC = clobber_main.cpp \ - clobber_parse_options.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../goto-symex/rewrite_union$(OBJEXT) \ - ../pointer-analysis/dereference$(OBJEXT) \ - ../goto-instrument/dump_c$(OBJEXT) \ - ../goto-instrument/goto_program2code$(OBJEXT) \ - # Empty last line - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = clobber$(EXEEXT) - -all: clobber$(EXEEXT) - -############################################################################### - -clobber$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: clobber-mac-signed - -clobber-mac-signed: cbmc$(EXEEXT) - strip clobber$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) clobber$(EXEEXT) diff --git a/src/clobber/README.md b/src/clobber/README.md deleted file mode 100644 index fef0bd9392..0000000000 --- a/src/clobber/README.md +++ /dev/null @@ -1,6 +0,0 @@ -\ingroup module_hidden -\defgroup clobber clobber - -# Folder clobber - -`clobber\` is a module that is a tool. diff --git a/src/clobber/clobber_main.cpp b/src/clobber/clobber_main.cpp deleted file mode 100644 index c52099efb6..0000000000 --- a/src/clobber/clobber_main.cpp +++ /dev/null @@ -1,28 +0,0 @@ -/*******************************************************************\ - -Module: Symex Main Module - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symex Main Module - -#include "clobber_parse_options.h" - -#include - -#ifdef _MSC_VER -int wmain(int argc, const wchar_t **argv_wide) -{ - auto vec=narrow_argv(argc, argv_wide); - auto narrow=to_c_str_array(std::begin(vec), std::end(vec)); - auto argv=narrow.data(); -#else -int main(int argc, const char **argv) -{ -#endif - clobber_parse_optionst parse_options(argc, argv); - return parse_options.main(); -} diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp deleted file mode 100644 index 2855e5fa7e..0000000000 --- a/src/clobber/clobber_parse_options.cpp +++ /dev/null @@ -1,413 +0,0 @@ -/*******************************************************************\ - -Module: Symex Command Line Options Processing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symex Command Line Options Processing - -#include "clobber_parse_options.h" - -#include -#include -#include - -#include -#include -#include -#include - -#include -#include - -#include -#include -#include -#include -#include -#include -#include - -#include - -#include - -clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv) - : parse_options_baset(CLOBBER_OPTIONS, argc, argv), - language_uit(cmdline, ui_message_handler), - ui_message_handler(cmdline, std::string("CLOBBER ") + CBMC_VERSION) -{ -} - -void clobber_parse_optionst::get_command_line_options(optionst &options) -{ - if(config.set(cmdline)) - { - usage_error(); - exit(1); - } - - if(cmdline.isset("debug-level")) - options.set_option("debug-level", cmdline.get_value("debug-level")); - - if(cmdline.isset("unwindset")) - options.set_option("unwindset", cmdline.get_value("unwindset")); - - // all checks supported by goto_check - PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_value("error-label")); -} - -/// invoke main modules -int clobber_parse_optionst::doit() -{ - if(cmdline.isset("version")) - { - std::cout << CBMC_VERSION << '\n'; - return 0; - } - - register_language(new_ansi_c_language); - register_language(new_cpp_language); - - // - // command line options - // - - optionst options; - get_command_line_options(options); - - eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); - - goto_modelt goto_model; - - try - { - goto_model=initialize_goto_model(cmdline, get_message_handler()); - - - // show it? - if(cmdline.isset("show-loops")) - { - show_loop_ids(get_ui(), goto_model); - return 6; - } - - // show it? - if( - cmdline.isset("show-goto-functions") || - cmdline.isset("list-goto-functions")) - { - show_goto_functions( - goto_model, - get_message_handler(), - ui_message_handler.get_ui(), - cmdline.isset("list-goto-functions")); - return 6; - } - - label_properties(goto_model); - - if(cmdline.isset("show-properties")) - { - show_properties(goto_model, get_message_handler(), get_ui()); - return 0; - } - - set_properties(goto_model.goto_functions); - - // do instrumentation - - const namespacet ns(goto_model.symbol_table); - - std::ofstream out("simulator.c"); - - if(!out) - throw std::string("failed to create file simulator.c"); - - dump_c(goto_model.goto_functions, true, false, false, ns, out); - - status() << "instrumentation complete; compile and execute simulator.c" - << eom; - - return 0; - } - - catch(const std::string &error_msg) - { - error() << error_msg << messaget::eom; - return 8; - } - - catch(const char *error_msg) - { - error() << error_msg << messaget::eom; - return 8; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << messaget::eom; - return 8; - } - - #if 0 - // let's log some more statistics - debug() << "Memory consumption:" << messaget::endl; - memory_info(debug()); - debug() << eom; - #endif -} - -bool clobber_parse_optionst::set_properties(goto_functionst &goto_functions) -{ - if(cmdline.isset("property")) - ::set_properties(goto_functions, cmdline.get_values("property")); - - return false; -} - -bool clobber_parse_optionst::process_goto_program( - const optionst &options, - goto_modelt &goto_model) -{ - { - // do partial inlining - status() << "Partial Inlining" << eom; - goto_partial_inline(goto_model, get_message_handler()); - - // add generic checks - status() << "Generic Property Instrumentation" << eom; - goto_check(options, goto_model); - - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - - // if we aim to cover, replace - // all assertions by false to prevent simplification - - if(cmdline.isset("cover-assertions")) - make_assertions_false(goto_model); - } - - return false; -} - -#if 0 -void clobber_parse_optionst::report_properties( - const path_searcht::property_mapt &property_map) -{ - for(const auto &prop_pair : property_map) - { - if(get_ui()==ui_message_handlert::XML_UI) - { - xmlt xml_result("result"); - xml_result.set_attribute("claim", id2string(prop_pair.first)); - - std::string status_string; - - switch(prop_pair.second.status) - { - case path_searcht::PASS: status_string="OK"; break; - case path_searcht::FAIL: status_string="FAILURE"; break; - case path_searcht::NOT_REACHED: status_string="OK"; break; - } - - xml_result.set_attribute("status", status_string); - - std::cout << xml_result << "\n"; - } - else - { - status() << "[" << prop_pair.first << "] " - << prop_pair.second.description << ": "; - switch(prop_pair.second.status) - { - case path_searcht::PASS: status() << "OK"; break; - case path_searcht::FAIL: status() << "FAILED"; break; - case path_searcht::NOT_REACHED: status() << "OK"; break; - } - status() << eom; - } - - if(cmdline.isset("show-trace") && - prop_pair.second.status==path_searcht::FAIL) - show_counterexample(prop_pair.second.error_trace); - } - - if(!cmdline.isset("property")) - { - status() << eom; - - unsigned failed=0; - - for(const auto &prop_pair : property_map) - if(prop_pair.second.status==path_searcht::FAIL) - failed++; - - status() << "** " << failed - << " of " << property_map.size() << " failed" - << eom; - } -} -#endif - -void clobber_parse_optionst::report_success() -{ - result() << "VERIFICATION SUCCESSFUL" << eom; - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="SUCCESS"; - std::cout << xml; - std::cout << '\n'; - } - break; - - default: - UNREACHABLE; - } -} - -void clobber_parse_optionst::show_counterexample( - const goto_tracet &error_trace) -{ - const namespacet ns(symbol_table); - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - std::cout << "\nCounterexample:\n"; - show_goto_trace(std::cout, ns, error_trace); - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml; - convert(ns, error_trace, xml); - std::cout << xml << '\n'; - } - break; - - default: - UNREACHABLE; - } -} - -void clobber_parse_optionst::report_failure() -{ - result() << "VERIFICATION FAILED" << eom; - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="FAILURE"; - std::cout << xml; - std::cout << '\n'; - } - break; - - default: - UNREACHABLE; - } -} - -/// display command line help -void clobber_parse_optionst::help() -{ - // clang-format off - std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n' - << - "* * Copyright (C) 2014 * *\n" - "* * Daniel Kroening * *\n" - "* * University of Oxford * *\n" - "* * kroening@kroening.com * *\n" - "\n" - "Usage: Purpose:\n" - "\n" - " symex [-?] [-h] [--help] show help\n" - " symex file.c ... source file names\n" - "\n" - "Frontend options:\n" - " -I path set include path (C/C++)\n" - " -D macro define preprocessor macro (C/C++)\n" - " --preprocess stop after preprocessing\n" - " --16, --32, --64 set width of int\n" - " --LP64, --ILP64, --LLP64,\n" - " --ILP32, --LP32 set width of int, long and pointers\n" - " --little-endian allow little-endian word-byte conversions\n" - " --big-endian allow big-endian word-byte conversions\n" - " --unsigned-char make \"char\" unsigned by default\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" - HELP_SHOW_GOTO_FUNCTIONS - " --ppc-macos set MACOS/PPC architecture\n" - " --mm model set memory model (default: sc)\n" - " --arch set architecture (default: " - << configt::this_architecture() << ")\n" - " --os set operating system (default: " - << configt::this_operating_system() << ")\n" - #ifdef _WIN32 - " --gcc use GCC as preprocessor\n" - #endif - " --no-arch don't set up an architecture\n" - " --no-library disable built-in abstract C library\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --round-to-nearest IEEE floating point rounding mode (default)\n" - " --round-to-plus-inf IEEE floating point rounding mode\n" - " --round-to-minus-inf IEEE floating point rounding mode\n" - " --round-to-zero IEEE floating point rounding mode\n" - "\n" - "Program instrumentation options:\n" - HELP_GOTO_CHECK - " --show-properties show the properties\n" - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --error-label label check that label is unreachable\n" - "\n" - "Symex options:\n" - " --function name set main function name\n" - " --property nr only check one specific property\n" - " --depth nr limit search depth\n" - " --context-bound nr limit number of context switches\n" - " --unwind nr unwind nr times\n" - "\n" - "Other options:\n" - " --version show version and exit\n" - " --xml-ui use XML-formatted output\n" - "\n"; - // clang-format on -} diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h deleted file mode 100644 index fd35c90940..0000000000 --- a/src/clobber/clobber_parse_options.h +++ /dev/null @@ -1,71 +0,0 @@ -/*******************************************************************\ - -Module: Command Line Parsing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Command Line Parsing - -#ifndef CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H -#define CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H - -#include -#include - -#include - -#include -#include -#include - -class goto_functionst; -class optionst; - -// clang-format off -#define CLOBBER_OPTIONS \ - "(depth):(context-bound):(unwind):" \ - OPT_GOTO_CHECK \ - OPT_SHOW_GOTO_FUNCTIONS \ - OPT_SHOW_PROPERTIES \ - "(no-assertions)(no-assumptions)" \ - "(error-label):(verbosity):(no-library)" \ - "(version)" \ - "(string-abstraction)" \ - "(show-locs)(show-vcc)(show-trace)" \ - "(property):" \ -// clang-format on - -class clobber_parse_optionst: - public parse_options_baset, - public language_uit -{ -public: - virtual int doit(); - virtual void help(); - - clobber_parse_optionst(int argc, const char **argv); - clobber_parse_optionst( - int argc, - const char **argv, - const std::string &extra_options); - -protected: - ui_message_handlert ui_message_handler; - - void get_command_line_options(optionst &); - - bool process_goto_program( - const optionst &options, - goto_modelt &); - - bool set_properties(goto_functionst &); - - void report_success(); - void report_failure(); - void show_counterexample(const class goto_tracet &); -}; - -#endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H diff --git a/src/clobber/module_dependencies.txt b/src/clobber/module_dependencies.txt deleted file mode 100644 index 3ad32b3903..0000000000 --- a/src/clobber/module_dependencies.txt +++ /dev/null @@ -1,10 +0,0 @@ -analyses -ansi-c -cbmc -clobber -cpp -goto-programs -goto-instrument -java_bytecode # will go away -langapi # should go away -util