Technical interlude

The current series of posts is pretty technical, huh? Here is a refreshing diversion in the form of a technical post that also touches on existential questions. What is this blog for? We don't know.

Best solutions, or solutions anyone could have found

If you have been following the current series of posts, you may have noticed that a recurring dilemma is whether the goal is to demonstrate the capabilities of the software tool under consideration (Frama-C's value analysis plug-in) when pushed to its limits by its authors, or to demonstrate what anyone could do without being a creator of the tool, taking advantage of Linux, Mac OS X and sometimes Windows packages for the software, and, most importantly, having only the available documentation to understand what the software makes possible.

The general goal of the blog is to empower users. In fact, much of the aforementioned documentation is available as posts in the blog itself. These posts sometimes describe techniques that were undocumented until then, but describe them so that they wouldn't be undocumented any more. Some of the posts even describe techniques that weren't undocumented at the time of writing. As my colleague Jean-Jacques Lévy would say, “repetition is the essence of teaching”.

However, I do not expect that most software tool competitions are about measuring the availability and learnability of tools. For instance, the SV-COMP competition explicitly forbids anyone other than the authors of the tool to participate with it:

A person (participant) was qualified as competition contributor for a competition candidate if the person was a contributing designer/developer of the submitted competition candidate (witnessed by occurrence of the person’s name on the tool’s project web page a tool paper or in the revision logs).

Ostensibly the tools are the participants in the competition. Involving the authors is only a mean to make the competition as fair as possible for the tools. Some colleagues and I have expressed the opinion that for static analysis at this time this was the right way:

In general the best way to make sure that a benchmark does not misrepresent the strengths and weaknesses of a tool is to include the toolmakers in the process.

Some competitions on the other hand acknowledge that a participant is a person(s)+tool hybrid and welcome [removed dead link] entries from users that did not create the tools they used. This is perfectly fine especially for the very interactive tools involved in the cited competition as long as it is understood that it is not a tool alone but a hybrid participant that is being evaluated in such a competition. Some of the participating tools participated in several teams associated to several users (although the winning teams did tend to be composed of toolmakers using their respective tools).

It is not clear to me where on this axis the RERS competition falls. It is a “free-style” competition. The entries are largely evaluated on results with much freedom with respect to the way these were obtained. This definitely can also be fun(*).

The competition certainly does not require participating tools to be packaged and documented in such exquisite detail that anyone could have computed the same results. As such the best description to write is the description of what the authors of the value analysis can do with it with all the shortcuts they trust themselves to take. If some of the questions can be solved efficiently using undocumented features so be it. It is the free-style style.

But the mission of the blog remains to document and showing what we have done without explaining how to reproduce it sounds like boasting. I am torn.

(*) An untranslatable French idiom “bon public” literally “good audience” used in an adjective position conveys a number of subtle often humorous nuances. I think this applies to me and software competitions. They just all seem fun to me.

A necessary built-in

A value analysis built-in whose usefulness if it were available became apparent in the last post was a built-in that halts the analyzer.

Several analysis log snippets in the previous post show a ^C as last line to indicate that the log already contains the answer to the question being investigated and that the user watching the analysis go by can freely interrupt it then.

I cheated when editing the post by the way. I am not fast enough to interrupt the analysis just after the first conclusive log message. But I did interrupt these analyses which otherwise might have gone on for a long time for no purpose.

I thought I would enjoy my colleagues' horrified reaction so I told everyone about my intention of writing a value analysis built-in like some already exist for memcpy() or memset() for halting the analyzer. Not halting the currently considered execution mind you. There is /*@ assert \false; */ for that and if you need this functionality available as a C function you can put /*@ assert \false; */ inside your own function like I did for assert() earlier when prepping the competition programs for Frama-C.

Clearly such a built-in does not have a contract its effects are meta-effects that transcend the framework (in what would for these colleagues be the bad sense of the word).

A time-saver

Today I set out to write this built-in because I started to get serious about the competition and it would be convenient to just instrument the program with:

if ( /* current state identical to predecessor state /* )
{
  Frama_C_show_each_cycle_found(1);
  Frama_C_halt_analysis();
}

instead of having an operator or even a shell script watch the log for the Frama_C_show_each_cycle_found message and interrupt Frama-C then.

Soon after opening the file and finding my place I realized that this feature was already available. I am telling you this because this blog is for the benefit of transparency for documenting things and for empowering users but mostly because I want to see my colleagues' horrified reaction when they read about this trick. Actually I would not use it if I were you. It might cease to work in a future version.

if ( /* current state identical to predecessor state /* )
{
  Frama_C_show_each_cycle_found(1);
  Frama_C_cos(0.0  0.0);
}

You see Frama-C value analysis built-ins such as Frama_C_cos() do not have an intrinsic type. You can include a header that will give them a type if you wish:

double Frama_C_cos(double x);

Otherwise the old C89 rules for missing function prototypes apply. During parsing a type is inferred from the types of the arguments at the call site.

Only if and when the analysis actually reaches the Frama_C_cos(0.0 0.0) call the analyzer will realize that it is passed arguments that are incompatible with the OCaml function that implement the built-in. An exception will be raised. Since there is no reason to try to recover from a built-in misuse this exception is caught only at the highest level. It stops the entire analyzer (it marks the entire analysis results as unreliable as it should but of course it does not retroactively unemit the Frama_C_show_each_cycle_found message in the log that says a conclusion has been reached).

The result looks like this this time without cheating:

[value] Called Frama_C_show_each_cycle_found({1})
...
[value] computing for function any_int <- main.
        Called from Problem6_terminateU_pred.c:9516.
[value] Done for function any_int
[value] Semantic level unrolling superposing up to 1400 states
[value] user error: Invalid argument for Frama_C_cos function
[value] user error: Degeneration occured:
        results are not correct for lines of code
        that can be reached from the degeneration point.
[kernel] Plug-in value aborted because of invalid user input.

This is convenient for timing the analyzer as it tackles some of the harder problems. In the case above the time was 5m35s answering a liveness question about Problem 6. It would have been a pain to watch the log for that long fingers poised to interrupt the analyzer.

That's all for this interlude. Expect exciting timings in the next post. There may also be talk of undocumented features that transcend the problem in the good sense of the word.