Merge pull request #5568 from jezhiggins/expression-transform

Expression transform

Author: martin-cs

src/analyses/variable-sensitivity/value_set_abstract_value.cpp

@@ -9,6 +9,7 @@
 #include "value_set_abstract_value.h"
 
 #include <ansi-c/expr2c.h>
+#include <util/simplify_expr.h>
 
 value_set_abstract_valuet::value_set_abstract_valuet(
   const typet &type,
@@ -125,3 +126,92 @@ void value_set_abstract_valuet::output(
   }
   out << "}";
 }
+
+static void merge_all_possible_results(
+  std::shared_ptr<const value_set_abstract_valuet> &out_value,
+  const exprt &expr,
+  const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
+  const namespacet &ns,
+  std::vector<exprt> &operands_so_far)
+{
+  if(expr.operands().size() == operands_so_far.size())
+  {
+    exprt expr_with_evaluated_operands_filled_in = expr;
+    expr_with_evaluated_operands_filled_in.operands() = operands_so_far;
+    simplify(expr_with_evaluated_operands_filled_in, ns);
+    if(expr_with_evaluated_operands_filled_in.is_constant())
+    {
+      bool out_modifications;
+      auto post_merge = abstract_objectt::merge(
+        out_value,
+        std::make_shared<value_set_abstract_valuet>(
+          expr.type(),
+          value_set_abstract_valuet::valuest{
+            expr_with_evaluated_operands_filled_in}),
+        out_modifications);
+      if(
+        auto post_merge_casted =
+          std::dynamic_pointer_cast<const value_set_abstract_valuet>(
+            post_merge))
+      {
+        out_value = post_merge_casted;
+        return;
+      }
+    }
+    out_value = std::make_shared<value_set_abstract_valuet>(expr.type());
+  }
+  else
+  {
+    for(auto const &operand_value :
+        operand_value_sets[operands_so_far.size()]->get_values())
+    {
+      operands_so_far.push_back(operand_value);
+      merge_all_possible_results(
+        out_value, expr, operand_value_sets, ns, operands_so_far);
+      operands_so_far.pop_back();
+    }
+  }
+}
+
+static std::shared_ptr<const value_set_abstract_valuet>
+merge_all_possible_results(
+  const exprt &expr,
+  const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
+  const namespacet &ns)
+{
+  const bool is_top = false;
+  const bool is_bottom = true;
+  auto result_abstract_value =
+    std::make_shared<const value_set_abstract_valuet>(
+      expr.type(), is_top, is_bottom);
+  auto operands_so_far = std::vector<exprt>{};
+  merge_all_possible_results(
+    result_abstract_value, expr, operand_value_sets, ns, operands_so_far);
+  return result_abstract_value;
+}
+
+abstract_object_pointert value_set_abstract_valuet::expression_transform(
+  const exprt &expr,
+  const std::vector<abstract_object_pointert> &operands,
+  const abstract_environmentt &environment,
+  const namespacet &ns) const
+{
+  // TODO possible special case handling for things like
+  //  __CPROVER_rounding_mode where we know what valid values look like
+  //  which we could make use of in place of TOP
+  auto operand_value_sets = std::vector<const value_set_abstract_valuet *>{};
+  for(auto const &possible_value_set : operands)
+  {
+    PRECONDITION(possible_value_set != nullptr);
+    const auto as_value_set =
+      dynamic_cast<const value_set_abstract_valuet *>(possible_value_set.get());
+    if(
+      as_value_set == nullptr || as_value_set->is_top() ||
+      as_value_set->is_bottom())
+    {
+      return std::make_shared<value_set_abstract_valuet>(expr.type());
+    }
+    operand_value_sets.push_back(as_value_set);
+  }
+  return merge_all_possible_results(expr, operand_value_sets, ns);
+}

src/analyses/variable-sensitivity/value_set_abstract_value.h

@@ -44,6 +44,12 @@ class value_set_abstract_valuet : public abstract_valuet
 
   exprt to_constant() const override;
 
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override;
+
   void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
     const override;
 

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

