[BUG] CN crashes on a spec with a variably-sized array

[peterohanley]

Summary

A spec like Owned<char[2-i]>(...) seems to trigger various bugs inside CN. I wanted this to break multidimensional arrays apart along a line in the second dimension.

Bug

This file gets a stack trace:

guso@000492-guso src % cat stacktrace1.c 
void
g(char *x)
{
   for (int i = 0; i < 1; ++i)
    /*@ inv
        take tinv = Owned<char[2-i]>(x, j);
    @*/

    {
    }

}
guso@000492-guso src % cn stacktrace1.c 
internal error: TODO: failed to fetch object declaration ==> Symbol(489, SD_ObjectAddress"i")
cn: internal error, uncaught exception:
    Failure("internal error: TODO: failed to fetch object declaration ==> Symbol(489, SD_ObjectAddress\"i\")")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29
    Called from Dune__exe__Core_to_mucore.do_ail_desugar_op in file "backend/cn/core_to_mucore.ml", line 47, characters 8-23
    Called from Dune__exe__Core_to_mucore.do_ail_desugar_rdonly in file "backend/cn/core_to_mucore.ml", line 53, characters 16-49
    Called from Dune__exe__Core_to_mucore.desugar_cond in file "backend/cn/core_to_mucore.ml", line 1101, characters 15-70
    Called from Dune__exe__Core_to_mucore.desugar_conds.(fun) in file "backend/cn/core_to_mucore.ml", line 1116, characters 24-46
    Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
    Called from Dune__exe__Core_to_mucore.desugar_conds in file "backend/cn/core_to_mucore.ml", line 1115, characters 23-167
    Called from Dune__exe__Core_to_mucore.normalise_label in file "backend/cn/core_to_mucore.ml", line 1163, characters 32-54
    Called from Dune__exe__Core_to_mucore.normalise_label in file "backend/cn/core_to_mucore.ml", line 1157, characters 13-373
    Called from Dune__exe__Effectful.Make.PmapM.mapM.(fun) in file "backend/cn/effectful.ml", line 111, characters 20-25
    Called from Pmap.fold in file "pmap.ml", line 156, characters 15-38
    Called from Dune__exe__Core_to_mucore.normalise_fun_map_decl.(fun) in file "backend/cn/core_to_mucore.ml", line 1297, characters 13-286
    Called from Dune__exe__Core_to_mucore.make_largs.aux in file "backend/cn/core_to_mucore.ml", line 960, characters 16-26
    Called from Dune__exe__Core_to_mucore.make_function_args.aux in file "backend/cn/core_to_mucore.ml", line 1044, characters 18-87
    Called from Dune__exe__Core_to_mucore.make_function_args.aux in file "backend/cn/core_to_mucore.ml", line 1039, characters 9-101
    Called from Dune__exe__Core_to_mucore.normalise_fun_map_decl in file "backend/cn/core_to_mucore.ml", line 1289, characters 7-939
    Called from Dune__exe__Core_to_mucore.normalise_fun_map.(fun) in file "backend/cn/core_to_mucore.ml", line 1351, characters 15-193
    Called from Pmap.fold in file "pmap.ml", line 156, characters 15-38
    Called from Dune__exe__Core_to_mucore.normalise_fun_map in file "backend/cn/core_to_mucore.ml", line 1349, characters 2-759
    Called from Dune__exe__Core_to_mucore.normalise_file in file "backend/cn/core_to_mucore.ml", line 1511, characters 4-185
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 185, characters 22-116
    Re-raised at Dune__exe__Main.main in file "backend/cn/main.ml", line 231, characters 8-73
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, characters 37-44

This related file just gets caught by a not yet:

guso@000492-guso src % cat stacktrace1.c
void
f(char *x)
{
    int i= 0;
    while (i < 10)
    /*@ inv
        take tinv = Owned<char[2-i]>(x, j);
    @*/
    {
    }

}
guso@000492-guso src % cn stacktrace1.c 
unknown location  error: feature not yet supported: variable length array type 2

Perhaps the symbol could not be found because of something related to this error.

These would not be valid specs anyway, j is never defined, but it doesn't seem to be relevant.

Acceptance Criteria

Implement variable length arrays, or properly catch them in this case. If they remain not supported I would like the error to mention the location, to help if the file is large.

Do

• assign issue to a Milestone
• define acceptance criteria
• add appropriate labels
• Implement the feature or emit the feature not supported warning here

[PeterSewell]

it shouldn't crash, indeed - but that spec needs an iterated separating conjunction

…

