Merge pull request #731 from tautschnig/more-rewriting

Simplifier and symex rewriting fixes/extensions

Author: peterschrammel

src/goto-symex/symex_clean_expr.cpp

@@ -67,11 +67,13 @@ void goto_symext::process_array_expr_rec(
     expr.swap(tmp);
   }
   else
+  {
     Forall_operands(it, expr)
     {
       typet t=it->type();
       process_array_expr_rec(*it, t);
     }
+  }
 
   if(!base_type_eq(expr.type(), type, ns))
   {
@@ -166,12 +168,41 @@ void goto_symext::replace_array_equal(exprt &expr)
     replace_array_equal(*it);
 }
 
+/// Rewrite index/member expressions in byte_extract to offset
+static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
+{
+  Forall_operands(it, expr)
+    adjust_byte_extract_rec(*it, ns);
+
+  if(expr.id()==ID_byte_extract_big_endian ||
+     expr.id()==ID_byte_extract_little_endian)
+  {
+    byte_extract_exprt &be=to_byte_extract_expr(expr);
+    if(be.op().id()==ID_symbol &&
+       to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
+      return;
+
+    object_descriptor_exprt ode;
+    ode.build(expr, ns);
+
+    be.op()=ode.root_object();
+    be.offset()=ode.offset();
+  }
+}
+
 void goto_symext::clean_expr(
   exprt &expr,
   statet &state,
   const bool write)
 {
   replace_nondet(expr);
   dereference(expr, state, write);
+
+  // make sure all remaining byte extract operations use the root
+  // object to avoid nesting of with/update and byte_update when on
+  // lhs
+  if(write)
+    adjust_byte_extract_rec(expr, ns);
+
   replace_array_equal(expr);
 }

src/solvers/flattening/flatten_byte_operators.cpp

@@ -242,12 +242,12 @@ exprt flatten_byte_extract(
 
         byte_extract_exprt tmp(unpacked);
         tmp.type()=subtype;
-        tmp.offset()=simplify_expr(new_offset, ns);
+        tmp.offset()=new_offset;
 
         array.copy_to_operands(flatten_byte_extract(tmp, ns));
       }
 
-      return array;
+      return simplify_expr(array, ns);
     }
   }
   else if(type.id()==ID_struct)
@@ -277,13 +277,13 @@ exprt flatten_byte_extract(
 
       byte_extract_exprt tmp(unpacked);
       tmp.type()=comp.type();
-      tmp.offset()=simplify_expr(new_offset, ns);
+      tmp.offset()=new_offset;
 
       s.move_to_operands(tmp);
     }
 
     if(!failed)
-      return s;
+      return simplify_expr(s, ns);
   }
 
   const exprt &root=unpacked.op();
@@ -333,7 +333,7 @@ exprt flatten_byte_extract(
   {
     concatenation_exprt concatenation(src.type());
     concatenation.operands().swap(op);
-    return concatenation;
+    return simplify_expr(concatenation, ns);
   }
 }
 
@@ -413,7 +413,7 @@ exprt flatten_byte_update(
           result.swap(with_expr);
         }
 
-        return result;
+        return simplify_expr(result, ns);
       }
       else // sub_size!=1
       {
@@ -512,7 +512,7 @@ exprt flatten_byte_update(
           result=with_expr;
         }
 
-        return result;
+        return simplify_expr(result, ns);
       }
     }
     else
@@ -583,7 +583,7 @@ exprt flatten_byte_update(
     // original_bits |= newvalue
     bitor_exprt bitor_expr(bitand_expr, value_shifted);
 
-    return bitor_expr;
+    return simplify_expr(bitor_expr, ns);
   }
   else
   {

src/util/simplify_expr.cpp

@@ -318,12 +318,14 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
   if(config.ansi_c.NULL_is_zero &&
      (expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
+     op_type.id()==ID_pointer &&
      expr.op0().id()==ID_plus &&
      expr.op0().operands().size()==2 &&
-     expr.op0().op0().id()==ID_typecast &&
+     ((expr.op0().op0().id()==ID_typecast &&
      expr.op0().op0().operands().size()==1 &&
-     expr.op0().op0().op0().is_zero() &&
-     op_type.id()==ID_pointer)
+       expr.op0().op0().op0().is_zero()) ||
+      (expr.op0().op0().is_constant() &&
+       to_constant_expr(expr.op0().op0()).get_value()==ID_NULL)))
   {
     mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns);
     if(sub_size!=-1)
@@ -727,6 +729,20 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
       return false;
     }
   }
+  else if(operand.id()==ID_address_of)
+  {
+    const exprt &o=to_address_of_expr(operand).object();
+
+    // turn &array into &array[0] when casting to pointer-to-element-type
+    if(o.type().id()==ID_array &&
+       base_type_eq(expr_type, pointer_type(o.type().subtype()), ns))
+    {
+      expr=address_of_exprt(index_exprt(o, from_integer(0, size_type())));
+
+      simplify_rec(expr);
+      return false;
+    }
+  }
 
   return true;
 }
