Check for null-pointer deref on array access

Author: smowton

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -524,15 +524,15 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
   exprt pointer2=
     typecast_exprt(pointer, java_reference_type(class_type));
 
-  const dereference_exprt obj_deref(pointer2, 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);
 
-  member_exprt member_expr(
+  const member_exprt member_expr(
     obj_deref,
     fieldref.get(ID_component_name),
     fieldref.type());
 
-  // tag it so it's easy to identify during instrumentation
-  member_expr.set(ID_java_member_access, true);
   return member_expr;
 }
 
@@ -1496,7 +1496,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       exprt pointer=
         typecast_exprt(op[0], java_array_type(type_char));
 
-      const dereference_exprt deref(pointer, pointer.type().subtype());
+      dereference_exprt deref(pointer, pointer.type().subtype());
+      deref.set(ID_java_member_access, true);
 
       const member_exprt data_ptr(
         deref,
@@ -1559,7 +1560,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       exprt pointer=
         typecast_exprt(op[0], java_array_type(type_char));
 
-      const dereference_exprt deref(pointer, pointer.type().subtype());
+      dereference_exprt deref(pointer, pointer.type().subtype());
+      deref.set(ID_java_member_access, true);
 
       const member_exprt data_ptr(
         deref,
@@ -2237,8 +2239,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       exprt pointer=
         typecast_exprt(op[0], java_array_type(statement[0]));
 
-      const dereference_exprt array(pointer, pointer.type().subtype());
+      dereference_exprt array(pointer, pointer.type().subtype());
       assert(pointer.type().subtype().id()==ID_symbol);
+      array.set(ID_java_member_access, true);
 
       const member_exprt length(array, "length", java_int_type());
 

src/java_bytecode/java_bytecode_instrument.cpp

@@ -550,23 +550,17 @@ codet java_bytecode_instrumentt::instrument_expr(
         expr.op1(),
         expr.source_location()));
   }
-  else if(expr.id()==ID_member &&
+  else if(expr.id()==ID_dereference &&
           expr.get_bool(ID_java_member_access))
   {
-    // this corresponds to either getfield or putfield
-    // so we must check null pointer dereference
-    const member_exprt &member_expr=to_member_expr(expr);
-    if(member_expr.op0().id()==ID_dereference)
-    {
-      const dereference_exprt dereference_expr=
-        to_dereference_expr(member_expr.op0());
-      codet null_dereference_check=
-        check_null_dereference(
-          dereference_expr.op0(),
-          dereference_expr.source_location(),
-          false);
-      result.move_to_operands(null_dereference_check);
-    }
+    // Check pointer non-null before access:
+    const dereference_exprt dereference_expr=to_dereference_expr(expr);
+    codet null_dereference_check=
+      check_null_dereference(
+        dereference_expr.op0(),
+        dereference_expr.source_location(),
+        false);
+    result.move_to_operands(null_dereference_check);
   }
 
   if(result==code_blockt())