From 7f002faa9e476df5d0fa61e49462c2179cc52e4d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 14 Oct 2018 08:47:12 +0000 Subject: [PATCH 1/2] Move Java-independent expression simplifier unit tests Test that are unrelated to Java bytecode should be performed as part of the top-level unit tests. This is a preparation step for adding further unit tests. --- jbmc/unit/util/simplify_expr.cpp | 46 ------------------------ unit/Makefile | 1 + unit/util/simplify_expr.cpp | 61 ++++++++++++++++++++++++++++++++ 3 files changed, 62 insertions(+), 46 deletions(-) create mode 100644 unit/util/simplify_expr.cpp 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/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..c10335da649 --- /dev/null +++ b/unit/util/simplify_expr.cpp @@ -0,0 +1,61 @@ +/*******************************************************************\ + + Module: Unit tests of the expression simplifier + + Author: Michael Tautschnig + +\*******************************************************************/ + +#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); +} From 42c6746fde862cd5cd154b5cb3fde24fc371cc28 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 May 2018 18:33:42 +0100 Subject: [PATCH 2/2] Fix typo in simplify_byte_extract As the comment says, only simplify when byte_extract_id() matches the current configuration (and not on a mismatch!). Added a unit test as it isn't entirely obvious what regression tests may produce such expressions. --- src/util/simplify_expr.cpp | 6 +++--- unit/util/simplify_expr.cpp | 23 +++++++++++++++++++++++ 2 files changed, 26 insertions(+), 3 deletions(-) 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/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index c10335da649..8f75262f446 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -9,7 +9,9 @@ #include #include +#include #include +#include #include #include #include @@ -59,3 +61,24 @@ TEST_CASE("Simplify const pointer offset") 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); +}