@@ -1826,6 +1842,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
             index_exprt(
               result,
               from_integer(offset, expr.offset().type()));
+          result.make_typecast(expr.type());
 
           if(!base_type_eq(expr.type(), op_type_ptr->subtype(), ns))
              result.make_typecast(expr.type());
@@ -1886,7 +1903,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         simplify_member(expr.op());
         expr.offset()=
           from_integer(offset-m_offset_bits/8, expr.offset().type());
-        simplify_rec(expr.offset());
+        simplify_rec(expr);
 
         return false;
       }
@@ -2116,6 +2133,14 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 
       return false;
     }
+
+    if(result_expr.is_not_nil())
+    {
+      simplify_rec(result_expr);
+      expr.swap(result_expr);
+
+      return false;
+    }
   }
 
   // replace elements of array or struct expressions, possibly using

src/util/simplify_expr_boolean.cpp

@@ -72,21 +72,60 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
       return false;
     }
   }
-  else if(expr.id()==ID_or ||
-          expr.id()==ID_and ||
-          expr.id()==ID_xor)
+  else if(expr.id()==ID_xor)
   {
-    if(operands.empty())
-      return true;
-
     bool result=true;
 
-    exprt::operandst::const_iterator last;
-    bool last_set=false;
-
     bool negate=false;
 
-    for(exprt::operandst::iterator it=operands.begin();
+    for(exprt::operandst::const_iterator it=operands.begin();
+        it!=operands.end();)
+    {
+      if(it->type().id()!=ID_bool)
+        return true;
+
+      bool erase;
+
+      if(it->is_true())
+      {
+        erase=true;
+        negate=!negate;
+      }
+      else
+        erase=it->is_false();
+
+      if(erase)
+      {
+        it=operands.erase(it);
+        result=false;
+      }
+      else
+        it++;
+    }
+
+    if(operands.empty())
+    {
+      expr.make_bool(negate);
+      return false;
+    }
+    else if(operands.size()==1)
+    {
+      exprt tmp(operands.front());
+      if(negate)
+        tmp.make_not();
+      expr.swap(tmp);
+      return false;
+    }
+
+    return result;
+  }
+  else if(expr.id()==ID_and || expr.id()==ID_or)
+  {
+    std::unordered_set<exprt, irep_hash> expr_set;
+
+    bool result=true;
+
+    for(exprt::operandst::const_iterator it=operands.begin();
         it!=operands.end();)
     {
       if(it->type().id()!=ID_bool)
@@ -106,77 +145,37 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
         return false;
       }
 
-      bool erase;
-
-      if(expr.id()==ID_and)
-        erase=is_true;
-      else if(is_true && expr.id()==ID_xor)
-      {
-        erase=true;
-        negate=!negate;
-      }
-      else
-        erase=is_false;
-
-      if(last_set && *it==*last &&
-         (expr.id()==ID_or || expr.id()==ID_and))
-        erase=true; // erase duplicate operands
+      bool erase=
+        (expr.id()==ID_and ? is_true : is_false) ||
+        !expr_set.insert(*it).second;
 
       if(erase)
       {
         it=operands.erase(it);
         result=false;
       }
       else
-      {
-        last=it;
-        last_set=true;
         it++;
-      }
     }
 
     // search for a and !a
-    if(expr.id()==ID_and || expr.id()==ID_or)
-    {
-      // first gather all the a's with !a
-
-      std::unordered_set<exprt, irep_hash> expr_set;
-
-      forall_operands(it, expr)
-        if(it->id()==ID_not &&
-           it->operands().size()==1 &&
-           it->type().id()==ID_bool)
-          expr_set.insert(it->op0());
-
-      // now search for a
-
-      if(!expr_set.empty())
+    for(const exprt &op : operands)
+      if(op.id()==ID_not &&
+         op.operands().size()==1 &&
+         op.type().id()==ID_bool &&
+         expr_set.find(op.op0())!=expr_set.end())
       {
-        forall_operands(it, expr)
-        {
-          if(it->id()!=ID_not &&
-             expr_set.find(*it)!=expr_set.end())
-          {
-            expr.make_bool(expr.id()==ID_or);
-            return false;
-          }
-        }
+        expr.make_bool(expr.id()==ID_or);
+        return false;
       }
-    }
 
     if(operands.empty())
     {
-      if(expr.id()==ID_and || negate)
-        expr=true_exprt();
-      else
-        expr=false_exprt();
-
+      expr.make_bool(expr.id()==ID_and);
       return false;
     }
     else if(operands.size()==1)
     {
-      if(negate)
-        expr.op0().make_not();
       exprt tmp(operands.front());
       expr.swap(tmp);
       return false;