Squashed 'cbmc/' changes from f90ed9e..6409eae

6409eae Merge pull request diffblue#2449 from tautschnig/c++-template-cleanup
1134455 Merge pull request diffblue#2443 from tautschnig/vs-rdecl
6e9e655 Merge pull request diffblue#2520 from smowton/smowton/feature/constant-propagator-selectivity
9013779 Merge pull request diffblue#2383 from tautschnig/no-sed
56a487e Constant propagator: add callback to filter tracked values
a354513 Merge pull request diffblue#2510 from polgreen/hex_trace
3545be4 Merge pull request diffblue#2523 from peterschrammel/do-not-ignore-full-slice
819c683 Merge pull request diffblue#2493 from jeannielynnmoulton/jeannie/InnerClasses
a018652 allow unsigned long instead of unsigned in regression test for hex_trace
d5bbdd8 represent numerical values in CBMC trace in hex
19bddce Do not ignore --full-slice
5350133 Refactor inner class parsing.
6e554d9 Merge pull request diffblue#2500 from diffblue/git-version-speedup
9ba55e2 Marks anonymous classes as inner classes
b96c7ba move build commands for version.h from common to util/
6ce7b13 Clarifies language in documentation.
c0c1029 Fixes parsing for anonymous classes
1930aef Refactors parsing of inner classes attribute.
b28562b Adds unit test for parsing inner classes.
c336455 Stores inner class data in java class types.
457bac9 Parses InnerClasses attribute of java bytecode.
34bd58f Clean up unused template instantiation symbols
fea1f47 Remove unused parameter from rDeclarator
e00c6ee Set BUILD_ENV via make variable instead of patching via sed

git-subtree-dir: cbmc
git-subtree-split: 6409eae

Author: smowton

CMakeLists.txt

@@ -39,48 +39,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)

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

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:

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)

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),

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)

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;
 

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);
 }

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);

jbmc/src/jbmc/CMakeLists.txt

@@ -29,5 +29,3 @@ target_link_libraries(jbmc-lib
 # Executable
 add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)
-
-git_revision(jbmc-lib)

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),

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)

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),

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 \