From 128b5d3a20647db3d0b17cc918d17fe5cadc07ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 23:27:05 +0100 Subject: Add top level backward simulation --- src/Compiler.v | 127 ++++++++++++++++++++++++++++++----- src/translation/HTLgenproof.v | 149 ++++++++++++++++++++++-------------------- src/verilog/ValueInt.v | 10 +-- 3 files changed, 191 insertions(+), 95 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index 17d8921..05353f9 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -16,6 +16,8 @@ * along with this program. If not, see . *) +From coqup Require Import HTLgenproof. + From compcert.common Require Import Errors Linking. @@ -49,8 +51,9 @@ From coqup Require Verilog Veriloggen Veriloggenproof - HTLgen - HTLgenproof. + HTLgen. + +From compcert Require Import Smallstep. Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. @@ -85,7 +88,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print print_HTL @@ Veriloggen.transl_program. -Definition transf_frontend (p: Csyntax.program) : res RTL.program := +Check mkpass. + +Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -93,11 +98,6 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program - @@ print (print_RTL 0). - -Definition transf_hls (p : Csyntax.program) : res Verilog.program := - OK p - @@@ transf_frontend @@@ transf_backend. Local Open Scope linking_scope. @@ -110,27 +110,30 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass Inliningproof.match_prog - ::: mkpass HTLgenproof.match_prog + ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. -Definition match_prog: Csyntax.program -> RTL.program -> Prop := +Definition match_prog: Csyntax.program -> Verilog.program -> Prop := pass_match (compose_passes CompCert's_passes). -Theorem transf_frontend_match: +Theorem transf_hls_match: forall p tp, - transf_frontend p = OK tp -> + transf_hls p = OK tp -> match_prog p tp. Proof. intros p tp T. - unfold transf_frontend in T. simpl in T. + unfold transf_hls in T. simpl in T. destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. + destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. + destruct (HTLgen.transl_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + set (p9 := Veriloggen.transl_program p8) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -138,5 +141,99 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. - inversion T. reflexivity. + exists p7; split. apply Inliningproof.transf_program_match; auto. + exists p8; split. apply HTLgenproof.transf_program_match; auto. + exists p9; split. apply Veriloggenproof.transf_program_match; auto. + inv T. reflexivity. +Qed. + +Remark forward_simulation_identity: + forall sem, forward_simulation sem sem. +Proof. + intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. +- auto. +- exists s1; auto. +- subst s2; auto. +- subst s2. exists s1'; auto. +Qed. + +Theorem cstrategy_semantic_preservation: + forall p tp, + match_prog p tp -> + forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp) + /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp). +Proof. + intros p tp M. unfold match_prog, pass_match in M; simpl in M. +Ltac DestructM := + match goal with + [ H: exists p, _ /\ _ |- _ ] => + let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in + destruct H as (p & M & MM); clear H + end. + repeat DestructM. subst tp. + assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p9)). + { + eapply compose_forward_simulations. + eapply SimplExprproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply SimplLocalsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cshmgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Selectionproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLgenproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply HTLgenproof.transf_program_correct. eassumption. + eapply Veriloggenproof.transf_program_correct; eassumption. + } + split. auto. + apply forward_to_backward_simulation. + apply factor_forward_simulation. auto. eapply sd_traces. eapply Verilog.semantics_determinate. + apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. + apply Verilog.semantics_determinate. +Qed. + +Theorem c_semantic_preservation: + forall p tp, + match_prog p tp -> + backward_simulation (Csem.semantics p) (Verilog.semantics tp). +Proof. + intros. + apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). + eapply sd_traces; eapply Verilog.semantics_determinate. + apply factor_backward_simulation. + apply Cstrategy.strategy_simulation. + apply Csem.semantics_single_events. + eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. + exact (proj2 (cstrategy_semantic_preservation _ _ H)). +Qed. + +Theorem transf_c_program_correct: + forall p tp, + transf_hls p = OK tp -> + backward_simulation (Csem.semantics p) (Verilog.semantics tp). +Proof. + intros. apply c_semantic_preservation. apply transf_hls_match; auto. +Qed. + +Theorem separate_transf_c_program_correct: + forall c_units asm_units c_program, + nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units asm_units -> + link_list c_units = Some c_program -> + exists asm_program, + link_list asm_units = Some asm_program + /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics asm_program). +Proof. + intros. + assert (nlist_forall2 match_prog c_units asm_units). + { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } + assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + { eapply link_list_compose_passes; eauto. } + destruct H2 as (asm_program & P & Q). + exists asm_program; split; auto. apply c_semantic_preservation; auto. Qed. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 338e77d..2e91b99 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -17,7 +17,7 @@ *) From compcert Require RTL Registers AST. -From compcert Require Import Integers Globalenvs Memory. +From compcert Require Import Integers Globalenvs Memory Linking. From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. @@ -124,11 +124,17 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ main_is_internal p = true. -Definition match_prog_matches : - forall p tp, - match_prog p tp -> - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. - Proof. intros. unfold match_prog in H. tauto. Qed. +Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): + TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2). +Proof. + Admitted. + +Definition match_prog' (p: RTL.program) (tp: HTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma match_prog_matches : + forall p tp, match_prog p tp -> match_prog' p tp. +Proof. unfold match_prog. tauto. Qed. Lemma transf_program_match: forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. @@ -368,6 +374,47 @@ Section CORRECTNESS. rewrite H. auto. Qed. + Lemma op_stack_based : + forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, + tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') + (Verilog.Vnonblock (Verilog.Vvar res0) e) + (state_goto st pc') -> + reg_stack_based_pointers sp rs -> + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> + @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op + (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> + stack_based v sp. + Proof. + Ltac solve_no_ptr := + match goal with + | H: reg_stack_based_pointers ?sp ?rs |- stack_based (Registers.Regmap.get ?r ?rs) _ => + solve [apply H] + | H1: reg_stack_based_pointers ?sp ?rs, H2: Registers.Regmap.get _ _ = Values.Vptr ?b ?i + |- context[Values.Vptr ?b _] => + let H := fresh "H" in + assert (H: stack_based (Values.Vptr b i) sp) by (rewrite <- H2; apply H1); simplify; solve [auto] + | |- context[Registers.Regmap.get ?lr ?lrs] => + destruct (Registers.Regmap.get lr lrs) eqn:?; simplify; auto + | |- stack_based (?f _) _ => unfold f + | |- stack_based (?f _ _) _ => unfold f + | |- stack_based (?f _ _ _) _ => unfold f + | |- stack_based (?f _ _ _ _) _ => unfold f + | H: ?f _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: ?f _ _ _ _ _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: map (fun r : positive => Registers.Regmap.get r _) ?args = _ |- _ => + destruct args; inv H + | |- context[if ?c then _ else _] => destruct c; try discriminate + | H: match _ with _ => _ end = Some _ |- _ => repeat (unfold_match H) + | |- context[match ?g with _ => _ end] => destruct g; try discriminate + | |- _ => simplify; solve [auto] + end. + intros F V sp v m args rs op g pc' res0 pc f e fin rtrn st stk INSTR RSBP SEL EVAL. + inv INSTR. unfold translate_instr in H5. + unfold_match H5; repeat (unfold_match H5); repeat (simplify; solve_no_ptr). + Qed. + Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> @@ -396,11 +443,11 @@ Section CORRECTNESS. apply H in HPle. apply H in HPle0. eexists. split. econstructor; eauto. constructor. trivial. constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. - + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int. - pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3. - Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl. - apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4. - rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + + inv HPle0. constructor. unfold valueToPtr. + pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H2. + unfold Ptrofs.of_int. simpl. + apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3. + rewrite Ptrofs.unsigned_repr. apply H3. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. apply Int.unsigned_range_2. auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. @@ -532,7 +579,7 @@ Section CORRECTNESS. match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. Proof. intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. - inv_state. + inv_state. inv MARR. exploit eval_correct; eauto. intros. inversion H1. inversion H2. econstructor. split. apply Smallstep.plus_one. @@ -543,74 +590,32 @@ Section CORRECTNESS. constructor; trivial. econstructor; simpl; eauto. simpl. econstructor. econstructor. - apply H3. simplify. + apply H5. simplify. all: big_tac. - assert (Ple res0 (RTL.max_reg_function f)) + assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in H10. lia. + unfold Ple in HPle. lia. apply regs_lessdef_add_match. assumption. apply regs_lessdef_add_greater. unfold Plt; lia. assumption. - assert (Ple res0 (RTL.max_reg_function f)) + assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in H12; lia. - Admitted. -(* unfold_merge. simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - (*match_states*) - assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. - rewrite <- H1. - constructor; auto. - unfold_merge. - apply regs_lessdef_add_match. - constructor. - apply regs_lessdef_add_greater. - apply greater_than_max_func. - assumption. - - unfold state_st_wf. intros. inversion H2. subst. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - + econstructor. split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor; simpl; trivial. - constructor; trivial. - econstructor; simpl; eauto. - eapply eval_correct; eauto. - constructor. rewrite valueToInt_intToValue. trivial. - unfold_merge. simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - - match_states - assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. - rewrite <- H1. - constructor. - unfold_merge. - apply regs_lessdef_add_match. - constructor. - symmetry. apply valueToInt_intToValue. - apply regs_lessdef_add_greater. - apply greater_than_max_func. - assumption. assumption. - - unfold state_st_wf. intros. inversion H2. subst. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply st_greater_than_res. - assumption. - Admitted.*) + unfold Ple in HPle; lia. + eapply op_stack_based; eauto. + inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + Unshelve. trivial. + Qed. Hint Resolve transl_iop_correct : htlproof. Ltac tac := diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index aa99fbd..f0f6de6 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -81,9 +81,7 @@ Search Ptrofs.of_int Ptrofs.to_int. Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z - then Some (ptrToValue off) - else None + | Values.Vptr b off => Some (ptrToValue off) | Values.Vundef => Some (ZToValue 0%Z) | _ => None end. @@ -117,7 +115,6 @@ Inductive val_value_lessdef: val -> value -> Prop := | val_value_lessdef_ptr: forall b off v', off = valueToPtr v' -> - (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -162,8 +159,5 @@ Proof. destruct v; try discriminate; constructor. unfold valToValue in H. inversion H. unfold valueToInt. unfold intToValue in H1. auto. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. - inv H1. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. - inv H1. apply Z.eqb_eq. apply Heqb0. + inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. Qed. -- cgit From bfb722caf2d46867779222b45615481e9020f0aa Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 23:28:28 +0100 Subject: Rename asm to verilog --- src/Compiler.v | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index 05353f9..db3a810 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -222,18 +222,19 @@ Proof. Qed. Theorem separate_transf_c_program_correct: - forall c_units asm_units c_program, - nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units asm_units -> + forall c_units verilog_units c_program, + nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units -> link_list c_units = Some c_program -> - exists asm_program, - link_list asm_units = Some asm_program - /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics asm_program). + exists verilog_program, + link_list verilog_units = Some verilog_program + /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program). Proof. intros. - assert (nlist_forall2 match_prog c_units asm_units). + assert (nlist_forall2 match_prog c_units verilog_units). { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_hls_match; auto. } - assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + assert (exists verilog_program, link_list verilog_units = Some verilog_program + /\ match_prog c_program verilog_program). { eapply link_list_compose_passes; eauto. } - destruct H2 as (asm_program & P & Q). - exists asm_program; split; auto. apply c_semantic_preservation; auto. + destruct H2 as (verilog_program & P & Q). + exists verilog_program; split; auto. apply c_semantic_preservation; auto. Qed. -- cgit From aea11ef02422b8302779676a31adcf6dafbff0dd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 00:55:52 +0100 Subject: Proof of TransfHTLLink DONE --- src/translation/HTLgenproof.v | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2e91b99..12a1a70 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -127,7 +127,20 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) := Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2). Proof. - Admitted. + red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + apply link_prog_inv in H. + + unfold match_prog in *. + unfold main_is_internal in *. simplify. repeat (unfold_match H4). + repeat (unfold_match H3). simplify. + subst. rewrite H0 in *. specialize (H (AST.prog_main p2)). + exploit H. + apply Genv.find_def_symbol. exists b. split. + assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + apply Genv.find_def_symbol. exists b0. split. + assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + intros. inv H3. inv H5. destruct H6. inv H5. +Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. -- cgit From 45a955c6f2f238aeb4955ae4525efabcf822f31a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 03:09:49 +0100 Subject: A few operations left --- src/translation/HTLgenproof.v | 118 +++++++++++++++++++++++++++++++----------- 1 file changed, 88 insertions(+), 30 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 12a1a70..27eb9e5 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -136,9 +136,9 @@ Proof. subst. rewrite H0 in *. specialize (H (AST.prog_main p2)). exploit H. apply Genv.find_def_symbol. exists b. split. - assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + assumption. apply Genv.find_funct_ptr_iff. eassumption. apply Genv.find_def_symbol. exists b0. split. - assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + assumption. apply Genv.find_funct_ptr_iff. eassumption. intros. inv H3. inv H5. destruct H6. inv H5. Qed. @@ -428,6 +428,15 @@ Section CORRECTNESS. unfold_match H5; repeat (unfold_match H5); repeat (simplify; solve_no_ptr). Qed. + Lemma int_inj : + forall x y, + Int.unsigned x = Int.unsigned y -> + x = y. + Proof. + intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned. + rewrite <- H. trivial. + Qed. + Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> @@ -437,36 +446,85 @@ Section CORRECTNESS. translate_instr op args s = OK e s' i -> exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. Proof. + Ltac eval_correct_tac := + match goal with + | |- context[valueToPtr] => unfold valueToPtr + | |- context[valueToInt] => unfold valueToInt + | |- context[bop] => unfold bop + | |- context[boplit] => unfold boplit + | |- val_value_lessdef Values.Vundef _ => solve [constructor] + | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H + | |- val_value_lessdef (Values.Vint _) _ => constructor; auto + | H : context[RTL.max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) (Registers.Regmap.get ?r0 ?rs)] => + let HPle1 := fresh "HPle" in + let HPle2 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; apply H in HPle2; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)] + | H : context[RTL.max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) _] => + let HPle1 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; try (constructor; auto)] + | H : _ :: _ = _ :: _ |- _ => inv H + | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate + | |- Verilog.expr_runp _ _ _ _ _ => econstructor + | |- val_value_lessdef (?f _ _) _ => unfold f + | |- val_value_lessdef (?f _) _ => unfold f + | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H) + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _ + |- _ => rewrite H1 in H2; inv H2 + | |- _ => eexists; split; try constructor; solve [eauto] + | H : context[RTL.max_reg_function ?f] |- context[_ (Verilog.Vvar ?r) (Verilog.Vvar ?r0)] => + let HPle1 := fresh "H" in + let HPle2 := fresh "H" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto + | H : context[RTL.max_reg_function ?f] |- context[Verilog.Vvar ?r] => + let HPle := fresh "H" in + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle; eexists; split; try constructor; eauto + | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate + end. intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; - unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify. - - inv Heql. - assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H in HPle. eexists. split; try constructor; eauto. - - eexists. split. constructor. constructor. auto. - - inv Heql. - assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H in HPle. - eexists. split. econstructor; eauto. constructor. trivial. - unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor. - inv HPle. auto. - - inv Heql. - assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H in HPle. apply H in HPle0. - eexists. split. econstructor; eauto. constructor. trivial. - constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. - + inv HPle0. constructor. unfold valueToPtr. - pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H2. - unfold Ptrofs.of_int. simpl. - apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3. - rewrite Ptrofs.unsigned_repr. apply H3. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. - apply Int.unsigned_range_2. - auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. - apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. - replace Ptrofs.max_unsigned with Int.max_unsigned; auto. - apply Int.unsigned_range_2. - Admitted. + unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL; + repeat (simplify; eval_correct_tac; unfold valueToInt in *). + - pose proof Integers.Ptrofs.agree32_sub as H2; unfold Integers.Ptrofs.agree32 in H2. + unfold Ptrofs.of_int. simpl. + apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3. + rewrite Ptrofs.unsigned_repr. apply H3. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + - pose proof Integers.Ptrofs.agree32_sub as AGR; unfold Integers.Ptrofs.agree32 in AGR. + assert (ARCH: Archi.ptr64 = false) by auto. eapply AGR in ARCH. + apply int_inj. unfold Ptrofs.to_int. rewrite Int.unsigned_repr. + apply ARCH. Search Ptrofs.unsigned. pose proof Ptrofs.unsigned_range_2. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. + eapply H2 in ARCH. apply ARCH. + pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. + eapply H2 in ARCH. apply ARCH. + - admit. + - admit. + - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. + - rewrite Heqb in Heqb0. discriminate. + - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. + - rewrite Heqb in Heqb0. discriminate. + - admit. + - admit. (* ror *) + - admit. (* addressing *) + - admit. (* eval_condition *) + - admit. (* select *) + Admitted. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, -- cgit From 855ca59a303efd32f1979f4e508edb4ddb43adac Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 09:47:40 +0100 Subject: No admitted in Deterministic proof --- src/translation/HTLgenproof.v | 4 ++-- src/verilog/Value.v | 2 +- src/verilog/Verilog.v | 18 +++++++----------- 3 files changed, 10 insertions(+), 14 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 27eb9e5..51c0fa1 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -513,8 +513,8 @@ Section CORRECTNESS. eapply H2 in ARCH. apply ARCH. pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. eapply H2 in ARCH. apply ARCH. - - admit. - - admit. + - admit. (* mulhs *) + - admit. (* mulhu *) - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. - rewrite Heqb in Heqb0. discriminate. - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 2718a46..af2b822 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -468,7 +468,7 @@ Qed. Lemma ZToValue_eq : forall w1, - (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted. + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. Lemma wordsize_32 : Int.wordsize = 32%nat. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 9659189..78b057d 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -245,7 +245,7 @@ Definition program := AST.program fundef unit. Definition posToLit (p : positive) : expr := Vlit (posToValue p). -Definition fext := assocmap. +Definition fext := unit. Definition fextclk := nat -> fext. (** ** State @@ -345,10 +345,6 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack iexp i -> arr_assocmap_lookup stack r (valueToNat i) = Some v -> expr_runp fext reg stack (Vvari r iexp) v - | erun_Vinputvar : - forall fext reg stack r v, - fext!r = Some v -> - expr_runp fext reg stack (Vinputvar r) v | erun_Vbinop : forall fext reg stack op l r lv rv resv, expr_runp fext reg stack l lv -> @@ -391,11 +387,11 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. -Definition access_fext (f : fext) (r : reg) : res value := +(*Definition access_fext (f : fext) (r : reg) : res value := match AssocMap.get r f with | Some v => OK v | _ => OK (ZToValue 0) - end. + end.*) (* TODO FIX Vvar case without default *) (*Fixpoint expr_run (assoc : assocmap) (e : expr) @@ -650,11 +646,11 @@ Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat assumed to be the starting state of the module, and may have to be changed if other arguments to the module are also to be supported. *) -Definition initial_fextclk (m : module) : fextclk := +(*Definition initial_fextclk (m : module) : fextclk := fun x => match x with | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) - end. + end.*) (*Definition module_run (n : nat) (m : module) : res assocmap := mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) @@ -886,11 +882,11 @@ Lemma semantics_determinate : Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. assert (f = f0) by admit; subst. + - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. pose proof (mis_stepp_determinate H5 H15). crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. - red; simplify; intro; invert H0; invert H; crush. - invert H; invert H0; crush. -Admitted. +Qed. -- cgit