From 30cb51c22affc07a212611b5c6420c127933b8d4 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 21 Jan 2019 16:16:34 +0000 Subject: [PATCH 1/2] Add stub for new goto-harness tool This adds a new executable called goto-harness. Right now it doesn't actually do anything, but ultimately its purpose will be to generate "harness" functions for goto-programs - i.e. given some specification, it'll generate a function suitable as a cbmc entry point function that implements that specification. Planned for now are two types of harnesses: One that takes the name of a function with parameters and then generates a function that sets up these parameters and calls the function with them. This is similar to what cbmc does already, however will allow more flexibility in choosing how exactly these parameters will be initialised which was deemed out of scope for cbmc. The other will be able to take a snapshot of a concrete execution of a program, and then start an analysis from that point. --- CMakeLists.txt | 1 + src/CMakeLists.txt | 1 + src/Makefile | 4 ++ src/goto-harness/CMakeLists.txt | 7 +++ src/goto-harness/Makefile | 29 +++++++++++ src/goto-harness/goto_harness_main.cpp | 15 ++++++ .../goto_harness_parse_options.cpp | 51 +++++++++++++++++++ src/goto-harness/goto_harness_parse_options.h | 25 +++++++++ src/goto-harness/module_dependencies.txt | 2 + 9 files changed, 135 insertions(+) create mode 100644 src/goto-harness/CMakeLists.txt create mode 100644 src/goto-harness/Makefile create mode 100644 src/goto-harness/goto_harness_main.cpp create mode 100644 src/goto-harness/goto_harness_parse_options.cpp create mode 100644 src/goto-harness/goto_harness_parse_options.h create mode 100644 src/goto-harness/module_dependencies.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index d427280a67b..9b6dec0910c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -99,6 +99,7 @@ set_target_properties( goto-checker goto-diff goto-diff-lib + goto-harness goto-instrument goto-instrument-lib goto-programs diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1a87562a029..ad059eb0ad8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -103,3 +103,4 @@ add_subdirectory(goto-cc) add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) +add_subdirectory(goto-harness) diff --git a/src/Makefile b/src/Makefile index 4c001a87aff..08311a59d08 100644 --- a/src/Makefile +++ b/src/Makefile @@ -8,6 +8,7 @@ DIRS = analyses \ goto-cc \ goto-checker \ goto-diff \ + goto-harness \ goto-instrument \ goto-programs \ goto-symex \ @@ -27,6 +28,7 @@ all: cbmc.dir \ goto-cc.dir \ goto-diff.dir \ goto-instrument.dir \ + goto-harness.dir \ # Empty last line ############################################################################### @@ -47,6 +49,8 @@ languages: util.dir langapi.dir \ solvers.dir: util.dir +goto-harness.dir: util.dir + goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ goto-symex.dir linking.dir analyses.dir solvers.dir diff --git a/src/goto-harness/CMakeLists.txt b/src/goto-harness/CMakeLists.txt new file mode 100644 index 00000000000..cb04f7355b6 --- /dev/null +++ b/src/goto-harness/CMakeLists.txt @@ -0,0 +1,7 @@ +file(GLOB_RECURSE sources "*.cpp" "*.h") +add_executable(goto-harness ${sources}) +generic_includes(goto-harness) + +target_link_libraries(goto-harness + util +) diff --git a/src/goto-harness/Makefile b/src/goto-harness/Makefile new file mode 100644 index 00000000000..32b95b76b1c --- /dev/null +++ b/src/goto-harness/Makefile @@ -0,0 +1,29 @@ +SRC = \ + goto_harness_main.cpp \ + goto_harness_parse_options.cpp \ + # Empty last line + +OBJ += \ + ../util/util$(LIBEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +CLEANFILES = goto-harness$(EXEEXT) + +include ../config.inc +include ../common + +all: goto-harness$(EXEEXT) + +############################################################################### + +goto-harness$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: goto-harness-mac-signed + +goto-harness-mac-signed: goto-harness$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-harness$(EXEEXT) diff --git a/src/goto-harness/goto_harness_main.cpp b/src/goto-harness/goto_harness_main.cpp new file mode 100644 index 00000000000..285970764df --- /dev/null +++ b/src/goto-harness/goto_harness_main.cpp @@ -0,0 +1,15 @@ +/******************************************************************\ + +Module: goto_harness_main + +Author: Diffblue Ltd. + +\******************************************************************/ + +#include "goto_harness_parse_options.h" + +int main(int argc, const char *argv[]) +{ + auto parse_options = goto_harness_parse_optionst(argc, argv); + return parse_options.main(); +} diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp new file mode 100644 index 00000000000..af74e75bf4d --- /dev/null +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -0,0 +1,51 @@ +/******************************************************************\ + +Module: goto_harness_parse_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#include +#include +#include + +#include +#include + +#include "goto_harness_parse_options.h" + +int goto_harness_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << '\n'; + return CPROVER_EXIT_SUCCESS; + } + + help(); + return CPROVER_EXIT_USAGE_ERROR; +} + +void goto_harness_parse_optionst::help() +{ + std::cout << '\n' + << banner_string("Goto-Harness", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2019") << '\n' + << align_center_with_border("Diffblue Ltd.") << '\n' + << align_center_with_border("info@diffblue.com") + // ^--- No idea if this is the right email address + << '\n' + << '\n' + << "Usage: Purpose:\n" + << '\n' + << " goto-harness [-?] [-h] [--help] show help\n" + << " goto-harness --version show version\n"; +} + +goto_harness_parse_optionst::goto_harness_parse_optionst( + int argc, + const char *argv[]) + : parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv} +{ +} diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h new file mode 100644 index 00000000000..a56440902b7 --- /dev/null +++ b/src/goto-harness/goto_harness_parse_options.h @@ -0,0 +1,25 @@ +/******************************************************************\ + +Module: goto_harness_parse_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H +#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H + +#include + +#define GOTO_HARNESS_OPTIONS "(version)" // end GOTO_HARNESS_OPTIONS + +class goto_harness_parse_optionst : public parse_options_baset +{ +public: + int doit() override; + void help() override; + + goto_harness_parse_optionst(int argc, const char *argv[]); +}; + +#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H diff --git a/src/goto-harness/module_dependencies.txt b/src/goto-harness/module_dependencies.txt new file mode 100644 index 00000000000..55f1017c54b --- /dev/null +++ b/src/goto-harness/module_dependencies.txt @@ -0,0 +1,2 @@ +util +goto-harness From 7a8d3a8b5ac09e00bbefa5648a58dbecd15278a7 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 25 Jan 2019 18:34:02 +0000 Subject: [PATCH 2/2] Add goto-harness regression test This merely shows that the goto-harness executable was built (and indeed executable) --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/goto-harness/CMakeLists.txt | 2 ++ regression/goto-harness/Makefile | 21 +++++++++++++++++++ .../goto-harness-exists/test.desc | 6 ++++++ 5 files changed, 31 insertions(+) create mode 100644 regression/goto-harness/CMakeLists.txt create mode 100644 regression/goto-harness/Makefile create mode 100644 regression/goto-harness/goto-harness-exists/test.desc diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 49f05ef7853..c7508f6d470 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -47,3 +47,4 @@ add_subdirectory(cbmc-cpp) add_subdirectory(goto-cc-goto-analyzer) add_subdirectory(systemc) add_subdirectory(contracts) +add_subdirectory(goto-harness) diff --git a/regression/Makefile b/regression/Makefile index e868aaac56b..621e4a8402d 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -16,6 +16,7 @@ DIRS = cbmc \ test-script \ goto-analyzer-taint \ goto-gcc \ + goto-harness \ goto-cl \ goto-cc-cbmc \ cbmc-cpp \ diff --git a/regression/goto-harness/CMakeLists.txt b/regression/goto-harness/CMakeLists.txt new file mode 100644 index 00000000000..db819a8b0e4 --- /dev/null +++ b/regression/goto-harness/CMakeLists.txt @@ -0,0 +1,2 @@ +add_test_pl_tests( + "$") diff --git a/regression/goto-harness/Makefile b/regression/goto-harness/Makefile new file mode 100644 index 00000000000..b5b5de304a9 --- /dev/null +++ b/regression/goto-harness/Makefile @@ -0,0 +1,21 @@ +default: tests.log + +GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness + +test: + @../test.pl -p -c ${GOTO_HARNESS_EXE} + +tests.log: ../test.pl + @../test.pl -p -c ${GOTO_HARNESS_EXE} + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) {} \; + $(RM) tests.log diff --git a/regression/goto-harness/goto-harness-exists/test.desc b/regression/goto-harness/goto-harness-exists/test.desc new file mode 100644 index 00000000000..fe53e1f97e7 --- /dev/null +++ b/regression/goto-harness/goto-harness-exists/test.desc @@ -0,0 +1,6 @@ +CORE +dummy +--version +^\d+\.\d+ \([^)]+\) +^EXIT=0$ +^SIGNAL=0$