Fix the ordering of variable initialisation in goto-harness #5095

xbauch · 2019-09-06T15:47:47Z

When using the memory-snapshot harness.

See #4978 for the problem.

Previously we were using the refers-to relation (a refers to b if the value a should be initialised with contains -- as a subexpression -- the symbol b) as if it was a linear ordering between the snapshot symbols. That is, we called std::stable_sort with this relation which is incorrect.

Now we select one linearisation of the partial order (given by refers-to) to be the initilisation ordering. Note that we ignore cycles, or more precisely in the presence of a cycle we start from the first visited symbol. This is correct, because for

struct A { A*next; };
A a1;
A a2;
a1.next = &a2;
a2.next = &a1;

the snapshot is

a1 = {.next=&a2}
a2 = {.next=&a1}

And the order is irrelevant. There is also a test-case which was failing before.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e034622).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/126261769

codecov-io · 2019-09-06T17:14:21Z

Codecov Report

Merging #5095 into develop will increase coverage by 0.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5095      +/-   ##
===========================================
+ Coverage    67.32%   67.33%   +0.01%     
===========================================
  Files         1155     1155              
  Lines        94643    94669      +26     
===========================================
+ Hits         63715    63744      +29     
+ Misses       30928    30925       -3

Flag	Coverage Δ
#cproversmt2	`42.64% <ø> (ø)`	⬆️
#regression	`63.81% <100%> (+0.01%)`	⬆️
#unit	`31.96% <ø> (ø)`	⬆️

Impacted Files	Coverage Δ
...c/goto-harness/memory_snapshot_harness_generator.h	`97.36% <100%> (+8.47%)`	⬆️
...goto-harness/memory_snapshot_harness_generator.cpp	`88.52% <100%> (-1.8%)`	⬇️
src/util/std_expr.h	`90.26% <0%> (+0.42%)`	⬆️
src/memory-analyzer/analyze_symbol.cpp	`90.93% <0%> (+1%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update cb20917...fbb40a0. Read the comment docs.

hannes-steffenhagen-diffblue · 2019-09-23T15:38:54Z

I think the first commit here should probably just have the entire description of this PR in it

NlightNFotis

LGTM

NlightNFotis · 2019-09-23T15:27:08Z

src/goto-harness/memory_snapshot_harness_generator.cpp

 }

-bool memory_snapshot_harness_generatort::refers_to(
+void memory_snapshot_harness_generatort::collect_references(


While I understand the need for the change for this, I feel slightly uneasy about the change to the return value (which provides some sort of feedback) to a void return value.

hannes-steffenhagen-diffblue

Looks mostly good to me, but I think the partial order sort class could use some cleanup.

hannes-steffenhagen-diffblue · 2019-09-25T09:18:25Z

src/goto-harness/memory_snapshot_harness_generator.h

+
+    void sort(
+      const std::vector<std::pair<Key, Value>> &input,
+      std::vector<std::pair<Key, Value>> &output)


Is there a reason this can't do an in-place sort?

hannes-steffenhagen-diffblue · 2019-09-25T10:06:27Z

src/goto-harness/memory_snapshot_harness_generator.h

+      const Key &key,
+      const std::map<Key, Value> &input,
+      std::vector<std::pair<Key, Value>> &output)
+    {


This seems to be basically doing a DFS. Might be worth just renaming the function to reflect that.

It could just have an API like

template<typename Value, typename GetNodeFromValue, typename GetNeighbors, typename OnFirstVisit> void depth_first_search(Value &&entry_node, GetKeyFromValue &&get_key_from_value, GetNeighbors &&getNeighbors, OnFirstVisit &&onFirstVisit);

and then you could use it above like

auto get_key_from_value = [](const std::pair<Key, Value>& kv_pair) { return kv_pair.first; }; auto get_neighbors = [&](const Key& key) { return por.at(key); } auto on_first_visit = [&](const Value& value) { output.push_back(value); } for(const auto &item : input) { dfs(item, get_key_from_value, get_neighbors, on_first_visit); }

(Note that I've changed Value to what was previously std::pair<Key,Value>, and instead there's a separate function for getting the key from the value).

❗ This is just a suggestion, I'm not saying you have to do it exactly this way obviously, but in any case I think it's worth emphasising that "recurse then insert" is basically doing DFS in the code, either by renaming the function or mentioning it in a comment

I went half-way. Given that the ordering is on keys only, the structure is only templated by Key and the sort, dfs functions and templated by some T.

hannes-steffenhagen-diffblue · 2019-09-25T10:07:47Z

src/goto-harness/memory_snapshot_harness_generator.h

+    const std::map<Key, std::set<Key>> &por;
+
+    std::set<Key> inserted;
+    std::set<Key> seen;


Note that these make sort a destructive method, i.e. an instance becomes unusable after sort is first called. Might be better to just pass these on as parameters, or loopify the recursion and just keep these as local variables

I wrapped the dfs in a cleaner function.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 373947e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129287253
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: a4df02c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129292085
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

by linearising the preorder induced by the symbol values referring to other symbols. Previously we were using the `refers-to` relation (`a` refers to `b` if the value `a` should be initialised with contains -- as a subexpression -- the symbol `b`) as if it was a linear ordering between the snapshot symbols. That is, we called std::stable_sort with this relation which is incorrect. Now we select one linearisation of the preorder (given by `refers-to`) to be the initilisation ordering. Note that we ignore cycles, or more precisely in the presence of a cycle we start from the first visited symbol.

when setting the order in which to initialise the variables from a snapshot. This test is designed to be failing slightly more often than the `dynamic-array-int` test by inserting extra variables in between the preordered ones. They cannot be named `array` because that irep-name already exists.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: fbb40a0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/134848870

xbauch requested a review from smowton September 6, 2019 15:48

allredj reviewed Sep 6, 2019

View reviewed changes

NlightNFotis approved these changes Sep 23, 2019

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Sep 25, 2019

View reviewed changes

xbauch force-pushed the fix/snapshot-harness-order branch 2 times, most recently from 373947e to a4df02c Compare September 26, 2019 13:07

xbauch marked this pull request as ready for review September 26, 2019 14:01

xbauch requested review from chrisr-diffblue, danpoe, martin-cs and peterschrammel as code owners September 26, 2019 14:01

allredj reviewed Sep 26, 2019

View reviewed changes

xbauch force-pushed the fix/snapshot-harness-order branch from a4df02c to 2a0eb7f Compare November 1, 2019 16:17

xbauch force-pushed the fix/snapshot-harness-order branch from 2a0eb7f to fbb40a0 Compare November 4, 2019 11:21

allredj reviewed Nov 4, 2019

View reviewed changes

xbauch merged commit 001b6f9 into diffblue:develop Nov 4, 2019

Fix the ordering of variable initialisation in goto-harness #5095

Fix the ordering of variable initialisation in goto-harness #5095

Uh oh!

Conversation

xbauch commented Sep 6, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Sep 6, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

hannes-steffenhagen-diffblue commented Sep 23, 2019

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Sep 23, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Sep 25, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Sep 25, 2019

Choose a reason for hiding this comment

Uh oh!

xbauch Sep 26, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Sep 25, 2019

Choose a reason for hiding this comment

Uh oh!

xbauch Sep 26, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

codecov-io commented Sep 6, 2019 •

edited

Loading