cbmc:refactor/ai_base_apis_2

Last commit made on 2019-11-25
Get this branch:
git clone -b refactor/ai_base_apis_2 https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
refactor/ai_base_apis_2
Repository:
lp:cbmc

Recent commits

529d7a5... by martin <martin@raphael>

Thread a single history through all initialisation and fixedpoints

This is needed to support histories that carry information across
function calls. It requires some changes to the internal API in
ai_baset but should not give any changes to the results computed.

b472724... by martin <martin@raphael>

Move a function so that the ordering in .cpp matches the .h

dd9bf17... by martin <martin@raphael>

Update the documentation in the key abstract interpreter classes

This reflects the changes in the structure and best practice that
result from this series of patches.

1587143... by martin <martin@raphael>

One domain per history storage in abstract interpretation

This allows more sophisticated history abstractions that have
more than on distinct history per location (for example loop
unwinding and calling context).

30beeda... by martin <martin@raphael>

Replace locations with history abstractions in the abstract interpreter

This is a fundamental change in how the abstract intepreter works.
Previously it's working unit was a location. Transforms were between
locations and the most precise unit for domain storage was per location.
History objects are abstractions that represent one or more control
flow path histories. A single location is the most coarse grains of
these but they can include calling contexts, paths taken, loop iterations
thread changes, etc. This change should be backwards compatible but
also allow more sophisticated histories, giving loop unwinding, context
sensitivity, path sensitivity, thread awareness and many others.

a5b390d... by martin <martin@raphael>

Add a typedef for "a pointer to a domain" to simplify interfaces

These are used because it allows const analysers / ai_storage
objects to generate new (bottom) domains, so on-the-fly domain
creation is properly supported.

bf96a08... by martin <martin@raphael>

Refactor and tidy how function calls are handled in AI

The current ai_baset has a "skip if not available, otherwise recurse"
policy which cannot be altered or removed. Recursion causes problems
for domains with large height as they can crash the analyser. It also
mixes the (interprocedural) state of the /analysis/ with the recursive
state of the /analyser/. This forces an undesireable design choice --
it means that anything interprocedural must be handled purely in the
domain. Doing so has several limitations and so this patch allows
inheritance to change how interprocedural analysis is done.

bf8cdf7... by martin <martin@raphael>

Delegate the storage of domains to an object owned by ai_baset

By delegating the storage of domains to a separate object (in a
similar way to the creation and other domain specific things in
ai_domain_factory) we gain the ability to play with and modify the
number and way that domains are stored without needing to inherit
from ai_baset and re-implement things. This creates new
possibilities such as pruning domains during analysis, have one
domain per function or even just one over-all (needed to obsolete
some of the older AI frameworks). It also means that inheritance
from ai_baset or ait can be used to alter how the algorithm works
without being tied to a particular storage model.

4f10a4f... by martin <martin@raphael>

Move the domain factory from ait into the base class

The rest of the architecture has been smoothed enough to do this.
This is part of a goal of removing functionality from ait so that
it can be modularised and extended in other ways.

c1e4926... by martin <martin@raphael>

Move the domain-specific call of merge into the factory

This is part of a larger effort to move all of the domain-specific
code out of ait so it can just manipulate the domain interface and
doesn't need to know the actual type of the domains.