Invariant cleanup util dir tz files req exception review #2957

hannes-steffenhagen-diffblue · 2018-09-14T13:44:17Z

No description provided.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2f46062).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84838498
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

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).

allredj

Passed Diffblue compatibility checks (cbmc commit: 139a471).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84839985

allredj

Passed Diffblue compatibility checks (cbmc commit: 1881f0f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84840419

allredj

Passed Diffblue compatibility checks (cbmc commit: 6175217).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85033649

peterschrammel · 2018-09-17T17:12:47Z

src/util/union_find.cpp

@@ -51,11 +51,11 @@ void unsigned_union_find::isolate(size_type a)
    if(c==1)
      return;

-    assert(c>=2);
+    INVARIANT(c>=2, "Ensure unreachability for c <= 1"); // TODO review


clang-format (several occurrences)

peterschrammel · 2018-09-17T17:14:15Z

src/util/union_find.cpp

@@ -64,7 +64,7 @@ void unsigned_union_find::isolate(size_type a)
  // get its root
  size_type r=find(a);

-  // assert(r!=a);
+  // assert(r!=a);  // Commented out dead code? To review


peterschrammel · 2018-09-17T17:14:22Z

src/util/union_find.cpp

@@ -80,13 +80,13 @@ void unsigned_union_find::re_root(size_type old_root, size_type new_root)
  old_root=find(old_root);

  // same set?
-  // assert(find(new_root)==old_root);
+  // assert(find(new_root)==old_root); // Commented out dead code? To review


allredj

Passed Diffblue compatibility checks (cbmc commit: 543dc4d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85044564

allredj

Passed Diffblue compatibility checks (cbmc commit: 50fd483).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85127881

tautschnig · 2018-09-18T12:48:46Z

regression/cbmc/trace-values/trace-values.desc

@@ -12,7 +12,7 @@ trace-values.c
 ^  null\$object=6 .*$
 ^  junk\$object=7 .*$
 ^  dynamic_object1\[1.*\]=8 .*$
-^  my_nested\[1.*\]={ .f=0, .array={ 0, 4, 0 } } .*$
+^  my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$


Ok (I was actually kind-of surprised this passed back when the test was added) - but really this doesn't need to be in this PR and should be a PR of its own instead? And what made you notice the problem? What works now that didn't work before?

tautschnig · 2018-09-18T12:49:10Z

src/util/exception_utils.h

@@ -33,4 +33,23 @@ class invalid_user_input_exceptiont
  std::string what() const noexcept;
 };

+class system_exceptiont


See comment in another PR: this needs documentation.

Could this derive from cprover_exception_baset to that it can be caught easily at top-level?

tautschnig · 2018-09-18T12:51:13Z

src/util/union_find.cpp

@@ -51,11 +51,11 @@ void unsigned_union_find::isolate(size_type a)
    if(c==1)
      return;

-    assert(c>=2);
+    INVARIANT(c >= 2, "Ensure unreachability for c <= 1"); // TODO review


So that's really to say that c == 0 is impossible? Maybe that should be checked above, right after the assignment to c?

tautschnig · 2018-09-18T12:51:50Z

src/util/union_find.cpp

-  assert(nodes[old_root].count>=2);
+  INVARIANT(
+    new_root != old_root, "Ensure the algorithm roots differ"); // TODO review
+  INVARIANT(nodes[old_root].count >= 2, ""); // TODO review suitable statement


Work in progress?

tautschnig · 2018-09-18T12:53:28Z

src/util/union_find.h

@@ -64,7 +65,7 @@ class unsigned_union_find
  void resize(size_type size)
  {
    // We only enlarge. Shrinking is yet to be implemented.
-    assert(nodes.size()<=size);
+    PRECONDITION(nodes.size() <= size);


Maybe we should just change the API to only permit increasing size by a non-negative number of elements? This code has been around for a while, and "yet to be implemented" never materialised - so really it was never required.

@tautschnig That is presently the API (size_type is negative). However the argument isn't an increase/decrease in size but rather the absolute new size, hence the check.

Yes, but what about changing the API to make this check unnecessary?

There are two problems with an enlarge(size_t n) method: a) C++ STL usually uses resize(); b) you'd need another check like that to prevent overflowing of current_size+n.

Indeed. Then we should probably change this into

if(nodes.size() > size) UNIMPLEMENTED;

to convey what the comment says.

@tautschnig The Invariant documentation suggests that UNIMPLEMENTED should not be used though? It'd be slightly more accurate to use UNIMPLEMENTED I suppose, but it's a very marginal difference.

Sure, this is a very minor point. I'm not aware of any annotation that conveys the intent better than UNIMPLEMENTED does here, but I'm not going to insist it be used.

tautschnig · 2018-09-18T12:54:31Z

src/util/xml_expr.cpp

