Invariant cleanup goto programs sz by xbauch · Pull Request #2968 · diffblue/cbmc

xbauch · 2018-09-17T13:36:55Z

No description provided.

allredj

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

peterschrammel · 2018-09-17T17:27:44Z

src/goto-programs/set_properties.cpp

-    throw "property "+id2string(*property_set.begin())+" not found";
+  INVARIANT_WITH_DIAGNOSTICS(
+    property_set.empty(),
+    "Property ",


start with lower case (several occurrences)

This one is a message that is aimed at the user; it is NOT checking an invariant!

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

src/goto-programs/string_instrumentation.cpp

    error().source_location=target->source_location;
    error() << "sprintf expected to have two or more arguments" << eom;
-    throw 0;
+    UNREACHABLE;


The check as a whole should be an invariant (several occurrences).

This is not an invariant either; it is an input condition check. An invariant is something that the program maintains internally, and not something it expects the environment to provide.

I would expect this to be ensured by the C frontend (which it actually does). After that we should be able to assume it invariant.

kroening

There is a fundamental confusion here between invariants and input checks.

xbauch · 2018-09-18T09:39:40Z

I've tried distinguishing between user input error and invariants. Unknown user input is handled by a new exception class and invalid input by the invalid_user_input_exceptiont. The messages were unified to start lower case and end without full stop.

tautschnig · 2018-09-18T09:56:01Z

src/goto-programs/slice_global_inits.cpp

-  if(!goto_functions.function_map.count(entry_point))
-    throw "entry point not found";
+  INVARIANT(
+    goto_functions.function_map.count(entry_point), "entry point not found");


Do all current invocations of this function make sure this invariant truly holds?

Well it's not guaranteed by the invocation; I guess it's more like a property of a well-formed goto-program. Maybe a DATA_INVARIANT would be more appropriate.

I'd say the fix is to make sure it is guaranteed by all current invocations. The INVARIANT then makes this future-proof as additional invocation points added later on may fail to do the same check.

I dag a bit deeper and the input goto_model is (so far always) a product of read_goto_binary. I've added a post-condition to the read_bin_goto_object_v4 function, so that only models with entry points are presently produced.

This is really not guaranteed, and it's not desired to be guaranteed.
This is really a 'user input error'.

Ok. I think we use invalid_user_input exceptions for invalid command line options. On one hand the error originates from the source code but on the other hand the well-formedness of a goto-programs requires an entry point. For now the code throws incorrect_goto_program exception, but I can re-write it, if incorrect_source_program would be more accurate.

tautschnig · 2018-09-18T09:57:41Z

src/goto-programs/string_instrumentation.cpp

+
+    throw invalid_user_input_exceptiont(
+      "sprintf expected to have two or more arguments",
+      "sprintf(char *str, const char *format, ...);");


Is the error() output above now redundant? It certainly seems to be a bad idea to duplicate text?

tautschnig · 2018-09-18T09:58:56Z

src/goto-programs/vcd_goto_trace.cpp

  else if(expr.id()==ID_union)
  {
-    assert(expr.operands().size()==1);
+    INVARIANT(expr.operands().size() == 1, "union only takes 1 operand");


I'd suggest to use union_exprt/to_union_expr. Let's not duplicate invariant checks.

kroening · 2018-09-18T10:56:26Z

Another problem is that throwing an exception is very terminal -- we may wish to record the fact that there is an error, and continue processing, possibly to generate further error messages.

tautschnig · 2018-09-18T10:58:15Z

Another problem is that throwing an exception is very terminal -- we may wish to record the fact that there is an error, and continue processing, possibly to generate further error messages.

Yes, but whether this can or cannot be done is very context dependent, and I'm not sure this specifically applies to any of the changes in this PR?

allredj

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

tautschnig · 2018-09-19T14:50:25Z

src/goto-programs/read_bin_goto_object.cpp


  functions.compute_location_numbers();

+  POSTCONDITION(functions.function_map.count(goto_functionst::entry_point()));


Nit pick: Visual Studio warns about this conversion from an integer to a Boolean. So either add != 0 or use functions.function_map.find(...) != functions.function_map.end().

Added comparison with 0.

tautschnig · 2018-09-19T14:51:46Z

src/goto-programs/show_symbol_table.cpp

-      if(ptr==nullptr)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
+      INVARIANT_WITH_DIAGNOSTICS(
+        ptr != nullptr, "symbol ", id2string(symbol.name), " has unknown mode");


There is #2984, which will do away with all this code...

Rolled back all changes in this file, hopefully #2984 will clean it adequately.

tautschnig · 2018-09-19T14:52:33Z

src/goto-programs/vcd_goto_trace.cpp

-#include <cassert>
 #include <ctime>

+#include <util/invariant.h>


No invariant added?

Removed as now redundant, invariant check is inside to_union_expr.

allredj

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

xbauch · 2018-09-20T08:57:05Z

Squashed the commits, rebased, re-worked to use the incorrect_goto_program_exceptiont from #2996.

allredj

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

kroening · 2018-09-21T20:55:39Z

src/goto-instrument/goto_instrument_parse_options.cpp

+  POSTCONDITION(
+    goto_model.goto_functions.function_map.count(
+      goto_functionst::entry_point()) != 0);
 }


This is certainly not guaranteed to hold -- we may wish to instrument goto binaries before linking is completed.

Ok, removed.

kroening · 2018-09-21T20:57:18Z

src/goto-programs/set_properties.cpp

+    throw invalid_user_input_exceptiont(
+      "property " + id2string(*property_set.begin()) + " unknown",
+      "--property id");
 }


