Merge branch 'arrays-proof' into develop

3 files changed, 204 insertions, 31 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 68f9900..43a6674 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,7 +17,7 @@
  *)
 
 From compcert Require Import Maps.
-From compcert Require Errors Globalenvs.
+From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
 From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
 
@@ -245,19 +245,28 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :
   | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
   end.
 
+Definition check_address_parameter (p : Z) : bool :=
+  Z.eqb (Z.modulo p 4) 0
+  && Z.leb Integers.Ptrofs.min_signed p
+  && Z.leb p Integers.Ptrofs.min_signed.
+
 Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
-  match a, args with
+  match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
-  | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
   | Op.Ascaled scale offset, r1::nil =>
-    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
-  | Op.Aindexed2scaled scale offset, r1::r2::nil =>
-    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-  (* Stack arrays/referenced variables *)
+    if (check_address_parameter scale) && (check_address_parameter offset)
+    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
+    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    if (check_address_parameter scale) && (check_address_parameter offset)
+    then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
-    ret (Vlit (ZToValue 32 a))
-  | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other")
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter a)
+    then ret (Vlit (ZToValue 32 a))
+    else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+  | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
 
 (** Translate an instruction to a statement. FIX mulhs mulhu *)
@@ -340,23 +349,24 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
            (args : list reg) (stack : reg) : mon expr :=
   match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Mint32, Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *)
+  | Mint32, Op.Aindexed off, r1::nil =>
     ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4)))))
   | Mint32, Op.Ascaled scale offset, r1::nil =>
-    if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
+    if (check_address_parameter scale) && (check_address_parameter offset)
     then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 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 ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
+    if (check_address_parameter scale) && (check_address_parameter offset)
     then ret (Vvari stack
                     (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4))))
                                  (boplitz Vmul r2 (scale / 4))))
     else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
-    if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
-    else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset")
-  | _, _, _ => error (Errors.msg "Htlgen: translate_arr_access unsuported addressing")
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter a)
+    then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
+    else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
+  | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
   end.
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 046ae06..be7538c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -69,20 +69,24 @@ Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe
       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
+   | _ => True
+   end.
+
 Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
-  forall r, match Registers.Regmap.get r rs with
-        | Values.Vptr sp' off => sp' = sp
-        | _ => True
-        end.
+  forall r, stack_based (Registers.Regmap.get r rs) sp.
 
 Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
   (sp : Values.val) : Prop :=
   forall ptr,
     0 <= ptr < (stack_length / 4) ->
-    match Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))) with
-    | Some (Values.Vptr sp' off) => sp' = spb
-    | _ => True
-    end.
+    stack_based (Option.default
+                   Values.Vundef
+                   (Mem.loadv AST.Mint32 m
+                              (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
+                spb.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall asa asr sf f sp sp' rs mem m st res
@@ -514,10 +518,10 @@ Section CORRECTNESS.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
         econstructor. econstructor. econstructor. simplify.
-        econstructor. econstructor. econstructor. econstructor. simplify.
-        econstructor.
-        econstructor.
-        econstructor.
+        econstructor. econstructor. econstructor. simplify.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *)
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]).
         econstructor.
         econstructor.
         econstructor.
@@ -526,6 +530,7 @@ Section CORRECTNESS.
         econstructor.
         econstructor.
         econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]).
         econstructor.
         econstructor.
         econstructor.
@@ -549,7 +554,135 @@ Section CORRECTNESS.
         unfold Verilog.merge_regs. unfold_merge.
         apply regs_lessdef_add_match.
 
