Memory snapshot harness lines #4411

xbauch · 2019-03-20T10:15:50Z

Before the user had to run the CBMC first to find out the location where they wanted to start their snaphot. This PR adds to option to specify the code line.

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.

tautschnig · 2019-03-22T08:55:37Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      const auto &goto_function = entry.second;
+
+      if(!goto_function.body_available())
+        continue;


That's actually unnecessary, the std::find_if will do the right thing either way.

I don't understand. I call find_if on the instructions inside goto_function.body. If the body is not body_available is it still safe to do?

It is safe (body_available() just tests emptiness), but arguably that could change at some point in the future.

Ok, I removed it but left a comment.

tautschnig · 2019-03-22T08:56:14Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+      if(it != goto_program.instructions.end())
+      {
+        entry_function_name = entry.first; //TODO - move elsewhere


I don't think I understand this TODO.

Sorry, should have been removed before.

tautschnig · 2019-03-22T08:57:27Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+        goto_program.instructions.end(),
+        [this](const goto_programt::instructiont &instruction) {
+          return safe_string2unsigned(id2string(
+                   instruction.source_location.get_line())) >= *line_number;


But then the same line number can occur in multiple files?

Well find_if should return the first location with "high enough" line number. Is this still relevant if we insist on having the user specify the file as well?

If the user can/has to specify the file then that's sorted, thanks!

tautschnig · 2019-03-22T08:58:43Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      const auto &goto_program = goto_function->second.body;
+      if(!location_number.has_value())
+        return goto_program.instructions.begin();
+      if(goto_program.instructions.size() > *location_number)


Why is this condition necessary?

Because I'm advancing the iterator by *location_number position and I don't want to get past the end().

Ah, sorry, I missed that. But also this isn't how the location_number member of instructions works: these location numbers are guaranteed to be unique across all goto functions, and monotonically increasing in a single function. Therefore a location number could well be larger than the size of a single function. At the same time, there could be gaps, so locations in a function could legitimately be numbered "7, 10, 15" instead of "1, 2, 3."

I give up. What about find_if to get the right instruction? That should be safe right?

Yes, I'm afraid you will have to do some form of search (technically binary search would be faster, but quite likely no one will notice the cost of linear search here).

But would binary search on a std::list really be faster? I thought that random access there is linear in the distance of the jump.

That's a question of how expensive the comparison operation is. Most likely you are right in that binary search would not add any value (or may indeed be more expensive).

tautschnig · 2019-03-22T08:59:57Z

src/goto-harness/memory_snapshot_harness_generator.h

@@ -34,6 +35,7 @@ Author: Daniel Poetzl
  "--initial-location <func[:<n>]>\n"                                          \
  "                              use given function and location number as "   \
  "entry\n                              point\n"                               \
+  "--initial-line <n>            use given line as entry point\n"              \


Can we actually use file:line? I think the line number alone is too ambiguous. You might actually end up picking an instruction from some system header file!

That's a very good idea. Added in the last commit. Which will also be squashed.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1f0d7e9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105415411
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e2598d2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105422508
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 948b575).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105424064
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

martin-cs

Seems like a reasonable feature. Will approve once @tautschnig 's comments have been resolved.

src/goto-programs/goto_program.h

hannes-steffenhagen-diffblue

Looks good to me overall, not even really nitpicks just suggestion/questions

hannes-steffenhagen-diffblue · 2019-03-26T16:53:04Z

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -61,6 +63,24 @@ void memory_snapshot_harness_generatort::handle_option(
  {
    variables_to_havoc.insert(values.begin(), values.end());
  }
+  else if(option == "initial-file-line")


🚲 🏚️ maybe --initial-source-location?

hannes-steffenhagen-diffblue · 2019-03-26T16:54:51Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      require_exactly_one_value(option, values);
+
+    std::vector<std::string> start;
+    split_string(initial_file_line, ':', start, true);


split_string has a special cased version for working with 2 values, maybe worth considering?

hannes-steffenhagen-diffblue · 2019-03-26T16:58:31Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+        "invalid initial location specification", "--initial-file-line");
+    }
+
+    initial_file_name = start.front();


💡 might be worth wrapping these two in a struct to keep (and make obvious) the invariant that either both or neither of these are set

@hannes-steffenhagen-diffblue This required a little bigger change: the last 7 commits. Please have a look if its still acceptable.

hannes-steffenhagen-diffblue · 2019-03-27T15:00:27Z

src/goto-harness/memory_snapshot_harness_generator.h

