diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ef56f62ef4a..e23cd3de23e 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -125,21 +125,16 @@ void code_contractst::check_apply_loop_contracts( // // Assertions for assigns clause checking are inserted in the loop body. - // an intermediate goto_program to store generated instructions - // to be inserted before the loop head - goto_programt pre_loop_head_instrs; - // Process "loop_entry" history variables. // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant. - std::map history_var_map; - replace_history_parameter( - symbol_table, - invariant, - history_var_map, - loop_head_location, - mode, - pre_loop_head_instrs, - ID_loop_entry); + auto replace_history_result = replace_history_loop_entry( + symbol_table, invariant, loop_head_location, mode); + invariant.swap(replace_history_result.expression_after_replacement); + const auto &history_var_map = replace_history_result.parameter_to_history; + // an intermediate goto_program to store generated instructions + // to be inserted before the loop head + goto_programt &pre_loop_head_instrs = + replace_history_result.history_construction; // Create a temporary to track if we entered the loop, // i.e., the loop guard was satisfied. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 7c986067f40..dbdfc4f6597 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -167,7 +167,7 @@ void dfcc_instrument_loopt::operator()( goto_programt::targett loop_latch = loop.find_latch(goto_function.body).value(); - const auto &history_var_map = add_prehead_instructions( + const auto history_var_map = add_prehead_instructions( loop_id, goto_function, symbol_table, @@ -234,7 +234,8 @@ void dfcc_instrument_loopt::operator()( goto_function.body.update(); } -std::map dfcc_instrument_loopt::add_prehead_instructions( +std::unordered_map +dfcc_instrument_loopt::add_prehead_instructions( const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table, @@ -269,22 +270,13 @@ std::map dfcc_instrument_loopt::add_prehead_instructions( // GOTO HEAD; // ``` - goto_programt pre_loop_head_instrs; - std::map history_var_map; // initialize loop_entry history vars; - { - // Process "loop_entry" history variables. - // We find and replace all "__CPROVER_loop_entry" in invariant. - replace_history_parameter( - symbol_table, - invariant, - history_var_map, - loop_head_location, - language_mode, - pre_loop_head_instrs, - ID_loop_entry); - } + auto replace_history_result = replace_history_loop_entry( + symbol_table, invariant, loop_head_location, language_mode); + invariant.swap(replace_history_result.expression_after_replacement); + goto_programt &pre_loop_head_instrs = + replace_history_result.history_construction; // entered_loop = false { @@ -354,7 +346,7 @@ std::map dfcc_instrument_loopt::add_prehead_instructions( goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location)); goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs); - return history_var_map; + return replace_history_result.parameter_to_history; } goto_programt::instructiont::targett @@ -614,7 +606,7 @@ void dfcc_instrument_loopt::add_exit_instructions( goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, - const std::map &history_var_map, + const std::unordered_map &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, @@ -690,10 +682,7 @@ void dfcc_instrument_loopt::add_exit_instructions( // Mark history variables as going out of scope. for(const auto &v : history_var_map) - { - loop_exit_program.add( - goto_programt::make_dead(to_symbol_expr(v.second), exit_location)); - } + loop_exit_program.add(goto_programt::make_dead(v.second, exit_location)); // Mark decreases clause snapshots as gong out of scope. for(size_t i = 0; i < old_decreases_vars.size(); i++) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h index 33f11a8b364..050e1690ce6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -197,7 +197,7 @@ class dfcc_instrument_loopt /// \param[in] in_base_case temporary variable `in_base_case`. /// \param[in] symbol_mode Language mode of the function. /// \return `history_var_map` that maps variables to loop_entry variables. - std::map add_prehead_instructions( + std::unordered_map add_prehead_instructions( const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table, @@ -348,7 +348,7 @@ class dfcc_instrument_loopt goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, - const std::map &history_var_map, + const std::unordered_map &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index c1164d085a6..2bc96a8c29a 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -11,7 +11,6 @@ Date: September 2021 #include "utils.h" #include -#include #include #include #include @@ -450,81 +449,107 @@ void add_quantified_variable( } } -void replace_history_parameter( +static void replace_history_parameter_rec( symbol_table_baset &symbol_table, exprt &expr, - std::map ¶meter2history, - source_locationt location, + std::unordered_map ¶meter2history, + const source_locationt &location, const irep_idt &mode, goto_programt &history, - const irep_idt &id) + const irep_idt &history_id) { for(auto &op : expr.operands()) { - replace_history_parameter( - symbol_table, op, parameter2history, location, mode, history, id); + replace_history_parameter_rec( + symbol_table, op, parameter2history, location, mode, history, history_id); } - if(expr.id() == ID_old || expr.id() == ID_loop_entry) - { - const auto ¶meter = to_history_expr(expr, id).expression(); + if(expr.id() != ID_old && expr.id() != ID_loop_entry) + return; - const auto &id = parameter.id(); - if( - id == ID_dereference || id == ID_member || id == ID_symbol || + const auto ¶meter = to_history_expr(expr, history_id).expression(); + const auto &id = parameter.id(); + DATA_INVARIANT_WITH_DIAGNOSTICS( + id == ID_dereference || id == ID_member || id == ID_symbol || id == ID_ptrmember || id == ID_constant || id == ID_typecast || - id == ID_index) - { - auto it = parameter2history.find(parameter); + id == ID_index, + "Tracking history of " + id2string(id) + + " expressions is not supported yet.", + parameter.pretty()); - if(it == parameter2history.end()) - { - // 0. Create a skip target to jump to, if the parameter is invalid - goto_programt skip_program; - const auto skip_target = - skip_program.add(goto_programt::make_skip(location)); - - // 1. Create a temporary symbol expression that represents the - // history variable - symbol_exprt tmp_symbol = - new_tmp_symbol(parameter.type(), location, mode, symbol_table) - .symbol_expr(); - - // 2. Associate the above temporary variable to it's corresponding - // expression - parameter2history[parameter] = tmp_symbol; - - // 3. Add the required instructions to the instructions list - // 3.1. Declare the newly created temporary variable - history.add(goto_programt::make_decl(tmp_symbol, location)); - - // 3.2. Skip storing the history if the expression is invalid - history.add(goto_programt::make_goto( - skip_target, - not_exprt{ - all_dereferences_are_valid(parameter, namespacet(symbol_table))}, - location)); - - // 3.3. Add an assignment such that the value pointed to by the new - // temporary variable is equal to the value of the corresponding - // parameter - history.add( - goto_programt::make_assignment(tmp_symbol, parameter, location)); - - // 3.4. Add a skip target - history.destructive_append(skip_program); - } + // speculatively insert a dummy, which will be replaced below if the insert + // actually happened + auto entry = + parameter2history.insert({parameter, symbol_exprt::typeless(ID_nil)}); - expr = parameter2history[parameter]; - } - else - { - throw invalid_source_file_exceptiont( - "Tracking history of " + id2string(parameter.id()) + - " expressions is not supported yet.", - expr.source_location()); - } + if(entry.second) + { + // 1. Create a temporary symbol expression that represents the + // history variable + entry.first->second = + new_tmp_symbol(parameter.type(), location, mode, symbol_table) + .symbol_expr(); + + // 2. Add the required instructions to the instructions list + // 2.1. Declare the newly created temporary variable + history.add(goto_programt::make_decl(entry.first->second, location)); + + // 2.2. Skip storing the history if the expression is invalid + auto goto_instruction = history.add(goto_programt::make_incomplete_goto( + not_exprt{ + all_dereferences_are_valid(parameter, namespacet(symbol_table))}, + location)); + + // 2.3. Add an assignment such that the value pointed to by the new + // temporary variable is equal to the value of the corresponding + // parameter + history.add( + goto_programt::make_assignment(entry.first->second, parameter, location)); + + // 2.4. Complete conditional jump for invalid-parameter case + auto label_instruction = history.add(goto_programt::make_skip(location)); + goto_instruction->complete_goto(label_instruction); } + + expr = entry.first->second; +} + +replace_history_parametert replace_history_old( + symbol_table_baset &symbol_table, + const exprt &expr, + const source_locationt &location, + const irep_idt &mode) +{ + replace_history_parametert result; + result.expression_after_replacement = expr; + replace_history_parameter_rec( + symbol_table, + result.expression_after_replacement, + result.parameter_to_history, + location, + mode, + result.history_construction, + ID_old); + return result; +} + +replace_history_parametert replace_history_loop_entry( + symbol_table_baset &symbol_table, + const exprt &expr, + const source_locationt &location, + const irep_idt &mode) +{ + replace_history_parametert result; + result.expression_after_replacement = expr; + replace_history_parameter_rec( + symbol_table, + result.expression_after_replacement, + result.parameter_to_history, + location, + mode, + result.history_construction, + ID_loop_entry); + return result; } void generate_history_variables_initialization( @@ -533,19 +558,12 @@ void generate_history_variables_initialization( const irep_idt &mode, goto_programt &program) { - std::map parameter2history; - goto_programt history; // Find and replace "old" expression in the "expression" variable - replace_history_parameter( - symbol_table, - clause, - parameter2history, - clause.source_location(), - mode, - history, - ID_old); + auto result = + replace_history_old(symbol_table, clause, clause.source_location(), mode); + clause.swap(result.expression_after_replacement); // Add all the history variable initialization instructions - program.destructive_append(history); + program.destructive_append(result.history_construction); } bool is_transformed_loop_head(const goto_programt::const_targett &target) diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index ed7a7adf27d..5a8aaa93004 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -242,16 +242,28 @@ void add_quantified_variable( exprt &expression, const irep_idt &mode); -/// This function recursively identifies the "old" expressions within expr +struct replace_history_parametert +{ + exprt expression_after_replacement; + std::unordered_map parameter_to_history; + goto_programt history_construction; +}; + +/// This function recursively identifies the "old" expressions within \p expr /// and replaces them with corresponding history variables. -void replace_history_parameter( +replace_history_parametert replace_history_old( symbol_table_baset &symbol_table, - exprt &expr, - std::map ¶meter2history, - source_locationt location, - const irep_idt &mode, - goto_programt &history, - const irep_idt &id); + const exprt &expr, + const source_locationt &location, + const irep_idt &mode); + +/// This function recursively identifies the "loop_entry" expressions within +/// \p expr and replaces them with corresponding history variables. +replace_history_parametert replace_history_loop_entry( + symbol_table_baset &symbol_table, + const exprt &expr, + const source_locationt &location, + const irep_idt &mode); /// This function generates all the instructions required to initialize /// history variables.