Merge pull request #3826 from smowton/smowton/fix/json-expr-simplify-pointers

Fix json_expr simplification of pointers

Author: smowton

.travis.yml

@@ -96,6 +96,7 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -130,6 +131,7 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -158,6 +160,7 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -186,6 +189,7 @@ jobs:
             - clang-7
             - libstdc++-5-dev
             - libubsan0
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -212,6 +216,7 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -238,6 +243,7 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-7
+            - jq
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-7 bin/gcc
@@ -270,6 +276,7 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
+            - jq
       before_install:
         - mkdir bin
         # Use gcc/g++ 5 for tests, as Clang doesn't work yet

buildspec-windows.yml

@@ -4,7 +4,7 @@ phases:
   install:
     commands:
       - choco install cyg-get -y --no-progress
-      - cyg-get bash patch bison flex make wget perl
+      - cyg-get bash patch bison flex make wget perl jq
       - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
 
   build:

buildspec.yml

@@ -8,7 +8,7 @@ phases:
       - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
       - add-apt-repository ppa:openjdk-r/ppa -y
       - apt-get update -y
-      - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386
+      - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq
       - apt-get install -y openjdk-8-jdk
       - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
       - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1

jbmc/regression/CMakeLists.txt

@@ -12,3 +12,4 @@ add_subdirectory(janalyzer-taint)
 add_subdirectory(jbmc-concurrency)
 add_subdirectory(jbmc-inheritance)
 add_subdirectory(jbmc-generics)
+add_subdirectory(jbmc-json-ui)

jbmc/regression/Makefile

@@ -6,6 +6,7 @@ DIRS = janalyzer \
        jbmc \
        jbmc-concurrency \
        jbmc-inheritance \
+       jbmc-json-ui \
        jbmc-strings \
        jdiff \
        strings-smoke-tests \

jbmc/regression/jbmc-json-ui/CMakeLists.txt

@@ -0,0 +1,9 @@
+find_program(JQ jq)
+if(NOT JQ)
+  message("Skipping JBMC JSON-UI tests: couldn't find jq in your path")
+else()
+  add_test_pl_tests(
+      "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:jbmc>"
+  )
+endif()
+

jbmc/regression/jbmc-json-ui/Makefile

@@ -0,0 +1,37 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+ifeq (, $(shell which jq))
+	echo "JBMC JSON-UI tests skipped (can't find 'jq' in your path)"
+else
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../chain.sh ../../../src/jbmc/jbmc"
+endif
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl test
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log tests-symex-driven-loading.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

jbmc/regression/jbmc-json-ui/chain.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+JBMC_PATH=$1
+shift
+
+JQ_COMMAND=$1
+shift
+
+$JBMC_PATH "$@" | jq -c "$JQ_COMMAND"

jbmc/regression/jbmc-json-ui/pointer-simplification/test.class

@@ -0,0 +1,12 @@
+CORE
+test.class
+'.[] | select(has("result")) | .result | .[] | select(has("trace")) | .trace | .[] | select(has("value")) | .value | select(.name == "pointer") | {has_data: has("data")}' --json-ui --trace
+^EXIT=0$
+^SIGNAL=0$
+\{"has_data":true\}
+--
+\{"has_data":false\}
+--
+This checks that all pointer assignments in the test program have a "data" entry,
+which is given when json_expr can determine what object is referenced on the RHS
+(e.g. x = &dynamic_object1.@some_subclass yields "data": "dynamic_object1" in the trace)

jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc

@@ -0,0 +1,12 @@
+public class test {
+
+  public static void main(String[] args) {
+
+    test t = new test();
+    test[] ts = new test[1];
+    ts[0] = t;
+    assert ts[0] == null;
+
+  }
+
+}

jbmc/regression/jbmc-json-ui/pointer-simplification/test.java

@@ -14,6 +14,7 @@ Author: Peter Schrammel
 #include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/expr.h>
+#include <util/expr_util.h>
 #include <util/fixedbv.h>
 #include <util/identifier.h>
 #include <util/ieee_float.h>
@@ -46,27 +47,35 @@ static exprt simplify_json_expr(const exprt &src)
       }
     }
   }
-  else if(
-    src.id() == ID_address_of &&
-    to_address_of_expr(src).object().id() == ID_member &&
-    id2string(
-      to_member_expr(to_address_of_expr(src).object()).get_component_name())
-        .find("@") != std::string::npos)
+  else if(src.id() == ID_typecast)
   {
-    // simplify expressions of the form &member_expr(object, @class_identifier)
-    return simplify_json_expr(to_address_of_expr(src).object());
+    return simplify_json_expr(to_typecast_expr(src).op());
   }
-  else if(
-    src.id() == ID_address_of &&
-    to_address_of_expr(src).object().id() == ID_index &&
-    to_index_expr(to_address_of_expr(src).object()).index().id() ==
-      ID_constant &&
-    to_constant_expr(to_index_expr(to_address_of_expr(src).object()).index())
-      .value_is_zero_string())
+  else if(src.id() == ID_address_of)
   {
-    // simplify expressions of the form  &array[0]
-    return simplify_json_expr(
-      to_index_expr(to_address_of_expr(src).object()).array());
+    const exprt &object = skip_typecast(to_address_of_expr(src).object());
+
+    if(object.id() == ID_symbol)
+    {
+      // simplify expressions of the form &symbol
+      return simplify_json_expr(object);
+    }
+    else if(
+      object.id() == ID_member &&
+      id2string(to_member_expr(object).get_component_name()).find("@") !=
+      std::string::npos)
+    {
+      // simplify expressions of the form &member(object, @class_identifier)
+      return simplify_json_expr(object);
+    }
+    else if(
+      object.id() == ID_index &&
+      to_index_expr(object).index().id() == ID_constant &&
+      to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
+    {
+      // simplify expressions of the form  &array[0]
+      return simplify_json_expr(to_index_expr(object).array());
+    }
   }
   else if(
     src.id() == ID_member &&