diff --git a/unit/Makefile b/unit/Makefile index 1f92f2be2d62..ec4860b5766e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -7,6 +7,7 @@ SRC = unit_tests.cpp \ # Test source files SRC += unit_tests.cpp \ + analyses/ai/ai.cpp \ analyses/ai/ai_simplify_lhs.cpp \ analyses/call_graph.cpp \ analyses/constant_propagator.cpp \ diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp new file mode 100644 index 000000000000..7441b2a83bb9 --- /dev/null +++ b/unit/analyses/ai/ai.cpp @@ -0,0 +1,297 @@ +/*******************************************************************\ + + Module: Unit tests for selectively retaining particular domains in ait + + Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Unit tests for selectively retaining particular domains in ait + +#include + +#include + +#include + +#include + +#include + +#include +#include +#include +#include + +/// A very simple analysis that counts executed instructions along a particular +/// path, taking the max at merge points and saturating at 100 instructions. +/// It should indicate that instructions not within a loop have a certain path +/// length, and those reachable from a loop have a path length of 100 +/// (i.e. potentially infinity) +class instruction_counter_domaint : public ai_domain_baset +{ +public: + + optionalt path_length; + + void transform(locationt, locationt, ai_baset &, const namespacet &) override + { + if(*path_length < 100) + ++*path_length; + } + + void make_bottom() override + { + path_length = {}; + } + void make_top() override + { + UNREACHABLE; + } + void make_entry() override + { + path_length = 0; + } + bool is_bottom() const override + { + return !path_length.has_value(); + } + bool is_top() const override + { + UNREACHABLE; + return true; + } + + bool merge(const instruction_counter_domaint &b, locationt from, locationt to) + { + if(b.is_bottom()) + return false; + + if(!path_length.has_value()) + path_length = 0; + + unsigned old_count = *path_length; + // Max path length to get here: + *path_length = + std::max(*path_length, *b.path_length); + return *path_length != old_count; + } +}; + +class instruction_counter_analysist : public ait +{ +public: + + static bool is_y_assignment(const goto_programt::instructiont &i) + { + if(!i.is_assign()) + return false; + const code_assignt &assign = to_code_assign(i.code); + return + assign.lhs().id() == ID_symbol && + id2string(to_symbol_expr(assign.lhs()).get_identifier()).find('y') != + std::string::npos; + } + + static bool is_y_assignment_location(locationt l) + { + // At assignments to variables with a 'y' in their name, keep the domain. + // Otherwise let ait decide whether to keep it. + return is_y_assignment(*l); + } +}; + +static code_function_callt make_void_call(const symbol_exprt &function) +{ + code_function_callt ret; + ret.function() = function; + return ret; +} + +SCENARIO( + "ait general testing", "[core][analyses][ai][general]") +{ + // Make a program like: + + // __CPROVER_start() { f(); } + // + // f() { + // int x = 10; + // int y = 20; + // h(); + // while(x != 0) { + // x -= 1; + // y -= 1; + // g(); + // } + // g(); // To ensure that this later call doesn't overwrite the earlier + // // calls from within the loop (i.e. the top of 'g' is respected + // // as a merge point) + // } + // + // Called from within loop, so should have a long possible path + // g() { int gy = 0; } + // + // Only called before loop, so should have a short path + // h() { int hy = 0; } + + register_language(new_ansi_c_language); + config.ansi_c.set_LP64(); + + goto_modelt goto_model; + + // g: + + symbolt gy; + gy.name = "gy"; + gy.mode = ID_C; + gy.type = signed_int_type(); + + symbolt g; + g.name = "g"; + g.mode = ID_C; + g.type = code_typet({}, void_typet()); + g.value = code_assignt(gy.symbol_expr(), from_integer(0, signed_int_type())); + + // h: + + symbolt hy; + hy.name = "hy"; + hy.mode = ID_C; + hy.type = signed_int_type(); + + symbolt h; + h.name = "h"; + h.mode = ID_C; + h.type = code_typet({}, void_typet()); + h.value = code_assignt(hy.symbol_expr(), from_integer(0, signed_int_type())); + + goto_model.symbol_table.add(g); + goto_model.symbol_table.add(gy); + goto_model.symbol_table.add(h); + goto_model.symbol_table.add(hy); + + // f: + + symbolt x; + x.name = "x"; + x.mode = ID_C; + x.type = signed_int_type(); + + symbolt y; + y.name = "y"; + y.mode = ID_C; + y.type = signed_int_type(); + + goto_model.symbol_table.add(x); + goto_model.symbol_table.add(y); + + code_blockt f_body; + + f_body.copy_to_operands(code_declt(x.symbol_expr())); + f_body.copy_to_operands(code_declt(y.symbol_expr())); + + f_body.copy_to_operands( + code_assignt(x.symbol_expr(), from_integer(10, signed_int_type()))); + f_body.copy_to_operands( + code_assignt(y.symbol_expr(), from_integer(20, signed_int_type()))); + + f_body.copy_to_operands(make_void_call(h.symbol_expr())); + + code_whilet loop; + + loop.cond() = + notequal_exprt(x.symbol_expr(), from_integer(0, signed_int_type())); + + code_blockt loop_body; + loop_body.copy_to_operands( + code_assignt( + x.symbol_expr(), + minus_exprt(x.symbol_expr(), from_integer(1, signed_int_type())))); + loop_body.copy_to_operands( + code_assignt( + y.symbol_expr(), + minus_exprt(y.symbol_expr(), from_integer(1, signed_int_type())))); + loop_body.copy_to_operands(make_void_call(g.symbol_expr())); + + loop.body() = loop_body; + + f_body.move_to_operands(loop); + + f_body.copy_to_operands(make_void_call(g.symbol_expr())); + + symbolt f; + f.name = "f"; + f.mode = ID_C; + f.type = code_typet({}, void_typet()); + f.value = f_body; + + goto_model.symbol_table.add(f); + + // __CPROVER_start: + + symbolt start; + start.name = goto_functionst::entry_point(); + start.mode = ID_C; + start.type = code_typet({}, void_typet()); + start.value = make_void_call(f.symbol_expr()); + + goto_model.symbol_table.add(start); + + null_message_handlert nullout; + goto_convert(goto_model, nullout); + + WHEN("The target program is analysed") + { + instruction_counter_analysist example_analysis; + example_analysis(goto_model); + + THEN("No state should be bottom") + { + forall_goto_functions(f_it, goto_model.goto_functions) + { + forall_goto_program_instructions(i_it, f_it->second.body) + { + REQUIRE_FALSE(example_analysis[i_it].is_bottom()); + } + } + } + + THEN("The first y-assignment should have a short path; " + "the second should have a long one") + { + const auto &f_instructions = + goto_model.goto_functions.function_map.at("f").body.instructions; + + std::vector y_assignments; + for(auto l = f_instructions.begin(); l != f_instructions.end(); ++l) + if(instruction_counter_analysist::is_y_assignment_location(l)) + y_assignments.push_back(l); + + REQUIRE(y_assignments.size() == 2); + REQUIRE_FALSE(example_analysis[y_assignments[0]].is_bottom()); + REQUIRE(*(example_analysis[y_assignments[0]].path_length) < 100); + REQUIRE_FALSE(example_analysis[y_assignments[1]].is_bottom()); + REQUIRE(*(example_analysis[y_assignments[1]].path_length) == 100); + } + + THEN("The assignment in function 'g' should have a long path") + { + const auto &g_instructions = + goto_model.goto_functions.function_map.at("g").body.instructions; + REQUIRE(g_instructions.begin()->is_assign()); + REQUIRE_FALSE(example_analysis[g_instructions.begin()].is_bottom()); + REQUIRE(*example_analysis[g_instructions.begin()].path_length == 100); + } + + THEN("The assignment in function 'h' should have a short path") + { + const auto &h_instructions = + goto_model.goto_functions.function_map.at("h").body.instructions; + REQUIRE(h_instructions.begin()->is_assign()); + REQUIRE_FALSE(example_analysis[h_instructions.begin()].is_bottom()); + REQUIRE(*example_analysis[h_instructions.begin()].path_length < 100); + } + } +}