That new exception isn't caught!

Added catch blocks to all call sites.

kroening · 2018-09-21T20:58:35Z

src/goto-programs/slice_global_inits.cpp

-  if(!goto_functions.function_map.count(entry_point))
-    throw "entry point not found";
+  INVARIANT(
+    goto_functions.function_map.count(entry_point), "entry point not found");


This is really not guaranteed, and it's not desired to be guaranteed.
This is really a 'user input error'.

kroening · 2018-09-21T20:59:22Z

src/goto-programs/slice_global_inits.cpp

-  assert(f_it!=goto_functions.function_map.end());
+  INVARIANT(
+    f_it != goto_functions.function_map.end(), "initialize function not found");



This isn't an internal invariant, but a well-formed-ness condition on the goto binary.

Changed to incorrect goto exception.

kroening · 2018-09-21T20:59:59Z

src/goto-programs/string_instrumentation.cpp

+    throw incorrect_goto_program_exceptiont(
+      "sprintf expected to have two or more arguments",
+      target->source_location);
  }


This isn't really a property of the goto-program, but one of the original source code.

Introduced new exception for source code errors (used a few times in this file).

kroening · 2018-09-21T21:00:11Z

src/goto-programs/string_instrumentation.cpp

+    throw incorrect_goto_program_exceptiont(
+      "snprintf expected to have three or more arguments",
+      target->source_location);
  }


kroening · 2018-09-21T21:01:12Z

src/goto-programs/vcd_goto_trace.cpp

-    assert(expr.operands().size()==1);
-    return as_vcd_binary(expr.op0(), ns);
+    return as_vcd_binary(to_union_expr(expr).op0(), ns);
  }


I'd write .op() above.

kroening · 2018-09-21T21:02:13Z

src/goto-programs/write_goto_binary.cpp

+    throw invalid_user_input_exceptiont(
+      "version no longer supported",
+      "supported version = " + std::to_string(current_goto_version));
+  else if(version > current_goto_version)


If you print the current version, also print the version of the goto binary.

allredj

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

peterschrammel · 2018-09-24T15:19:34Z

src/cbmc/cbmc_parse_options.cpp

      ::set_properties(goto_model, cmdline.get_values("property"));
  }

+  catch(const incorrect_goto_program_exceptiont &e)


I don't like these try-catch blocks that do not perform any recovery action. In my opinion, all the try-catch blocks in cbmc_parse_options can be removed because the only action that is taken is to exit. The same can be achieved in a much cleaner way by catching those exceptions at top-level (parse_optionst) only.

Yes, it's much neater catching them all in parse_option_baset.

allredj

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

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

src/util/parse_options.cpp

    std::cerr << e.what() << "\n";
    return CPROVER_EXIT_USAGE_ERROR;
  }
+  catch(const incorrect_goto_program_exceptiont &e)


Isn't that subsumed by the case below?

Yes, I guess the intention is to distinguish individual exception classes, maybe different error message or return code. There is not dedicated error code for incorrect goto programs, only for PARSE_ERROR.

parse_options_baset is mean to be very broadly applicable -- including in programs that do not know anything about goto_programs. I would go for a broader superclass here.

