Merge pull request #1111 from thk123/feature/unit-test-utility

Improvements to the unit tests directory

Author: Daniel Kroening

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

unit/Makefile

@@ -1,12 +1,18 @@
 .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 \
+      src/ansi-c/c_to_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
@@ -15,19 +21,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 +57,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)

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 <catch.hpp>
+
+c_to_exprt::c_to_exprt():
+  message_handler(
+    std::unique_ptr<message_handlert>(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;
+}

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 <memory>
+
+#include <util/expr.h>
+#include <util/message.h>
+#include <util/ui_message.h>
+#include <util/namespace.h>
+#include <ansi-c/ansi_c_language.h>
+
+class c_to_exprt
+{
+public:
+  c_to_exprt();
+  exprt operator()(const std::string &input_string, const namespacet &ns);
+
+private:
+  std::unique_ptr<message_handlert> message_handler;
+  ansi_c_languaget language;
+};
+
+#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H

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 <catch.hpp>
+#include <util/arith_tools.h>
+
+/// 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;
+}

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 <util/std_expr.h>
+
+// 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

unit/unit_tests.cpp

@@ -8,3 +8,11 @@
 
 #define CATCH_CONFIG_MAIN
 #include "catch.hpp"
+#include <util/irep.h>
+
+// Debug printer for irept
+std::ostream &operator<<(std::ostream &os, const irept &value)
+{
+  os << value.pretty();
+  return os;
+}