search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

quick_typecheck3 should not clear #722

Closed andrew-appel closed 9 months ago

andrew-appel commented 9 months ago

Coq issue 18049 made it apparent that there is a bad interaction between Floyd internal tactic quick_typecheck3 and Floyd tactic unlocalize, especially starting in Coq 8.17. In this version of Coq, auto is slightly more powerful, which causes quick_typecheck3 to succeed in certain cases where it failed in Coq 8.16 and before. This should be a good thing, but it uncovered this bad interaction.

To solve the problem, it is best if quick_typecheck3 and default_entailer_for_load_store do not clear anything from above the line. The following workaround will work in VST 2.12 for Coq 8.17. Presumably this should be the standard behavior of these tactics in the next release of VST.

Ltac quick_typecheck3 ::=
 apply quick_derives_right; go_lowerx; intros;
 repeat apply andp_right; auto; fail.

Ltac default_entailer_for_load_store ::=
  try quick_typecheck3;
  unfold tc_efield, tc_LR, tc_LR_strong; simpl typeof;
  try solve [entailer!].

I have not yet tested this exhaustively, which is why it's an issue report rather than a pull request.

andrew-appel commented 9 months ago

The nature of the bad interaction is this: If there are unification variables in the context, caused by using the localize tactic before doing the forward that calls default_entailer_for_load_store, then clearing these variables will cause problems for the unlocalize tactic when that tactic calls refine.

andrew-appel commented 9 months ago

Closed by #723