diff options
| -rw-r--r-- | src/hls/HTL.v | 12 | ||||
| -rw-r--r-- | src/hls/HTLgen.v | 8 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 46 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 2 |
4 files changed, 39 insertions, 29 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 8d51750..d777d66 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -129,14 +129,10 @@ Qed. Definition genv := Globalenvs.Genv.t fundef unit. -Definition find_module (i: ident) (ge : genv) : option module := - match Globalenvs.Genv.find_symbol ge i with +Definition find_func {F V} (ge : Globalenvs.Genv.t F V) (symb : AST.ident) : option F := + match Globalenvs.Genv.find_symbol ge symb with | None => None - | Some b => - match Globalenvs.Genv.find_funct_ptr ge b with - | Some (AST.Internal f) => Some f - | _ => None - end + | Some b => Globalenvs.Genv.find_funct_ptr ge b end. Inductive stackframe : Type := @@ -208,7 +204,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Returnstate sf mid retval) | step_initcall : forall g callerid caller st asr asa sf callee_id callee callee_reset callee_params callee_param_vals, - find_module callee_id g = Some callee -> + find_func g callee_id = Some (AST.Internal callee) -> caller.(mod_externctrl)!callee_reset = Some (callee_id, ctrl_reset) -> (forall n param, nth_error callee_params n = Some param -> diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index c63847a..3b4b934 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -518,12 +518,6 @@ Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := Definition map_externctrl_params := xmap_externctrl_params 0. -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) => @@ -552,7 +546,7 @@ Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instru | 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 rtl_find_func ge fn with + then match find_func ge fn with | Some (AST.Internal _) => do params <- map_externctrl_params fn args; diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 53dbdb5..533f18e 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1336,11 +1336,11 @@ Section CORRECTNESS. Lemma only_internal_calls : forall fd fn rs, RTL.find_function ge (inr fn) rs = Some fd -> - (exists f : RTL.function, rtl_find_func ge fn = Some (AST.Internal f)) -> + (exists f : RTL.function, HTL.find_func ge fn = Some (AST.Internal f)) -> (exists f, fd = AST.Internal f). Proof. intros * ? [? ?]. - unfold rtl_find_func in *. + unfold HTL.find_func in *. unfold RTL.find_function in *. destruct (Genv.find_symbol ge fn); try discriminate. exists x. crush. @@ -1416,6 +1416,23 @@ Section CORRECTNESS. eapply nonblock_all_exec. Qed. + Lemma transl_find : forall fn f, + HTL.find_func ge fn = Some (AST.Internal f) -> + match_prog prog tprog -> + (exists f', HTL.find_func tge fn = Some (AST.Internal f')). + Proof. + intros. + unfold HTL.find_func in *. + rewrite symbols_preserved. + destruct (Genv.find_symbol ge fn); try discriminate. + destruct (function_ptr_translated _ _ H) as [? [? ?]]. + replace (Genv.find_funct_ptr tge b). + inversion H2. + destruct (transl_module prog f); try discriminate. + inversion H4. + exists m. crush. + Qed. + Lemma transl_icall_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc', @@ -1432,11 +1449,11 @@ Section CORRECTNESS. intros * H Hfunc * MSTATE. inv_state. edestruct (only_internal_calls fd); eauto; subst fd. - simpl in *. + inv CONST. + simplify. + destruct (transl_find _ _ ltac:(eauto) TRANSL). eexists. split. - - inv CONST. - simplify. - eapply Smallstep.plus_three; simpl in *. + - eapply Smallstep.plus_three; simpl in *. + eapply HTL.step_module; simpl. * repeat econstructor; auto. * repeat econstructor; auto. @@ -1504,15 +1521,18 @@ Section CORRECTNESS. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. * admit. - + eapply HTL.step_initcall. - * (* find called module *) admit. - * (* callee reset mapped *) admit. - * (* params mapped *) admit. - * (* callee reset unset *) admit. - * (* params set *) admit. + + eapply HTL.step_initcall; simplify. + * eassumption. + * eassumption. + * (* params mapped *) admit. (** TODO: We might have to change the statement of step_initcall *) + * big_tac. + assert (dst <= (RTL.max_reg_function f))%positive + by (eapply RTL.max_reg_function_def; eauto). + not_control_reg. + * admit. + eauto with htlproof. - econstructor; try solve [repeat econstructor; eauto with htlproof ]. - + (* Called module is translated *) admit. + + admit. + (* Match stackframes *) admit. + (* Argument values match *) admit. Admitted. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 21de6bd..9c5804d 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -87,7 +87,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap | tr_code_call : forall sig fn args dst n, c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> - (exists fd, rtl_find_func ge fn = Some (AST.Internal fd)) -> + (exists fd, find_func ge fn = Some (AST.Internal fd)) -> Z.pos n <= Int.max_unsigned -> (exists pc2 fn_rst fn_return fn_finish fn_params, |