[ldv-project] Benchmarking new predicate analysis with UFs
Mikhail Mandrykin
mandrykin at ispras.ru
Mon Aug 26 20:16:33 MSK 2013
Hello!
Here are the results of benchmarking four configurations of CPAchecker with
predicate analysis (with variables and with with UFs) on the ldv-regression,
heap-manipulation, bitvector and Device Drivers 64 categories.
The message is also attached as report.txt.
== The configurations ==
-- Predicate analysis with real variables and recursion skipping.
Just as config/predicateAnalysis-PredAbsRefiner-ABEl.properties with
# Recursion skipping
analysis.summaryEdges=true
analysis.functionPointerCalls=true
cpa.callstack.skipRecursion=true
-- Predicate analysis with bit-vector variables and recursion skipping.
The same as the previous configuration, but with
# Turn on bit-vectors
cpa.predicate.replaceBitvectorWithRationalAndFunctionTheory = false
cpa.predicate.ignoreExtractConcat=false
# Turn on field aliasing
cpa.predicate.handlePointerAliasing = true
cpa.predicate.handleFieldAliasing = true
cpa.predicate.handleFieldAccess = true
# Using 32-bit Linux machine model
analysis.machineModel = LINUX32
-- Predicate analysis with bit-vector uninterpreted functions
(UFs from bit-vectors to bit-vectors). This is the new configuration
employing the
analysis currently implemented in the pointer-predicates branch of
git://forge.ispras.ru/cpachecker.git. The same as the previous configuration
with
# Excluding malloc, __kmalloc and kzalloc from nondet functions
# The analysis treats them as memory allocating functions instead
cpa.predicate.nondetFunctions = {"sscanf", "random"}
# Options enabling preliminary CFA transformations required by the analysis
with UF
# The transformations are rather simple and described further
cfa.simplifyPointerExpressions = false
cfa.transformUnsizedArrays = true
cfa.transformPointerArithmetic = true
cfa.transformArrows = true
cfa.transformStarAmper = true
cfa.transformFunctionPointers = true
cfa.ignoreConst=true
cfa.ignoreVolatile=true
# Options enabling PathFormulaWithUF and the usage of the
# appropriate address disjointness constraints
cpa.predicate.pointerAnalysisWithUFs = true
cpa.predicate.refinement.pointerAnalysisWithUFs = true
This configuration is based on file
config/predicateAnalysis-PredAbsRefiner-ABEl-UF.properties in the pointer-
predicates branch.
-- Predicate analysis with real uninterpreted functions (UFs from reals to
reals). This is the same as the previous
configuration, but with
# Turn off bit-vectors
cpa.predicate.replaceBitvectorWithRationalAndFunctionTheory = true
cpa.predicate.ignoreExtractConcat=true
This configuration is based on file
config/predicateAnalysis-PredAbsRefiner-ABEl-UF-replace.properties in the
pointer-predicates branch.
== The results ==
-- ldv-regression category. Attached as ldv-regression-table.html. This also
includes fixed manual tests submitted this year
(some of the tests were originally incorrect).
Overall in this category in comparison with the variable-based analysis
the new analysis wins 204 points for the real and 161 points for the
bit-vector case correspondingly.
The timeouts on ex3_forlist.c_safe.cil.c and ex3_forlist.c_safe.i for the BV
case
are caused by huge interpolants derived from the formulas
involving essential arithmetics (addition, subtraction, multiplication). The
interpolants contain
many constraints on the single bits extracted from bit-vector variable values.
These interpolants seem to blow up
in (de)instantiation.
The parsing failures are spurious (I just accidentally included some original
files in the benchmark).
The exceptions on test23_safe.c, test24_safe.c and test27_safe.c (the BV case)
are MathSAT failures (in fails on ab-mixed terms
encountered in the unsatisfiability proof).
The false UNSAFEs on test29_safe.c, test_union.c_safe_1.cil.c, and
test_union.c_safe_1.i arise because of the current union fields
encoding. In case the union is not shared (its address hasn't been taken yet
anywhere on the path),
the union fields are encoded just as separate
variables. So their values are treated as independent. But even in case the
union turns out to be shared
(addressed or dynamically allocated), its different-typed fields are encoded
with different UFs, so their values are still independent,
though they can share the same memory address. Currently I have some thoughts
about implementing support for assignments to unions by
explicitly assigning the right hand side to every field of the union with the
appropriate type-conversions, but still putting it off
because of the complications in the general case when a union can contain
structures, arrays and other unions in itself.
-- heap-manipulation category. Attached as heap-manipulation-table.html.
Overall in this category the new analysis currently looses 10 points in the BV
case and 5 points in the real case.
On non-cillified files both BV and real configurations time out on SAFE
benchmarks and give UNSAFEs verdicts
for their UNSAFE counterparts except in the two cases.
On bubble_sort_linux_unsafe.i the analysis loops infinitely in the successive
refinements before reaching the actual error location.
On dll_of_dll_safe.i the loss of precision because of typing heuristic occurs.
In dll_create_generic() the variable dll of type (void*)
is declared. Its address passed to either dll_insert_slave() or
dll_insert_master() called by function pointer. But the functions
actually take arguments of either (struct slave_item **) or (struct
master_item **). So they assign the value to the dll variable using
the UFs for types (struct slave_item *) or (struct master_item *). Then the
caller function dll_create_generic() returns the value of
dll dereferencing it as a value of type (void *) and thus assumes its value to
be arbitrary. This is rather a fundamental limitation of
the new analysis which can be partially addressed by assuming all possible
actual types for each (void *) type encountered.
It seems that all false UNSAFEs on the cillified files are caused by the
transformation of memory allocations, e.g:
struct sth *psth = (struct sth*) malloc(sizeof(struct sth));
-->
unsigned int tmp_0 = 16U; // size of (struct sth) computed and substituted by
CIL
void *tmp_1 = malloc(tmp_0);
psth = (struct sth*) tmp_1;
After such transformation the malloc() is not properly recognized and the
corresponding memory locations aren't properly tracked,
which leads to the loss of precision. This transformation is currently
disabled by the CIL options we use in LDV so it shouldn't
be frequently encountered in our new benchmarks.
Meanwhile on the SAFE benchmarks the analysis discovers predicates for the
linked lists up to the depth of 10 in about 30 seconds.
-- Device Drivers 64 category (partial). Attached as dd64-table.html
In this category I have only analyzed single-file non-cillified drivers.
Overall in this category the new analysis looses 6 points in the real case and
the results for the BV case are too strange because
the variable-based analysis failed on too many benchmarks. Though I know we've
already tried bit-precise analysis on the drivers and
haven't got so many UNKNOWNs. It seems due to the non-cillified filed being
used, which turned out to be poorly supported by the
bit-precise configuration.
I haven't investigated the results in detail yet. Also it turned out that
preliminary predicate extraction heuristic has significant
influence on the results in this category (I first launched the new analysis
without this heuristic
and got 26 correct results instead of 29).
-- Bit vectors. Attached as bitvector-table.html
The table only contains results for BV configurations. It just shows that the
results in this category don't differ significantly.
I have also launched the new analysis on the both subcategories of the Control
Flow Integer set. I haven't done thorough
comparison (used small time and memory limits and only cared about the
failures), but the analysis gives too many false UNSAFEs
for the ssh/* part of the memsimple subcategory, while the ntdrivers/*
verdicts match.
== The implementation ==
Current implementation is based upon the r8330 of the svn master branch. So
the changes in the LHS representation (splitting of
CUnaryExpression and introduction of CLeftHandSide) aren't merged.
Besides merging this the preliminary CFA transformations:
cfa.transformUnsizedArrays = true transforms declarations like int a[] =
{1, 2, 3}, b[]; into int a[3] = {1, 2, 3}, *b;
cfa.transformPointerArithmetic = true transforms pointer arithmetic into
array subscripts (e.g.
a - 2 + i into a[i - 2] if a is a pointer).
cfa.transformArrows = true eliminates all ->s, but doesn't do any
simplifications of the LHS (unlike cfa.simplifyPointerExpressions)
cfa.transformStarAmper = true transforms *&s into just s
cfa.transformFunctionPointers = true transforms *f and &f for function
pointers to just f (to eliminate implicit conversions)
cfa.ignoreConst=true just drops all const qualifiers from all the types in
the CFA
cfa.ignoreVolatile=true does the same for the volatile qualifier
These transformation are currently implemented outside of ASTConverter.java as
a separate CFA transformer base on
4 visitors (for expressions, types, statements and initializers). But the
visitors transform one CFA into another with different
expressions, types etc. and this leads to a kind of memory leak since some
references (from CFA function heads, summary edges and
function exit nodes) still lead to the old CFA nodes.
The possible enhancements I've thought of
include combination with explicit analysis, which can allow to further
simplify the formulas using the information
about the possible values of the pointer variables on the path, better support
for unions and void* types, better recognition of memory
allocations (by looking at the variable type in the LHS) and implementing some
path formula slicing algorithm.
Regards, Mikhail
--
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin at ispras.ru
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bitvector-diff.csv
Type: text/csv
Size: 1417 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment.csv>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bitvector-table.csv
Type: text/csv
Size: 4588 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0001.csv>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: dd64-table.csv
Type: text/csv
Size: 11372 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0002.csv>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: dd64-diff.csv
Type: text/csv
Size: 9872 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0003.csv>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0001.html>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: heap-manipulation-diff.csv
Type: text/csv
Size: 5601 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0004.csv>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0003.html>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0004.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: heap-manipulation-table.csv
Type: text/csv
Size: 7524 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0005.csv>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ldv-regression-diff.csv
Type: text/csv
Size: 9208 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0006.csv>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0005.html>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0006.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ldv-regression-table.csv
Type: text/csv
Size: 31368 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0007.csv>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130826/a5d9f242/attachment-0007.html>
-------------- next part --------------
Hello!
== The configurations ==
-- Predicate analysis with real variables and recursion skipping.
Just as config/predicateAnalysis-PredAbsRefiner-ABEl.properties with
# Recursion skipping
analysis.summaryEdges=true
analysis.functionPointerCalls=true
cpa.callstack.skipRecursion=true
-- Predicate analysis with bit-vector variables and recursion skipping.
The same as the previous configuration, but with
# Turn on bit-vectors
cpa.predicate.replaceBitvectorWithRationalAndFunctionTheory = false
cpa.predicate.ignoreExtractConcat=false
# Turn on field aliasing
cpa.predicate.handlePointerAliasing = true
cpa.predicate.handleFieldAliasing = true
cpa.predicate.handleFieldAccess = true
# Using 32-bit Linux machine model
analysis.machineModel = LINUX32
-- Predicate analysis with bit-vector uninterpreted functions
(UFs from bit-vectors to bit-vectors). This is the new configuration employing the
analysis currently implemented in the pointer-predicates branch of
git://forge.ispras.ru/cpachecker.git. The same as the previous configuration
with
# Excluding malloc, __kmalloc and kzalloc from nondet functions
# The analysis treats them as memory allocating functions instead
cpa.predicate.nondetFunctions = {"sscanf", "random"}
# Options enabling preliminary CFA transformations required by the analysis with UF
# The transformations are rather simple and described further
cfa.simplifyPointerExpressions = false
cfa.transformUnsizedArrays = true
cfa.transformPointerArithmetic = true
cfa.transformArrows = true
cfa.transformStarAmper = true
cfa.transformFunctionPointers = true
cfa.ignoreConst=true
cfa.ignoreVolatile=true
# Options enabling PathFormulaWithUF and the usage of the
# appropriate address disjointness constraints
cpa.predicate.pointerAnalysisWithUFs = true
cpa.predicate.refinement.pointerAnalysisWithUFs = true
This configuration is based on file
config/predicateAnalysis-PredAbsRefiner-ABEl-UF.properties in the pointer-predicates branch.
-- Predicate analysis with real uninterpreted functions (UFs from reals to reals). This is the same as the previous
configuration, but with
# Turn off bit-vectors
cpa.predicate.replaceBitvectorWithRationalAndFunctionTheory = true
cpa.predicate.ignoreExtractConcat=true
This configuration is based on file
config/predicateAnalysis-PredAbsRefiner-ABEl-UF-replace.properties in the pointer-predicates branch.
== The results ==
-- ldv-regression category. Attached as ldv-regression-table.html. This also includes fixed manual tests submitted this year
(some of the tests were originally incorrect).
Overall in this category in comparison with the variable-based analysis
the new analysis wins 204 points for the real and 161 points for the
bit-vector case correspondingly.
The timeouts on ex3_forlist.c_safe.cil.c and ex3_forlist.c_safe.i for the BV case
are caused by huge interpolants derived from the formulas
involving essential arithmetics (addition, subtraction, multiplication). The interpolants contain
many constraints on the single bits extracted from bit-vector variable values. These interpolants seem to blow up
in (de)instantiation.
The parsing failures are spurious (I just accidentally included some original files in the benchmark).
The exceptions on test23_safe.c, test24_safe.c and test27_safe.c (the BV case) are MathSAT failures (in fails on ab-mixed terms
encountered in the unsatisfiability proof).
The false UNSAFEs on test29_safe.c, test_union.c_safe_1.cil.c, and test_union.c_safe_1.i arise because of the current union fields
encoding. In case the union is not shared (its address hasn't been taken yet anywhere on the path),
the union fields are encoded just as separate
variables. So their values are treated as independent. But even in case the union turns out to be shared
(addressed or dynamically allocated), its different-typed fields are encoded with different UFs, so their values are still independent,
though they can share the same memory address. Currently I have some thoughts about implementing support for assignments to unions by
explicitly assigning the right hand side to every field of the union with the appropriate type-conversions, but still putting it off
because of the complications in the general case when a union can contain structures, arrays and other unions in itself.
-- heap-manipulation category. Attached as heap-manipulation-table.html.
Overall in this category the new analysis currently looses 10 points in the BV case and 5 points in the real case.
On non-cillified files both BV and real configurations time out on SAFE benchmarks and give UNSAFEs verdicts
for their UNSAFE counterparts except in the two cases.
On bubble_sort_linux_unsafe.i the analysis loops infinitely in the successive refinements before reaching the actual error location.
On dll_of_dll_safe.i the loss of precision because of typing heuristic occurs. In dll_create_generic() the variable dll of type (void*)
is declared. Its address passed to either dll_insert_slave() or dll_insert_master() called by function pointer. But the functions
actually take arguments of either (struct slave_item **) or (struct master_item **). So they assign the value to the dll variable using
the UFs for types (struct slave_item *) or (struct master_item *). Then the caller function dll_create_generic() returns the value of
dll dereferencing it as a value of type (void *) and thus assumes its value to be arbitrary. This is rather a fundamental limitation of
the new analysis which can be partially addressed by assuming all possible actual types for each (void *) type encountered.
It seems that all false UNSAFEs on the cillified files are caused by the transformation of memory allocations, e.g:
struct sth *psth = (struct sth*) malloc(sizeof(struct sth));
-->
unsigned int tmp_0 = 16U; // size of (struct sth) computed and substituted by CIL
void *tmp_1 = malloc(tmp_0);
psth = (struct sth*) tmp_1;
After such transformation the malloc() is not properly recognized and the corresponding memory locations aren't properly tracked,
which leads to the loss of precision. This transformation is currently disabled by the CIL options we use in LDV so it shouldn't
be frequently encountered in our new benchmarks.
Meanwhile on the SAFE benchmarks the analysis discovers predicates for the linked lists up to the depth of 10 in about 30 seconds.
-- Device Drivers 64 category (partial). Attached as dd64-table.html
In this category I have only analyzed single-file non-cillified drivers.
Overall in this category the new analysis looses 6 points in the real case and the results for the BV case are too strange because
the variable-based analysis failed on too many benchmarks. Though I know we've already tried bit-precise analysis on the drivers and
haven't got so many UNKNOWNs. It seems due to the non-cillified filed being used, which turned out to be poorly supported by the
bit-precise configuration.
I haven't investigated the results in detail yet. Also it turned out that preliminary predicate extraction heuristic has significant
influence on the results in this category (I first launched the new analysis without this heuristic
and got 26 correct results instead of 29).
-- Bit vectors. Attached as bitvector-table.html
The table only contains results for BV configurations. It just shows that the results in this category don't differ significantly.
I have also launched the new analysis on the both subcategories of the Control Flow Integer set. I haven't done thorough
comparison (used small time and memory limits and only cared about the failures), but the analysis gives too many false UNSAFEs
for the ssh/* part of the memsimple subcategory, while the ntdrivers/* verdicts match.
== The implementation ==
Current implementation is based upon the r8330 of the svn master branch. So the changes in the LHS representation (splitting of
CUnaryExpression and introduction of CLeftHandSide) aren't merged.
Besides merging this the preliminary CFA transformations:
cfa.transformUnsizedArrays = true transforms declarations like int a[] = {1, 2, 3}, b[]; into int a[3] = {1, 2, 3}, *b;
cfa.transformPointerArithmetic = true transforms pointer arithmetic into array subscripts (e.g.
a - 2 + i into a[i - 2] if a is a pointer).
cfa.transformArrows = true eliminates all ->s, but doesn't do any simplifications of the LHS (unlike cfa.simplifyPointerExpressions)
cfa.transformStarAmper = true transforms *&s into just s
cfa.transformFunctionPointers = true transforms *f and &f for function pointers to just f (to eliminate implicit conversions)
cfa.ignoreConst=true just drops all const qualifiers from all the types in the CFA
cfa.ignoreVolatile=true does the same for the volatile qualifier
These transformation are currently implemented outside of ASTConverter.java as a separate CFA transformer base on
4 visitors (for expressions, types, statements and initializers). But the visitors transform one CFA into another with different
expressions, types etc. and this leads to a kind of memory leak since some references (from CFA function heads, summary edges and
function exit nodes) still lead to the old CFA nodes.
The possible enhancements I've thought of
include combination with explicit analysis, which can allow to further simplify the formulas using the information
about the possible values of the pointer variables on the path, better support for unions and void* types, better recognition of memory
allocations (by looking at the variable type in the LHS) and implementing some path formula slicing algorithm.
Regards, Mikhail
More information about the ldv-project
mailing list