Loop bound estimation and loop abstraction?

[bitcalc]

Hi,

In the FSE2014 Corral paper, I see that Corral has implemented the loop abstraction and loop bound estimation. What options should I use to enable them?

I haven't found a Corral discussion place, so I am posting my question here, hoping that someone can direct me to the right place.

Thanks.

[zvonimir]

Corral folks will be more knowledgeable about this, but I believe that /maxStaticLoopBound:N achieves the latter (loop bound estimation), where N gives the upper bound on the estimated bounds (I think).
You can find all the flags listed here:
https://github.com/boogie-org/corral/blob/master/source/Configs.cs
I am not sure which one turns on loop abstraction.

[bitcalc]

I did a few tests and could confirm that the /maxStaticLoopBound:N triggers the loop bound estimation.

According to the paper, when the loop iterations become greater than 50 "chosen heuristically
to be 50" (Section 5) loop abstraction should be triggered. I tested the following loop with the iteration up to hundreds, but I couldn't see that the loop abstraction was used.

#include <stdlib.h>
#include "smack.h"

#define SIZE 1000

int main(int argc, char **argv) {
  int *a = malloc(SIZE * sizeof(int));
  for (int i = 0; i < SIZE; ++i) {
    if (i == SIZE - 2) {
      a[SIZE] = 0;
    }
  }
  free(a);
  return a[0];
}

[akashlal]

Only loop-bound estimation is implemented inside Corral. The loop abstraction is implemented outside, in the system that generates the boogie file for Corral.

[bitcalc]

Is there any tool that is publically available and implements the loop abstraction for Corral?

[akashlal]

I am not aware of anything available publically. Sorry.

…

On Thu, Dec 13, 2018, 22:24 bitcalc ***@***.*** wrote: Is there any tool that is publically available and implements the loop abstraction for Corral? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#80 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzIY2dsPnpR1tOW23TTqYCEeSTKIeJSks5u40QygaJpZM4ZQtL8> .

[bitcalc]

Does Windows SDK, Visual Studio, or any Microsoft product include a tool that does it? If so, what is the command name and arguments? I appreciate any information.