Merge pull request #1229 from smowton/smowton/feature/use_null_check_annotation_everywhere

smowton · web-flow · commit 1f2bb67b86ae · 2017-08-11T14:51:18.000+01:00
Use null check annotation everywhere
diff --git a/regression/cbmc-java/stack_var4/test.desc b/regression/cbmc-java/stack_var4/test.desc
@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/stack_var5/test.desc b/regression/cbmc-java/stack_var5/test.desc
@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/stack_var6/test.desc b/regression/cbmc-java/stack_var6/test.desc
@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/stack_var7/test.desc b/regression/cbmc-java/stack_var7/test.desc
@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/strings/StaticCharMethods05/test.desc
@@ -3,7 +3,7 @@ StaticCharMethods05.class
 --refine-strings
 ^EXIT=10$
 ^SIGNAL=0$
-^\[pointer_dereference\.2\] reference is null in \*this->data: FAILURE$
+null-pointer-exception\.14\] Throw null: FAILURE
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
 ^\[.*assertion\.2\] .* line 22 .* FAILURE$
 ^VERIFICATION FAILED$
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -909,7 +909,7 @@ void goto_checkt::pointer_validity_check(
   const exprt &access_ub,
   const irep_idt &mode)
 {
-  if(mode!=ID_java && !enable_pointer_check)
+  if(!enable_pointer_check)
     return;
 
   const exprt &pointer=expr.op0();
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -524,9 +524,7 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
   exprt pointer2=
     typecast_exprt(pointer, java_reference_type(class_type));
 
-  dereference_exprt obj_deref(pointer2, class_type);
-  // tag it so it's easy to identify during instrumentation
-  obj_deref.set(ID_java_member_access, true);
+  dereference_exprt obj_deref=checked_dereference(pointer2, class_type);
 
   const member_exprt member_expr(
     obj_deref,
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -29,15 +29,11 @@ class java_bytecode_instrumentt:public messaget
   java_bytecode_instrumentt(
     symbol_tablet &_symbol_table,
     const bool _throw_runtime_exceptions,
-    message_handlert &_message_handler,
-    const size_t _max_array_length,
-    const size_t _max_tree_depth):
+    message_handlert &_message_handler):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     throw_runtime_exceptions(_throw_runtime_exceptions),
-    message_handler(_message_handler),
-    max_array_length(_max_array_length),
-    max_tree_depth(_max_tree_depth)
+    message_handler(_message_handler)
     {
     }
 
@@ -47,8 +43,6 @@ class java_bytecode_instrumentt:public messaget
   symbol_tablet &symbol_table;
   const bool throw_runtime_exceptions;
   message_handlert &message_handler;
-  const size_t max_array_length;
-  const size_t max_tree_depth;
 
   codet throw_exception(
     const exprt &cond,
@@ -566,29 +560,52 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
   instrument_code(expr);
 }
 
+/// Instruments the code attached to `symbol` with
+/// runtime exceptions or corresponding assertions.
+/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
+/// Otherwise, assertions are emitted.
+/// \param symbol_table: global symbol table (may gain exception type stubs and
+///   similar)
+/// \param symbol: the symbol to instrument
+/// \param throw_runtime_exceptions: flag determining whether we instrument the
+///   code with runtime exceptions or with assertions. The former applies if
+///   this flag is set to true.
+/// \param message_handler: stream to report status and warnings
+void java_bytecode_instrument_symbol(
+  symbol_tablet &symbol_table,
+  symbolt &symbol,
+  const bool throw_runtime_exceptions,
+  message_handlert &message_handler)
+{
+  java_bytecode_instrumentt instrument(
+    symbol_table,
+    throw_runtime_exceptions,
+    message_handler);
+  INVARIANT(
+    symbol.value.id()==ID_code,
+    "java_bytecode_instrument expects a code-typed symbol");
+  instrument(symbol.value);
+}
+
 /// Instruments all the code in the symbol_table with
 /// runtime exceptions or corresponding assertions.
 /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
 /// Otherwise, assertions are emitted.
-/// \par parameters: `symbol_table`: the symbol table to instrument
-/// `throw_runtime_exceptions`: flag determining whether we instrument the code
-/// with runtime exceptions or with assertions. The former applies if this flag
-/// is set to true.
-/// `max_array_length`: maximum array length; the only reason we need this is
-/// in order to be able to call the object factory to create exceptions.
+/// \param symbol_table: global symbol table, all of whose code members
+///   will be annotated (may gain exception type stubs and similar)
+/// \param throw_runtime_exceptions: flag determining whether we instrument the
+///   code with runtime exceptions or with assertions. The former applies if
+///   this flag is set to true.
+/// \param message_handler: stream to report status and warnings
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
   const bool throw_runtime_exceptions,
-  message_handlert &message_handler,
-  const size_t max_array_length,
-  const size_t max_tree_depth)
+  message_handlert &message_handler)
 {
   java_bytecode_instrumentt instrument(
     symbol_table,
     throw_runtime_exceptions,
-    message_handler,
-    max_array_length,
-    max_tree_depth);
+    message_handler);
 
   std::vector<irep_idt> symbols_to_instrument;
   forall_symbols(s_it, symbol_table.symbols)
