Merge pull request #1253 from peterschrammel/bugfix/json-output-arrays

Fix JSON array output

Author: peterschrammel

regression/cbmc-java/json_trace3/Test.class

@@ -0,0 +1,9 @@
+public class Test {
+  public static void main(long[] a) {
+    if(a.length<3)
+      return;
+    for(int i=0; i<a.length; i++) {
+      a[i]=(long)i;
+    }
+  }
+}

regression/cbmc-java/json_trace3/Test.java

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--cover location --trace --json-ui --unwind 5
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"lhs": "dynamic_2_array\[1L\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "15",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "6"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
+--
+"name": "unknown"
+^warning: ignoring

regression/cbmc-java/json_trace3/test.desc

@@ -705,7 +705,7 @@ void goto_convertt::do_java_new_array(
   else
     allocate_data_type=data.type();
 
-  side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, allocate_data_type);
+  side_effect_exprt data_java_new_expr(ID_java_new_array, allocate_data_type);
 
   // The instruction may specify a (hopefully small) upper bound on the
   // array size, in which case we allocate a fixed-length array that may
@@ -714,29 +714,29 @@ void goto_convertt::do_java_new_array(
   // backend.
   const irept size_bound=rhs.find(ID_length_upper_bound);
   if(size_bound.is_nil())
-    data_cpp_new_expr.set(ID_size, rhs.op0());
+    data_java_new_expr.set(ID_size, rhs.op0());
   else
-    data_cpp_new_expr.set(ID_size, size_bound);
+    data_java_new_expr.set(ID_size, size_bound);
 
   // Must directly assign the new array to a temporary
   // because goto-symex will notice `x=side_effect_exprt` but not
   // `x=typecast_exprt(side_effect_exprt(...))`
   symbol_exprt new_array_data_symbol=
     new_tmp_symbol(
-      data_cpp_new_expr.type(),
+      data_java_new_expr.type(),
       "new_array_data",
       dest,
       location)
     .symbol_expr();
   goto_programt::targett t_p2=dest.add_instruction(ASSIGN);
-  t_p2->code=code_assignt(new_array_data_symbol, data_cpp_new_expr);
+  t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr);
   t_p2->source_location=location;
 
   goto_programt::targett t_p=dest.add_instruction(ASSIGN);
-  exprt cast_cpp_new=new_array_data_symbol;
-  if(cast_cpp_new.type()!=data.type())
-    cast_cpp_new=typecast_exprt(cast_cpp_new, data.type());
-  t_p->code=code_assignt(data, cast_cpp_new);
+  exprt cast_java_new=new_array_data_symbol;
+  if(cast_java_new.type()!=data.type())
+    cast_java_new=typecast_exprt(cast_java_new, data.type());
+  t_p->code=code_assignt(data, cast_java_new);
   t_p->source_location=location;
 
   // zero-initialize the data

src/goto-programs/builtin_functions.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/invariant.h>
+#include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -64,42 +65,11 @@ void remove_pointer_offsets(exprt &src, const symbol_exprt &array_symbol)
       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)
+exprt simplify_array_access(const exprt &src, const namespacet &ns)
 {
   if(src.id()==ID_index && to_index_expr(src).array().id()==ID_symbol)
   {
@@ -108,6 +78,7 @@ exprt simplify_array_access(const exprt &src)
     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)
@@ -117,8 +88,10 @@ exprt simplify_array_access(const exprt &src)
     remove_pointer_offsets(index);
 
     // We look for an actual integer value for the index
-    std::size_t i;
-    if(!simplify_index(index, i))
+    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;
@@ -196,7 +169,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);
+        exprt simplified=simplify_array_access(step.full_lhs, ns);
         full_lhs_string=from_expr(ns, identifier, simplified);
 
         const symbolt *symbol;
@@ -210,7 +183,8 @@ 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);
+          exprt simplified=simplify_array_access(step.full_lhs_value, ns);
+
           full_lhs_value=json(simplified, ns, symbol->mode);
         }
         else

src/goto-programs/json_goto_trace.cpp

@@ -60,7 +60,8 @@ void goto_symext::symex_assign(
       throw "symex_assign: unexpected function call: "+id2string(identifier);
     }
     else if(statement==ID_cpp_new ||
-            statement==ID_cpp_new_array)
+            statement==ID_cpp_new_array ||
+            statement==ID_java_new_array)
       symex_cpp_new(state, lhs, side_effect_expr);
     else if(statement==ID_malloc)
       symex_malloc(state, lhs, side_effect_expr);

src/goto-symex/symex_assign.cpp

@@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/prefix.h>
 #include <util/string2int.h>
-
+#include <util/invariant_utils.h>
 #include <util/c_types.h>
 
 #include <linking/zero_initializer.h>
@@ -361,6 +361,11 @@ void goto_symext::symex_output(
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }
 
+/// Handles side effects of type 'new' for C++ and 'new array'
+/// for C++ and Java language modes
+/// \param state: Symex state
+/// \param lhs: left-hand side of assignment
+/// \param code: right-hand side containing side effect
 void goto_symext::symex_cpp_new(
   statet &state,
   const exprt &lhs,
@@ -371,7 +376,8 @@ void goto_symext::symex_cpp_new(
   if(code.type().id()!=ID_pointer)
     throw "new expected to return pointer";
 
-  do_array=(code.get(ID_statement)==ID_cpp_new_array);
+  do_array=(code.get(ID_statement)==ID_cpp_new_array ||
+            code.get(ID_statement)==ID_java_new_array);
 
   dynamic_counter++;
 
@@ -384,7 +390,13 @@ void goto_symext::symex_cpp_new(
              "dynamic_"+count_string+"_value";
   symbol.name="symex_dynamic::"+id2string(symbol.base_name);
   symbol.is_lvalue=true;
-  symbol.mode=ID_cpp;
+  if(code.get(ID_statement)==ID_cpp_new_array ||
+     code.get(ID_statement)==ID_cpp_new)
+    symbol.mode=ID_cpp;
+  else if(code.get(ID_statement)==ID_java_new_array)
+    symbol.mode=ID_java;
+  else
+    INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
 
   if(do_array)
   {
@@ -397,7 +409,6 @@ void goto_symext::symex_cpp_new(
   else
     symbol.type=code.type().subtype();
 
-  // symbol.type.set("#active", symbol_expr(active_symbol));
   symbol.type.set("#dynamic", true);
 
   new_symbol_table.add(symbol);
@@ -425,7 +436,10 @@ void goto_symext::symex_cpp_delete(
   statet &state,
   const codet &code)
 {
-  // bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
+  // TODO
+  #if 0
+  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
+  #endif
 }
 
 void goto_symext::symex_trace(