Merge pull request #4186 from tautschnig/byte-op-strings

byte_extract lowering of string constants [blocks: #2068]

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
+#include <util/string_constant.h>
 
 #include "flatten_byte_extract_exceptions.h"
 
@@ -275,6 +276,26 @@ static exprt unpack_rec(
       ns,
       unpack_byte_array);
   }
+  else if(src.id() == ID_string_constant)
+  {
+    return unpack_rec(
+      to_string_constant(src).to_array_expr(),
+      little_endian,
+      offset_bytes,
+      max_bytes,
+      ns,
+      unpack_byte_array);
+  }
+  else if(src.id() == ID_constant && src.type().id() == ID_string)
+  {
+    return unpack_rec(
+      string_constantt(to_constant_expr(src).get_value()).to_array_expr(),
+      little_endian,
+      offset_bytes,
+      max_bytes,
+      ns,
+      unpack_byte_array);
+  }
   else if(src.type().id()!=ID_empty)
   {
     // a basic type; we turn that into extractbits while considering

unit/solvers/lowering/byte_operators.cpp

@@ -21,6 +21,7 @@
 #include <util/simplify_expr.h>
 #include <util/simplify_expr_class.h>
 #include <util/std_types.h>
+#include <util/string_constant.h>
 #include <util/symbol_table.h>
 
 SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
@@ -90,6 +91,35 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     }
   }
 
+  GIVEN("A a byte_extract from a string constant")
+  {
+    string_constantt s("ABCD");
+    const byte_extract_exprt be1(
+      ID_byte_extract_little_endian,
+      s,
+      from_integer(1, index_type()),
+      unsignedbv_typet(16));
+
+    THEN("byte_extract lowering yields the expected value")
+    {
+      const exprt lower_be1 = lower_byte_extract(be1, ns);
+
+      REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
+      REQUIRE(lower_be1.type() == be1.type());
+      REQUIRE(
+        lower_be1 == from_integer((int{'C'} << 8) + 'B', unsignedbv_typet(16)));
+
+      byte_extract_exprt be2 = be1;
+      be2.id(ID_byte_extract_big_endian);
+      const exprt lower_be2 = lower_byte_extract(be2, ns);
+
+      REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
+      REQUIRE(lower_be2.type() == be2.type());
+      REQUIRE(
+        lower_be2 == from_integer((int{'B'} << 8) + 'C', unsignedbv_typet(16)));
+    }
+  }
+
   GIVEN("A collection of types")
   {
     unsignedbv_typet u8(8);