Merge pull request #3155 from tautschnig/fix-simplify-byte-extract

Fix typo in simplify_byte_extract

Author: Daniel Kroening

jbmc/unit/util/simplify_expr.cpp

@@ -9,58 +9,12 @@
 #include <testing-utils/catch.hpp>
 
 #include <java_bytecode/java_types.h>
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/config.h>
 #include <util/namespace.h>
-#include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
-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
 {
 

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);

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 \

unit/util/simplify_expr.cpp

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+ Module: Unit tests of the expression simplifier
+
+ Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/c_types.h>
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/namespace.h>
+#include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+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);
+}