Create harness to initialize memory from snapshot #4150

danpoe · 2019-02-10T20:22:00Z

This PR replaces PR #3755.

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).
n/a 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-02-11T08:12:50Z

src/goto-programs/goto_program.h

@@ -529,6 +529,23 @@ class goto_programt
    return t;
  }

+  optionalt<const_targett> get_target(const unsigned location_number) const


We have elsewhere erased the const qualifier from POD parameters, so it's probably better to drop it here.

IMHO this is good to keep on definitions, as it still meaningful "I'm not going to modify this value in this body". I'd only remove it from declarations, where it is meaningless.

tautschnig · 2019-02-11T08:15:26Z

src/goto-programs/goto_program.h

+    }
+
+    return std::next(
+      instructions.begin(), location_number - start_location_number);


I'm not sure we provide a guarantee that location numbers are contiguous. You might want to add a CHECK_RETURN to make sure what you are about to return has the expected location_number.

Check added.

tautschnig · 2019-02-11T08:21:09Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      throw invalid_command_line_argument_exceptiont(
+        "no instruction with location number " +
+        std::to_string(*location_number) + " in function " + function);
+    }


I think this check should be done as part of the options parsing very early on.

At present goto-harness loads the goto binary only after the options checking. We could move the loading of the goto binary to before the options checking, and then give a reference to the goto model to the constructor of every harness generator. Then we could move some of the checks out of generate() and into handle_option(). Does that sound reasonable?

Although that's a non-trivial change it would seem like a good idea to me. The earlier we know about a problem the better?

