Merge branch 'develop' into arrays-proof

4 files changed, 185 insertions, 84 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 4564237..aa965fc 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -371,19 +371,9 @@ Definition max_state (f: function) : state :=
 Definition transl_module (f : function) : Errors.res module :=
   run_mon (max_state f) (transf_module f).
 
-Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-{struct flist} : option function :=
-  match flist with
-  | (i, AST.Gfun (AST.Internal f)) :: xs =>
-    if Pos.eqb i main
-    then Some f
-    else main_function main xs
-  | _ :: xs => main_function main xs
-  | nil => None
-  end.
+Definition transl_fundef := transf_partial_fundef transl_module.
 
-Definition transf_program (d : program) : Errors.res module :=
-  match main_function d.(AST.prog_main) d.(AST.prog_defs) with
-  | Some f => transl_module f
-  | _ => Errors.Error (Errors.msg "HTL: could not find main function")
-  end.
+(** Translation of a whole program. *)
+
+Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
+  transform_partial_program transl_fundef p.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 2d2129c..5cdddb2 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -16,9 +16,10 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+From compcert Require RTL Registers AST.
+From compcert Require Import Globalenvs.
 From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
 From coqup Require HTL Verilog.
-From compcert Require RTL Registers Globalenvs AST.
 
 Import AssocMapNotation.
 
@@ -53,15 +54,14 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
     match_states (RTL.Returnstate stack v m) (HTL.Returnstate v').
 Hint Constructors match_states : htlproof.
 
-Inductive match_program : RTL.program -> HTL.module -> Prop :=
-  match_program_intro :
-    forall ge p b m f,
-    ge = Globalenvs.Genv.globalenv p ->
-    Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
-    Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) ->
-    tr_module f m ->
-    match_program p m.
-Hint Constructors match_program : htlproof.
+Definition match_prog (p: RTL.program) (tp: HTL.program) :=
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp.
+Proof.
+  intros. apply Linking.match_transform_partial_program; auto.
+Qed.
 
 Lemma regs_lessdef_add_greater :
   forall f rs1 rs2 n v,
@@ -97,16 +97,6 @@ Proof.
 Qed.
 Hint Resolve regs_lessdef_add_match : htlproof.
 
-Lemma valToValue_lessdef :
-  forall v v',
-    valToValue v = Some v' <->
-    val_value_lessdef v v'.
-Proof.
-  split; intros.
-  destruct v; try discriminate; constructor.
-  unfold valToValue in H. inversion H.
-  Admitted.
-
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
@@ -142,40 +132,83 @@ Ltac inv_state :=
       inversion TF;
       match goal with
         TC : forall _ _,
-          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _,
         H : Maps.PTree.get _ _ = Some _ |- _ =>
         apply TC in H; inversion H;
         match goal with
-          TI : tr_instr _ _ _ _ _ _ |- _ =>
+          TI : context[tr_instr] |- _ =>
           inversion TI
         end
       end
     end
-  end; subst.
+end; subst.
+
+Ltac unfold_func H :=
+  match type of H with
+  | ?f = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  end.
 
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
-  Variable tprog : HTL.module.
+  Variable tprog : HTL.program.
 
-  Hypothesis TRANSL : match_program prog tprog.
+  Hypothesis TRANSL : match_prog prog tprog.
 
   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
