Merge pull request diffblue#493 from diffblue/merge-cbmc-develop-2018-07-06

Merge cbmc develop 2018 07 06

Author: smowton

cbmc/CMakeLists.txt

@@ -42,48 +42,6 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
-# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
-find_package(Git)
-if(GIT_FOUND)
-  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
-    "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
-      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
-    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
-    execute_process(
-      COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
-      OUTPUT_VARIABLE GIT_INFO
-      OUTPUT_STRIP_TRAILING_WHITESPACE
-    )
-    configure_file(\${CUR}/version.h.in version.h)
-    "
-  )
-else()
-  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
-    "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
-      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
-    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
-    set(GIT_INFO \"n/a\")
-    configure_file(\${CUR}/version.h.in version.h)
-    "
-  )
-endif()
-
-macro(git_revision target)
-  file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
-    "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
-  add_custom_target(
-    ${target}-version.h
-    COMMAND ${CMAKE_COMMAND}
-      -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
-      -D CUR=${CMAKE_CURRENT_BINARY_DIR}
-      -P ${CMAKE_BINARY_DIR}/version.cmake
-  )
- add_dependencies(${target} ${target}-version.h)
-endmacro()
-include_directories(${CMAKE_CURRENT_BINARY_DIR})
-
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)

cbmc/appveyor.yml

@@ -2,7 +2,6 @@ version: 1.0.{build}
 image: Visual Studio 2013
 clone_depth: 50
 environment:
-  BUILD_ENV: MSVC
   PATH: C:\projects\cbmc\deps\bin;%PATH%
   INCLUDE: C:\projects\cbmc\deps\include
 install:
@@ -57,9 +56,8 @@ build_script:
     cp -r deps/minisat2-2.2.1 minisat-2.2.1
     patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64
-    sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
-    make -C src -j2
-    make -C jbmc/src -j2
+    make -C src -j2 BUILD_ENV=MSVC
+    make -C jbmc/src -j2 BUILD_ENV=MSVC
 
 test_script:
 - cmd: |
@@ -81,10 +79,10 @@ test_script:
     rmdir /s /q goto-instrument\slice08
     cd ..
 
-    make -C regression test
+    make -C regression test BUILD_ENV=MSVC
 
-    make -C unit all -j2
-    make -C unit test
+    make -C unit all -j2 BUILD_ENV=MSVC
+    make -C unit test BUILD_ENV=MSVC
 
     cd jbmc/regression
     rmdir /s /q jbmc\VarLengthArrayTrace1
@@ -93,7 +91,7 @@ test_script:
     rmdir /s /q jbmc\tableswitch2
     cd ../..
 
-    make -C jbmc/regression test
+    make -C jbmc/regression test BUILD_ENV=MSVC
 
-    make -C jbmc/unit all -j2
-    make -C jbmc/unit test
+    make -C jbmc/unit all -j2 BUILD_ENV=MSVC
+    make -C jbmc/unit test BUILD_ENV=MSVC

cbmc/buildspec-windows.yml

@@ -8,20 +8,19 @@ phases:
 
   build:
     commands:
-      - 'C:\tools\cygwin\bin\sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc'
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         C:\tools\cygwin\bin\bash -c "make -C src minisat2-download DOWNLOADER=wget"
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C src" '
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C unit all" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C src BUILD_ENV=MSVC" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C unit all BUILD_ENV=MSVC" '
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src" '
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all BUILD_ENV=MSVC ; exit 0" '
 
   post_build:
     commands:
@@ -49,19 +48,19 @@ phases:
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC ; exit 0" '
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC ; exit 0" '
 
 artifacts:
   files:

cbmc/jbmc/src/janalyzer/CMakeLists.txt

@@ -24,5 +24,3 @@ target_link_libraries(janalyzer-lib
 # Executable
 add_executable(janalyzer janalyzer_main.cpp)
 target_link_libraries(janalyzer janalyzer-lib)
-
-git_revision(janalyzer-lib)

cbmc/jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -49,15 +49,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 #include <util/options.h>
 #include <util/unicode.h>
+#include <util/version.h>
 
 #include <goto-analyzer/static_show_domain.h>
 #include <goto-analyzer/static_simplifier.h>
 #include <goto-analyzer/static_verifier.h>
 #include <goto-analyzer/taint_analysis.h>
 #include <goto-analyzer/unreachable_instructions.h>
 
-#include "version.h"
-
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JANALYZER_OPTIONS, argc, argv),
     messaget(ui_message_handler),

cbmc/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -276,6 +276,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set(ID_interface, c.is_interface);
   class_type.set(ID_synthetic, c.is_synthetic);
   class_type.set_final(c.is_final);
+  class_type.set_is_inner_class(c.is_inner_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)

cbmc/jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -217,6 +217,7 @@ class java_bytecode_parse_treet
     bool is_interface = false;
     bool is_synthetic = false;
     bool is_annotation = false;
+    bool is_inner_class = false;
     bool attribute_bootstrapmethods_read = false;
     size_t enum_elements=0;
 

cbmc/jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -119,6 +119,8 @@ class java_bytecode_parsert:public parsert
   void rfields(classt &parsed_class);
   void rmethods(classt &parsed_class);
   void rmethod(classt &parsed_class);