tautschnig · 2019-02-11T08:22:59Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+    split_string(initial_location, ':', start, true);
+
+    if(
+      start.size() == 0 || (start.size() >= 1 && start.front().empty()) ||


Use start.empy() instead of size() == 0

start.size() >= 1 is trivially true here

tautschnig · 2019-02-11T08:28:19Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  if(function.empty())
+  {
+    INVARIANT(
+      location_number.has_value(),


Should be negated (if no function is provided, then location_number must not be set.

tautschnig · 2019-02-11T08:44:06Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+  code_function_callt function_call(
+    called_function_symbol.symbol_expr(), arguments);
+  code.add(function_call);


Use std::move or inline the constructor call.

tautschnig · 2019-02-11T08:44:40Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  }
+
+  code_function_callt function_call(
+    called_function_symbol.symbol_expr(), arguments);


std::move(arguments)

tautschnig · 2019-02-11T08:45:57Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  CHECK_RETURN(r.second);
+
+  auto f_it = goto_model.goto_functions.function_map.insert(
+    std::make_pair(function.name, goto_functiont()));


I'd use emplace(function.name, goto_functiont())

tautschnig · 2019-02-11T08:47:58Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+        "` already in "
+        "the symbol table",
+      "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT);
+  }


I'd do that check as early as possible, no need to waste time doing add_init_section or the likes.

tautschnig · 2019-02-11T08:48:45Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+  code_blockt harness_function_body;
+
+  add_assignments_to_globals(snapshot, harness_function_body);


Make that function return a code_blockt rather than passing it by reference.

kroening · 2019-02-11T10:12:00Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+      goto_program.insert_before(std::prev(goto_program.instructions.end()));
+
+    init_it->make_assignment(code_assignt(var, false_exprt()));
+  }


Now that since #4001 you can say
goto_program.insert_before(..., goto_programt::make_assignment(...));
The instructiont::make_assignment(...) will eventually go away.

NlightNFotis

LGTM. Just one comment.

NlightNFotis · 2019-02-11T10:25:42Z

src/goto-harness/memory_snapshot_harness_generator.h

+
+  void insert_function(goto_modelt &goto_model, const symbolt &function) const;
+
+  std::string memory_snapshot;


Nit: I would change this name to memory_snapshot_file or something else, because its naming is slightly confusing: When I first saw it in generate(), I thought it had a complex data structure behind it, but it appears it's just a string indicating the file to read the json_symbol_table from.

hannes-steffenhagen-diffblue

Mostly nitpicks / questions, otherwise looks good to me

hannes-steffenhagen-diffblue · 2019-02-11T10:42:42Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  const symbol_exprt &var = symbol.symbol_expr();
+
+  // initialise var in __CPROVER_initialize if it is present
+  const auto f_it =


Can you give this is a more meaningful name, such as cprover_init_it or something along those lines?

Also, can you elaborate why you need to change __CPROVER_initialize to make this work? (ideally as a comment in the code as well)

hannes-steffenhagen-diffblue · 2019-02-11T10:44:11Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+  goto_programt &goto_program = goto_function.body;
+
+  const symbolt &symbol = get_fresh_aux_symbol(


Can you give symbol a more meaningful name, such as func_init_done or func_init_done_symbol if you want to keep its symbol-ness part of the name?

Also, can you add a comment here about what func_init_done means?

hannes-steffenhagen-diffblue · 2019-02-11T10:45:50Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+    function_symbol.mode,
+    symbol_table);
+
+  const symbol_exprt &var = symbol.symbol_expr();


Can you give this a more meaningful name, like func_init_done_variable?

Better names added.

hannes-steffenhagen-diffblue · 2019-02-11T10:48:29Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  code.add(function_call);
+}
+
+void memory_snapshot_harness_generatort::insert_function(


If this is supposed to insert the harness function specifically rather than just any function, can you rename this to insert_harness_function_into_goto_model or something like this? (I know these names are getting rather lengthy, this is just an example)

hannes-steffenhagen-diffblue · 2019-02-11T10:55:29Z

src/goto-harness/memory_snapshot_harness_generator.h

+  "--memory-snapshot <file>      initialise memory from JSON memory snapshot\n"\
+  "--initial-location <func[:<n>]>\n"                                          \
+  "                              use given function and location number as "   \
+  "entry\n                              point\n"                               \


⛏️ Looks like the formatting here got messed up a bit

Actually looks ok on the command line.

hannes-steffenhagen-diffblue · 2019-02-11T11:00:00Z

regression/goto-harness/chain.sh

@@ -23,5 +23,7 @@ if [ -e "${name}-mod.gb" ] ; then
  rm -f "${name}-mod.gb"
 fi

-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
+$cbmc --show-goto-functions "${name}.gb"


Do you need this information for the tests or is this just intended to make debugging a bit easier?

Not need, so I guess debugging.

allredj

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

hannes-steffenhagen-diffblue · 2019-03-01T12:20:52Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+
+  // initialise var in __CPROVER_initialize if it is present
+  const auto f_it =
+    goto_functions.function_map.find(CPROVER_PREFIX "initialize");


I'm not sure why you need this at all, shouldn't the generated harness function be enough for whatever you were going to to with initialize?

This may need modification after diffblue#4150 is merged.

tautschnig · 2019-03-14T21:48:18Z

@danpoe @xbauch This needs a rebase.

This adds const iterators to iterate over the internal_symbols map of the symbol table. So far, only non-const iterators existed.

This adds several regression tests for the feature of creating a harness that initialises the memory from a memory snapshot.

Adds two invocations of cbmc --show-goto-functions to regression/goto-harness/chain.sh to output the goto program before and after the harness generation.

This adds a harness generator to goto-harness that takes a goto program and a memory snapshot in JSON format (via the option --memory-snapshot), and then builds a harness that initialises the global variables from the snapshot. In addition the harness generator provides the option --initial-location to specify the starting point of the execution. The harness thus behaves as if the original program would start execution at the given program location.

In case we get an array (and not an object) we first find the right object and then pass it to be converted.

danpoe requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners February 10, 2019 20:22

danpoe mentioned this pull request Feb 10, 2019

Load memory snapshot into cbmc #3755

Closed

6 tasks

tautschnig approved these changes Feb 11, 2019

View reviewed changes

tautschnig assigned danpoe Feb 11, 2019

kroening reviewed Feb 11, 2019

View reviewed changes

NlightNFotis approved these changes Feb 11, 2019

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Feb 11, 2019

View reviewed changes

danpoe force-pushed the feature/memory-snapshot-harness branch 3 times, most recently from ad416e2 to 6869881 Compare February 11, 2019 16:06

allredj reviewed Feb 11, 2019

View reviewed changes

hannes-steffenhagen-diffblue reviewed Mar 1, 2019

View reviewed changes

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 8, 2019

Squashed commits from prerequisite PR diffblue#4150 - Do not review

d5c94a8

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 11, 2019

Add documentation to memory snapshot harness

175f325

This may need modification after diffblue#4150 is merged.

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 11, 2019

Add documentation to memory snapshot harness

d2cec20

This may need modification after diffblue#4150 is merged.

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 13, 2019

Add documentation to memory snapshot harness

1c09ffd

This may need modification after diffblue#4150 is merged.

xbauch mentioned this pull request Mar 13, 2019

Memory snapshot harness havoc #4351

Merged

7 tasks

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 13, 2019

Add documentation to memory snapshot harness

df38cc3

This may need modification after diffblue#4150 is merged.

tautschnig assigned xbauch Mar 14, 2019

tautschnig added the Needs rebase label Mar 14, 2019

danpoe added 2 commits March 15, 2019 10:49

Add const iterator to symbol table

991061b

This adds const iterators to iterate over the internal_symbols map of the symbol table. So far, only non-const iterators existed.

Regression tests for the memory snapshot harness generator

36983c1

This adds several regression tests for the feature of creating a harness that initialises the memory from a memory snapshot.

danpoe and others added 4 commits March 15, 2019 10:49

Output goto functions in goto-harness regression tests

20ee8df

Adds two invocations of cbmc --show-goto-functions to regression/goto-harness/chain.sh to output the goto program before and after the harness generation.

Add method to get a const_targett from a location number

b5657a8

Search the JSON for symbol table

9c9da96

In case we get an array (and not an object) we first find the right object and then pass it to be converted.

danpoe force-pushed the feature/memory-snapshot-harness branch 2 times, most recently from 1a3d4f4 to 7bc616a Compare March 15, 2019 13:53

Fix based on comments

7bc616a

danpoe removed the Needs rebase label Mar 15, 2019

danpoe merged commit f9f0733 into diffblue:develop Mar 15, 2019

danpoe deleted the feature/memory-snapshot-harness branch June 2, 2020 17:19


		code_blockt harness_function_body;

		add_assignments_to_globals(snapshot, harness_function_body);


		void insert_function(goto_modelt &goto_model, const symbolt &function) const;

		std::string memory_snapshot;


		goto_programt &goto_program = goto_function.body;

		const symbolt &symbol = get_fresh_aux_symbol(

Create harness to initialize memory from snapshot #4150

Create harness to initialize memory from snapshot #4150

Uh oh!

Conversation

danpoe commented Feb 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

NlightNFotis 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!

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

danpoe commented Feb 10, 2019 •

edited

Loading