Merge pull request #2917 from mgudemann/fix/interpreter/null_pointer_no_operand

Support null-pointer without operand in interpreter

Author: Matthias Güdemann

src/goto-programs/interpreter.cpp

@@ -600,7 +600,7 @@ exprt interpretert::get_value(
   {
     return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
   }
-  else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of))
+  else if(real_type.id() == ID_pointer)
   {
     if(rhs[integer2size_t(offset)]==0)
     {
@@ -1090,4 +1090,3 @@ void interpreter(
     message_handler);
   interpreter();
 }
-

src/goto-programs/interpreter_class.h

@@ -306,6 +306,8 @@ class interpretert:public messaget
 
   void initialize(bool init);
   void show_state();
+
+  friend class interpreter_testt;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H

src/goto-programs/interpreter_evaluate.cpp

@@ -330,16 +330,23 @@ void interpretert::evaluate(
 
       dest.clear();
     }
-    else if((expr.type().id()==ID_pointer)
-         || (expr.type().id()==ID_address_of))
+    else if(expr.type().id() == ID_pointer)
     {
       mp_integer i=0;
       if(expr.has_operands() && expr.op0().id()==ID_address_of)
       {
         evaluate(expr.op0(), dest);
         return;
       }
-      if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(expr.has_operands() && !to_integer(expr.op0(), i))
+      {
+        dest.push_back(i);
+        return;
+      }
+      // check if expression is constant null pointer without operands
+      else if(
+        !expr.has_operands() && !to_integer(to_constant_expr(expr), i) &&
+        i.is_zero())
       {
         dest.push_back(i);
         return;

src/solvers/refinement/string_builtin_function.h

@@ -83,7 +83,7 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
     array_string_exprt input)
     : string_builtin_functiont(std::move(return_code)),
       result(std::move(result)),
-      input(std::move(result))
+      input(std::move(input))
   {
   }
 

unit/Makefile

@@ -45,6 +45,7 @@ SRC += unit_tests.cpp \
        util/symbol_table.cpp \
        util/unicode.cpp \
        catch_example.cpp \
+       interpreter/interpreter.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.

unit/interpreter/interpreter.cpp

@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+ Module: Interpreter unit tests.
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/interpreter_class.h>
+#include <util/message.h>
+#include <util/mp_arith.h>
+#include <util/namespace.h>
+
+typedef interpretert::mp_vectort mp_vectort;
+
+class interpreter_testt
+{
+  symbol_tablet symbol_table;
+  goto_functionst goto_functions;
+  null_message_handlert null_message_handler;
+  interpretert interpreter;
+
+public:
+  explicit interpreter_testt()
+    : interpreter(symbol_table, goto_functions, null_message_handler)
+  {
+  }
+
+  mp_vectort evaluate(const exprt &expression)
+  {
+    mp_vectort result;
+    interpreter.evaluate(expression, result);
+    return result;
+  }
+};
+
+SCENARIO("interpreter evaluation null pointer expressions")
+{
+  interpreter_testt interpreter_test;
+  mp_vectort null_vector = {0};
+
+  THEN("null pointer without operands")
+  {
+    unsignedbv_typet java_char(16);
+    pointer_typet pointer_type(java_char, 64);
+
+    constant_exprt constant_expr(ID_NULL, pointer_type);
+
+    mp_vectort mp_vector = interpreter_test.evaluate(constant_expr);
+
+    REQUIRE_THAT(mp_vector, Catch::Equals(null_vector));
+  }
+  THEN("null pointer with operands")
+  {
+    pointer_typet outer_pointer_type(empty_typet(), 64);
+    constant_exprt outer_expression(
+      "0000000000000000000000000000000000000000000000000000000000000000",
+      outer_pointer_type);
+
+    pointer_typet inner_pointer_type(empty_typet(), 64);
+    constant_exprt inner_expression(ID_NULL, inner_pointer_type);
+
+    outer_expression.move_to_operands(inner_expression);
+
+    mp_vectort mp_vector = interpreter_test.evaluate(outer_expression);
+
+    REQUIRE_THAT(mp_vector, Catch::Equals(null_vector));
+  }
+}

unit/interpreter/module_dependencies.txt

@@ -0,0 +1,3 @@
+goto-programs
+testing-utils
+util