[analyzer][RFC] Design idea: separate modelling from checking

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

[analyzer][RFC] Design idea: separate modelling from checking

Eric Fiselier 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

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer][RFC] Design idea: separate modelling from checking

Eric Fiselier via cfe-dev
First things first: right now literally nothing prevents us from
re-using state traits from multiple checkers or translation units. As in:

   // Model.cpp
   REGISTER_MAP_WITH_PROGRAMSTATE(StreamState, SymbolRef, int)
   namespace stream_state {
     int get(ProgramStateRef State, SymbolRef Sym) {
       return State->get<StreamState>(Sym);
     }
     ProgramStateRef set(ProgramStateRef State, SymbolRef Sym, int Val) {
       return State->set<StreamState>(Sym, Val);
     }
   }

   // Model.h
   namespace stream_state {
     int get(ProgramStateRef State, SymbolRef Sym);
     ProgramStateRef set(ProgramStateRef State, SymbolRef Sym, int Val);
   }

   // Checker.cpp
   #include "Model.h"
   void Checker::checkPreCall(const CallEvent &Call, CheckerContext &C) {
     SymbolRef Sym = Call.getArgSVal(0).getAsSymbol();
     int Val = stream_state::get(C.getState(), Sym);
   }

This approach is, i guess, even already used, for dynamic type info. I
guess nobody paid attention to that, so i was constantly running around
and whining how much we need it, and also taint checker wasn't made this
way for the same reason, i guess. One more item to refactor into a
proper trait that way would be region extent, which is essentially a
trait over the region - and it is probably even a mutable trait (see
jump-over-VLA bug).

The only downside i see with the implementation above is that we no
longer enjoy our nice object oriented syntax, i.e. get(State, Key)
instead of State->get(Key). We could probably improve upon that. And,
yeah, there's one more function call that wouldn't be inlined, to it may
be a tiny bit slower.

So if we are mostly concerned about huge overgrown and
poorly-interoperating checkers (MallocChecker, CStringChecker,
RetainCountChecker, GenericTaintChecker), we already have everything we
need, and i'm all for splitting them up.

~~~

Now, for when we want our "models" (checkers that only do modeling) to
be turned off. I think we never want them to be turned off, unless our
driver says they aren't applicable (i.e. C++-specific model in plain C,
or Windows-specific checks under Unix-like OSes), so we can delegate
this to the Driver(?). The reason why i think they should be never
turned off is because they, well, *improve modeling*. They are useful
for cutting off infeasible paths, or doing state splits properly when
those are indeed required. Even the taint checker - taint is essentially
a huge state split into all possible values. For instance, we should
probably disable inlined defensive check suppressions over tainted values.

Though leaving an emergency interface around for turning off broken
models would be nice.

~~~

Now, yeah, we can already do manual checker dependencies, as in

   registerMyChecker(CheckerManager &Mgr) {
     Mgr.registerChecker<MyModel>();
     Mgr.registerChecker<MyChecker>();
   }

This also guarantees that all models are loaded before the checkers that
need them, but not necessarily before other checkers. Not sure if we care.

Also in this case disabling the model is hard - all checkers that rely
on this model would need to be disabled as well.

As an alternative, we could make checker manager refuse to register
stuff that's explicitly disabled:

   registerMyChecker(CheckerManager &Mgr) {
     if (Mgr.registerChecker<MyModel>())
       Mgr.registerChecker<MyChecker>();
   }

This is unlikely to cause confusion when people try to enable checker
but it doesn't get enabled because model is off, because
   1. models are always on, and
   2. when they're off it is an emergency that the user is already aware of.
So i guess it'd be better this way.

~~~

Regarding races between checkers who model the same stuff - i agree that
this is a problem, regardless of how we separate models and checkers, no
idea what to do.

