Merge pull request diffblue#487 from diffblue/CBMC_merge_2018-07-04

CBMC merge 2018-07-04

Author: NathanJPhillips

cbmc/COMPILING.md

@@ -32,11 +32,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    To compile JBMC, you additionally need the JDK and the java-models-library.
    For the JDK, on Debian-like distributions, do as root:
    ```
-   apt-get install openjdk-8-jdk
+   apt-get install unzip openjdk-8-jdk
    ```
    On Red Hat/Fedora or derivates, do as root:
    ```
-   dnf install java-1.8.0-openjdk-devel
+   dnf install unzip java-1.8.0-openjdk-devel
    ```
 
 2. As a user, get the CBMC source via
@@ -180,11 +180,16 @@ Follow these instructions:
       have to adjust the section in `src/common` that defines `CC` and `CXX`
       for BUILD_ENV = Cygwin.
       Then start the Cygwin shell.
-4. In the Cygwin shell, type
+4. To compile CMBC, open the Cygwin shell and type
    ```
    make -C src DOWNLOADER=wget minisat2-download
    make -C src
    ```
+5. To compile JMBC, open the Cygwin shell and type
+   ```
+   make -C jbmc/src java-models-library-download
+   make -C jbmc/src
+   ```
 
 (Optional) A Visual Studio project file can be generated with the script
 "generate_vcxproj" that is in the subdirectory "scripts".  The project file is

cbmc/jbmc/regression/jbmc-strings/Makefile

@@ -28,4 +28,4 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log

cbmc/jbmc/regression/jbmc/Makefile

@@ -20,7 +20,7 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log
 
 %.class: %.java ../../src/org.cprover.jar
 	javac -g -cp ../../src/org.cprover.jar:. $<

cbmc/jbmc/src/java_bytecode/expr2java.h

