Add function harness generator and generator factory
This adds a framework for adding various new harness generator types and adds tests. It also adds a harness generator that calls a given goto function. Co-authored-by: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com> Co-authored-by: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
This commit is contained in:
Hannes Steffenhagen
Fotis Koutoulakis
parent
6a865c59f0
commit
7b55287072
|
|
@ -102,6 +102,8 @@ src/goto-cc/goto-cc
|
|||
src/goto-cc/goto-gcc
|
||||
src/goto-cc/goto-cc.exe
|
||||
src/goto-cc/goto-cl.exe
|
||||
src/goto-harness/goto-harness
|
||||
src/goto-harness/goto-harness.exe
|
||||
src/goto-instrument/goto-instrument
|
||||
src/goto-instrument/goto-instrument.exe
|
||||
src/solvers/smt2_solver
|
||||
|
|
|
|||
|
|
@ -1,2 +1,12 @@
|
|||
if(WIN32)
|
||||
set(is_windows true)
|
||||
else()
|
||||
set(is_windows false)
|
||||
endif()
|
||||
|
||||
add_test_pl_tests(
|
||||
"$<TARGET_FILE:goto-harness>")
|
||||
"../chain.sh \
|
||||
$<TARGET_FILE:goto-cc> \
|
||||
$<TARGET_FILE:goto-harness> \
|
||||
$<TARGET_FILE:cbmc> \
|
||||
${is_windows}")
|
||||
|
|
|
|||
|
|
@ -1,12 +1,24 @@
|
|||
default: tests.log
|
||||
|
||||
include ../../src/config.inc
|
||||
include ../../src/common
|
||||
|
||||
GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
|
||||
CBMC_EXE=../../../src/cbmc/cbmc
|
||||
|
||||
ifeq ($(BUILD_ENV_),MSVC)
|
||||
GOTO_CC_EXE=../../../src/goto-cc/goto-cl
|
||||
is_windows=true
|
||||
else
|
||||
GOTO_CC_EXE=../../../src/goto-cc/goto-cc
|
||||
is_windows=false
|
||||
endif
|
||||
|
||||
test:
|
||||
@../test.pl -p -c ${GOTO_HARNESS_EXE}
|
||||
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
|
||||
|
||||
tests.log: ../test.pl
|
||||
@../test.pl -p -c ${GOTO_HARNESS_EXE}
|
||||
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
|
||||
|
||||
show:
|
||||
@for dir in *; do \
|
||||
|
|
|
|||
|
|
@ -0,0 +1,27 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -e
|
||||
|
||||
goto_cc=$1
|
||||
goto_harness=$2
|
||||
cbmc=$3
|
||||
is_windows=$4
|
||||
entry_point='generated_entry_function'
|
||||
|
||||
name=${*:$#}
|
||||
name=${name%.c}
|
||||
args=${*:5:$#-5}
|
||||
|
||||
if [[ "${is_windows}" == "true" ]]; then
|
||||
$goto_cc "${name}.c"
|
||||
mv "${name}.exe" "${name}.gb"
|
||||
else
|
||||
$goto_cc -o "${name}.gb" "${name}.c"
|
||||
fi
|
||||
|
||||
if [ -e "${name}-mod.gb" ] ; then
|
||||
rm -f "${name}-mod.gb"
|
||||
fi
|
||||
|
||||
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
|
||||
$cbmc --function $entry_point "${name}-mod.gb"
|
||||
|
|
@ -0,0 +1,7 @@
|
|||
#include <assert.h>
|
||||
|
||||
int function_to_test(int some_argument)
|
||||
{
|
||||
assert(some_argument == 0);
|
||||
return some_argument;
|
||||
}
|
||||
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
main.c
|
||||
--harness-type call-function --function function_to_test
|
||||
^\[function_to_test.assertion.1\] line \d+ assertion some_argument == 0: FAILURE$
|
||||
^VERIFICATION FAILED$
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
CORE
|
||||
dummy
|
||||
--version
|
||||
^\d+\.\d+ \([^)]+\)
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
@ -49,7 +49,7 @@ languages: util.dir langapi.dir \
|
|||
|
||||
solvers.dir: util.dir
|
||||
|
||||
goto-harness.dir: util.dir
|
||||
goto-harness.dir: util.dir goto-programs.dir
|
||||
|
||||
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
|
||||
goto-symex.dir linking.dir analyses.dir solvers.dir
|
||||
|
|
|
|||
|
|
@ -3,5 +3,6 @@ add_executable(goto-harness ${sources})
|
|||
generic_includes(goto-harness)
|
||||
|
||||
target_link_libraries(goto-harness
|
||||
util
|
||||
util
|
||||
goto-programs
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,10 +1,17 @@
|
|||
SRC = \
|
||||
function_call_harness_generator.cpp \
|
||||
goto_harness_generator.cpp \
|
||||
goto_harness_generator_factory.cpp \
|
||||
goto_harness_main.cpp \
|
||||
goto_harness_parse_options.cpp \
|
||||
# Empty last line
|
||||
|
||||
OBJ += \
|
||||
../util/util$(LIBEXT) \
|
||||
../goto-programs/goto-programs$(LIBEXT) \
|
||||
../big-int/big-int$(LIBEXT) \
|
||||
../langapi/langapi$(LIBEXT) \
|
||||
../linking/linking$(LIBEXT) \
|
||||
# Empty last line
|
||||
|
||||
INCLUDES= -I ..
|
||||
|
|
|
|||
|
|
@ -0,0 +1,134 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: harness generator for functions
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#include "function_call_harness_generator.h"
|
||||
|
||||
#include <goto-programs/goto_convert.h>
|
||||
#include <goto-programs/goto_model.h>
|
||||
#include <util/allocate_objects.h>
|
||||
#include <util/exception_utils.h>
|
||||
#include <util/std_code.h>
|
||||
#include <util/std_expr.h>
|
||||
#include <util/ui_message.h>
|
||||
|
||||
#include "function_harness_generator_options.h"
|
||||
#include "goto_harness_parse_options.h"
|
||||
|
||||
struct function_call_harness_generatort::implt
|
||||
{
|
||||
ui_message_handlert *message_handler;
|
||||
irep_idt function;
|
||||
};
|
||||
|
||||
function_call_harness_generatort::function_call_harness_generatort(
|
||||
ui_message_handlert &message_handler)
|
||||
: goto_harness_generatort{}, p_impl(util_make_unique<implt>())
|
||||
{
|
||||
p_impl->message_handler = &message_handler;
|
||||
}
|
||||
|
||||
function_call_harness_generatort::~function_call_harness_generatort() = default;
|
||||
|
||||
void function_call_harness_generatort::handle_option(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values)
|
||||
{
|
||||
if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
|
||||
{
|
||||
p_impl->function = require_exactly_one_value(option, values);
|
||||
}
|
||||
else
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"function harness generator cannot handle this option", "--" + option};
|
||||
}
|
||||
}
|
||||
|
||||
void function_call_harness_generatort::generate(
|
||||
goto_modelt &goto_model,
|
||||
const irep_idt &harness_function_name)
|
||||
{
|
||||
auto const &function = p_impl->function;
|
||||
auto &symbol_table = goto_model.symbol_table;
|
||||
auto function_found = symbol_table.lookup(function);
|
||||
auto harness_function_found = symbol_table.lookup(harness_function_name);
|
||||
|
||||
if(function_found == nullptr)
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"function that should be harnessed is not found " + id2string(function),
|
||||
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
|
||||
}
|
||||
|
||||
if(harness_function_found != nullptr)
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"harness function already in the symbol table " +
|
||||
id2string(harness_function_name),
|
||||
"--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
|
||||
}
|
||||
|
||||
auto allocate_objects = allocate_objectst{function_found->mode,
|
||||
function_found->location,
|
||||
"__goto_harness",
|
||||
symbol_table};
|
||||
|
||||
// create body for the function
|
||||
code_blockt function_body{};
|
||||
|
||||
const auto &function_type = to_code_type(function_found->type);
|
||||
const auto ¶meters = function_type.parameters();
|
||||
|
||||
code_function_callt::operandst arguments{};
|
||||
arguments.reserve(parameters.size());
|
||||
|
||||
for(const auto ¶meter : parameters)
|
||||
{
|
||||
auto argument = allocate_objects.allocate_automatic_local_object(
|
||||
parameter.type(), parameter.get_base_name());
|
||||
arguments.push_back(std::move(argument));
|
||||
}
|
||||
|
||||
code_function_callt function_call{function_found->symbol_expr(),
|
||||
std::move(arguments)};
|
||||
function_call.add_source_location() = function_found->location;
|
||||
|
||||
function_body.add(std::move(function_call));
|
||||
|
||||
// create the function symbol
|
||||
symbolt harness_function_symbol{};
|
||||
harness_function_symbol.name = harness_function_symbol.base_name =
|
||||
harness_function_symbol.pretty_name = harness_function_name;
|
||||
|
||||
harness_function_symbol.is_lvalue = true;
|
||||
harness_function_symbol.mode = function_found->mode;
|
||||
harness_function_symbol.type = code_typet{{}, empty_typet{}};
|
||||
harness_function_symbol.value = function_body;
|
||||
|
||||
symbol_table.insert(harness_function_symbol);
|
||||
|
||||
goto_model.goto_functions.function_map[harness_function_name].type =
|
||||
to_code_type(harness_function_symbol.type);
|
||||
auto &body =
|
||||
goto_model.goto_functions.function_map[harness_function_name].body;
|
||||
goto_convert(
|
||||
static_cast<const codet &>(harness_function_symbol.value),
|
||||
goto_model.symbol_table,
|
||||
body,
|
||||
*p_impl->message_handler,
|
||||
function_found->mode);
|
||||
body.add(goto_programt::make_end_function());
|
||||
}
|
||||
|
||||
void function_call_harness_generatort::validate_options()
|
||||
{
|
||||
if(p_impl->function == ID_empty)
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"required parameter entry function not set",
|
||||
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
|
||||
}
|
||||
|
|
@ -0,0 +1,43 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: harness generator for functions
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#ifndef CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
|
||||
#define CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
|
||||
|
||||
#include <list>
|
||||
#include <memory>
|
||||
#include <string>
|
||||
|
||||
#include <util/ui_message.h>
|
||||
|
||||
#include "goto_harness_generator.h"
|
||||
|
||||
/// Function harness generator that for a specified goto-function
|
||||
/// generates a harness that sets up its arguments and calls it.
|
||||
class function_call_harness_generatort : public goto_harness_generatort
|
||||
{
|
||||
public:
|
||||
explicit function_call_harness_generatort(
|
||||
ui_message_handlert &message_handler);
|
||||
~function_call_harness_generatort() override;
|
||||
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
|
||||
override;
|
||||
|
||||
protected:
|
||||
void handle_option(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values) override;
|
||||
|
||||
void validate_options() override;
|
||||
|
||||
private:
|
||||
struct implt;
|
||||
std::unique_ptr<implt> p_impl;
|
||||
};
|
||||
|
||||
#endif // CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: functions_harness_generator_options
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
|
||||
#define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
|
||||
|
||||
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
|
||||
#define FUNCTION_HARNESS_GENERATOR_OPTIONS \
|
||||
"(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"
|
||||
// FUNCTION_HARNESS_GENERATOR_OPTIONS
|
||||
|
||||
// clang-format off
|
||||
#define FUNCTION_HARNESS_GENERATOR_HELP \
|
||||
"function harness generator (--harness-type call-function)\n\n" \
|
||||
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \
|
||||
" the function the harness should call\n" \
|
||||
// FUNCTION_HARNESS_GENERATOR_HELP
|
||||
// clang-format on
|
||||
|
||||
#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
|
||||
|
|
@ -0,0 +1,35 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: goto_harness_generator
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#include "goto_harness_generator.h"
|
||||
|
||||
#include <list>
|
||||
#include <string>
|
||||
|
||||
#include <util/exception_utils.h>
|
||||
#include <util/invariant.h>
|
||||
|
||||
std::string goto_harness_generatort::require_exactly_one_value(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values)
|
||||
{
|
||||
if(values.size() != 1)
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{"expected exactly one value",
|
||||
"--" + option};
|
||||
}
|
||||
|
||||
return values.front();
|
||||
}
|
||||
|
||||
void goto_harness_generatort::assert_no_values(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values)
|
||||
{
|
||||
PRECONDITION_WITH_DIAGNOSTICS(values.empty(), option);
|
||||
}
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: goto_harness_generator
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
|
||||
#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
|
||||
|
||||
#include <list>
|
||||
#include <string>
|
||||
|
||||
#include <util/irep.h>
|
||||
|
||||
class goto_modelt;
|
||||
|
||||
class goto_harness_generatort
|
||||
{
|
||||
public:
|
||||
/// Generate a harness according to the set options
|
||||
virtual void
|
||||
generate(goto_modelt &goto_model, const irep_idt &harness_function_name) = 0;
|
||||
|
||||
virtual ~goto_harness_generatort() = default;
|
||||
friend class goto_harness_generator_factoryt;
|
||||
|
||||
protected:
|
||||
/// Handle a command line argument. Should throw an exception if the option
|
||||
/// doesn't apply to this generator. Should only set options rather than
|
||||
/// immediately performing work
|
||||
virtual void handle_option(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values) = 0;
|
||||
|
||||
/// Check if options are in a sane state, throw otherwise
|
||||
virtual void validate_options() = 0;
|
||||
|
||||
/// Returns the only value of a single element list,
|
||||
/// throws an exception if not passed a single element list
|
||||
static std::string require_exactly_one_value(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values);
|
||||
|
||||
/// Asserts that the list of values to an option passed is empty
|
||||
static void assert_no_values(
|
||||
const std::string &option,
|
||||
const std::list<std::string> &values);
|
||||
};
|
||||
|
||||
#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
|
||||
|
|
@ -0,0 +1,64 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: goto_harness_generator_factory
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#include "goto_harness_generator_factory.h"
|
||||
|
||||
#include <util/exception_utils.h>
|
||||
#include <util/invariant.h>
|
||||
#include <util/make_unique.h>
|
||||
#include <util/string_utils.h>
|
||||
|
||||
#include <algorithm>
|
||||
#include <functional>
|
||||
#include <iterator>
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
|
||||
void goto_harness_generator_factoryt::register_generator(
|
||||
std::string generator_name,
|
||||
build_generatort build_generator)
|
||||
{
|
||||
PRECONDITION(generators.find(generator_name) == generators.end());
|
||||
auto res = generators.insert({generator_name, build_generator});
|
||||
CHECK_RETURN(res.second);
|
||||
}
|
||||
|
||||
std::unique_ptr<goto_harness_generatort>
|
||||
goto_harness_generator_factoryt::factory(
|
||||
const std::string &generator_name,
|
||||
const generator_optionst &generator_options)
|
||||
{
|
||||
auto it = generators.find(generator_name);
|
||||
|
||||
if(it != generators.end())
|
||||
{
|
||||
auto generator = it->second();
|
||||
for(const auto &option : generator_options)
|
||||
{
|
||||
generator->handle_option(option.first, option.second);
|
||||
}
|
||||
generator->validate_options();
|
||||
|
||||
return generator;
|
||||
}
|
||||
else
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont(
|
||||
"unknown generator type",
|
||||
"--" GOTO_HARNESS_GENERATOR_TYPE_OPT,
|
||||
join_strings(
|
||||
std::ostringstream(),
|
||||
generators.begin(),
|
||||
generators.end(),
|
||||
", ",
|
||||
[](const std::pair<std::string, build_generatort> &value) {
|
||||
return value.first;
|
||||
})
|
||||
.str());
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,57 @@
|
|||
/******************************************************************\
|
||||
|
||||
Module: goto_harness_generator_factory
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\******************************************************************/
|
||||
|
||||
#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
|
||||
#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
|
||||
|
||||
#include <functional>
|
||||
#include <map>
|
||||
#include <memory>
|
||||
#include <string>
|
||||
|
||||
#include "goto_harness_generator.h"
|
||||
|
||||
#define GOTO_HARNESS_GENERATOR_TYPE_OPT "harness-type"
|
||||
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "harness-function-name"
|
||||
|
||||
// clang-format off
|
||||
#define GOTO_HARNESS_FACTORY_OPTIONS \
|
||||
"(" GOTO_HARNESS_GENERATOR_TYPE_OPT "):" \
|
||||
"(" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "):" \
|
||||
// end GOTO_HARNESS_FACTORY_OPTIONS
|
||||
|
||||
// clang-format on
|
||||
|
||||
/// helper to select harness type by name.
|
||||
class goto_harness_generator_factoryt
|
||||
{
|
||||
public:
|
||||
/// the type of a function that produces a goto-harness generator.
|
||||
using build_generatort =
|
||||
std::function<std::unique_ptr<goto_harness_generatort>()>;
|
||||
|
||||
using generator_optionst = std::map<std::string, std::list<std::string>>;
|
||||
|
||||
/// register a new goto-harness generator with the given name.
|
||||
/// \param generator_name: name of newly registered generator
|
||||
/// \param build_generator: the function that builds the generator
|
||||
void register_generator(
|
||||
std::string generator_name,
|
||||
build_generatort build_generator);
|
||||
|
||||
/// return a generator matching the generator name.
|
||||
/// throws if no generator with the supplied name is registered.
|
||||
std::unique_ptr<goto_harness_generatort> factory(
|
||||
const std::string &generator_name,
|
||||
const generator_optionst &generator_options);
|
||||
|
||||
private:
|
||||
std::map<std::string, build_generatort> generators;
|
||||
};
|
||||
|
||||
#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
|
||||
|
|
@ -6,47 +6,182 @@ Author: Diffblue Ltd.
|
|||
|
||||
\******************************************************************/
|
||||
|
||||
#include <cstddef>
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
#include "goto_harness_parse_options.h"
|
||||
|
||||
#include <cstddef>
|
||||
#include <set>
|
||||
#include <string>
|
||||
#include <utility>
|
||||
|
||||
#include <goto-programs/goto_convert.h>
|
||||
#include <goto-programs/goto_model.h>
|
||||
#include <goto-programs/read_goto_binary.h>
|
||||
#include <goto-programs/write_goto_binary.h>
|
||||
#include <util/config.h>
|
||||
#include <util/exception_utils.h>
|
||||
#include <util/exit_codes.h>
|
||||
#include <util/invariant.h>
|
||||
#include <util/version.h>
|
||||
|
||||
#include "goto_harness_parse_options.h"
|
||||
#include "function_call_harness_generator.h"
|
||||
#include "goto_harness_generator_factory.h"
|
||||
|
||||
// The basic idea is that this module is handling the following
|
||||
// sequence of events:
|
||||
// 1. Initialise a goto-model by parsing an input (goto) binary
|
||||
// 2. Initialise the harness generator (with some config) that will handle
|
||||
// the mutation of the goto-model. The generator should create a new
|
||||
// function that can be called by `cbmc --function`. The generated function
|
||||
// should implement the behaviour of the harness (What exactly this means
|
||||
// depends on the configuration)
|
||||
// 3. Write the end result of that process to the output binary
|
||||
|
||||
int goto_harness_parse_optionst::doit()
|
||||
{
|
||||
if(cmdline.isset("version"))
|
||||
{
|
||||
std::cout << CBMC_VERSION << '\n';
|
||||
logger.status() << CBMC_VERSION << '\n';
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
help();
|
||||
return CPROVER_EXIT_USAGE_ERROR;
|
||||
auto got_harness_config = handle_common_options();
|
||||
auto factory = make_factory();
|
||||
|
||||
auto factory_options = collect_generate_factory_options();
|
||||
|
||||
// Initialise harness generator
|
||||
auto harness_generator =
|
||||
factory.factory(got_harness_config.harness_type, factory_options);
|
||||
CHECK_RETURN(harness_generator != nullptr);
|
||||
|
||||
// This just sets up the defaults (and would interpret options such as --32).
|
||||
config.set(cmdline);
|
||||
|
||||
// Read goto binary into goto-model
|
||||
auto read_goto_binary_result =
|
||||
read_goto_binary(got_harness_config.in_file, logger.get_message_handler());
|
||||
if(!read_goto_binary_result.has_value())
|
||||
{
|
||||
throw deserialization_exceptiont{"failed to read goto program from file `" +
|
||||
got_harness_config.in_file + "'"};
|
||||
}
|
||||
auto goto_model = std::move(read_goto_binary_result.value());
|
||||
config.set_from_symbol_table(goto_model.symbol_table);
|
||||
|
||||
harness_generator->generate(
|
||||
goto_model, got_harness_config.harness_function_name);
|
||||
|
||||
// Write end result to new goto-binary
|
||||
if(write_goto_binary(
|
||||
got_harness_config.out_file, goto_model, logger.get_message_handler()))
|
||||
{
|
||||
throw system_exceptiont{"failed to write goto program from file `" +
|
||||
got_harness_config.out_file + "'"};
|
||||
}
|
||||
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
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";
|
||||
logger.status()
|
||||
<< '\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") << '\n'
|
||||
<< '\n'
|
||||
<< "Usage: Purpose:\n"
|
||||
<< '\n'
|
||||
<< " goto-harness [-?] [-h] [--help] show help\n"
|
||||
<< " goto-harness --version show version\n"
|
||||
<< " goto-harness <in> <out> --harness-function-name <name> --harness-type "
|
||||
"<harness-type> [harness options]\n"
|
||||
<< "\n"
|
||||
<< "<in> <out> goto binaries to read from / write to\n"
|
||||
<< "--harness-function-name the name of the harness function to "
|
||||
"generate\n"
|
||||
<< "--harness-type one of the harness types listed below\n"
|
||||
<< "\n\n"
|
||||
<< FUNCTION_HARNESS_GENERATOR_HELP << messaget::eom;
|
||||
}
|
||||
|
||||
goto_harness_parse_optionst::goto_harness_parse_optionst(
|
||||
int argc,
|
||||
const char *argv[])
|
||||
: parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv, ui_message_handler},
|
||||
ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION)
|
||||
ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION),
|
||||
logger(ui_message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
goto_harness_parse_optionst::goto_harness_configt
|
||||
goto_harness_parse_optionst::handle_common_options()
|
||||
{
|
||||
goto_harness_configt goto_harness_config{};
|
||||
|
||||
// This just checks the positional arguments to be 2.
|
||||
// Options are not in .args
|
||||
if(cmdline.args.size() != 2)
|
||||
{
|
||||
help();
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"need to specify both input and output goto binary file names (may be "
|
||||
"the same)",
|
||||
"<in goto binary> <out goto binary>"};
|
||||
}
|
||||
|
||||
goto_harness_config.in_file = cmdline.args[0];
|
||||
goto_harness_config.out_file = cmdline.args[1];
|
||||
|
||||
if(!cmdline.isset(GOTO_HARNESS_GENERATOR_TYPE_OPT))
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
|
||||
}
|
||||
goto_harness_config.harness_type =
|
||||
cmdline.get_value(GOTO_HARNESS_GENERATOR_TYPE_OPT);
|
||||
|
||||
// Read the name of the harness function to generate
|
||||
if(!cmdline.isset(GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT))
|
||||
{
|
||||
throw invalid_command_line_argument_exceptiont{
|
||||
"required option not set",
|
||||
"--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
|
||||
}
|
||||
goto_harness_config.harness_function_name = {
|
||||
cmdline.get_value(GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT)};
|
||||
|
||||
return goto_harness_config;
|
||||
}
|
||||
|
||||
goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory()
|
||||
{
|
||||
auto factory = goto_harness_generator_factoryt{};
|
||||
factory.register_generator("call-function", [this]() {
|
||||
return util_make_unique<function_call_harness_generatort>(
|
||||
ui_message_handler);
|
||||
});
|
||||
return factory;
|
||||
}
|
||||
|
||||
goto_harness_generator_factoryt::generator_optionst
|
||||
goto_harness_parse_optionst::collect_generate_factory_options()
|
||||
{
|
||||
auto const common_options =
|
||||
std::set<std::string>{"version",
|
||||
GOTO_HARNESS_GENERATOR_TYPE_OPT,
|
||||
GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
|
||||
|
||||
auto factory_options = goto_harness_generator_factoryt::generator_optionst{};
|
||||
|
||||
for(auto const &option : cmdline.option_names())
|
||||
{
|
||||
if(common_options.find(option) == common_options.end())
|
||||
{
|
||||
factory_options.insert({option, cmdline.get_values(option.c_str())});
|
||||
}
|
||||
}
|
||||
|
||||
return factory_options;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,23 @@ Author: Diffblue Ltd.
|
|||
#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H
|
||||
#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H
|
||||
|
||||
#include <string>
|
||||
|
||||
#include <goto-programs/goto_model.h>
|
||||
#include <util/parse_options.h>
|
||||
#include <util/ui_message.h>
|
||||
|
||||
#define GOTO_HARNESS_OPTIONS "(version)" // end GOTO_HARNESS_OPTIONS
|
||||
#include "function_harness_generator_options.h"
|
||||
#include "goto_harness_generator_factory.h"
|
||||
|
||||
// clang-format off
|
||||
#define GOTO_HARNESS_OPTIONS \
|
||||
"(version)" \
|
||||
GOTO_HARNESS_FACTORY_OPTIONS \
|
||||
FUNCTION_HARNESS_GENERATOR_OPTIONS \
|
||||
// end GOTO_HARNESS_OPTIONS
|
||||
|
||||
// clang-format on
|
||||
|
||||
class goto_harness_parse_optionst : public parse_options_baset
|
||||
{
|
||||
|
|
@ -22,13 +35,30 @@ public:
|
|||
|
||||
goto_harness_parse_optionst(int argc, const char *argv[]);
|
||||
|
||||
protected:
|
||||
ui_message_handlert ui_message_handler;
|
||||
|
||||
ui_message_handlert::uit get_ui()
|
||||
private:
|
||||
struct goto_harness_configt
|
||||
{
|
||||
return ui_message_handler.get_ui();
|
||||
}
|
||||
std::string in_file;
|
||||
std::string out_file;
|
||||
std::string harness_type;
|
||||
irep_idt harness_function_name;
|
||||
};
|
||||
|
||||
ui_message_handlert ui_message_handler;
|
||||
messaget logger;
|
||||
|
||||
/// Handle command line arguments that are common to all
|
||||
/// harness generators.
|
||||
goto_harness_configt handle_common_options();
|
||||
|
||||
/// Gather all the options that are not handled by
|
||||
/// `handle_common_options()`.
|
||||
goto_harness_generator_factoryt::generator_optionst
|
||||
collect_generate_factory_options();
|
||||
|
||||
/// Setup the generator factory. This is the function you
|
||||
/// need to change when you add a new generator.
|
||||
goto_harness_generator_factoryt make_factory();
|
||||
};
|
||||
|
||||
#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H
|
||||
|
|
|
|||
|
|
@ -1,2 +1,3 @@
|
|||
util
|
||||
goto-harness
|
||||
goto-programs
|
||||
Loading…
Reference in New Issue