Refactoring around the goto-cc entry point. #5442

thomasspriggs · 2020-08-03T13:15:47Z

As I was working on #5440, I found the entry point code less than straight forward to follow. I carried out this refactorings locally in order to make it easier for me to understand. I am raising this separate PR containing the refactoring work only as it was not required in order to implement the feature in the original PR, but should still improve maintainability.

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.
N/A - No user visible behaviour changes. ~~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 - None claimed ~~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.

hannes-steffenhagen-diffblue · 2020-08-03T15:00:28Z

src/goto-cc/armcc_cmdline.cpp

@@ -265,6 +265,21 @@ static const char *options_with_arg[]=
  nullptr
 };

+static bool
+prefix_in_list(const char *option, const char **list, std::string &prefix)


I think we could simplify a lot of this if we stored the args in the mode as std::vector<std::string> instead of char **. Then we could also just use regular std::find or something like that instead of this.

That sounds like a good follow up refactoring.

hannes-steffenhagen-diffblue · 2020-08-03T15:01:41Z

src/goto-cc/armcc_cmdline.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening
 #include <cstring>
 #include <iostream>

+#include "optional.h"


should be <util/optional.h>

hannes-steffenhagen-diffblue · 2020-08-03T15:02:45Z

src/goto-cc/armcc_cmdline.cpp

@@ -265,19 +267,18 @@ static const char *options_with_arg[]=
  nullptr
 };

-static bool
-prefix_in_list(const char *option, const char **list, std::string &prefix)
+static optionalt<std::string>


Like I said above, I'd prefer not touching this like this for now and instead changing how we store command line arguments, then we don't have to invent our own finds at all.

Yes, I think that using a standard container would be a great follow-up refactoring. However I would argue that removing the need for an output parameter is already a step in the right direction, which makes the usages of this function more readable.

hannes-steffenhagen-diffblue · 2020-08-03T15:03:46Z

src/goto-cc/goto_cc_cmdline.cpp

@@ -117,3 +117,13 @@ void goto_cc_cmdlinet::add_infile_arg(const std::string &arg)
    fclose(tmp);
  }
 }
+
+bool goto_cc_cmdlinet::have_infile_arg() const


I think we should probably just make sure to put definitions in cpp files in general.

hannes-steffenhagen-diffblue · 2020-08-03T15:05:04Z

src/util/bv_encoding.h

+
+Author: Diffblue Ltd
+
+\*******************************************************************/


I think I mentioned this before but we want to move away from this style of module header... we might have to adjust our linter for that though.

I have removed this commit from this PR.

hannes-steffenhagen-diffblue · 2020-08-03T15:20:39Z

src/util/bv_encoding.h

+
+#include <cstddef>
+
+struct bv_encodingt


Moves it into a different namespace though

Ok. I'll leave it where it was then.

hannes-steffenhagen-diffblue · 2020-08-03T15:21:42Z

src/util/bv_encoding.h

@@ -11,7 +11,7 @@ Author: Diffblue Ltd

 #include <cstddef>

-struct bv_encodingt
+struct bv_encodingt final


I'm not sure that's necessary, I find final to be a bit noisy. To me final actually suggests the opposite of what you're saying here: This is part of a class hierarchy, it's just supposed to be at the bottom of it.

You know that isn't part of a hierarchy from reading this line of code, because no base classes are specified. Having it specified as final also means that you are always safe to pass / return / assign instances of this class by value, without risk of slicing occurring. I do take your point about noise however. I think I may drop this commit as I don't really want to include anything in this PR, where the pros and cons could be argued either way. Suffice to say that my current habit is to make new classes/structs final by default, in the same way as I would make variables and member functions const by default.

hannes-steffenhagen-diffblue · 2020-08-03T15:25:08Z

src/util/bv_encoding.cpp

