Invariant cleanup goto programs jr #2967

hannes-steffenhagen-diffblue · 2018-09-17T13:24:45Z

Only 793fe3b and later are new (will require rebase later, this is just up for review now).

allredj

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

peterschrammel · 2018-09-17T17:19:07Z

src/goto-programs/lazy_goto_model.cpp

-        throw 0;
+        throw deserialization_exceptiont(
+          "failed to figure out type of file"
+          "\nsource location: " +


A structured variant would be good to enable proper JSON/XML output of the source location.

Actually, it seems like the source location here is only used to communicate the filename. I'll reword the error message.

In this case the source location is actually just used to communicate the file name, so I think I'll just reword the message

peterschrammel · 2018-09-17T17:19:28Z

src/goto-programs/lazy_goto_model.cpp

@@ -94,8 +95,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
  const std::vector<std::string> &files=cmdline.args;
  if(files.empty())
  {
-    msg.error() << "Please provide a program" << messaget::eom;
-    throw 0;
+    throw invalid_user_input_exceptiont("No program provided", "", "");


Provide a proper constructor for such a case

peterschrammel · 2018-09-17T17:19:56Z

src/goto-programs/link_goto_model.cpp

-
+  {
+    // TODO more helpful error message
+    throw deserialization_exceptiont("Typechecking main failed");


start with lower case (several occurrences)

peterschrammel · 2018-09-17T17:20:37Z

src/goto-programs/remove_vector.cpp

@@ -114,13 +115,14 @@ static void remove_vector(exprt &expr)
    }
    else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
    {
+      DATA_INVARIANT(
+        expr.operands().size() == 1, "unary operators have one operands");


peterschrammel · 2018-09-17T17:21:17Z

src/goto-programs/replace_calls.cpp

-          throw "Returns must not be removed before replacing calls";
+        INVARIANT(
+          !has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX),
+          "this happens before returns are removed");


The original message was somehow better.

tautschnig · 2018-09-19T15:21:40Z

src/goto-programs/lazy_goto_model.cpp

@@ -158,8 +159,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)

    if(language_files.typecheck(symbol_table))
    {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      // TODO more helpful error message


I'm not sure this is a TODO (and neither in the parser case): those "more helpful error messages" are provided already, during parsing/type checking.

src/goto-programs/osx_fat_reader.cpp

tautschnig · 2018-09-19T15:25:22Z

src/goto-programs/remove_complex.cpp

@@ -32,10 +32,10 @@ static exprt complex_member(const exprt &expr, irep_idt id)
  }
  else
  {
-    assert(expr.type().id()==ID_struct);
+    PRECONDITION(expr.type().id() == ID_struct);


That's actually checked by the subsequent to_struct_type

tautschnig · 2018-09-19T15:27:44Z

src/goto-programs/remove_complex.cpp

@@ -222,12 +229,12 @@ static void remove_complex(exprt &expr)

  if(expr.id()==ID_complex_real)
  {
-    assert(expr.operands().size()==1);
+    static_cast<void>(to_complex_real_expr(expr));


Better use this in the subsequent statement: expr = complex_member(to_complex_real_expr(expr).op(), ID_real)

tautschnig · 2018-09-19T15:28:59Z

src/goto-programs/remove_unused_functions.cpp

+          INVARIANT(
+            call.function().id() == ID_symbol,
+            "by this point, all kinds of function calls should have been "
+            "converted to simple function calls");


Maybe add the error message as a comment in here, but really to_symbol_expr below actually takes care of this.

allredj

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

hannes-steffenhagen-diffblue · 2018-10-03T11:31:30Z

@peterschrammel @tautschnig I believe I've addressed your comments on here now, could you please re-review?

tautschnig · 2018-10-03T11:56:17Z

src/goto-programs/lazy_goto_model.cpp

@@ -17,6 +17,7 @@
 #include <langapi/language.h>

 #include <fstream>
+#include <util/exception_utils.h>


Nit pick: please move this a few lines up, with the other util includes.

tautschnig · 2018-10-03T11:57:48Z

src/goto-programs/lazy_goto_model.cpp

-                    << '\'' << messaget::eom;
-        throw 0;
+        throw system_exceptiont(
+          "failed to open input file `" + filename + '\'');


Isn't this (most likely) also an invalid_user_input_exceptiont. It's of course possible that your file system is somehow hosed, but in almost all cases the user will be the one who got it wrong.

It's quite possible that the root cause is because the user passed in the wrong filename. Or it could fail for other reasons. The only thing we know at this point is that we can't open the file, so we report that as such here.

tautschnig · 2018-10-03T11:58:55Z

src/goto-programs/lazy_goto_model.cpp

@@ -147,8 +147,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)

      if(language.parse(infile, filename))
      {
-        msg.error() << "PARSING ERROR" << messaget::eom;
-        throw 0;
+        throw deserialization_exceptiont("PARSING ERROR");


Isn't this invalid input? (I.e., another case of a user error.)

deserialization_exceptiont is for "invalid inputs", but of another kind. If you look at invalid_user_input_exceptiont it's actually just indicating malformed arguments (IMHO it should be renamed to something like bad_argument_exceptiont), whereas deserialization_exceptiont means we got some input but it wasn't in the format that we expected.

tautschnig · 2018-10-03T11:59:15Z

src/goto-programs/lazy_goto_model.cpp

@@ -158,8 +157,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)

    if(language_files.typecheck(symbol_table))
    {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      throw deserialization_exceptiont("CONVERSION ERROR");


As above: I don't think deserialization_exceptiont is the right choice.

tautschnig · 2018-10-03T12:00:16Z

src/goto-programs/link_goto_model.cpp

-      linking.object_type_updates))
-    throw 0;
+  {
+    throw deserialization_exceptiont("typechecking main failed");


As above: this is the result of invalid user input.

tautschnig · 2018-10-03T12:02:58Z

src/goto-programs/remove_complex.cpp

-          ID_complex_real, expr.op0(), expr.op0().type().subtype());
+          ID_complex_real,
+          typecast_expr.op(),
+          typecast_expr.op().type().subtype());


