From 29ef1d2d374dcca6ea719c63339f18900be2532f Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 16 May 2021 15:17:24 +0100 Subject: Most of Ireturn proof --- src/hls/AssocMap.v | 8 +++++++ src/hls/HTLgen.v | 28 ++++++++++++++---------- src/hls/HTLgenproof.v | 59 ++++++++++++++++++++++++++++++++++++++++++++++----- src/hls/HTLgenspec.v | 2 +- 4 files changed, 80 insertions(+), 17 deletions(-) diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 68a8416..7e616af 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -219,3 +219,11 @@ Lemma find_get_assocmap : assoc ! r = Some v -> assoc # r = v. Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. + +Lemma fso : forall m v k1 k2, k1 <> k2 -> (m # k1 <- v) # k2 = m # k2. +Proof. + unfold "_ # _". + unfold AssocMapExt.get_default. + intros. + destruct_match; rewrite AssocMap.gso in Heqo by auto; rewrite Heqo; auto. +Qed. diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index a7e3584..365d981 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -446,12 +446,16 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). +Fixpoint nonblock_all pairs := + match pairs with + | (dst, src) :: pairs' => Vseq (nonblock dst (Vvar src)) (nonblock_all pairs') + | nil => Vskip + end. + (** [fork] a datapath statement which sets up the execution of a function *) Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt := let reset_mod := Vnonblock (Vvar rst) (posToLit 1) in - let assign_params := - List.fold_left (fun acc (a : reg*reg) => let (dst, src) := a in Vseq (nonblock dst (Vvar src)) acc) - params Vskip in + let assign_params := nonblock_all params in Vseq reset_mod assign_params. Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := @@ -459,13 +463,15 @@ Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in Vseq stop_reset set_result. -Definition return_val fin rtrn r := - let retval := - match r with - | Some r' => Vvar r' - | None => Vlit (ZToValue 0%Z) - end in - Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval). +Definition return_val r := + match r with + | Some r' => Vvar r' + | None => Vlit (ZToValue 0%Z) + end. + +Definition do_return fin rtrn r := + Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (return_val r)). Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)). @@ -537,7 +543,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => do idle_state <- create_state; - do _ <- add_instr n idle_state (return_val fin rtrn r); + do _ <- add_instr n idle_state (do_return fin rtrn r); add_instr_skip idle_state (idle fin) end end. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index d297c80..077a8dc 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1143,12 +1143,11 @@ Section CORRECTNESS. - inv CONST. assumption. - inv CONST. assumption. - repeat econstructor. - - repeat econstructor. simpl. apply H5. + - repeat econstructor. intuition eauto. - big_tac. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - - unfold Ple in HPle. lia. + assert (Ple res0 (RTL.max_reg_function f)) + by eauto using RTL.max_reg_function_def. + xomega. - big_tac. + apply regs_lessdef_add_match. assumption. apply regs_lessdef_add_greater. unfold Plt; lia. assumption. @@ -1172,6 +1171,56 @@ Section CORRECTNESS. Qed. Hint Resolve transl_iop_correct : htlproof. + Lemma return_val_exec_spec : forall f or asr asa, + Verilog.expr_runp f asr asa (return_val or) + (match or with + | Some r => asr#r + | None => ZToValue 0 + end). + Proof. destruct or; repeat econstructor. Qed. + + Lemma transl_ireturn_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) + (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) + (m' : mem), + (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall R1 : HTL.state, + match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. + Proof. + intros * H H0 * MSTATE. + inv_state. + inv CONST. simplify. + eexists. split. + - eapply Smallstep.plus_two. + + eapply HTL.step_module; eauto; try solve [ repeat econstructor ]. + * repeat econstructor. apply return_val_exec_spec. + * big_tac. + * admit. + + simplify. + eapply HTL.step_finish. + * big_tac. + * big_tac. + + eauto with htlproof. + - constructor; eauto with htlproof. + destruct or. + + rewrite fso. (* Return value is not fin *) + * big_tac. + inv MASSOC. + apply H10. + eapply RTL.max_reg_function_use; eauto; crush. + * assert (Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush). + xomega. + + eauto with htlproof. + Unshelve. + exact tt. eauto. + Admitted. + Hint Resolve transl_ireturn_correct : htlproof. + Ltac tac := repeat match goal with | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 1c2d090..d02aff6 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -107,7 +107,7 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c c!pc = Some (RTL.Ireturn r) -> (exists pc2, - stmnts!pc = Some (return_val fin rtrn r) /\ + stmnts!pc = Some (do_return fin rtrn r) /\ trans!pc = Some (state_goto st pc2) /\ stmnts!pc2 = Some (idle fin) /\ trans!pc2 = Some Vskip) -> -- cgit