Buffer overrun error in opt_pk_add_dimensions_cons about elina HOT 10 CLOSED

Made better fix, it should be fine now.

Cheers,
Gagan

from elina.

I fixed this, thanks for spotting, this is similar to the first one, I will check if there are other parts in the code where it can also occur.

Cheers,
Gagan

from elina.

Hi Sungkeun,

Thanks for your feedback. This is weird and there should not be any buffer overrun there. Do you have the exact test case when it crashes?

Cheers,
Gagan

from elina.

Hi Gagan,

open Apron

let () =
  let man = Elina_poly.manager_alloc_loose () in
  let abs = Abstract1.top man (Environment.make [||] [||]) in
  let env = Environment.make [|Var.of_string "x"|] [||] in
  ignore (Abstract1.change_environment man abs env false)

It has the buffer overrun behavior, though it would not make an explicit crash at this point. By adding the following lines before the line 110 of opt_pk_resize.c, you can see it actually accesses invalid heap memory, i.e., dim[1].

fprintf(stderr, "dim size %u\n", size);
fprintf(stderr, "access dim[%u]\n", l);
fflush(stderr);

results:

dim size 1
access dim[1]

Sincerely,
Sungkeun

from elina.

Hi Sungkeun,

Thanks for spotting it, I have made a "quick" fix. Have not tested it properly and not sure if it breaks other things. Let me know if it there are further issues.

Cheers,
Gagan

from elina.

Hi Gagan,
Thank you! I will try it.
Sungkeun

from elina.

Hi Gagan,

I think I found another similar buffer overrun in opt_pk_resize.c:318.

Test code is:

open Apron

let () =
  let man = Elina_poly.manager_alloc_loose () in
  let x = Var.of_string "x" in
  let y = Var.of_string "y" in
  let env = Environment.make [|x; y|] [||] in
  let tab = Parser.lincons1_of_lstring env ["y>=0"] in
  let abs = Abstract1.of_lincons_array man env tab in
  ignore (Abstract1.minimize_environment man abs)

As the above one, it would not raise an explicit crash. If I add the following print functions before the line 318:

fprintf(stderr, "dima size %u\n", dimchange->intdim+dimchange->realdim);
fprintf(stderr, "access dima[%u]\n", l);
fflush(stderr);

Results:

dima size 1
access dima[0]
dima size 1
access dima[1]

FWIW, the call stack given by address sanitizer is:

ERROR: AddressSanitizer: heap-buffer-overflow
    #0 opt_pk_remove_dimensions opt_pk_resize.c:318
    #1 ap_abstract0_remove_dimensions ap_abstract0.c:1260
    #2 ap_abstract0_apply_dimchange2 ap_abstract0.c:1507
    #3 ap_abstract1_change_environment ap_abstract1.c:1019
    #4 ap_abstract1_minimize_environment ap_abstract1.c:1057
    #5 camlidl_abstract1_ap_abstract1_minimize_environment abstract1_caml.c:1669

Thank you, Gagan!
Sungkeun

from elina.

Thank you, Gagan. I will try it.

Sincerely,
Sungkeun

from elina.

Let me know, I made a scan through the code and did not see this pattern elsewher but who knows maybe you find something soon :). I am on the move today but will try to fix any potential bugs whenever i get time.

Cheers,
Gagan

from elina.

Thank you for your quick response. 😄 It looks OK as of now. I will reopen the issue if I find a similar one. Hope your move well.

Sincerely,
Sungkeun

from elina.