[cfe-dev] [analyzer][RFC] Design idea: separate modelling from checking

[Aleksei Sidorin via cfe-dev]

It seems like it is the analyzer RFC week so I'll contribute a bit. :)

TL;DR: I think we may need to split up checkers from execution modeling 
in order to resolve unclear dependencies between checkers, improve 
checker development process and resolve some non-trivial issues. There 
is no any proof-of-concept implementation, just some thoughts I (and our 
team) wish to summarize and to describe the issue. Feel free to share 
your opinion or correct me if I made wrong assumptions or wrong conclusions.

0. Pre-history.
There were some thoughts on this topic shared personally during 
meetings. I and Artem Dergachev agreed on the fact that checker 
capabilities to do everything that make implementation of some common 
approaches to simplify the checker API much harder; unfortunately, I 
don't know if any decision about this was made on latest LLVM devmeeting 
because its results were not shared.

=============================================================
                       1. Problem
=============================================================

Now, many checkers perform modelling of events interesting for them 
(most of these events are function calls). They may bind a return value 
to the expression, perform Store binding, and split states with 
generating multiple nodes. This approach has some pros:
1. If a checker is disabled, modelling is not performed. So, we save 
some computation time.
2. It may look like kind of encapsulation for modelling operations.

However, I think this approach has several disadvantages.

1. It introduces dependencies between checkers. If we need to ensure 
that return value of malloc() is null or not in our checker, we need to 
turn on MallocChecker and:
   1) keep its traits in ProgramState (memory consumption);
   2) suffer from its checking operations that consume time without any 
reason for us;
   3) watch its warnings that are not useful for our checker.

The story with GenericTaint checker (which is strongly needed for many 
security checks) is even more painful: in addition to this, we also need 
to keep separate functions directly in ProgramState to access taint 
information.

The requirement to always enable 'core' checkers was a some kind of 
warning bell because it exposes the problem directly to users. This 
requirement may be non-evident for analyzer users that may need even to 
silence 'core' warnings. There may also be modelers appearing later that 
are not in 'core' so this mandatory list will only grow. And, finally, 
the main problem is that switching off 'core' can lead to assertion 
failures which are definitely not the best way to inform user about need 
to enable these checkers.

Another result of this is having checkers that don't throw warnings at 
all. Such checkers as core.NoReturn and core.LibraryFunctions are 
strongly required to use because they greatly improve analysis quality 
but actually, they don't check anything.

2. Result ExplodedGraph depends on checker execution order. For example, 
if a checker splits state into two with adding transitions, another 
checker will be launched twice if it is executed after the splitter but 
only once if it is executed before. The state splitting itself is a very 
sharp tool that we may need to hide from novice users as it doubles 
branch analysis time, but that's another story. The problem is that 
checker can meet different constraints on the same code depending not 
only on checkers enabled or disabled but even on their order so even 
testing of such dependencies becomes much harder. Such interaction may 
potentially result in lost warnings or false positives.

Checkers can also write to same Environment or Store entries erasing 
each other's data. That kind of interaction is usually easy to debug but 
is still an issue we may wish to avoid: testing checker sets is much 
harder than testing a single checker due to lots of combinations.

3. What is more (maybe, even the most) important is that as the result 
of (2) we may have non-consistent checker warnings if some checkers are 
enabled or disabled. If analysis of some large function is terminated by 
max-nodes limit, the reachability of different nodes depends on state 
splitting. So, a warning may appear if a checker is the only enabled, 
but it may disappear if there are more checkers that split state --- we 
may just don't get to the point where a warning occurs. Such 
inconsistency may become a problem both for developers and for warning 
tracking systems.

4. This approach forces developers to do a work that, ideally, should be 
done by analyzer engine, in the checker. So, the results are not shared 
with other checkers or are shared in some non-trivial way (see 
GenericTaint example).

=============================================================
                       2. Possible approaches
=============================================================

While dependencies and broken encapsulation are something we can 
potentially deal with, non-consistency needs some more than just testing 
and verification. And currently I don't see the approach other that 
forbidding checkers to perform modeling operations.

As I understand, to achieve consistency, checkers should always get same 
ExplodedGraph independently on checkers enabled or disabled. The only 
way to do it is to build ExplodedGraph without interactions with 
checkers. So, we should run modelers independently and then use their 
results in checkers. Checkers are only permitted to read from 
Environment/Store and to operate with GDM.

There are several options.

1. Extract all modellers and launch them before checker run.

    The problem here is how to select the modellers we need to run.
    1) We can launch them all. So, the graph will be bigger. But it will 
always be the same, independently on how many checkers are running. So, 
there is no any inconsistency. Another advantage is that all statements 
that depend on checker modelling are modelled correctly: for example, 
the return result of 'malloc()' will be in HeapSpace independently on 
memory checks enabled/disabled.
    2) Launch only modellers that are required for checkers mentioned in 
command line. This will keep resources but inconsistency will still be a 
problem here.

The problem here is when should we launch modellers. Usually, we have 
three evaluation phases: PreStmt (checkers), modelling by engine and 
PostStmt. And it is not evident for me which phase is suitable for this. 
For example, core.CallAndMessage checker can generate sink nodes on 
PreStmt and if it is disabled, analyzer engine can crash. Some modellers 
need to constraint the return value and need to be launched after engine 
finished the modelling.

2. Silence the checkers that are used as dependencies of other checkers 
and not mentioned in the run line. So, 'core' is always launched 
mandatory but is just silenced if the user doesn't want to see warnings. 
This seems to be the easiest way; however, it doesn't solve the problem 
with inconsistent warnings. The only way to get consistent ExplodedGraph 
here is to launch all checkers and then silence disabled ones.

3. Move the modelling into the ExprEngine. So, ExprEngine will generate 
events that other checkers can subscribe on. This is mostly OK but some 
problems are also present: they are lack of incapsulation and ExprEngine 
growth. There is still a problem with plugins: to modify modelling, 
developer has to re-compile the analyzer or... write a checker.

Personally, I prefer option 1.1. Initially, it can even be implemented 
with existing checker interface. What we should do here is to strictly 
specify the order in which modellers run in order to avoid problems with 
unexpected interactions.

However, there can be options and problems I did not consider. Does 
somebody have any opinion on this? It will also be cool if somebody will 
share the result of latest LLVM devmeeting: as I remember, there should 
have been a BoF about checkers API.

-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics