CSVSA: tolerate ID_unknown with weird types

Generally when value_sett responds with an ID_unknown it uses a type appropriate to the queried expression -- so when asking
about a parameter of type A* we could expect a response type-compatible with A*. However this is not rigorously enforced, and
certain recursive calls can generate an A, A[] can move back and forth with A, and potentially other irregularities. Rather
than try to enforce a policy, CSVSA now tolerates unusual responses and simply does its best to guess the intended type.

Author: smowton

src/pointer-analysis/context_sensitive_value_set_analysis.cpp

@@ -476,11 +476,34 @@ csvsa_function_contextt::get_virtual_callees(locationt l_call) const
     exprt val;
     if(raw_value.id() == ID_unknown)
     {
-      INVARIANT(
-        raw_value.type().id() == ID_pointer,
-        "an unknown expression used as a `this` arg should have pointer type");
+      // Under some circumstances the ID_unknown can indicate the type of the
+      // referred object, not the pointer. Given there are no hard and fast
+      // rules for the type of the returned ID_unknown we really just try our
+      // best to get a good hint about the referred object type here.
+
+      typet unknown_type = raw_value.type();
+      if(unknown_type.id() == ID_pointer)
+        unknown_type = unknown_type.subtype();
+
+      unknown_type = ns.follow(unknown_type);
+
+      if(unknown_type.id() != ID_struct)
+      {
+        // Last fallback: suppose the `this` argument type matches the virtual
+        // callee type. For example, if we're calling A.f() and `this` appears
+        // to be an unknown integer or something else impossible to call,
+        // we'll guess it must be at least an A*.
+        const code_typet::parametert *this_parameter =
+          to_code_type(call.function().type()).get_this();
+        INVARIANT(
+          this_parameter != nullptr,
+          "Virtual call should have 'this' parameter");
+
+        unknown_type =
+          ns.follow(to_pointer_type(this_parameter->type()).subtype());
+      }
 
-      val = exprt(ID_unknown, raw_value.type().subtype());
+      val = exprt(ID_unknown, unknown_type);
 
       // If the unknown is a parent of the expected this-argument type, or is of
       // opaque type and so unknown position in the class hierarchy, lift