Use safe pointers for optional arguments

This basic safe-pointer class doesn't do any lifetime management;
rather it just enforces explicit null-checks and throws if they
don't go as expected.

Author: smowton

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1720,7 +1720,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
       if(needed_classes && arg0.type().id()==ID_symbol)
-        needed_classes->insert(to_symbol_type(arg0.type()).get_identifier());
+      {
+        needed_classes->insert(
+          to_symbol_type(arg0.type()).get_identifier());
+      }
       results[0]=java_bytecode_promotion(symbol_expr);
 
       // set $assertionDisabled to false
@@ -1739,7 +1742,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
       if(needed_classes && arg0.type().id()==ID_symbol)
-        needed_classes->insert(to_symbol_type(arg0.type()).get_identifier());
+        needed_classes->insert(
+          to_symbol_type(arg0.type()).get_identifier());
       c=code_assignt(symbol_expr, op[0]);
     }
     else if(statement==patternt("?2?")) // i2c etc.
@@ -2203,8 +2207,8 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   bool disable_runtime_checks,
   size_t max_array_length,
-  std::vector<irep_idt> *needed_methods,
-  std::set<irep_idt> *needed_classes)
+  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,

src/java_bytecode/java_bytecode_convert_method.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/message.h>
+#include <util/safe_pointer.h>
 
 #include "java_bytecode_parse_tree.h"
 
@@ -23,8 +24,8 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   bool disable_runtime_checks,
   size_t max_array_length,
-  std::vector<irep_idt> *needed_methods,
-  std::set<irep_idt> *needed_classes);
+  safe_pointer<std::vector<irep_idt> > needed_methods,
+  safe_pointer<std::set<irep_idt> > needed_classes);
 
 // Must provide both the optional parameters or neither.
 inline void java_bytecode_convert_method(
@@ -42,8 +43,8 @@ inline void java_bytecode_convert_method(
     message_handler,
     disable_runtime_checks,
     max_array_length,
-    nullptr,
-    nullptr);
+    safe_pointer<std::vector<irep_idt> >::create_null(),
+    safe_pointer<std::set<irep_idt> >::create_null());
 }
 
 void java_bytecode_convert_method_lazy(

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/safe_pointer.h>
 #include <analyses/cfg_dominators.h>
 #include "java_bytecode_parse_tree.h"
 #include "java_bytecode_convert_class.h"
@@ -31,8 +32,8 @@ class java_bytecode_convert_methodt:public messaget
     message_handlert &_message_handler,
     bool _disable_runtime_checks,
     size_t _max_array_length,
-    std::vector<irep_idt> *_needed_methods,
-    std::set<irep_idt> *_needed_classes):
+    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),
@@ -57,8 +58,8 @@ class java_bytecode_convert_methodt:public messaget
   symbol_tablet &symbol_table;
   const bool disable_runtime_checks;
   const size_t max_array_length;
-  std::vector<irep_idt> *needed_methods;
-  std::set<irep_idt> *needed_classes;
+  safe_pointer<std::vector<irep_idt> > needed_methods;
+  safe_pointer<std::set<irep_idt> > needed_classes;
 
   irep_idt method_id;
   irep_idt current_method;

src/java_bytecode/java_bytecode_language.cpp

@@ -586,8 +586,8 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
           get_message_handler(),
           disable_runtime_checks,
           max_user_array_length,
-          &method_worklist2,
-          &needed_classes);
+          safe_pointer<std::vector<irep_idt> >::create_non_null(&method_worklist2),
+          safe_pointer<std::set<irep_idt> >::create_non_null(&needed_classes));
         gather_virtual_callsites(
           symbol_table.lookup(mname).value,
           virtual_callsites);

src/util/safe_pointer.h

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: Simple checked pointers
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SAFE_POINTER_H
+#define CPROVER_UTIL_SAFE_POINTER_H
+
+template<class T> class safe_pointer
+{
+ public:
+  operator bool() const
+  {
+    return !!ptr;
+  }
+
+  T *get() const
+  {
+    assert(ptr && "dereferenced a null safe pointer");
+    return ptr;
+  }
+
+  T &operator*() const
+  {
+    return *get();
+  }
+
+  T *operator->() const
+  {
+    return get();
+  }
+
+  static safe_pointer<T> create_null()
+  {
+    return safe_pointer();
+  }
+
+  static safe_pointer<T> create_non_null(
+    T *target)
+  {
+    assert(target && "initialized safe pointer with null");
+    return safe_pointer(target);
+  }
+
+  static safe_pointer<T> create_maybe_null(
+    T *target)
+  {
+    return safe_pointer(target);
+  }
+
+ protected:
+  T *ptr;
+
+  explicit safe_pointer(T *target) : ptr(target)
+  {}
+
+  safe_pointer() : ptr(nullptr)
+  {}
+};
+
+#endif