I think that at least in the case of the Environment we can protect
ourselves from races by just making its entries unmodifiable. When the
expression is computed, it gets placed into the Environment. When it
leaves the scope, it is automatically garbage-collected from the
environment. And i think we should completely disallow replacing
existing values in the environment - no matter who tries to do that, be
it core or checkers - unless we're in for a full-scale renaming of one
symbolic value into another symbolic value (we aren't). The problem is
that we do a lot of that even in the core, so i'd really like to have
this fixed.

For the Store this seems harder, because Store is definitely designed to
be mutable, and modeling writes is quite a normal course of behavior for
the checkers. So i've no idea how to protect ourselves from races here.

Because traits are often Store-like, we'd have these problems with them
as well.

~~~

Now, the really big reason why we wanted to have shared checker states
is that we wanted to let the core inspect them and perhaps automate some
routine work in the checkers. For that purpose, each checker giving
access to their state with the help of custom getters and setters is
definitely not sufficient. Even if getter/setter interface is
standardized, the core would never guess how to actually operate on it.

On that topic i don't have much updates yet.

It is obvious that we need to restrict checkers in what they can do, so
that the core could comprehend it. We have this idea around to make
traits part of the Store, but the Store is too smart and unreliable, and
in many cases it would be an overkill. The alternative is to make a list
of simple kinds-of-traits that we support ("abstract models" that know
how to model but don't know what to model, eg. an abstract model of
"some trait over a symbol that represents the status of an object
identified by that symbol" that would be used by MallocChecker and
StreamChecker), and provide standardized interfaces for the model
developers to make use of them for their specific models, while teaching
the core how to do maintenance on them; this would increase the number
of levels of abstractions to 4: core <-> abstract models <- specific
models <- checkers. But the fatter our abstract models become, the
easier would it be to develop specific checkers.

Which is kinda nice.


On 15/12/2017 6:23 AM, Aleksei Sidorin wrote:

> 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.
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer][RFC] Design idea: separate modelling from checking

Eric Fiselier via cfe-dev
Hi!

In general, I like the idea of separating modeling and diagnostics.

On 16 December 2017 at 00:40, Artem Dergachev <[hidden email]> wrote:
First things first: right now literally nothing prevents us from re-using state traits from multiple checkers or translation units. As in:

  // Model.cpp
  REGISTER_MAP_WITH_PROGRAMSTATE(StreamState, SymbolRef, int)
  namespace stream_state {
    int get(ProgramStateRef State, SymbolRef Sym) {
      return State->get<StreamState>(Sym);
    }
    ProgramStateRef set(ProgramStateRef State, SymbolRef Sym, int Val) {
      return State->set<StreamState>(Sym, Val);
    }
  }

  // Model.h
  namespace stream_state {
    int get(ProgramStateRef State, SymbolRef Sym);
    ProgramStateRef set(ProgramStateRef State, SymbolRef Sym, int Val);
  }

  // Checker.cpp
  #include "Model.h"
  void Checker::checkPreCall(const CallEvent &Call, CheckerContext &C) {
    SymbolRef Sym = Call.getArgSVal(0).getAsSymbol();
    int Val = stream_state::get(C.getState(), Sym);
  }

This approach is, i guess, even already used, for dynamic type info. I guess nobody paid attention to that, so i was constantly running around and whining how much we need it, and also taint checker wasn't made this way for the same reason, i guess. One more item to refactor into a proper trait that way would be region extent, which is essentially a trait over the region - and it is probably even a mutable trait (see jump-over-VLA bug).

The only downside i see with the implementation above is that we no longer enjoy our nice object oriented syntax, i.e. get(State, Key) instead of State->get(Key). We could probably improve upon that. And, yeah, there's one more function call that wouldn't be inlined, to it may be a tiny bit slower.

So if we are mostly concerned about huge overgrown and poorly-interoperating checkers (MallocChecker, CStringChecker, RetainCountChecker, GenericTaintChecker), we already have everything we need, and i'm all for splitting them up.

~~~

