[ldv-project] Benchmarking new predicate analysis with UFs

[Mikhail Mandrykin]

> Did you have
> cfa.simplifyPointerExpressions = true
> here (as in config/predicateAnaylsis-bitprecise.properties)?

> That would be explainable if the option
> cfa.simplifyPointerExpressions was not set to true.

No, so I've re-run the benchmark with this option. But it seems it won't  
influence the results greatly, because when I manually re-run the failed 
benchmarks with the option (used options attached in 
UsedConfiguration.properties), at least 9 out of 12 failures persisted. The 
exceptions are basically typing errors like these ones:

6x 			java.lang.IllegalArgumentException: A symbol with name `action at 4' 
already exists, with type: <BitVec, 64, > 
2x			 java.lang.IllegalArgumentException: bv extraction of an empty range: 
[22671:22672]
1x			type error. term eeprom_wait_ready::status at 3 has type <BitVec, 64, >, 
but <BitVec, 48, > was expected. (make_equal)

Also there are 6 Out of Memory results (9GB of heap and 12 GB total limit is 
used) on the tests where three other configurations completed successfully. 

> However, the options that you present look much simpler to me, couldn't
> these simplifications be implemented directly in the analysis itself
> (where C asts are transformed to formulas)?

I think transformPointerArithmetic, transformArrows, transformStarAmper, 
ignoreConst and ignoreVolatile can be easily moved to the analysis itself. 

> Options that do not have any disadvantages and just simplify the AST
> could be implemented in the ASTConverter itself (without being
> user-configurable). transformUnsizedArrays could be such an option
> (although we would need to make sure that all references to that
> variable also have pointer type instead of array type because analyses
> expect that the type of variables does not change).

The current CFA transformations change the type in all references as well, so 
I'll then look at doing the same in the ASTConverter. 

> For transformFunctionPointers, I wonder why you need this.
> We actually added code to CPAchecker to make the reverse transformation
> (adding * to a function pointer when it is called; adding & to a
> function when it is converted to a function pointer) to be able to
> easily detect these cases in the AST and not confuse them with regular
> function calls or variable accesses, and this helped to make the code of
> the analysis easier and give less false answers.

As I remember I had problems with typing here. In the CFA (especially in case 
of funciton pointer call handling with assume edges) there were comparisons of 
the form *f == *g where for instance f is a function and g  is a function 
pointer variable. Here my transformation only removes the star from *f. But 
maybe that's the only case when it's needed and that should be fixed somewhere 
else (in the CFA creation or in the analysis itself).

Regards, Mikhail
-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin at ispras.ru
-------------- next part --------------
analysis.functionPointerCalls = true
analysis.machineModel = LINUX64
analysis.programNames = /home/mikhail/ppreds/simple-tests/dd64/module_get_put-drivers-scsi-megaraid.ko_safe.cil.out.i.pp.i
analysis.summaryEdges = true
analysis.traversal.order = bfs
analysis.traversal.useCallstack = true
analysis.traversal.useReversePostorder = true
analysis.useRefinement = true
ARGCPA.cpa = cpa.composite.CompositeCPA
cegar.refiner = cpa.predicate.PredicateRefiner
cfa.simplifyPointerExpressions = true
cfa.useMultiEdges = true
CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, cpa.conditions.global.GlobalConditionsCPA
cpa = cpa.arg.ARGCPA
cpa.callstack.skipRecursion = true
cpa.conditions.global.time.wall = -1
cpa.predicate.blk.alwaysAtFunctions = false
cpa.predicate.blk.alwaysAtLoops = true
cpa.predicate.handleFieldAccess = true
cpa.predicate.handleFieldAliasing = true
cpa.predicate.handlePointerAliasing = true
cpa.predicate.ignoreExtractConcat = false
cpa.predicate.refinement.performInitialStaticRefinement = true
cpa.predicate.replaceBitvectorWithRationalAndFunctionTheory = false
log.level = OFF
output.disable = false
specification = /home/mikhail/repos/cpachecker/config/specification/sv-comp.spc