Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

peterschrammel · 2019-04-16T12:42:26Z

Most of this PR are incremental clean-ups of jbmc_parse_optionst. Review commit by commit.

[almost] 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.
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).
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.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: aa3dda9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108567170
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1ce9697).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108568076
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

tautschnig · 2019-04-17T08:21:11Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -829,7 +827,7 @@ void jbmc_parse_optionst::process_goto_function(
    function.get_function_id(),
    goto_function,
    symbol_table,
-    get_message_handler());
+    log.get_message_handler());


Nit pick: I think this change is in the wrong commit as it is a fix-up for the previous change.

tautschnig · 2019-04-17T08:25:12Z

jbmc/src/jbmc/jbmc_parse_options.cpp

+      {
+        // We can only output these after goto-symex has run.
+        (void)show_loaded_symbols(*goto_model_ptr);
+        (void)show_loaded_functions(*goto_model_ptr);


I don't understand this bit of code: the comment says that we cannot do any of this output, but then invokes two output functions, which seems like a contradiction. And then why does it do any output at all here, where has this been requested?

It says we needed to wait until after symex, which we just ran (the verifier() call above)

(normally of course we can --show-goto-functions before symex, but not when symex itself is deciding what gets loaded)

Ok, but why are we doing this output at all?

tautschnig · 2019-04-17T08:26:05Z

src/goto-checker/all_properties_verifier.h

-    // have we got anything to check? otherwise we return PASS
-    if(!has_properties_to_check(properties))
-      return resultt::PASS;
-


The commit message suggests that this code must be put somewhere else, but then the commit only removes code?

incremental_goto_checker is already doing that.

tautschnig · 2019-04-17T08:27:31Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -557,7 +557,7 @@ int jbmc_parse_optionst::doit()
  if(get_goto_program_ret != -1)
    return get_goto_program_ret;

-  if(!cmdline.isset("symex-driven-lazy-loading"))
+  if(!options.get_bool_option("symex-driven-lazy-loading"))


Is there anything we could do to completely hide cmdline from such code so that it cannot wrongly be reintroduced?

Will come with progress on #4404

smowton · 2019-04-17T08:41:09Z

src/goto-checker/properties.cpp

 propertiest initialize_properties(const abstract_goto_modelt &goto_model)
 {
  propertiest properties;
+  update_properties_from_goto_model(properties, goto_model);


@tautschnig I believe this might be the resolution to your complain about check-properties code being deleted? (perhaps these two commits should be merged?)

"check-properties code being deleted" - what is this about?

Where you said "incremental_goto_checker is already doing that."

smowton

Thankyou, this factors the symex-driven stuff much better than I managed back when I first wrote this!

reduces code duplication

removes indent

set_properties has no return value.

reduces code duplication

is unreachable

With symex-driven-lazy-loading there might not be any properties initially. Incremental_goto_checker is already doing that check anyway.

With symex-driven-lazy-loading we know the full set of properties only after goto-symex has finished.

Only use options after cmdline has been parsed into options.

goes now through goto-checker classes instead of bmct/all_propertiest.

reduces indentation

These have now been entirely replaced by goto-checker.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f96818d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108667061
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, pkesseli, smowton and tautschnig as code owners April 16, 2019 12:42

peterschrammel force-pushed the goto-checker-symex-driven branch from 1d7c902 to aa3dda9 Compare April 16, 2019 17:20

allredj reviewed Apr 16, 2019

View reviewed changes

peterschrammel added the Goto-checker label Apr 16, 2019

tautschnig changed the title ~~Symex-driven lazy loading uses goto-checker~~ Symex-driven lazy loading uses goto-checker [blocks: #2212] Apr 17, 2019

tautschnig added the blocker label Apr 17, 2019

tautschnig approved these changes Apr 17, 2019

View reviewed changes

tautschnig assigned smowton and peterschrammel Apr 17, 2019

smowton reviewed Apr 17, 2019

View reviewed changes

smowton approved these changes Apr 17, 2019

View reviewed changes

peterschrammel added 12 commits April 17, 2019 09:50

Deduplicate show_loaded_X

4b4f2d1

reduces code duplication

Remove unnecessary block scopes

ffc9710

removes indent

Clean up set_properties helper method

014b9da

set_properties has no return value.

Generalize get_goto_model for symex-driven lazy loading

f08a238

reduces code duplication

Fallback to old bmct is unnecessary

807451d

is unreachable

Fix typo

b02de78

Has_properties check must be in incremental_goto_checker

13c1f76

With symex-driven-lazy-loading there might not be any properties initially. Incremental_goto_checker is already doing that check anyway.

Update properties from goto model

061d1b6

With symex-driven-lazy-loading we know the full set of properties only after goto-symex has finished.

Use options instead of cmdline

400c354

Only use options after cmdline has been parsed into options.

Symex-driven lazy loading uses goto-checker

8cc0c35

goes now through goto-checker classes instead of bmct/all_propertiest.

Remove unnecessary block scope

4072e8b

reduces indentation

Remove obsolete bmc.cpp and all_properties.cpp

028aadd

These have now been entirely replaced by goto-checker.

peterschrammel added 2 commits April 17, 2019 09:56

Purge docs references to bmct

8454539

Use macros of exit codes in JBMC

f96818d

peterschrammel force-pushed the goto-checker-symex-driven branch from 1ce9697 to f96818d Compare April 17, 2019 08:56

allredj reviewed Apr 17, 2019

View reviewed changes

peterschrammel merged commit 6c8954b into diffblue:develop Apr 17, 2019

peterschrammel deleted the goto-checker-symex-driven branch April 17, 2019 12:52

tautschnig mentioned this pull request Apr 17, 2019

Revert "property_checkert interface" #2212

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

peterschrammel commented Apr 16, 2019 •

edited

Loading

allredj left a comment

allredj left a comment

tautschnig Apr 17, 2019

tautschnig Apr 17, 2019

smowton Apr 17, 2019

smowton Apr 17, 2019

tautschnig Apr 17, 2019

tautschnig Apr 17, 2019

peterschrammel Apr 17, 2019

tautschnig Apr 17, 2019

peterschrammel Apr 17, 2019

smowton Apr 17, 2019

peterschrammel Apr 17, 2019

tautschnig Apr 17, 2019

peterschrammel Apr 17, 2019

smowton left a comment

allredj left a comment

Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

Symex-driven lazy loading uses goto-checker [blocks: #2212] #4541

Conversation

peterschrammel commented Apr 16, 2019 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Apr 16, 2019 •

edited

Loading