Merge pull request #4902 from tautschnig/bitand

Value sets: Support bitand/bitor over pointers

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;