Improve algorithm for determining possible callees:

* Discard candidates that aren't type-compatible with the callee's `this` arugment
* Promote ID_unknown values to at least the callee's type
* Warn if we still have to throw the unknown away (which indicates the static type is
  abstract, so we would have to have e.g. guessed that a call to java.Closable.close is
  actually java.io.FileInputStream.close, which is smarter than our stub-handling code
  at present.

Author: smowton

regression/CSVSA/TestIncompatibleTypes/A.class

@@ -0,0 +1,33 @@
+package CSVSA.TestIncompatibleTypes;
+
+public class Test {
+
+  public static void test(int unknown) {
+    A a = unknown == 0 ? new B() : new C();
+
+    if(a instanceof C) {
+      C c = (C)a;
+      // CSVSA should spot that the `new B()` above is not a possible callee.
+      c.f();
+    }
+  }
+
+}
+
+class A {
+
+  public void f() { }
+
+}
+
+class B extends A {
+
+  public void f() { }
+
+}
+
+class C extends A {
+
+  public void f() { }
+
+}

regression/CSVSA/TestIncompatibleTypes/B.class

@@ -0,0 +1,13 @@
+from regression.CSVSA.csvsa_driver import CsvsaDriver
+
+
+folder_name = 'TestIncompatibleTypes'
+
+
+def test_tolerate_unreachable_functions():
+    csvsa_driver = \
+        CsvsaDriver(folder_name).with_test_function('test').with_show_goto_functions(False)
+    with csvsa_driver.run() as csvsa_expectation:
+        csvsa_expectation.check_successful_run()
+        csvsa_expectation.check_matches("Callsite at 44 may call: java::CSVSA.TestIncompatibleTypes.C.f")
+        csvsa_expectation.check_does_not_match("Callsite at 44 may call: java::CSVSA.TestIncompatibleTypes.B.f")

regression/CSVSA/TestIncompatibleTypes/C.class

@@ -0,0 +1,43 @@
+package CSVSA.TestOpaqueTypePromotion;
+
+public class Test {
+
+  public static void test() {
+
+    AbstractTest at = Opaque.getAbstractTest();
+    // CSVSA should notice that the opaque object returned must have been
+    // a ConcreteTest if the `f()` call is reachable:
+    ((ConcreteTest)at).f();
+
+    // In this case CSVSA won't know what the call might target, and should stub
+    // the callsite (introduce a synthetic stub function)
+    at.f();
+
+    // In this case CSVSA shouldn't guess that we actually target ConcreteTest,
+    // as it doesn't know the parent-child relationship between the opaque type
+    // and ConcreteTest.
+    (new Opaque()).f();
+
+  }
+
+}
+
+abstract class AbstractTest {
+
+  abstract void f();
+
+}
+
+class ConcreteTest extends AbstractTest {
+
+  void f() { }
+
+}
+
+class Opaque extends ConcreteTest {
+
+  // For testing, this class is deleted, so the method
+  // definition is irrelevant.
+  public static AbstractTest getAbstractTest() { return new ConcreteTest(); }
+
+}

regression/CSVSA/TestIncompatibleTypes/Test.class

@@ -0,0 +1,14 @@
+from regression.CSVSA.csvsa_driver import CsvsaDriver
+
+
+folder_name = 'TestOpaqueTypePromotion'
+
+
+def test_opaque_type_promotion():
+    csvsa_driver = \
+        CsvsaDriver(folder_name).with_test_function('test').with_show_goto_functions(False)
+    with csvsa_driver.run() as csvsa_expectation:
+        csvsa_expectation.check_successful_run()
+        csvsa_expectation.check_matches("Callsite at 17 may call: java::CSVSA.TestOpaqueTypePromotion.ConcreteTest.f:()V")
+        csvsa_expectation.check_matches("Callsite at 25 (java::CSVSA.TestOpaqueTypePromotion.AbstractTest.f:()V) stubbed")
+        csvsa_expectation.check_matches("Callsite at 43 (java::CSVSA.TestOpaqueTypePromotion.Opaque.f:()V) stubbed")

regression/CSVSA/TestIncompatibleTypes/Test.java

@@ -22,6 +22,7 @@ def __init__(self, folder_name):
         self.folder_name = folder_name
         self.with_test_class_name('Test')
         self.with_test_function('f')
+        self.show_goto_functions = True
 
     def with_test_class_name(self, test_class_name):
         self.class_name = test_class_name
@@ -32,14 +33,21 @@ def with_test_function(self, test_function_name):
         self.function_name = test_function_name
         return self
 
+    def with_show_goto_functions(self, show_goto_functions):
+        self.show_goto_functions = show_goto_functions
+        return self
+
     def run(self):
         """Run CSVSA and parse the output before returning it"""
         fq_class_name = '.'.join(['CSVSA', self.folder_name, self.class_name])
         fq_function_name = fq_class_name + '.' + self.function_name
         executable_path = os.path.join(os.environ['SECURITY_SCANNER_HOME'], 'bin', 'security-analyzer')
         class_path = os.path.join('CSVSA', self.folder_name, self.class_filename)
-        cmd = [executable_path, '--function', fq_function_name, '--lazy-methods-context-sensitive',
-               '--show-goto-functions', class_path]
+        cmd = [executable_path, '--function', fq_function_name, '--lazy-methods-context-sensitive', class_path]
+        if self.show_goto_functions:
+            cmd.append('--show-goto-functions')
+        else:
+            cmd.append('--show-csvsa-value-sets')
 
         executable_runner = ExecutableRunner(cmd)
         (stdout, _, return_code) = executable_runner.run(pipe_stderr_to_stdout=True)

regression/CSVSA/TestIncompatibleTypes/__init__.py

@@ -179,6 +179,14 @@ int sec_driver_parse_optionst::doit()
     }
     csvsa_analysis=
       csvsa_load_and_analyze_functions(lazy_goto_model, get_message_handler());