+  void
+  rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -1576,6 +1578,77 @@ void java_bytecode_parsert::relement_value_pair(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.6
+/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6
+/// Parses the InnerClasses attribute for the current parsed class,
+/// which contains an array of information about its inner classes. We are
+/// interested in getting information only for inner classes, which is
+/// determined by checking if the parsed class matches any of the inner classes
+/// in its inner class array. If the parsed class is not an inner class, then it
+/// is ignored. When a parsed class is an inner class, the accessibility
+/// information for the parsed class is overwritten, and the parsed class is
+/// marked as an inner class.
+void java_bytecode_parsert::rinner_classes_attribute(
+  classt &parsed_class,
+  const u4 &attribute_length)
+{
+  std::string name = parsed_class.name.c_str();
+  u2 number_of_classes = read_u2();
+  u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+  INVARIANT(
+    number_of_bytes_to_be_read == attribute_length,
+    "The number of bytes to be read for the InnerClasses attribute does not "
+    "match the attribute length.");
+
+  const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & {
+    return pool_entry(index);
+  };
+  const auto remove_separator_char = [](std::string str, char ch) {
+    str.erase(std::remove(str.begin(), str.end(), ch), str.end());
+    return str;
+  };
+
+  for(int i = 0; i < number_of_classes; i++)
+  {
+    u2 inner_class_info_index = read_u2();
+    u2 outer_class_info_index = read_u2();
+    UNUSED u2 inner_name_index = read_u2();
+    u2 inner_class_access_flags = read_u2();
+
+    std::string inner_class_info_name =
+      class_infot(pool_entry(inner_class_info_index))
+        .get_name(pool_entry_lambda);
+    bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0;
+    bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0;
+    bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0;
+
+    // If the original parsed class name matches the inner class name,
+    // the parsed class is an inner class, so overwrite the parsed class'
+    // access information and mark it as an inner class.
+    bool is_inner_class = remove_separator_char(id2string(parsed_class.name), '.') ==
+      remove_separator_char(inner_class_info_name, '/');
+    if(is_inner_class)
+      parsed_class.is_inner_class = is_inner_class;
+    if(!is_inner_class)
+      continue;
+    // Note that if outer_class_info_index == 0, the inner class is an anonymous
+    // or local class, and is treated as private.
+    if(outer_class_info_index == 0)
+    {
+      parsed_class.is_private = true;
+      parsed_class.is_protected = false;
+      parsed_class.is_public = false;
+    }
+    else
+    {
+      parsed_class.is_private = is_private;
+      parsed_class.is_protected = is_protected;
+      parsed_class.is_public = is_public;
+    }
+  }
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();
@@ -1640,6 +1713,11 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
     parsed_class.attribute_bootstrapmethods_read = true;
     read_bootstrapmethods_entry(parsed_class);
   }
+  else if(attribute_name == "InnerClasses")
+  {
+    java_bytecode_parsert::rinner_classes_attribute(
+      parsed_class, attribute_length);
+  }
   else
     skip_bytes(attribute_length);
 }

cbmc/jbmc/src/java_bytecode/java_types.h

@@ -111,6 +111,16 @@ class java_class_typet:public class_typet
     return set(ID_access, access);
   }
 
+  const bool get_is_inner_class() const
+  {
+    return get_bool(ID_is_inner_class);
+  }
+
+  void set_is_inner_class(const bool &is_inner_class)
+  {
+    return set(ID_is_inner_class, is_inner_class);
+  }
+
   bool get_final()
   {
     return get_bool(ID_final);

cbmc/jbmc/src/jbmc/CMakeLists.txt

@@ -34,5 +34,3 @@ add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)
 
 install(TARGETS jbmc DESTINATION bin)
-
-git_revision(jbmc-lib)

cbmc/jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -16,10 +16,11 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>
 
-#include <util/exit_codes.h>
 #include <util/config.h>
-#include <util/unicode.h>
+#include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/unicode.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -60,8 +61,6 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/replace_java_nondet.h>
 #include <java_bytecode/simple_method_stubbing.h>
 
-#include "version.h"
-
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(JBMC_OPTIONS, argc, argv),
   messaget(ui_message_handler),

cbmc/jbmc/src/jdiff/CMakeLists.txt

@@ -26,5 +26,3 @@ target_link_libraries(jdiff-lib
 # Executable
 add_executable(jdiff jdiff_main.cpp)
 target_link_libraries(jdiff jdiff-lib)
-
-git_revision(jdiff-lib)

cbmc/jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -20,6 +20,7 @@ Author: Peter Schrammel
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/options.h>
+#include <util/version.h>
 
 #include <langapi/language.h>
 
@@ -60,8 +61,6 @@ Author: Peter Schrammel
 #include <goto-diff/goto_diff.h>
 #include <goto-diff/unified_diff.h>
 
-#include "version.h"
-
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JDIFF_OPTIONS, argc, argv),
     jdiff_languagest(cmdline, ui_message_handler),

cbmc/jbmc/unit/Makefile

@@ -12,6 +12,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \