Skip to content

Error Localization

Jump to bottom
Matthias Heizmann edited this page May 15, 2017 · 47 revisions

More types of statements

Should we handle assume statements separately?

Suppose we have an assume statement

image

To check if the assume statement is relevant or not, our algorithm checks if the following triple is unsatisfiable:

image

I think the triple will always be unsatisfiable, but the assume statement is never in the unsatisfiable core and hence never marked as relevant in our implementation.
Possible Solution:
Maybe we don't need to consider the relevancy of an assume statement . We should consider the branch after the assume statement. If the branch is relevant, then the assume statement is relevant.

Another possible criteria to determine the relevancy of an assume statement is :
image is relevant if replacing this assume statement with image (else) and the corresponding else branch does not lead us to the error anymore

2017-05-17 Discussion assume statements

  • do not try to find relevance criterion for assume statements
  • our analysis finds "only" error relevant value assignments
  • in a trace we cannot pinpoint the assume statement that causes the error -- the programmer could always introduce an assume false and the error would not be reachable on this trace
  • we take control flow structure of program as given and find only "faulty assignments"
  • TODO find good arguments (maybe in related work) why we do not analyze assumes

Call/return statements?

TODO check examples (better small ones with procedure calls, probably SV-COMP benchmarks form subcategory/folder recursive)

Comparison to related work

  • Do others also consider assume statements?
  • Why do we replace assignments by havoc and not by skip?
    One example why we need it: x:=7; x:=7; assert x!=7; (TODO: more convincing example)

Several error traces

Should we consider several error traces?

How?

Proof of correctness of our Algorithm

We proved that if an assignment statement Pi[i] of the form x:=t at position i is relevant then P => WP(Q, havoc(x)) does not hold. Where Q = not WP(false; pi[i+1, n]) and P = not WP(false; pi[i,n]).
But the way our algorithm actually works is, it checks if the hoare triple {P} pi[i] {Q} is valid (that is the triple (P, pi[i], -Q) is unsatisfiable ) and it checks if the statement x:=t is in the unsatisfiable core. If yes, then the statement is marked as relevant.

In case of the havoc statement, our algorithm checks if the hoare triple is satisfiable. If yes, then the havoc is relevant.

Add 2 lemmas stating:

  • If pi[i] is an assignment statement of the formx := t and the hoare triple {P} pi[i] {Q} is unsatisfiable and pi[i] is in the unsatisfiable core, then P => WP(Q, havoc(x)) does not hold.

  • if pi[i] is a havoc statement of the form havoc(x) and the hoare triple {P} pi[i] {Q} is satisfiable then P => WP(Q, havoc(x)) does not hold.

No need to state the lemmas. Just a paragraph explaining how we do it in practice

Skeleton for the paper

Terminology

(my email form 2017-02-14) How should we call the "normal" relevancy and the "Golden Frame" relevancy?

Some preliminary ideas.

  • "Assignment Relevancy" and "Havoc Relevancy"
  • "Restrictive Relevancy" and "Relaxing Relevancy"
  • "Input Relevancy"
  • Something that does not have "Relevancy" in its name.
  • "Error Enforcing" and "Error Admitting"
  • "Error Supporting"
  • "Error Fostering"
  • Something related to "Security"

Security Analysis

  • When is a bug a security bug?
  • One possible answer: When some (or only the last?) function whose result is influenced by user/network has the @ symbol. (Means that specific user input can trigger bug)

One task: Check the trunk/examples/programs/toy/faultlocalization/vadim/ examples that Vadim Mutilin form the Linux Verification Center has sent to us.

Improve Performance

Find bottlenecks in analysis of large counterexamples. Matthias: The bottleneck for the LDV examples seems to be the array quantifier elimination during the computation of WP for summaries (resp. the return statements).

  • The array quantifier elimination can be improved significantly (note for MH: explicit index-value comparison instead of simplifyDDA postprocessing).
  • Compute WP without explicit summaries (note for MH: use symbolic summary for return, compute preliminary WP up to call, instanciate symbolic summary, obtain final WP via post-processing).
Clone this wiki locally