[WP] Assertion failed in Instance tactic called from a custom strategy
Steps to reproduce the issue
I tried to narrow down the example, but it's hard to determine where is the problem exactly. I have an example file foo_lemma.c and a custom strategy plugin strategy_foo.ml.
Essentially the strategy tries to guide the solvers by finding witnesses in the hypotheses to instantiate existentially quantified predicates in the goal. It follows the iterative nature of the T
predicates by unfolding them one step at a time until success. As recommended by the WP manual, the custom strategy only uses pre-defined tactics (namely Definition and Instance).
Launch frama-c -wp -load-module strategy_foo.ml -wp-auto Foo:T foo_lemma.c
.
Expected behaviour
Frama-C should prove the lemma or at least not fail.
Actual behaviour
Frama-C fails with the following error:
[wp] foo_lemma.c:55: Warning:
[Instance] Exception <File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed>
[kernel] Current source was: foo_lemma.c:55
The full backtrace is:
Raised at ProverSearch.fork in file "src/plugins/wp/ProverSearch.ml", line 57, characters 6-13
Called from ProverSearch.lookup in file "src/plugins/wp/ProverSearch.ml", line 62, characters 10-33
Called from ProverSearch.first in file "src/plugins/wp/ProverSearch.ml", line 84, characters 25-54
Called from ProverScript.Env.search in file "src/plugins/wp/ProverScript.ml", line 192, characters 12-62
Called from ProverScript.autosearch in file "src/plugins/wp/ProverScript.ml", line 299, characters 8-34
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.progress in file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
Called from Task.progress in file "src/libraries/utils/task.ml", line 363, characters 14-36
Re-raised at Task.progress in file "src/libraries/utils/task.ml", line 369, characters 6-13
Called from Task.server_progress.(fun) in file "src/libraries/utils/task.ml", line 475, characters 14-27
Called from Stdlib__list.find_all.find in file "list.ml", line 242, characters 17-20
Called from Task.server_progress in file "src/libraries/utils/task.ml", line 473, characters 22-273
Called from Task.on_idle.(fun) in file "src/libraries/utils/task.ml", line 344, characters 14-18
Called from Register.do_wp_proofs in file "src/plugins/wp/register.ml", line 656, characters 4-33
Called from Register.cmdline_run in file "src/plugins/wp/register.ml", line 722, characters 8-26
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 14-17
Re-raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
Called from Stdlib__queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
Additional information
I tried to see if the error would raise in GUI mode by manually activating the custom tactics in the editor instead of using -wp-auto Foo:T
:
frama-c-gui -wp -load-module strategy_foo.ml foo_lemma.c
It turns out that it won't raise an error dialog, but the following stderr message ** (frama-c-gui:426361): CRITICAL **: 17:47:51.667: GSourceFunc: callback raised an exception
, and the GUI remains in a somewhat stuck state.
This could be another issue by itself maybe.
I tracked down the error: the assertion fails here (qed/term.ml:2516
), from the call here (wp/TacInstance.ml:163
).
It seems that for some reason (maybe related to the way I wrote my tactic?), the variable x
chosen to unbind phi
actually is not fresh (enough).
On a local version of Frama-C I tried to replace the code at line 157 with the following:
let pool = F.pool ~copy:env.feedback#pool () in
List.iter (F.add_var pool) (F.e_vars (F.QED.lc_repr phi));
let x = F.fresh pool tau in
Basically I'm force-ensuring that the subsequent assertion will not fail, and this seems to solve the problem, as far as I can tell.