From 7d4d4bd5d9dcc54ce1c2f80d2e12f014e84f2d8f Mon Sep 17 00:00:00 2001
From: Kurt Degiorgio <degiorgiokurt@outlook.com>
Date: Thu, 14 Jun 2018 21:25:57 +0100
Subject: [PATCH] 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).
---
 jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ++++++++
 src/goto-symex/goto_symex.h          | 3 +++
 src/goto-symex/goto_symex_state.cpp  | 5 +++--
 src/goto-symex/goto_symex_state.h    | 3 ++-
 src/goto-symex/symex_assign.cpp      | 3 ++-
 5 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 7e10eb471a6..aef623f4536 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/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
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 6ab6d0416dd..0e7342c2493 100644
--- a/src/goto-symex/goto_symex.h
+++ b/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
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 40612693ed7..e306a86d13d 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/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
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index b6c839c7659..6051d034ac9 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/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;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 6465fb9f7d3..d9dcc19c498 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/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);