diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-04 19:59:21 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-04 20:05:04 +0100 |
commit | 4d7236541250808487820beec0b3f79ac2a901dc (patch) | |
tree | b08c984b02b3b44744885af849d3a81bad479121 /src/hls | |
parent | 95ef66d14377cbd88142b5ccb3d598fde6fec243 (diff) | |
download | vericert-4d7236541250808487820beec0b3f79ac2a901dc.tar.gz vericert-4d7236541250808487820beec0b3f79ac2a901dc.zip |
Correct lookup for called funcs, simplify tr_module
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/HTLgen.v | 32 | ||||
-rw-r--r-- | src/hls/HTLgenproof.v | 17 | ||||
-rw-r--r-- | src/hls/HTLgenspec.v | 44 |
3 files changed, 61 insertions, 32 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index bacee9c..2e4cf48 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -488,7 +488,13 @@ Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := Definition map_externctrl_params := xmap_externctrl_params 0. -Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := +Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) := + match Globalenvs.Genv.find_symbol ge symb with + | None => None + | Some b => Globalenvs.Genv.find_funct_ptr ge b + end. + +Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => match i with @@ -516,7 +522,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned - then match funmap ! fn with + then match rtl_find_func ge fn with | Some (AST.Internal _) => do params <- map_externctrl_params fn args; @@ -526,6 +532,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: do finish_reg <- map_externctrl fn ctrl_finish; do reset_reg <- map_externctrl fn ctrl_reset; do return_reg <- map_externctrl fn ctrl_return; + do _ <- map_externctrl fn ctrl_clk; let fork_instr := fork reset_reg params in let join_instr := join return_reg reset_reg dst in @@ -568,16 +575,18 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -Definition transf_module (funmap : PTree.t RTL.fundef) (main : ident) (f: function) : mon HTL.module := +Definition declare_params params := collectlist (fun r => declare_reg (Some Vinput) r 32) params. + +Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then + do _ <- declare_params (RTL.fn_params f); do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _ <- collectlist (transf_instr funmap fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; - do clk <- map_externctrl main ctrl_clk; + do clk <- create_reg (Some Vinput) 1; + do _ <- collectlist (transf_instr ge fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with @@ -614,10 +623,17 @@ Definition max_state (f: function) : state := (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition prog_funmap (prog : RTL.program) : (PTree.t ) := +Definition prog_funmap (prog : RTL.program) : (PTree.t RTL.fundef) := + AssocMap_Properties.of_list ( + Option.map_option (fun '(ident, def) => match def with + | AST.Gfun f => Some (ident, f) + | _ => None + end) + (AST.prog_defs prog) + ). Definition transl_module (prog : RTL.program) (f : function) : Errors.res HTL.module := - run_mon (max_state f) (transf_module f). + run_mon (max_state f) (transf_module (Globalenvs.Genv.globalenv prog) (AST.prog_main prog) f). Definition transl_fundef prog := transf_partial_fundef (transl_module prog). diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index cba21b0..eb7326a 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -179,7 +179,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp /\ + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\ main_is_internal p = true. Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): @@ -201,7 +201,7 @@ Proof. Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp. Lemma match_prog_matches : forall p tp, match_prog p tp -> match_prog' p tp. @@ -386,9 +386,8 @@ Ltac not_control_reg := solve [ unfold Ple, Plt in *; try multimatch goal with - | [ H : forall r, - (exists x, _ ! r = Some x) -> (r > _)%positive /\ (_ > r)%positive - |- context[?r'] + | [ H : forall r, (exists x, _ ! r = Some x) -> (_ < r < _)%positive + |- context[?r'] ] => destruct (H r' ltac:(eauto)) end; lia @@ -467,7 +466,7 @@ Section CORRECTNESS. Admitted. Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog. + Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog. Proof. intros; apply match_prog_matches; assumption. Qed. Lemma symbols_preserved: @@ -478,7 +477,7 @@ Section CORRECTNESS. forall (b: Values.block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -488,7 +487,7 @@ Section CORRECTNESS. forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -3069,7 +3068,7 @@ Section CORRECTNESS. rewrite symbols_preserved; eauto. - eauto. - constructor; auto with htlproof. - apply transl_module_correct with (AST.prog_main prog). + apply transl_module_correct. assert (Some (AST.Internal x) = Some (AST.Internal m)) as Heqm. { rewrite <- H6. setoid_rewrite <- A. trivial. } inv Heqm. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 387def0..b666620 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -134,10 +134,10 @@ Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := (fin > st)%positive -> (rtrn > fin)%positive -> (stk > rtrn)%positive -> - (forall r, (exists x, externctrl!r = Some x) -> (r > stk /\ start > r)%positive) -> (start > stk)%positive -> (rst > start)%positive -> (clk > rst)%positive -> + (forall r, (exists x, externctrl!r = Some x) -> (r > clk)%positive) -> tr_module ge f m. Hint Constructors tr_module : htlspec. @@ -341,12 +341,12 @@ Proof. sauto use: helper__map_externctrl_params_spec. Qed. Hint Resolve map_externctrl_params_spec : htlspec. Lemma iter_expand_instr_spec : - forall l ge fin rtrn stack s s' i x c, - HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + forall l prog fin rtrn stack s s' i x c, + HTLMonadExtra.collectlist (transf_instr (Globalenvs.Genv.globalenv prog) fin rtrn stack) l s = OK x s' i -> list_norepet (List.map fst l) -> (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> (forall pc instr, In (pc, instr) l -> c!pc = Some instr -> - tr_code ge c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). + tr_code (Globalenvs.Genv.globalenv prog) c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). Proof. (** Used to solve the simpler cases of tr_code: those involving tr_instr *) Ltac tr_code_simple_tac := @@ -377,17 +377,16 @@ Proof. inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. inversion H. - assert (exists fd, rtl_find_func ge i0 = Some (AST.Internal fd)) by admit. - eapply tr_code_call; eauto; crush. destruct (map_externctrl_params_combine _ _ _ _ _ _ EQ1) as [? [? ?]]; subst. repeat (eapply ex_intro). + repeat split; try monad_crush. (* slow *) * intros. destruct (map_externctrl_params_spec _ _ _ _ _ _ _ _ EQ1 ltac:(eauto)) as [param [? ?]]. exists param; crush; trans_step s3 s'. - * monadInv EQ2. crush. + * admit. (* (* FIXME: Causes Qed to hang *) monadInv EQ2. crush. *) + (* Icond *) tr_code_simple_tac. + (* Ireturn *) inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. @@ -441,9 +440,22 @@ Proof. Qed. Hint Resolve tr_code_trans : htlspec. +Lemma declare_params_freshreg_trans : forall params s s' x i, + declare_params params s = OK x s' i -> + st_freshreg s = st_freshreg s'. +Proof. + induction params; unfold declare_params in *; intros * H. + - inv H. trivial. + - monadInv H. + transitivity (st_freshreg s0). + + monadInv EQ. auto. + + eauto. +Qed. +Hint Resolve declare_params_freshreg_trans : htlspec. + Theorem transl_module_correct : - forall i f m ge, - transl_module i f = Errors.OK m -> tr_module ge f m. + forall p f m, + transl_module p f = Errors.OK m -> tr_module (Globalenvs.Genv.globalenv p) f m. Proof. intros * H. unfold transl_module in *. @@ -464,10 +476,12 @@ Proof. | [ EQ : get _ = OK _ _ _ |- _ ] => monadInv EQ end. - econstructor; eauto with htlspec; try lia; - try solve [some_monad_inv; repeat ((simpl in *; some_monad_inv) + idtac); - some_incr; simplify; - unfold Ple in *; lia - ]. - admit. (* No control registers are in externctrl *) + econstructor; + eauto with htlspec; + try solve [ repeat some_monad_inv; crush ]. + - auto_apply declare_params_freshreg_trans. + some_monad_inv; monad_crush. + - (* forall r, (exists x, externctrl!r = Some x) -> (r >= clk)%positive *) + (* Problematic because it does not cover *) + admit. Admitted. |