@@ -58,8 +58,8 @@ std::string type2java(const typet &type, const namespacet &ns);
 template <typename float_type>
 std::string floating_point_to_java_string(float_type value)
 {
-  static const bool is_float = std::is_same<float_type, float>::value;
-  static const std::string class_name = is_float ? "Float" : "Double";
+  const bool is_float = std::is_same<float_type, float>::value;
+  const std::string class_name = is_float ? "Float" : "Double";
   if(std::isnan(value))
     return class_name + ".NaN";
   if(std::isinf(value) && value >= 0.)

cbmc/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -118,7 +118,15 @@ class java_bytecode_convert_classt:public messaget
   // see definition below for more info
   static void add_array_types(symbol_tablet &symbol_table);
 
-  static bool is_overlay_method(const methodt &method);
+  static bool is_overlay_method(const methodt &method)
+  {
+    return method.has_annotation(ID_overlay_method);
+  }
+
+  static bool is_ignored_method(const methodt &method)
+  {
+    return method.has_annotation(ID_ignored_method);
+  }
 
   bool check_field_exists(
     const fieldt &field,
@@ -393,7 +401,7 @@ void java_bytecode_convert_classt::convert(
   new_symbol.base_name = base_name;
   new_symbol.pretty_name=c.name;
   new_symbol.name=qualified_classname;
-  class_type.set(ID_name, new_symbol.name);
+  class_type.set_name(new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;
@@ -455,6 +463,8 @@ void java_bytecode_convert_classt::convert(
   {
     for(const methodt &method : overlay_class.get().methods)
     {
+      if(is_ignored_method(method))
+        continue;
       const irep_idt method_identifier =
         qualified_classname + "." + id2string(method.name)
           + ":" + method.descriptor;
@@ -496,6 +506,8 @@ void java_bytecode_convert_classt::convert(
   }
   for(const methodt &method : c.methods)
   {
+    if(is_ignored_method(method))
+      continue;
     const irep_idt method_identifier=
       qualified_classname + "." + id2string(method.name)
         + ":" + method.descriptor;
@@ -716,15 +728,15 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     if(symbol_table.has_symbol(symbol_type_identifier))
       return;
 
-    class_typet class_type;
+    java_class_typet class_type;
     // we have the base class, java.lang.Object, length and data
     // of appropriate type
     class_type.set_tag(symbol_type_identifier);
     // Note that non-array types don't have "java::" at the beginning of their
     // tag, and their name is "java::" + their tag. Since arrays do have
     // "java::" at the beginning of their tag we set the name to be the same as
     // the tag.
-    class_type.set(ID_name, symbol_type_identifier);
+    class_type.set_name(symbol_type_identifier);
 
     class_type.components().reserve(3);
     class_typet::componentt base_class_component(
@@ -877,13 +889,6 @@ 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::find_annotation(
-           method.annotations, ID_overlay_method)
-    .has_value();
-}
-
 bool java_bytecode_convert_class(
   const java_class_loadert::parse_tree_with_overlayst &parse_trees,
   symbol_tablet &symbol_table,

cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -849,7 +849,7 @@ const select_pointer_typet &
 void java_bytecode_languaget::methods_provided(
   std::unordered_set<irep_idt> &methods) const
 {
-  static std::string cprover_class_prefix = "java::org.cprover.CProver.";
+  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
 
   // Add all string solver methods to map
   string_preprocess.get_all_function_names(methods);

cbmc/jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -84,6 +84,11 @@ class java_bytecode_parse_treet
       is_private(false), is_static(false), is_final(false)
     {
     }
+
+    bool has_annotation(const irep_idt &annotation_id) const
+    {
+      return find_annotation(annotations, annotation_id).has_value();
+    }
   };
 
   class methodt:public membert

cbmc/jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -301,9 +301,9 @@ class base_ref_infot : public structured_pool_entryt
 public:
   explicit base_ref_infot(pool_entryt entry) : structured_pool_entryt(entry)
   {
-    static std::set<u1> info_tags = {
-      CONSTANT_Fieldref, CONSTANT_Methodref, CONSTANT_InterfaceMethodref};
-    PRECONDITION(info_tags.find(entry.tag) != info_tags.end());
+    PRECONDITION(
+      entry.tag == CONSTANT_Fieldref || entry.tag == CONSTANT_Methodref ||
+      entry.tag == CONSTANT_InterfaceMethodref);
     class_index = entry.ref1;
     name_and_type_index = entry.ref2;
   }

cbmc/jbmc/src/java_bytecode/java_class_loader.cpp

@@ -168,50 +168,48 @@ java_class_loadert::get_parse_tree(
     }
   }
 
-  if(!parse_trees.empty())
+  auto parse_tree_it = parse_trees.begin();
+  // If the first class implementation is an overlay emit a warning and
+  // skip over it until we find a non-overlay class
+  while(parse_tree_it != parse_trees.end())
   {
-    auto parse_tree_it = parse_trees.begin();
-    // If the first class implementation is an overlay emit a warning and
-    // skip over it until we find a non-overlay class
-    while(parse_tree_it != parse_trees.end())
-    {
-      // Skip parse trees that failed to load - though these shouldn't exist yet
-      if(parse_tree_it->loading_successful)
-      {
-        if(!is_overlay_class(parse_tree_it->parsed_class))
-        {
-          // Keep the non-overlay class
-          ++parse_tree_it;
-          break;
-        }
-        warning()
-          << "Skipping class " << class_name
-          << " marked with OverlayClassImplementation but found before"
-            " original definition"
-          << eom;
-      }
-      auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
-      ++parse_tree_it;
-      parse_trees.erase(unloaded_or_overlay_out_of_order_it);
-    }
-    // Collect overlay classes
-    while(parse_tree_it != parse_trees.end())
+    // Skip parse trees that failed to load - though these shouldn't exist yet
+    if(parse_tree_it->loading_successful)
     {
-      // Remove non-initial classes that aren't overlays
       if(!is_overlay_class(parse_tree_it->parsed_class))
       {
-        warning()
-          << "Skipping duplicate definition of class " << class_name
-          << " not marked with OverlayClassImplementation" << eom;
-        auto duplicate_non_overlay_it = parse_tree_it;
+        // Keep the non-overlay class
         ++parse_tree_it;
-        parse_trees.erase(duplicate_non_overlay_it);
+        break;
       }
-      else
-        ++parse_tree_it;
+      warning()
+        << "Skipping class " << class_name
+        << " marked with OverlayClassImplementation but found before"
+          " original definition"
+        << eom;
     }
-    return parse_trees;
+    auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
+    ++parse_tree_it;
+    parse_trees.erase(unloaded_or_overlay_out_of_order_it);
   }
+  // Collect overlay classes
+  while(parse_tree_it != parse_trees.end())
+  {
+    // Remove non-initial classes that aren't overlays
+    if(!is_overlay_class(parse_tree_it->parsed_class))
+    {
+      warning()
+        << "Skipping duplicate definition of class " << class_name
+        << " not marked with OverlayClassImplementation" << eom;
+      auto duplicate_non_overlay_it = parse_tree_it;
+      ++parse_tree_it;
+      parse_trees.erase(duplicate_non_overlay_it);
+    }
+    else
+      ++parse_tree_it;
+  }
+  if(!parse_trees.empty())
+    return parse_trees;
 
   // Not found or failed to load
   warning() << "failed to load class `" << class_name << '\'' << eom;

cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -210,6 +210,7 @@ void java_string_library_preprocesst::add_string_type(
 {
   java_class_typet string_type;
   string_type.set_tag(class_name);
+  string_type.set_name("java::" + id2string(class_name));
   string_type.components().resize(3);
   string_type.components()[0].set_name("@java.lang.Object");
   string_type.components()[0].set_pretty_name("@java.lang.Object");

cbmc/jbmc/src/java_bytecode/java_types.h

@@ -158,6 +158,20 @@ class java_class_typet:public class_typet
     return type_checked_cast<annotated_typet>(
       static_cast<typet &>(*this)).get_annotations();
   }
+
+  /// Get the name of the struct, which can be used to look up its symbol
+  /// in the symbol table.
+  const irep_idt &get_name() const
+  {
+    return get(ID_name);
+  }
+
+  /// Set the name of the struct, which can be used to look up its symbol
+  /// in the symbol table.
+  void set_name(const irep_idt &name)
+  {
+    set(ID_name, name);
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)

cbmc/jbmc/src/java_bytecode/java_utils.cpp

@@ -67,7 +67,7 @@ void generate_class_stub(
   message_handlert &message_handler,
   const struct_union_typet::componentst &componentst)
 {
-  class_typet class_type;
+  java_class_typet class_type;
 
   class_type.set_tag(class_name);
   class_type.set(ID_base_name, class_name);
@@ -79,7 +79,7 @@ void generate_class_stub(
   new_symbol.base_name=class_name;
   new_symbol.pretty_name=class_name;
   new_symbol.name="java::"+id2string(class_name);
-  class_type.set(ID_name, new_symbol.name);
+  class_type.set_name(new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;

cbmc/jbmc/src/java_bytecode/load_method_by_regex.cpp

@@ -41,7 +41,7 @@ bool does_pattern_miss_descriptor(const std::string &pattern)
   if(descriptor_index == std::string::npos)
     return true;
 
-  static const std::string java_prefix = "java::";
+  const std::string java_prefix = "java::";
   return descriptor_index == java_prefix.length() - 1 &&
          has_prefix(pattern, java_prefix);
 }

cbmc/regression/cbmc/Makefile

@@ -15,5 +15,5 @@ show:
 
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
-	find -name '*.gb' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
 	$(RM) tests.log

cbmc/regression/cbmc/gcc_switch_case_range2/main.c

@@ -0,0 +1,32 @@
+typedef enum
+{
+  VALUE_1,
+  VALUE_2,
+  VALUE_3,
+  VALUE_4
+} values;
+
+int main()
+{
+  unsigned x;
+  switch(x)
+  {
+  case VALUE_1:
+    __CPROVER_assert(0, "0 works");
+    break;
+#ifdef __GNUC__
+  case VALUE_2 ... 3:
+#else
+  case VALUE_2:
+  case VALUE_3:
+  case VALUE_4:
+#endif
+    __CPROVER_assert(0, "... works");
+    break;
+  default:
+    __CPROVER_assert(0, "default works");
+    break;
+  }
+
+  return 0;
+}

cbmc/regression/cbmc/gcc_switch_case_range2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 3 of 3 failed
+--
+^warning: ignoring

cbmc/regression/goto-gcc/Makefile

@@ -18,4 +18,5 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
+	find -name '*.goto-cc-saved' -execdir $(RM) '{}' \;
 	$(RM) tests.log

cbmc/regression/invariants/Makefile

@@ -25,3 +25,8 @@ show:
 
 driver$(EXEEXT): $(OBJ)
 	$(LINKBIN)
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) driver$(EXEEXT) driver$(DEPEXT) driver$(OBJEXT)
+	$(RM) tests.log

cbmc/regression/test.pl

@@ -421,7 +421,7 @@ ($)
 close LOG;
 
 if($opt_p && $failures != 0) {
-  open LOG,"<tests.log" or die "Failed to open tests.log\n";
+  open LOG,"<$logfile_name" or die "Failed to open $logfile_name\n";
 
   my $printed_this_test = 1;
   my $current_test = "";

cbmc/src/ansi-c/c_typecheck_code.cpp

@@ -535,6 +535,7 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
     exprt &case_expr=code.case_op();
     typecheck_expr(case_expr);
     implicit_typecast(case_expr, switch_op_type);
+    make_constant(case_expr);
   }
 }
 
@@ -561,6 +562,8 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
   typecheck_expr(code.op1());
   implicit_typecast(code.op0(), switch_op_type);
   implicit_typecast(code.op1(), switch_op_type);
+  make_constant(code.op0());
+  make_constant(code.op1());
 }
 
 void c_typecheck_baset::typecheck_gcc_local_label(codet &code)