From 3570ba2827908b280315c922ba7e43289f6d802a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 22:12:38 +0100 Subject: not yet the transfer functions that record predicates --- backend/CSE3proof.v | 61 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 54 insertions(+), 7 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 215f5c41..7af62b95 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -771,7 +771,28 @@ Proof. TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - admit. + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst (preanalysis tenv f))) as IND by + (apply checked_is_inductive_allstep; + eapply transf_function_invariants_inductive; eassumption). + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. + specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)). + cbn in IND. + rewrite H in IND. + assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) + match (fst (preanalysis tenv f)) # pc with + | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x + | None => None + end) as INDUCTIVE by (destruct b; intuition). + clear IND. + + change node with positive. + + destruct ((fst (preanalysis tenv f)) # pc). + 2: exfalso; exact REL. + + destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)). + - eapply rel_ge. exact INDUCTIVE. exact REL. + - cbn in INDUCTIVE. exfalso. exact INDUCTIVE. } unfold find_cond_in_fmap in FIND_COND. change RB.t with (option RELATION.t) in REL. @@ -796,12 +817,38 @@ Proof. inv FIND_COND. destruct b; trivial; cbn in H2; discriminate. } - rewrite <- subst_args_ok with (invariants := (fst (preanalysis tenv f))) (ctx := (context_from_hints (snd (preanalysis tenv f)))) (pc := pc) (sp:=sp) (m:=m) in COND_PRESENT_TRUE. - admit. - unfold fmap_sem. - change RB.t with (option RELATION.t). - rewrite FIND_REL. - exact REL. + clear COND_PRESENT_TRUE COND_PRESENT_FALSE. + pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE. + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE. + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + discriminate. + econstructor; split. * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. ** TR_AT. unfold transf_instr. rewrite FIND_COND. -- cgit