Simplifying array access and expressions with pointer offsets

We simplify expressions containing array accesses before producing a
json representation of the trace.
This commit also adds comments on the functions in the cpp files

Includes improvements in json_goto_trace.cpp following review of PR#922

Author: romainbrenguier

src/goto-programs/json_goto_trace.cpp

@@ -14,11 +14,162 @@ Author: Daniel Kroening
 #include <cassert>
 
 #include <util/json_expr.h>
+#include <util/arith_tools.h>
 
 #include <langapi/language_util.h>
 
 #include "json_goto_trace.h"
 
+/*******************************************************************\
+
+Function: remove_pointer_offsets
+
+  Inputs:
+    src - an expression
+
+ Purpose: Replaces in src, expressions of the form pointer_offset(constant)
+          by that constant.
+
+\*******************************************************************/
+
+void remove_pointer_offsets(exprt &src)
+{
+  if(src.id()==ID_pointer_offset && src.op0().id()==ID_constant)
+    src=src.op0();
+  else
+    for(auto &op : src.operands())
+      remove_pointer_offsets(op);
+}
+
+/*******************************************************************\
+
+Function: remove_pointer_offsets
+
+  Inputs:
+    src - an expression
+    array_symbol - a symbol expression representing an array
+
+ Purpose: Replaces in src, expressions of the form
+          pointer_offset(array_symbol) by a constant value of 0.
+          This is meant to simplify array expressions.
+
+\*******************************************************************/
+
+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);
+}
+
+/*******************************************************************\
+
+Function: simplify_index
+
+  Inputs:
+    idx - an expression representing an index in an array
+    out - a reference to an unsigned value of type size_t, which will
+          hold the result of the simplification if it is successful
+
+ Outputs: Boolean flag that is true if the `idx` expression could not be
+          simplified into a unsigned constant value.
+
+ Purpose: Simplify the expression in index as much as possible to try
+          to get an unsigned constant.
+
+\*******************************************************************/
+
+bool simplify_index(const exprt &idx, std::size_t &out)
+{
+  if(idx.id()==ID_constant)
+  {
+    std::string value_str(id2string(to_constant_expr(idx).get_value()));
+    mp_integer int_value=binary2integer(value_str, false);
+    if(int_value>std::numeric_limits<std::size_t>::max())
+      return true;
+    out=int_value.to_long();
+    return false;
+  }
+  else if(idx.id()==ID_plus)
+  {
+    std::size_t l, r;
+    if(!simplify_index(idx.op0(), l) && !simplify_index(idx.op1(), r))
+    {
+      out=l+r;
+      return false;
+    }
+  }
+
+  return true;
+}
+
+/*******************************************************************\
+
+Function: simplify_array_access
+
+  Inputs:
+    src - an expression potentialy containing array accesses (index_expr)
+
+ Outputs: an expression similar in meaning to src but where array accesses
+          have been simplified
+
+ Purpose: Simplify an expression before putting it in the json format
+
+\*******************************************************************/
+
+exprt simplify_array_access(const exprt &src)
+{
+  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);
+    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
+    std::size_t i;
+    if(!simplify_index(index, i))
+      return to_index_expr(src).array().operands()[i];
+  }
+  return src;
+}
+
+/*******************************************************************\
+
+Function: convert
+
+  Inputs:
+    ns - a namespace
+    goto_trace - a trace in a goto program
+    dest - referecence to a json object in which the goto trace will
+           be added
+
+ Outputs: none
+
+ Purpose: Produce a json representation of a trace.
+
+\*******************************************************************/
+
 void convert(
   const namespacet &ns,
   const goto_tracet &goto_trace,
@@ -84,7 +235,8 @@ void convert(
         json_objectt full_lhs_value;
 
         assert(step.full_lhs.is_not_nil());
-        full_lhs_string=from_expr(ns, identifier, step.full_lhs);
+        exprt simplified=simplify_array_access(step.full_lhs);
+        full_lhs_string=from_expr(ns, identifier, simplified);
 
         const symbolt *symbol;
         irep_idt base_name, display_name;
@@ -98,7 +250,8 @@ void convert(
 
           json_assignment["mode"]=json_stringt(id2string(symbol->mode));
           assert(step.full_lhs_value.is_not_nil());
-          full_lhs_value=json(step.full_lhs_value, ns, symbol->mode);
+          exprt simplified=simplify_array_access(step.full_lhs_value);
+          full_lhs_value=json(simplified, ns, symbol->mode);
         }
         else
         {