Merge pull request #5095 from xbauch/fix/snapshot-harness-order

Fix the ordering of variable initialisation in goto-harness

Author: petr-bauch

regression/snapshot-harness/dynamic-array-int-ordering/main.c

@@ -0,0 +1,64 @@
+#include <assert.h>
+#include <malloc.h>
+
+int a;
+int *a1;
+int *iterator1;
+int *a2;
+int *a3;
+int *iterator2;
+int *a4;
+int *a5;
+int *iterator3;
+int *a6;
+int *a7;
+int *array2;
+int *a8;
+
+void initialize()
+{
+  array2 = (int *)malloc(sizeof(int) * 10);
+  array2[0] = 1;
+  array2[1] = 2;
+  array2[2] = 3;
+  array2[3] = 4;
+  array2[4] = 5;
+  array2[5] = 6;
+  array2[6] = 7;
+  array2[7] = 8;
+  array2[8] = 9;
+  array2[9] = 10;
+  iterator1 = (int *)array2;
+  iterator2 = &array2[1];
+  iterator3 = array2 + 1;
+  a1 = &a;
+  a2 = a1;
+  a3 = a2;
+  a4 = a3;
+  a5 = a4;
+  a6 = a5;
+  a7 = a6;
+  a8 = a7;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == iterator3);
+  assert(iterator2 == &array2[1]);
+  assert(*iterator3 == array2[1]);
+  assert(*iterator3 == 2);
+  iterator3 = &array2[9];
+  iterator3++;
+  assert(*iterator3 == 0);
+
+  return 0;
+}

regression/snapshot-harness/dynamic-array-int-ordering/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == iterator3: SUCCESS
+\[main.assertion.4\] line [0-9]+ assertion iterator2 == \&array2\[1\]: SUCCESS
+\[main.assertion.5\] line [0-9]+ assertion \*iterator3 == array2\[1\]: SUCCESS
+\[main.assertion.6\] line [0-9]+ assertion \*iterator3 == 2: SUCCESS
+\[main.pointer_dereference.27\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator3: FAILURE
+\[main.assertion.7\] line [0-9]+ assertion \*iterator3 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/dynamic-array-int/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
+first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -209,47 +209,38 @@ size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
     return pointer_depth(t.subtype()) + 1;
 }
 
