WIP

src/analyses/Makefile

@@ -40,6 +40,7 @@ SRC = ai.cpp \
       variable-sensitivity/constant_pointer_abstract_object.cpp \
       variable-sensitivity/context_abstract_object.cpp \
       variable-sensitivity/data_dependency_context.cpp \
+      variable-sensitivity/example_abstract_value.cpp \
       variable-sensitivity/full_array_abstract_object.cpp \
       variable-sensitivity/full_struct_abstract_object.cpp \
       variable-sensitivity/interval_abstract_value.cpp \

src/analyses/variable-sensitivity/example_abstract_value.cpp

@@ -0,0 +1,117 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity example
+
+ Author: Martin Brain
+
+\*******************************************************************/
+
+#include "example_abstract_value.h"
+
+#include "abstract_environment.h"
+#include "abstract_object_statistics.h"
+
+example_abstract_valuet::example_abstract_valuet(const typet &t)
+  : abstract_value_objectt(t)
+{
+}
+
+example_abstract_valuet::example_abstract_valuet(
+  const typet &t,
+  bool tp,
+  bool bttm)
+  : abstract_value_objectt(t, tp, bttm)
+{
+}
+
+example_abstract_valuet::example_abstract_valuet(
+  const exprt &e,
+  const abstract_environmentt &environment,
+  const namespacet &ns)
+  : example_abstract_valuet(
+      represents_example(e)
+        ? make_example_expr(e)
+        : (e.operands().size() == 2 ? example_from_relation(e)
+                                    : constant_example_exprt(e.type())))
+{
+}
+
+exprt example_abstract_valuet::to_constant() const
+{
+}
+
+void example_abstract_valuet::set_top_internal()
+{
+}
+
+size_t example_abstract_valuet::internal_hash() const
+{
+  return std::hash<std::string>{}(example.pretty());
+}
+
+bool example_abstract_valuet::internal_equality(
+  const abstract_object_pointert &other) const
+{
+  auto cast_other =
+    std::dynamic_pointer_cast<const example_abstract_valuet>(other);
+  return cast_other && example == cast_other->example;
+}
+
+void example_abstract_valuet::output(
+  std::ostream &out,
+  const ai_baset &ai,
+  const namespacet &ns) const
+{
+  if(!is_top() && !is_bottom())
+  {
+  }
+  else
+  {
+    abstract_objectt::output(out, ai, ns);
+  }
+}
+
+abstract_object_pointert example_abstract_valuet::merge_with_value(
+  const abstract_value_pointert &other,
+  const widen_modet &widen_mode) const
+{
+}
+
+abstract_object_pointert example_abstract_valuet::meet_with_value(
+  const abstract_value_pointert &other) const
+{
+}
+
+index_range_implementation_ptrt
+example_abstract_valuet::index_range_implementation(const namespacet &ns) const
+{
+}
+
+value_range_implementation_ptrt
+example_abstract_valuet::value_range_implementation() const
+{
+}
+
+abstract_value_pointert
+example_abstract_valuet::constrain(const exprt &lower, const exprt &upper) const
+{
+}
+
+exprt example_abstract_valuet::to_predicate_internal(const exprt &name) const
+{
+}
+
+void example_abstract_valuet::get_statistics(
+  abstract_object_statisticst &statistics,
+  abstract_object_visitedt &visited,
+  const abstract_environmentt &env,
+  const namespacet &ns) const
+{
+  abstract_objectt::get_statistics(statistics, visited, env, ns);
+  ++statistics.number_of_example_abstract_objects;
+  if(example.is_single_value_example())
+  {
+    ++statistics.number_of_single_value_examples;
+  }
+  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
+}

src/analyses/variable-sensitivity/example_abstract_value.h

