Goto instrument loop unwinding #241

danpoe · 2016-09-27T15:12:30Z

Loop unwinding with:

partial loops, assume, assert, rest loops
unwindsets

danpoe · 2016-09-28T18:53:11Z

The Linux builds now also work with a new travis.yml file that provides a more recent version of libstdc++.

kroening · 2016-10-30T14:22:09Z

May I ask for some reasonable squashing of commits, please?

danpoe · 2016-10-31T11:08:42Z

Ok, done.

tautschnig · 2016-11-10T13:50:54Z

src/util/string_utils.cpp

+
+  split_string(s, delim, result, strip);
+  if(result.size()!=2)
+    throw std::invalid_argument("number of parts != 2");


As in other places just strings are thrown (and then also caught) I would suggest to use
throw "split string did not generate exactly 2 parts";
(and drop #include <stdexcept>)

tautschnig · 2016-11-10T13:52:22Z

regression/goto-instrument-unwind/assert1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 10 --unwinding-assertions"


I was surprised to see the quotes, see below for a suggestion on how to get rid of them.

tautschnig · 2016-11-10T14:11:40Z

regression/goto-instrument-unwind/unwind-chain.sh

@@ -6,22 +6,18 @@ goto_instrument=$src/goto-instrument/goto-instrument
 cbmc=$src/cbmc/cbmc

 function usage() {
-  echo "Usage: chain unwind-num test_file.c"
+  echo "Usage: chain <options> <testfile>"


If the testfile were required to be the first (instead of the last) argument then the code could be simplified and all the quotes would become unnecessary. More below.

Doesn't test.pl always pass the testfile as the last argument?

So maybe test.pl should be tweaked to simplify such scripts? Else there could be a brief options parser in this code to extract the last argument from $@.

tautschnig · 2016-11-10T14:12:20Z

regression/goto-instrument-unwind/unwind-chain.sh

-  echo $unwind_num
-  echo $name
-else
+if [ $# -ne 2 ]; then


Use [ -z $# ] if moving the file argument into the first position and add || [ ! -s $1 ] to ensure it's a valid file(name).

tautschnig · 2016-11-10T14:12:54Z

regression/goto-instrument-unwind/unwind-chain.sh

 fi

+name=$(echo $2 | cut -d. -f1)


To address both the argument swapping and add support for path names containing "." use:

name=$(echo $1 | sed 's/\.[^\.]*$//') shift

tautschnig · 2016-11-10T14:27:38Z

src/goto-instrument/unwind.cpp

 {
-  std::vector<goto_programt::targett> exit_points;
-  unwind(goto_program, loop_head, loop_exit, k, exit_points);
+  assert(k>=0);


k is unsigned, this is trivially true.

tautschnig · 2016-11-10T14:28:05Z

src/goto-instrument/unwind.cpp

-  assert(k!=0);
-
-  iteration_points.resize(k);
+  assert(k>=0);


k is unsigned

tautschnig · 2016-11-10T14:28:47Z

src/goto-instrument/unwind.cpp

-  // not needed if there is an unconditional goto before loop_exit.
+  // rest program after unwound part
+  goto_programt rest_program;
+  assert(rest_program.instructions.empty());


That's a fresh goto_programt, should be trivially true?!

tautschnig · 2016-11-10T14:30:23Z

src/goto-instrument/unwind.cpp

+  }
+  else
+  {
+    assert(k==0);


If I read the code correctly, this is the else case of k!=0 - should be trivially true.

tautschnig · 2016-11-10T14:32:00Z

src/goto-programs/goto_program_template.h

+  {
+    return instructions.insert(target, instructiont());
+  }
+


Nit: just one blank line

tautschnig · 2016-11-25T23:14:08Z

danpoe commented on this pull request. > @@ -1324,6 +1360,10 @@ void goto_instrument_parse_optionst::help() "Semantic transformations:\n" " --nondet-volatile makes reads from volatile variables non-deterministic\n" " --unwind <n> unwinds the loops <n> times\n" + " --unwindset L:B,... unwind loop L with a bound of B\n" + " --partial-loops permit paths with partial loops\n" + " --unwinding-assertions generate unwinding assertions\n" + " --rest-loops add loop for remaining iterations after unwound part\n" How about "--continuation-loops"? It's not perfect either but at least gives some idea about what it does.

I do like this suggestion if it weren't for "continuation" to have a well-defined meaning in programming languages already. Maybe "--continue-as-loops" ? Best, Michael

danpoe · 2016-11-26T21:02:55Z

Ok, I think I've addressed everything.

tautschnig

I've added some nice-to-have notes.

tautschnig · 2016-11-30T23:22:49Z

src/util/string_utils.cpp

+
+\*******************************************************************/
+
+// unit tests


I would suggest to place this in the unit/ top-level folder.

Ok, I've added this to the unit tests folder.

tautschnig · 2016-11-30T23:25:46Z

src/goto-instrument/goto_instrument_parse_options.cpp

-      goto_functions.update();
-      goto_functions.compute_loop_numbers();
+        if(unwind)
+          k=stoi(cmdline.get_value("unwind"));


I'm a bit surprised this works without std::, but it has done before. Maybe use safe_string2int so that we can later put in std::stoi across the codebase?

I've changed this to safe_string2int().

tautschnig · 2016-11-30T23:26:33Z

.travis.yml

@@ -1,22 +1,43 @@
 language: cpp

-os:


Did you intentionally add .travis.yml changes to this pull request? (I am in favour of those changes, just asking.)

I'm using some new versions of methods of, e.g., std::set that were added in C++11. This didn't compile with the old travis file as the STL version it used for the Linux builds was too old.

Ok, thanks for clarifying!

tautschnig · 2016-12-01T16:57:18Z

Unless anyone else voices concerns, it should just be a rebase that's blocking a merge.

kroening · 2016-12-01T17:01:03Z

src/util/string_utils.cpp

+    return "";
+
+  // find last non-space char
+  long j; // need signed type here


should that be ssize_t?

kroening · 2016-12-01T17:01:27Z

src/util/string_utils.cpp

+  // find last non-space char
+  long j; // need signed type here
+  for(j=n-1; j>=0; j--)
+  {


Or use some reverse iterator?

I've used a reverse iterator for this now.

kroening · 2016-12-01T17:02:57Z

src/goto-instrument/goto_instrument_parse_options.cpp

+        {
+          std::string us;
+          std::string fn=cmdline.get_value("unwindset-file");
+          std::ifstream file(fn);


This unfortunately needs to include widen() on WIN32, or Unicode filenames won't work.

danpoe · 2016-12-02T12:13:10Z

This is now rebased and I've addressed the additional comments.

Fix issue #241 - Conversion from int

SEC-41 : Integration of the 'full-slicer' into the pipe-line (tools-chain).

…s-with-sharing-merge Fix reaching definitions with sharing merge

kroening self-assigned this Sep 27, 2016

kroening added the enhancement label Sep 27, 2016

danpoe force-pushed the goto-instrument-loop-unwinding branch from 5d3eea2 to 7612db8 Compare September 28, 2016 17:43

danpoe force-pushed the goto-instrument-loop-unwinding branch from 7612db8 to d948765 Compare October 31, 2016 10:54

tautschnig requested changes Nov 10, 2016

View reviewed changes

danpoe force-pushed the goto-instrument-loop-unwinding branch from d7b0f33 to 39dd631 Compare November 17, 2016 16:39

danpoe force-pushed the goto-instrument-loop-unwinding branch from dba29d6 to f13cff5 Compare November 26, 2016 20:42

tautschnig approved these changes Nov 30, 2016

View reviewed changes

danpoe force-pushed the goto-instrument-loop-unwinding branch from f13cff5 to c8c7c29 Compare December 1, 2016 15:31

kroening reviewed Dec 1, 2016

View reviewed changes

src/util/string_utils.cpp

return "";

// find last non-space char

long j; // need signed type here

Copy link

Member

kroening Dec 1, 2016

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should that be ssize_t?

kroening reviewed Dec 1, 2016

View reviewed changes

danpoe added 2 commits December 2, 2016 11:40

new travis file

c8fa5be

goto instrument loop unwinding with strategies

1157ad3

danpoe force-pushed the goto-instrument-loop-unwinding branch from c8c7c29 to 1157ad3 Compare December 2, 2016 12:11

kroening merged commit a9ba37f into diffblue:master Dec 6, 2016

danpoe deleted the goto-instrument-loop-unwinding branch January 17, 2017 17:47

peterschrammel added a commit that referenced this pull request May 10, 2017

Merge pull request #840 from allredj/test-gen-string-fix-241

0bc3416

Fix issue #241 - Conversion from int

smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018

Merge pull request diffblue#241 from diffblue/feature/slicer_integration

706d19f

SEC-41 : Integration of the 'full-slicer' into the pipe-line (tools-chain).

chrisr-diffblue added a commit to chrisr-diffblue/cbmc that referenced this pull request Aug 24, 2018

Merge pull request diffblue#241 from danpoe/fixes/reaching-definition…

05dbd4b

…s-with-sharing-merge Fix reaching definitions with sharing merge


		\*******************************************************************/

		// unit tests

Goto instrument loop unwinding #241

Goto instrument loop unwinding #241

Uh oh!

Conversation

danpoe commented Sep 27, 2016

Uh oh!

danpoe commented Sep 28, 2016

Uh oh!

kroening commented Oct 30, 2016

Uh oh!

danpoe commented Oct 31, 2016

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!

tautschnig commented Nov 25, 2016 via email

Uh oh!

danpoe commented Nov 26, 2016

Uh oh!

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

tautschnig commented Dec 1, 2016

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!

danpoe commented Dec 2, 2016

Uh oh!

Uh oh!