theyoucheng / cbmc Goto Github PK
View Code? Open in Web Editor NEWThis project forked from diffblue/cbmc
C Bounded Model Checker
Home Page: http://www.cprover.org/cbmc
License: Other
This project forked from diffblue/cbmc
C Bounded Model Checker
Home Page: http://www.cprover.org/cbmc
License: Other
Currently, it appears that some line numbers are reported multiple times with different suspicious levels in the final report of fault localization. Only the one with the highest faulty probability is due to be there.
The fault localization procedure is implemented based on the "incremental" branch of CBMC, which for now does not support "--beautify".
I noticed that FCBMC was running a touch slowly on one of the simplest benchmarks when compared to CBMC (insertion_sort_safe.c : FCBMC = 14 secs, CBMC = 0.6 secs) - especially given the final matrix included only 4 traces - so I began investigating why...
It seems as if the implementation is often calling the model checker to return traces which execute the same LOC as a previous trace returned by it, but differ insofar as the number of unwindings executed differ. Then, in the final simplified coverage matrix the data about these traces are then completely deleted. This can potentially be highly inefficient - for instance in the below example 14 traces are generated but only 4 are used in our actual analysis, which means that most of the traces should not be called for in the first place by the model checker.
In general (and following the implementation described in my thesis), the specified implementation of the single bug optimal data generation algorithm should only ever call the model checker in order to find a new trace which is different to all previous traces generated - where different means different in terms of LOC executed in the original faulty benchmark version (importantly - different does not mean different in terms of LOC executed in the unwound version!). In other words, it should never be possible to call the model checker and it return a trace which executes the same LOC as a trace which was previously returned by it.
The command and output is as follows:
cbmc insertion_sort_unsafe.c --incremental --stop-on-fail --unwind 4 --localize-faults --localize-faults-method sbo --localize-faults-max-display 100 --verbosity 0yes, got a failing trace
failing traces:
1 1 1 1 1 1 1 1 1 0 0 0 0 1 0 0 0 1 0 1 1
1 0 1 1 1 1 1 1 1 0 0 0 0 1 0 0 0 1 0 1 1
1 0 1 1 0 1 1 1 0 0 0 0 0 1 0 0 0 1 0 1 1
1 0 0 1 0 1 1 1 0 0 0 0 0 1 0 0 0 1 0 1 1
passing traces:
1 0 1 1 1 1 1 1 0 0 1 0 0 1 0 1 0 1 0 1 1
1 0 1 1 0 1 1 1 0 0 1 0 0 1 0 1 0 1 0 1 1
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1
s traces:
1 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1
1 1 1 1 0 1 1 1 0 0 1 0 0 1 0 1 0 1 0 1 1
1 1 1 1 1 1 1 1 0 0 1 0 0 1 0 1 0 1 0 1 1
1 1 1 1 0 1 1 1 1 0 1 0 0 1 0 1 0 1 0 1 1
1 0 1 1 0 1 1 1 1 0 1 0 0 1 0 1 0 1 0 1 1
1 0 1 1 1 1 1 1 1 0 1 0 0 1 0 1 0 1 0 1 1
1 1 1 1 1 1 1 1 1 0 1 0 0 1 0 1 0 1 0 1 1
1 0 0 1 0 1 1 0 0 1 1 1 0 1 0 1 0 1 0 1 1
*** after simplification (blocks) ***
[1] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 15 function main ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 21 function main
[3] ##file insertion_sort_unsafe.c line 18 function main ##file insertion_sort_unsafe.c line 19 function main
[4972] ##file insertion_sort_unsafe.c line 17 function main
[47627] ##file insertion_sort_unsafe.c line 23 function main ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[true] ##file insertion_sort_unsafe.c line 10 function main
failing traces:
1 1 1 1 1
passing traces:
1 1 1 1 1
1 0 0 1 1
1 1 0 1 1
after compute spectra
**ef:
1 1 1 1 1
**ep:
3 2 1 3 3
**nf:
0 0 0 0 0
**np:
0 1 2 0 0
after measure_sb
0.25 0.5 0.75 0.25 0.25
** Most likely fault location:
Fault localization scores:
[__VERIFIER_assert.assertion.1]: Single Bug Optimal Fault Localization
[score: 0.75] ##file insertion_sort_unsafe.c line 17 function main
[score: 0.5] ##file insertion_sort_unsafe.c line 18 function main ##file insertion_sort_unsafe.c line 19 function main
[score: 0.25] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 15 function main ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 21 function main
[score: 0.25] ##file insertion_sort_unsafe.c line 23 function main ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[score: 0.25] ##file insertion_sort_unsafe.c line 10 function main
Just leaving the installation instructions here (no issue)...
git clone https://github.com/theyoucheng/cbmc cbmc && cd cbmc && git checkout fault-localization-incr && cd src && make minisat2-download && make
cd cbmc && cd src && git pull origin fault-localization-incr && make
There seem to be two errors when I run the following command on the given program (which I'll email you shortly)
cbmc insertion_sort_unsafe.c --incremental --stop-on-fail --unwind 4 --localize-faults --localize-faults-method sbo --localize-faults-max-traces 20 --localize-faults-max-display 100 --verbosity 0 --slice-formula
The output is as follows:
*** after simplification (blocks) ***
[1] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 21 function main
[3] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[206] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 21 function main
[208] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[3068] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[3941] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 21 function main
[3943] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 17 function main
[15803] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[15875] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[47491] ##file insertion_sort_unsafe.c line 23 function main ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[115911] ##file insertion_sort_unsafe.c line 23 function main ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[115994] ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[true] ##file insertion_sort_unsafe.c line 10 function main ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 23 function main
failing traces:
1 1 1 1 1 1 1 1 0 1 1 1 1
1 0 1 1 0 1 1 1 0 1 1 1 1
1 0 1 0 0 1 1 1 1 1 1 1 1
1 1 1 0 0 1 1 1 0 1 1 1 1
1 0 1 0 0 1 1 1 0 1 1 1 1
1 0 1 1 1 1 1 1 0 1 1 1 1
1 0 1 1 1 1 1 1 1 1 1 1 1
1 1 1 1 1 1 1 1 1 1 1 1 1
1 1 1 1 0 1 1 1 1 1 1 1 1
1 0 1 1 0 1 1 1 1 1 1 1 1
1 1 1 1 0 1 1 1 0 1 1 1 1
1 1 1 0 0 1 1 1 1 1 1 1 1
passing traces:
1 0 1 0 0 1 1 1 0 1 1 1 1
1 0 1 0 0 0 0 0 0 1 1 0 1
0 0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 1 0 0 1
1 1 1 0 0 0 0 0 0 1 1 0 1
1 1 1 1 1 1 1 1 0 1 1 1 1
1 0 1 1 1 1 1 1 0 1 1 1 1
1 1 1 1 0 1 1 1 0 1 1 1 1
1 1 1 0 0 1 1 1 0 1 1 1 1
1 1 1 1 1 1 1 0 0 1 1 1 1
1 1 1 0 0 1 0 0 0 1 1 1 1
1 1 0 0 0 0 0 0 0 1 0 0 1
1 1 1 1 0 1 0 0 0 1 1 1 1
1 0 1 1 0 1 0 0 0 1 1 1 1
after compute spectra
**ef:
12 6 12 8 4 12 12 12 6 12 12 12 12
**ep:
13 8 11 6 3 9 6 5 0 13 11 9 14
**nf:
0 6 0 4 8 0 0 0 6 0 0 0 0
**np:
1 6 3 8 11 5 8 9 14 1 3 5 0
after measure_sb
11.1333 5.46667 11.2667 7.6 3.8 11.4 11.6 11.6667 6 11.1333 11.2667 11.4 11.0667
** Most likely fault location:
Fault localization scores:
[__VERIFIER_assert.assertion.1]: Single Bug Optimal Fault Localization
[score: 11.6667] ##file insertion_sort_unsafe.c line 16 function main ##file insertion_sort_unsafe.c line 18 function main
[score: 11.6] ##file insertion_sort_unsafe.c line 17 function main
[score: 11.4] ##file insertion_sort_unsafe.c line 13 function main ##file insertion_sort_unsafe.c line 14 function main ##file insertion_sort_unsafe.c line 21 function main
[score: 11.4] ##file insertion_sort_unsafe.c line 24 function main ##file insertion_sort_unsafe.c line 3 function __VERIFIER_assert
[score: 11.2667] ##file insertion_sort_unsafe.c line 23 function main
[score: 11.0667] ##file insertion_sort_unsafe.c line 10 function main
The errors are as follows:
Unless I've missed something here, Line 17 is executed just in case line 16 is (the conditional expression is executed just in case its body is), and so the suspiciousness should be the same - this is not the case however given the first two reports of the fault localisation scores report the body as having different scores (impossible if they always execute together). Note that correcting this will also mean sbo performs better by putting the bug in top equal place.
Each line of code should only refer to one column in the finalised matrix. This is not the case for lines 16 and 23 for example. This property is essential for the correct functioning of the measures (in particular pfl). The correct specification for the matrix is as follows: for each row in the matrix, a line of code should have a 1/0 in that row just in case that line of code was executed at some (any) point during the execution which in turn corresponds to that row.
cbmc cs_read_write_lock_false.c --unwind 200
detects the failure in the program, however, if we run the same verification with "--incremental" option, it returns "verification successful":
cbmc cs_read_write_lock_false.c --incremental --stop-on-fail --unwind 200
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.