Added extra use-case hints to the already present invariant definitions. #1

NlightNFotis · 2018-07-31T16:00:31Z

This is just a dummy PR, against my own fork, so that people can review early the changes in the invariant code and documentation before they get submitted to develop.

hannes-steffenhagen-diffblue

I'm not really sure these changes are necessary

hannes-steffenhagen-diffblue · 2018-07-31T16:02:46Z

src/util/invariant.h

+// member variables of the object, in case they are implicit input to
+// the function. It is also supposed to signal that even though an object
+// is in a valid state, a particular function may not be operating on
+// objects with the particular properties this one enjoys.


yes, this is why I wanted a review. Maybe an Englishman can chime in? I don't know what a proper expression for that would be, but I don't think that what's there is unreasonable.

Instead of adding the first part of this description, can we rephrase the existing one above? Maybe something like The condition should only contain (unmodified) inputs to the method. Inputs include arguments passed to the method, as well as member variables that the method may read.

hannes-steffenhagen-diffblue · 2018-07-31T16:04:29Z

src/util/invariant.h

+//
+// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
+// supposed to assert much more specific details about what a function has
+// returned, that is dependent on the specific needs of a caller.


The difference between POST_CONDITION and CHECK_RETURN isn't the details, it's that one is a statement of a function about itself, whereas the other is a statement about what a caller expects from a function.

hannes-steffenhagen-diffblue · 2018-07-31T16:04:53Z

src/util/invariant.h

+//
+// It is okay for a DATA_INVARIANT to have an empty string as a reason string
+// if you can't state the reason, or doing so doesn't add any information -
+// just restates the condition.


IMHO doesn't belong as part of the documentation, also note that there are almost always better options.

hannes-steffenhagen-diffblue · 2018-07-31T16:06:55Z

src/util/invariant.h

+// to migrate documentation and "error handling" in older code.
+//
+// It is okay to use these annotations during development locally, but
+// make sure they are not present in any PR you are submitting.


That's a code/development style consideration that doesn't really belong here; In actual reality this is no different from "should not be used", obviously any code that's not made visible to other people doesn't fall under the style guidelines.

danpoe · 2018-07-31T18:35:13Z

src/util/invariant.h

+// member variables of the object, in case they are implicit input to
+// the function. It is also supposed to signal that even though an object
+// is in a valid state, a particular function may not be operating on
+// objects with the particular properties this one enjoys.


Instead of adding the first part of this description, can we rephrase the existing one above? Maybe something like The condition should only contain (unmodified) inputs to the method. Inputs include arguments passed to the method, as well as member variables that the method may read.

danpoe · 2018-07-31T18:44:51Z

src/util/invariant.h

+//
+// A POSTCONDITION documents what the function can guarantee after a "normal"
+// execution about the state it returns to its caller (properties of objects
+// that it returns).


Can we rephrase this to something like: A POSTCONDITION documents what the method guarantees about its output when it returns, given that it was called with valid inputs. Outputs include the return value of the method, as well as member variables that the method may write.

danpoe · 2018-08-01T16:11:19Z

src/util/invariant.cpp

-      << "Reason: " << reason
-      << "\nBacktrace:\n"
+      << "Reason: " << reason << '\n'
+      << "Backtrace:" << '\n'


Could include newline in string: "Backtrace:\n"

Ahh no. It was like that but I changed it to make it more uniform and consistent with the rest of the stringbuilding process.

danpoe · 2018-08-01T17:29:26Z

src/util/invariant.h

+    function,
+    line,
+    backtrace,
+    std::forward<Params>(params)...,


Can we have the variable number of arguments as the last argument? (i.e., change the order of this line and the subsequent one). We also need to change the order of the reason and the condition parameters of the constructor of invariant_failedt then.

danpoe

LGTM

krobelus · 2018-08-02T14:42:07Z

src/util/invariant.h

@@ -225,15 +230,26 @@ inline void invariant_violated_string(
 // for INVARIANT.

 // The condition should only contain (unmodified) arguments to the method.
+// Inputs includ arguments passed to the function, as well as member 


typo, should be "include"

krobelus · 2018-08-02T14:43:02Z

src/util/invariant.h

@@ -242,6 +258,10 @@ inline void invariant_violated_string(
 // changed by a previous method call.
 // "The contract of the previous method call means the following
 //  condition holds".
+//
+// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
+// a statement about the what the caller expects from a function, whereas a


typo, "the" should be removed

krobelus · 2018-08-02T15:01:20Z

src/util/invariant.cpp

-      << " line " << line << '\n'
-      << "Reason: " << reason
-      << "\nBacktrace:\n"
+      << "File " << file << " function " << function << " line " << line << '\n'


Since you're already touching this, maybe it's clearer to insert a comma after the function name, or use something like <file:line>

krobelus · 2018-08-02T15:01:21Z

src/util/invariant.cpp

+      << "File " << file << " function " << function << " line " << line << '\n'
+      << "Condition: " << condition << '\n'
+      << "Reason: " << reason << '\n'
+      << "Backtrace:" << '\n'
      << backtrace << '\n';


It seems that the word "Backtrace" occurs twice in the example, so I think we should remove
https://github.com/NlightNFotis/cbmc/blob/invariant_changes/src/util/invariant.cpp#L82

Nice, I hadn't seen that backtrace was there. Thanks for it.

NlightNFotis · 2018-08-02T15:43:01Z

@krobelus Solid review, thanks for your time.

NlightNFotis · 2018-08-02T16:03:43Z

This has served its purpose as a primary discussion ground for this work, and has now been superseded by the actual PR against develop --> diffblue#2666

We should keep the struct tag type, not follow it and get the struct type

hannes-steffenhagen-diffblue reviewed Jul 31, 2018

View reviewed changes

danpoe reviewed Jul 31, 2018

View reviewed changes

danpoe reviewed Aug 1, 2018

View reviewed changes

NlightNFotis force-pushed the invariant_changes branch from 062c8b1 to 33ca9e2 Compare August 2, 2018 13:22

danpoe approved these changes Aug 2, 2018

View reviewed changes

krobelus reviewed Aug 2, 2018

View reviewed changes

NlightNFotis force-pushed the invariant_changes branch 2 times, most recently from fed7ea1 to fe36e4e Compare August 2, 2018 15:48

NlightNFotis added 3 commits August 2, 2018 16:56

Added extra use-case hints to the already present invariant definitions.

acc1586

Pass the condition to the invariant_failedt constructor.

a7b972d

Refactor invariant_failedt definition.

07d0703

NlightNFotis force-pushed the invariant_changes branch from fe36e4e to 07d0703 Compare August 2, 2018 15:58

NlightNFotis closed this Aug 2, 2018

NlightNFotis pushed a commit that referenced this pull request Apr 9, 2019

Fix wrong type for dereference expression #1

a72469a

We should keep the struct tag type, not follow it and get the struct type

Added extra use-case hints to the already present invariant definitions. #1

Added extra use-case hints to the already present invariant definitions. #1

Uh oh!

Conversation

NlightNFotis commented Jul 31, 2018

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!

Choose a reason for hiding this comment

Uh oh!

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

NlightNFotis commented Aug 2, 2018

Uh oh!

NlightNFotis commented Aug 2, 2018

Uh oh!

Uh oh!