Unifying Approach for Control-Flow-Based Loop Abstraction

Abstract

Loop abstraction is a central technique for program analysis, because loops can cause large state spaces if they are unfolded. In many cases, simple tricks can accelerate the program analysis significantly. There are several successful techniques for loop abstraction, but they are hard-wired into different tools and therefore difficult to compare and experiment with. We present a framework that allows us to implement loop abstractions in one common environment, where each technique can be freely switched on and off on-the-fly during the analysis. We treat loops as part of the abstract model of the program, and use counterexample- guided abstraction refinement to increase the precision of the analysis by dynamically selecting particular techniques for loop abstraction. The framework is independent from the underlying abstract domain of the program analysis, and can therefore be used on several different program analyses. We implemented several existing approaches and evaluate their effects on the program analysis.

Page Contents

We provide the following content:

1. The main results of our paper with extended plots and result tables (see below)
2. The Hoare-style proofs of some loop abstraction techniques mentioned in the paper
3. Descriptions on how to use our implementation in the CPAchecker framework
4. Instructions on how to reproduce our experimental results

Main Results

Our implementation is available on the branch loopsummary of CPAchecker.

Everything to reproduce our experiments is available in this repository:

https://gitlab.com/sosy-lab/research/data/loop-abstraction

The detailed experimental results are also compiled into the following BenchExec tables. The following table contains the experimental data that Fig. 6 and Table 1 was based on, i.e., all runs where CPAchecker was the verifying tool:

• CPAchecker

For Table 2, where we looked at the effect of our loop abstractions on verifers other than CPAchecker, we provide one table for each of them:

• Ultimate Automizer
• CBMC
• Symbiotic

How to Use Loop Summaries with CPAchecker

1. Setup

   CPAchecker is available at : https://gitlab.com/sosy-lab/software/cpachecker The loop summary feature is currently not yet merged into the main development branch, so for testing the feature you need to check out the feature branch named loopsummary. For information on the requirements of CPAchecker, we refer to the installation documentation. In a nut shell, you need to run the following:

   $ git clone https://gitlab.com/sosy-lab/software/cpachecker/
   $ cd cpachecker
   $ git checkout loopsummary
   $ ant

   The last command will build CPAchecker. In the following, we will assume CPAchecker is built and the current working directory is inside the directory cpachecker

2. Generating Patches for different Loop Abstraction Strategies

   One of the features we provide is providing abstracted versions of the loops in a program as patch files. To use this feature, run CPAchecker as follows:

   $ scripts/cpa.sh -generateLoopAbstractions test/programs/loopsummary/havoc.c

   Here we use the program havoc.c from the folder test/programs/loopsummary in CPAchecker. This folder contains some programs that are used for internal testing of the features related to loop abstractions. The parameter -generateLoopAbstractions will tell CPAchecker to use the configuration in config/generateLoopAbstractions.properties, which will start a custom algorithm that goes through all the loops in the program and all the loop abstraction strategies we support, then creates a patch for all of the different ways a loop abstraction can be performed with our framework. The result is stored in the folder output/LA. For the program havoc.c, the result is as follows:

   havoc.c.loop_at_offset_574.NAIVELOOPACCELERATION.patch
   havoc.c.loop_at_offset_399.NAIVELOOPACCELERATION.patch
   havoc.c.loop_at_offset_574.OUTPUTLOOPACCELERATION.patch
   havoc.c.loop_at_offset_399.OUTPUTLOOPACCELERATION.patch
   havoc.c.loop_at_offset_574.LOOPCONSTANTEXTRAPOLATION.patch
   havoc.c.loop_at_offset_399.LOOPCONSTANTEXTRAPOLATION.patch
   havoc.c.loop_at_offset_399.HAVOCSTRATEGY.patch
   havoc.c.loop_at_offset_574.HAVOCSTRATEGY.patch

   Each of the patches contains the offset (number of characters after which the loop starts) of the loop that is abstracted as well as the name of the strategy that is used.

   For example, the patch havoc.c.loop_at_offset_399.HAVOCSTRATEGY.patch looks like this:

   --- havoc.c
   +++ havoc.c
   @@ -14,13 +14,16 @@
      return;
    }
    
    int main(void) {
      unsigned int x = 1000000;
   -  while (x > 0) {
   -    x -= 4;
   +  // START HAVOCSTRATEGY
   +  if (x > (0)) {
   +  x = __VERIFIER_nondet_uint();
      }
   +  if (x > (0)) abort();
   +  // END HAVOCSTRATEGY
      __VERIFIER_assert(!(x % 4));
    
      int y = 0;
      for (int z = 0; y<1000000 ; y += 2) {
        ;

   Note For the loop abstractions, we will use certain functions like the VERIFIER_nondet_X functions that mark nondeterministic values or the abort function. In order to use the patches successfully, you might need to add some extern declarations to the program. These can however just always be added and should not cause any issues:

   extern void abort(void);
   extern int __VERIFIER_nondet_int();
   extern _Bool __VERIFIER_nondet_bool();
   extern char __VERIFIER_nondet_char();
   extern double __VERIFIER_nondet_double();
   extern float __VERIFIER_nondet_float();
   extern unsigned long __VERIFIER_nondet_ulong();
   extern unsigned long long __VERIFIER_nondet_ulonglong();
   extern unsigned int __VERIFIER_nondet_uint();
   extern int __VERIFIER_nondet_int();

3. Verification Using Loop Abstractions with CPAchecker

   In this section, we explain how you can run the configurations of CPAchecker that are boosted with the continously refined loop abstraction strategies. The three configurations mentioned in the paper are in the folder config/loopsummary and named predicateAnalysis-loopsummary.properties, valueAnalysis-loopsummary.properties, and bmc-incremental-loopsummary.properties.

   For example, to verify the program test/programs/loopsummary/outputabstraction.c using predicate analysis with loop abstractions, run the following command:

   scripts/cpa.sh -config config/loopsummary/predicateAnalysis-loopsummary.properties -spec config/properties/unreach-call.prp test/programs/loopsummary/outputabstraction.c

   CPAchecker will then on success also output a modified version of the input program containing the loop abstractions that were used to proof the program correct (if possible). This will also be located in the directory output/LA, so for the command above CPAchecker will generate a modified copy of the program at output/LA/outputabstraction.c. Here, also the necessary extern declarations were already inserted, such that the generated program can be checked by any of the verifiers that support the SV-COMP specific conventions.

More details are available in our research paper.