From fc4aab3ffbf2a9eb26108e31e565958b63240d5c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 30 Jun 2018 17:05:12 +0100
Subject: [PATCH] avoid non-termination of
 simplify_exprt::simplify_byte_extract when given array_of

---
 .../jbmc/simplify_expr_termination/test.class | Bin 0 -> 528 bytes
 .../jbmc/simplify_expr_termination/test.desc  |  10 ++++
 .../jbmc/simplify_expr_termination/test.java  |  11 +++++
 src/util/simplify_expr.cpp                    |  43 +++++++++++-------
 src/util/simplify_expr_class.h                |   3 +-
 src/util/simplify_expr_struct.cpp             |   7 +--
 6 files changed, 54 insertions(+), 20 deletions(-)
 create mode 100644 jbmc/regression/jbmc/simplify_expr_termination/test.class
 create mode 100644 jbmc/regression/jbmc/simplify_expr_termination/test.desc
 create mode 100644 jbmc/regression/jbmc/simplify_expr_termination/test.java

diff --git a/jbmc/regression/jbmc/simplify_expr_termination/test.class b/jbmc/regression/jbmc/simplify_expr_termination/test.class
new file mode 100644
index 0000000000000000000000000000000000000000..e10a48a9a29f6cbbb7e7eb6ef517a29077206efc
GIT binary patch
literal 528
zcmYL`OD_Xa6vzK(Ubh`XUrLpFBo<icf~5%YNW^PVkzh5Q-Y_*<nVI@9{Q@>NNHjs%
z`%EIv9n|LBbI<vo|NPFKkFV!90Lz%RAy7=i#E8JC4IM>+l8rHx1;z=5SvQJg82jy3
zwCP7~J&+9oof51SzvaiP1buG)m|$$Q8<LRO^IP(ub5)n&krES3??QT)iEM{3Sc_fn
za^Jm9x&jk~)QT7UTG_RBC-mgDuLjexjN-+nd*eE=G2kGDG@+yl)xd3?SJ(f@w!*L-
zGJ+Zqs5qF!6e0VsJghgR7ZbEI2G9K0Hv-;{Fw&5bAIe7GkRjs^H+Z#E%<$s~ek{tC
z6ar^DND*;#_*UVQ_%s)KpnE06AV(`H@){UIhI1v|gO*gw)~m6*pf7cidw|x(zzg(~
z9*lS6j#XMRpNGM@$<gAE@lRo=ELT#XPm~05oaOrv%ZV?L%bQQIx)8=K4E+(B0{Suh
Q15zd?G-pj=7n1hyH^`)0fdBvi

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/simplify_expr_termination/test.desc b/jbmc/regression/jbmc/simplify_expr_termination/test.desc
new file mode 100644
index 00000000000..877d071af8e
--- /dev/null
+++ b/jbmc/regression/jbmc/simplify_expr_termination/test.desc
@@ -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
diff --git a/jbmc/regression/jbmc/simplify_expr_termination/test.java b/jbmc/regression/jbmc/simplify_expr_termination/test.java
new file mode 100644
index 00000000000..51999734a5d
--- /dev/null
+++ b/jbmc/regression/jbmc/simplify_expr_termination/test.java
@@ -0,0 +1,11 @@
+public class test {
+
+  public static int check()
+  {
+    boolean[] assigned = new boolean[3];
+    if (assigned[0] == false) {
+        assert false;
+    }
+    return 1;
+  }
+}
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index c2e07be9630..4b719aac548 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -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,11 +1630,12 @@ 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)
@@ -1642,15 +1643,16 @@ 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;
   }
 
-  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));
 
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index a1760e72a9b..5e192292666 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -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;
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 331d04c3001..ba308ac8ea6 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -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);