Merge pull request #2354 from Degiorgio/disable-soundness-check-for-shared-pointers

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

Author: cesaro

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);