Linux Driver Verification » BLAST

In C language two different stack-allocated variables always have different addresses at their scope. However, no reasoning about it is actually in use.

The same holds for memory regions, that are allocated via malloc and have not been freed at a program location.

This issue is formalized in two test cases in test_malloc.c file of blast regression test suite. Here's the code that demonstrates the problem:

int main()
{
        int a,b;
        int *p1=&a;
        int *p2=&b;
        assert(p1!=p2);   //BLAST doesn't think it's safe!
        return 0;
}

Options: -alias bdd -aliasclos -cref -predH 7 -lattice -include-lattice symb -include-lattice list -craig 2 -debug -bddprint -cldepth 2

Any possible help with this is welcome. I'd prefer to solve this problem and substantially use it in our models.

A possible idea is to implement this thing via simple instrumentation that should be inserted to BLAST. Since we only check non-recursive control flows, each variable will only have ONE address throughout the program run. Therefore, at points of their declarations (or at entries to proper functions), BLAST can issue dummy blocks that contain several "assignments" in form of "&local_var = 1", "&other_var = 2" etc. They will be then used in checking and it will prevent BLAST from adding predicate for each pair of variables.

However, this may lead to excessive payload on solver. So this idea was later extended to tracking addresses only of those variables that are interesting to specific models. For example, track mutexes only, drivers/char/ipmi/ipmi_msghandler.c:

static DEFINE_MUTEX(ipmi_interfaces_mutex);
static DEFINE_MUTEX(smi_watchers_mutex);

mutex_lock(&smi_watchers_mutex);
mutex_lock(&ipmi_interfaces_mutex);

We don't need tracking other addresses (although we might want to), but we surely need tracking mutexes.