-        all: admit.
+        pose proof H1.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity.
+        rewrite H4 in H5.
+        setoid_rewrite Integers.Ptrofs.add_zero_l in H5.
+
+        specialize (H5 (uvalueToZ
+                (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2)
+                   (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1))).
+
+        assert (0 <= uvalueToZ
+                      (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2)
+                             (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1) <
+                Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit.
+        apply H5 in H6.
+
+        invert MASSOC.
+        pose proof (H7 r0).
+        pose proof (H7 r1).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+        apply H8 in HPler0.
+        apply H10 in HPler1.
+        invert HPler0; invert HPler1; try congruence.
+        rewrite EQr0 in H12.
+        rewrite EQr1 in H13.
+
+        assert ((Integers.Ptrofs.unsigned
+            (Integers.Ptrofs.add i0
+               (Integers.Ptrofs.of_int
+                  (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z))
+                                    (Integers.Int.repr z0))))) =
+                (Integers.Ptrofs.unsigned
+               (Integers.Ptrofs.repr
+                  (4 *
+                   uvalueToZ
+                     (vplus
+                        (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3)
+                           (ZToValue 32 (z0 / 4)) ?EQ2)
+                        (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4)
+                        ?EQ1))))) by admit.
+
+        rewrite <- H19 in H6.
+        rewrite H0 in H6.
+        invert H6.
+        assert (forall x, Z.to_nat (uvalueToZ x) = valueToNat x) as VALUE_IDENTITY by admit.
+        rewrite VALUE_IDENTITY in H21.
+        assumption.
+
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        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 H3.
+        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.
+
+        unfold reg_stack_based_pointers. intros.
+        destruct (Pos.eq_dec r2 dst); subst.
+
+        rewrite Registers.Regmap.gss.
+
+        unfold arr_stack_based_pointers in ASBP.
+        specialize (ASBP ((Integers.Ptrofs.unsigned
+            (Integers.Ptrofs.add i0
+               (Integers.Ptrofs.of_int
+                  (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z))
+                     (Integers.Int.repr z0))))) / 4)).
+        exploit ASBP; auto; intros.
+        1: {
+          split.
+          - admit. (*apply Z.div_pos; lia.*)
+          - admit. (* apply Zmult_lt_reg_r with (p := 4); try lia. *)
+            (* repeat rewrite ZLib.div_mul_undo; lia. *)
+        }
+        replace (4 * ((Integers.Ptrofs.unsigned
+            (Integers.Ptrofs.add i0
+               (Integers.Ptrofs.of_int
+                  (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z))
+                     (Integers.Int.repr z0)))))  / 4)) with (Integers.Ptrofs.unsigned
+            (Integers.Ptrofs.add i0
+               (Integers.Ptrofs.of_int
+                  (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z))
+                     (Integers.Int.repr z0)))))  in H0.
+        2: {
+          rewrite Z.mul_comm.
+          admit.
+          (* rewrite ZLib.div_mul_undo; lia. *)
+        }
+        rewrite Integers.Ptrofs.repr_unsigned in H0.
+        simplify.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity.
+        rewrite H4 in H0.
+        setoid_rewrite Integers.Ptrofs.add_zero_l in H0.
+        rewrite H1 in H0.
+        simplify.
+        assumption.
+
+        rewrite Registers.Regmap.gso; auto.
 
       + invert MARR. simplify.
 
@@ -646,7 +779,32 @@ Section CORRECTNESS.
         eauto. apply combine_none.
         assumption.
 
-        (* FIXME: RSBP Proof. *)
+        unfold reg_stack_based_pointers. intros.
+        destruct (Pos.eq_dec r0 dst); subst.
+
+        rewrite Registers.Regmap.gss.
+
+        unfold arr_stack_based_pointers in ASBP.
+        specialize (ASBP (Integers.Ptrofs.unsigned i0 / 4)).
+        exploit ASBP; auto; intros.
+        1: {
+          split.
+          - apply Z.div_pos; lia.
+          - apply Zmult_lt_reg_r with (p := 4); try lia.
+            repeat rewrite ZLib.div_mul_undo; lia.
+        }
+        replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0.
+        2: {
+          rewrite Z.mul_comm.
+          rewrite ZLib.div_mul_undo; lia.
+        }
+        rewrite Integers.Ptrofs.repr_unsigned in H0.
+        simplify.
+        rewrite H1 in H0.
+        simplify.
+        assumption.
+
+        rewrite Registers.Regmap.gso; auto.
 
     - destruct c, chunk, addr, args; simplify; rt; simplify.
       + admit.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 18a69ef..ad946ca 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -294,6 +294,11 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     forall i v',
     i = valueToInt v' ->
     val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+    forall b off v',
+    off = Ptrofs.repr (valueToZ v') ->
+    (Z.modulo (valueToZ v') 4) = 0%Z ->
+    val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
 Inductive opt_val_value_lessdef: option val -> value -> Prop :=