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,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       }
     }
   }
+
+  if(cmdline.isset("java-threading"))
+    options.set_option("java-threading", true);
 }
 
 /// invoke main modules

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_unsound_pointer_handling)
 {
   // identifier should be l0 or l1, make sure it's l1
   rename(lhs, ns, L1);
@@ -343,7 +344,9 @@ 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_unsound_pointer_handling)
     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_unsound_pointer_handling=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,
+    options.get_bool_option("java-threading"));
 
   exprt ssa_full_lhs=full_lhs;
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);