-bool memory_snapshot_harness_generatort::refers_to(
-  const exprt &expr,
-  const irep_idt &name) const
-{
-  if(expr.id() == ID_symbol)
-    return to_symbol_expr(expr).get_identifier() == name;
-  return std::any_of(
-    expr.operands().begin(),
-    expr.operands().end(),
-    [this, name](const exprt &subexpr) { return refers_to(subexpr, name); });
-}
-
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   const symbol_tablet &snapshot,
   goto_modelt &goto_model) const
 {
   recursive_initializationt recursive_initialization{
     recursive_initialization_config, goto_model};
 
-  using snapshot_pairt = std::pair<irep_idt, symbolt>;
-  std::vector<snapshot_pairt> ordered_snapshot_symbols;
-  for(auto pair : snapshot)
-  {
-    const auto name = id2string(pair.first);
-    if(!has_prefix(name, CPROVER_PREFIX))
-      ordered_snapshot_symbols.push_back(pair);
-  }
-
+  std::vector<std::pair<irep_idt, symbolt>> ordered_snapshot_symbols;
   // sort the snapshot symbols so that the non-pointer symbols are first, then
   // pointers, then pointers-to-pointers, etc. so that we don't assign
   // uninitialized values
-  std::stable_sort(
-    ordered_snapshot_symbols.begin(),
-    ordered_snapshot_symbols.end(),
-    [this](const snapshot_pairt &left, const snapshot_pairt &right) {
-      if(refers_to(right.second.value, left.first))
-        return true;
-      else
-        return pointer_depth(left.second.symbol_expr().type()) <
-               pointer_depth(right.second.symbol_expr().type());
-    });
+  {
+    std::vector<std::pair<irep_idt, symbolt>> selected_snapshot_symbols;
+    using relationt = typename preordert<irep_idt>::relationt;
+    relationt reference_relation;
+
+    for(const auto &snapshot_pair : snapshot)
+    {
+      const auto name = id2string(snapshot_pair.first);
+      if(name.find(CPROVER_PREFIX) != 0)
+      {
+        collect_references(
+          snapshot_pair.second.value,
+          [&reference_relation, &snapshot_pair](const irep_idt &id) {
+            reference_relation.insert(std::make_pair(snapshot_pair.first, id));
+          });
+        selected_snapshot_symbols.push_back(snapshot_pair);
+      }
+    }
+    preordert<irep_idt> reference_order{reference_relation};
+    reference_order.sort(selected_snapshot_symbols, ordered_snapshot_symbols);
+  }
 
   code_blockt code{};
 

src/goto-harness/memory_snapshot_harness_generator.h

@@ -275,11 +275,95 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   /// \return pointer depth of type \p t
   size_t pointer_depth(const typet &t) const;
 
-  /// Recursively test pointer reference
-  /// \param expr: expression to be tested
-  /// \param name: name to be located
-  /// \return true if \p expr refers to an object named \p name
-  bool refers_to(const exprt &expr, const irep_idt &name) const;
+  template <typename Adder>
+  void collect_references(const exprt &expr, Adder &&add_reference) const
+  {
+    if(expr.id() == ID_symbol)
+      add_reference(to_symbol_expr(expr).get_identifier());
+    for(const auto &operand : expr.operands())
+    {
+      collect_references(operand, add_reference);
+    }
+  }
+
+  /// Simple structure for linearising posets. Should be constructed with a map
+  /// assigning a key to a set of keys that precede it.
+  template <typename Key>
+  struct preordert
+  {
+  public:
+    using relationt = std::multimap<Key, Key>;
+    using keyst = std::set<Key>;
+
+    explicit preordert(const relationt &preorder_relation)
+      : preorder_relation(preorder_relation)
+    {
+    }
+
+    template <typename T>
+    void sort(
+      const std::vector<std::pair<Key, T>> &input,
+      std::vector<std::pair<Key, T>> &output)
+    {
+      std::unordered_map<Key, T> searchable_input;
+      using valuet = std::pair<Key, T>;
+
+      for(const auto &item : input)
+      {
+        searchable_input[item.first] = item.second;
+      }
+      auto associate_key_with_t =
+        [&searchable_input](const Key &key) -> optionalt<valuet> {
+        if(searchable_input.count(key) != 0)
+          return valuet(key, searchable_input[key]);
+        else
+          return {};
+      };
+      auto push_to_output = [&output](const valuet &value) {
+        output.push_back(value);
+      };
+      for(const auto &item : input)
+      {
+        dfs(item, associate_key_with_t, push_to_output);
+      }
+    }
+
+  private:
+    const relationt &preorder_relation;
+
+    keyst seen;
+    keyst inserted;
+
+    template <typename Value, typename Map, typename Handler>
+    void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
+    {
+      PRECONDITION(seen.empty() && inserted.empty());
+      dfs_inner(node, key_to_t, handle);
+      seen.clear();
+      inserted.clear();
+    }
+
+    template <typename Value, typename Map, typename Handler>
+    void dfs_inner(Value &&node, Map &&key_to_t, Handler &&handle)
+    {
+      const Key &key = node.first;
+      if(seen.count(key) == 0)
+      {
+        seen.insert(key);
+        auto key_range = preorder_relation.equal_range(key);
+        for(auto it = key_range.first; it != key_range.second; ++it)
+        {
+          auto maybe_value = key_to_t(it->second);
+          if(maybe_value.has_value())
+            dfs_inner(*maybe_value, key_to_t, handle);
+        }
+      }
+      if(inserted.count(key) != 0)
+        return;
+      handle(node);
+      inserted.insert(key);
+    }
+  };
 
   /// data to store the command-line options
   std::string memory_snapshot_file;