diff --git a/jbmc/unit/util/simplify_expr.cpp b/jbmc/unit/util/simplify_expr.cpp index 41f8adad246..95b7ee157f3 100644 --- a/jbmc/unit/util/simplify_expr.cpp +++ b/jbmc/unit/util/simplify_expr.cpp @@ -9,58 +9,12 @@ #include #include -#include -#include #include #include -#include #include #include #include -TEST_CASE("Simplify pointer_offset(address of array index)") -{ - config.set_arch("none"); - - symbol_tablet symbol_table; - namespacet ns(symbol_table); - - array_typet array_type(char_type(), from_integer(2, size_type())); - symbol_exprt array("A", array_type); - index_exprt index(array, from_integer(1, index_type())); - address_of_exprt address_of(index); - - exprt p_o=pointer_offset(address_of); - - exprt simp=simplify_expr(p_o, ns); - - REQUIRE(simp.id()==ID_constant); - mp_integer offset_value; - REQUIRE(!to_integer(simp, offset_value)); - REQUIRE(offset_value==1); -} - -TEST_CASE("Simplify const pointer offset") -{ - config.set_arch("none"); - - symbol_tablet symbol_table; - namespacet ns(symbol_table); - - // build a numeric constant of some pointer type - constant_exprt number=from_integer(1234, size_type()); - number.type()=pointer_type(char_type()); - - exprt p_o=pointer_offset(number); - - exprt simp=simplify_expr(p_o, ns); - - REQUIRE(simp.id()==ID_constant); - mp_integer offset_value; - REQUIRE(!to_integer(simp, offset_value)); - REQUIRE(offset_value==1234); -} - namespace { diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 23aeef9850f..c07eb747280 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1722,9 +1722,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) // byte extract of full object is object // don't do any of the following if endianness doesn't match, as // bytes need to be swapped - if(offset==0 && - base_type_eq(expr.type(), expr.op().type(), ns) && - byte_extract_id()!=expr.id()) + if( + offset == 0 && base_type_eq(expr.type(), expr.op().type(), ns) && + byte_extract_id() == expr.id()) { exprt tmp=expr.op(); expr.swap(tmp); diff --git a/unit/Makefile b/unit/Makefile index 261393bd89e..b6fe09fc521 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -43,6 +43,7 @@ SRC += analyses/ai/ai.cpp \ util/replace_symbol.cpp \ util/sharing_map.cpp \ util/sharing_node.cpp \ + util/simplify_expr.cpp \ util/small_map.cpp \ util/small_shared_two_way_ptr.cpp \ util/std_expr.cpp \ diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp new file mode 100644 index 00000000000..8f75262f446 --- /dev/null +++ b/unit/util/simplify_expr.cpp @@ -0,0 +1,84 @@ +/*******************************************************************\ + + Module: Unit tests of the expression simplifier + + Author: Michael Tautschnig + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +TEST_CASE("Simplify pointer_offset(address of array index)") +{ + config.set_arch("none"); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + array_typet array_type(char_type(), from_integer(2, size_type())); + symbol_exprt array("A", array_type); + index_exprt index(array, from_integer(1, index_type())); + address_of_exprt address_of(index); + + exprt p_o=pointer_offset(address_of); + + exprt simp=simplify_expr(p_o, ns); + + REQUIRE(simp.id()==ID_constant); + mp_integer offset_value; + REQUIRE(!to_integer(simp, offset_value)); + REQUIRE(offset_value==1); +} + +TEST_CASE("Simplify const pointer offset") +{ + config.set_arch("none"); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + // build a numeric constant of some pointer type + constant_exprt number=from_integer(1234, size_type()); + number.type()=pointer_type(char_type()); + + exprt p_o=pointer_offset(number); + + exprt simp=simplify_expr(p_o, ns); + + REQUIRE(simp.id()==ID_constant); + mp_integer offset_value; + REQUIRE(!to_integer(simp, offset_value)); + REQUIRE(offset_value==1234); +} + +TEST_CASE("Simplify byte extract") +{ + // this test does require a proper architecture to be set so that byte extract + // uses adequate endianness + cmdlinet cmdline; + config.set(cmdline); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + // byte-extracting type T at offset 0 from an object of type T yields the + // object + symbol_exprt s("foo", size_type()); + byte_extract_exprt be( + byte_extract_id(), s, from_integer(0, index_type()), size_type()); + + exprt simp = simplify_expr(be, ns); + + REQUIRE(simp == s); +}