[BUG] Predicate not found

[podhrmic]

When running cn instrument -I. --include=../../include/wars.h --magic-comment-char-dollar trusted_boot.c I get the following error:

cn: internal error, uncaught exception:
    Failure("Predicate not found")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.cn_to_ail_resource_internal.calculate_return_type in file "backend/cn/lib/cn_internal_to_ail.ml", line 2578, characters 40-70
    Called from Cn__Cn_internal_to_ail.cn_to_ail_resource_internal.(fun) in file "backend/cn/lib/cn_internal_to_ail.ml", line 2594, characters 20-48
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", line 3297, characters 6-81
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3316-3322, characters 6-11
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3434-3440, characters 6-16
    Called from Cn__Executable_spec_internal.generate_c_pres_and_posts_internal in file "backend/cn/lib/executable_spec_internal.ml", lines 73-79, characters 4-30
    Called from Stdlib__List.map in file "list.ml", line 87, characters 15-19
    Called from Stdlib__List.map in file "list.ml", line 88, characters 14-21
    Called from Cn__Executable_spec_internal.generate_c_specs_internal in file "backend/cn/lib/executable_spec_internal.ml", line 201, characters 14-59
    Called from Cn__Executable_spec.main in file "backend/cn/lib/executable_spec.ml", lines 221-227, characters 4-11
    Called from Dune__exe__Main.generate_executable_specs.(fun) in file "backend/cn/bin/main.ml", lines 405-414, characters 10-26
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", lines 157-168, characters 6-48
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    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 35, characters 37-44
make: *** [Makefile:48: cn_instrument_trusted_boot] Error 125

Source here: trusted_boot.c (best to git clone whole OpenSUT repo).

Note that cn verify ... on the same file passes.

@ZippeyKeys12 suggested that this is related to using Alloc in the CN specs. After removing references to Alloc in trusted_boot.c I get the following error:

cn: internal error, uncaught exception:
    Failure("Not of correct form: more complicated RHS of binexpr than just i")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in file "backend/cn/lib/cn_internal_to_ail.ml", line 536, characters 11-86
    Called from Cn__Cn_internal_to_ail.cn_to_ail_resource_internal.(fun) in file "backend/cn/lib/cn_internal_to_ail.ml", line 2658, characters 21-61
    Called from Cn__Cn_internal_to_ail.cn_to_ail_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", line 3150, characters 6-81
    Called from Cn__Cn_internal_to_ail.cn_to_ail_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", line 3160, characters 17-64
    Called from Cn__Cn_internal_to_ail.cn_to_ail_post_internal in file "backend/cn/lib/cn_internal_to_ail.ml", line 3173, characters 15-62
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", line 3372, characters 27-73
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3301-3307, characters 6-15
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3316-3322, characters 6-11
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3434-3440, characters 6-16
    Called from Cn__Executable_spec_internal.generate_c_pres_and_posts_internal in file "backend/cn/lib/executable_spec_internal.ml", lines 73-79, characters 4-30
    Called from Stdlib__List.map in file "list.ml", line 86, characters 15-19
    Called from Stdlib__List.map in file "list.ml", line 88, characters 14-21
    Called from Cn__Executable_spec_internal.generate_c_specs_internal in file "backend/cn/lib/executable_spec_internal.ml", line 201, characters 14-59
    Called from Cn__Executable_spec.main in file "backend/cn/lib/executable_spec.ml", lines 221-227, characters 4-11
    Called from Dune__exe__Main.generate_executable_specs.(fun) in file "backend/cn/bin/main.ml", lines 405-414, characters 10-26
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", lines 157-168, characters 6-48
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    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 35, characters 37-44
make: *** [Makefile:48: cn_instrument_trusted_boot] Error 125

[ZippeyKeys12]

The second part is another case of #689

[rbanerjee20]

Thanks for flagging this. For the first part of the error, this is indeed related to Alloc which was introduced as part of VIP and the runtime testing does not yet contain a translation for this. As part of #723 there will be a temporary workaround for this merged into master, and we will return to implementing VIP as part of runtime testing properly in the future as it requires some thought.

For the second part, I suspect it is due to lines in the test file (e.g. this one) that contain conditions on i that are not just inequalities. Currently the runtime testing only supports conditions in iterated separating conjunctions that are pairs of inequalities, of the form i >= _ && i < _, for example. These each expressions are translated into while loops in C that require a start value for i, which is calculated from the condition which is expected to be of the described simple format.