GitLab

It only works correctly if both profiling and static prediction are
used: it then compares both and gives stats in COMPCERT_PREDICT_STATS
file.

The stats are of the form:
  total correct mispredicts missed

total = number of total CBs encountered
correct = number of correct predictions
mispredicts = times when static prediction did a wrong guess (predicted
    the opposite from profiling, or predicted Some _ when profiling said
    None)
missed = times when static prediction was not able to give a verdict,
       though the profiling gave one

Another remnant of trying to devise a complicated algorithm for a
problem that was, in fact, very simple: I just had to check whether the
branch was within the loop body.

I tested it functionally on the benchmarks: only heapsort is changed, in
slightly worst (4-5%), because the old get_loop_info had done a buggy
guess that proved to be lucky for that particular case.

The other benchmarks are unchanged: the predictions stay the exact same.

The get_loop_info could potentially be improved by having a natural loop
detection that extends to outer loops (not just inner loops), though I
expect the performance improvements would be very small.

Note : the issue is still present later in Duplicateproof. This is
because I am examining an "identity ptree" which is way too big. I am
having a look to see if I could make this ptree less big - to not
include nodes that are identity

Loops with multiple CBs were only partially predicted for some cases
(the header CB would get predicted, but not the CBs inside)

This would happen in the case of breaks leading to another loop, such
as:

```c
void lift_check_level()
{
  int i;
  int middle = lift_one_level >> 2;
  if ( lift_cntValid ) {

    for ( lift_level = 1; lift_level < 14; ++lift_level ) {
      if ( lift_cnt < lift_levelPos[lift_level] - middle )
        break; /* This break */
    }
  } else
    lift_level = 0;

  for ( i = 0; i < 14; ++i )
    lift_ctrl_io_led[i] = ( i == lift_level - 1 );
}
```

Various typos made the code fail silently for certain loops

It was too permissive

In some cases of two imbricated loops, we would tail-duplicate too much,
because of the input trace traversing both loop headers.

Happened when a loop was predicted not to be taken

Right now though the compilation time is too high for glpk, I need to
figure out why