Segmentation fault by minimize

[skcho]

Hello,

The following code, in which it tries to minimize an abstract value, failed with segmentation fault.

open Apron

let _ =
  let man = Elina_poly.manager_alloc_loose () in
  let env = Environment.make [||] [||] in
  let abs = Abstract1.top man env in
  Abstract1.minimize man abs

segmentation fault: 11

Same result in C.

#include <limits.h>
#include "ap_environment.h"
#include "ap_abstract1.h"
#include "opt_pk.h"

int main(int argc, char **argv){
  elina_manager_t* man = opt_pk_manager_alloc(false);
  ap_environment_t* env = ap_environment_alloc_empty();
  ap_abstract1_t abs = ap_abstract1_top(man, env);
  ap_abstract1_minimize(man, &abs);
  return 0;
}

I am suspecting there may be a type mismatch on registering the minimize function. The type of its argument is opt_pk_t*, not opt_pk_array_t*, though I am not sure this is the source of the crash.

void opt_pk_minimize(elina_manager_t* man, opt_pk_t* o);

[GgnDpSngh]

Hi,

The minimize function is just there as a placeholder. It is not supported by ELINA as the conversion algorithm already removes all redundant constraints/generators. What do you need it for?

Cheers,
Gagan

[skcho]

OK, I understand. 😄

What do you need it for?

I used Apron's octagon domain in our analyzer, at that time I needed the minimize function to keep small size of abstract states. Then, I simply changed the manager to Elina's, which triggered the issue.

the conversion algorithm already removes all redundant constraints/generators

If it already does the minimizations in another place, what about using a void function as the replaceholder, in order to avoid the segmentation faults. Of course, we can change our analyzer not to call the function when using Elina's domain. 😉

Sincerely,
Sungkeun

[GgnDpSngh]

Hi Sungkeun,

I changed the implementation so that it will not crash but also not do anything :). Let me know if it works. I am curious about the APRON's Octagon minimize() function because as far as I remember it is also a placeholder and does not do anything but maybe it changed in the newer version.

Cheers,
Gagan

[skcho]

Yes, you're right. What I have used is minimize_environment, which may not invoke the minimize function. I wrongly thought they are related... (I am sorry for that) and coincidently I succeeded to make the test case. 😓

Anyway, thank you for the fix!
Sungkeun