diff options
author | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
commit | 7e20d7bed643300605d9ff157d6dd206a7bb6b7b (patch) | |
tree | 6139957c9b1f70715af635e99e713c621e403e6f /src/translation | |
parent | 88553f08d8f2ad96ae615e9648b7c1417573247a (diff) | |
parent | e9076031a8f759b10606e8507490ed8c68b16a43 (diff) | |
download | vericert-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.tar.gz vericert-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 8 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 26 |
2 files changed, 30 insertions, 4 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 0fe6656..1a72261 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -410,7 +410,13 @@ Definition max_state (f: function) : state := Definition transl_module (f : function) : Errors.res module := run_mon (max_state f) (transf_module f). -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transl_fundef (f : RTL.fundef) : Errors.res HTL.fundef := + match f with + | Internal f' => + Errors.bind (transl_module f') + (fun f'' => Errors.OK (Internal f'')) + | _ => Errors.Error (Errors.msg "External function could not be translated.") + end. (** Translation of a whole program. *) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 5cdddb2..a8177cf 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -51,7 +51,11 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (HTL.State m st assoc) | match_returnstate : forall v v' stack m, val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v m) (HTL.Returnstate v'). + match_states (RTL.Returnstate stack v m) (HTL.Returnstate v') +| match_initial_call : + forall f m m0 st + (TF : tr_module f m), + match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap). Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := @@ -450,7 +454,21 @@ Section CORRECTNESS. Smallstep.initial_state (RTL.semantics prog) s1 -> exists s2 : Smallstep.state (HTL.semantics tprog), Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. - Proof. Admitted. + Proof. + induction 1. + exploit function_ptr_translated; eauto. + intros [tf [A B]]. + unfold transl_fundef, Errors.bind in B. + repeat (unfold_match B). inversion B. subst. + econstructor; split. econstructor. + apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (AST.prog_main tprog) with (AST.prog_main prog). + rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. + eexact A. trivial. + constructor. + apply transl_module_correct. auto. + Qed. Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : @@ -458,7 +476,9 @@ Section CORRECTNESS. (r : Integers.Int.int), match_states s1 s2 -> Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. - Proof. Admitted. + Proof. + intros. inv H0. inv H. inv H4. constructor. trivial. + Qed. Hint Resolve transl_final_states : htlproof. Theorem transf_program_correct: |