diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index b0978465a3f..f211e7eb832 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -2,6 +2,8 @@ SRC = \ c_to_expr.cpp \ load_java_class.cpp \ require_expr.cpp \ + require_goto_statements.cpp \ + require_symbol.cpp \ require_type.cpp \ # Empty last line (please keep above list sorted!) diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f1eb485fd4e..f79e14f7c9b 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -26,6 +26,15 @@ symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path) +{ + return load_java_class( + java_class_name, class_path, new_java_bytecode_language()); +} + +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + std::unique_ptr java_lang) { // We don't expect the .class suffix to allow us to check the name of the // class @@ -39,8 +48,6 @@ symbol_tablet load_java_class( symbol_tablet new_symbol_table; - std::unique_ptrjava_lang(new_java_bytecode_language()); - std::istringstream java_code_stream("ignored"); null_message_handlert message_handler; diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index d81bb2f7636..c1c8ecd65cf 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -14,9 +14,16 @@ #define CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H #include +#include +#include symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path); +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + std::unique_ptr java_lang); + #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp new file mode 100644 index 00000000000..8881ad54666 --- /dev/null +++ b/unit/testing-utils/require_goto_statements.cpp @@ -0,0 +1,133 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include "require_goto_statements.h" +#include "catch.hpp" + +#include +#include + +/// Expand value of a function to include all child codets +/// \param function_value: The value of the function (e.g. got by looking up +/// the function in the symbol table and getting the value) +/// \return: All ID_code statements in the tree rooted at \p function_value +std::vector +require_goto_statements::get_all_statements(const exprt &function_value) +{ + std::vector statements; + for(auto sub_expression_it = function_value.depth_begin(); + sub_expression_it != function_value.depth_end(); + ++sub_expression_it) + { + if(sub_expression_it->id() == ID_code) + { + statements.push_back(to_code(*sub_expression_it)); + } + } + + return statements; +} + +/// Find assignment statements of the form \p structure_name.\component_name = +/// \param statements: The statements to look through +/// \param structure_name: The name of variable of type struct +/// \param component_name: The name of the component that should be assigned +/// \return: All the assignments to that component. +std::vector +require_goto_statements::find_struct_component_assignments( + const std::vector &statements, + const irep_idt &structure_name, + const irep_idt &component_name) +{ + std::vector component_assignments; + + for(const auto &assignment : statements) + { + if(assignment.get_statement() == ID_assign) + { + const code_assignt &code_assign = to_code_assign(assignment); + + if(code_assign.lhs().id() == ID_member) + { + const auto &member_expr = to_member_expr(code_assign.lhs()); + const auto &symbol = member_expr.symbol(); + + if( + symbol.get_identifier() == structure_name && + member_expr.get_component_name() == component_name) + { + component_assignments.push_back(code_assign); + } + } + } + } + return component_assignments; +} + +/// For a given variable name, gets the assignments to it in the provided +/// instructions. +/// \param pointer_name: The name of the variable +/// \param instructions: The instructions to look through +/// \return: A structure that contains the null assignment if found, and a +/// vector of all other assignments +require_goto_statements::pointer_assignment_locationt +require_goto_statements::find_pointer_assignments( + const irep_idt &pointer_name, + const std::vector &instructions) +{ + pointer_assignment_locationt locations; + for(const codet &statement : instructions) + { + if(statement.get_statement() == ID_assign) + { + const code_assignt &code_assign = to_code_assign(statement); + if( + code_assign.lhs().id() == ID_symbol && + to_symbol_expr(code_assign.lhs()).get_identifier() == pointer_name) + { + if( + code_assign.rhs() == + null_pointer_exprt(to_pointer_type(code_assign.lhs().type()))) + { + locations.null_assignment = code_assign; + } + else + { + locations.non_null_assignments.push_back(code_assign); + } + } + } + } + + return locations; +} + +/// Find the declaration of the specific variable. +/// \param variable_name: The name of the variable. +/// \param entry_point_instructions: The statements to look through +/// \return The declaration statement corresponding to that variable +/// \throws no_decl_found_exceptiont if no declaration of the specific +/// variable is found +const code_declt &require_goto_statements::require_declaration_of_name( + const irep_idt &variable_name, + const std::vector &entry_point_instructions) +{ + for(const auto &statement : entry_point_instructions) + { + if(statement.get_statement() == ID_decl) + { + const auto &decl_statement = to_code_decl(statement); + + if(decl_statement.get_identifier() == variable_name) + { + return decl_statement; + } + } + } + throw no_decl_found_exceptiont(variable_name.c_str()); +} diff --git a/unit/testing-utils/require_goto_statements.h b/unit/testing-utils/require_goto_statements.h new file mode 100644 index 00000000000..d55a96fde7c --- /dev/null +++ b/unit/testing-utils/require_goto_statements.h @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utilties for inspecting goto functions + +#include +#include +#include +#include +#include +#include + +#ifndef CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H +#define CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H + +// NOLINTNEXTLINE(readability/namespace) +namespace require_goto_statements +{ +struct pointer_assignment_locationt +{ + optionalt null_assignment; + std::vector non_null_assignments; +}; + +class no_decl_found_exceptiont : public std::exception +{ +public: + explicit no_decl_found_exceptiont(const std::string &var_name) + : _varname(var_name) + { + } + + virtual const char *what() const throw() + { + std::ostringstream stringStream; + stringStream << "Failed to find declaration for: " << _varname; + return stringStream.str().c_str(); + } + +private: + std::string _varname; +}; + +std::vector find_struct_component_assignments( + const std::vector &statements, + const irep_idt &structure_name, + const irep_idt &component_name); + +std::vector get_all_statements(const exprt &function_value); + +pointer_assignment_locationt find_pointer_assignments( + const irep_idt &pointer_name, + const std::vector &instructions); + +const code_declt &require_declaration_of_name( + const irep_idt &variable_name, + const std::vector &entry_point_instructions); +} + +#endif // CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H