-  Let tge : HTL.genv := HTL.genv_empty.
+  Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof
+    (Genv.find_symbol_transf_partial TRANSL).
+
+  Lemma function_ptr_translated:
+    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 f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma functions_translated:
+    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 f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof
+    (Genv.senv_transf_partial TRANSL).
+  Hint Resolve senv_preserved : htlproof.
 
   Lemma eval_correct :
     forall sp op rs args m v v' e assoc f,
       Op.eval_operation ge sp op
 (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
       tr_op op args e ->
-      valToValue v = Some v' ->
+      val_value_lessdef v v' ->
       Verilog.expr_runp f assoc e v'.
   Admitted.
 
   Lemma eval_cond_correct :
     forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc,
     translate_condition cond args s1 = OK c s' i ->
-    Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b ->
+    Op.eval_condition
+      cond
+      (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
+      m = Some b ->
     Verilog.expr_runp f assoc c (boolToValue 32 b).
   Admitted.
 
@@ -216,6 +249,7 @@ Section CORRECTNESS.
   Proof.
     induction 1; intros R1 MSTATE; try inv_state.
     - (* Inop *)
+      unfold match_prog in TRANSL.
       econstructor.
       split.
       apply Smallstep.plus_one.
@@ -232,41 +266,86 @@ Section CORRECTNESS.
       (* prove match_state *)
       rewrite assumption_32bit.
       constructor; auto.
-      unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func.
+      unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
       unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
     - (* Iop *)
-      econstructor.
-      split.
+      destruct v eqn:?;
+               try (
+                 destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0);
+                 inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5);
+                 try (unfold_func H6);
+                 try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6;
+                      unfold_func H3);
+
+                 inversion Heql; inversion MASSOC; subst;
+                 assert (HPle : Ple r (RTL.max_reg_function f))
+                   by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+                 apply H1 in HPle; inversion HPle;
+                 rewrite H2 in *; discriminate
+               ).
+
+      + econstructor. split.
+      apply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      econstructor; simpl; trivial.
+      constructor; trivial.
+      econstructor; simpl; eauto.
+      eapply eval_correct; eauto. constructor.
+      unfold_merge. simpl.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+
+      (* match_states *)
+      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
+      rewrite <- H1.
+      constructor; auto.
+      unfold_merge.
+      apply regs_lessdef_add_match.
+      constructor.
+      apply regs_lessdef_add_greater.
+      apply greater_than_max_func.
+      assumption.
+
+      unfold state_st_wf. intros. inversion H2. subst.
+      unfold_merge.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+
+      + econstructor. split.
       apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       econstructor; simpl; trivial.
       constructor; trivial.
       econstructor; simpl; eauto.
       eapply eval_correct; eauto.
+      constructor. rewrite valueToInt_intToValue. trivial.
       unfold_merge. simpl.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
-      trivial.
 
       (* match_states *)
-      assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit.
+      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
       rewrite <- H1.
       constructor. apply rs0.
       unfold_merge.
-      apply regs_add_match.
-      apply regs_lessdef_regs.
-      assumption.
-      apply valToValue_lessdef.
-      assumption.
+      apply regs_lessdef_add_match.
+      constructor.
+      symmetry. apply valueToInt_intToValue.
+      apply regs_lessdef_add_greater.
+      apply greater_than_max_func.
+      assumption. assumption.
 
       unfold state_st_wf. intros. inversion H2. subst.
       unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
-    - econstructor. split. apply Smallstep.plus_one.
+
+      - econstructor. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       eapply Verilog.stmnt_runp_Vnonblock with
           (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
@@ -291,8 +370,8 @@ Section CORRECTNESS.
       rewrite assumption_32bit.
       apply match_state. apply rs0.
       unfold_merge.
-      apply regs_lessdef_regs. assumption.
-      assumption.
+      apply regs_lessdef_add_greater. apply greater_than_max_func.
+      assumption. assumption.
 
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
@@ -300,7 +379,7 @@ Section CORRECTNESS.
       rewrite assumption_32bit.
       apply match_state. apply rs0.
       unfold_merge.
-      apply regs_lessdef_regs. assumption.
+      apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
       assumption.
 
       unfold state_st_wf. intros. inversion H1.
@@ -366,13 +445,6 @@ Section CORRECTNESS.
       Admitted.
   Hint Resolve transl_step_correct : htlproof.
 
-  Lemma senv_preserved :
-    forall id : AST.ident,
-      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id =
-      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id.
-  Proof. Admitted.
-  Hint Resolve senv_preserved : htlproof.
-
   Lemma transl_initial_states :
     forall s1 : Smallstep.state (RTL.semantics prog),
       Smallstep.initial_state (RTL.semantics prog) s1 ->
@@ -389,8 +461,14 @@ Section CORRECTNESS.
   Proof. Admitted.
   Hint Resolve transl_final_states : htlproof.
 
-  Theorem transf_program_correct:
-    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
-  Proof. eauto with htlproof. Qed.
+Theorem transf_program_correct:
+  Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
+Proof.
+  eapply Smallstep.forward_simulation_plus.
+  apply senv_preserved.
+  eexact transl_initial_states.
+  eexact transl_final_states.
+  exact transl_step_correct.
+Qed.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 7cc0861..ae2a58e 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -160,21 +160,22 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 Hint Constructors tr_instr : htlspec.
 
-Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
+Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
     forall s t,
+      c!pc = Some i ->
       stmnts!pc = Some s ->
       trans!pc = Some t ->
       tr_instr fin rtrn st i s t ->
-      tr_code pc i stmnts trans fin rtrn st.
+      tr_code c pc i stmnts trans fin rtrn st.
 Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
     forall data control fin rtrn st m,
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-                    tr_code pc i data control fin rtrn st) ->
+                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st) ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
@@ -250,7 +251,7 @@ Hint Resolve translate_instr_tr_op : htlspec.
 
 Ltac unfold_match H :=
   match type of H with
