Merge pull request #649 from cristina-david/remove-disable-runtime-checks

Remove the disable-runtime-checks flag for Java

Author: Daniel Kroening

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -27,14 +27,12 @@ class java_bytecode_convert_classt:public messaget
   java_bytecode_convert_classt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     lazy_methodst& _lazy_methods,
     lazy_methods_modet _lazy_methods_mode,
     bool _string_refinement_enabled):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     lazy_methods(_lazy_methods),
     lazy_methods_mode(_lazy_methods_mode),
@@ -60,7 +58,6 @@ class java_bytecode_convert_classt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   lazy_methodst &lazy_methods;
   lazy_methods_modet lazy_methods_mode;
@@ -169,7 +166,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
         method,
         symbol_table,
         get_message_handler(),
-        disable_runtime_checks,
         max_array_length);
     }
     else
@@ -364,7 +360,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &lazy_methods,
   lazy_methods_modet lazy_methods_mode,
@@ -373,7 +368,6 @@ bool java_bytecode_convert_class(
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     lazy_methods,
     lazy_methods_mode,

src/java_bytecode/java_bytecode_convert_class.h

@@ -19,7 +19,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &,
   lazy_methods_modet,

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1084,20 +1084,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(op.size()==1 && results.size()==1);
       code_blockt block;
-      if(!disable_runtime_checks)
-      {
-        // TODO throw NullPointerException instead
-        const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
-        const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-        const exprt not_equal_null(
-          binary_relation_exprt(lhs, ID_notequal, rhs));
-        code_assertt check(not_equal_null);
-        check.add_source_location()
-          .set_comment("Throw null");
-        check.add_source_location()
-          .set_property_class("null-pointer-exception");
-        block.move_to_operands(check);
-      }
+      // TODO throw NullPointerException instead
+      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
+      const exprt not_equal_null(
+        binary_relation_exprt(lhs, ID_notequal, rhs));
+      code_assertt check(not_equal_null);
+      check.add_source_location()
+        .set_comment("Throw null");
+      check.add_source_location()
+        .set_property_class("null-pointer-exception");
+      block.move_to_operands(check);
 
       side_effect_expr_throwt throw_expr;
       throw_expr.add_source_location()=i_it->source_location;
@@ -1110,20 +1107,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="checkcast")
     {
-      if(!disable_runtime_checks)
-      {
-        // checkcast throws an exception in case a cast of object
-        // on stack to given type fails.
-        // The stack isn't modified.
-        // TODO: convert assertions to exceptions.
-        assert(op.size()==1 && results.size()==1);
-        binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
-        c=code_assertt(check);
-        c.add_source_location().set_comment("Dynamic cast check");
-        c.add_source_location().set_property_class("bad-dynamic-cast");
-      }
-      else
-        c=code_skipt();
+      // checkcast throws an exception in case a cast of object
+      // on stack to given type fails.
+      // The stack isn't modified.
+      // TODO: convert assertions to exceptions.
+      assert(op.size()==1 && results.size()==1);
+      binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
+      c=code_assertt(check);
+      c.add_source_location().set_comment("Dynamic cast check");
+      c.add_source_location().set_property_class("bad-dynamic-cast");
 
       results[0]=op[0];
     }
@@ -1308,13 +1300,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const dereference_exprt element(data_plus_offset, element_type);
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        codet bounds_check=
-          get_array_bounds_check(deref, op[1], i_it->source_location);
-        bounds_check.add_source_location()=i_it->source_location;
-        c.move_to_operands(bounds_check);
-      }
+      codet bounds_check=
+        get_array_bounds_check(deref, op[1], i_it->source_location);
+      bounds_check.add_source_location()=i_it->source_location;
+      c.move_to_operands(bounds_check);
       code_assignt array_put(element, op[2]);
       array_put.add_source_location()=i_it->source_location;
       c.move_to_operands(array_put);
@@ -1354,11 +1343,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       dereference_exprt element(data_plus_offset, element_type);
 
-      if(!disable_runtime_checks)
-      {
-        c=get_array_bounds_check(deref, op[1], i_it->source_location);
-        c.add_source_location()=i_it->source_location;
-      }
+      c=get_array_bounds_check(deref, op[1], i_it->source_location);
+      c.add_source_location()=i_it->source_location;
       results[0]=java_bytecode_promotion(element);
     }
     else if(statement==patternt("?load"))