+  const std::string &argument,
+  const std::size_t pointer_width)
+{
+  const unsigned int object_bits = unsafe_string2unsigned(argument);


Use string2optional here so you can handle a parse error with a proper error message. The unsafe_ functions are for when you know the parse will succeed.

Yep. A non-integer argument will cause an invariant violation, both before and after this PR. This is expected as the PR is intended to be refactoring only, not bug fixing. I agree that we should improve the error handling here.

Making this member function non-virtual makes it easier to follow the control flow because it is clear it not overridden in any sub class. This is should be easy enough to add back should a need to override this arise.

Putting implementations in `.cpp` files is the best-practise because it reduces compile times.

This avoids the need to declare and mutate iterators. Its states what it is doing by means of the name of the algorithm - `std::any_of`, which saves on reading a loop to work it out.

Making this member function non-virtual makes it easier to follow the control flow because it is clear it not overridden in any sub class. This is should be easy enough to add back should a need to override this arise.

This makes the `goto_cc_cmdlinet` class easier to follow because it can be read without seeing this special case for `armcc`.

This avoids using an output parameter, which makes it more straight forward to read the data flow.

Because this gives us compatability with modern C++ features such as ranged for loops and the algorithms in the standard template library. Because using a standard container rather than a null terminated array improves memory safety. Clang format is off for the lists of options in order to keep the existing manual formatting. This existing formatting is consistent with the other lists of options.

chrisr-diffblue · 2020-08-11T10:55:14Z

unit/goto-cc/armcc_cmdline.cpp

@@ -0,0 +1,32 @@
+// Copyright 2020 Diffblue Limited. All Rights Reserved.


I think the licence header is wrong - thats the internal Diffblue header - CBMC contributions require a different header.

chrisr-diffblue

All looks good apart from the copyright header - happy to approve once that is fixed up.

To demonstrate that the refactored version works as expected.

thomasspriggs force-pushed the tas/goto-cc-refactoring branch from 95a56d9 to 49e9b69 Compare August 3, 2020 13:39

hannes-steffenhagen-diffblue reviewed Aug 3, 2020

View reviewed changes

thomasspriggs added 6 commits August 10, 2020 11:27

Make goto_cc_modet::help non-virtual

00bdff1

Making this member function non-virtual makes it easier to follow the control flow because it is clear it not overridden in any sub class. This is should be easy enough to add back should a need to override this arise.

Move goto_cc_cmdlinet::have_infile_arg to .cpp

1fc57a6

Putting implementations in `.cpp` files is the best-practise because it reduces compile times.

Refactor goto_cc_cmdlinet::have_infile_arg using std::any_of

f0b4f89

This avoids the need to declare and mutate iterators. Its states what it is doing by means of the name of the algorithm - `std::any_of`, which saves on reading a loop to work it out.

Make goto_cc_modet::main non-virtual

1eaa260

Making this member function non-virtual makes it easier to follow the control flow because it is clear it not overridden in any sub class. This is should be easy enough to add back should a need to override this arise.

Move prefix_in_list to the single location where it is used

0313558

This makes the `goto_cc_cmdlinet` class easier to follow because it can be read without seeing this special case for `armcc`.

Refactor prefix_in_list to return its result using optionalt

cc12dff

This avoids using an output parameter, which makes it more straight forward to read the data flow.

thomasspriggs force-pushed the tas/goto-cc-refactoring branch from 49e9b69 to c562025 Compare August 10, 2020 11:30

thomasspriggs changed the title ~~Refactoring around the goto-cc entry point and the object-bits argument.~~ Refactoring around the goto-cc entry point. Aug 10, 2020

thomasspriggs force-pushed the tas/goto-cc-refactoring branch from c562025 to 53d609d Compare August 10, 2020 13:32

thomasspriggs marked this pull request as ready for review August 10, 2020 13:43

thomasspriggs requested review from chrisr-diffblue, kroening and tautschnig as code owners August 10, 2020 13:43

thomasspriggs force-pushed the tas/goto-cc-refactoring branch 2 times, most recently from 1f3710f to feacb93 Compare August 10, 2020 16:45

chrisr-diffblue reviewed Aug 11, 2020

View reviewed changes

Add unit test of prefix_in_list

f7787c8

To demonstrate that the refactored version works as expected.

thomasspriggs force-pushed the tas/goto-cc-refactoring branch from feacb93 to f7787c8 Compare August 11, 2020 15:34

chrisr-diffblue approved these changes Aug 11, 2020

View reviewed changes

thomasspriggs merged commit 7d30335 into diffblue:develop Aug 11, 2020

thomasspriggs deleted the tas/goto-cc-refactoring branch August 11, 2020 22:19


		Author: Diffblue Ltd

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

		@@ -0,0 +1,32 @@
		// Copyright 2020 Diffblue Limited. All Rights Reserved.

Refactoring around the goto-cc entry point. #5442

Refactoring around the goto-cc entry point. #5442

Uh oh!

Conversation

thomasspriggs commented Aug 3, 2020

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!