@@ -8,6 +8,7 @@
 #include "variable_sensitivity_object_factory.h"
 #include "interval_array_abstract_object.h"
 #include "util/namespace.h"
+#include "value_set_abstract_value.h"
 
 variable_sensitivity_object_factoryt
   variable_sensitivity_object_factoryt::s_instance;
@@ -24,10 +25,18 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(const typet type)
   {
     abstract_object_type =
       configuration.advanced_sensitivities.intervals ? INTERVAL : CONSTANT;
+    if(configuration.advanced_sensitivities.new_value_set)
+    {
+      abstract_object_type = VALUE_SET;
+    }
   }
   else if(type.id() == ID_floatbv)
   {
     abstract_object_type = CONSTANT;
+    if(configuration.advanced_sensitivities.new_value_set)
+    {
+      abstract_object_type = VALUE_SET;
+    }
   }
   else if(type.id() == ID_array)
   {
@@ -121,6 +130,11 @@ variable_sensitivity_object_factoryt::get_abstract_object(
     return initialize_abstract_object<abstract_objectt>(
       followed_type, top, bottom, e, environment, ns);
   case VALUE_SET:
+    if(configuration.advanced_sensitivities.new_value_set)
+    {
+      return initialize_abstract_object<value_set_abstract_valuet>(
+        followed_type, top, bottom, e, environment, ns);
+    }
     return initialize_abstract_object<value_set_abstract_objectt>(
       followed_type, top, bottom, e, environment, ns);
   default:

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h

@@ -50,6 +50,7 @@ struct vsd_configt
   {
     bool intervals;
     bool value_set;
+    bool new_value_set;
   } advanced_sensitivities;
 
   static vsd_configt from_options(const optionst &options)
@@ -83,6 +84,8 @@ struct vsd_configt
       options.get_bool_option("interval");
     config.advanced_sensitivities.value_set =
       options.get_bool_option("value-set");
+    config.advanced_sensitivities.new_value_set =
+      options.get_bool_option("new-value-set");
 
     return config;
   }

unit/analyses/variable-sensitivity/value_set/abstract_value.cpp

@@ -12,6 +12,7 @@ Author: Diffblue Ltd.
 #include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
 #include <ansi-c/expr2c.h>
 
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <sstream>
 #include <string>
 #include <util/arith_tools.h>
@@ -57,6 +58,7 @@ class ContainsAllOf
       {
         oss << ", ";
       }
+      first = false;
       oss << expr2c(value, ns);
     }
     oss << " }";
@@ -359,3 +361,119 @@ TEST_CASE(
 
   REQUIRE(value_set.to_constant() == value);
 }
