Project

General

Profile

Actions

Bug #3701

open

CPAchecker degradation on drivers/staging/go7007/s2250.ko

Added by Vadim Mutilin over 11 years ago. Updated over 11 years ago.

Status:
Open
Priority:
Normal
Assignee:
Category:
-
Start date:
11/19/2012
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

The previous of CPAchecker (March 2012) finishes with UNSAFE verdict while new version (Nov 2012) time outs with 15 min limit


Files

errloc_automaton.txt (286 Bytes) errloc_automaton.txt Vadim Mutilin, 11/19/2012 01:04 PM
s2250_cpa.cfg (2.18 KB) s2250_cpa.cfg Vadim Mutilin, 11/19/2012 01:04 PM
s2250_input.cil.out.i.gz (41.8 KB) s2250_input.cil.out.i.gz Vadim Mutilin, 11/19/2012 01:04 PM

Updated by Vadim Mutilin over 11 years ago

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

Actions #2

Updated by Vadim Mutilin over 11 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.

Actions #3

Updated by Alexey Khoroshilov over 11 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.

Actions

Also available in: Atom PDF