@@ -600,9 +617,5 @@ void java_bytecode_instrument(
   // instrument(...) can add symbols to the table, so it's
   // not safe to hold a reference to a symbol across a call.
   for(const auto &symbol : symbols_to_instrument)
-  {
-    exprt value=symbol_table.lookup(symbol).value;
-    instrument(value);
-    symbol_table.lookup(symbol).value=value;
-  }
+    instrument(symbol_table.lookup(symbol).value);
 }
diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h
@@ -11,10 +11,15 @@ Date:   June 2017
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 
+void java_bytecode_instrument_symbol(
+  symbol_tablet &symbol_table,
+  symbolt &symbol,
+  const bool throw_runtime_exceptions,
+  message_handlert &_message_handler);
+
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
   const bool throw_runtime_exceptions,
-  message_handlert &_message_handler,
-  const size_t max_array_length,
-  const size_t max_depth);
+  message_handlert &_message_handler);
+
 #endif
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
@@ -459,9 +459,7 @@ bool java_bytecode_languaget::typecheck(
   java_bytecode_instrument(
     symbol_table,
     throw_runtime_exceptions,
-    get_message_handler(),
-    max_nondet_array_length,
-    max_nondet_tree_depth);
+    get_message_handler());
 
   // now typecheck all
   if(java_bytecode_typecheck(
@@ -746,6 +744,13 @@ void java_bytecode_languaget::replace_string_methods(
       // Replace body of the function by code generated by string preprocess
       symbolt &symbol=context.lookup(id);
       symbol.value=generated_code;
+      // Specifically instrument the new code, since this comes after the
+      // blanket instrumentation pass called before typechecking.
+      java_bytecode_instrument_symbol(
+        context,
+        symbol,
+        throw_runtime_exceptions,
+        get_message_handler());
     }
   }
 }
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -24,6 +24,7 @@ Date:   April 2017
 #include <util/string_expr.h>
 #include "java_types.h"
 #include "java_object_factory.h"
+#include "java_utils.h"
 
 #include "java_string_library_preprocess.h"
 
@@ -334,7 +335,8 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   {
     if(implements_java_char_sequence(p.type()))
     {
-      dereference_exprt deref(p, to_pointer_type(p.type()).subtype());
+      dereference_exprt deref=
+        checked_dereference(p, to_pointer_type(p.type()).subtype());
       process_single_operand(ops, deref, loc, symbol_table, init_code);
     }
     else if(is_java_char_array_pointer_type(p.type()))
@@ -371,14 +373,16 @@ exprt::operandst
   exprt op1=operands[1];
 
   assert(implements_java_char_sequence(op0.type()));
-  dereference_exprt deref0(op0, to_pointer_type(op0.type()).subtype());
+  dereference_exprt deref0=
+    checked_dereference(op0, to_pointer_type(op0.type()).subtype());
   process_single_operand(ops, deref0, loc, symbol_table, init_code);
 
   // TODO: Manage the case where we have a non-String Object (this should
   // probably be handled upstream. At any rate, the following code should be
   // protected with assertions on the type of op1.
   typecast_exprt tcast(op1, to_pointer_type(op0.type()));
-  dereference_exprt deref1(tcast, to_pointer_type(op0.type()).subtype());
+  dereference_exprt deref1=
+    checked_dereference(tcast, to_pointer_type(op0.type()).subtype());
   process_single_operand(ops, deref1, loc, symbol_table, init_code);
   return ops;
 }
