From 61b433cd903fa4182ae255f0f61f692eb163d677 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 19:57:56 +0100 Subject: remains one admit --- backend/CSE3proof.v | 54 +++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 46 insertions(+), 8 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3fbc9912..215f5c41 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -765,14 +765,52 @@ Proof. eapply external_call_sound; eauto with cse3. - (* Icond *) - 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. reflexivity. - * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. - eassumption. - * reflexivity. - + econstructor; eauto. - destruct b; IND_STEP. + destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND. + + econstructor; split. + * eapply exec_Inop; try eassumption. + TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. + * replace bfound with b. + { econstructor; eauto. + admit. + } + unfold find_cond_in_fmap in FIND_COND. + change RB.t with (option RELATION.t) in REL. + change Regmap.get with PMap.get in REL. + destruct (@PMap.get (option RELATION.t) pc + (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL. + 2: discriminate. + pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + destruct (is_condition_present pc rel cond args). + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + destruct (is_condition_present pc rel (negate_condition cond) args). + { 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. + } + 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. + + 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. + reflexivity. + ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + eassumption. + ** reflexivity. + * econstructor; eauto. + destruct b; IND_STEP. - (* Ijumptable *) econstructor. split. -- cgit 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 From d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 20:16:47 +0100 Subject: analysis with Abst_same --- backend/CSE3proof.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 7af62b95..9a55f529 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -449,6 +449,7 @@ Lemma step_simulation: exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. induction 1; intros S1' MS; inv MS. + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))). - (* Inop *) exists (State ts tf sp pc' rs m). split. + apply exec_Inop; auto. @@ -779,9 +780,14 @@ Proof. 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 + match + match (fst (preanalysis tenv f)) # pc with + | Some x => + apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x + | None => Abst_same RB.bot + end + with + | Abst_same rel' => rel' end) as INDUCTIVE by (destruct b; intuition). clear IND. -- cgit From 816ff701ed0e448fccf0b19cfc08a91ace49123d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 00:12:18 +0100 Subject: progress moving to list of items --- backend/CSE3proof.v | 273 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 208 insertions(+), 65 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 9a55f529..972cae5f 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -422,6 +422,7 @@ Qed. Hint Resolve sem_rel_b_top : cse3. +(* Ltac IND_STEP := match goal with REW: (fn_code ?fn) ! ?mpc = Some ?minstr @@ -442,20 +443,42 @@ Ltac IND_STEP := eapply rel_ge; eauto with cse3 (* ; for printing idtac mpc mpc' fn minstr *) end. - + *) + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. induction 1; intros S1' MS; inv MS. - all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))). + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *. + all: try set (invs := (fst (preanalysis tenv f))) in *. - (* Inop *) exists (State ts tf sp pc' rs m). split. + apply exec_Inop; auto. TR_AT. reflexivity. + econstructor; eauto. - IND_STEP. + + (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + unfold sem_rel_b. + apply (rel_ge inv_pc inv_pc'); auto. + (* END INVARIANT *) + - (* Iop *) exists (State ts tf sp pc' (rs # res <- v) m). split. + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. @@ -517,9 +540,28 @@ Proof. + econstructor; eauto. * eapply wt_exec_Iop with (f:=f); try eassumption. eauto with wt. - * IND_STEP. - apply oper_sound; eauto with cse3. - + * + (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload *) exists (State ts tf sp pc' (rs # dst <- v) m). split. + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. @@ -576,8 +618,27 @@ Proof. + econstructor; eauto. * eapply wt_exec_Iload with (f:=f); try eassumption. eauto with wt. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload notrap1 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. @@ -633,8 +694,27 @@ Proof. assumption. + econstructor; eauto. * apply wt_undef; assumption. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Iload notrap2 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. @@ -691,8 +771,27 @@ Proof. assumption. + econstructor; eauto. * apply wt_undef; assumption. - * IND_STEP. - apply oper_sound; eauto with cse3. + * (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Istore *) exists (State ts tf sp pc' rs m'). split. @@ -705,8 +804,27 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - IND_STEP. - apply store_sound with (a0:=a) (m0:=m); eauto with cse3. + (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply store_sound with (a0:=a) (m0:=m); unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Icall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. @@ -721,9 +839,29 @@ Proof. * econstructor; eauto. ** rewrite sig_preserved with (f:=fd); assumption. ** intros. - IND_STEP. - apply kill_reg_sound; eauto with cse3. - eapply kill_mem_sound; eauto with cse3. + + (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + { apply kill_reg_sound; unfold ctx; eauto with cse3. + eapply kill_mem_sound; unfold ctx; eauto with cse3. } * rewrite sig_preserved with (f:=fd) by trivial. rewrite <- H7. apply wt_regset_list; auto. @@ -761,54 +899,48 @@ Proof. * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. - * IND_STEP. - apply kill_builtin_res_sound; eauto with cse3. - eapply external_call_sound; eauto with cse3. + * (* 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. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + + apply kill_builtin_res_sound; unfold ctx; eauto with cse3. + eapply external_call_sound; unfold ctx; eauto with cse3. - (* Icond *) - destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND. + destruct (find_cond_in_fmap (ctx := ctx) invs pc cond args) as [bfound | ] eqn:FIND_COND. + econstructor; split. * eapply exec_Inop; try eassumption. - TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. + TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - 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 - match (fst (preanalysis tenv f)) # pc with - | Some x => - apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x - | None => Abst_same RB.bot - end - with - | Abst_same rel' => rel' - 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. + admit. } - unfold find_cond_in_fmap in FIND_COND. - change RB.t with (option RELATION.t) in REL. - change Regmap.get with PMap.get in REL. - destruct (@PMap.get (option RELATION.t) pc - (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL. - 2: discriminate. + unfold sem_rel_b in REL. + destruct (invs # pc) as [rel | ] eqn:FIND_REL. + 2: contradiction. pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE. pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE. rewrite eval_negate_condition in COND_PRESENT_FALSE. + unfold find_cond_in_fmap in FIND_COND. + change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND. + rewrite FIND_REL in FIND_COND. destruct (is_condition_present pc rel cond args). { rewrite COND_PRESENT_TRUE in H0 by trivial. congruence. @@ -834,7 +966,8 @@ Proof. congruence. } unfold fmap_sem. - change RB.t with (option RELATION.t). + unfold sem_rel_b. + fold invs. rewrite FIND_REL. exact REL. } @@ -850,20 +983,22 @@ Proof. destruct b; trivial; cbn in H2; discriminate. } unfold fmap_sem. - change RB.t with (option RELATION.t). + unfold sem_rel_b. + fold invs. 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. + ** TR_AT. unfold transf_instr. fold invs. fold ctx. + rewrite FIND_COND. reflexivity. ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. eassumption. ** reflexivity. * econstructor; eauto. - destruct b; IND_STEP. + admit. - (* Ijumptable *) econstructor. split. @@ -872,8 +1007,7 @@ Proof. * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. - assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption). - IND_STEP. + admit. - (* Ireturn *) destruct or as [arg | ]. @@ -915,9 +1049,18 @@ Proof. apply wt_init_regs. rewrite <- wt_params in WTARGS. assumption. - * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))). - ** apply sem_rel_b_top. - ** apply transf_function_invariants_inductive with (tf:=tf); auto. + * assert ((check_inductiveness f tenv (fst (preanalysis tenv f)))=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]. + clear IND_step. + apply RB.beq_correct in IND_entry. + unfold RB.eq in *. + destruct ((fst (preanalysis tenv f)) # (fn_entrypoint f)). + 2: contradiction. + cbn. + rewrite <- IND_entry. + apply sem_rel_top. - (* external *) simpl in FUN. @@ -935,7 +1078,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Qed. +Admitted. Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> -- cgit From b4af6cbe24b1108b4e49d3c17fecc37255bd6151 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:07:32 +0100 Subject: avancement dans les preuves --- backend/CSE3proof.v | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 972cae5f..69e779cd 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -930,7 +930,40 @@ Proof. TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { 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 andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. + 2: discriminate. + destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. + 2: discriminate. + rewrite rel_leb_correct in IND_so. + rewrite rel_leb_correct in IND_not. + destruct b. + { + rewrite INV_so. + cbn. + eapply rel_ge; eauto. + } + { + rewrite INV_not. + cbn. + eapply rel_ge; eauto. + } + (* END INVARIANT *) } unfold sem_rel_b in REL. destruct (invs # pc) as [rel | ] eqn:FIND_REL. -- cgit From 8f2cf0b53b3a7fd4bc339fddf89197601eb549c2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:13:40 +0100 Subject: one 'admit' less --- backend/CSE3proof.v | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 69e779cd..661329e8 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -930,7 +930,7 @@ Proof. TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - (* BEGIN INVARIANT *) + (* 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. @@ -1031,7 +1031,41 @@ Proof. eassumption. ** reflexivity. * 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 andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. + 2: discriminate. + destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. + 2: discriminate. + rewrite rel_leb_correct in IND_so. + rewrite rel_leb_correct in IND_not. + destruct b. + { + rewrite INV_so. + cbn. + eapply rel_ge; eauto. + } + { + rewrite INV_not. + cbn. + eapply rel_ge; eauto. + } + (* END INVARIANT *) - (* Ijumptable *) econstructor. split. -- cgit From 04667b444164f8a54c1aab0a8e2422e1951bf9bc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:47:24 +0100 Subject: proof for jumptable --- backend/CSE3proof.v | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) (limited to 'backend/CSE3proof.v') 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 | ]. -- cgit From 79c039d7b33878d00f22ad8542dc30a78aa8b70a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 11:34:35 +0100 Subject: CSE3 + conditions proof --- backend/CSE3proof.v | 67 +++++++++++++++++++++++++++-------------------------- 1 file changed, 34 insertions(+), 33 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index cc4ab686..50a32d56 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -352,6 +352,23 @@ Qed. Hint Resolve rel_ge : cse3. +Lemma relb_ge: + forall inv inv' + (GE : RB.ge inv' inv) + ctx sp rs m + (REL: sem_rel_b sp ctx inv rs m), + sem_rel_b sp ctx inv' rs m. +Proof. + intros. + destruct inv; cbn in *. + 2: contradiction. + destruct inv'; cbn in *. + 2: assumption. + eapply rel_ge; eassumption. +Qed. + +Hint Resolve relb_ge : cse3. + Lemma sem_rhs_sop : forall sp op rs args m v, eval_operation ge sp op rs ## args m = Some v -> @@ -946,23 +963,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) } unfold sem_rel_b in REL. @@ -1048,23 +1057,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) - (* Ijumptable *) @@ -1171,7 +1172,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Admitted. +Qed. Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> -- cgit From eb1121d703835e76babc15b057276d2852ade4ab Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 16:25:46 +0100 Subject: totally switch off conditions in cse3 --- backend/CSE3proof.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 50a32d56..ca43d0bd 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -983,6 +983,8 @@ Proof. unfold find_cond_in_fmap in FIND_COND. change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND. rewrite FIND_REL in FIND_COND. + destruct (Compopts.optim_CSE3_conditions tt). + 2: discriminate. destruct (is_condition_present pc rel cond args). { rewrite COND_PRESENT_TRUE in H0 by trivial. congruence. -- cgit