Skip check for unsoundness in shared pointer handling (java only)

If the 'java-threading' option is specified this commit prevents symex
from throwing an exception when it encounters pointers that are shared
across threads. This is unsound but given that pointers are ubiquitous
in java this check must be disabled (until the concurrency encoding is
fixed).

Author: Degiorgio

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -399,6 +399,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       }
     }
   }
+
+  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
+  // exception when it encounters pointers that are shared across threads.
+  // This is unsound but given that pointers are ubiquitous in java this check
+  // must be disabled in order to support the analysis of multithreaded java
+  // code.
+  if(cmdline.isset("java-threading"))
+    options.set_option("allow-pointer-unsoundness", true);
 }
 
 /// invoke main modules

src/goto-symex/goto_symex.h

@@ -58,6 +58,8 @@ class goto_symext
       options(options),
       max_depth(options.get_unsigned_int_option("depth")),
       doing_path_exploration(options.is_set("paths")),
+      allow_pointer_unsoundness(
+        options.get_bool_option("allow-pointer-unsoundness")),
       total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
@@ -201,6 +203,7 @@ class goto_symext
 
   const unsigned max_depth;
   const bool doing_path_exploration;
+  const bool allow_pointer_unsoundness;
 
 public:
   // these bypass the target maps

src/goto-symex/goto_symex_state.cpp

@@ -311,7 +311,8 @@ void goto_symex_statet::assignment(
   const exprt &rhs,  // L2
   const namespacet &ns,
   bool rhs_is_simplified,
-  bool record_value)
+  bool record_value,
+  bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
   rename(lhs, ns, L1);
@@ -343,7 +344,7 @@ void goto_symex_statet::assignment(
   assert_l2_renaming(rhs);
 
   // see #305 on GitHub for a simple example and possible discussion
-  if(is_shared && lhs.type().id() == ID_pointer)
+  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
     throw "pointer handling for concurrency is unsound";
 
   // for value propagation -- the RHS is L2

src/goto-symex/goto_symex_state.h

@@ -175,7 +175,8 @@ class goto_symex_statet final
     const exprt &rhs,  // L2
     const namespacet &ns,
     bool rhs_is_simplified,
-    bool record_value);
+    bool record_value,
+    bool allow_pointer_unsoundness=false);
 
   // what to propagate
   bool constant_propagation(const exprt &expr) const;

src/goto-symex/symex_assign.cpp

@@ -232,7 +232,8 @@ void goto_symext::symex_assign_symbol(
     ssa_rhs,
     ns,
     options.get_bool_option("simplify"),
-    constant_propagation);
+    constant_propagation,
+    allow_pointer_unsoundness);
 
   exprt ssa_full_lhs=full_lhs;
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);