Bug #3701
open
CPAchecker degradation on drivers/staging/go7007/s2250.ko
Added by Vadim Mutilin about 12 years ago.
Updated almost 12 years ago.
Description
The previous of CPAchecker (March 2012) finishes with UNSAFE verdict while new version (Nov 2012) time outs with 15 min limit
Files
I found that degradation is caused by a commit of revision 6727.
This revision changes two files:
U src/org/sosy_lab/cpachecker/cfa/parser/eclipse/CFAFunctionBuilder.java
U src/org/sosy_lab/cpachecker/cfa/parser/eclipse/ASTConverter.java
The input file and configuration attached.
Command line
for cpachecker
s2250_input.cil.out.i -config s2250_cpa.cfg -entryfunction ldv_main0_sequence_infinite_withcheck_stateful -outputpath cpa-tmp -ea -Xmx1200m
for ldv-manager
RCV_MEMLIMIT=3500000 LDV_DEBUG=100 RCV_VERIFIER=cpachecker CPACHECKER_CONFIG=predicateAnalysis.properties CPACHECKER_OPTIONS='-heap 1200m' ldv-manager envs=linux-3.0.4.tar.bz2 drivers=drivers/staging/go7007/s2250.ko kernel_driver=1 rule_models=32_1
The degradation is caused by the order of then and else edges.
In the new version the CFA traversal at first goes by the path without error, while old version directly comes the error.
To restore the old behaviour we may simply change the order in function addConditionEdges:
+ final CAssumeEdge trueEdge = new CAssumeEdge(condition.toASTString(),
+ rootNode.getLineNumber(), rootNode, thenNode, condition, true);
+ addToCFA(trueEdge);
// edge connecting condition with elseNode
+ final CAssumeEdge falseEdge = new CAssumeEdge("!(" + condition.toASTString() + ")",
+ rootNode.getLineNumber(), rootNode, elseNode, condition, false);
+ addToCFA(falseEdge);
but do we actually need it?
Anyway we need to speed up CPAchecker so it can find UNSAFE regardles of CFA edges order.
It can be another point of configurability of CPAchecker.
Another idea to research is to stop exploration of a code subtree by timeout and to continue to explore another subtree after that.
Also available in: Atom
PDF