Integrate fault localizer into goto checker [blocks: 4215] #3970

peterschrammel · 2019-01-27T23:18:27Z

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

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

tautschnig · 2019-02-19T00:04:08Z

src/goto-checker/report_util.cpp

+  {
+    log.debug() << score_pair.first->source_location
+                << "\n  score: " << score_pair.second << messaget::eom;
+  }


Use messaget::conditional_output to avoid doing a lot of work when it most likely won't be of any value.

tautschnig · 2019-02-19T00:08:55Z

src/goto-checker/goto_symex_fault_localizer.cpp

+    log.status() << "Localizing fault" << messaget::eom;
+
+    // pick localization method
+    //  if(options.get_option("localize-faults-method")=="TBD")


I suppose this is copy&paste?

Yes, I am inclined to remove this option altogether as nobody has ever implemented any alternative method in 3 years.

tautschnig · 2019-02-19T00:10:17Z

src/goto-checker/goto_symex_fault_localizer.cpp

+  if(solver() == decision_proceduret::resultt::D_SATISFIABLE)
+    return false;
+
+  return true;


return solver() != decision_proceduret::resultt::D_SATISFIABLE;

tautschnig · 2019-02-19T00:12:07Z

src/goto-checker/goto_symex_fault_localizer.cpp

+  v.resize(localization_points.size());
+
+  for(std::size_t i = 0; i < localization_points.size(); ++i)
+    v[i] = tvt(tvt::tv_enumt::TV_UNKNOWN);


localization_points_valuet v(localization_points.size(), tvt::unknown());

smowton · 2019-02-19T09:32:04Z

src/goto-checker/report_util.cpp

+{
+  PRECONDITION(!fault_location.scores.empty());
+
+  auto max_it = fault_location.scores.begin();


Use std::max and a comparator?

smowton · 2019-02-19T09:36:32Z

src/goto-checker/goto_symex_fault_localizer.cpp

+    {
+      l.second->second++;
+    }
+    else if(solver.l_get(l.first).is_false() && l.second->second > 0)


l.second->second is a bit opaque -- comment on what that is?

smowton · 2019-02-19T09:38:13Z

src/goto-checker/all_properties_verifier_with_fault_localization.h

+        if(properties.at(property_id).status == property_statust::FAIL)
+        {
+          // get correctly truncated error trace for property and store it
+          (void)traces.insert(


Are these both expected to be insert-new-key? If so suggest cross-checking with a CHECK_RETURN that they are indeed new.

(If not, suggest inserting a dummy value and only calling the expensive build / localize functions if they really are new)

I've added an invariant in the trace storage.

Make sure a failed property only occurs once in updated_properties so that storing its trace is only attempted once.

Utility function to freeze all guards, as e.g. needed for fault localization.

Print information about the likely fault location.

Can be implemented by an incremental goto checker to provide information about the likely fault location.

Requires prop_convt, symex_target_equationt and frozen guards.

Uses goto_symex_fault_localizert to provide the functionality.

Variant that reports fault localization information.

Available by using multi-path symex checker

peterschrammel added work in progress do not review dependent - do not merge Goto-checker labels Jan 27, 2019

peterschrammel self-assigned this Jan 27, 2019

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, NathanJPhillips, pkesseli, smowton, tautschnig and thk123 as code owners January 27, 2019 23:18

tautschnig changed the title ~~[WIP] Integrate fault localizer into goto checker [depends: 3968]~~ [WIP] Integrate fault localizer into goto checker Feb 2, 2019

tautschnig added Needs rebase and removed dependent - do not merge labels Feb 2, 2019

peterschrammel force-pushed the fault-localizer branch from 9476ab3 to 2ca57a4 Compare February 17, 2019 14:38

peterschrammel changed the title ~~[WIP] Integrate fault localizer into goto checker~~ Integrate fault localizer into goto checker Feb 17, 2019

peterschrammel removed Needs rebase do not review work in progress labels Feb 17, 2019

peterschrammel force-pushed the fault-localizer branch 2 times, most recently from dc881ce to eca9530 Compare February 18, 2019 21:21

allredj reviewed Feb 18, 2019

View reviewed changes

peterschrammel mentioned this pull request Feb 18, 2019

Remove obsolete cbmc/fault_localization [blocks: 4216] #4215

Merged

7 tasks

peterschrammel added the blocker label Feb 18, 2019

peterschrammel changed the title ~~Integrate fault localizer into goto checker~~ Integrate fault localizer into goto checker [blocks: 4215] Feb 18, 2019

tautschnig approved these changes Feb 19, 2019

View reviewed changes

tautschnig assigned smowton Feb 19, 2019

smowton reviewed Feb 19, 2019

View reviewed changes

peterschrammel unassigned smowton Feb 19, 2019

peterschrammel force-pushed the fault-localizer branch from eca9530 to 469c522 Compare February 19, 2019 18:10

peterschrammel added 12 commits February 19, 2019 19:03

Add invariant for avoiding duplicated error traces

d575d5f

Make sure a failed property only occurs once in updated_properties so that storing its trace is only attempted once.

Add freeze_guards to bmc_util

f072391

Utility function to freeze all guards, as e.g. needed for fault localization.

Add const version for returning last trace step

560b720

Add fault localization output functions

123280a

Print information about the likely fault location.

Add fault localization provider interface

8aab418

Can be implemented by an incremental goto checker to provide information about the likely fault location.

Fault localizer for goto-symex

8d01d81

Requires prop_convt, symex_target_equationt and frozen guards.

Make multi-path symex checker a fault localization provider

b436150

Uses goto_symex_fault_localizert to provide the functionality.

All properties verifier with fault localization

80f1ee8

Variant that reports fault localization information.

Stop-on-fail verifier with fault localization

feb8bcb

Variant that reports fault localization information.

Use goto verifier for fault localization in CBMC

19f2cec

Available by using multi-path symex checker

Use goto verifier for fault localization in JBMC

28435fe

Available by using multi-path symex checker

Remove unused localize-faults-method option

b1d9072

peterschrammel force-pushed the fault-localizer branch from 469c522 to b1d9072 Compare February 19, 2019 19:05

peterschrammel assigned smowton and unassigned peterschrammel Feb 20, 2019

smowton approved these changes Feb 20, 2019

View reviewed changes

peterschrammel merged commit f4dedec into diffblue:develop Feb 20, 2019

peterschrammel deleted the fault-localizer branch February 20, 2019 17:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Integrate fault localizer into goto checker [blocks: 4215] #3970

Integrate fault localizer into goto checker [blocks: 4215] #3970

Uh oh!

peterschrammel commented Jan 27, 2019 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

tautschnig Feb 19, 2019

Uh oh!

tautschnig Feb 19, 2019

Uh oh!

peterschrammel Feb 19, 2019

Uh oh!

tautschnig Feb 19, 2019

Uh oh!

tautschnig Feb 19, 2019

Uh oh!

smowton Feb 19, 2019

Uh oh!

smowton Feb 19, 2019

Uh oh!

smowton Feb 19, 2019

Uh oh!

smowton Feb 19, 2019

Uh oh!

peterschrammel Feb 19, 2019

Uh oh!

Uh oh!

Integrate fault localizer into goto checker [blocks: 4215] #3970

Integrate fault localizer into goto checker [blocks: 4215] #3970

Uh oh!

Conversation

peterschrammel commented Jan 27, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

Uh oh!

peterschrammel commented Jan 27, 2019 •

edited

Loading