@@ -1899,17 +1885,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        c.move_to_operands(check);
-      }
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      c.move_to_operands(check);
+
       if(max_array_length!=0)
       {
         constant_exprt size_limit=
@@ -1941,26 +1925,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       code_blockt checkandcreate;
-      if(!disable_runtime_checks)
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      checkandcreate.move_to_operands(check);
+
+      if(max_array_length!=0)
       {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        checkandcreate.move_to_operands(check);
-
-        if(max_array_length!=0)
-        {
-          constant_exprt size_limit=
-            from_integer(max_array_length, java_int_type());
-          binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
-          code_assumet assume_le_max_size(le_max_size);
-          checkandcreate.move_to_operands(assume_le_max_size);
-        }
+        constant_exprt size_limit=
+          from_integer(max_array_length, java_int_type());
+        binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
+        code_assumet assume_le_max_size(le_max_size);
+        checkandcreate.move_to_operands(assume_le_max_size);
       }
+
       const exprt tmp=tmp_variable("newarray", ref_type);
       c=code_assignt(tmp, java_new_array);
       results[0]=tmp;
@@ -2430,15 +2412,13 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer<std::vector<irep_idt> > needed_methods,
   safe_pointer<std::set<irep_idt> > needed_classes)
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     needed_methods,
     needed_classes);

src/java_bytecode/java_bytecode_convert_method.h

@@ -22,7 +22,6 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer<std::vector<irep_idt> > needed_methods,
   safe_pointer<std::set<irep_idt> > needed_classes);
@@ -33,15 +32,13 @@ inline void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length)
 {
   java_bytecode_convert_method(
     class_symbol,
     method,
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     safe_pointer<std::vector<irep_idt> >::create_null(),
     safe_pointer<std::set<irep_idt> >::create_null());

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -30,13 +30,11 @@ class java_bytecode_convert_methodt:public messaget
   java_bytecode_convert_methodt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     safe_pointer<std::vector<irep_idt> > _needed_methods,
     safe_pointer<std::set<irep_idt> > _needed_classes):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     needed_methods(_needed_methods),
     needed_classes(_needed_classes)
@@ -56,7 +54,6 @@ class java_bytecode_convert_methodt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   safe_pointer<std::vector<irep_idt> > needed_methods;
   safe_pointer<std::set<irep_idt> > needed_classes;

src/java_bytecode/java_bytecode_language.cpp

@@ -42,7 +42,6 @@ Function: java_bytecode_languaget::get_language_options
 
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
-  disable_runtime_checks=cmd.isset("disable-runtime-check");
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   string_refinement_enabled=cmd.isset("string-refine");
   if(cmd.isset("java-max-input-array-length"))
@@ -525,7 +524,6 @@ bool java_bytecode_languaget::typecheck(
          c_it->second,
          symbol_table,
          get_message_handler(),
-         disable_runtime_checks,
          max_user_array_length,
          lazy_methods,
          lazy_methods_mode,
@@ -646,7 +644,6 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
           *parsed_method.second,
           symbol_table,
           get_message_handler(),
-          disable_runtime_checks,
           max_user_array_length,
           safe_pointer<std::vector<irep_idt> >::create_non_null(
             &method_worklist2),
@@ -761,7 +758,6 @@ void java_bytecode_languaget::convert_lazy_method(
     *lazy_method_entry.second,
     symtab,
     get_message_handler(),
-    disable_runtime_checks,
     max_user_array_length);
 }
 

src/java_bytecode/java_bytecode_language.h

@@ -94,12 +94,6 @@ class java_bytecode_languaget:public languaget
   std::vector<irep_idt> main_jar_classes;
   java_class_loadert java_class_loader;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-
-  bool disable_runtime_checks;      // disable run-time checks for java, i.e.,
-                                    // ASSERTS for
-                                    //  - checkcast / instanceof
-                                    //  - array bounds check
-                                    //  - array size for newarray
   size_t max_nondet_array_length;   // maximal length for non-det array creation
   size_t max_user_array_length;     // max size for user code created arrays
   lazy_methodst lazy_methods;