Multi-path symex-only checker [blocks: 3795] #3794

peterschrammel · 2019-01-13T18:25:10Z

Based on #3585, only review last 4 commits

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.

src/cbmc/cbmc_parse_options.cpp

tautschnig · 2019-01-13T20:54:47Z

src/goto-checker/multi_path_symex_only_checker.cpp

+      get_memory_model(options, ns);
+    memory_model->set_message_handler(ui_message_handler);
+    (*memory_model)(equation);
+  }


I don't think this is of any use for this checker?

It won't have any impact on the property status, but I'd like still want to see the entire SSA.

Yes, but doing unnecessary work should at least be explicitly documented via comments.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 8253fa4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97176111

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b197d35).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97179981

tautschnig · 2019-01-14T08:47:03Z

The depended-on PRs have been merged, this needs a rebase and possibly further work to make CI pass.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 7bf4d12).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97960133

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2061df5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97972656

smowton · 2019-01-21T13:57:33Z

src/goto-checker/bmc_util.cpp

+    }
+    else
+    {
+      property_infot &property_info = properties.at(property_id);


Repeated lookup should probably be replaced with

auto emplace_result = properties.emplace( property_id, property_infot{step.source.pc, step.comment, status}); if(emplace_result.second) { ... } else { property_infot &property_info = emplace_result.first->second; ... }

smowton · 2019-01-21T14:03:41Z

src/goto-checker/bmc_util.cpp

+
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::NOT_CHECKED)


Is there a chance the status was PASS before the loop above changed it to NOT_CHECKED, and therefore we might spuriously note it as changed? I think that can't happen because it's hard to imagine that |=result with either UNKNOWN or PASS on the RHS would turn PASS -> NOT_CHECKED, but just want to check I've understood.

No, cannot happen. |= is supposed to be monotonic, i.e. once you have a PASS, you cannot go back to something undetermined anymore.

smowton · 2019-01-21T14:04:19Z

src/goto-checker/bmc_util.h

  const optionst &,
  ui_message_handlert &);

+/// Sets property status to PASS or FAIL for properties whose


Does it? It appears to only set properties to PASS

smowton · 2019-01-21T14:07:30Z

jbmc/src/java_bytecode/java_multi_path_symex_only_checker.cpp

+  : multi_path_symex_only_checkert(options, ui_message_handler, goto_model)
+{
+  // unwinds <clinit> loops to number of enum elements
+  if(options.get_bool_option("java-unwind-enum-static"))


Maybe factor this code with the identical code in jbmc?

Factored out into separate file. The instance of the code in jbmc_parse_options will disappear with the do_language_agnostic_bmc call.

They are not inlined using goto_partial_inline anymore.

Updates the property infos with properties created by goto-symex and sets the status of already determined properies.

multi_path_symex_only_checkert is a bounded model checking algorithm that determines the status of properties through symbolic execution and constant propagation. I.e. it doesn't call the SAT solver. If desired CBMC could expose this to support a symex-only BMC algorithm. For now, this is used to implement show-vcc and program-only (which are rather orthogonal to the BMC algorithm used, but currently assume symex-only).

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 3809454).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98183898
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, pkesseli, smowton and tautschnig as code owners January 13, 2019 18:25

peterschrammel added the dependent - do not merge label Jan 13, 2019

peterschrammel mentioned this pull request Jan 13, 2019

Multi-path symex checker [blocks: 3796] #3795

Merged

7 tasks

peterschrammel changed the title ~~Multi path symex-only checker [depends: 3585]~~ Multi-path symex-only checker [depends: 3585, blocks: 3795] Jan 13, 2019

peterschrammel added Goto-checker blocker labels Jan 13, 2019

peterschrammel force-pushed the multi-path-symex-only-checker branch from b322f1e to 8253fa4 Compare January 13, 2019 20:31

peterschrammel commented Jan 13, 2019

View reviewed changes

src/cbmc/cbmc_parse_options.cpp Outdated Show resolved Hide resolved

tautschnig reviewed Jan 13, 2019

View reviewed changes