@@ -466,9 +470,12 @@ string_exprt java_string_library_preprocesst::replace_char_array(
   code_blockt &code)
 {
   refined_string_typet ref_type=refined_string_type;
-  dereference_exprt array(array_pointer, array_pointer.type().subtype());
+  dereference_exprt array=
+    checked_dereference(array_pointer, array_pointer.type().subtype());
   exprt array_data=get_data(array, symbol_table);
   // `deref_array` is *(array_pointer->data)`
+  // No null-pointer-exception check here since all array structures
+  // have non-null data
   const typet &content_type=ref_type.get_content_type();
   dereference_exprt deref_array(array_data, array_data.type().subtype());
 
@@ -724,7 +731,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
   symbol_tablet &symbol_table)
 {
   assert(implements_java_char_sequence(lhs.type()));
-  dereference_exprt deref(lhs, lhs.type().subtype());
+  dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype());
 
   code_blockt code;
 
@@ -741,7 +748,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
   struct_rhs.copy_to_operands(rhs_length);
   struct_rhs.copy_to_operands(rhs_array);
   code.add(code_assignt(
-    dereference_exprt(lhs, lhs.type().subtype()), struct_rhs));
+    checked_dereference(lhs, lhs.type().subtype()), struct_rhs));
 
   return code;
 }
@@ -782,7 +789,7 @@ codet java_string_library_preprocesst::
     symbol_tablet &symbol_table)
 {
   assert(implements_java_char_sequence(lhs.type()));
-  dereference_exprt deref(lhs, lhs.type().subtype());
+  dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype());
 
   code_blockt code;
   exprt new_array=allocate_fresh_array(
@@ -816,7 +823,7 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   else
     deref_type=rhs.type().subtype();
 
-  dereference_exprt deref(rhs, deref_type);
+  dereference_exprt deref=checked_dereference(rhs, deref_type);
 
   // Fields of the string object
   exprt rhs_length=get_length(deref, symbol_table);
@@ -1170,7 +1177,7 @@ codet java_string_library_preprocesst::make_string_to_char_array_code(
   code.add(code_assignt(deref_data, string_expr.content()));
 
   // lhs->data = &data[0]
-  dereference_exprt deref_lhs(lhs, lhs.type().subtype());
+  dereference_exprt deref_lhs=checked_dereference(lhs, lhs.type().subtype());
   exprt lhs_data=get_data(deref_lhs, symbol_table);
   index_exprt first_elt(
     deref_data, from_integer(0, java_int_type()), java_char_type());
@@ -1519,7 +1526,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
 
   // class_identifier is this->@class_identifier
   member_exprt class_identifier(
-    dereference_exprt(this_obj, this_obj.type().subtype()),
+    checked_dereference(this_obj, this_obj.type().subtype()),
     "@class_identifier",
     string_typet());
 
@@ -1743,7 +1750,8 @@ codet java_string_library_preprocesst::make_string_length_code(
 
   code_typet::parameterst params=type.parameters();
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
-  dereference_exprt deref(arg_this, arg_this.type().subtype());
+  dereference_exprt deref=
+    checked_dereference(arg_this, arg_this.type().subtype());
 
   // Create a new string_exprt to be picked up by the solver
   string_exprt str_expr=fresh_string_expr(loc, symbol_table, code);
diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp
@@ -171,3 +171,11 @@ irep_idt resolve_friendly_method_name(
     }
   }
 }
+
+dereference_exprt checked_dereference(const exprt &expr, const typet &type)
+{
+  dereference_exprt result(expr, type);
+  // tag it so it's easy to identify during instrumentation
+  result.set(ID_java_member_access, true);
+  return result;
+}
diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/type.h>
 #include <util/symbol_table.h>
 #include <util/message.h>
+#include <util/std_expr.h>
 
 #include "java_bytecode_parse_tree.h"
 
@@ -64,4 +65,9 @@ irep_idt resolve_friendly_method_name(
   const symbol_tablet &symbol_table,
   std::string &error);
 
+/// Dereference an expression and flag it for a null-pointer check
+/// \param expr: expression to dereference and check
+/// \param type: expected result type (typically expr.type().subtype())
+dereference_exprt checked_dereference(const exprt &expr, const typet &type);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

Original file line number	Diff line number	Diff line change
`@@ -909,7 +909,7 @@ void goto_checkt::pointer_validity_check(`
`909`	`909`	`const exprt &access_ub,`
`910`	`910`	`const irep_idt &mode)`
`911`	`911`	`{`
`912`		`- if(mode!=ID_java && !enable_pointer_check)`
	`912`	`+ if(!enable_pointer_check)`
`913`	`913`	`return;`
`914`	`914`
`915`	`915`	`const exprt &pointer=expr.op0();`