Use after free in opt_pk_assign.c

[skcho]

Hello Gagan,

I encountered a use-after-free error in opt_pk_assign.c:1220. In my testing, it looks like op->acl->size is freed at line 1215 (by making abs to bottom I think), then is used at line 1220.

https://github.com/eth-sri/ELINA/blob/dc60b03c7f84865dca78acee351c2593c712031b/elina_poly/opt_pk_assign.c#L1214-L1220

The test code is:

open Apron

let _ =
  let man = Elina_poly.manager_alloc_loose () in
  let a = Var.of_string "a" in
  let env = Environment.make [|a|] [||] in
  let abs = Abstract1.top man env in
  let vars = [|a|] in
  let texprs = [|Parser.texpr1_of_string env "(1-a)*a"|] in
  Abstract1.assign_texpr_array man abs vars texprs None

Message from ASAN is:

AddressSanitizer: heap-use-after-free
READ of size 2 at 0x602000000f38 thread T0
    #0 opt_poly_asssub_texpr_array opt_pk_assign.c:1220
    #1 opt_pk_assign_texpr_array opt_pk_assign.c:1325
    #2 ap_abstract0_asssub_texpr_array ap_abstract0.c:1139
    #3 ap_abstract1_asssub_texpr_array ap_abstract1.c:931
    #4 ap_abstract1_assign_texpr_array ap_abstract1.c:958
    #5 camlidl_abstract1_ap_abstract1_assign_texpr_array abstract1_caml.c:1200
    #6 camlAssign_texpr__entry (assign_texpr.native:x86_64+0x100003d38)

freed by thread T0 here:
    #0 wrap_free (libclang_rt.asan_osx_dynamic.dylib:x86_64h+0x56e8d)
    #1 free_array_comp_list array_comp_list.c:52
    #2 opt_poly_array_clear opt_pk_representation.c:91
    #3 opt_poly_set_bottom opt_pk_constructor.c:47
    #4 opt_pk_meet_lincons_array_cons opt_pk_meetjoin.c:425
    #5 opt_pk_meet_lincons_array opt_pk_meetjoin.c:724
    #6 elina_generic_meet_intlinearize_tcons_array elina_generic.c:223
    #7 opt_pk_meet_tcons_array opt_pk_meetjoin.c:736
    #8 elina_generic_asssub_texpr_array elina_generic.c:506
    #9 opt_poly_asssub_texpr_array opt_pk_assign.c:1215
    #10 opt_pk_assign_texpr_array opt_pk_assign.c:1325
    #11 ap_abstract0_asssub_texpr_array ap_abstract0.c:1139
    #12 ap_abstract1_asssub_texpr_array ap_abstract1.c:931
    #13 ap_abstract1_assign_texpr_array ap_abstract1.c:958
    #14 camlidl_abstract1_ap_abstract1_assign_texpr_array abstract1_caml.c:1200
    #15 camlAssign_texpr__entry (assign_texpr.native:x86_64+0x100003d38)

Sincerely, Sungkeun Cho

[GgnDpSngh]

Hi Sungkeun,

Thanks for this interesting test case. Looking at the trace, I think the bug may be elsewhere as the output of an assignment should not be bottom if the input is not bottom. I will check and let you know.

Cheers, Gagan

[GgnDpSngh]

Hi Sungkeun,

I have fixed the bug, it was in the handling of interval linear expressions with zero variables in the function "meet_lincons_array". There was an incorrect assumption that the coefficients can only be scalars whereas your expression generates the interval expression [-oo,+oo]=0. Thank you very much for spotting this bug.

Cheers, Gagan

[skcho]

Thank you Gagan. 😄 I will try that.

Sincerely, Sungkeun