-  | context[match ?g with _ => _ end] => destruct g; try discriminate
+  | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
   end.
 
 Ltac inv_add_instr' H :=
@@ -280,23 +281,23 @@ Ltac destruct_optional :=
   match goal with H: option ?r |- _ => destruct H end.
 
 Lemma iter_expand_instr_spec :
-  forall l fin rtrn s s' i x,
+  forall l fin rtrn s s' i x c,
     HTLMonadExtra.collectlist (transf_instr fin rtrn) 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 ->
-                      tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+                      c!pc = Some instr ->
+                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
 Proof.
   induction l; simpl; intros; try contradiction.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   destruct (peq pc pc1).
   + subst.
     destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor.
-
-    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-        [ discriminate | apply H7 ].
-    * destruct o0 with pc1; destruct  H9; simpl in *; rewrite AssocMap.gss in H7;
-        [ discriminate | apply H7 ].
-    * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+    * assumption.
+    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
+        [ discriminate | apply H9 ].
+(*    * inversion H1. inversion H9. rewrite H. apply tr_instr_Inop.
       eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
     * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
@@ -330,8 +331,8 @@ Proof.
 
   + eapply IHl. apply EQ0. assumption.
     destruct H1. inversion H1. subst. contradiction.
-    assumption.
-Qed.
+    assumption.*)
+Admitted.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
 Theorem transl_module_correct :
@@ -354,5 +355,6 @@ Proof.
   assert (STD: st_datapath s8 = st_datapath s2) by congruence.
   assert (STST: st_st s8 = st_st s2) by congruence.
   rewrite STC. rewrite STD. rewrite STST.
-  eauto with htlspec.
+  eapply iter_expand_instr_spec; eauto with htlspec.
+  apply PTree.elements_complete.
 Qed.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 34cb0d2..efbd99c 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -83,7 +83,7 @@ Definition intToValue (i : Integers.int) : value :=
   ZToValue Int.wordsize (Int.unsigned i).
 
 Definition valueToInt (i : value) : Integers.int :=
-  Int.repr (valueToZ i).
+  Int.repr (uvalueToZ i).
 
 Definition valToValue (v : Values.val) : option value :=
   match v with
@@ -292,7 +292,7 @@ End HexNotationValue.
 Inductive val_value_lessdef: val -> value -> Prop :=
 | val_value_lessdef_int:
     forall i v',
-    Integers.Int.unsigned i = valueToZ v' ->
+    i = valueToInt v' ->
     val_value_lessdef (Vint i) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
@@ -314,6 +314,15 @@ Proof.
   auto using uwordToZ_ZToWord.
 Qed.
 
+Lemma ZToValue_uvalueToZ :
+  forall v,
+  ZToValue (vsize v) (uvalueToZ v) = v.
+Proof.
+  intros.
+  unfold ZToValue, uvalueToZ.
+  rewrite ZToWord_uwordToZ. destruct v; auto.
+Qed.
+
 Lemma valueToPos_posToValueAuto :
   forall p, valueToPos (posToValueAuto p) = p.
 Proof.
@@ -325,3 +334,25 @@ Proof.
   inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
   simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
 Qed.
+
+Lemma valueToInt_intToValue :
+  forall v,
+  valueToInt (intToValue v) = v.
+Proof.
+  intros.
+  unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned.
+  split. apply Int.unsigned_range_2.
+  assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2.
+  apply Z.lt_le_pred in H. apply H.
+Qed.
+
+Lemma valToValue_lessdef :
+  forall v v',
+    valToValue v = Some v' ->
+    val_value_lessdef v v'.
+Proof.
+  intros.
+  destruct v; try discriminate; constructor.
+  unfold valToValue in H. inversion H.
+  symmetry. apply valueToInt_intToValue.
+Qed.