allredj reviewed Jan 13, 2019

View reviewed changes

peterschrammel force-pushed the multi-path-symex-only-checker branch from 8253fa4 to b197d35 Compare January 13, 2019 22:45

allredj reviewed Jan 13, 2019

View reviewed changes

peterschrammel force-pushed the multi-path-symex-only-checker branch from b197d35 to ac60c6c Compare January 14, 2019 00:47

tautschnig changed the title ~~Multi-path symex-only checker [depends: 3585, blocks: 3795]~~ Multi-path symex-only checker [blocks: 3795] Jan 14, 2019

tautschnig removed the dependent - do not merge label Jan 14, 2019

tautschnig assigned peterschrammel Jan 14, 2019

tautschnig changed the title ~~Multi-path symex-only checker [blocks: 3795]~~ Multi-path symex-only checker [depends-on: 3585, blocks: 3795] Jan 14, 2019

tautschnig added the dependent - do not merge label Jan 14, 2019

tautschnig removed the dependent - do not merge label Jan 14, 2019

tautschnig changed the title ~~Multi-path symex-only checker [depends-on: 3585, blocks: 3795]~~ Multi-path symex-only checker [blocks: 3795] Jan 14, 2019

peterschrammel force-pushed the multi-path-symex-only-checker branch 3 times, most recently from a6bb072 to 92f74e4 Compare January 14, 2019 12:12

peterschrammel requested review from NathanJPhillips and thk123 as code owners January 20, 2019 15:17

peterschrammel force-pushed the multi-path-symex-only-checker branch 2 times, most recently from 1f510d2 to 7bf4d12 Compare January 20, 2019 16:01

peterschrammel added dependent - do not merge and removed do not merge labels Jan 20, 2019

peterschrammel changed the title ~~Multi-path symex-only checker [blocks: 3795]~~ Multi-path symex-only checker [depends: 3860, blocks: 3795] Jan 20, 2019

allredj reviewed Jan 20, 2019

View reviewed changes

peterschrammel force-pushed the multi-path-symex-only-checker branch from 7bf4d12 to 2061df5 Compare January 20, 2019 23:02

peterschrammel changed the title ~~Multi-path symex-only checker [depends: 3860, blocks: 3795]~~ Multi-path symex-only checker [blocks: 3795] Jan 20, 2019

peterschrammel removed dependent - do not merge work in progress labels Jan 20, 2019

allredj reviewed Jan 21, 2019

View reviewed changes

peterschrammel assigned smowton and thk123 Jan 21, 2019

smowton reviewed Jan 21, 2019

View reviewed changes

peterschrammel force-pushed the multi-path-symex-only-checker branch from 2061df5 to ad11373 Compare January 21, 2019 23:31

smowton approved these changes Jan 22, 2019

View reviewed changes

peterschrammel added 7 commits January 22, 2019 13:50

Do collect properties from inlined functions

ef0f093

They are not inlined using goto_partial_inline anymore.

Allow UNKNOWN as neutral element in property status updates

661a39c

Add properties_result_from_symex_target_equation

c3e5f4e

Updates the property infos with properties created by goto-symex and sets the status of already determined properies.

Use goto verifier for program-only and show-vcc in CBMC

f1c6488

Goto checkers for Java require further preprocessing

1b8f38b

Use goto verifier for program-only and show-vcc in JBMC

3809454

peterschrammel force-pushed the multi-path-symex-only-checker branch from ad11373 to 3809454 Compare January 22, 2019 13:50

allredj reviewed Jan 22, 2019

View reviewed changes

peterschrammel merged commit f23f4f3 into diffblue:develop Jan 22, 2019

peterschrammel deleted the multi-path-symex-only-checker branch January 22, 2019 16:33

Multi-path symex-only checker [blocks: 3795] #3794

Multi-path symex-only checker [blocks: 3795] #3794

Uh oh!

Conversation

peterschrammel commented Jan 13, 2019

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 14, 2019

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!

peterschrammel Jan 21, 2019 • 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

peterschrammel Jan 21, 2019 •

edited

Loading