+
+    if(cmdline.isset("show-csvsa-value-sets"))
+    {
+      csvsa_analysis->get_context(0).print_tree(lazy_goto_model, status());
+      status() << messaget::eom;
+
+      return CPROVER_EXIT_SUCCESS;
+    }
   }
   else
     lazy_goto_model.load_all_functions();
@@ -572,6 +580,11 @@ void sec_driver_parse_optionst::help()
     " --xml file_name                  output results in XML format to given file\n"
     " --function                       set main function name\n"
     " --lvsa-summary-directory         directory to store LVSA summaries\n"
+    " --lazy-methods-context-sensitive use CSVSA to determine which methods to\n" // NOLINT (*)
+    "                                  load and specialize functions to resolve\n" // NOLINT (*)
+    "                                  their virtual callsites\n"
+    " --show-csvsa-value-sets          print CSVSA's value sets (possible pointer\n" // NOLINT (*)
+    "                                  targets) and exit.\n"
     "\n"
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar              set the classpath\n"

regression/CSVSA/TestIncompatibleTypes/test_incompatible_types.py

@@ -47,6 +47,7 @@ class optionst;
   "(do-not-use-precise-access-paths)" \
   "(rebuild-taint-cache)" \
   "(lazy-methods-context-sensitive)" \
+  "(show-csvsa-value-sets)" \
   UI_MESSAGE_OPTIONS \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   // End of options

regression/CSVSA/TestOpaqueTypePromotion/AbstractTest.class

@@ -419,12 +419,31 @@ void csvsa_function_contextt::transform_function_stub(
   transform_child_callsite(l_call, {fname});
 }
 
