diff options
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/RTLBlockgen.v | 112 | ||||
-rw-r--r-- | src/hls/RTLBlockgenproof.v | 83 |
2 files changed, 171 insertions, 24 deletions
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 8b0ea65..cb18147 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -179,17 +179,117 @@ Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i: | None => false end. +Definition check_valid_node (tc: code) (e: node) := + match tc ! e with + | Some _ => true + | _ => false + end. + +Fixpoint check_code' (c: RTL.code) (tc: code) (pc: node) (b: bb) (i: cf_instr) := + match b, i, c ! pc with + | RBnop :: (_ :: _) as b', _, Some (RTL.Inop pc') => + check_code' c tc pc' b' i + | RBop None op args dst :: (_ :: _) as b', _, Some (RTL.Iop op' args' dst' pc') => + ceq operation_eq op op' + && ceq list_pos_eq args args' + && ceq peq dst dst' + && check_code' c tc pc' b' i + | RBload None chunk addr args dst :: (_ :: _) as b', _, + Some (RTL.Iload chunk' addr' args' dst' pc') => + ceq memory_chunk_eq chunk chunk' + && ceq addressing_eq addr addr' + && ceq list_pos_eq args args' + && ceq peq dst dst' + && check_code' c tc pc' b' i + | RBstore None chunk addr args src :: (_ :: _) as b', _, + Some (RTL.Istore chunk' addr' args' src' pc') => + ceq memory_chunk_eq chunk chunk' + && ceq addressing_eq addr addr' + && ceq list_pos_eq args args' + && ceq peq src src' + && check_code' c tc pc' b' i + | RBnop :: nil, RBgoto pc', Some (RTL.Inop pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + | RBop None op args dst :: nil, RBgoto pc', Some (RTL.Iop op' args' dst' pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + && ceq operation_eq op op' + && ceq list_pos_eq args args' + && ceq peq dst dst' + | RBload None chunk addr args dst :: nil, RBgoto pc', + Some (RTL.Iload chunk' addr' args' dst' pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + && ceq memory_chunk_eq chunk chunk' + && ceq addressing_eq addr addr' + && ceq list_pos_eq args args' + && ceq peq dst dst' + | RBstore None chunk addr args src :: nil, RBgoto pc', + Some (RTL.Istore chunk' addr' args' src' pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + && ceq memory_chunk_eq chunk chunk' + && ceq addressing_eq addr addr' + && ceq list_pos_eq args args' + && ceq peq src src' + | RBnop :: nil, RBcall sig (inl r) args dst pc', + Some (RTL.Icall sig' (inl r') args' dst' pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + && ceq signature_eq sig sig' + && ceq peq r r' + && ceq list_pos_eq args args' + && ceq peq dst dst' + | RBnop :: nil, RBcall sig (inr i) args dst pc', + Some (RTL.Icall sig' (inr i') args' dst' pc'') => + check_valid_node tc pc' + && ceq peq pc' pc'' + && ceq signature_eq sig sig' + && ceq peq i i' + && ceq list_pos_eq args args' + && ceq peq dst dst' + | RBnop :: nil, RBtailcall sig' (inl r') args', + Some (RTL.Itailcall sig (inl r) args) => + ceq signature_eq sig sig' + && ceq peq r r' + && ceq list_pos_eq args args' + | RBnop :: nil, RBtailcall sig' (inr r') args', + Some (RTL.Itailcall sig (inr r) args) => + ceq signature_eq sig sig' + && ceq peq r r' + && ceq list_pos_eq args args' + | RBnop :: nil, RBcond cond' args' n1' n2', Some (RTL.Icond cond args n1 n2) => + check_valid_node tc n1 + && check_valid_node tc n2 + && ceq condition_eq cond cond' + && ceq list_pos_eq args args' + && ceq peq n1 n1' + && ceq peq n2 n2' + | RBnop :: nil, RBjumptable r' ns', Some (RTL.Ijumptable r ns) => + ceq peq r r' + && ceq list_pos_eq ns ns' + && forallb (check_valid_node tc) ns + | RBnop :: nil, RBreturn (Some r'), Some (RTL.Ireturn (Some r)) => + ceq peq r r' + | RBnop :: nil, RBreturn None, Some (RTL.Ireturn None) => true + | _, _, _ => false + end. + +Definition check_code c tc pc b := + check_code' c tc pc b.(bb_body) b.(bb_exit). + Parameter partition : RTL.function -> Errors.res function. Definition transl_function (f: RTL.function) := match partition f with | Errors.OK f' => - let blockids := map fst (PTree.elements f'.(fn_code)) in - if forall_ptree (check_present_blocks f'.(fn_code) blockids (fold_right Pos.max 1 blockids)) - f.(RTL.fn_code) then - Errors.OK - (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint)) - else Errors.Error (Errors.msg "check_present_blocks failed") + if check_valid_node f'.(fn_code) f.(RTL.fn_entrypoint) then + if forall_ptree (check_code f.(RTL.fn_code) f'.(fn_code)) f'.(fn_code) then + Errors.OK + (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint)) + else Errors.Error (Errors.msg "check_present_blocks failed") + else Errors.Error (Errors.msg "entrypoint does not exists") | Errors.Error msg => Errors.Error msg end. diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 875c582..642264f 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -35,6 +35,7 @@ Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import vericert.common.Vericertlib. +Require Import vericert.common.DecEq. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLBlockgen. @@ -325,6 +326,65 @@ whole execution (in one big step) of the basic block. | Some b' => 1 + length b' end. + Lemma check_valid_node_correct : + forall a b, check_valid_node a b = true -> valid_succ a b. + Proof. + intros. unfold valid_succ, check_valid_node in *. + destruct_match; try discriminate; eauto. + Qed. + + Lemma transl_entrypoint_exists : + forall f tf, + transl_function f = OK tf -> + valid_succ (fn_code tf) (fn_entrypoint tf). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + eauto using check_valid_node_correct. + Qed. + + Lemma ceq_eq : + forall A a (b: A) c, + ceq a b c = true -> + b = c. + Proof. + intros. unfold ceq in H. destruct_match; try discriminate. auto. + Qed. + + Ltac unfold_ands := + repeat match goal with + | H: _ && _ = true |- _ => apply andb_prop in H + | H: _ /\ _ |- _ => inv H + | H: ceq _ _ _ = true |- _ => apply ceq_eq in H; subst + end. + + Lemma transl_match_code' : + forall c tc b pc i, + check_code' c tc pc b i = true -> + match_block c tc pc b i. + Proof. + induction b; [crush|]. + intros. unfold check_code' in H. + do 4 (destruct_match; try discriminate); + try (repeat (destruct_match; try discriminate; []); unfold_ands; constructor; auto using check_valid_node_correct); + fold check_code' in *; + try (destruct_match; try discriminate; unfold_ands; econstructor; eauto); + apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct. + Qed. + + Lemma transl_match_code : + forall f tf, + transl_function f = OK tf -> + match_code f.(RTL.fn_code) tf.(fn_code). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + unfold match_code; intros. + eapply forall_ptree_true in Heqb0; eauto. + unfold check_code in *. + eauto using transl_match_code'. + Qed. + Lemma transl_initial_states : forall s1, RTL.initial_state prog s1 -> exists s2, RTLBlock.initial_state tprog s2 /\ match_states None s1 s2. @@ -751,18 +811,6 @@ whole execution (in one big step) of the basic block. unfold sem_extrap. intros. setoid_rewrite H5 in H8. crush. Qed. - Lemma transl_entrypoint_exists : - forall f tf, - transl_function f = OK tf -> - exists b, (fn_code tf) ! (fn_entrypoint tf) = Some b. - Proof. Admitted. - - Lemma transl_match_code : - forall f tf, - transl_function f = OK tf -> - match_code f.(RTL.fn_code) tf.(fn_code). - Proof. Admitted. - Lemma init_regs_equiv : forall b a, init_regs a b = RTL.init_regs a b. Proof. induction b; crush. Qed. @@ -781,9 +829,8 @@ whole execution (in one big step) of the basic block. inversion 1; subst; simplify. monadInv TF. inv H0. pose proof (transl_match_code _ _ EQ). - pose proof (transl_entrypoint_exists _ _ EQ). + pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1. simplify. - exploit transl_entrypoint_exists; eauto; simplify. destruct x0. apply sim_plus. do 3 econstructor. assert (fn_stacksize x = RTL.fn_stacksize f). @@ -802,14 +849,14 @@ whole execution (in one big step) of the basic block. repeat (destruct_match; try discriminate; []). inv EQ; auto. } unfold match_code in H0. - pose proof (H0 _ _ H3). + pose proof (H0 _ _ H2). econstructor; eauto. rewrite <- H1. eauto. rewrite H1. - rewrite init_regs_equiv. rewrite H4. eapply star_refl. + rewrite init_regs_equiv. rewrite H3. eapply star_refl. unfold sem_extrap; intros. - setoid_rewrite H2 in H7; simplify. - rewrite H4. eauto. + setoid_rewrite H2 in H6; simplify. + rewrite H3. eauto. Qed. Lemma transl_externalcall_correct: |