Merge branch 'develop' of https://github.com/diffblue/cbmc into JohnDumbell/Update-Assertion-Validation

Author: JohnDumbell

README.md

@@ -3,6 +3,8 @@
 
 [CProver Wiki](http://www.cprover.org/wiki)
 
+[CProver Documentation](http://cprover.diffblue.com)
+
 About
 =====
 

doc/architectural/cprover-architecture-overview.md

@@ -3,7 +3,7 @@
 
 \author Martin Brain, Peter Schrammel
 
-# Overview of CPROVER Directories
+\section overview-dirs Overview of CPROVER Directories
 
 ## `src/`
 
@@ -90,7 +90,7 @@ The `–help` option gives instructions for use and the
 format of the description files.
 
 
-# General Information
+\section general-info General Information
 
 First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
 how to get, build and use CBMC. This document covers the

doc/satabs-user-manual.md

@@ -1,3 +1,4 @@
+\ingroup module_hidden
 \page other_documentation Other Documentation
 
 \section satabs SATABS

regression/cbmc-java/reachability-slice/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
 1001
@@ -9,3 +9,5 @@ A.class
 --
 Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
 At the time of writing of this test, 1002 is removed.
+
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

regression/cbmc-java/reachability-slice/test2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
 1001
@@ -7,3 +7,5 @@ A.class
 1005
 --
 1004
+--
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

regression/cbmc-java/reachability-slice/test3.desc

@@ -1,8 +1,11 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --cover location
 1001
 1002
 1003
 1004
 1005
+--
+--
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -99,15 +99,21 @@ const void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
       pointer_type.subtype().get(ID_identifier) ==
       pointer_subtype_struct.get(ID_name));
 
-    const java_generic_typet &generic_pointer =
-      to_java_generic_type(pointer_type);
-
-    // If the pointer points to an incomplete class, don't treat the generics
-    if(!pointer_subtype_struct.get_bool(ID_incomplete_class))
+    // If the pointer points to:
+    // - an incomplete class or
+    // - a class that is neither generic nor implicitly generic (this
+    //  may be due to unsupported class signature)
+    // then ignore the generic types in the pointer and do not add any pairs.
+    // TODO TG-1996 should decide how mocking and generics should work
+    // together. Currently an incomplete class is never marked as generic. If
+    // this changes in TG-1996 then the condition below should be updated.
+    if(
+      !pointer_subtype_struct.get_bool(ID_incomplete_class) &&
+      (is_java_generic_class_type(pointer_subtype_struct) ||
+       is_java_implicitly_generic_class_type(pointer_subtype_struct)))
     {
-      PRECONDITION(
-        is_java_generic_class_type(pointer_subtype_struct) ||
-        is_java_implicitly_generic_class_type(pointer_subtype_struct));
+      const java_generic_typet &generic_pointer =
+        to_java_generic_type(pointer_type);
       const std::vector<java_generic_parametert> &generic_parameters =
         get_all_generic_parameters(pointer_subtype_struct);
 
@@ -135,14 +141,23 @@ const void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
   const symbol_typet &symbol_type,
   const typet &symbol_struct)
 {
-  if(is_java_generic_symbol_type(symbol_type))
+  // If the struct is:
+  // - an incomplete class or
+  // - a class that is neither generic nor implicitly generic (this
+  //  may be due to unsupported class signature)
+  // then ignore the generic types in the symbol_type and do not add any pairs.
+  // TODO TG-1996 should decide how mocking and generics should work
+  // together. Currently an incomplete class is never marked as generic. If
+  // this changes in TG-1996 then the condition below should be updated.
+  if(
+    is_java_generic_symbol_type(symbol_type) &&
+    !symbol_struct.get_bool(ID_incomplete_class) &&
+    (is_java_generic_class_type(symbol_struct) ||
+     is_java_implicitly_generic_class_type(symbol_struct)))
   {
-    java_generic_symbol_typet generic_symbol =
+    const java_generic_symbol_typet &generic_symbol =
       to_java_generic_symbol_type(symbol_type);
 
-    PRECONDITION(
-      is_java_generic_class_type(symbol_struct) ||
-      is_java_implicitly_generic_class_type(symbol_struct));
     const std::vector<java_generic_parametert> &generic_parameters =
       get_all_generic_parameters(symbol_struct);
 

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -202,10 +202,12 @@ void java_bytecode_convert_classt::convert(const classt &c)
       }
       class_type=generic_class_type;
     }
-    catch(unsupported_java_class_signature_exceptiont)
+    catch(const unsupported_java_class_signature_exceptiont &e)
     {
-      warning() << "we currently don't support parsing for example double "
-        "bounded, recursive and wild card generics" << eom;
+      warning() << "Class: " << c.name
+                << "\n could not parse signature: " << c.signature.value()
+                << "\n " << e.what() << "\n ignoring that the class is generic"
+                << eom;
     }
   }
 
