Merge pull request #922 from romainbrenguier/pull-request/arrays-in-trace

Better output of arrays in json

Author: romainbrenguier

regression/strings-smoke-tests/jsonArrays/test.class

@@ -0,0 +1,10 @@
+CORE
+test.class
+--refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location
+^EXIT=0$
+^SIGNAL=0$
+\"data\".*\"tmp_object_factory\$6.*\"
+--
+This checks that tmp_object_factory$6 gets affected to the data field
+of some strings, which was not the case in previous versions of cbmc,
+as it was just ignored by the json output.

regression/strings-smoke-tests/jsonArrays/test.desc

@@ -0,0 +1,8 @@
+public class test
+{
+    public static int check(String s)
+    {
+        int i=Integer.parseInt(s);
+        return i;
+    }
+}

regression/strings-smoke-tests/jsonArrays/test.java

@@ -14,11 +14,112 @@ 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"
 
+/// 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=src.op0();
+  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 the expression in index as much as possible to try to get an
+/// unsigned constant.
+/// \param idx: an expression representing an index in an array
+/// \param out: a reference to an unsigned value of type size_t, which will hold
+///   the result of the simplification if it is successful
+/// \return Boolean flag that is true if the `idx` expression could not be
+///   simplified into a unsigned constant value.
+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;
+}
+
+/// 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)
+{
+  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;
+}
+
+/// Produce a json representation of a trace.
+/// \param ns: a namespace
+/// \param goto_trace: a trace in a goto program
+/// \param dest: referecence to a json object in which the goto trace will be
+///   added
 void convert(
   const namespacet &ns,
   const goto_tracet &goto_trace,
@@ -84,7 +185,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 +200,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
         {

src/goto-programs/json_goto_trace.cpp

@@ -52,16 +52,26 @@ static exprt simplify_json_expr(
           id2string(to_member_expr(
             src.op0()).get_component_name()).find("@")!=std::string::npos)
   {
-    // simplify things of the form  &member_expr(object, @class_identifier)
+    // simplify expressions of the form &member_expr(object, @class_identifier)
     return simplify_json_expr(src.op0(), ns);
   }
+  else if(src.id()==ID_address_of &&
+          src.operands().size()==1 &&
+          src.op0().id()==ID_index &&
+          to_index_expr(src.op0()).index().id()==ID_constant &&
+          to_constant_expr(
+            to_index_expr(src.op0()).index()).value_is_zero_string())
+  {
+    // simplify expressions of the form  &array[0]
+    return simplify_json_expr(to_index_expr(src.op0()).array(), ns);
+  }
   else if(src.id()==ID_member &&
           src.operands().size()==1 &&
           id2string(
             to_member_expr(src).get_component_name())
               .find("@")!=std::string::npos)
   {
-    // simplify things of the form  member_expr(object, @class_identifier)
+    // simplify expressions of the form  member_expr(object, @class_identifier)
     return simplify_json_expr(src.op0(), ns);
   }