On Tue, 18 Jun 2024 at 18:57, peterohanley ***@***.***> wrote: Summary A spec like Owned<char[2-i]>(...) seems to trigger various bugs inside CN. I wanted this to break multidimensional arrays apart along a line in the second dimension. Bug This file gets a stack trace: ***@***.*** src % cat stacktrace1.c void g(char *x) { for (int i = 0; i < 1; ++i) /*@ inv take tinv = Owned<char[2-i]>(x, j); @*/ { } } ***@***.*** src % cn stacktrace1.c internal error: TODO: failed to fetch object declaration ==> Symbol(489, SD_ObjectAddress"i") cn: internal error, uncaught exception: Failure("internal error: TODO: failed to fetch object declaration ==> Symbol(489, SD_ObjectAddress\"i\")") Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Cerb_frontend__State_exception.stExpect_bind in file "ocaml_frontend/generated/state_exception.ml", line 19, characters 24-29 Called from Dune__exe__Core_to_mucore.do_ail_desugar_op in file "backend/cn/core_to_mucore.ml", line 47, characters 8-23 Called from Dune__exe__Core_to_mucore.do_ail_desugar_rdonly in file "backend/cn/core_to_mucore.ml", line 53, characters 16-49 Called from Dune__exe__Core_to_mucore.desugar_cond in file "backend/cn/core_to_mucore.ml", line 1101, characters 15-70 Called from Dune__exe__Core_to_mucore.desugar_conds.(fun) in file "backend/cn/core_to_mucore.ml", line 1116, characters 24-46 Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34 Called from Dune__exe__Core_to_mucore.desugar_conds in file "backend/cn/core_to_mucore.ml", line 1115, characters 23-167 Called from Dune__exe__Core_to_mucore.normalise_label in file "backend/cn/core_to_mucore.ml", line 1163, characters 32-54 Called from Dune__exe__Core_to_mucore.normalise_label in file "backend/cn/core_to_mucore.ml", line 1157, characters 13-373 Called from Dune__exe__Effectful.Make.PmapM.mapM.(fun) in file "backend/cn/effectful.ml", line 111, characters 20-25 Called from Pmap.fold in file "pmap.ml", line 156, characters 15-38 Called from Dune__exe__Core_to_mucore.normalise_fun_map_decl.(fun) in file "backend/cn/core_to_mucore.ml", line 1297, characters 13-286 Called from Dune__exe__Core_to_mucore.make_largs.aux in file "backend/cn/core_to_mucore.ml", line 960, characters 16-26 Called from Dune__exe__Core_to_mucore.make_function_args.aux in file "backend/cn/core_to_mucore.ml", line 1044, characters 18-87 Called from Dune__exe__Core_to_mucore.make_function_args.aux in file "backend/cn/core_to_mucore.ml", line 1039, characters 9-101 Called from Dune__exe__Core_to_mucore.normalise_fun_map_decl in file "backend/cn/core_to_mucore.ml", line 1289, characters 7-939 Called from Dune__exe__Core_to_mucore.normalise_fun_map.(fun) in file "backend/cn/core_to_mucore.ml", line 1351, characters 15-193 Called from Pmap.fold in file "pmap.ml", line 156, characters 15-38 Called from Dune__exe__Core_to_mucore.normalise_fun_map in file "backend/cn/core_to_mucore.ml", line 1349, characters 2-759 Called from Dune__exe__Core_to_mucore.normalise_file in file "backend/cn/core_to_mucore.ml", line 1511, characters 4-185 Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 185, characters 22-116 Re-raised at Dune__exe__Main.main in file "backend/cn/main.ml", line 231, characters 8-73 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, characters 37-44 This related file just gets caught by a not yet: ***@***.*** src % cat stacktrace1.c void f(char *x) { int i= 0; while (i < 10) /*@ inv take tinv = Owned<char[2-i]>(x, j); @*/ { } } ***@***.*** src % cn stacktrace1.c unknown location error: feature not yet supported: variable length array type 2 Perhaps the symbol could not be found because of something related to this error. These would not be valid specs anyway, j is never defined, but it doesn't seem to be relevant. Acceptance Criteria Implement variable length arrays, or properly catch them in this case. If they remain not supported I would like the error to mention the location, to help if the file is large. Do - assign issue to a Milestone - define acceptance criteria - add appropriate labels - Implement the feature or emit the feature not supported warning here — Reply to this email directly, view it on GitHub <#101>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZS7I6AWNPLQE7RGN7DZIBYGPAVCNFSM6AAAAABJQQSHA6VHI2DSMVQWIX3LMV43ASLTON2WKOZSGM3DANBQGQYDQNY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>