@@ -0,0 +1,102 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity example
+
+ Author: Martin Brain
+
+\*******************************************************************/
+
+/// \file
+/// An example abstract object representing a set of possible values.
+
+#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_EXAMPLE_ABSTRACT_VALUE_H
+#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_EXAMPLE_ABSTRACT_VALUE_H
+
+#include <analyses/variable-sensitivity/abstract_value_object.h>
+
+class example_abstract_valuet : public abstract_value_objectt
+{
+public:
+  // These are the methods all abstract objects must have
+  // Constructors
+  example_abstract_valuet(const typet &t, bool tp, bool bttm);
+  example_abstract_valuet(
+    const exprt &e,
+    const abstract_environmentt &environment,
+    const namespacet &ns);
+
+  // Manipulation
+  abstract_object_pointert expression_transform(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override;
+
+  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;
+
+  abstract_object_pointert
+  meet(const abstract_object_pointert &other) const override;
+
+  // Context information
+  abstract_object_pointert
+  write_location_context(const locationt &location) const override;
+  abstract_object_pointert
+  merge_location_context(const locationt &location) const override;
+  abstract_object_pointert unwrap_context() const override;
+
+  // Output
+  exprt to_constant() const override;
+  exprt to_predicate(const exprt &name) const;
+  void output(
+    std::ostream &out,
+    const class ai_baset &ai,
+    const class namespacet &ns) const override;
+
+  // Utility
+  bool verify() const override;
+  void get_statistics(
+    abstract_object_statisticst &statistics,
+    abstract_object_visitedt &visited,
+    const abstract_environmentt &env,
+    const namespacet &ns) const override;
+
+  abstract_object_pointert
+  visit_sub_elements(const abstract_object_visitort &visitor) const override;
+
+  size_t internal_hash() const override;
+  bool internal_equality(const abstract_object_pointert &other) const override;
+
+  // Destructor
+  ~example_abstract_valuet() override = default;
+
+  // Added by abstract value
+  constant_interval_exprt to_interval() const override;
+
+  abstract_value_pointert
+  constrain(const exprt &lower, const exprt &upper) const override;
+
+  index_range_implementation_ptrt
+  index_range_implementation(const namespacet &ns) const override;
+
+  value_range_implementation_ptrt value_range_implementation() const override;
+
+  // Unclear
+
+  template <typename... Args>
+  static std::shared_ptr<example_abstract_valuet> make_example(Args &&...args)
+  {
+    return std::make_shared<example_abstract_valuet>(
+      std::forward<Args>(args)...);
+  }
+
+protected:
+  CLONE
+};
+
+#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_EXAMPLE_ABSTRACT_VALUE_H

src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

@@ -21,6 +21,7 @@ enum ABSTRACT_OBJECT_TYPET
   TWO_VALUE,
   CONSTANT,
   INTERVAL,
+  EXAMPLE,
   ARRAY_SENSITIVE,
   ARRAY_INSENSITIVE,
   VALUE_SET_OF_POINTERS,

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -83,7 +83,7 @@
   "(vsd-liveness)"
 
 #define HELP_VSD                                                               \
-  " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}] \t "       \
+  " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}|{yexample}] \t "       \
   "value tracking\n"                                                           \
   " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t "                       \
   "struct field sensitive analysis\n"                                          \

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

@@ -13,7 +13,7 @@
 #include "constant_abstract_value.h"
 #include "constant_pointer_abstract_object.h"
 #include "data_dependency_context.h"
-#include "full_array_abstract_object.h"
+#include "example_abstract_value.h"
 #include "full_struct_abstract_object.h"
 #include "interval_abstract_value.h"
 #include "liveness_context.h"
@@ -167,6 +167,9 @@ variable_sensitivity_object_factoryt::get_abstract_object(
   case VALUE_SET:
     return initialize_abstract_object<value_set_abstract_objectt>(
       followed_type, top, bottom, e, environment, ns, configuration);
+  case EXAMPLE:
+    return initialize_abstract_object<example_abstract_valuet>(
+      followed_type, top, bottom, e, environment, ns, configuration);
 
   case ARRAY_INSENSITIVE:
     return initialize_abstract_object<two_value_array_abstract_objectt>(