diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-10 14:14:43 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-10 14:14:43 +0100 |
commit | 4a958045828763310f25303ce993218da15f2864 (patch) | |
tree | 200f815241280aceb51b99082bbcdce07cda1bf7 /src | |
parent | 46a0acaf018e04aabcc2066c43094a3d6678e36e (diff) | |
download | vericert-4a958045828763310f25303ce993218da15f2864.tar.gz vericert-4a958045828763310f25303ce993218da15f2864.zip |
Prove that called module exists for Icall
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/HTLgenproof.v | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 232c52c..61d08e0 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -508,6 +508,30 @@ Section CORRECTNESS. rewrite H. auto. Qed. + Lemma match_find_function : forall fn rs f m, + RTL.find_function ge (inr fn) rs = Some (AST.Internal f) -> + HTL.find_func tge fn = Some (AST.Internal m) -> + tr_module ge f m. + Proof. + intros * Hrtl Hhtl. + destruct TRANSL as [MATCH _]. + + unfold RTL.find_function in *. unfold_match Hrtl. + unfold HTL.find_func in *. unfold_match Hhtl. + replace b0 with b in *. clear b0. + + destruct (function_ptr_translated _ _ Hrtl) as [tf [? ?]]. + replace tf with (AST.Internal m) in *. clear tf. + + - apply transl_module_correct. + simpl in *. + destruct (transl_module prog f) eqn:E; crush. + - assert (Some (AST.Internal m) = Some tf) by + hauto lq: on unfold: HTL.program, Genv.find_funct_ptr. + sauto. + - scongruence use: symbols_preserved. + 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') @@ -1564,8 +1588,8 @@ Section CORRECTNESS. not_control_reg. * simpl; trivial. + eauto with htlproof. - - econstructor; try solve [repeat econstructor; eauto with htlproof ]. - + admit. + - constructor; try solve [repeat econstructor; eauto with htlproof ]. + + eauto using match_find_function. + (* Match stackframes *) admit. + (* Argument values match *) admit. Admitted. |