diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 09:47:24 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 09:50:05 +0100 |
commit | 04667b444164f8a54c1aab0a8e2422e1951bf9bc (patch) | |
tree | 0ce762a4cd160583f52533ac4f4c7e3bc2ea90fd | |
parent | 8f2cf0b53b3a7fd4bc339fddf89197601eb549c2 (diff) | |
download | compcert-kvx-04667b444164f8a54c1aab0a8e2422e1951bf9bc.tar.gz compcert-kvx-04667b444164f8a54c1aab0a8e2422e1951bf9bc.zip |
proof for jumptable
-rw-r--r-- | backend/CSE3proof.v | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 661329e8..cc4ab686 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -1074,7 +1074,33 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - admit. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite forallb_forall in IND_step_me. + assert (RB.ge (invs # pc') (Some inv_pc)) as GE. + { + apply relb_leb_correct. + specialize IND_step_me with (pc', Some inv_pc). + apply IND_step_me. + apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))). + eapply list_nth_z_in. + eassumption. + } + destruct (invs # pc'); cbn in *. + 2: contradiction. + eapply rel_ge; eauto. + (* END INVARIANT *) - (* Ireturn *) destruct or as [arg | ]. |