Bug #3701
openCPAchecker degradation on drivers/staging/go7007/s2250.ko
0%
Description
The previous of CPAchecker (March 2012) finishes with UNSAFE verdict while new version (Nov 2012) time outs with 15 min limit
Files
Updated by Vadim Mutilin almost 12 years ago
- File errloc_automaton.txt errloc_automaton.txt added
- File s2250_cpa.cfg s2250_cpa.cfg added
- File s2250_input.cil.out.i.gz s2250_input.cil.out.i.gz added
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
Updated by Vadim Mutilin almost 12 years ago
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.
Updated by Alexey Khoroshilov almost 12 years ago
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.