Add special case for deref-of-typecast-of-if

This results from expressions such as *(int*)*p, and is very nearly as easy to handle as the
already-special-cased deref-of-if case. In essence we transform *(type*)(x ? y : z) into
x ? *(type*)y : *(type*)z, which should yield a more compact expression due to not conflating
the alias sets that can be derived from the two arms of the conditional.

Author: smowton

regression/cbmc/double_deref/README

@@ -20,7 +20,7 @@ result = (derefd_pointer == &o3 ? o3 : derefd_pointer == &o4 ? o4 : derefd_point
 
 The tests in this directory check that auxiliary let-expressions like this are only used when appropriate by inspecting formula VCCs:
 double_deref.desc -- a directly nested double-dereference, should not use a let-expression
-double_deref_with_cast.desc -- a double-deref with an intervening cast (*(int*)*p for example), should use a let-expression
+double_deref_with_cast.desc -- a double-deref with an intervening cast (*(int*)*p for example), should not use a let-expression
 double_deref_with_member.desc -- a double-deref with an intervening member expression (p->field1->field2), should use a let-expression
 double_deref_with_pointer_arithmetic.desc -- a double-deref with intervening pointer arithmetic (p[idx1][idx2]), should use a let-expression
 *_single_alias.desc -- variants of the above where the first dereference points to a single possible object, so no let-expression is necessary

regression/cbmc/double_deref/double_deref_with_cast.desc

@@ -1,10 +1,10 @@
 CORE
 double_deref_with_cast.c
 --show-vcc
-^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 =
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[1-9]+\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]
+\{1\} \(cast\(main::1::pptr!0@1#2, signedbv\[32\]\*\*\) = address_of\(main::1::ptr2!0@1\) \? main::argc!0@1#1 = 2 \: main::argc!0@1#1 = 1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
+derefd_pointer::derefd_pointer
 --
 See README for details about these tests

src/pointer-analysis/value_set_dereference.cpp

@@ -72,6 +72,27 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     exprt false_case = dereference(if_expr.false_case());
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
+  else if(pointer.id() == ID_typecast)
+  {
+    const exprt *underlying = &pointer;
+    // Note this isn't quite the same as skip_typecast, which would also skip
+    // things such as int-to-ptr typecasts which we shouldn't ignore
+    while(
+      underlying->id() == ID_typecast && underlying->type().id() == ID_pointer)
+    {
+      underlying = &to_typecast_expr(*underlying).op();
+    }
+
+    if(underlying->id() == ID_if && underlying->type().id() == ID_pointer)
+    {
+      const auto &if_expr = to_if_expr(*underlying);
+      return
+        if_exprt(
+          if_expr.cond(),
+          dereference(typecast_exprt(if_expr.true_case(), pointer.type())),
+          dereference(typecast_exprt(if_expr.false_case(), pointer.type())));
+    }
+  }
 
   // type of the object
   const typet &type=pointer.type().subtype();