Squashed 'cbmc/' changes from 54f3731..6a10f1a

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline
96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8
1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports)
c157ba7 Revert "CMake version.cpp: switch back to add_custom_target"
7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache
63652fc add clcache to Windows build
6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp
35d09d5 CMake version.cpp: switch back to add_custom_target
80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string
7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep
ad5c375 use a string instead of macro for version number
b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats
eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type
c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only
0855872 Address review comments diffblue#2
eaa7664 Wrap lines properly
e682eb9 Add \ref in lots of places
3023cca Address review comments
758f069 Move dstringt documentation to above dstringt
a54c82d Move documentation of irept to be above irept
b827ea4 Use type equality check in unit tests
77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2
1f4ef40 Add class loader debug output
4ae8eb6 Move sharing map friends declarations to unit tests
186897c Sharing stats for the sharing map
4438b43 Fix sharing map internal assertion
332febe Remove wrong sharing map internal assertions
be7e140 Activate internal checks for the sharing map unit tests
713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map
87f90ee Add replace_all string utility
ea2d393 Make test work on windows
4fa9943 Make array element type be not a comment
655248a Add unit test for when there are no exceptions.
a6e7c4b Refactors interface for exceptions to not use irepts.
1134bba Creates java_method_typet which extends code_typet
aa83622 Unit tests method get_super_class
565c999 Unit tests throws exceptions parsing.
eb88509 Use parsed information for thrown exceptions.
5c7dcac Parses the exception attribute
7fcc42d Adds const to get/set_outer_class
5994dd8 Add method to get super class from java class type.
fbad2d9 Rename variable extends to super_class
6d0776f if function is not in the function map, treat as if it has no body
da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok
0202f34 refactor pointer_validity_check using address_check
4a24ad4 use __CPROVER_r/w_ok in string.c library
732ce2a expand __CPROVER_r/w_ok in goto_check
acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end
0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions
5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64
7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression
44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening
f74c161 test for __float80 and __float128
8288a72 __float80 is a typedef, not a keyword
5495625 FreeBSD: default flavor is now CLANG
e63402e added _Null_unspecified clang extension
16a49a7 bugfix: __float128
3849bb0 rename APPLE flavor to CLANG
060b59c separate pointer check for integer addresses
9b5847e fix flattening of ID_invalid_pointer
432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked.
cbfcc5c added support for _int64 keyword
0148347 Avoid signed/unsigned casts and conversion in goto_inline

git-subtree-dir: cbmc
git-subtree-split: 6a10f1a

Author: NathanJPhillips

.gitignore

