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/CSE3analysis.v | 50 ++++---- backend/CSE3analysisproof.v | 2 + backend/CSE3proof.v | 273 +++++++++++++++++++++++++++++++++----------- 3 files changed, 233 insertions(+), 92 deletions(-) (limited to 'backend') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8cfbaaa1..46ae4aea 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -127,9 +127,6 @@ End RELATION. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). -Inductive abst_insn_out := -| Abst_same : RB.t -> abst_insn_out. - Inductive sym_op : Type := | SOp : operation -> sym_op | SLoad : memory_chunk -> addressing -> sym_op. @@ -464,28 +461,29 @@ Section OPERATIONS. | _ => rel end. - Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out := + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with - | Inop _ - | Icond _ _ _ _ _ - | Ijumptable _ _ => Abst_same (Some rel) - | Istore chunk addr args src _ => - Abst_same (Some (store tenv chunk addr args src rel)) - | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel)) - | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel)) - | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel))) - | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel))) - | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot + | Inop pc' => (pc', (Some rel))::nil + | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil + | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets + | Istore chunk addr args src pc' => + (pc', (Some (store tenv chunk addr args src rel)))::nil + | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil + | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil + | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil + | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil + | Itailcall _ _ _ | Ireturn _ => nil end. End PER_NODE. -Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out := - match ro with - | None => Abst_same RB.bot - | Some x => - match code ! pc with - | None => Abst_same RB.bot - | Some instr => apply_instr pc tenv instr x +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : + list (node * RB.t) := + match code ! pc with + | None => nil + | Some instr => + match ro with + | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr) + | Some x => apply_instr pc tenv instr x end end. @@ -507,12 +505,10 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva match PMap.get pc inv with | None => true | Some rel => - match apply_instr pc tenv instr rel with - | Abst_same rel' => - List.forallb - (fun pc' => relb_leb rel' (PMap.get pc' inv)) - (RTL.successors_instr instr) - end + List.forallb + (fun szz => + relb_leb (snd szz) (PMap.get (fst szz) inv)) + (apply_instr pc tenv instr rel) end). (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 10ffe760..8cc009cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1288,6 +1288,7 @@ Section SOUNDNESS. Hint Resolve external_call_sound : cse3. + (* Section INDUCTIVENESS. Variable fn : RTL.function. Variable tenv : typing_env. @@ -1348,4 +1349,5 @@ Section SOUNDNESS. End INDUCTIVENESS. Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3. + *) End SOUNDNESS. 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