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

@@ -8,7 +8,7 @@ operator, such as **p, *(int*)*p, p->field1->field2, etc. At present a directly
 (p == &o1 ? (o1 == &o3 ? o3 : o4) : (o2 == &o5 ? o5 : o6))
 
 This deref operator push-in is performed (implicitly) by value_set_dereferencet::dereference, which special-cases
-the ternary conditional expression.
+the ternary conditional expression and typecasts of ternary conditionals.
 More complicated expressions are handled using a let-expression. Example:
 
 p->field1->field2 ==>
@@ -21,7 +21,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,26 @@ 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();