diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 23d814b75a9..3d8fbba8b19 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -367,6 +367,12 @@ bool simplify_exprt::simplify_typecast(exprt &expr) { } } + else + { + exprt smaller_width_value=expr.op0(); + expr.swap(smaller_width_value); + return false; + } } // Push a numerical typecast into pointer arithmetic diff --git a/unit/Makefile b/unit/Makefile index a1de1539ee7..bcfdb615940 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -2,6 +2,8 @@ SRC = unit_tests.cpp \ catch_example.cpp \ + util/simplify_expr/simplify_typecast.cpp \ + unit-src/unit_util.cpp \ # Empty last line INCLUDES= -I ../src/ -I. @@ -24,6 +26,7 @@ LIBS += ../src/ansi-c/ansi-c$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ ../src/analyses/analyses$(LIBEXT) \ ../src/solvers/solvers$(LIBEXT) \ + ../src/util/util$(LIBEXT) \ # Empty last line TESTS = unit_tests$(EXEEXT) \ diff --git a/unit/unit-src/unit_util.cpp b/unit/unit-src/unit_util.cpp new file mode 100644 index 00000000000..de273d5d5d0 --- /dev/null +++ b/unit/unit-src/unit_util.cpp @@ -0,0 +1,14 @@ +/*******************************************************************\ + + Module: Unit Test Utility Functions + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#include "unit_util.h" + +std::ostream &operator<<(std::ostream &os, const irept &value) +{ + os << value.pretty(); + return os; +} diff --git a/unit/unit-src/unit_util.h b/unit/unit-src/unit_util.h new file mode 100644 index 00000000000..e718e1b2819 --- /dev/null +++ b/unit/unit-src/unit_util.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + + Module: Unit Test Utility Functions + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#ifndef CPROVER_UNIT_SRC_UNIT_UTIL_H +#define CPROVER_UNIT_SRC_UNIT_UTIL_H + +#include +#include + +/// For printing irept data structures when used inside the unit tests +/// (e.g. for INFO, REQUIRE etc macros +/// \param os: The ostream to write to +/// \param value: The irept data structure to print +/// \returns The ostream after writing to it +std::ostream &operator<<(std::ostream &os, const irept &value); + +#endif // CPROVER_UNIT_SRC_UNIT_UTIL_H diff --git a/unit/util/simplify_expr/simplify_typecast.cpp b/unit/util/simplify_expr/simplify_typecast.cpp new file mode 100644 index 00000000000..3aa3200ffe6 --- /dev/null +++ b/unit/util/simplify_expr/simplify_typecast.cpp @@ -0,0 +1,142 @@ +/*******************************************************************\ + + Module: MODULE NAME + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Unit tests for util/simplify_expr.cpp + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + + +#include + +SCENARIO("Simplifying an expression", "[core][util][simplify_expr]" + "[simplify_typecast]") +{ + ui_message_handlert message_handler; + ansi_c_languaget language; + language.set_message_handler(message_handler); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + GIVEN("A namespace with some symbols in on a default architecture") + { + array_typet array_type( + signedbv_typet(32), constant_exprt::integer_constant(5)); + + symbolt a_symbol; + a_symbol.base_name="a"; + a_symbol.name="a"; + a_symbol.type=array_type; + a_symbol.is_lvalue=true; + symbol_table.add(a_symbol); + + symbolt i_symbol; + i_symbol.base_name="i"; + i_symbol.name="i"; + i_symbol.type=signedbv_typet(32); + i_symbol.is_lvalue=true; + symbol_table.add(i_symbol); + + config.set_arch("none"); + + WHEN("Simplifying a[(signed long int)0]") + { + exprt out_expr; + bool success=language.to_expr("a[(signed long int)0]", "", out_expr, ns); + + // Validate the conversion to expr + REQUIRE_FALSE(success); + THEN("Should get a[0]") + { + exprt simplified_expr=simplify_expr(out_expr, ns); + REQUIRE(simplified_expr.id()==ID_index); + + index_exprt index=to_index_expr(simplified_expr); + + const exprt &index_part=index.index(); + REQUIRE(index_part.id()==ID_constant); + } + } + WHEN("Simplifying a[(signed long int)i]") + { + exprt out_expr; + bool success=language.to_expr("a[(signed long int)i]", "", out_expr, ns); + + // Validate the conversion to expr + REQUIRE_FALSE(success); + THEN("Should get a[i]") + { + exprt simplified_expr=simplify_expr(out_expr, ns); + REQUIRE(simplified_expr.id()==ID_index); + + index_exprt index=to_index_expr(simplified_expr); + + const exprt &index_part=index.index(); + REQUIRE(index_part.id()==ID_symbol); + const symbol_exprt symbol_expr=to_symbol_expr(index_part); + REQUIRE(symbol_expr.get_identifier()=="i"); + } + } + WHEN("Simplifying a[(signed int)i]") + { + exprt out_expr; + bool success=language.to_expr("a[(signed int)i]", "", out_expr, ns); + + // Validate the conversion to expr + REQUIRE_FALSE(success); + THEN("Should get a[i]") + { + exprt simplified_expr=simplify_expr(out_expr, ns); + REQUIRE(simplified_expr.id()==ID_index); + + index_exprt index=to_index_expr(simplified_expr); + + const exprt &index_part=index.index(); + REQUIRE(index_part.id()==ID_symbol); + const symbol_exprt symbol_expr=to_symbol_expr(index_part); + REQUIRE(symbol_expr.get_identifier()=="i"); + } + } + WHEN("Simplifying a[(signed short)i]") + { + exprt out_expr; + bool success=language.to_expr("a[(signed short)i]", "", out_expr, ns); + + // Validate the conversion to expr + REQUIRE_FALSE(success); + + // Since this is cast could go wrong (if i has a value greater than + // SHRT_MAX for example) it should not be removed by the simplify + THEN("Should get a[(signed short)i]") + { + exprt simplified_expr=simplify_expr(out_expr, ns); + REQUIRE(simplified_expr.id()==ID_index); + + index_exprt index=to_index_expr(simplified_expr); + + const exprt &index_part=index.index(); + + // The expression will have changed as we are still able to remove + // one type cast (the cast from short to long) + REQUIRE(index_part.id()==ID_typecast); + REQUIRE(index_part.type().id()==ID_signedbv); + signedbv_typet signed_bv_type=to_signedbv_type(index_part.type()); + REQUIRE(signed_bv_type.get_width()==config.ansi_c.short_int_width); + } + } + } +}