+
+static abstract_environmentt get_value_set_abstract_environment()
+{
+  vsd_configt config;
+  config.advanced_sensitivities.new_value_set = true;
+  config.context_tracking.data_dependency_context = false;
+  config.context_tracking.last_write_context = false;
+  variable_sensitivity_object_factoryt::instance().set_options(config);
+  auto environment = abstract_environmentt{};
+  environment.make_top();
+  return environment;
+}
+
+TEST_CASE("Eval on an constant gives us that constant", VALUE_SET_TEST_TAGS)
+{
+  const auto environment = get_value_set_abstract_environment();
+  namespacet ns{symbol_tablet{}};
+  const auto zero = from_integer(0, signedbv_typet{32});
+  const auto eval_result = environment.eval(zero, ns);
+  REQUIRE(eval_result != nullptr);
+  REQUIRE(!eval_result->is_top());
+  REQUIRE(!eval_result->is_bottom());
+  const auto eval_result_as_value_set =
+    std::dynamic_pointer_cast<const value_set_abstract_valuet>(
+      eval_result->unwrap_context());
+  REQUIRE(eval_result_as_value_set != nullptr);
+  REQUIRE(eval_result_as_value_set->get_values().size() == 1);
+  REQUIRE_THAT(eval_result_as_value_set->get_values(), ContainsAllOf{zero});
+}
+
+TEST_CASE(
+  "Eval on a plus expression with constant operands gives us the result of "
+  "that plus",
+  VALUE_SET_TEST_TAGS)
+{
+  const auto environment = get_value_set_abstract_environment();
+  namespacet ns{symbol_tablet{}};
+  const auto s32_type = signedbv_typet{32};
+  const auto three = from_integer(3, s32_type);
+  const auto five = from_integer(5, s32_type);
+  const auto three_plus_five = plus_exprt{three, five};
+
+  auto eval_result = environment.eval(three_plus_five, ns);
+  REQUIRE(eval_result != nullptr);
+  REQUIRE(!eval_result->is_top());
+  REQUIRE(!eval_result->is_bottom());
+
+  const auto eval_result_as_value_set =
+    std::dynamic_pointer_cast<const value_set_abstract_valuet>(
+      eval_result->unwrap_context());
+  REQUIRE(eval_result_as_value_set != nullptr);
+  const auto eight = from_integer(8, s32_type);
+  REQUIRE(eval_result_as_value_set->get_values().size() == 1);
+  REQUIRE_THAT(eval_result_as_value_set->get_values(), ContainsAllOf{eight});
+}
+
+TEST_CASE(
+  "Eval on a multiply expression on symbols gives us the results of that "
+  "multiplication",
+  VALUE_SET_TEST_TAGS)
+{
+  auto environment = get_value_set_abstract_environment();
+  symbol_tablet symbol_table;
+
+  const auto s32_type = signedbv_typet{32};
+
+  symbolt a_symbol{};
+  a_symbol.name = a_symbol.pretty_name = a_symbol.base_name = "a";
+  a_symbol.is_lvalue = true;
+  a_symbol.type = s32_type;
+  symbol_table.add(a_symbol);
+
+  symbolt b_symbol{};
+  b_symbol.name = b_symbol.pretty_name = b_symbol.base_name = "b";
+  b_symbol.is_lvalue = true;
+  b_symbol.type = s32_type;
+  symbol_table.add(b_symbol);
+  symbol_table.add(b_symbol);
+
+  const namespacet ns{symbol_table};
+
+  const auto three = from_integer(3, s32_type);
+  const auto four = from_integer(4, s32_type);
+  const auto five = from_integer(5, s32_type);
+  const auto six = from_integer(6, s32_type);
+
+  const auto three_or_five = std::make_shared<const value_set_abstract_valuet>(
+    s32_type, value_set_abstract_valuet::valuest{three, five});
+  environment.assign(a_symbol.symbol_expr(), three_or_five, ns);
+
+  const auto four_or_six = std::make_shared<const value_set_abstract_valuet>(
+    s32_type, value_set_abstract_valuet::valuest{four, six});
+  environment.assign(b_symbol.symbol_expr(), four_or_six, ns);
+
+  const auto a_times_b =
+    mult_exprt{a_symbol.symbol_expr(), b_symbol.symbol_expr()};
+
+  const auto eval_result = environment.eval(a_times_b, ns);
+  REQUIRE(eval_result != nullptr);
+  REQUIRE(!eval_result->is_top());
+  REQUIRE(!eval_result->is_bottom());
+
+  const auto eval_result_as_value_set =
+    std::dynamic_pointer_cast<const value_set_abstract_valuet>(
+      eval_result->unwrap_context());
+  REQUIRE(eval_result_as_value_set != nullptr);
+  REQUIRE(eval_result_as_value_set->get_values().size() == 4);
+
+  const auto twelve = from_integer(12, s32_type);
+  const auto eighteen = from_integer(18, s32_type);
+  const auto twenty = from_integer(20, s32_type);
+  const auto twentyfour = from_integer(30, s32_type);
+  REQUIRE_THAT(
+    eval_result_as_value_set->get_values(),
+    ContainsAllOf(twelve, eighteen, twenty, twentyfour));
+}