Merge pull request diffblue#437 from diffblue/CBMC_merge_2018-06-04

SEC-440: Cbmc merge 2018-06-04

Author: owen-jones-diffblue

.travis.yml

@@ -70,6 +70,7 @@ jobs:
             - g++-5
             - libubsan0
             - python3-pip
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
           # Install pytest locally and adjust PATH so pip3 can find it
@@ -137,6 +138,7 @@ jobs:
             - libubsan0
             - parallel
             - python3-pip
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
           # Install pytest locally and adjust PATH so pip3 can find it
@@ -171,6 +173,7 @@ jobs:
             - libubsan0
             - parallel
             - python3-pip
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
         - export CCACHE_CPP2=yes
@@ -203,6 +206,7 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - python3-pip
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
         - export CCACHE_CPP2=yes

cbmc/.travis.yml

@@ -83,6 +83,7 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
@@ -115,6 +116,7 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
@@ -140,8 +142,9 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
+            - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
@@ -165,8 +168,9 @@ jobs:
             - clang-3.7
             - libstdc++-5-dev
             - libubsan0
+            - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
@@ -188,6 +192,7 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
+            - libc6-dev-i386
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       install:

cbmc/buildspec.yml

@@ -6,7 +6,7 @@ phases:
       - echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
       - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
       - apt-get update -y
-      - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache
+      - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386
       - apt-get install -y openjdk-7-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

cbmc/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class

@@ -0,0 +1,4 @@
+
+public @interface ExampleAnnotation {
+
+}

cbmc/jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,5 @@
+
+public enum ExampleEnum {
+
+}
+

cbmc/jbmc/regression/jbmc/class-literals/ExampleEnum.class

@@ -0,0 +1,4 @@
+
+interface ExampleInterface {
+
+}

cbmc/jbmc/regression/jbmc/class-literals/ExampleEnum.java

@@ -0,0 +1,4 @@
+; Compile me with Jasmin 2.1+ (https://sourceforge.net/projects/jasmin/)
+
+.class public synthetic ExampleSynthetic
+.super java/lang/Object

cbmc/jbmc/regression/jbmc/class-literals/ExampleInterface.class

@@ -0,0 +1,35 @@
+
+public class Test {
+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();
+    assert ExampleSynthetic.class.isSynthetic();
+
+    assert char[].class.isArray();
+    assert short[].class.isArray();
+    assert int[].class.isArray();
+    assert long[].class.isArray();
+    assert float[].class.isArray();
+    assert double[].class.isArray();
+    assert boolean[].class.isArray();
+    assert Object[].class.isArray();
+    assert Object[][].class.isArray();
+
+    // Note use of '==' not '.equals', as we expect the same exact literal,
+    // which in jbmc always have the same address.
+    // Note names of array classes are not tested yet, as arrays' types are
+    // printed as their raw signature, to be addressed separately.
+    // Note also primitive types (e.g. int.class) are not addresses here, as
+    // they are created through box types' static initializers (e.g. Integer
+    // has a static member TYPE that holds the Class for `int.class`)
+
+    assert ExampleAnnotation.class.getName() == "ExampleAnnotation";
+    assert ExampleInterface.class.getName() == "ExampleInterface";
+    assert ExampleEnum.class.getName() == "ExampleEnum";
+
+  }
+
+}

cbmc/jbmc/regression/jbmc/class-literals/ExampleInterface.java

@@ -0,0 +1,45 @@
+package java.lang;
+
+public class Class {
+
+  private String name;
+
+  private boolean isAnnotation;
+  private boolean isArray;
+  private boolean isInterface;
+  private boolean isSynthetic;
+  private boolean isLocalClass;
+  private boolean isMemberClass;
+  private boolean isEnum;
+
+  public void cproverInitializeClassLiteral(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+
+    this.name = name;
+    this.isAnnotation = isAnnotation;
+    this.isArray = isArray;
+    this.isInterface = isInterface;
+    this.isSynthetic = isSynthetic;
+    this.isLocalClass = isLocalClass;
+    this.isMemberClass = isMemberClass;
+    this.isEnum = isEnum;
+
+  }
+
+  public String getName() { return name; }
+
+  public boolean isAnnotation() { return isAnnotation; }
+  public boolean isArray() { return isArray; }
+  public boolean isInterface() { return isInterface; }
+  public boolean isSynthetic() { return isSynthetic; }
+  public boolean isLocalClass() { return isLocalClass; }
+  public boolean isMemberClass() { return isMemberClass; }
+  public boolean isEnum() { return isEnum; }
+}

cbmc/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

cbmc/jbmc/regression/jbmc/class-literals/ExampleSynthetic.j

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+lazy-methods is incompatible with symex-driven lazy loading

cbmc/jbmc/regression/jbmc/class-literals/Test.class

@@ -13,6 +13,7 @@
 #include "java_string_library_preprocess.h"
 #include "remove_exceptions.h"
 
+#include <util/expr_iterator.h>
 #include <util/suffix.h>
 
 #include <goto-programs/resolve_inherited_component.h>
@@ -52,6 +53,31 @@ ci_lazy_methodst::ci_lazy_methodst(
   class_hierarchy(symbol_table);
 }
 
+/// Checks if an expression refers to any class literals (e.g. MyType.class)
+/// These are expressed as ldc instructions in Java bytecode, and as symbols
+/// of the form `MyType@class_model` in GOTO programs.
+/// \param expr: expression to check
+/// \return true if the expression or any of its subexpressions refer to a
+///   class
+static bool references_class_model(const exprt &expr)
+{
+  static const symbol_typet class_type("java::java.lang.Class");
+
+  for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
+  {
+    if(can_cast_expr<symbol_exprt>(*it) &&
+       it->type() == class_type &&
+       has_suffix(
+         id2string(to_symbol_expr(*it).get_identifier()),
+         JAVA_CLASS_MODEL_SUFFIX))
+    {
+      return true;
+    }
+  }
+
+  return false;
+}
+
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods
 /// may be reachable from the main entry point. In brief, static methods are
 /// reachable if we find a callsite in another reachable site, while virtual
