JSON code cleanup

src/cbmc/bmc_cover.cpp

@@ -394,7 +394,8 @@ bool bmc_covert::operator()()
               json_objectt json_input;
               json_input["id"]=json_stringt(id2string(step.io_id));
               if(step.io_args.size()==1)
-                json_input["value"]=json(step.io_args.front(), bmc.ns);
+                json_input["value"]=
+                  json(step.io_args.front(), bmc.ns, ID_unknown);
               json_test.push_back(json_input);
             }
           }

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);
         }
@@ -192,7 +116,7 @@ void convert(
           DATA_INVARIANT(
             step.full_lhs_value.is_not_nil(),
             "full_lhs_value in assignment must not be nil");
-          full_lhs_value=json(step.full_lhs_value, ns);
+          full_lhs_value=json(step.full_lhs_value, ns, ID_unknown);
         }
 
         json_assignment["value"]=full_lhs_value;

src/symex/symex_cover.cpp

@@ -164,7 +164,8 @@ void symex_parse_optionst::report_cover(
                 json_objectt json_input;
                 json_input["id"]=json_stringt(id2string(step.io_id));
                 if(step.io_args.size()==1)
-                  json_input["value"]=json(step.io_args.front(), ns);
+                  json_input["value"]=
+                    json(step.io_args.front(), ns, ID_unknown);
                 json_test.push_back(json_input);
               }
             }

src/util/json_expr.h

@@ -23,12 +23,12 @@ class namespacet;
 json_objectt json(
   const exprt &,
   const namespacet &,
-  const irep_idt &mode=ID_unknown);
+  const irep_idt &mode);
 
 json_objectt json(
   const typet &,
   const namespacet &,
-  const irep_idt &mode=ID_unknown);
+  const irep_idt &mode);
 
 json_objectt json(const source_locationt &);
 

src/util/simplify_expr_pointer.cpp

@@ -375,14 +375,41 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
     return false;
   }
-  else if(ptr.id()==ID_constant &&
-          ptr.get(ID_value)==ID_NULL)
+  else if(ptr.id()==ID_constant)
   {
-    expr=from_integer(0, expr.type());
+    constant_exprt &c_ptr=to_constant_expr(ptr);
 
-    simplify_node(expr);
+    if(c_ptr.get_value()==ID_NULL ||
+       c_ptr.value_is_zero_string())
+    {
+      expr=from_integer(0, expr.type());
 
-    return false;
+      simplify_node(expr);
+
+      return false;
+    }
+    else
+    {
+      // this is a pointer, we can't use to_integer
+      mp_integer number=binary2integer(id2string(c_ptr.get_value()), false);
+      // a null pointer would have been caught above, return value 0
+      // will indicate that conversion failed
+      if(number==0)
+        return true;
+
+      // The constant address consists of OBJECT-ID || OFFSET.
+      mp_integer offset_bits=
+        pointer_offset_bits(ptr.type(), ns)-config.bv_encoding.object_bits;
+      number%=power(2, offset_bits);
+
+      expr=from_integer(number, expr.type());
+
+      simplify_node(expr);
+
+      return false;
+    }
+
+    return true;
   }
 
   return true;

unit/Makefile

@@ -5,9 +5,6 @@ SRC = src/expr/require_expr.cpp \
       src/ansi-c/c_to_expr.cpp \
       unit_tests.cpp \
       catch_example.cpp \
-      util/expr_iterator.cpp \
-      analyses/call_graph.cpp \
-      java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
       # Empty last line
 
 # Test source files
@@ -23,8 +20,10 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
-       solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
+       solvers/refinement/string_refinement/substitute_array_list.cpp \
+       util/expr_iterator.cpp \
+       util/simplify_expr.cpp \
        catch_example.cpp \
        # Empty last line
 

unit/util/simplify_expr.cpp

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+ Module: Unit tests of the expression simplifier
+
+ Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+TEST_CASE("Simplify pointer_offset(address of array index)")
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  array_typet array_type(char_type(), from_integer(2, size_type()));
+  symbol_exprt array("A", array_type);
+  index_exprt index(array, from_integer(1, index_type()));
+  address_of_exprt address_of(index);
+
+  exprt p_o=pointer_offset(address_of);
+
+  exprt simp=simplify_expr(p_o, ns);
+
+  REQUIRE(simp.id()==ID_constant);
+  mp_integer offset_value;
+  REQUIRE(!to_integer(simp, offset_value));
+  REQUIRE(offset_value==1);
+}
+
+TEST_CASE("Simplify const pointer offset")
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  // build a numeric constant of some pointer type
+  constant_exprt number=from_integer(1234, size_type());
+  number.type()=pointer_type(char_type());
+
+  exprt p_o=pointer_offset(number);
+
+  exprt simp=simplify_expr(p_o, ns);
+
+  REQUIRE(simp.id()==ID_constant);
+  mp_integer offset_value;
+  REQUIRE(!to_integer(simp, offset_value));
+  REQUIRE(offset_value==1234);
+}