+    irep_idt function_name;
+    optionalt<goto_programt::const_targett> start_instruction;
+
+    void initialize_via_goto(


I'd be more comfortable if these were builder/constructor functions, i.e. entry_locationt make_from_goto_location(...);, entry_locationt make_from_source_location

Good idea: done.

hannes-steffenhagen-diffblue · 2019-03-27T15:02:26Z

src/goto-harness/memory_snapshot_harness_generator.h

+    irep_idt function_name;
+    optionalt<unsigned> location_number;
+
+    entry_goto_locationt(const std::string &cmdl_option);


explicit - also, I'm personally not a huge fan of "do work" constructors, i.e. this one parses from string, I'd prefer if it was a function that said it did that in its name

Done + constructors are now trivial.

hannes-steffenhagen-diffblue · 2019-03-27T15:02:45Z

src/goto-harness/memory_snapshot_harness_generator.h

+    irep_idt file_name;
+    unsigned line_number;
+
+    entry_source_locationt(const std::string &cmdl_option);


also explicit and the above comment

hannes-steffenhagen-diffblue · 2019-03-27T15:03:57Z

src/goto-harness/memory_snapshot_harness_generator.h

+      const entry_source_locationt &entry_source_location,
+      const goto_functionst &goto_functions);
+
+    bool valid() const


Ideally it shouldn't be possible to construct this in an invalid state, if it can be avoided

hannes-steffenhagen-diffblue · 2019-03-27T15:06:38Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+  if(start.size() == 2)
+  {
+    location_number = optionalt<unsigned>(safe_string2unsigned(start.back()));


this should be string2optional_unsigned instead, and you should check the result... if this function returns nullopt it means its argument wasn't a valid integer, which is something you don't want to silently ignore

(with safe_string2unsigned you're basically asserting that this conversion will always succeed which is not correct for user supplied strings)

hannes-steffenhagen-diffblue · 2019-03-27T15:06:46Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  }
+
+  file_name = initial_file_string;
+  line_number = safe_string2unsigned(initial_line_string);


same as above

hannes-steffenhagen-diffblue · 2019-03-27T15:09:09Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      "choose either source or goto location to specify the entry point",
+      "--initial-source/goto-location");
+  }
+


I think this needs a check that only one of goto location and source location is set?

It's there somewhere (line 69).

To test the new entry point selection and reflect the renaming of the option.

And unify the option names.

Two kinds of user specification: either via goto location or via source line. We wrap these in entry_goto/source_locationt and build the production of the final entry_locationt.

We only store the strings here.

Most of the sanity checks are in the wrappers and the `get_target` function is now redundant.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 0249ba0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106287968
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.

tautschnig assigned xbauch Mar 22, 2019

xbauch marked this pull request as ready for review March 22, 2019 08:25

xbauch requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners March 22, 2019 08:25

xbauch force-pushed the feature/memory-snapshot-harness-lines branch from c09dc87 to b6788e3 Compare March 22, 2019 08:31

tautschnig reviewed Mar 22, 2019

View reviewed changes

xbauch force-pushed the feature/memory-snapshot-harness-lines branch from 979cd9e to e2598d2 Compare March 22, 2019 10:10

allredj reviewed Mar 22, 2019

View reviewed changes

martin-cs reviewed Mar 22, 2019

View reviewed changes

src/goto-programs/goto_program.h Show resolved Hide resolved

tautschnig approved these changes Mar 23, 2019

View reviewed changes

tautschnig assigned chrisr-diffblue and hannes-steffenhagen-diffblue Mar 23, 2019

hannes-steffenhagen-diffblue approved these changes Mar 27, 2019

View reviewed changes

xbauch added the do not merge label Mar 27, 2019

hannes-steffenhagen-diffblue reviewed Mar 27, 2019

View reviewed changes

Petr Bauch added 4 commits March 28, 2019 16:11

Add and modify regression tests

7d95a71

To test the new entry point selection and reflect the renaming of the option.

Add source location option

51e24a2

And unify the option names.

Introduce wrappers for entry location

1d2e01c

Two kinds of user specification: either via goto location or via source line. We wrap these in entry_goto/source_locationt and build the production of the final entry_locationt.

Simply handling the options

6643eb4

We only store the strings here.

xbauch force-pushed the feature/memory-snapshot-harness-lines branch from e3e90ec to 217ee86 Compare March 28, 2019 16:41

xbauch removed the do not merge label Mar 28, 2019

xbauch force-pushed the feature/memory-snapshot-harness-lines branch from 217ee86 to 8fc213e Compare March 28, 2019 21:15

Reflect the existence of wrappers

0249ba0

Most of the sanity checks are in the wrappers and the `get_target` function is now redundant.

xbauch force-pushed the feature/memory-snapshot-harness-lines branch from 8fc213e to 0249ba0 Compare March 29, 2019 08:07

xbauch merged commit 535bde0 into diffblue:develop Mar 29, 2019

xbauch deleted the feature/memory-snapshot-harness-lines branch March 29, 2019 09:06

allredj reviewed Mar 29, 2019

View reviewed changes

Memory snapshot harness lines #4411

Memory snapshot harness lines #4411

Uh oh!

Conversation

xbauch commented Mar 20, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch Mar 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch Mar 22, 2019 •

edited

Loading