From b4aa578616acaab35e8c5c8ca7f58cc971d0baf5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 13 Aug 2020 16:40:26 +0100 Subject: Finished all the proofs Removed support for case statements temporarily. --- src/translation/HTLgen.v | 5 ++-- src/translation/HTLgenproof.v | 68 +++++++++++++++++++++++-------------------- src/translation/HTLgenspec.v | 12 ++++---- 3 files changed, 46 insertions(+), 39 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 87a6de6..68e0293 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -478,8 +478,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni add_branch_instr e n n1 n2 else error (Errors.msg "State is larger than 2^32.") | Ijumptable r tbl => - do s <- get; - add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) + (*do s <- get; + add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) + error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => match r with | Some r' => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 6664617..403a97f 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -2327,39 +2327,47 @@ Section CORRECTNESS. Proof. intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. inv_state. - - eexists. split. apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. -(* eapply Verilog.stmnt_runp_Vnonblock_reg with - (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). - constructor. - - simpl. destruct b. - eapply Verilog.erun_Vternary_true. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - eapply Verilog.erun_Vternary_false. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - constructor. + - eexists. split. apply Smallstep.plus_one. + clear H33. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + econstructor; simpl; trivial. + constructor; trivial. + eapply Verilog.erun_Vternary_true; simpl; eauto. + eapply eval_cond_correct; eauto. intros. + intros. eapply RTL.max_reg_function_use. apply H22. auto. + econstructor. auto. + simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + apply AssocMap.gss. - big_tac. + inv MARR. inv CONST. + big_tac. + constructor; rewrite AssocMap.gso; simplify; try assumption; lia. + - eexists. split. apply Smallstep.plus_one. + clear H32. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + econstructor; simpl; trivial. + constructor; trivial. + eapply Verilog.erun_Vternary_false; simpl; eauto. + eapply eval_cond_correct; eauto. intros. + intros. eapply RTL.max_reg_function_use. apply H22. auto. + econstructor. auto. + simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + apply AssocMap.gss. - invert MARR. - destruct b; rewrite assumption_32bit; big_tac. + inv MARR. inv CONST. + big_tac. + constructor; rewrite AssocMap.gso; simplify; try assumption; lia. - Unshelve. - constructor. - Qed.*) - Admitted. + Unshelve. all: exact tt. + Qed. Hint Resolve transl_icond_correct : htlproof. - Lemma transl_ijumptable_correct: + (*Lemma transl_ijumptable_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) (n : Integers.Int.int) (pc' : RTL.node), @@ -2372,8 +2380,8 @@ Section CORRECTNESS. Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - Admitted. - Hint Resolve transl_ijumptable_correct : htlproof. + + Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma transl_ireturn_correct: forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) @@ -2674,5 +2682,3 @@ Section CORRECTNESS. Qed. End CORRECTNESS. - -Check transl_step_correct. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 93d5612..541f9fa 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -147,11 +147,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) -| tr_instr_Ijumptable : + (state_goto st n). +(*| tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) @@ -446,7 +446,7 @@ Proof. - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. - - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. + (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) Qed. Hint Resolve transf_instr_freshreg_trans : htlspec. @@ -551,12 +551,12 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. * inversion H14. constructor. congruence. * apply in_map with (f := fst) in H14. contradiction. - + *) + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. -- cgit