Loop abstraction [depends-on: #2707]

[zhixing-xu]

Two flags '--abstract-loops', '--abstractset' are added into goto-instrument and cbmc to support automated loop abstraction for given program.

The goal of this loop abstraction method is to prove memory safety in specific loops without having to unwind them.

If memory safety assertions in a loop are only decided by the loop variables and values unchanged in the loop, and the assertions outside the loop does not depend on loop contents; the loop could be reduced into 1 iteration (shrinkable), by making the loop variables nondet with constraints inflicted by the loop condition. As illustrated in the following example:

Original code:

for(int i=0; i<N; i++){
    for(int j=0; j<M; j++){
        ...
        image[f(i,j)] = value; 
        assert(f(i,j) in bound);
    }
}

After abstraction

i=nondet_int();
j=nondet_int();
assume i<=N && i>=0;
assume j<=M && j>=0;
image[f(i,j)] = value; 
assert(f(i,j) in bound);

'--abstract-loops' enables the method and '--abstractset' allows user to specify loops to be reduced. The method first check if the loops follow the property that allows them to be abstracted by analyzing the data dependence of the loop variables and assertions. For the loops following the property, it proceeds to do the abstraction on them.

This PR also includes #2707, which gives more accurate data dependency through function calls, thus helping decide the loop shrinkability problem better.
It would beneficial to also include #2646, #2694, they give more accurate data dependency for dynamic objects. The regression test abstract-loops3 would pass with these patches.

[peterschrammel]

Thanks, @zhixing-xu for your contribution. While we are going to review this in more detail, could you please the compilation, linting and formatting errors?

• Compilation errors on Windows:

cl -DSATCHECK_MINISAT2  -DHAVE_MINISAT2 /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF -I .. /nologo /c /EHsc abstract_loops.cpp /Foabstract_loops.obj
abstract_loops.cpp
abstract_loops.cpp(363): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(363): error C3861: 'inserter': identifier not found
abstract_loops.cpp(372): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(372): error C3861: 'inserter': identifier not found
abstract_loops.cpp(402): warning C4267: 'argument': conversion from 'size_t' to 'unsigned int', possible loss of data
abstract_loops.cpp(531): error C2039: 'inserter': is not a member of 'std'
C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\INCLUDE\iostream(12): note: see declaration of 'std'
abstract_loops.cpp(531): error C3861: 'inserter': identifier not found
make[2]: *** [../common:222: abstract_loops.obj] Error 2

• Linting errors: https://travis-ci.org/diffblue/cbmc/jobs/423135252#L479

• Formatting errors: https://travis-ci.org/diffblue/cbmc/jobs/423135251#L511 (use git-clang-format to clang-format the changes made in your commits)

• Merge branch 'develop' into loop_abstract 08c2ec0: Please rebase instead of merging.

[TGWDB]

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.