Now, for when we want our "models" (checkers that only do modeling) to be turned off. I think we never want them to be turned off, unless our driver says they aren't applicable (i.e. C++-specific model in plain C, or Windows-specific checks under Unix-like OSes), so we can delegate this to the Driver(?). The reason why i think they should be never turned off is because they, well, *improve modeling*. They are useful for cutting off infeasible paths, or doing state splits properly when those are indeed required. Even the taint checker - taint is essentially a huge state split into all possible values. For instance, we should probably disable inlined defensive check suppressions over tainted values.

Though leaving an emergency interface around for turning off broken models would be nice.

I think it is important to have such interface. One might have modeling that is applicable only to some of the projects and not the others (e.g.: specific to a library or an STL implementation).


~~~

Now, yeah, we can already do manual checker dependencies, as in

  registerMyChecker(CheckerManager &Mgr) {
    Mgr.registerChecker<MyModel>();
    Mgr.registerChecker<MyChecker>();
  }

This also guarantees that all models are loaded before the checkers that need them, but not necessarily before other checkers. Not sure if we care.

Does the order of loading the checks determine the order of callbacks? So does this solve the racing between checks?
 

Also in this case disabling the model is hard - all checkers that rely on this model would need to be disabled as well.

As an alternative, we could make checker manager refuse to register stuff that's explicitly disabled:

  registerMyChecker(CheckerManager &Mgr) {
    if (Mgr.registerChecker<MyModel>())
      Mgr.registerChecker<MyChecker>();
  }

This is unlikely to cause confusion when people try to enable checker but it doesn't get enabled because model is off, because
  1. models are always on, and
  2. when they're off it is an emergency that the user is already aware of.
So i guess it'd be better this way.

I think it would be great to have good warning messages for the user. I.e.: warning: explicitly enabled checker X cannot be turned on due to its dependency Y is explicitly disabled.

Otherwise it might be surprising that a check does not give any warning even is it is turned on.
 

~~~

Regarding races between checkers who model the same stuff - i agree that this is a problem, regardless of how we separate models and checkers, no idea what to do.

I think that at least in the case of the Environment we can protect ourselves from races by just making its entries unmodifiable. When the expression is computed, it gets placed into the Environment. When it leaves the scope, it is automatically garbage-collected from the environment. And i think we should completely disallow replacing existing values in the environment - no matter who tries to do that, be it core or checkers - unless we're in for a full-scale renaming of one symbolic value into another symbolic value (we aren't). The problem is that we do a lot of that even in the core, so i'd really like to have this fixed.

For the Store this seems harder, because Store is definitely designed to be mutable, and modeling writes is quite a normal course of behavior for the checkers. So i've no idea how to protect ourselves from races here.

Because traits are often Store-like, we'd have these problems with them as well.

~~~

Now, the really big reason why we wanted to have shared checker states is that we wanted to let the core inspect them and perhaps automate some routine work in the checkers. For that purpose, each checker giving access to their state with the help of custom getters and setters is definitely not sufficient. Even if getter/setter interface is standardized, the core would never guess how to actually operate on it.

On that topic i don't have much updates yet.

It is obvious that we need to restrict checkers in what they can do, so that the core could comprehend it. We have this idea around to make traits part of the Store, but the Store is too smart and unreliable, and in many cases it would be an overkill. The alternative is to make a list of simple kinds-of-traits that we support ("abstract models" that know how to model but don't know what to model, eg. an abstract model of "some trait over a symbol that represents the status of an object identified by that symbol" that would be used by MallocChecker and StreamChecker), and provide standardized interfaces for the model developers to make use of them for their specific models, while teaching the core how to do maintenance on them; this would increase the number of levels of abstractions to 4: core <-> abstract models <- specific models <- checkers. But the fatter our abstract models become, the easier would it be to develop specific checkers.

Which is kinda nice.



On 15/12/2017 6:23 AM, Aleksei Sidorin wrote:
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).

I like the idea of not putting everything in the analyzer engine, but we definitely need a nicer infrastructure for that.
 

=============================================================
                      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.

This does not solve the problem of possible interdependent modellers.
 

   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.




_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev