From 611f8a156883a9f50a4c6d40785dcae81ab748aa Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 4 Jun 2020 09:37:41 +0100 Subject: [PATCH 1/7] Move nondet volatile functionality into class nondet_volatilet This is in preparation of adding a new feature to selectively provide models for volatile reads. For this member variables will be added to nondet_volatilet to store configuration. --- src/goto-instrument/nondet_volatile.cpp | 33 +++++++++++++++++++++---- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index d8ee5fcc21d..b20938d4fbc 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -20,7 +20,29 @@ Date: September 2011 using havoc_predicatet = std::function; -static bool is_volatile(const namespacet &ns, const typet &src) +class nondet_volatilet +{ +public: + static void nondet_volatile( + symbol_tablet &symbol_table, + goto_programt &goto_program, + havoc_predicatet should_havoc); + +private: + static bool is_volatile(const namespacet &ns, const typet &src); + + static void nondet_volatile_rhs( + const symbol_tablet &symbol_table, + exprt &expr, + havoc_predicatet should_havoc); + + static void nondet_volatile_lhs( + const symbol_tablet &symbol_table, + exprt &expr, + havoc_predicatet should_havoc); +}; + +bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src) { if(src.get_bool(ID_C_volatile)) return true; @@ -35,7 +57,7 @@ static bool is_volatile(const namespacet &ns, const typet &src) return false; } -static void nondet_volatile_rhs( +void nondet_volatilet::nondet_volatile_rhs( const symbol_tablet &symbol_table, exprt &expr, havoc_predicatet should_havoc) @@ -59,7 +81,7 @@ static void nondet_volatile_rhs( } } -static void nondet_volatile_lhs( +void nondet_volatilet::nondet_volatile_lhs( const symbol_tablet &symbol_table, exprt &expr, havoc_predicatet should_havoc) @@ -91,7 +113,7 @@ static void nondet_volatile_lhs( } } -static void nondet_volatile( +void nondet_volatilet::nondet_volatile( symbol_tablet &symbol_table, goto_programt &goto_program, havoc_predicatet should_havoc) @@ -139,7 +161,8 @@ static void nondet_volatile( void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc) { Forall_goto_functions(f_it, goto_model.goto_functions) - nondet_volatile(goto_model.symbol_table, f_it->second.body, should_havoc); + nondet_volatilet::nondet_volatile( + goto_model.symbol_table, f_it->second.body, should_havoc); goto_model.goto_functions.update(); } From 4b841c7f17ad320b91f9bbfbdf9f9b6a2247f474 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 4 Jun 2020 09:43:59 +0100 Subject: [PATCH 2/7] Rework command line handling of the nonde volatile feature This refactors the command line handling and typechecking in class nondet_volatilet, and adds a new option --nondet-volatile-model (unimplemented) which will allow selectivly providing models for volatile reads. --- .../nondet-volatile-03/test.desc | 2 +- src/goto-instrument/nondet_volatile.cpp | 215 +++++++++++++++--- src/goto-instrument/nondet_volatile.h | 9 +- 3 files changed, 191 insertions(+), 35 deletions(-) diff --git a/regression/goto-instrument/nondet-volatile-03/test.desc b/regression/goto-instrument/nondet-volatile-03/test.desc index 7cda9c67582..f0c032024f3 100644 --- a/regression/goto-instrument/nondet-volatile-03/test.desc +++ b/regression/goto-instrument/nondet-volatile-03/test.desc @@ -2,7 +2,7 @@ CORE test.c --nondet-volatile-variable x ^Invalid User Input$ -given name x does not represent a volatile variable with static lifetime$ +symbol `x` does not represent a volatile variable with static lifetime$ ^EXIT=1$ ^SIGNAL=0$ -- diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index b20938d4fbc..6e140eb9d09 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -16,6 +16,7 @@ Date: September 2011 #include #include #include +#include #include using havoc_predicatet = std::function; @@ -28,6 +29,9 @@ class nondet_volatilet goto_programt &goto_program, havoc_predicatet should_havoc); + static const symbolt & + typecheck_variable(const irep_idt &id, const namespacet &ns); + private: static bool is_volatile(const namespacet &ns, const typet &src); @@ -40,6 +44,19 @@ class nondet_volatilet const symbol_tablet &symbol_table, exprt &expr, havoc_predicatet should_havoc); + + static void typecheck_model( + const irep_idt &id, + const symbolt &variable, + const namespacet &ns); + + void + typecheck_options(const goto_modelt &goto_model, const optionst &options); + + // configuration obtained from command line options + bool all_nondet; + std::set nondet_variables; + std::map variable_models; }; bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src) @@ -158,6 +175,146 @@ void nondet_volatilet::nondet_volatile( } } +const symbolt & +nondet_volatilet::typecheck_variable(const irep_idt &id, const namespacet &ns) +{ + const symbolt *symbol; + + if(ns.lookup(id, symbol)) + { + throw invalid_command_line_argument_exceptiont( + "given symbol `" + id2string(id) + "` not found in symbol table", + "--" NONDET_VOLATILE_VARIABLE_OPT); + } + + if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile)) + { + throw invalid_command_line_argument_exceptiont( + "symbol `" + id2string(id) + + "` does not represent a volatile variable " + "with static lifetime", + "--" NONDET_VOLATILE_VARIABLE_OPT); + } + + INVARIANT(!symbol->is_type, "symbol must not represent a type"); + + INVARIANT(!symbol->is_function(), "symbol must not represent a function"); + + return *symbol; +} + +void nondet_volatilet::typecheck_model( + const irep_idt &id, + const symbolt &variable, + const namespacet &ns) +{ + const symbolt *symbol; + + if(ns.lookup(id, symbol)) + { + throw invalid_command_line_argument_exceptiont( + "given model name " + id2string(id) + " not found in symbol table", + "--" NONDET_VOLATILE_MODEL_OPT); + } + + if(!symbol->is_function()) + { + throw invalid_command_line_argument_exceptiont( + "symbol `" + id2string(id) + "` is not a function", + "--" NONDET_VOLATILE_MODEL_OPT); + } + + const auto &code_type = to_code_type(symbol->type); + + if(variable.type != code_type.return_type()) + { + throw invalid_command_line_argument_exceptiont( + "return type of model `" + id2string(id) + + "` is not compatible with the " + "type of the modelled variable " + + id2string(variable.name), + "--" NONDET_VOLATILE_MODEL_OPT); + } + + if(!code_type.parameters().empty()) + { + throw invalid_command_line_argument_exceptiont( + "model `" + id2string(id) + "` must not take parameters ", + "--" NONDET_VOLATILE_MODEL_OPT); + } +} + +void nondet_volatilet::typecheck_options( + const goto_modelt &goto_model, + const optionst &options) +{ + PRECONDITION(nondet_variables.empty()); + PRECONDITION(variable_models.empty()); + + if(options.get_bool_option(NONDET_VOLATILE_OPT)) + { + all_nondet = true; + return; + } + + const namespacet ns(goto_model.symbol_table); + + if(options.is_set(NONDET_VOLATILE_VARIABLE_OPT)) + { + const auto &variable_list = + options.get_list_option(NONDET_VOLATILE_VARIABLE_OPT); + + nondet_variables.insert(variable_list.begin(), variable_list.end()); + + for(const auto &id : nondet_variables) + { + typecheck_variable(id, ns); + } + } + + if(options.is_set(NONDET_VOLATILE_MODEL_OPT)) + { + const auto &model_list = options.get_list_option(NONDET_VOLATILE_MODEL_OPT); + + for(const auto &s : model_list) + { + std::string variable; + std::string model; + + try + { + split_string(s, ':', variable, model, true); + } + catch(const deserialization_exceptiont &e) + { + throw invalid_command_line_argument_exceptiont( + "cannot split argument `" + s + "` into variable name and model name", + "--" NONDET_VOLATILE_MODEL_OPT); + } + + const auto &variable_symbol = typecheck_variable(variable, ns); + + if(nondet_variables.count(variable) != 0) + { + throw invalid_command_line_argument_exceptiont( + "conflicting options for variable `" + variable + "`", + "--" NONDET_VOLATILE_VARIABLE_OPT "/--" NONDET_VOLATILE_MODEL_OPT); + } + + typecheck_model(model, variable_symbol, ns); + + const auto p = variable_models.insert(std::make_pair(variable, model)); + + if(!p.second && p.first->second != model) + { + throw invalid_command_line_argument_exceptiont( + "conflicting models for variable `" + variable + "`", + "--" NONDET_VOLATILE_MODEL_OPT); + } + } + } +} + void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc) { Forall_goto_functions(f_it, goto_model.goto_functions) @@ -171,29 +328,45 @@ void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options) { PRECONDITION(!options.is_set(NONDET_VOLATILE_OPT)); PRECONDITION(!options.is_set(NONDET_VOLATILE_VARIABLE_OPT)); + PRECONDITION(!options.is_set(NONDET_VOLATILE_MODEL_OPT)); const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT); const bool nondet_volatile_variable_opt = cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT); + const bool nondet_volatile_model_opt = + cmdline.isset(NONDET_VOLATILE_MODEL_OPT); - if(nondet_volatile_opt && nondet_volatile_variable_opt) + if( + nondet_volatile_opt && + (nondet_volatile_variable_opt || nondet_volatile_model_opt)) { throw invalid_command_line_argument_exceptiont( - "only one of " NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT - "can " - "be given at a time", - NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT); + "--" NONDET_VOLATILE_OPT + " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT + " or --" NONDET_VOLATILE_MODEL_OPT, + "--" NONDET_VOLATILE_OPT "/--" NONDET_VOLATILE_VARIABLE_OPT + "/--" NONDET_VOLATILE_MODEL_OPT); } if(nondet_volatile_opt) { options.set_option(NONDET_VOLATILE_OPT, true); } - else if(cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT)) + else { - options.set_option( - NONDET_VOLATILE_VARIABLE_OPT, - cmdline.get_values(NONDET_VOLATILE_VARIABLE_OPT)); + if(nondet_volatile_variable_opt) + { + options.set_option( + NONDET_VOLATILE_VARIABLE_OPT, + cmdline.get_values(NONDET_VOLATILE_VARIABLE_OPT)); + } + + if(nondet_volatile_model_opt) + { + options.set_option( + NONDET_VOLATILE_MODEL_OPT, + cmdline.get_values(NONDET_VOLATILE_MODEL_OPT)); + } } } @@ -211,31 +384,9 @@ void nondet_volatile(goto_modelt &goto_model, const optionst &options) std::set variables(variable_list.begin(), variable_list.end()); const namespacet ns(goto_model.symbol_table); - // typecheck given variables for(const auto &id : variables) { - const symbolt *symbol; - - if(ns.lookup(id, symbol)) - { - throw invalid_command_line_argument_exceptiont( - "given name " + id2string(id) + " not found in symbol table", - NONDET_VOLATILE_VARIABLE_OPT); - } - - if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile)) - { - throw invalid_command_line_argument_exceptiont( - "given name " + id2string(id) + - " does not represent a volatile " - "variable with static lifetime", - NONDET_VOLATILE_VARIABLE_OPT); - } - - INVARIANT(!symbol->is_type, "symbol must not represent a type"); - - INVARIANT( - symbol->type.id() != ID_code, "symbol must not represent a function"); + nondet_volatilet::typecheck_variable(id, ns); } auto should_havoc = [&variables](const exprt &expr) { diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h index 8f8142ad42a..dc12bf83551 100644 --- a/src/goto-instrument/nondet_volatile.h +++ b/src/goto-instrument/nondet_volatile.h @@ -20,17 +20,22 @@ class optionst; // clang-format off #define NONDET_VOLATILE_OPT "nondet-volatile" #define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable" +#define NONDET_VOLATILE_MODEL_OPT "nondet-volatile-model" #define OPT_NONDET_VOLATILE \ "(" NONDET_VOLATILE_OPT ")" \ - "(" NONDET_VOLATILE_VARIABLE_OPT "):" + "(" NONDET_VOLATILE_VARIABLE_OPT "):" \ + "(" NONDET_VOLATILE_MODEL_OPT "):" #define HELP_NONDET_VOLATILE \ " --" NONDET_VOLATILE_OPT " makes reads from volatile variables " \ "non-deterministic\n" \ " --" NONDET_VOLATILE_VARIABLE_OPT " \n" \ " makes reads from given volatile variable " \ - "non-deterministic\n" + "non-deterministic\n" \ + " --" NONDET_VOLATILE_MODEL_OPT ":\n" \ + " models reads from given volatile variable " \ + "by a call to the given model" // clang-format on void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options); From 47bb11e84d02e5b0e88d1bd93721daf967be1b14 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 4 Jun 2020 15:52:03 +0100 Subject: [PATCH 3/7] Refactor existing nondet volatile code Refactor the code such as to allow later addition of new feature to selectively provide models for volatile reads --- src/goto-instrument/nondet_volatile.cpp | 162 +++++++++++------------- 1 file changed, 73 insertions(+), 89 deletions(-) diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index 6e140eb9d09..7cc3470de46 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -19,39 +19,52 @@ Date: September 2011 #include #include -using havoc_predicatet = std::function; - class nondet_volatilet { public: - static void nondet_volatile( - symbol_tablet &symbol_table, - goto_programt &goto_program, - havoc_predicatet should_havoc); + nondet_volatilet(goto_modelt &goto_model, const optionst &options) + : goto_model(goto_model), all_nondet(false) + { + typecheck_options(options); + } + + void operator()() + { + if(!all_nondet && nondet_variables.empty() && variable_models.empty()) + { + return; + } + + for(auto &f : goto_model.goto_functions.function_map) + { + nondet_volatile(goto_model.symbol_table, f.second.body); + } - static const symbolt & - typecheck_variable(const irep_idt &id, const namespacet &ns); + goto_model.goto_functions.update(); + } private: static bool is_volatile(const namespacet &ns, const typet &src); - static void nondet_volatile_rhs( - const symbol_tablet &symbol_table, - exprt &expr, - havoc_predicatet should_havoc); + void handle_volatile_expression(exprt &expr, const namespacet &ns); + + void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr); - static void nondet_volatile_lhs( - const symbol_tablet &symbol_table, - exprt &expr, - havoc_predicatet should_havoc); + void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr); - static void typecheck_model( + void + nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program); + + const symbolt &typecheck_variable(const irep_idt &id, const namespacet &ns); + + void typecheck_model( const irep_idt &id, const symbolt &variable, const namespacet &ns); - void - typecheck_options(const goto_modelt &goto_model, const optionst &options); + void typecheck_options(const optionst &options); + + goto_modelt &goto_model; // configuration obtained from command line options bool all_nondet; @@ -74,66 +87,71 @@ bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src) return false; } +void nondet_volatilet::handle_volatile_expression( + exprt &expr, + const namespacet &ns) +{ + if( + all_nondet || + (expr.id() == ID_symbol && + nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0)) + { + typet t = expr.type(); + t.remove(ID_C_volatile); + + // replace by nondet + side_effect_expr_nondett nondet_expr(t, expr.source_location()); + expr.swap(nondet_expr); + } +} + void nondet_volatilet::nondet_volatile_rhs( const symbol_tablet &symbol_table, - exprt &expr, - havoc_predicatet should_havoc) + exprt &expr) { Forall_operands(it, expr) - nondet_volatile_rhs(symbol_table, *it, should_havoc); + nondet_volatile_rhs(symbol_table, *it); if(expr.id()==ID_symbol || expr.id()==ID_dereference) { const namespacet ns(symbol_table); - if(is_volatile(ns, expr.type()) && should_havoc(expr)) - { - typet t=expr.type(); - t.remove(ID_C_volatile); - // replace by nondet - side_effect_expr_nondett nondet_expr(t, expr.source_location()); - expr.swap(nondet_expr); + if(is_volatile(ns, expr.type())) + { + handle_volatile_expression(expr, ns); } } } void nondet_volatilet::nondet_volatile_lhs( const symbol_tablet &symbol_table, - exprt &expr, - havoc_predicatet should_havoc) + exprt &expr) { if(expr.id()==ID_if) { - nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), should_havoc); - nondet_volatile_lhs( - symbol_table, to_if_expr(expr).true_case(), should_havoc); - nondet_volatile_lhs( - symbol_table, to_if_expr(expr).false_case(), should_havoc); + nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond()); + nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case()); + nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case()); } else if(expr.id()==ID_index) { - nondet_volatile_lhs( - symbol_table, to_index_expr(expr).array(), should_havoc); - nondet_volatile_rhs( - symbol_table, to_index_expr(expr).index(), should_havoc); + nondet_volatile_lhs(symbol_table, to_index_expr(expr).array()); + nondet_volatile_rhs(symbol_table, to_index_expr(expr).index()); } else if(expr.id()==ID_member) { - nondet_volatile_lhs( - symbol_table, to_member_expr(expr).struct_op(), should_havoc); + nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op()); } else if(expr.id()==ID_dereference) { - nondet_volatile_rhs( - symbol_table, to_dereference_expr(expr).pointer(), should_havoc); + nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer()); } } void nondet_volatilet::nondet_volatile( symbol_tablet &symbol_table, - goto_programt &goto_program, - havoc_predicatet should_havoc) + goto_programt &goto_program) { namespacet ns(symbol_table); @@ -143,10 +161,8 @@ void nondet_volatilet::nondet_volatile( if(instruction.is_assign()) { - nondet_volatile_rhs( - symbol_table, to_code_assign(instruction.code).rhs(), should_havoc); - nondet_volatile_lhs( - symbol_table, to_code_assign(instruction.code).lhs(), should_havoc); + nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs()); + nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs()); } else if(instruction.is_function_call()) { @@ -160,16 +176,16 @@ void nondet_volatilet::nondet_volatile( it=code_function_call.arguments().begin(); it!=code_function_call.arguments().end(); it++) - nondet_volatile_rhs(symbol_table, *it, should_havoc); + nondet_volatile_rhs(symbol_table, *it); // do return value - nondet_volatile_lhs(symbol_table, code_function_call.lhs(), should_havoc); + nondet_volatile_lhs(symbol_table, code_function_call.lhs()); } else if(instruction.has_condition()) { // do condition exprt cond = instruction.get_condition(); - nondet_volatile_rhs(symbol_table, cond, should_havoc); + nondet_volatile_rhs(symbol_table, cond); instruction.set_condition(cond); } } @@ -244,10 +260,9 @@ void nondet_volatilet::typecheck_model( } } -void nondet_volatilet::typecheck_options( - const goto_modelt &goto_model, - const optionst &options) +void nondet_volatilet::typecheck_options(const optionst &options) { + PRECONDITION(!all_nondet); PRECONDITION(nondet_variables.empty()); PRECONDITION(variable_models.empty()); @@ -315,15 +330,6 @@ void nondet_volatilet::typecheck_options( } } -void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc) -{ - Forall_goto_functions(f_it, goto_model.goto_functions) - nondet_volatilet::nondet_volatile( - goto_model.symbol_table, f_it->second.body, should_havoc); - - goto_model.goto_functions.update(); -} - void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options) { PRECONDITION(!options.is_set(NONDET_VOLATILE_OPT)); @@ -372,28 +378,6 @@ void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options) void nondet_volatile(goto_modelt &goto_model, const optionst &options) { - if(options.get_bool_option(NONDET_VOLATILE_OPT)) - { - nondet_volatile(goto_model); - } - else if(options.is_set(NONDET_VOLATILE_VARIABLE_OPT)) - { - const auto &variable_list = - options.get_list_option(NONDET_VOLATILE_VARIABLE_OPT); - - std::set variables(variable_list.begin(), variable_list.end()); - const namespacet ns(goto_model.symbol_table); - - for(const auto &id : variables) - { - nondet_volatilet::typecheck_variable(id, ns); - } - - auto should_havoc = [&variables](const exprt &expr) { - return expr.id() == ID_symbol && - variables.count(to_symbol_expr(expr).get_identifier()) != 0; - }; - - nondet_volatile(goto_model, should_havoc); - } + nondet_volatilet nv(goto_model, options); + nv(); } From d08257ebe4ed92a90b0f488f589702d6f14c2ea5 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 4 Jun 2020 16:17:59 +0100 Subject: [PATCH 4/7] Add new feature to provide models for volatile reads Implements the option --nondet-volatile-model : to allow to specify models which are called whenever the given volatile variable is read. The return value of the model is used as the value read from the volatile variable. --- src/goto-instrument/nondet_volatile.cpp | 119 +++++++++++++++++++----- 1 file changed, 96 insertions(+), 23 deletions(-) diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index 7cc3470de46..560c243056c 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -14,6 +14,7 @@ Date: September 2011 #include "nondet_volatile.h" #include +#include #include #include #include @@ -46,11 +47,23 @@ class nondet_volatilet private: static bool is_volatile(const namespacet &ns, const typet &src); - void handle_volatile_expression(exprt &expr, const namespacet &ns); + void handle_volatile_expression( + exprt &expr, + const namespacet &ns, + goto_programt &pre, + goto_programt &post); - void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr); + void nondet_volatile_rhs( + const symbol_tablet &symbol_table, + exprt &expr, + goto_programt &pre, + goto_programt &post); - void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr); + void nondet_volatile_lhs( + const symbol_tablet &symbol_table, + exprt &expr, + goto_programt &pre, + goto_programt &post); void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program); @@ -89,8 +102,11 @@ bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src) void nondet_volatilet::handle_volatile_expression( exprt &expr, - const namespacet &ns) + const namespacet &ns, + goto_programt &pre, + goto_programt &post) { + // Check if we should replace the variable by a nondet expression if( all_nondet || (expr.id() == ID_symbol && @@ -99,18 +115,56 @@ void nondet_volatilet::handle_volatile_expression( typet t = expr.type(); t.remove(ID_C_volatile); - // replace by nondet side_effect_expr_nondett nondet_expr(t, expr.source_location()); expr.swap(nondet_expr); + + return; + } + + // Now check if we should replace the variable by a model + + if(expr.id() != ID_symbol) + { + return; + } + + const irep_idt &id = to_symbol_expr(expr).get_identifier(); + const auto &it = variable_models.find(id); + + if(it == variable_models.end()) + { + return; } + + const auto &model_symbol = ns.lookup(it->second); + + const auto &new_variable = get_fresh_aux_symbol( + to_code_type(model_symbol.type).return_type(), + "", + "modelled_volatile", + source_locationt(), + ID_C, + goto_model.symbol_table) + .symbol_expr(); + + pre.instructions.push_back(goto_programt::make_decl(new_variable)); + + code_function_callt call(new_variable, model_symbol.symbol_expr(), {}); + pre.instructions.push_back(goto_programt::make_function_call(call)); + + post.instructions.push_back(goto_programt::make_dead(new_variable)); + + expr = new_variable; } void nondet_volatilet::nondet_volatile_rhs( const symbol_tablet &symbol_table, - exprt &expr) + exprt &expr, + goto_programt &pre, + goto_programt &post) { Forall_operands(it, expr) - nondet_volatile_rhs(symbol_table, *it); + nondet_volatile_rhs(symbol_table, *it, pre, post); if(expr.id()==ID_symbol || expr.id()==ID_dereference) @@ -119,33 +173,37 @@ void nondet_volatilet::nondet_volatile_rhs( if(is_volatile(ns, expr.type())) { - handle_volatile_expression(expr, ns); + handle_volatile_expression(expr, ns, pre, post); } } } void nondet_volatilet::nondet_volatile_lhs( const symbol_tablet &symbol_table, - exprt &expr) + exprt &expr, + goto_programt &pre, + goto_programt &post) { if(expr.id()==ID_if) { - nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond()); - nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case()); - nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case()); + nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), pre, post); + nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case(), pre, post); + nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case(), pre, post); } else if(expr.id()==ID_index) { - nondet_volatile_lhs(symbol_table, to_index_expr(expr).array()); - nondet_volatile_rhs(symbol_table, to_index_expr(expr).index()); + nondet_volatile_lhs(symbol_table, to_index_expr(expr).array(), pre, post); + nondet_volatile_rhs(symbol_table, to_index_expr(expr).index(), pre, post); } else if(expr.id()==ID_member) { - nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op()); + nondet_volatile_lhs( + symbol_table, to_member_expr(expr).struct_op(), pre, post); } else if(expr.id()==ID_dereference) { - nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer()); + nondet_volatile_rhs( + symbol_table, to_dereference_expr(expr).pointer(), pre, post); } } @@ -155,14 +213,21 @@ void nondet_volatilet::nondet_volatile( { namespacet ns(symbol_table); - Forall_goto_program_instructions(i_it, goto_program) + for(auto i_it = goto_program.instructions.begin(); + i_it != goto_program.instructions.end(); + i_it++) { - goto_programt::instructiont &instruction=*i_it; + goto_programt pre; + goto_programt post; + + goto_programt::instructiont &instruction = *i_it; if(instruction.is_assign()) { - nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs()); - nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs()); + nondet_volatile_rhs( + symbol_table, to_code_assign(instruction.code).rhs(), pre, post); + nondet_volatile_lhs( + symbol_table, to_code_assign(instruction.code).lhs(), pre, post); } else if(instruction.is_function_call()) { @@ -176,18 +241,26 @@ void nondet_volatilet::nondet_volatile( it=code_function_call.arguments().begin(); it!=code_function_call.arguments().end(); it++) - nondet_volatile_rhs(symbol_table, *it); + nondet_volatile_rhs(symbol_table, *it, pre, post); // do return value - nondet_volatile_lhs(symbol_table, code_function_call.lhs()); + nondet_volatile_lhs(symbol_table, code_function_call.lhs(), pre, post); } else if(instruction.has_condition()) { // do condition exprt cond = instruction.get_condition(); - nondet_volatile_rhs(symbol_table, cond); + nondet_volatile_rhs(symbol_table, cond, pre, post); instruction.set_condition(cond); } + + const auto pre_size = pre.instructions.size(); + goto_program.insert_before_swap(i_it, pre); + std::advance(i_it, pre_size); + + const auto post_size = post.instructions.size(); + goto_program.destructive_insert(std::next(i_it), post); + std::advance(i_it, post_size); } } From cc46483a9e445687656b4728b2176d20a71b9eff Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 3 Jun 2020 20:33:12 +0100 Subject: [PATCH 5/7] Add regression tests for --nondet-volatile-model --- .../nondet-volatile-model-01/test.c | 20 +++++++++++++++ .../nondet-volatile-model-01/test.desc | 12 +++++++++ .../nondet-volatile-model-02/test.c | 25 +++++++++++++++++++ .../nondet-volatile-model-02/test.desc | 16 ++++++++++++ .../nondet-volatile-model-03/test.c | 20 +++++++++++++++ .../nondet-volatile-model-03/test.desc | 11 ++++++++ 6 files changed, 104 insertions(+) create mode 100644 regression/goto-instrument/nondet-volatile-model-01/test.c create mode 100644 regression/goto-instrument/nondet-volatile-model-01/test.desc create mode 100644 regression/goto-instrument/nondet-volatile-model-02/test.c create mode 100644 regression/goto-instrument/nondet-volatile-model-02/test.desc create mode 100644 regression/goto-instrument/nondet-volatile-model-03/test.c create mode 100644 regression/goto-instrument/nondet-volatile-model-03/test.desc diff --git a/regression/goto-instrument/nondet-volatile-model-01/test.c b/regression/goto-instrument/nondet-volatile-model-01/test.c new file mode 100644 index 00000000000..ad937de7b1c --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-01/test.c @@ -0,0 +1,20 @@ +#include + +volatile int a; +volatile int b; + +int model() +{ + int value; + __CPROVER_assume(value >= 0); + return value; +} + +void main() +{ + assert(a == 0); + + assert(b >= 0); + assert(b == 0); + assert(b != 0); +} diff --git a/regression/goto-instrument/nondet-volatile-model-01/test.desc b/regression/goto-instrument/nondet-volatile-model-01/test.desc new file mode 100644 index 00000000000..215cfcce941 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-01/test.desc @@ -0,0 +1,12 @@ +CORE +test.c +--nondet-volatile-model b:model +\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS +\[main.assertion.2\] line \d+ assertion b >= 0: SUCCESS +\[main.assertion.3\] line \d+ assertion b == 0: FAILURE +\[main.assertion.4\] line \d+ assertion b != 0: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that the read from b is modelled via the given model diff --git a/regression/goto-instrument/nondet-volatile-model-02/test.c b/regression/goto-instrument/nondet-volatile-model-02/test.c new file mode 100644 index 00000000000..5374b21a96b --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-02/test.c @@ -0,0 +1,25 @@ +#include + +volatile int a; +volatile int b; +volatile int c; + +int model() +{ + int value; + __CPROVER_assume(value >= 0); + return value; +} + +void main() +{ + assert(a == 0); + + assert(b >= 0); + assert(b == 0); + assert(b != 0); + + assert(c >= 0); + assert(c == 0); + assert(c != 0); +} diff --git a/regression/goto-instrument/nondet-volatile-model-02/test.desc b/regression/goto-instrument/nondet-volatile-model-02/test.desc new file mode 100644 index 00000000000..b3812b2413e --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-02/test.desc @@ -0,0 +1,16 @@ +CORE +test.c +--nondet-volatile-variable b --nondet-volatile-model c:model +\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS +\[main.assertion.2\] line \d+ assertion b >= 0: FAILURE +\[main.assertion.3\] line \d+ assertion b == 0: FAILURE +\[main.assertion.4\] line \d+ assertion b != 0: FAILURE +\[main.assertion.5\] line \d+ assertion c >= 0: SUCCESS +\[main.assertion.6\] line \d+ assertion c == 0: FAILURE +\[main.assertion.7\] line \d+ assertion c != 0: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that both options for selectively havocking/modelling volatile reads can +be used together diff --git a/regression/goto-instrument/nondet-volatile-model-03/test.c b/regression/goto-instrument/nondet-volatile-model-03/test.c new file mode 100644 index 00000000000..e115f236837 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-03/test.c @@ -0,0 +1,20 @@ +#include + +volatile int a; +volatile int b; + +int model_a() +{ + return 1; +} + +int model_b() +{ + return 2; +} + +void main() +{ + int result = a + b; + assert(result == 3); +} diff --git a/regression/goto-instrument/nondet-volatile-model-03/test.desc b/regression/goto-instrument/nondet-volatile-model-03/test.desc new file mode 100644 index 00000000000..03f05d01f52 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-03/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--nondet-volatile-model a:model_a --nondet-volatile-model b:model_b +\[main.assertion.1\] line \d+ assertion result == 3: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +-- +Checks that two volatile reads in the same expression can both be modelled by +given functions From 47ad91abbeb3aec95b87c7d75853b2fa4734b4b8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 8 Jun 2020 09:19:27 +0100 Subject: [PATCH 6/7] Add regression tests for invalid usage of --nondet-volatile-model --- .../nondet-volatile-model-04/test.c | 13 +++++++++++++ .../nondet-volatile-model-04/test1.desc | 11 +++++++++++ .../nondet-volatile-model-04/test2.desc | 11 +++++++++++ .../nondet-volatile-model-05/test.c | 18 ++++++++++++++++++ .../nondet-volatile-model-05/test1.desc | 11 +++++++++++ .../nondet-volatile-model-05/test2.desc | 11 +++++++++++ 6 files changed, 75 insertions(+) create mode 100644 regression/goto-instrument/nondet-volatile-model-04/test.c create mode 100644 regression/goto-instrument/nondet-volatile-model-04/test1.desc create mode 100644 regression/goto-instrument/nondet-volatile-model-04/test2.desc create mode 100644 regression/goto-instrument/nondet-volatile-model-05/test.c create mode 100644 regression/goto-instrument/nondet-volatile-model-05/test1.desc create mode 100644 regression/goto-instrument/nondet-volatile-model-05/test2.desc diff --git a/regression/goto-instrument/nondet-volatile-model-04/test.c b/regression/goto-instrument/nondet-volatile-model-04/test.c new file mode 100644 index 00000000000..ebaeca4fc31 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-04/test.c @@ -0,0 +1,13 @@ +#include + +volatile int a; + +float model() +{ + return 1; +} + +void main() +{ + a; +} diff --git a/regression/goto-instrument/nondet-volatile-model-04/test1.desc b/regression/goto-instrument/nondet-volatile-model-04/test1.desc new file mode 100644 index 00000000000..5dd8cf9eddc --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-04/test1.desc @@ -0,0 +1,11 @@ +CORE +test.c +--nondet-volatile-model a:model +^Invalid User Input$ +return type of model .* is not compatible with the type of the modelled variable +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Check that the command line typechecking reports when a model with a return type +that is incompatible with the type of the modelled variable is given diff --git a/regression/goto-instrument/nondet-volatile-model-04/test2.desc b/regression/goto-instrument/nondet-volatile-model-04/test2.desc new file mode 100644 index 00000000000..dc5ef6a1b34 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-04/test2.desc @@ -0,0 +1,11 @@ +CORE +test.c +--nondet-volatile-model a:non_existing_model +^Invalid User Input$ +given model name .* not found in symbol table +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Check that the command line typechecking reports when a given model for a +variable cannot be found diff --git a/regression/goto-instrument/nondet-volatile-model-05/test.c b/regression/goto-instrument/nondet-volatile-model-05/test.c new file mode 100644 index 00000000000..5a1d92178dc --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-05/test.c @@ -0,0 +1,18 @@ +#include + +volatile int a; + +int model_a() +{ + return 1; +} + +int model_b() +{ + return 2; +} + +void main() +{ + a; +} diff --git a/regression/goto-instrument/nondet-volatile-model-05/test1.desc b/regression/goto-instrument/nondet-volatile-model-05/test1.desc new file mode 100644 index 00000000000..581011f6744 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-05/test1.desc @@ -0,0 +1,11 @@ +CORE +test.c +--nondet-volatile-model a:model_a --nondet-volatile-model a:model_b +^Invalid User Input$ +conflicting models for variable +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Check that the command line typechecking reports when two conflicting models are +given for a variable diff --git a/regression/goto-instrument/nondet-volatile-model-05/test2.desc b/regression/goto-instrument/nondet-volatile-model-05/test2.desc new file mode 100644 index 00000000000..52f91e2c55d --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-model-05/test2.desc @@ -0,0 +1,11 @@ +CORE +test.c +--nondet-volatile-model a:model_a --nondet-volatile-variable a +^Invalid User Input$ +conflicting options for variable +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Check that the command line typechecking reports when conflicting options are +given for a variable From d8c64417231b6bf2b7277ac9d472555349521ce6 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 9 Jun 2020 11:50:02 +0100 Subject: [PATCH 7/7] Add regression test for interaction of volatile/non-volatile variables --- regression/goto-instrument/nondet-volatile-04/test.c | 10 ++++++++++ .../goto-instrument/nondet-volatile-04/test.desc | 9 +++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/goto-instrument/nondet-volatile-04/test.c create mode 100644 regression/goto-instrument/nondet-volatile-04/test.desc diff --git a/regression/goto-instrument/nondet-volatile-04/test.c b/regression/goto-instrument/nondet-volatile-04/test.c new file mode 100644 index 00000000000..bb7ce0c1f76 --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-04/test.c @@ -0,0 +1,10 @@ +#include + +volatile int x; +int y; + +void main() +{ + y = x; + assert(x == y); +} diff --git a/regression/goto-instrument/nondet-volatile-04/test.desc b/regression/goto-instrument/nondet-volatile-04/test.desc new file mode 100644 index 00000000000..712d9cf523a --- /dev/null +++ b/regression/goto-instrument/nondet-volatile-04/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--nondet-volatile +^\[main.assertion.1\] line \d+ assertion x == y: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Check interaction between a volatile and a non-volatile variable