Add unit tests for value-set-analysis customisation

unit/Makefile

@@ -23,6 +23,7 @@ SRC += unit_tests.cpp \
        miniBDD_new.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_utils_test.cpp \
+       pointer-analysis/custom_value_set_analysis.cpp \
        sharing_node.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

unit/pointer-analysis/CustomVSATest.java

@@ -0,0 +1,46 @@
+
+public class CustomVSATest {
+
+  public Object never_read;
+
+  public static Object cause;
+  public static Object effect;
+  public static Object first_effect_read;
+  public static Object second_effect_read;
+  public static Object maybe_unknown_read;
+
+  public static void test() {
+
+    Object weak_local = new Object();
+    // Under standard VSA the following should be a strong write;
+    // with our test custom VSA it will be weak.
+    weak_local = new Object();
+
+    // Normally this would set the value of `ignored`, but our custom
+    // VSA discards the instruction completely:
+    Object ignored = new Object();
+
+    // Similarly this write should have no effect:
+    Object no_write = new Object();
+
+    CustomVSATest vsa = new CustomVSATest();
+    vsa.never_read = new Object();
+
+    // Again this should be disregarded:
+    Object read = vsa.never_read;
+
+    // This should acquire a "*" unknown-object, even though
+    // it is obvious what it points to:
+    Object maybe_unknown = new Object();
+    maybe_unknown_read=maybe_unknown;
+
+    effect = new Object();
+    first_effect_read = effect;
+
+    // Under our custom VSA, this write should cause effect to become null:
+    cause = new Object();
+    second_effect_read = effect;
+
+  }
+
+}

unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -0,0 +1,325 @@
+/*******************************************************************\
+
+Module: Value-set analysis tests
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/config.h>
+#include <langapi/mode.h>
+#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/goto_inline.h>
+#include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/java_types.h>
+#include <pointer-analysis/value_set_analysis.h>
+
+/// An example customised value_sett. It makes a series of small changes
+/// to the underlying value_sett logic, which can then be verified by the
+/// test below:
+/// * Writes to variables with 'ignored' in their name are ignored.
+/// * Never propagate values via the field "never_read"
+/// * Adds an ID_unknown to the value of variable "maybe_unknown" as it is read
+/// * When a variable named `cause` is written, one named `effect` is zeroed.
+class test_value_sett:public value_sett
+{
+public:
+  static bool assigns_to_ignored_variable(const code_assignt &assign)
+  {
+    if(assign.lhs().id()!=ID_symbol)
+      return false;
+    const irep_idt &id=to_symbol_expr(assign.lhs()).get_identifier();
+    return id2string(id).find("ignored")!=std::string::npos;
+  }
+
+  void apply_code_rec(const codet &code, const namespacet &ns) override
+  {
+    // Ignore assignments to the local "ignored"
+    if(code.get_statement()==ID_assign &&
+       assigns_to_ignored_variable(to_code_assign(code)))
+    {
+      return;
+    }
+    else
+    {
+      value_sett::apply_code_rec(code, ns);
+    }
+  }
+
+  void assign_rec(
+    const exprt &lhs,
+    const object_mapt &values_rhs,
+    const std::string &suffix,
+    const namespacet &ns,
+    bool add_to_sets) override
+  {
+    // Disregard writes against variables containing 'no_write':
+    if(lhs.id()==ID_symbol)
+    {
+      const irep_idt &id=to_symbol_expr(lhs).get_identifier();
+      if(id2string(id).find("no_write")!=std::string::npos)
+        return;
+    }
+
+    value_sett::assign_rec(lhs, values_rhs, suffix, ns, add_to_sets);
+  }
+
+  void get_value_set_rec(
+    const exprt &expr,
+    object_mapt &dest,
+    const std::string &suffix,
+    const typet &original_type,
+    const namespacet &ns) const override
+  {
+    // Ignore reads from fields named "never_read"
+    if(expr.id()==ID_member &&
+       to_member_expr(expr).get_component_name()=="never_read")
+    {
+      return;
+    }
+    else
+    {
+      value_sett::get_value_set_rec(
+        expr, dest, suffix, original_type, ns);
+    }
+  }
+
+  void adjust_assign_rhs_values(
+    const exprt &expr,
+    const namespacet &ns,
+    object_mapt &dest) const override
+  {
+    // Always add an ID_unknown to reads from variables containing
+    // "maybe_unknown":
+    exprt read_sym=expr;
+    while(read_sym.id()==ID_typecast)
+      read_sym=read_sym.op0();
+    if(read_sym.id()==ID_symbol)
+    {
+      const irep_idt &id=to_symbol_expr(read_sym).get_identifier();
+      if(id2string(id).find("maybe_unknown")!=std::string::npos)
+        insert(dest, exprt(ID_unknown, read_sym.type()));
+    }
+  }
+
+  void apply_assign_side_effects(
+    const exprt &lhs,
+    const exprt &rhs,
+    const namespacet &ns) override
+  {
+    // Whenever someone touches the variable "cause", null the
+    // variable "effect":
+    if(lhs.id()==ID_symbol)
+    {
+      const irep_idt &id=to_symbol_expr(lhs).get_identifier();
+      const auto &id_str=id2string(id);
+      auto find_idx=id_str.find("cause");
+      if(find_idx!=std::string::npos)
+      {
+        std::string effect_id=id_str;
+        effect_id.replace(find_idx, 5, "effect");
+        assign(
+          symbol_exprt(effect_id, lhs.type()),
+          null_pointer_exprt(to_pointer_type(lhs.type())),
+          ns,
+          true,
+          false);
+      }
+    }
+  }
+};
+
+typedef
+  value_set_analysis_templatet<value_set_domain_templatet<test_value_sett>>
+  test_value_set_analysist;
+
+#define TEST_PREFIX "java::CustomVSATest."
+#define TEST_FUNCTION_NAME TEST_PREFIX "test:()V"
+#define TEST_LOCAL_PREFIX TEST_FUNCTION_NAME "::"
+
+template<class VST>
+static value_setst::valuest
+get_values(const VST &value_set, const namespacet &ns, const exprt &expr)
+{
+  value_setst::valuest vals;
+  value_set.get_value_set(expr, vals, ns);
+  return vals;
+}
+
+static std::size_t exprs_with_id(
+  const value_setst::valuest &exprs, const irep_idt &id)
+{
+  return std::count_if(
+    exprs.begin(),
+    exprs.end(),
+    [&id](const exprt &expr)
+    {
+      return expr.id()==id ||
+        (expr.id()==ID_object_descriptor &&
+         to_object_descriptor_expr(expr).object().id()==id);
+    });
+}
+
+SCENARIO("test_value_set_analysis",
+         "[core][pointer-analysis][value_set_analysis]")
+{
+  GIVEN("Normal and custom value-set analysis of CustomVSATest::test")
+  {
+    null_message_handlert null_output;
+    cmdlinet command_line;
+
+    // This classpath is the default, but the config object
+    // is global and previous unit tests may have altered it
+    command_line.set("java-cp-include-files", ".");
+    config.java.classpath={"."};
+    command_line.args.push_back("pointer-analysis/CustomVSATest.jar");
+
+    register_language(new_java_bytecode_language);
+
+    goto_modelt goto_model=
+      initialize_goto_model(command_line, null_output);
+
+    namespacet ns(goto_model.symbol_table);
+
+    // Fully inline the test program, to avoid VSA conflating
+    // constructor callsites confusing the results we're trying to check:
+    goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output);
+
+    const goto_programt &test_function=
+      goto_model.goto_functions.function_map.at(TEST_PREFIX "test:()V").body;
+
+    value_set_analysist::locationt test_function_end=
+      std::prev(test_function.instructions.end());
+
+    value_set_analysist normal_analysis(ns);
+    normal_analysis(goto_model.goto_functions);
+    const auto &normal_function_end_vs=
+      normal_analysis[test_function_end].value_set;
+
+    test_value_set_analysist test_analysis(ns);
+    test_analysis(goto_model.goto_functions);
+    const auto &test_function_end_vs=
+      test_analysis[test_function_end].value_set;
+
+    reference_typet jlo_ref_type=java_lang_object_type();
+
+    WHEN("Writing to a local named 'ignored'")
+    {
+      symbol_exprt written_symbol(
+        TEST_LOCAL_PREFIX "23::ignored", jlo_ref_type);
+      THEN("The normal analysis should write to it")
+      {
+        auto normal_exprs=
+          get_values(normal_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1);
+        REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0);
+      }
+      THEN("The custom analysis should ignore the write to it")
+      {
+        auto test_exprs=
+          get_values(test_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==0);
+        REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1);
+      }
+    }
+
+    WHEN("Writing to a local named 'no_write'")
+    {
+      symbol_exprt written_symbol(
+        TEST_LOCAL_PREFIX "31::no_write", jlo_ref_type);
+      THEN("The normal analysis should write to it")
+      {
+        auto normal_exprs=
+          get_values(normal_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1);
+        REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0);
+      }
+      THEN("The custom analysis should ignore the write to it")
+      {
+        auto test_exprs=
+          get_values(test_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==0);
+        REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1);
+      }
+    }
+
+    WHEN("Reading from a field named 'never_read'")
+    {
+      symbol_exprt written_symbol(
+        TEST_LOCAL_PREFIX "55::read", jlo_ref_type);
+      THEN("The normal analysis should find a dynamic object")
+      {
+        auto normal_exprs=
+          get_values(normal_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1);
+        REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0);
+      }
+      THEN("The custom analysis should have no information about it")
+      {
+        auto test_exprs=
+          get_values(test_function_end_vs, ns, written_symbol);
+        REQUIRE(test_exprs.size()==0);
+      }
+    }
+
+    WHEN("Reading from a variable named 'maybe_unknown'")
+    {
+      symbol_exprt written_symbol(
+        TEST_PREFIX "maybe_unknown_read", jlo_ref_type);
+      THEN("The normal analysis should find a dynamic object")
+      {
+        auto normal_exprs=
+          get_values(normal_function_end_vs, ns, written_symbol);
+        REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1);
+        REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0);
+      }
+      THEN("The custom analysis should find a dynamic object "
+           "*and* an unknown entry")
+      {
+        auto test_exprs=
+          get_values(test_function_end_vs, ns, written_symbol);
+        REQUIRE(test_exprs.size()==2);
+        REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1);
+        REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==1);
+      }
+    }
+
+    WHEN("Writing to a variable named 'cause'")
+    {
+      symbol_exprt read_before_cause_write(
+        TEST_PREFIX "first_effect_read", jlo_ref_type);
+        auto normal_exprs_before=
+          get_values(normal_function_end_vs, ns, read_before_cause_write);
+        auto test_exprs_before=
+          get_values(test_function_end_vs, ns, read_before_cause_write);
+      symbol_exprt read_after_cause_write(
+        TEST_PREFIX "second_effect_read", jlo_ref_type);
+        auto normal_exprs_after=
+          get_values(normal_function_end_vs, ns, read_after_cause_write);
+        auto test_exprs_after=
+          get_values(test_function_end_vs, ns, read_after_cause_write);
+
+      THEN("Before writing to 'cause' both analyses should think 'effect' "
+           "points to some object")
+      {
+        REQUIRE(normal_exprs_before.size()==1);
+        REQUIRE(exprs_with_id(normal_exprs_before, ID_dynamic_object)==1);
+
+        REQUIRE(test_exprs_before.size()==1);
+        REQUIRE(exprs_with_id(test_exprs_before, ID_dynamic_object)==1);
+      }
+
+      THEN("After writing to 'cause', the normal analysis should see no change "
+           "to 'effect', while the custom analysis should see it changed")
+      {
+        REQUIRE(normal_exprs_after.size()==1);
+        REQUIRE(exprs_with_id(normal_exprs_after, ID_dynamic_object)==1);
+
+        REQUIRE(test_exprs_after.size()==1);
+        REQUIRE(exprs_with_id(test_exprs_after, "NULL-object")==1);
+      }
+    }
+  }
+}