@@ -253,11 +255,12 @@ void java_bytecode_convert_classt::convert(const classt &c)
           base, superclass_ref.value(), qualified_classname);
         class_type.add_base(generic_base);
       }
-      catch(unsupported_java_class_signature_exceptiont)
+      catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        debug() << "unsupported generic superclass signature "
-                << id2string(*superclass_ref)
-                << " falling back on using the descriptor" << eom;
+        warning() << "Superclass: " << c.extends << " of class: " << c.name
+                  << "\n could not parse signature: " << superclass_ref.value()
+                  << "\n " << e.what()
+                  << "\n ignoring that the superclass is generic" << eom;
         class_type.add_base(base);
       }
     }
@@ -292,11 +295,12 @@ void java_bytecode_convert_classt::convert(const classt &c)
           base, interface_ref.value(), qualified_classname);
         class_type.add_base(generic_base);
       }
-      catch(unsupported_java_class_signature_exceptiont)
+      catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        debug() << "unsupported generic interface signature "
-                << id2string(*interface_ref)
-                << " falling back on using the descriptor" << eom;
+        warning() << "Interface: " << interface << " of class: " << c.name
+                  << "\n could not parse signature: " << interface_ref.value()
+                  << "\n " << e.what()
+                  << "\n ignoring that the interface is generic" << eom;
         class_type.add_base(base);
       }
     }

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -286,18 +286,21 @@ code_typet member_type_lazy(
       }
       else
       {
-        message.warning() << "method: " << class_name << "." << method_name
-          << "\n signature: " << signature.value() << "\n descriptor: "
-          << descriptor << "\n different number of parameters, reverting to "
-          "descriptor" << message.eom;
+        message.warning() << "Method: " << class_name << "." << method_name
+                          << "\n signature: " << signature.value()
+                          << "\n descriptor: " << descriptor
+                          << "\n different number of parameters, reverting to "
+                             "descriptor"
+                          << message.eom;
       }
     }
-    catch(unsupported_java_class_signature_exceptiont &e)
+    catch(const unsupported_java_class_signature_exceptiont &e)
     {
-      message.warning() << "method: " << class_name << "." << method_name
-        << "\n could not parse signature: " << signature.value() << "\n "
-        << e.what() << "\n" << " reverting to descriptor: "
-        << descriptor << message.eom;
+      message.warning() << "Method: " << class_name << "." << method_name
+                        << "\n could not parse signature: " << signature.value()
+                        << "\n " << e.what() << "\n"
+                        << " reverting to descriptor: " << descriptor
+                        << message.eom;
     }
   }
   return to_code_type(member_type_from_descriptor);

src/java_bytecode/java_bytecode_language.h

@@ -172,6 +172,10 @@ class java_bytecode_languaget:public languaget
 
 private:
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
+
+  /// Maps synthetic method names on to the particular type of synthetic method
+  /// (static initializer, initializer wrapper, etc). For full documentation see
+  /// synthetic_method_map.h
   synthetic_methods_mapt synthetic_methods;
   stub_global_initializer_factoryt stub_global_initializer_factory;
   class_hierarchyt class_hierarchy;

src/java_bytecode/synthetic_methods_map.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Java Static Initializers
+Module: Synthetic methods map
 
 Author: Chris Smowton, [email protected]
 
@@ -9,12 +9,31 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H
 #define CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H
 
