Merge pull request #2497 from diffblue/simplify_byte_extract_fix

avoid non-termination of simplify_exprt::simplify_byte_extract(array_of(...))

Author: kroening

jbmc/regression/jbmc/simplify_expr_termination/test.class

@@ -0,0 +1,10 @@
+CORE
+test.class
+--function test.check
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Checks that a non-termination bug no longer occurs in simplify_byte_extract

jbmc/regression/jbmc/simplify_expr_termination/test.desc

@@ -0,0 +1,11 @@
+public class test {
+
+  public static int check()
+  {
+    boolean[] assigned = new boolean[3];
+    if (assigned[0] == false) {
+        assert false;
+    }
+    return 1;
+  }
+}

jbmc/regression/jbmc/simplify_expr_termination/test.java

@@ -1593,7 +1593,7 @@ exprt simplify_exprt::bits2expr(
   return nil_exprt();
 }
 
-std::string simplify_exprt::expr2bits(
+optionalt<std::string> simplify_exprt::expr2bits(
   const exprt &expr,
   bool little_endian)
 {
@@ -1630,27 +1630,29 @@ std::string simplify_exprt::expr2bits(
     std::string result;
     forall_operands(it, expr)
     {
-      std::string tmp=expr2bits(*it, little_endian);
-      if(tmp.empty())
-        return tmp; // failed
-      result+=tmp;
+      auto tmp=expr2bits(*it, little_endian);
+      if(!tmp.has_value())
+        return {}; // failed
+      result+=tmp.value();
     }
+
     return result;
   }
   else if(expr.id()==ID_array)
   {
     std::string result;
     forall_operands(it, expr)
     {
-      std::string tmp=expr2bits(*it, little_endian);
-      if(tmp.empty())
-        return tmp; // failed
-      result+=tmp;
+      auto tmp=expr2bits(*it, little_endian);
+      if(!tmp.has_value())
+        return {}; // failed
+      result+=tmp.value();
     }
+
     return result;
   }
 
-  return "";
+  return {};
 }
 
 bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
@@ -1734,12 +1736,19 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     return true;
 
   if(expr.op().id()==ID_array_of &&
-     expr.op().op0().id()==ID_constant)
+     to_array_of_expr(expr.op()).op().id()==ID_constant)
   {
-    std::string const_bits=
-      expr2bits(expr.op().op0(),
+    const auto const_bits_opt=
+      expr2bits(to_array_of_expr(expr.op()).op(),
                 byte_extract_id()==ID_byte_extract_little_endian);
 
+    if(!const_bits_opt.has_value())
+      return true;
+
+    std::string const_bits=const_bits_opt.value();
+
+    DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
+
     // double the string until we have sufficiently many bits
     while(mp_integer(const_bits.size())<offset*8+el_size)
       const_bits+=const_bits;
@@ -1776,15 +1785,17 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   }
 
   // extract bits of a constant
-  std::string bits=
+  const auto bits=
     expr2bits(expr.op(), expr.id()==ID_byte_extract_little_endian);
+
   // exact match of length only - otherwise we might lose bits of
   // flexible array members at the end of a struct
-  if(mp_integer(bits.size())==el_size+offset*8)
+  if(bits.has_value() &&
+     mp_integer(bits->size())==el_size+offset*8)
   {
     std::string bits_cut=
       std::string(
-        bits,
+        bits.value(),
         integer2size_t(offset*8),
         integer2size_t(el_size));
 

src/util/simplify_expr.cpp

@@ -151,7 +151,8 @@ class simplify_exprt
   // bit-level conversions
   exprt bits2expr(
     const std::string &bits, const typet &type, bool little_endian);
-  std::string expr2bits(const exprt &expr, bool little_endian);
+
+  optionalt<std::string> expr2bits(const exprt &, bool little_endian);
 
 protected:
   const namespacet &ns;

src/util/simplify_expr_class.h

@@ -190,11 +190,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
     if(target_size!=-1)
     {
       mp_integer target_bits=target_size*8;
-      std::string bits=expr2bits(op, true);
+      const auto bits=expr2bits(op, true);
 
-      if(mp_integer(bits.size())>=target_bits)
+      if(bits.has_value() &&
+         mp_integer(bits->size())>=target_bits)
       {
-        std::string bits_cut=std::string(bits, 0, integer2size_t(target_bits));
+        std::string bits_cut=std::string(*bits, 0, integer2size_t(target_bits));
 
         exprt tmp=bits2expr(bits_cut, expr.type(), true);