VSD: Simplifying abstract_objectt::write, collapsing inheritance hierarchy

scripts/expected_doxygen_warnings.txt

@@ -1,16 +1,16 @@
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:232: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:246: warning: no matching class member found for 
   template
   satcheck_glucose_baset< Glucose::Solver >::~satcheck_glucose_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:238: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:252: warning: no matching class member found for 
   template
   satcheck_glucose_baset< Glucose::SimpSolver >::~satcheck_glucose_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:312: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:313: warning: no matching class member found for 
   template
   satcheck_minisat2_baset< Minisat::Solver >::~satcheck_minisat2_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:318: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:319: warning: no matching class member found for 
   template
   satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset()
 
@@ -87,16 +87,16 @@ warning: Included by graph for 'arith_tools.h' not generated, too many nodes (18
 warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'namespace.h' not generated, too many nodes (113), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'namespace.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (122), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/Makefile

@@ -34,31 +34,26 @@ SRC = ai.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
       variable-sensitivity/abstract_object.cpp \
-      variable-sensitivity/abstract_enviroment.cpp \
-      variable-sensitivity/abstract_value.cpp \
-      variable-sensitivity/array_abstract_object.cpp \
+      variable-sensitivity/abstract_environment.cpp \
+      variable-sensitivity/abstract_value_object.cpp \
       variable-sensitivity/constant_abstract_value.cpp \
       variable-sensitivity/constant_pointer_abstract_object.cpp \
       variable-sensitivity/context_abstract_object.cpp \
       variable-sensitivity/write_location_context.cpp \
       variable-sensitivity/pointer_abstract_object.cpp \
-      variable-sensitivity/struct_abstract_object.cpp \
       variable-sensitivity/variable_sensitivity_domain.cpp \
       variable-sensitivity/variable_sensitivity_object_factory.cpp \
       variable-sensitivity/full_struct_abstract_object.cpp \
-      variable-sensitivity/constant_array_abstract_object.cpp \
-      variable-sensitivity/union_abstract_object.cpp \
+      variable-sensitivity/full_array_abstract_object.cpp \
       variable-sensitivity/write_stack.cpp \
       variable-sensitivity/write_stack_entry.cpp \
       variable-sensitivity/data_dependency_context.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
       variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
       variable-sensitivity/interval_abstract_value.cpp \
-      variable-sensitivity/interval_array_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_value.cpp \
       variable-sensitivity/value_set_pointer_abstract_object.cpp \
-      variable-sensitivity/value_set_array_abstract_object.cpp \
       variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/variable_sensitivity_configuration.cpp \
       # Empty last line

src/analyses/variable-sensitivity/abstract_aggregate_object.h

@@ -0,0 +1,227 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity
+
+ Author: Jez Higgins, jez@jezuk.co.uk
+
+\*******************************************************************/
+
+/// \file
+/// Common behaviour for abstract objects modelling aggregate values -
+/// arrays, structs, etc.
+#ifndef CBMC_ABSTRACT_AGGREGATE_OBJECT_H
+#define CBMC_ABSTRACT_AGGREGATE_OBJECT_H
+
+#include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/abstract_object.h>
+#include <stack>
+
+class abstract_aggregate_tag
+{
+};
+
+template <class aggregate_typet, class aggregate_traitst>
+class abstract_aggregate_objectt : public abstract_objectt,
+                                   public abstract_aggregate_tag
+{
+public:
+  explicit abstract_aggregate_objectt(const typet &type)
+    : abstract_objectt(type)
+  {
+    PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
+  }
+
+  abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
+    : abstract_objectt(type, tp, bttm)
+  {
+    PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
+  }
+
+  abstract_aggregate_objectt(
+    const exprt &expr,
+    const abstract_environmentt &environment,
+    const namespacet &ns)
+    : abstract_objectt(expr, environment, ns)
+  {
+    PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
+  }
+
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override
+  {
+    if(expr.id() == aggregate_traitst::ACCESS_EXPR_ID())
+      return read_component(environment, expr, ns);
+
+    return abstract_objectt::expression_transform(
+      expr, operands, environment, ns);
+  }
+
+  abstract_object_pointert write(
+    abstract_environmentt &environment,
+    const namespacet &ns,
+    const std::stack<exprt> &stack,
+    const exprt &specifier,
+    const abstract_object_pointert &value,
+    bool merging_write) const override
+  {
+    return write_component(
+      environment, ns, stack, specifier, value, merging_write);
+  }
+
+  void get_statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns) const override
+  {
+    abstract_objectt::get_statistics(statistics, visited, env, ns);
+    aggregate_traitst::get_statistics(statistics, visited, env, ns);
+    this->statistics(statistics, visited, env, ns);
+  }
+
+protected:
+  virtual abstract_object_pointert read_component(
+    const abstract_environmentt &environment,
+    const exprt &expr,
+    const namespacet &ns) const
+  {
+    // If we are bottom then so are the components
+    // otherwise the components could be anything
+    return environment.abstract_object_factory(
+      aggregate_traitst::read_type(expr.type(), type()),
+      ns,
+      !is_bottom(),
+      is_bottom());
+  }
+
+  virtual abstract_object_pointert write_component(
+    abstract_environmentt &environment,
+    const namespacet &ns,
+    const std::stack<exprt> &stack,
+    const exprt &expr,
+    const abstract_object_pointert &value,
+    bool merging_write) const
+  {
+    if(is_top() || is_bottom())
+    {
+      return shared_from_this();
+    }
+    else
+    {
+      return std::make_shared<aggregate_typet>(type(), true, false);
+    }
+  }
+
+  virtual void statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns) const = 0;
+
+  template <class keyt, typename hash>
+  static bool merge_shared_maps(
+    const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map1,
+    const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map2,
+    sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map)
+  {
+    bool modified = false;
+
+    typename sharing_mapt<keyt, abstract_object_pointert, false, hash>::
+      delta_viewt delta_view;
+    map1.get_delta_view(map2, delta_view, true);
+
+    for(auto &item : delta_view)
+    {
+      bool changes = false;
+      abstract_object_pointert v_new =
+        abstract_objectt::merge(item.m, item.get_other_map_value(), changes);
+      if(changes)
+      {
+        modified = true;
+        out_map.replace(item.k, v_new);
+      }
+    }
+
+    return modified;
+  }
+};
+
+struct array_aggregate_typet
+{
+  static const irep_idt TYPE_ID()
+  {
+    return ID_array;
+  }
+  static const irep_idt ACCESS_EXPR_ID()
+  {
+    return ID_index;
+  }
+  static typet read_type(const typet &, const typet &object_type)
+  {
+    array_typet array_type(to_array_type(object_type));
+    return array_type.subtype();
+  }
+
+  static void get_statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns)
+  {
+    ++statistics.number_of_arrays;
+  }
+};
+
+struct struct_aggregate_typet
+{
+  static const irep_idt &TYPE_ID()
+  {
+    return ID_struct;
+  }
+  static const irep_idt &ACCESS_EXPR_ID()
+  {
+    return ID_member;
+  }
+  static const typet &read_type(const typet &expr_type, const typet &)
+  {
+    return expr_type;
+  }
+
+  static void get_statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns)
+  {
+    ++statistics.number_of_structs;
+  }
+};
+
+struct union_aggregate_typet
+{
+  static const irep_idt TYPE_ID()
+  {
+    return ID_union;
+  }
+  static const irep_idt ACCESS_EXPR_ID()
+  {
+    return ID_member;
+  }
+  static typet read_type(const typet &, const typet &object_type)
+  {
+    return object_type;
+  }
+
+  static void get_statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns)
+  {
+  }
+};
+
+#endif //CBMC_ABSTRACT_AGGREGATE_OBJECT_H