@@ -28,7 +28,7 @@ Release/*
 *.obj
 *.a
 *.lib
-version.h
+util/version.cpp
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_builtin_headers.inc

buildspec-windows.yml

@@ -5,6 +5,7 @@ phases:
     commands:
       - choco install cyg-get -y --no-progress
       - cyg-get bash patch bison flex make wget perl
+      - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
 
   build:
     commands:
@@ -13,14 +14,22 @@ phases:
         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 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;c:\tools\clcache\clcache-4.1.0;$env:Path"
+        $env:CLCACHE_DIR = "C:\clcache"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make CXX=clcache.exe -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 CXX=clcache.exe -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 setup-submodules" && 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" '
+        $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path"
+        $env:CLCACHE_DIR = "C:\clcache"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make CXX=clcache.exe -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 CXX=clcache.exe -j4 -C jbmc/unit all BUILD_ENV=MSVC" '
+
+      - |
+        # display cache stats
+        $env:Path = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$env:Path"
+        $env:CLCACHE_DIR = "C:\clcache"
+        cmd /c 'clcache -s'
 
   post_build:
     commands:
@@ -72,3 +81,4 @@ artifacts:
 
 cache:
   paths:
+    - 'c:\clcache'

doc/cbmc-user-manual.md

@@ -2190,6 +2190,15 @@ to the program. If the expression evaluates to false, the execution
 aborts without failure. More detail on the use of assumptions is in the
 section on [Assumptions and Assertions](modeling-assertions.shtml).
 
+#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
+
+    void __CPROVER_r_ok(const void *, size_t size);
+    void __CPROVER_w_ok(cosnt void *, size_t size);
+
+The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
+memory starting at the given pointer with the given size is safe.
+**\_\_CPROVER\_w_ok** does the same with writing.
+
 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
 
     _Bool __CPROVER_same_object(const void *, const void *);

jbmc/lib/java-models-library

@@ -60,7 +60,7 @@ Author: Daniel Kroening, [email protected]
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JANALYZER_OPTIONS, argc, argv),
     messaget(ui_message_handler),
-    ui_message_handler(cmdline, "JANALYZER " CBMC_VERSION)
+    ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
 {
 }
 
@@ -342,7 +342,7 @@ int janalyzer_parse_optionst::doit()
   //
   // Print a banner
   //
-  status() << "JANALYZER version " CBMC_VERSION " " << sizeof(void *) * 8
+  status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8
            << "-bit " << config.this_architecture() << " "
            << config.this_operating_system() << eom;
 

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -280,6 +280,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set_is_static_class(c.is_static_class);
   class_type.set_is_anonymous_class(c.is_anonymous_class);
   class_type.set_outer_class(c.outer_class);
+  class_type.set_super_class(c.super_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)
@@ -303,9 +304,9 @@ void java_bytecode_convert_classt::convert(
   else
     class_type.set_access(ID_default);
 
-  if(!c.extends.empty())
+  if(!c.super_class.empty())
   {
-    const symbol_typet base("java::" + id2string(c.extends));
+    const symbol_typet base("java::" + id2string(c.super_class));
 
     // if the superclass is generic then the class has the superclass reference
     // including the generic info in its signature
@@ -323,7 +324,7 @@ void java_bytecode_convert_classt::convert(
       }
       catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        warning() << "Superclass: " << c.extends << " of class: " << c.name
+        warning() << "Superclass: " << c.super_class << " of class: " << c.name
                   << "\n could not parse signature: " << superclass_ref.value()
                   << "\n " << e.what()
                   << "\n ignoring that the superclass is generic" << eom;
@@ -336,9 +337,9 @@ void java_bytecode_convert_classt::convert(
     }
     class_typet::componentt base_class_field;
     base_class_field.type() = class_type.bases().at(0).type();
-    base_class_field.set_name("@"+id2string(c.extends));
-    base_class_field.set_base_name("@"+id2string(c.extends));
-    base_class_field.set_pretty_name("@"+id2string(c.extends));
+    base_class_field.set_name("@" + id2string(c.super_class));
+    base_class_field.set_base_name("@" + id2string(c.super_class));
+    base_class_field.set_pretty_name("@" + id2string(c.super_class));
     class_type.components().push_back(base_class_field);
   }
 
@@ -561,7 +562,7 @@ void java_bytecode_convert_classt::convert(
   }
 
   // is this a root class?
-  if(c.extends.empty())
+  if(c.super_class.empty())
     java_root_class(*class_symbol);
 }
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -444,14 +444,14 @@ void java_bytecode_convert_methodt::convert(
 
   // Obtain a std::vector of code_typet::parametert objects from the
   // (function) type of the symbol
-  code_typet code_type = to_code_type(method_symbol.type);
-  code_type.set(ID_C_class, class_symbol.name);
-  method_return_type=code_type.return_type();
-  code_typet::parameterst &parameters=code_type.parameters();
+  java_method_typet method_type = to_java_method_type(method_symbol.type);
+  method_type.set(ID_C_class, class_symbol.name);
+  method_return_type = method_type.return_type();
+  code_typet::parameterst &parameters = method_type.parameters();
 
-  // Determine the number of local variable slots used by the JVM to maintan the
-  // formal parameters
-  slots_for_parameters=java_method_parameter_slots(code_type);
+  // Determine the number of local variable slots used by the JVM to maintain
+  // the formal parameters
+  slots_for_parameters = java_method_parameter_slots(method_type);
 
   debug() << "Generating codet: class "
              << class_symbol.name << ", method "
@@ -587,7 +587,10 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
-  const std::string signature_string = pretty_signature(code_type);
+  for(const auto &exception_name : m.throws_exception_table)
+    method_type.add_throws_exceptions(exception_name);
+
+  const std::string signature_string = pretty_signature(method_type);
 
   // Set up the pretty name for the method entry in the symbol table.
   // The pretty name of a constructor includes the base name of the class
@@ -601,7 +604,7 @@ void java_bytecode_convert_methodt::convert(
     method_symbol.pretty_name =
       id2string(class_symbol.pretty_name) + signature_string;
     INVARIANT(
-      code_type.get_is_constructor(),
+      method_type.get_is_constructor(),
       "Member type should have already been marked as a constructor");
   }
   else
@@ -610,14 +613,13 @@ void java_bytecode_convert_methodt::convert(
                                 id2string(m.base_name) + signature_string;
   }
 
-  method_symbol.type = code_type;
-
-  current_method=method_symbol.name;
-  method_has_this=code_type.has_this();
+  method_symbol.type = method_type;
+  current_method = method_symbol.name;
+  method_has_this = method_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
     method_symbol.value = convert_instructions(
       m,
-      code_type,
+      method_type,
       method_symbol.name,
       to_java_class_type(class_symbol.type).lambda_method_handles());
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -38,8 +38,8 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const
   }
 
   out << "class " << name;
-  if(!extends.empty())
-    out << " extends " << extends;
+  if(!super_class.empty())
+    out << " extends " << super_class;
   out << " {" << '\n';
 
   for(fieldst::const_iterator

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -114,6 +114,8 @@ struct java_bytecode_parse_treet
     typedef std::vector<exceptiont> exception_tablet;
     exception_tablet exception_table;
 
+    std::vector<irep_idt> throws_exception_table;
+
     struct local_variablet
     {
       irep_idt name;
@@ -197,7 +199,7 @@ struct java_bytecode_parse_treet
     classt &operator=(classt &&) = default;
     #endif
 
-    irep_idt name, extends;
+    irep_idt name, super_class;
     bool is_abstract=false;
     bool is_enum=false;
     bool is_public=false, is_protected=false, is_private=false;

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -121,6 +121,7 @@ class java_bytecode_parsert:public parsert
   void rmethod(classt &parsed_class);
   void
   rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
+  std::vector<irep_idt> rexceptions_attribute();
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -503,8 +504,7 @@ void java_bytecode_parsert::rClassFile()
     constant(this_class).type().get(ID_C_base_name);
 
   if(super_class!=0)
-    parsed_class.extends=
-      constant(super_class).type().get(ID_C_base_name);
+    parsed_class.super_class = constant(super_class).type().get(ID_C_base_name);
 
   rinterfaces(parsed_class);
   rfields(parsed_class);
@@ -621,8 +621,8 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
     irep_idt name=src.get(ID_C_base_name);
     if(has_prefix(id2string(name), "array["))
     {
-      const typet &element_type=
-        static_cast<const typet &>(src.find(ID_C_element_type));
+      const typet &element_type =
+        static_cast<const typet &>(src.find(ID_element_type));
       get_class_refs_rec(element_type);
     }
     else
@@ -1243,6 +1243,10 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
   {
     rRuntimeAnnotation_attribute(method.annotations);
   }
+  else if(attribute_name == "Exceptions")
+  {
+    method.throws_exception_table = rexceptions_attribute();
+  }
   else
     skip_bytes(attribute_length);
 }
@@ -1655,6 +1659,26 @@ void java_bytecode_parsert::rinner_classes_attribute(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.5
+/// https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5
+/// Parses the Exceptions attribute for the current method,
+/// and returns a vector of exceptions.
+std::vector<irep_idt> java_bytecode_parsert::rexceptions_attribute()
+{
+  u2 number_of_exceptions = read_u2();
+
+  std::vector<irep_idt> exceptions;
+  for(size_t i = 0; i < number_of_exceptions; i++)
+  {
+    u2 exception_index_table = read_u2();
+    const irep_idt exception_name =
+      constant(exception_index_table).type().get(ID_C_base_name);
+    exceptions.push_back(exception_name);
+  }
+  return exceptions;
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -24,7 +24,11 @@ void java_class_loader_limitt::setup_class_load_limit(
   // '@' signals file reading with list of class files to load
   use_regex_match = java_cp_include_files[0] != '@';
   if(use_regex_match)
+  {
     regex_matcher=std::regex(java_cp_include_files);
+    debug() << "Limit loading to classes matching '" << java_cp_include_files
+            << "'" << eom;
+  }
   else
   {
     assert(java_cp_include_files.length()>1);
@@ -54,7 +58,10 @@ bool java_class_loader_limitt::load_class_file(const std::string &file_name)
   if(use_regex_match)
   {
     std::smatch string_matches;
-    return std::regex_match(file_name, string_matches, regex_matcher);
+    if(std::regex_match(file_name, string_matches, regex_matcher))
+      return true;
+    debug() << file_name + " discarded since not matching loader regexp" << eom;
+    return false;
   }
   else
     // load .class file only if it is in the match set

jbmc/src/java_bytecode/java_class_loader_limit.cpp

@@ -1253,7 +1253,7 @@ void java_object_factoryt::allocate_nondet_length_array(
   side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
   java_new_array.copy_to_operands(length_sym_expr);
   java_new_array.set(ID_length_upper_bound, max_length_expr);
-  java_new_array.type().subtype().set(ID_C_element_type, element_type);
+  java_new_array.type().subtype().set(ID_element_type, element_type);
   code_assignt assign(lhs, java_new_array);
   assign.add_source_location()=loc;
   assignments.copy_to_operands(assign);
@@ -1277,8 +1277,8 @@ void java_object_factoryt::gen_nondet_array_init(
 
   const typet &type=ns.follow(expr.type().subtype());
   const struct_typet &struct_type=to_struct_type(type);
-  const typet &element_type=
-    static_cast<const typet &>(expr.type().subtype().find(ID_C_element_type));
+  const typet &element_type =
+    static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
 
   auto max_length_expr=from_integer(
     object_factory_parameters.max_nondet_array_length, java_int_type());

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -88,7 +88,7 @@ reference_typet java_lang_object_type()
 }
 
 /// Construct an array pointer type. It is a pointer to a symbol with identifier
-/// java::array[]. Its ID_C_element_type is set to the corresponding primitive
+/// java::array[]. Its ID_element_type is set to the corresponding primitive
 /// type, or void* for arrays of references.
 /// \param subtype Character indicating the type of array
 reference_typet java_array_type(const char subtype)
@@ -119,7 +119,7 @@ reference_typet java_array_type(const char subtype)
 
   symbol_typet symbol_type("java::"+id2string(class_name));
   symbol_type.set(ID_C_base_name, class_name);
-  symbol_type.set(ID_C_element_type, java_type_from_char(subtype));
+  symbol_type.set(ID_element_type, java_type_from_char(subtype));
 
   return java_reference_type(symbol_type);
 }
@@ -131,7 +131,7 @@ const typet &java_array_element_type(const symbol_typet &array_symbol)
   DATA_INVARIANT(
     is_java_array_tag(array_symbol.get_identifier()),
     "Symbol should have array tag");
-  return array_symbol.find_type(ID_C_element_type);
+  return array_symbol.find_type(ID_element_type);
 }
 
 /// Return a non-const reference to the element type of a given java array type
@@ -141,7 +141,7 @@ typet &java_array_element_type(symbol_typet &array_symbol)
   DATA_INVARIANT(
     is_java_array_tag(array_symbol.get_identifier()),
     "Symbol should have array tag");
-  return array_symbol.add_type(ID_C_element_type);
+  return array_symbol.add_type(ID_element_type);
 }
 
 /// Checks whether the given type is an array pointer type
@@ -555,7 +555,7 @@ typet java_type_from_string(
   case '[': // array type
     {
       // If this is a reference array, we generate a plain array[reference]
-      // with void* members, but note the real type in ID_C_element_type.
+      // with void* members, but note the real type in ID_element_type.
       if(src.size()<=1)
         return nil_typet();
       char subtype_letter=src[1];
@@ -567,7 +567,7 @@ typet java_type_from_string(
          subtype_letter=='T')   // Array of generic types
         subtype_letter='A';
       typet tmp=java_array_type(std::tolower(subtype_letter));
-      tmp.subtype().set(ID_C_element_type, subtype);
+      tmp.subtype().set(ID_element_type, subtype);
       return tmp;
     }