From 2779399a9dce3bc1c205e4c864a252f0dc0e7f2b Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 10 Jul 2017 14:36:59 +0100 Subject: [PATCH 1/5] Correct unit Makefile to use OBJ rather than LIBS Previously the order of the libraries in LIB would effect whether the unit tests compiled. Use OBJ rather than LIBS to ensure the --start-group/--end-group flags are used in linking. Previously, if a file in CProver changed, though the libraries would be rebuilt, the unit tests wouldn't be relinked against the new library, meaning you would get out of date binaries. This change ensures that the link process is rerun if any of the libraries are rebuilt. Adding dependency to cprover libs for other unit executables --- unit/Makefile | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/unit/Makefile b/unit/Makefile index 0afe7916788..37955b07d0b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -15,19 +15,21 @@ include ../src/common cprover.dir: $(MAKE) $(MAKEARGS) -C ../src -LIBS += ../src/ansi-c/ansi-c$(LIBEXT) \ - ../src/cpp/cpp$(LIBEXT) \ - ../src/json/json$(LIBEXT) \ - ../src/linking/linking$(LIBEXT) \ - ../src/util/util$(LIBEXT) \ - ../src/big-int/big-int$(LIBEXT) \ - ../src/goto-programs/goto-programs$(LIBEXT) \ - ../src/pointer-analysis/pointer-analysis$(LIBEXT) \ - ../src/langapi/langapi$(LIBEXT) \ - ../src/assembler/assembler$(LIBEXT) \ - ../src/analyses/analyses$(LIBEXT) \ - ../src/solvers/solvers$(LIBEXT) \ - # Empty last line +CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ + ../src/cpp/cpp$(LIBEXT) \ + ../src/json/json$(LIBEXT) \ + ../src/linking/linking$(LIBEXT) \ + ../src/util/util$(LIBEXT) \ + ../src/big-int/big-int$(LIBEXT) \ + ../src/goto-programs/goto-programs$(LIBEXT) \ + ../src/pointer-analysis/pointer-analysis$(LIBEXT) \ + ../src/langapi/langapi$(LIBEXT) \ + ../src/assembler/assembler$(LIBEXT) \ + ../src/analyses/analyses$(LIBEXT) \ + ../src/solvers/solvers$(LIBEXT) \ + # Empty last line + +OBJ += $(CPROVER_LIBS) TESTS = unit_tests$(EXEEXT) \ miniBDD$(EXEEXT) \ @@ -49,11 +51,11 @@ test: all unit_tests$(EXEEXT): $(OBJ) $(LINKBIN) -miniBDD$(EXEEXT): miniBDD$(OBJEXT) +miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS) $(LINKBIN) -string_utils$(EXEEXT): string_utils$(OBJEXT) +string_utils$(EXEEXT): string_utils$(OBJEXT) $(CPROVER_LIBS) $(LINKBIN) -sharing_node$(EXEEXT): sharing_node$(OBJEXT) +sharing_node$(EXEEXT): sharing_node$(OBJEXT) $(CPROVER_LIBS) $(LINKBIN) From b5c55b3e5e9da250b2f067aa90ead365645b5b9b Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 10 Jul 2017 13:52:32 +0100 Subject: [PATCH 2/5] Added utility functions for checking expressions Use namespace rather than class with static functions as more semantically correct. --- unit/Makefile | 15 ++++--- unit/src/expr/require_expr.cpp | 76 ++++++++++++++++++++++++++++++++++ unit/src/expr/require_expr.h | 33 +++++++++++++++ 3 files changed, 119 insertions(+), 5 deletions(-) create mode 100644 unit/src/expr/require_expr.cpp create mode 100644 unit/src/expr/require_expr.h diff --git a/unit/Makefile b/unit/Makefile index 37955b07d0b..6e4e5dfa9d5 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,12 +1,17 @@ .PHONY: all cprover.dir test -SRC = unit_tests.cpp \ - analyses/does_remove_const/does_expr_lose_const.cpp \ - analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ - analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ - catch_example.cpp \ +# Source files for test utilities +SRC = src/expr/require_expr.cpp \ # Empty last line +# Test source files +SRC += unit_tests.cpp \ + analyses/does_remove_const/does_expr_lose_const.cpp \ + analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ + analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ + catch_example.cpp \ + # Empty last line + INCLUDES= -I ../src/ -I. include ../src/config.inc diff --git a/unit/src/expr/require_expr.cpp b/unit/src/expr/require_expr.cpp new file mode 100644 index 00000000000..e81b5a2d70a --- /dev/null +++ b/unit/src/expr/require_expr.cpp @@ -0,0 +1,76 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Helper functions for requiring specific expressions +/// If the expression is of the wrong type, throw a CATCH exception +/// Also checks associated properties and returns a casted version of the +/// expression. + +#include "require_expr.h" + +#include +#include + +/// Verify a given exprt is an index_exprt with a a constant value equal to the +/// expected value +/// \param expr: The expression. +/// \param expected_index: The constant value that should be the index. +/// \return The expr cast to an index_exprt +index_exprt require_expr::require_index(const exprt &expr, int expected_index) +{ + REQUIRE(expr.id()==ID_index); + const index_exprt &index_expr=to_index_expr(expr); + REQUIRE(index_expr.index().id()==ID_constant); + const constant_exprt &index_value=to_constant_expr(index_expr.index()); + mp_integer index_integer_value; + to_integer(index_value, index_integer_value); + REQUIRE(index_integer_value==expected_index); + + return index_expr; +} + +/// Verify a given exprt is an index_exprt with a nil value as its index +/// \param expr: The expression. +/// \return The expr cast to an index_exprt +index_exprt require_expr::require_top_index(const exprt &expr) +{ + REQUIRE(expr.id()==ID_index); + const index_exprt &index_expr=to_index_expr(expr); + REQUIRE(index_expr.index().id()==ID_nil); + return index_expr; +} + +/// Verify a given exprt is an member_exprt with a component name equal to the +/// component_identifier +/// \param expr: The expression. +/// \param component_identifier: The name of the component that should be being +/// accessed. +/// \return The expr cast to a member_exprt. +member_exprt require_expr::require_member( + const exprt &expr, const irep_idt &component_identifier) +{ + REQUIRE(expr.id()==ID_member); + const member_exprt &member_expr=to_member_expr(expr); + REQUIRE(member_expr.get_component_name()==component_identifier); + return member_expr; +} + +/// Verify a given exprt is an symbol_exprt with a identifier name equal to the +/// symbol_name. +/// \param expr: The expression. +/// \param symbol_name: The intended identifier of the symbol +/// \return The expr cast to a symbol_exprt +symbol_exprt require_expr::require_symbol( + const exprt &expr, const irep_idt &symbol_name) +{ + REQUIRE(expr.id()==ID_symbol); + const symbol_exprt &symbol_expr=to_symbol_expr(expr); + REQUIRE(symbol_expr.get_identifier()==symbol_name); + return symbol_expr; +} diff --git a/unit/src/expr/require_expr.h b/unit/src/expr/require_expr.h new file mode 100644 index 00000000000..83bdad2132d --- /dev/null +++ b/unit/src/expr/require_expr.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Helper functions for requiring specific expressions +/// If the expression is of the wrong type, throw a CATCH exception +/// Also checks associated properties and returns a casted version of the +/// expression. + +#ifndef CPROVER_SRC_EXPR_REQUIRE_EXPR_H +#define CPROVER_SRC_EXPR_REQUIRE_EXPR_H + +#include + +// NOLINTNEXTLINE(readability/namespace) +namespace require_expr +{ + index_exprt require_index(const exprt &expr, int expected_index); + index_exprt require_top_index(const exprt &expr); + + member_exprt require_member( + const exprt &expr, const irep_idt &component_identifier); + + symbol_exprt require_symbol( + const exprt &expr, const irep_idt &symbol_name); +} + +#endif // CPROVER_SRC_EXPR_REQUIRE_EXPR_H From 00477334210a76ae76f54ca6befc4e8748831bd1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 10 Jul 2017 13:54:26 +0100 Subject: [PATCH 3/5] Adding pretty printer to main file --- unit/unit_tests.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/unit/unit_tests.cpp b/unit/unit_tests.cpp index a4ae333109f..8d007b83696 100644 --- a/unit/unit_tests.cpp +++ b/unit/unit_tests.cpp @@ -8,3 +8,11 @@ #define CATCH_CONFIG_MAIN #include "catch.hpp" +#include + +// Debug printer for irept +std::ostream &operator<<(std::ostream &os, const irept &value) +{ + os << value.pretty(); + return os; +} From 318502880f3876d153c56d049153f45154c9764d Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 10 Jul 2017 14:11:44 +0100 Subject: [PATCH 4/5] Added utility class to convert strings into expressions In turns the error return state into a CATCH exception so the test will fail without cluttering tests with checks on the flag when it is just setup code for the actual test. --- unit/Makefile | 1 + unit/src/ansi-c/c_to_expr.cpp | 35 +++++++++++++++++++++++++++++++++++ unit/src/ansi-c/c_to_expr.h | 35 +++++++++++++++++++++++++++++++++++ 3 files changed, 71 insertions(+) create mode 100644 unit/src/ansi-c/c_to_expr.cpp create mode 100644 unit/src/ansi-c/c_to_expr.h diff --git a/unit/Makefile b/unit/Makefile index 6e4e5dfa9d5..f329e489773 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -2,6 +2,7 @@ # Source files for test utilities SRC = src/expr/require_expr.cpp \ + src/ansi-c/c_to_expr.cpp \ # Empty last line # Test source files diff --git a/unit/src/ansi-c/c_to_expr.cpp b/unit/src/ansi-c/c_to_expr.cpp new file mode 100644 index 00000000000..bb71d5fabb1 --- /dev/null +++ b/unit/src/ansi-c/c_to_expr.cpp @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utility for converting strings in to exprt, throwing a CATCH exception +/// if this fails in any way. +/// +#include "c_to_expr.h" + +#include + +c_to_exprt::c_to_exprt(): + message_handler( + std::unique_ptr(new ui_message_handlert())) +{ + language.set_message_handler(*message_handler); +} + +/// Take an input string that should be a valid C rhs expression +/// \param input_string: The string to convert +/// \param ns: The global namespace +/// \return: A constructed expr representing the string +exprt c_to_exprt::operator()( + const std::string &input_string, const namespacet &ns) +{ + exprt expr; + bool result=language.to_expr(input_string, "", expr, ns); + REQUIRE(!result); + return expr; +} diff --git a/unit/src/ansi-c/c_to_expr.h b/unit/src/ansi-c/c_to_expr.h new file mode 100644 index 00000000000..dcaf0b0d1b7 --- /dev/null +++ b/unit/src/ansi-c/c_to_expr.h @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utility for converting strings in to exprt, throwing a CATCH exception +/// if this fails in any way. + +#ifndef CPROVER_SRC_ANSI_C_C_TO_EXPR_H +#define CPROVER_SRC_ANSI_C_C_TO_EXPR_H + +#include + +#include +#include +#include +#include +#include + +class c_to_exprt +{ +public: + c_to_exprt(); + exprt operator()(const std::string &input_string, const namespacet &ns); + +private: + std::unique_ptr message_handler; + ansi_c_languaget language; +}; + +#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H From e3f8d4aa2bbad999c3d64d9fb98c47922aa8e374 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 10 Jul 2017 16:54:44 +0100 Subject: [PATCH 5/5] Added constructor to auxilary symbol instead of a helper function The auxilary function had the same flags requried for the test, so added a utility constructor that allows specifying of name and type. --- src/util/symbol.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/symbol.h b/src/util/symbol.h index 5c9240c1dd7..7edae3146c0 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -145,6 +145,14 @@ class auxiliary_symbolt:public symbolt is_file_local=true; is_auxiliary=true; } + + auxiliary_symbolt(const irep_idt &name, const typet &type): + auxiliary_symbolt() + { + this->name=name; + this->base_name=name; + this->type=type; + } }; /*! \brief Symbol table entry of function parameter