@@ -122,6 +148,7 @@ bool ci_lazy_methodst::operator()(
 
   std::unordered_set<irep_idt> methods_already_populated;
   std::unordered_set<exprt, irep_hash> virtual_function_calls;
+  bool class_initializer_seen = false;
 
   bool any_new_classes = true;
   while(any_new_classes)
@@ -149,8 +176,19 @@ bool ci_lazy_methodst::operator()(
           // Couldn't convert this function
           continue;
         }
-        gather_virtual_callsites(
-          symbol_table.lookup_ref(mname).value, virtual_function_calls);
+        const exprt &method_body = symbol_table.lookup_ref(mname).value;
+
+        gather_virtual_callsites(method_body, virtual_function_calls);
+
+        if(!class_initializer_seen && references_class_model(method_body))
+        {
+          class_initializer_seen = true;
+          irep_idt initializer_signature =
+            get_java_class_literal_initializer_signature();
+          if(symbol_table.has_symbol(initializer_signature))
+            methods_to_convert_later.insert(initializer_signature);
+        }
+
         any_new_methods=true;
       }
     }

cbmc/jbmc/regression/jbmc/class-literals/Test.java

@@ -265,6 +265,9 @@ void java_bytecode_convert_classt::convert(
   class_type.set_tag(c.name);
   class_type.set(ID_base_name, c.name);
   class_type.set(ID_abstract, c.is_abstract);
+  class_type.set(ID_is_annotation, c.is_annotation);
+  class_type.set(ID_interface, c.is_interface);
+  class_type.set(ID_synthetic, c.is_synthetic);
   class_type.set_final(c.is_final);
   if(c.is_enum)
   {
@@ -875,8 +878,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
 bool java_bytecode_convert_classt::is_overlay_method(const methodt &method)
 {
-  return java_bytecode_parse_treet::does_annotation_exist(
-    method.annotations, ID_overlay_method);
+  return java_bytecode_parse_treet::find_annotation(
+           method.annotations, ID_overlay_method)
+    .has_value();
 }
 
 bool java_bytecode_convert_class(
@@ -1015,24 +1019,48 @@ static void find_and_replace_parameters(
 /// \param annotations: The java_annotationt collection to populate
 void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
-  std::vector<java_annotationt> &annotations)
+  std::vector<java_annotationt> &java_annotations)
 {
   for(const auto &annotation : parsed_annotations)
   {
-    annotations.emplace_back(annotation.type);
+    java_annotations.emplace_back(annotation.type);
     std::vector<java_annotationt::valuet> &values =
-      annotations.back().get_values();
+      java_annotations.back().get_values();
     std::transform(
       annotation.element_value_pairs.begin(),
       annotation.element_value_pairs.end(),
       std::back_inserter(values),
-      [](const decltype(annotation.element_value_pairs)::value_type &value)
-      {
+      [](const decltype(annotation.element_value_pairs)::value_type &value) {
         return java_annotationt::valuet(value.element_name, value.value);
       });
   }
 }
 
+/// Convert java annotations, e.g. as retrieved from the symbol table, back
+/// to type annotationt (inverse of convert_annotations())
+/// \param java_annotations: The java_annotationt collection to convert
+/// \param annotations: The annotationt collection to populate
+void convert_java_annotations(
+  const std::vector<java_annotationt> &java_annotations,
+  java_bytecode_parse_treet::annotationst &annotations)
+{
+  for(const auto &java_annotation : java_annotations)
+  {
+    annotations.emplace_back(java_bytecode_parse_treet::annotationt());
+    auto &annotation = annotations.back();
+    annotation.type = java_annotation.get_type();
+
+    std::transform(
+      java_annotation.get_values().begin(),
+      java_annotation.get_values().end(),
+      std::back_inserter(annotation.element_value_pairs),
+      [](const java_annotationt::valuet &value)
+        -> java_bytecode_parse_treet::annotationt::element_value_pairt {
+          return {value.get_name(), value.get_value()};
+        });
+  }
+}
+
 /// Checks if the class is implicitly generic, i.e., it is an inner class of
 /// any generic class. All uses of the implicit generic type parameters within
 /// the inner class are updated to point to the type parameters of the

cbmc/jbmc/regression/jbmc/class-literals/java/lang/Class.class

@@ -33,6 +33,10 @@ void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
   std::vector<java_annotationt> &annotations);
 
+void convert_java_annotations(
+  const std::vector<java_annotationt> &java_annotations,
+  java_bytecode_parse_treet::annotationst &annotations);
+
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);

cbmc/jbmc/regression/jbmc/class-literals/java/lang/Class.java

@@ -404,6 +404,9 @@ void java_bytecode_convert_method_lazy(
   }
 
   method_symbol.type=member_type;
+  // Not used in jbmc at present, but other codebases that use jbmc as a library
+  // use this information.
+  method_symbol.type.set(ID_C_abstract, m.is_abstract);
   symbol_table.add(method_symbol);
 }
 
@@ -1185,7 +1188,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       if(cur_pc==it->handler_pc)
       {
-        if(catch_type!=typet() || it->catch_type==symbol_typet())
+        if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
         {
           catch_type=symbol_typet("java::java.lang.Throwable");
           break;