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.

Author: tautschnig

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, "");
+}

regression/cbmc/Pointer_Arithmetic14/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;