From cc941d3ad55079acd4bc60a40e887d581156fe49 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 12 Jul 2019 20:21:29 +0000
Subject: [PATCH] Value sets: Support bit operations over pointers

Bit operations on pointers are used to defend against side channels
resulting from speculative execution. Hence we need to support these.
Without the support in value sets we silently just returned "unknown"
and thus subsequent dereferencing would fail.
---
 regression/cbmc/Pointer_Arithmetic14/main.c    | 16 ++++++++++++++++
 regression/cbmc/Pointer_Arithmetic14/test.desc |  8 ++++++++
 src/pointer-analysis/value_set.cpp             | 12 ++++++++----
 3 files changed, 32 insertions(+), 4 deletions(-)
 create mode 100644 regression/cbmc/Pointer_Arithmetic14/main.c
 create mode 100644 regression/cbmc/Pointer_Arithmetic14/test.desc

diff --git a/regression/cbmc/Pointer_Arithmetic14/main.c b/regression/cbmc/Pointer_Arithmetic14/main.c
new file mode 100644
index 0000000000..764b0cb1ff
--- /dev/null
+++ b/regression/cbmc/Pointer_Arithmetic14/main.c
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int main()
+{
+  int a = 42;
+  size_t mask = ~(size_t)0;
+  // applying bitmasks to pointers is used to defend against speculative
+  // execution side channels, hence we need to support this
+  __CPROVER_assert(*(int *)(mask & (size_t)&a) == 42, "");
+
+  // the following bitmasks are for completeness of the test only, they aren't
+  // necessarily as useful in practice
+  size_t mask_zero = 0;
+  __CPROVER_assert(*(int *)(mask_zero | (size_t)&a) == 42, "");
+  __CPROVER_assert(*(int *)(mask_zero ^ (size_t)&a) == 42, "");
+}
diff --git a/regression/cbmc/Pointer_Arithmetic14/test.desc b/regression/cbmc/Pointer_Arithmetic14/test.desc
new file mode 100644
index 0000000000..9efefbc736
--- /dev/null
+++ b/regression/cbmc/Pointer_Arithmetic14/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 87be2303a0..bc583e8e29 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -642,8 +642,11 @@ void value_sett::get_value_set_rec(
     else
       insert(dest, exprt(ID_unknown, original_type));
   }
-  else if(expr.id()==ID_plus ||
-          expr.id()==ID_minus)
+  else if(
+    expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_bitor ||
+    expr.id() == ID_bitand || expr.id() == ID_bitxor ||
+    expr.id() == ID_bitnand || expr.id() == ID_bitnor ||
+    expr.id() == ID_bitxnor)
   {
     if(expr.operands().size()<2)
       throw expr.id_string()+" expected to have at least two operands";
@@ -653,8 +656,9 @@ void value_sett::get_value_set_rec(
 
     // special case for pointer+integer
 
-    if(expr.operands().size()==2 &&
-       expr_type.id()==ID_pointer)
+    if(
+      expr.operands().size() == 2 && expr_type.id() == ID_pointer &&
+      (expr.id() == ID_plus || expr.id() == ID_minus))
     {
       exprt ptr_operand;