@@ -273,7 +274,7 @@ xmlt xml(
    {
      const struct_typet &struct_type=to_struct_type(type);
      const struct_typet::componentst &components=struct_type.components();
-      assert(components.size()==expr.operands().size());
+      CHECK_RETURN(components.size() == expr.operands().size());


I'd say that's either a PRECONDITION or a DATA_INVARIANT

tautschnig · 2018-09-18T12:54:48Z

src/util/xml_expr.cpp

@@ -287,7 +288,7 @@ xmlt xml(
  {
    result.name="union";

-    assert(expr.operands().size()==1);
+    PRECONDITION(expr.operands().size() == 1);


Use to_union_expr

tautschnig · 2018-09-18T12:59:34Z

src/util/tempdir.cpp

 {
+  // FIXME throwing from destructors is generally a bad idea
+  //       but I can't think of anything else that'd be reasonable here?


I think this code just shouldn't be doing this. If changing into the directory is desired, then the call site should do so. As a matter of fact, this code seems unused...

@tautschnig Agreed. We should consider rewriting this as part of a separate PR. For now, these changes have been undone.

Would you mind creating a fresh PR that just removes this code? I agree it doesn't fit this PR, but having said PR merged before this one would make things a lot easier.

@tautschnig #3054

peterschrammel · 2018-09-24T20:48:38Z

regression/cbmc/union10/union_list2.desc

-  (29) p1!0@1#2 == byte_extract_little_endian(u!0@1#4, 8l, struct list_item { unsigned int value; unsigned int $pad1; struct list_item *previous; } *)
-  (30) p2!0@1#2 == p1$object#0.previous
+  \(29\) p1!0@1#2 == byte_extract_little_endian\(u!0@1#4, 8l, struct list_item \{ unsigned int value; unsigned int $pad1; struct list_item *previous; \} *\)
+  \(30\) p2!0@1#2 == p1$object#0.previous


\.previous

peterschrammel · 2018-09-24T20:49:17Z

regression/cbmc/union10/union_list2.desc

 as
-  main::1::p1 = { <integer_address, *, unsigned char> }
+  main::1::p1 = \{ <integer_address, *, unsigned char> \}


peterschrammel · 2018-09-24T20:50:58Z

src/util/exception_utils.h

@@ -33,4 +33,23 @@ class invalid_user_input_exceptiont
  std::string what() const noexcept;
 };

+class system_exceptiont


Could this derive from cprover_exception_baset to that it can be caught easily at top-level?

peterschrammel · 2018-09-24T20:51:39Z

src/util/exception_utils.h

+  }
+};
+
+class deserialization_exceptiont


Derive from cprover_exception_baset?

allredj

Passed Diffblue compatibility checks (cbmc commit: 5d4ffbd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86141524

allredj

Passed Diffblue compatibility checks (cbmc commit: 6e91acb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86183571

* Deprecated c-style asserts in favour of cbmc invariants. * Some minor refactoring that was relevant to the cleanup.

allredj

Passed Diffblue compatibility checks (cbmc commit: d786c91).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86499366

hannes-steffenhagen-diffblue · 2018-10-02T15:58:00Z

@peterschrammel @tautschnig
I believe your comments on this PR are addressed now, could you please take another look at it?

hannes-steffenhagen-diffblue requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 14, 2018 13:44

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch from 2f46062 to 139a471 Compare September 14, 2018 13:53

allredj reviewed Sep 14, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch 2 times, most recently from 6175217 to 543dc4d Compare September 17, 2018 16:44

allredj reviewed Sep 17, 2018

View reviewed changes

peterschrammel reviewed Sep 17, 2018

View reviewed changes

allredj reviewed Sep 17, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch from 543dc4d to 50fd483 Compare September 18, 2018 10:26

allredj reviewed Sep 18, 2018

View reviewed changes

tautschnig reviewed Sep 18, 2018

View reviewed changes

tautschnig assigned hannes-steffenhagen-diffblue Sep 24, 2018

peterschrammel reviewed Sep 24, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch from 50fd483 to 5d4ffbd Compare September 27, 2018 11:00

tautschnig assigned sonodtt Sep 27, 2018

allredj reviewed Sep 27, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch from 5d4ffbd to 6e91acb Compare September 27, 2018 16:33

allredj reviewed Sep 27, 2018

View reviewed changes

Cleanup asserts & throws - replace with invariants

d786c91

* Deprecated c-style asserts in favour of cbmc invariants. * Some minor refactoring that was relevant to the cleanup.

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-tz_files-req_exception_review branch from 6e91acb to d786c91 Compare October 1, 2018 16:34

allredj reviewed Oct 1, 2018

View reviewed changes

tautschnig approved these changes Oct 2, 2018

View reviewed changes

tautschnig merged commit 573153a into diffblue:develop Oct 2, 2018

Invariant cleanup util dir tz files req exception review #2957

Invariant cleanup util dir tz files req exception review #2957

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Sep 14, 2018

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!

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

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!

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!

hannes-steffenhagen-diffblue Sep 24, 2018 • 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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

hannes-steffenhagen-diffblue Sep 24, 2018 •

edited

Loading