We now have a complex_real_exprt, please use this one in here while changing those lines.

tautschnig · 2018-10-03T12:09:53Z

src/goto-programs/remove_complex.cpp


      expr=struct_expr;
    }
    else if(expr.id()==ID_complex)
    {
-      assert(expr.operands().size()==2);
+      static_cast<void>(to_complex_expr(expr));
      expr.id(ID_struct);


Maybe we should just make this code a bit more explicit:

struct_exprt s(expr.type()); s.add_source_location() = expr.source_location(); s.copy_to_operands(to_complex_expr(expr).real(), to_complex_expr(expr).imag()); expr.swap(s);

I've been meaning to ask, why do we prefer swap over assignment in these cases?

Swapping two irept is literally just swapping two pointers, doing operator= involves a sequence of reference-count updates -- unless rvalue references can be used, at which point it's just a swap again. But then the mentioned reference-count updates may happen either way if one of the swapped irepts goes out of scope. So it's probably an unmeasurable difference.

tautschnig · 2018-10-03T12:11:18Z

src/goto-programs/remove_vector.cpp

@@ -108,13 +109,14 @@ static void remove_vector(exprt &expr)
    }
    else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
    {
+      DATA_INVARIANT(
+        expr.operands().size() == 1, "unary operators have one operand");


Could still use to_unary_expr instead

tautschnig · 2018-10-03T12:11:40Z

src/goto-programs/remove_vector.cpp

@@ -82,13 +82,14 @@ static void remove_vector(exprt &expr)
       expr.id()==ID_mod  || expr.id()==ID_bitxor ||
       expr.id()==ID_bitand || expr.id()==ID_bitor)
    {
+      DATA_INVARIANT(
+        expr.operands().size() == 2, "binary operators have 2 operands");


How about to_binary_expr?

allredj

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

hannes-steffenhagen-diffblue · 2018-10-04T15:29:42Z

I'll use the invalid_source_file_exceptiont for this, but it's blocked on #3099 at the moment (travis taking very long for some reason).

tautschnig · 2018-10-04T17:18:52Z

Should be unblocked by now (#3099 has been merged).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 3fa5d57).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87482764
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: e9067f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87486188

hannes-steffenhagen-diffblue · 2018-10-10T14:13:56Z

@tautschnig I've changed the exception types (except for one system_exceptiont where I still think it's the right one to use, even though I see the argument). Would you mind taking another look?

martin-cs

The older code is confused about which are binary and which are n-ary operations. This is not uncommon as I remember submitting the patch that started clarifying this. My guess is that there aren't tests for this. Fixing it may be beyond the scope of this PR but we should at least have the checks and invariants correctly annotated.

src/goto-programs/remove_complex.cpp

src/goto-programs/remove_unused_functions.cpp

src/goto-programs/remove_vector.cpp

allredj

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

hannes-steffenhagen-diffblue · 2018-10-16T10:27:41Z

@martin-cs I changed the DATA_INVARIANT to precondition, added a precondition in the other case where it just used to_binary_expr without a check before, and reworded the fixme comment to make it more clear that the operations are n-ary operations specifically rather than just "not binary".

martin-cs · 2018-10-16T10:46:55Z

@hannes-steffenhagen-diffblue : Thank you.

martin-cs

All issues I raised have been handled appropriately.

tautschnig · 2018-10-16T10:52:20Z

src/goto-programs/lazy_goto_model.cpp

-      throw 0;
+    {
+      source_locationt source_location;
+      source_location.set_file(irep_idt(file));


I am surprised you actually need the irep_idt in there?

We don't. Not sure why that's in here, I'll remove it.

tautschnig · 2018-10-16T11:16:29Z

src/goto-programs/remove_complex.cpp

-      assert(expr.operands().size()==2);
-      expr.id(ID_struct);
+      auto const &complex_expr = to_complex_expr(expr);
+      struct_exprt struct_expr{complex_expr.type()};


Nit pick: use round parentheses

allredj

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

allredj

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

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

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch from 4d8920e to 4f9e5c8 Compare September 17, 2018 15:15

allredj reviewed Sep 17, 2018

View reviewed changes

peterschrammel reviewed Sep 17, 2018

View reviewed changes

tautschnig reviewed Sep 19, 2018

View reviewed changes

tautschnig assigned hannes-steffenhagen-diffblue Sep 24, 2018

hannes-steffenhagen-diffblue added the work in progress label Oct 1, 2018

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch 3 times, most recently from ca29d81 to 5ec6f92 Compare October 3, 2018 09:30

allredj reviewed Oct 3, 2018

View reviewed changes

hannes-steffenhagen-diffblue removed the work in progress label Oct 3, 2018

tautschnig reviewed Oct 3, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch from 5ec6f92 to a7c8bab Compare October 3, 2018 14:49

allredj reviewed Oct 3, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch 2 times, most recently from 3fa5d57 to e9067f4 Compare October 10, 2018 12:22

allredj reviewed Oct 10, 2018

View reviewed changes

martin-cs requested changes Oct 11, 2018

View reviewed changes

src/goto-programs/remove_complex.cpp Outdated Show resolved Hide resolved

src/goto-programs/remove_unused_functions.cpp Show resolved Hide resolved

src/goto-programs/remove_vector.cpp Show resolved Hide resolved

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch from e9067f4 to 4a46e09 Compare October 11, 2018 17:05

allredj reviewed Oct 11, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch from 4a46e09 to 75414ce Compare October 16, 2018 10:26

martin-cs approved these changes Oct 16, 2018

View reviewed changes

tautschnig approved these changes Oct 16, 2018

View reviewed changes

allredj reviewed Oct 16, 2018

View reviewed changes

hannes-steffenhagen-diffblue added 14 commits October 16, 2018 17:00

Cleanup invariants in lazy_goto_model

c20fe41

Cleanup invariants in link_goto_model

c5f3488

Cleanup invariants in loop_ids

15fec06

Cleanup invariants in osx_fat_reader

63742c7

Cleanup invariants in parameter_assignments

b2bf11e

Cleanup invariants in pointer_arithmetic

50fd256

Cleanup invariants in printf_formatter

5145d8c

Cleanup invariants in read_bin_goto_object

0f35450

Cleanup invariants in remove_complex

46a233a

Cleanup invariants in remove_const_function_pointers

0b7375e

Cleanup invariants in remove_function_pointers

4011b08

Cleanup invariants in remove_unused_functions

bcc5ed9

Cleanup invariants in remove_vector

5aaeaf8

Cleanup invariants in replace_calls

365bb72

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto_programs-jr branch from 75414ce to 365bb72 Compare October 16, 2018 16:00

allredj reviewed Oct 16, 2018

View reviewed changes

hannes-steffenhagen-diffblue merged commit 3123dba into diffblue:develop Oct 16, 2018

Invariant cleanup goto programs jr #2967

Invariant cleanup goto programs jr #2967

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Sep 17, 2018

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!

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!

hannes-steffenhagen-diffblue commented Oct 3, 2018

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Oct 4, 2018

Uh oh!

tautschnig commented Oct 4, 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!

hannes-steffenhagen-diffblue commented Oct 10, 2018

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment