Merge branch 'develop' into arrays-proof

3 files changed, 32 insertions, 6 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:
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 1ea0b1b..a553453 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -19,7 +19,7 @@
 From Coq Require Import FSets.FMapPositive.
 From coqup Require Import Coquplib Value AssocMap.
 From coqup Require Verilog.
-From compcert Require Events Globalenvs Smallstep Integers.
+From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
 
 Import HexNotationValue.
@@ -109,7 +109,7 @@ Inductive initial_state (p: program): state -> Prop :=
 
 Inductive final_state : state -> Integers.int -> Prop :=
 | final_state_intro : forall retval retvali,
-    value_int_eqb retval retvali = true ->
+    retvali = valueToInt retval ->
     final_state (Returnstate retval) retvali.
 
 Definition semantics (m : program) :=