Use generic simplify_expr instead of local simplification rules

Author: tautschnig

src/goto-programs/json_goto_trace.cpp

@@ -21,82 +21,6 @@ Author: Daniel Kroening
 
 #include <langapi/language_util.h>
 
-/// Replaces in src, expressions of the form pointer_offset(constant) by that
-/// constant.
-/// \param src: an expression
-void remove_pointer_offsets(exprt &src)
-{
-  if(src.id()==ID_pointer_offset &&
-     src.op0().id()==ID_constant &&
-     src.op0().type().id()==ID_pointer)
-  {
-    std::string binary_str=id2string(to_constant_expr(src.op0()).get_value());
-    // The constant address consists of OBJECT-ID || OFFSET.
-    // Shift out the object-identifier bits, leaving only the offset:
-    mp_integer offset=binary2integer(
-      binary_str.substr(config.bv_encoding.object_bits), false);
-    src=from_integer(offset, src.type());
-  }
-  else
-    for(auto &op : src.operands())
-      remove_pointer_offsets(op);
-}
-
-/// Replaces in src, expressions of the form pointer_offset(array_symbol) by a
-/// constant value of 0. This is meant to simplify array expressions.
-/// \param src: an expression
-/// \param array_symbol: a symbol expression representing an array
-void remove_pointer_offsets(exprt &src, const symbol_exprt &array_symbol)
-{
-  if(src.id()==ID_pointer_offset &&
-     src.op0().id()==ID_constant &&
-     src.op0().op0().id()==ID_address_of &&
-     src.op0().op0().op0().id()==ID_index)
-  {
-    const index_exprt &idx=to_index_expr(src.op0().op0().op0());
-    const irep_idt &array_id=to_symbol_expr(idx.array()).get_identifier();
-    if(idx.array().id()==ID_symbol &&
-       array_id==array_symbol.get_identifier() &&
-       to_constant_expr(idx.index()).value_is_zero_string())
-      src=from_integer(0, src.type());
-  }
-  else
-    for(auto &op : src.operands())
-      remove_pointer_offsets(op, array_symbol);
-}
-
-/// Simplify an expression before putting it in the json format
-/// \param src: an expression potentialy containing array accesses (index_expr)
-/// \return an expression similar in meaning to src but where array accesses
-///   have been simplified
-exprt simplify_array_access(const exprt &src, const namespacet &ns)
-{
-  if(src.id()==ID_index && to_index_expr(src).array().id()==ID_symbol)
-  {
-    // Case where the array is a symbol.
-    const symbol_exprt &array_symbol=to_symbol_expr(to_index_expr(src).array());
-    exprt simplified_index=to_index_expr(src).index();
-    // We remove potential appearances of `pointer_offset(array_symbol)`
-    remove_pointer_offsets(simplified_index, array_symbol);
-    simplified_index=simplify_expr(simplified_index, ns);
-    return index_exprt(array_symbol, simplified_index);
-  }
-  else if(src.id()==ID_index && to_index_expr(src).array().id()==ID_array)
-  {
-    // Case where the array is given by an array of expressions
-    exprt index=to_index_expr(src).index();
-    remove_pointer_offsets(index);
-
-    // We look for an actual integer value for the index
-    index=simplify_expr(index, ns);
-    unsigned i;
-    if(index.id()==ID_constant &&
-       !to_unsigned_integer(to_constant_expr(index), i))
-      return to_index_expr(src).array().operands()[i];
-  }
-  return src;
-}
-
 /// Produce a json representation of a trace.
 /// \param ns: a namespace
 /// \param goto_trace: a trace in a goto program
@@ -169,7 +93,7 @@ void convert(
         DATA_INVARIANT(
           step.full_lhs.is_not_nil(),
           "full_lhs in assignment must not be nil");
-        exprt simplified=simplify_array_access(step.full_lhs, ns);
+        exprt simplified=simplify_expr(step.full_lhs, ns);
         full_lhs_string=from_expr(ns, identifier, simplified);
 
         const symbolt *symbol;
@@ -183,7 +107,7 @@ void convert(
             type_string=from_type(ns, identifier, symbol->type);
 
           json_assignment["mode"]=json_stringt(id2string(symbol->mode));
-          exprt simplified=simplify_array_access(step.full_lhs_value, ns);
+          exprt simplified=simplify_expr(step.full_lhs_value, ns);
 
           full_lhs_value=json(simplified, ns, symbol->mode);
         }