+/// \file
+///   Synthetic methods are particular methods internally generated by the
+///   Java frontend, including thunks to ensure static initializers are run once
+///   and initializers created for unknown / stub types. Compare normal methods,
+///   which are translated from Java bytecode. This file provides an
+///   enumeration specifying the kind of a particular synthetic method and a
+///   common type of a map giving a collection of synthetic methods.
+///   Functions stubs and array.clone() functions are also generated by the Java
+///   frontend but are not recorded using this framework, but may be in future.
+
+/// Synthetic method kinds.
 enum class synthetic_method_typet
 {
+  /// A static initializer wrapper
+  /// (code of the form `if(!already_run) clinit(); already_run = true;`)
+  /// These are generated for both user and stub types, to ensure the actual
+  /// static initializer is only run once on any given path.
   STATIC_INITIALIZER_WRAPPER,
+  /// A generated (synthetic) static initializer function for a stub type.
+  /// Because we don't have the bytecode for a stub type (by definition), we
+  /// generate a static initializer function to initialize its static fields.
   STUB_CLASS_STATIC_INITIALIZER
 };
 
+/// Maps method names on to a synthetic method kind.
 typedef std::unordered_map<irep_idt, synthetic_method_typet, irep_id_hash>
   synthetic_methods_mapt;
 

src/jbmc/jbmc_parse_options.cpp

@@ -385,7 +385,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     for(const char *opt :
       { "nondet-static",
         "full-slice",
-        "lazy-methods" })
+        "lazy-methods",
+        "reachability-slice",
+        "reachability-slice-fb" })
     {
       if(cmdline.isset(opt))
       {

unit/goto-programs/goto_program_generics/GenericBases.java

@@ -1,21 +1,3 @@
-// Helper classes
-class Wrapper<T> {
-  public T field;
-}
-
-class IntWrapper {
-  public int i;
-}
-
-class TwoWrapper<K, V> {
-  public K first;
-  public V second;
-}
-
-interface InterfaceWrapper<T> {
-  public T method(T t);
-}
-
 // A class extending a generic class instantiated with a standard library class
 class SuperclassInst extends Wrapper<Integer> {
   public void foo() {
@@ -24,14 +6,14 @@ public void foo() {
 }
 
 // A class extending a generic class instantiated with a user-defined class
-class SuperclassInst2 extends Wrapper<IntWrapper> {
+class SuperclassInst2 extends Wrapper<IWrapper> {
   public void foo() {
     this.field.i = 5;
   }
 }
 
 // A class extending an instantiated nested generic class
-class SuperclassInst3 extends Wrapper<Wrapper<IntWrapper>> {
+class SuperclassInst3 extends Wrapper<Wrapper<IWrapper>> {
   public void foo() {
     this.field.field.i = 5;
   }
@@ -54,7 +36,7 @@ public void foo() {
 
 // A generic class extending a generic class with both instantiated and
 // uninstantiated parameters
-class SuperclassMixed<U> extends TwoWrapper<U,IntWrapper> {
+class SuperclassMixed<U> extends PairWrapper<U,IWrapper> {
   public void foo(U value) {
     this.first = value;
     this.second.i = 5;
@@ -99,7 +81,7 @@ public void foo(U value) {
   }
   public Inner inner;
 
-  class InnerGen<T> extends TwoWrapper<U,T> {
+  class InnerGen<T> extends PairWrapper<U,T> {
     public void foo(U uvalue, T tvalue) {
       this.first = uvalue;
       this.second = tvalue;
@@ -113,11 +95,23 @@ class InnerThree extends Inner {
 }
 class SuperclassInnerUninstTest
 {
-  SuperclassInnerUninst<IntWrapper> f;
+  SuperclassInnerUninst<IWrapper> f;
   public void foo() {
-    IntWrapper x = new IntWrapper();
+    IWrapper x = new IWrapper(0);
     f.inner.foo(x);
     f.inner_gen.foo(x,true);
     f.inner_three.foo(x);
   }
 }
+
+class SuperclassUnsupported extends UnsupportedWrapper1<SuperclassUnsupported> {
+  public void foo() {
+    this.field = new SuperclassUnsupported();
+  }
+}
+
+class SuperclassOpaque extends OpaqueWrapper<IWrapper> {
+  public void foo() {
+      this.field.i = 5;
+    }
+}