#141 Bug in pointer analysis or documentation

[Ed Schwartz]

The CIL documentation suggests that calling Ptranal.analyze_file is all that is needed to use the pointer analysis APIs. If I call Ptranal.resolve_exp after doing this, I get:

*******
Assertion failed: collect_ptset_slow can't query graph
*******

If I call Ptranal.compute_results false after Ptranal.analyze_file, but before Ptranal.resolve_exp, everything works fine. It's not clear if this is a bug in the documentation (compute_results should be called, but it not documented), or if compute_results should not be needed, and the lazy computation is broken somehow.

If needed, I can produce a minimal example. I didn't want to do this in case the problem is only a documentation bug.

[Christoph L. Spiel]

    In some old (CIL feature) code of mine I

have found the following snippet right at the
start of my own feature.

Ptranal.analyze_mono := false;
Ptranal.no_sub := false;
Ptranal.smart_aliases := true;
Ptranal.feature.Cil.fd_doit a_source_file;

Obviously, the pointer analysis needs
configuring and running-in-advance.

IMHO, we have got two possibilities here: Either
each feature calls all prerequisite features and
modules, making it easy to "just get the work
done" and shallowing the learning curve of the CIL
system as a whole.

Or we do not call any dependencies, but just
document the need of calling them. This opens
up more possibilities for the user as she can
supply her own prerequisite features and thus is
not forced to use the hard-coded ones.
Moreover, this approach clarifies the user code
by explicit calls to the required functions as
shown above.

Gabriel is the boss. He will decide.

[Ed Schwartz]

Another problem is that even if I call compute_results, sometimes calls to Ptranal.resolve_exp raise the Not_found exception, even for expressions that appear in the program.

This is easy to fix by changing Ptranal.traverse_expr to call Ptranal.analyze_expr when Not_found is raised.

[Gabriel Kerneis]

Ed, Christoph,

I want to fix this issue, but I don't use Ptranal myself so I'd rather trust your judgement on this matter. As far as I understand it, we have two issues, here:

1) a documentation issue. Note that fd_doit does call both analyze_file and compute_results, so presumably what we are aiming at is documenting ptranal.mli to let the user know what functions need to be called before using the "high-level API"? (this is assuming the user wants to use Ptranal without enabling the feature on the command-line, which is reasonable since Cil and its extensions can also be used as a library.)

2) sometimes, calling analyze_file and compute_results is still not enough to pre-compute the analysis of expressions. I believe the root cause for this is that analyze_stmt (and others?) ignores a number of expressions and does not call analyze_expr on them (e.g. conditions in If and Switch). I don't know if this is a bug of analyze_stmt, traverse_expr (which should lazily catch the Not_found and run analyze_expr) or if we just need to document this behaviour. I am tempted to catch Not_found in every traverse_ and call the corresponding analyze_ in the handler. Does that sound sensible?

Patches and feedback welcomed. I have time to make a release before the summer, let's try and make it good :-)

[Ed Schwartz]

Sorry for the delay; I've been on vacation. Gabriel, your changes sound reasonable to me. Below is the specific change that I used, which worked well for me on the small test programs I was working with.

--- a/src/ext/pta/ptranal.ml
+++ b/src/ext/pta/ptranal.ml
@@ -380,7 +380,8 @@ let analyze_file (f : file) : unit =

 (* Same as analyze_expr, but no constraints. *)
 let rec traverse_expr (e : exp) : A.tau =
-  H.find expressions e
+  try H.find expressions e
+  with Not_found -> analyze_expr e

 and traverse_expr_as_lval (e : exp) : A.lvalue =
   match e with

[az bro]

In no way am I an expert on alias analysis, but maybe
this is a culprit:

    | If (e, b, b', l) ->
        (* ignore the expression e; expressions can't be side-effecting *)
        analyze_block b;
        analyze_block b'

I.e., some expressions are not analyzed,because they
cannot affect the analysis, but then, of course,
traverse_expr will fail.

Also note that analyze_lval depends on current_fundec
being set, which it won't be in the proposed fix:

let rec analyze_lval (lv : lval ) : A.lvalue =
    let find_access (l : A.lvalue) (is_var : bool) : A.lvalue =
       match !current_fundec with

[Gabriel Kerneis]

Good point. I'll just update the doc, then.

[Gabriel Kerneis]

No, updating the doc is not enough if the analyze_ functions are not exposed. Probably, then, the right thing is to call analyze_expr in analyze_stmt (for If, etc.). I'm a bit worried to miss some cases, it would be cleaner to use the visitor, but converting the code to visitor-style is not straightforward. If someone has a patch that solves this issue, I'd be glad to apply it. Otherwise, I'll try and fix it, but I'm don't feel very confident.

[Christoph L. Spiel]

Let me start with stating that it is very unfortunate that we are
mixing two problems in one issue report.

WRT the initial problem: The documentation is incomplete, calling just
Ptranal.analyze_file is not enough for a
points-to-analysis. Function Ptranal.compute_results
must be called before any query. See the very end of ptranal.ml.

The sure-fire way seems to be calling Ptranal.feature.Cil.fd_doit
with the file to analyze.

[Christoph L. Spiel]

WRT to the second problem:

Another problem is that even if I call compute_results, sometimes
calls to Ptranal.resolve_exp raise the Not_found exception, even for
expressions that appear in the program.

Could you please give us a minimal C-example program that reproduces the
error?