From 2c175bdbd9714a9aaf04426a315812e1cb0403e7 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 23 Oct 2017 15:06:21 +0100 Subject: [PATCH 01/10] Update load_java_class to construct the entry point function Take a language as a parameter to allow customisation on which language is used --- unit/testing-utils/load_java_class.cpp | 11 +++++++++-- unit/testing-utils/load_java_class.h | 7 +++++++ 2 files changed, 16 insertions(+), 2 deletions(-) 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 From b9914a810a9b37d0d28deee2cfdb0ad8ddaa829c Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 1 Nov 2017 17:38:06 +0000 Subject: [PATCH 02/10] Add some java testing utilities. --- unit/testing-utils/java_testing_utils.cpp | 222 ++++++++++++++++++++++ unit/testing-utils/java_testing_utils.h | 65 +++++++ 2 files changed, 287 insertions(+) create mode 100644 unit/testing-utils/java_testing_utils.cpp create mode 100644 unit/testing-utils/java_testing_utils.h diff --git a/unit/testing-utils/java_testing_utils.cpp b/unit/testing-utils/java_testing_utils.cpp new file mode 100644 index 00000000000..f5bd5a4cd2b --- /dev/null +++ b/unit/testing-utils/java_testing_utils.cpp @@ -0,0 +1,222 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include "java_testing_utils.h" + +struct_component_assignment_locationt combine_locations( + const struct_component_assignment_locationt &a, + const struct_component_assignment_locationt &b) +{ + struct_component_assignment_locationt new_locations; + + new_locations.assignment_locations.insert( + new_locations.assignment_locations.end(), + a.assignment_locations.begin(), + a.assignment_locations.end()); + + new_locations.assignment_locations.insert( + new_locations.assignment_locations.end(), + b.assignment_locations.begin(), + b.assignment_locations.end()); + + return new_locations; +} + +struct_component_assignment_locationt find_struct_component_assignments( + const exprt::operandst &entry_point_instructions, + const irep_idt &structure_name, + const irep_idt &component_name) +{ + struct_component_assignment_locationt component_assignments; + + for(const auto &instruction : entry_point_instructions) + { + const codet &assignment = to_code(instruction); + INVARIANT(instruction.id() == ID_code, "All instructions must be code"); + 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.assignment_locations.push_back(code_assign); + } + } + } + else if(assignment.get_statement() == ID_block) + { + const auto &assignments_in_block = find_struct_component_assignments( + assignment.operands(), structure_name, component_name); + component_assignments = + combine_locations(component_assignments, assignments_in_block); + } + else if(assignment.get_statement() == ID_ifthenelse) + { + const code_ifthenelset &if_else_block = + to_code_ifthenelse(to_code(assignment)); + const auto &assignments_in_block = find_struct_component_assignments( + exprt::operandst{if_else_block.then_case()}, + structure_name, + component_name); + component_assignments = + combine_locations(component_assignments, assignments_in_block); + + if(if_else_block.has_else_case()) + { + const auto &assignments_in_else = find_struct_component_assignments( + exprt::operandst{if_else_block.else_case()}, + structure_name, + component_name); + component_assignments = + combine_locations(component_assignments, assignments_in_else); + } + } + else if(assignment.get_statement() == ID_label) + { + const code_labelt &label_statement = to_code_label(assignment); + const auto &assignments_in_label = find_struct_component_assignments( + exprt::operandst{label_statement.code()}, + structure_name, + component_name); + component_assignments = + combine_locations(component_assignments, assignments_in_label); + } + } + return component_assignments; +} + +/// Combine two pointer locations. Takes the null assignment if present in +/// either (fails if present in both) and appends the non-null assignments +/// \param a: The first set of assignments +/// \param b: The second set of assignments +/// \return The resulting assignment +pointer_assignment_locationt combine_locations( + const pointer_assignment_locationt &a, + const pointer_assignment_locationt &b) +{ + pointer_assignment_locationt new_locations; + if(a.null_assignment.has_value()) + { + INVARIANT( + !b.null_assignment.has_value(), "Only expected one assignment to null"); + new_locations.null_assignment = a.null_assignment; + } + else if(b.null_assignment.has_value()) + { + INVARIANT( + !a.null_assignment.has_value(), "Only expected one assignment to null"); + new_locations.null_assignment = b.null_assignment; + } + + new_locations.non_null_assignments.insert( + new_locations.non_null_assignments.end(), + a.non_null_assignments.begin(), + a.non_null_assignments.end()); + + new_locations.non_null_assignments.insert( + new_locations.non_null_assignments.end(), + b.non_null_assignments.begin(), + b.non_null_assignments.end()); + + return new_locations; +} + +/// For a given variable name, gets the assignments to it in the functions +/// \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 +pointer_assignment_locationt find_pointer_assignments( + const irep_idt &pointer_name, + const exprt::operandst &instructions) +{ + pointer_assignment_locationt locations; + for(const exprt &assignment : instructions) + { + const codet &statement = to_code(assignment); + INVARIANT(assignment.id() == ID_code, "All instructions must be code"); + if(statement.get_statement() == ID_assign) + { + const code_assignt &code_assign = to_code_assign(to_code(assignment)); + 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); + } + } + } + else if(statement.get_statement() == ID_block) + { + const auto &assignments_in_block = + find_pointer_assignments(pointer_name, assignment.operands()); + locations = combine_locations(locations, assignments_in_block); + } + else if(statement.get_statement() == ID_ifthenelse) + { + const code_ifthenelset &if_else_block = + to_code_ifthenelse(to_code(assignment)); + const auto &assignments_in_block = find_pointer_assignments( + pointer_name, exprt::operandst{if_else_block.then_case()}); + locations = combine_locations(locations, assignments_in_block); + + if(if_else_block.has_else_case()) + { + const auto &assignments_in_else = find_pointer_assignments( + pointer_name, exprt::operandst{if_else_block.else_case()}); + locations = combine_locations(locations, assignments_in_else); + } + } + else if(statement.get_statement() == ID_label) + { + const code_labelt &label_statement = to_code_label(statement); + const auto &assignments_in_label = find_pointer_assignments( + pointer_name, exprt::operandst{label_statement.code()}); + locations = combine_locations(locations, assignments_in_label); + } + } + + return locations; +} + +const exprt &find_declaration_by_name( + const irep_idt &variable_name, + const exprt::operandst &entry_point_instructions) +{ + for(const auto &instruction : entry_point_instructions) + { + const codet &statement = to_code(instruction); + INVARIANT(instruction.id() == ID_code, "All instructions must be code"); + if(statement.get_statement() == ID_decl) + { + const auto &decl_statement = to_code_decl(statement); + + if(decl_statement.get_identifier() == variable_name) + { + return instruction; + } + } + } + throw no_decl_found_exception(variable_name.c_str()); +} \ No newline at end of file diff --git a/unit/testing-utils/java_testing_utils.h b/unit/testing-utils/java_testing_utils.h new file mode 100644 index 00000000000..3845c8c37b9 --- /dev/null +++ b/unit/testing-utils/java_testing_utils.h @@ -0,0 +1,65 @@ +/*******************************************************************\ + + 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_CHECK_GOTO_FUNCTIONS_H +#define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H + +class no_decl_found_exception : public std::exception +{ +public: + explicit no_decl_found_exception(const std::string &varname) + : _varname(varname) + { + } + + 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; +}; + +struct struct_component_assignment_locationt +{ + std::vector assignment_locations; +}; + +struct_component_assignment_locationt find_struct_component_assignments( + const exprt::operandst &entry_point_instructions, + const irep_idt &structure_name, + const irep_idt &component_name); + +struct pointer_assignment_locationt +{ + optionalt null_assignment; + std::vector non_null_assignments; +}; + +pointer_assignment_locationt find_pointer_assignments( + const irep_idt &pointer_name, + const exprt::operandst &instructions); + +const exprt &find_declaration_by_name( + const irep_idt &variable_name, + const exprt::operandst &entry_point_instructions); + +#endif //TEST_GEN_SUPERBUILD_JAVA_TESTING_UTILS_H From b96199f0e92faa7358554699982078d2fbc42f9b Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 1 Nov 2017 16:17:44 +0000 Subject: [PATCH 03/10] Moved and simplified the code for finding sub statements Rather than explicitly traversing code statements in each helper function, introduce an additional function that allows prepassing a function into all of the statements including substatements --- unit/testing-utils/java_testing_utils.cpp | 180 ++++++---------------- unit/testing-utils/java_testing_utils.h | 15 +- 2 files changed, 49 insertions(+), 146 deletions(-) diff --git a/unit/testing-utils/java_testing_utils.cpp b/unit/testing-utils/java_testing_utils.cpp index f5bd5a4cd2b..e313ee17420 100644 --- a/unit/testing-utils/java_testing_utils.cpp +++ b/unit/testing-utils/java_testing_utils.cpp @@ -6,39 +6,51 @@ \*******************************************************************/ -#include #include "java_testing_utils.h" -struct_component_assignment_locationt combine_locations( - const struct_component_assignment_locationt &a, - const struct_component_assignment_locationt &b) -{ - struct_component_assignment_locationt new_locations; - - new_locations.assignment_locations.insert( - new_locations.assignment_locations.end(), - a.assignment_locations.begin(), - a.assignment_locations.end()); - - new_locations.assignment_locations.insert( - new_locations.assignment_locations.end(), - b.assignment_locations.begin(), - b.assignment_locations.end()); +#include +#include - return new_locations; +std::vector get_all_statements(const exprt::operandst &instructions) +{ + std::vector statements; + for(const exprt &instruction : instructions) + { + // Add the statement + statements.push_back(to_code(instruction)); + + // Add any child statements (e.g. if this is a code_block + // TODO(tkiley): It should be possible to have a custom version of + // TODO(tkiley): back_inserter that also transforms to codet, but I don't + // TODO(tkiley): know how to do this + std::vector sub_expr; + std::copy_if( + instruction.depth_begin(), + instruction.depth_end(), + std::back_inserter(sub_expr), + [](const exprt &sub_statement) { + // Get all codet + return sub_statement.id() == ID_code; + }); + + std::transform( + sub_expr.begin(), + sub_expr.end(), + std::back_inserter(statements), + [](const exprt &sub_expr) { return to_code(sub_expr); }); + } + return statements; } -struct_component_assignment_locationt find_struct_component_assignments( - const exprt::operandst &entry_point_instructions, +std::vector find_struct_component_assignments( + const std::vector &statements, const irep_idt &structure_name, const irep_idt &component_name) { - struct_component_assignment_locationt component_assignments; + std::vector component_assignments; - for(const auto &instruction : entry_point_instructions) + for(const auto &assignment : statements) { - const codet &assignment = to_code(instruction); - INVARIANT(instruction.id() == ID_code, "All instructions must be code"); if(assignment.get_statement() == ID_assign) { const code_assignt &code_assign = to_code_assign(assignment); @@ -52,88 +64,14 @@ struct_component_assignment_locationt find_struct_component_assignments( symbol.get_identifier() == structure_name && member_expr.get_component_name() == component_name) { - component_assignments.assignment_locations.push_back(code_assign); + component_assignments.push_back(code_assign); } } } - else if(assignment.get_statement() == ID_block) - { - const auto &assignments_in_block = find_struct_component_assignments( - assignment.operands(), structure_name, component_name); - component_assignments = - combine_locations(component_assignments, assignments_in_block); - } - else if(assignment.get_statement() == ID_ifthenelse) - { - const code_ifthenelset &if_else_block = - to_code_ifthenelse(to_code(assignment)); - const auto &assignments_in_block = find_struct_component_assignments( - exprt::operandst{if_else_block.then_case()}, - structure_name, - component_name); - component_assignments = - combine_locations(component_assignments, assignments_in_block); - - if(if_else_block.has_else_case()) - { - const auto &assignments_in_else = find_struct_component_assignments( - exprt::operandst{if_else_block.else_case()}, - structure_name, - component_name); - component_assignments = - combine_locations(component_assignments, assignments_in_else); - } - } - else if(assignment.get_statement() == ID_label) - { - const code_labelt &label_statement = to_code_label(assignment); - const auto &assignments_in_label = find_struct_component_assignments( - exprt::operandst{label_statement.code()}, - structure_name, - component_name); - component_assignments = - combine_locations(component_assignments, assignments_in_label); - } } return component_assignments; } -/// Combine two pointer locations. Takes the null assignment if present in -/// either (fails if present in both) and appends the non-null assignments -/// \param a: The first set of assignments -/// \param b: The second set of assignments -/// \return The resulting assignment -pointer_assignment_locationt combine_locations( - const pointer_assignment_locationt &a, - const pointer_assignment_locationt &b) -{ - pointer_assignment_locationt new_locations; - if(a.null_assignment.has_value()) - { - INVARIANT( - !b.null_assignment.has_value(), "Only expected one assignment to null"); - new_locations.null_assignment = a.null_assignment; - } - else if(b.null_assignment.has_value()) - { - INVARIANT( - !a.null_assignment.has_value(), "Only expected one assignment to null"); - new_locations.null_assignment = b.null_assignment; - } - - new_locations.non_null_assignments.insert( - new_locations.non_null_assignments.end(), - a.non_null_assignments.begin(), - a.non_null_assignments.end()); - - new_locations.non_null_assignments.insert( - new_locations.non_null_assignments.end(), - b.non_null_assignments.begin(), - b.non_null_assignments.end()); - - return new_locations; -} - /// For a given variable name, gets the assignments to it in the functions /// \param pointer_name: The name of the variable /// \param instructions: The instructions to look through @@ -141,16 +79,14 @@ pointer_assignment_locationt combine_locations( /// vector of all other assignments pointer_assignment_locationt find_pointer_assignments( const irep_idt &pointer_name, - const exprt::operandst &instructions) + const std::vector &instructions) { pointer_assignment_locationt locations; - for(const exprt &assignment : instructions) + for(const codet &statement : instructions) { - const codet &statement = to_code(assignment); - INVARIANT(assignment.id() == ID_code, "All instructions must be code"); if(statement.get_statement() == ID_assign) { - const code_assignt &code_assign = to_code_assign(to_code(assignment)); + 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) @@ -167,34 +103,6 @@ pointer_assignment_locationt find_pointer_assignments( } } } - else if(statement.get_statement() == ID_block) - { - const auto &assignments_in_block = - find_pointer_assignments(pointer_name, assignment.operands()); - locations = combine_locations(locations, assignments_in_block); - } - else if(statement.get_statement() == ID_ifthenelse) - { - const code_ifthenelset &if_else_block = - to_code_ifthenelse(to_code(assignment)); - const auto &assignments_in_block = find_pointer_assignments( - pointer_name, exprt::operandst{if_else_block.then_case()}); - locations = combine_locations(locations, assignments_in_block); - - if(if_else_block.has_else_case()) - { - const auto &assignments_in_else = find_pointer_assignments( - pointer_name, exprt::operandst{if_else_block.else_case()}); - locations = combine_locations(locations, assignments_in_else); - } - } - else if(statement.get_statement() == ID_label) - { - const code_labelt &label_statement = to_code_label(statement); - const auto &assignments_in_label = find_pointer_assignments( - pointer_name, exprt::operandst{label_statement.code()}); - locations = combine_locations(locations, assignments_in_label); - } } return locations; @@ -202,21 +110,19 @@ pointer_assignment_locationt find_pointer_assignments( const exprt &find_declaration_by_name( const irep_idt &variable_name, - const exprt::operandst &entry_point_instructions) + const std::vector &entry_point_instructions) { - for(const auto &instruction : entry_point_instructions) + for(const auto &statement : entry_point_instructions) { - const codet &statement = to_code(instruction); - INVARIANT(instruction.id() == ID_code, "All instructions must be code"); if(statement.get_statement() == ID_decl) { const auto &decl_statement = to_code_decl(statement); if(decl_statement.get_identifier() == variable_name) { - return instruction; + return statement; } } } throw no_decl_found_exception(variable_name.c_str()); -} \ No newline at end of file +} diff --git a/unit/testing-utils/java_testing_utils.h b/unit/testing-utils/java_testing_utils.h index 3845c8c37b9..91327a5c09f 100644 --- a/unit/testing-utils/java_testing_utils.h +++ b/unit/testing-utils/java_testing_utils.h @@ -38,13 +38,8 @@ class no_decl_found_exception : public std::exception std::string _varname; }; -struct struct_component_assignment_locationt -{ - std::vector assignment_locations; -}; - -struct_component_assignment_locationt find_struct_component_assignments( - const exprt::operandst &entry_point_instructions, +std::vector find_struct_component_assignments( + const std::vector &statements, const irep_idt &structure_name, const irep_idt &component_name); @@ -54,12 +49,14 @@ struct pointer_assignment_locationt std::vector non_null_assignments; }; +std::vector get_all_statements(const exprt::operandst &instructions); + pointer_assignment_locationt find_pointer_assignments( const irep_idt &pointer_name, - const exprt::operandst &instructions); + const std::vector &instructions); const exprt &find_declaration_by_name( const irep_idt &variable_name, - const exprt::operandst &entry_point_instructions); + const std::vector &entry_point_instructions); #endif //TEST_GEN_SUPERBUILD_JAVA_TESTING_UTILS_H From a657ec1398538d0e2f007fc691821084fcd5c4eb Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 1 Nov 2017 16:37:55 +0000 Subject: [PATCH 04/10] Moved functions into a namespace and documented them Also tightened up the typess of returns and inputs. Also refactored get_all_statements to just take the root of the tree, rather than a vector of roots. --- unit/testing-utils/java_testing_utils.cpp | 72 +++++++++++++---------- unit/testing-utils/java_testing_utils.h | 7 ++- 2 files changed, 47 insertions(+), 32 deletions(-) diff --git a/unit/testing-utils/java_testing_utils.cpp b/unit/testing-utils/java_testing_utils.cpp index e313ee17420..63802ca25ad 100644 --- a/unit/testing-utils/java_testing_utils.cpp +++ b/unit/testing-utils/java_testing_utils.cpp @@ -11,38 +11,45 @@ #include #include -std::vector get_all_statements(const exprt::operandst &instructions) +/// Expand value of a function to include all child codets +/// \param instructions: 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(const exprt &instruction : instructions) - { - // Add the statement - statements.push_back(to_code(instruction)); - - // Add any child statements (e.g. if this is a code_block - // TODO(tkiley): It should be possible to have a custom version of - // TODO(tkiley): back_inserter that also transforms to codet, but I don't - // TODO(tkiley): know how to do this - std::vector sub_expr; - std::copy_if( - instruction.depth_begin(), - instruction.depth_end(), - std::back_inserter(sub_expr), - [](const exprt &sub_statement) { - // Get all codet - return sub_statement.id() == ID_code; - }); - - std::transform( - sub_expr.begin(), - sub_expr.end(), - std::back_inserter(statements), - [](const exprt &sub_expr) { return to_code(sub_expr); }); - } + + // Add any child statements (e.g. if this is a code_block + // TODO(tkiley): It should be possible to have a custom version of + // TODO(tkiley): back_inserter that also transforms to codet, but I don't + // TODO(tkiley): know how to do this + std::vector sub_expr; + std::copy_if( + function_value.depth_begin(), + function_value.depth_end(), + std::back_inserter(sub_expr), + [](const exprt &sub_statement) { + // Get all codet + return sub_statement.id() == ID_code; + }); + + std::transform( + sub_expr.begin(), + sub_expr.end(), + std::back_inserter(statements), + [](const exprt &sub_expr) { return to_code(sub_expr); }); + return statements; } -std::vector find_struct_component_assignments( +/// 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) @@ -77,7 +84,8 @@ std::vector find_struct_component_assignments( /// \param instructions: The instructions to look through /// \return: A structure that contains the null assignment if found, and a /// vector of all other assignments -pointer_assignment_locationt find_pointer_assignments( +require_goto_statements::pointer_assignment_locationt +require_goto_statements::find_pointer_assignments( const irep_idt &pointer_name, const std::vector &instructions) { @@ -108,7 +116,11 @@ pointer_assignment_locationt find_pointer_assignments( return locations; } -const exprt &find_declaration_by_name( +/// 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 +const code_declt &require_goto_statements::find_declaration_by_name( const irep_idt &variable_name, const std::vector &entry_point_instructions) { @@ -120,7 +132,7 @@ const exprt &find_declaration_by_name( if(decl_statement.get_identifier() == variable_name) { - return statement; + return decl_statement; } } } diff --git a/unit/testing-utils/java_testing_utils.h b/unit/testing-utils/java_testing_utils.h index 91327a5c09f..8412226b81e 100644 --- a/unit/testing-utils/java_testing_utils.h +++ b/unit/testing-utils/java_testing_utils.h @@ -38,6 +38,8 @@ class no_decl_found_exception : public std::exception std::string _varname; }; +namespace require_goto_statements +{ std::vector find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, @@ -49,14 +51,15 @@ struct pointer_assignment_locationt std::vector non_null_assignments; }; -std::vector get_all_statements(const exprt::operandst &instructions); +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 exprt &find_declaration_by_name( +const code_declt &find_declaration_by_name( const irep_idt &variable_name, const std::vector &entry_point_instructions); +} #endif //TEST_GEN_SUPERBUILD_JAVA_TESTING_UTILS_H From fa14b47d74ec446b6ca60c36947d6eda5896e6da Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 1 Nov 2017 16:52:32 +0000 Subject: [PATCH 05/10] Renamed utility file to require_goto_statements --- .../{java_testing_utils.cpp => require_goto_statements.cpp} | 2 +- .../{java_testing_utils.h => require_goto_statements.h} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename unit/testing-utils/{java_testing_utils.cpp => require_goto_statements.cpp} (99%) rename unit/testing-utils/{java_testing_utils.h => require_goto_statements.h} (100%) diff --git a/unit/testing-utils/java_testing_utils.cpp b/unit/testing-utils/require_goto_statements.cpp similarity index 99% rename from unit/testing-utils/java_testing_utils.cpp rename to unit/testing-utils/require_goto_statements.cpp index 63802ca25ad..7ccd00a555a 100644 --- a/unit/testing-utils/java_testing_utils.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -6,7 +6,7 @@ \*******************************************************************/ -#include "java_testing_utils.h" +#include "require_goto_statements.h" #include #include diff --git a/unit/testing-utils/java_testing_utils.h b/unit/testing-utils/require_goto_statements.h similarity index 100% rename from unit/testing-utils/java_testing_utils.h rename to unit/testing-utils/require_goto_statements.h From e67d22976b23d897bc670b523610c0c28a3e07f2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 1 Nov 2017 16:59:17 +0000 Subject: [PATCH 06/10] Renamed find declaration method To be more consistent, renamed to require rather than find since it throws if the declaration is not found --- unit/testing-utils/require_goto_statements.cpp | 3 ++- unit/testing-utils/require_goto_statements.h | 18 +++++++++--------- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp index 7ccd00a555a..a5da0c29eaa 100644 --- a/unit/testing-utils/require_goto_statements.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -7,6 +7,7 @@ \*******************************************************************/ #include "require_goto_statements.h" +#include "catch.hpp" #include #include @@ -120,7 +121,7 @@ require_goto_statements::find_pointer_assignments( /// \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 -const code_declt &require_goto_statements::find_declaration_by_name( +const code_declt &require_goto_statements::require_declaration_of_name( const irep_idt &variable_name, const std::vector &entry_point_instructions) { diff --git a/unit/testing-utils/require_goto_statements.h b/unit/testing-utils/require_goto_statements.h index 8412226b81e..18c501d684f 100644 --- a/unit/testing-utils/require_goto_statements.h +++ b/unit/testing-utils/require_goto_statements.h @@ -19,6 +19,14 @@ #ifndef CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H #define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H +namespace require_goto_statements +{ +struct pointer_assignment_locationt +{ + optionalt null_assignment; + std::vector non_null_assignments; +}; + class no_decl_found_exception : public std::exception { public: @@ -38,26 +46,18 @@ class no_decl_found_exception : public std::exception std::string _varname; }; -namespace require_goto_statements -{ std::vector find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, const irep_idt &component_name); -struct pointer_assignment_locationt -{ - optionalt null_assignment; - std::vector non_null_assignments; -}; - 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 &find_declaration_by_name( +const code_declt &require_declaration_of_name( const irep_idt &variable_name, const std::vector &entry_point_instructions); } From 25d765be37a713d06332b6c4cf6146dc22be6d6f Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 09:49:12 +0000 Subject: [PATCH 07/10] Use a for loop rather than chained algorithms --- .../testing-utils/require_goto_statements.cpp | 29 ++++++------------- 1 file changed, 9 insertions(+), 20 deletions(-) diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp index a5da0c29eaa..44aba8194e6 100644 --- a/unit/testing-utils/require_goto_statements.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -20,26 +20,15 @@ std::vector require_goto_statements::get_all_statements(const exprt &function_value) { std::vector statements; - - // Add any child statements (e.g. if this is a code_block - // TODO(tkiley): It should be possible to have a custom version of - // TODO(tkiley): back_inserter that also transforms to codet, but I don't - // TODO(tkiley): know how to do this - std::vector sub_expr; - std::copy_if( - function_value.depth_begin(), - function_value.depth_end(), - std::back_inserter(sub_expr), - [](const exprt &sub_statement) { - // Get all codet - return sub_statement.id() == ID_code; - }); - - std::transform( - sub_expr.begin(), - sub_expr.end(), - std::back_inserter(statements), - [](const exprt &sub_expr) { return to_code(sub_expr); }); + 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; } From 7938bacd987fed81c06f7218a97a6fca7ee54d22 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 09:56:03 +0000 Subject: [PATCH 08/10] Correcting linting errors --- unit/testing-utils/require_goto_statements.cpp | 2 +- unit/testing-utils/require_goto_statements.h | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp index 44aba8194e6..46fadab3a7a 100644 --- a/unit/testing-utils/require_goto_statements.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -126,5 +126,5 @@ const code_declt &require_goto_statements::require_declaration_of_name( } } } - throw no_decl_found_exception(variable_name.c_str()); + 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 index 18c501d684f..d55a96fde7c 100644 --- a/unit/testing-utils/require_goto_statements.h +++ b/unit/testing-utils/require_goto_statements.h @@ -16,9 +16,10 @@ #include #include -#ifndef CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H -#define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H +#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 @@ -27,11 +28,11 @@ struct pointer_assignment_locationt std::vector non_null_assignments; }; -class no_decl_found_exception : public std::exception +class no_decl_found_exceptiont : public std::exception { public: - explicit no_decl_found_exception(const std::string &varname) - : _varname(varname) + explicit no_decl_found_exceptiont(const std::string &var_name) + : _varname(var_name) { } @@ -62,4 +63,4 @@ const code_declt &require_declaration_of_name( const std::vector &entry_point_instructions); } -#endif //TEST_GEN_SUPERBUILD_JAVA_TESTING_UTILS_H +#endif // CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H From 455067643536cb254ff2c546da502a8182b8315e Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 11:22:34 +0000 Subject: [PATCH 09/10] Added missing utilities to the Makefile --- unit/testing-utils/Makefile | 2 ++ 1 file changed, 2 insertions(+) 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!) From 9cb456929a93c540032f5389ad10ebe593927f4b Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 16:51:33 +0000 Subject: [PATCH 10/10] Amend doxygen comments --- unit/testing-utils/require_goto_statements.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp index 46fadab3a7a..8881ad54666 100644 --- a/unit/testing-utils/require_goto_statements.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -13,7 +13,7 @@ #include /// Expand value of a function to include all child codets -/// \param instructions: The value of the function (e.g. got by looking up +/// \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 @@ -69,7 +69,8 @@ require_goto_statements::find_struct_component_assignments( return component_assignments; } -/// For a given variable name, gets the assignments to it in the functions +/// 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 @@ -110,6 +111,8 @@ require_goto_statements::find_pointer_assignments( /// \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)