HTLgenproof passing.arrays-proof

2 files changed, 127 insertions, 50 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index e637d6f..54ad77a 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -395,10 +395,6 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
     if (check_address_parameter off)
     then ret (Vvari stack (Vbinop Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4))))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
-  | Mint32, Op.Ascaled scale offset, r1::nil =>
-    if (check_address_parameter scale) && (check_address_parameter offset)
-    then ret (Vvari stack (Vbinop Vdiv (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) (Vlit (ZToValue 32 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if (check_address_parameter scale) && (check_address_parameter offset)
     then ret (Vvari stack
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 24191ae..cee04e9 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -57,18 +57,6 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem
                                  (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
     match_arrs m f sp mem asa.
 
-Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
-| match_stacks_nil :
-    match_stacks mem nil nil
-| match_stacks_cons :
-    forall cs lr r f sp pc rs m asr asa
-           (TF : tr_module f m)
-           (ST: match_stacks mem cs lr)
-           (MA: match_assocmaps f rs asr)
-           (MARR : match_arrs m f sp mem asa),
-      match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
-                       (HTL.Stackframe r m pc asr asa :: lr).
-
 Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
    match v with
    | Values.Vptr sp' off => sp' = sp
@@ -88,6 +76,21 @@ Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length
                               (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
                 spb.
 
+Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_stacks_nil :
+    match_stacks mem nil nil
+| match_stacks_cons :
+    forall cs lr r f sp sp' pc rs m asr asa
+           (TF : tr_module f m)
+           (ST: match_stacks mem cs lr)
+           (MA: match_assocmaps f rs asr)
+           (MARR : match_arrs m f sp mem asa)
+           (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
+           (RSBP: reg_stack_based_pointers sp' rs)
+           (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp),
+      match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
+                       (HTL.Stackframe r m pc asr asa :: lr).
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall asa asr sf f sp sp' rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
@@ -707,11 +710,6 @@ Section CORRECTNESS.
 
         rewrite Registers.Regmap.gso; auto.
 
-      + (* FIXME: Why is this degenerate? Should we support this mode? *)
-        unfold Op.eval_addressing in H0.
-        destruct (Archi.ptr64) eqn:ARCHI; simplify.
-        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate.
-
       + (** Preamble *)
         invert MARR. simplify.
 
@@ -1115,12 +1113,6 @@ Section CORRECTNESS.
       + admit.
       + admit.
 
-      (* + eexists. split. *)
-      (*   eapply Smallstep.plus_one. *)
-      (*   eapply HTL.step_module; eauto. *)
-      (*   econstructor. econstructor. econstructor. simplify. *)
-      + admit.
-
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       eapply Verilog.stmnt_runp_Vnonblock_reg with
@@ -1139,37 +1131,95 @@ Section CORRECTNESS.
       constructor.
       apply boolToValue_ValueToBool.
       constructor.
+      unfold Verilog.merge_regs.
       unfold_merge.
       apply AssocMap.gss.
 
       destruct b.
       rewrite assumption_32bit.
-      apply match_state.
+      simplify.
+      apply match_state with (sp' := sp'); eauto.
+      unfold Verilog.merge_regs.
       unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
-      assumption. assumption.
+      assumption.
 
-      unfold state_st_wf. intros. inversion H1.
-      subst. unfold_merge.
+      unfold state_st_wf. intros.
+      invert H3.
+      unfold Verilog.merge_regs. unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** Match arrays *)
+      invert MARR. simplify.
+      econstructor.
+      repeat split; simplify.
+      unfold HTL.empty_stack.
+      simplify.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H4.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      congruence.
+
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
       assumption.
 
       rewrite assumption_32bit.
-      apply match_state.
-      unfold_merge.
-      apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
+      apply match_state with (sp' := sp'); eauto.
+      unfold Verilog.merge_regs. unfold_merge.
+      apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
-      unfold state_st_wf. intros. inversion H1.
-      subst. unfold_merge.
+      unfold state_st_wf. intros.
+      invert H1.
+      unfold Verilog.merge_regs. unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** Match arrays *)
+      invert MARR. simplify.
+      econstructor.
+      repeat split; simplify.
+      unfold HTL.empty_stack.
+      simplify.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H2.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      congruence.
+
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
       assumption.
 
     - admit.
+
     - (* Return *)
       econstructor. split.
       eapply Smallstep.plus_two.
@@ -1184,6 +1234,7 @@ Section CORRECTNESS.
 
       constructor. constructor.
 
+      unfold Verilog.merge_regs.
       unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
@@ -1191,6 +1242,7 @@ Section CORRECTNESS.
       apply st_greater_than_res. apply st_greater_than_res.
 
       apply HTL.step_finish.
+      unfold Verilog.merge_regs.
       unfold_merge; simpl.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
@@ -1214,6 +1266,7 @@ Section CORRECTNESS.
       constructor.
       econstructor; simpl; trivial.
       apply Verilog.erun_Vvar. trivial.
+      unfold Verilog.merge_regs.
       unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
@@ -1221,6 +1274,7 @@ Section CORRECTNESS.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
+      unfold Verilog.merge_regs.
       unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
@@ -1238,21 +1292,26 @@ Section CORRECTNESS.
 
     - inversion MSTATE; subst. inversion TF; subst.
       econstructor. split. apply Smallstep.plus_one.
-      eapply HTL.step_call. simpl.
+      eapply HTL.step_call. simplify.
 
-      constructor. apply regs_lessdef_add_greater.
+      apply match_state with (sp' := stk); eauto.
+
+      apply regs_lessdef_add_greater.
       apply greater_than_max_func.
-      apply init_reg_assoc_empty. assumption. unfold state_st_wf.
-      intros. inv H1. apply AssocMap.gss. constructor.
+      apply init_reg_assoc_empty.
+      unfold state_st_wf.
+      intros. inv H3. apply AssocMap.gss. constructor.
 
-      econstructor; simpl.
-      reflexivity.
-      rewrite AssocMap.gss. reflexivity.
+      econstructor. simplify.
+      repeat split. unfold HTL.empty_stack.
+      simplify. apply AssocMap.gss.
+      unfold arr_repeat. simplify.
+      apply list_repeat_len.
       intros.
       destruct (Mem.load AST.Mint32 m' stk
                          (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
                                                       Integers.Ptrofs.zero
-                                                      (Integers.Ptrofs.repr ptr)))) eqn:LOAD.
+                                                      (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
       pose proof Mem.load_alloc_same as LOAD_ALLOC.
       pose proof H as ALLOC.
       eapply LOAD_ALLOC in ALLOC.
@@ -1261,21 +1320,43 @@ Section CORRECTNESS.
       repeat constructor.
       constructor.
 
-    - inversion MSTATE; subst. inversion MS; subst. econstructor.
+      unfold reg_stack_based_pointers. intros.
+      unfold RTL.init_regs; simplify.
+      destruct (RTL.fn_params f);
+      rewrite Registers.Regmap.gi; constructor.
+
+      unfold arr_stack_based_pointers. intros.
+      simplify.
+      destruct (Mem.load AST.Mint32 m' stk
+                         (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                      Integers.Ptrofs.zero
+                                                      (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
+      pose proof Mem.load_alloc_same as LOAD_ALLOC.
+      pose proof H as ALLOC.
+      eapply LOAD_ALLOC in ALLOC.
+      2: { exact LOAD. }
+      rewrite ALLOC.
+      repeat constructor.
+      constructor.
+
+    - invert MSTATE. invert MS.
+      econstructor.
       split. apply Smallstep.plus_one.
       constructor.
 
-      constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto.
+      constructor; auto.
+      econstructor; auto.
+      apply regs_lessdef_add_match; auto.
       apply regs_lessdef_add_greater. apply greater_than_max_func. auto.
 
       unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
       rewrite AssocMap.gss. trivial. apply st_greater_than_res.
 
+      admit.
+
       Unshelve.
       exact (AssocMap.empty value).
       exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
       (* exact (ZToValue 32 0). *)
       (* exact (AssocMap.empty value). *)
       (* exact (AssocMap.empty value). *)