+// TODO: Replace this with a graph visitor that can terminate the graph walk
+// when it finds a node of interest.
+static bool is_ancestor(
+  const irep_idt &ancestor,
+  irep_idt candidate,
+  const class_hierarchyt &class_hierarchy)
+{
+  if(ancestor == candidate)
+    return true;
+  auto ancestors = class_hierarchy.get_parents_trans(candidate);
+  return
+    std::find(ancestors.begin(), ancestors.end(), ancestor) != ancestors.end();
+}
+
 dispatch_table_entriest
 csvsa_function_contextt::get_virtual_callees(locationt l_call) const
 {
   const auto &call = to_code_function_call(l_call->code);
   INVARIANT(!call.arguments().empty(), "virtual calls must have a 'this' arg");
   const auto &this_expr = call.arguments()[0];
+  irep_idt namespaced_this_tag =
+    "java::" +
+    id2string(
+      to_struct_type(
+        ns.follow(to_pointer_type(this_expr.type()).subtype())).get_tag());
 
   dispatch_table_entriest callees;
   std::unordered_set<irep_idt, irep_id_hash> seen_class_ids;
@@ -440,6 +459,8 @@ csvsa_function_contextt::get_virtual_callees(locationt l_call) const
   const_cast<csvsa_function_contextt *>(this)->get_values(
     l_call, this_expr, raw_values);
 
+  const auto &class_hierarchy = driver.get_class_hierarchy();
+
   for(const auto &raw_value : raw_values)
   {
     // Ignore invalid / failed objects, which represent uninitialized pointers,
@@ -456,7 +477,23 @@ csvsa_function_contextt::get_virtual_callees(locationt l_call) const
       INVARIANT(
         raw_value.type().id() == ID_pointer,
         "an unknown expression used as a `this` arg should have pointer type");
+
       val = exprt(ID_unknown, raw_value.type().subtype());
+
+      // 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
+      // it to at least that type. Presumably this is something like an opaque
+      // method that returns an Object, which is later cast to a derived type.
+      const auto &struct_type = to_struct_type(ns.follow(val.type()));
+      const auto &struct_tag = struct_type.get_tag();
+      irep_idt namespaced_tag = "java::"+id2string(struct_tag);
+
+      if(
+        !struct_type.get_bool(ID_incomplete_class) &&
+        is_ancestor(namespaced_tag, namespaced_this_tag, class_hierarchy))
+      {
+        val.type() = symbol_typet(namespaced_this_tag);
+      }
     }
     else
       val = to_object_descriptor_expr(raw_value).object();
@@ -499,11 +536,21 @@ csvsa_function_contextt::get_virtual_callees(locationt l_call) const
       if(!seen_class_ids.insert(struct_tag).second)
         continue;
 
-      irep_idt namespaced_tag = "java::" + id2string(struct_tag);
+      irep_idt namespaced_tag = "java::"+id2string(struct_tag);
       const auto &function_name = call.function().get(ID_component_name);
+      resolve_inherited_componentt resolver(
+        ns.get_symbol_table(), class_hierarchy);
 
       const auto actual_callee = resolver(namespaced_tag, function_name, false);
-      if(actual_callee.is_valid())
+      if(!real_type.get_bool(ID_incomplete_class) &&
+         !is_ancestor(namespaced_this_tag, namespaced_tag, class_hierarchy))
+      {
+        // Skip values that can't be the callee because they are not derived
+        // from the `this` type of the callee (e.g. an `Object` instance cannot
+        // possibly be the callee of `A.f()`)
+        continue;
+      }
+      else if(actual_callee.is_valid())
       {
         dispatch_table_entryt new_callee;
         new_callee.class_id = namespaced_tag;
@@ -516,10 +563,27 @@ csvsa_function_contextt::get_virtual_callees(locationt l_call) const
       {
         // Stub call -- guess it exists on the first opaque parent type of the
         // given type:
-        const auto &hierarchy = driver.get_class_hierarchy();
         irep_idt callee_class = call.function().get(ID_C_class);
         while(!ns.lookup(callee_class).type.get_bool(ID_incomplete_class))
-          callee_class = hierarchy.class_map.at(callee_class).parents.at(0);
+        {
+          const auto &parents =
+            class_hierarchy.class_map.at(callee_class).parents;
+          if(parents.size() == 0)
+          {
+            warning() << "Can't find a possible callee for a value of type "
+                      << struct_tag << " calling "
+                      << call.function().get(ID_identifier) << messaget::eom;
+            callee_class = irep_idt();
+            break;
+          }
+          else
+          {
+            callee_class = parents.at(0);
+          }
+        }
+
+        if(callee_class.empty())
+          continue;
 
         irep_idt callee_function =
           id2string(callee_class) + "." + id2string(function_name);

regression/CSVSA/TestOpaqueTypePromotion/ConcreteTest.class

@@ -464,6 +464,19 @@ class csvsa_function_contextt : private value_set_analysist, public messaget
     std::ostream &out,
     bool brief = false) const;
 
+  /// Print a plain-text dump starting from the entry point:
+  void print_tree(
+    abstract_goto_modelt &goto_model,
+    std::ostream &out,
+    bool brief = false) const
+  {
+    print_tree(
+      goto_model.get_goto_function(goto_functionst::entry_point()).body,
+      0,
+      out,
+      brief);
+  }
+
   /// Print a brief plain-text dump of this context and its children
   void print_tree_brief(
     const goto_programt &prog,