Ok, catching incorrect_goto_program is omitted, and cprover_exception_baset is caught directly.

allredj

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

kroening · 2018-09-25T16:35:30Z

src/goto-programs/slice_global_inits.cpp

-    throw "entry point not found";
+  if(goto_functions.function_map.count(entry_point) == 0)
+    throw incorrect_goto_program_exceptiont("entry point not found");



I'd say it's misleading to throw this exception. A goto program without entry point is in no way malformed or incorrect.

Ok, I think that invalid_user_input would be misleading as well, so I've added user_input_error exception (locally in slice_global_inits until use elsewhere is required).

allredj

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

chrisr-diffblue · 2018-10-04T10:13:36Z

@kroening - Could you re-review this PR when you have a moment or two? we think this is now just blocked on your input.

kroening · 2018-10-04T10:17:26Z

src/goto-programs/slice_global_inits.h

+  }
+
+  std::string what() const
+  {


Add 'override'

kroening · 2018-10-04T10:19:12Z

src/goto-programs/string_instrumentation.h

+  {
+  }
+  std::string what() const
+  {


allredj

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

xbauch requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 17, 2018 13:36

allredj reviewed Sep 17, 2018

View reviewed changes

peterschrammel requested changes Sep 17, 2018

View reviewed changes

kroening requested changes Sep 18, 2018

View reviewed changes

tautschnig reviewed Sep 18, 2018

View reviewed changes

allredj reviewed Sep 18, 2018

View reviewed changes

tautschnig reviewed Sep 19, 2018

View reviewed changes

xbauch requested review from chrisr-diffblue and martin-cs as code owners September 19, 2018 15:57

allredj reviewed Sep 19, 2018

View reviewed changes

xbauch force-pushed the cleanup_goto-s-z branch from 0f2549d to a094ff7 Compare September 20, 2018 08:54

allredj reviewed Sep 20, 2018

View reviewed changes

tautschnig assigned kroening and peterschrammel Sep 20, 2018

kroening requested changes Sep 21, 2018

View reviewed changes

xbauch requested review from cesaro, cristina-david and mgudemann as code owners September 24, 2018 08:50

tautschnig assigned xbauch Sep 24, 2018

xbauch force-pushed the cleanup_goto-s-z branch from 650d39b to dbad224 Compare September 24, 2018 10:21

allredj reviewed Sep 24, 2018

View reviewed changes

peterschrammel reviewed Sep 24, 2018

View reviewed changes

xbauch force-pushed the cleanup_goto-s-z branch from 50719d5 to d556b4f Compare September 24, 2018 15:49

allredj reviewed Sep 24, 2018

View reviewed changes

peterschrammel approved these changes Sep 24, 2018

View reviewed changes

allredj reviewed Sep 25, 2018

View reviewed changes

kroening reviewed Sep 25, 2018

View reviewed changes

allredj reviewed Sep 26, 2018

View reviewed changes

kroening reviewed Oct 4, 2018

View reviewed changes

src/goto-programs/slice_global_inits.h

}

std::string what() const

{

Copy link

Collaborator

kroening Oct 4, 2018

Choose a reason for hiding this comment

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

Add 'override'

kroening reviewed Oct 4, 2018

View reviewed changes

src/goto-programs/string_instrumentation.h

{

}

std::string what() const

{

Copy link

Collaborator

kroening Oct 4, 2018

Choose a reason for hiding this comment

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

override

kroening approved these changes Oct 4, 2018

View reviewed changes

xbauch force-pushed the cleanup_goto-s-z branch 2 times, most recently from 059e0a1 to 3aee09c Compare October 4, 2018 11:57

Invariant cleanup goto programs sz

cb844be

xbauch force-pushed the cleanup_goto-s-z branch from 3aee09c to cb844be Compare October 4, 2018 12:30

xbauch merged commit b9b40ed into diffblue:develop Oct 4, 2018

allredj reviewed Oct 4, 2018

View reviewed changes

xbauch deleted the cleanup_goto-s-z branch December 4, 2018 08:58


		functions.compute_location_numbers();

		POSTCONDITION(functions.function_map.count(goto_functionst::entry_point()));

Conversation

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

kroening left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Sep 18, 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!

kroening commented Sep 18, 2018

Uh oh!

tautschnig commented Sep 18, 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Sep 20, 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!