Rough outline of stack address proof

3 files changed, 109 insertions, 34 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d5a8af2..cba2940 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -314,21 +314,21 @@ 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 addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
-  | Op.Ascaled scale offset, r1::nil =>
+  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
+  | Mint32, Op.Ascaled scale offset, r1::nil =>
     if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
     then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4)))))
     else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+  | 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))
     then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4))))
     else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+  | 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 "Veriloggen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
+  | _, _, _ => 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 1f9e368..34fa8ec 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -51,7 +51,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem
         0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) ->
         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)))
-                              (nth (Z.to_nat ptr) stack (ZToValue 32 0))) ->
+                              (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) ->
     match_arrs m f sp mem asa.
 
 Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
@@ -425,38 +425,113 @@ Section CORRECTNESS.
         | [ H: Values.Vptr _ _ = Values.Vptr _ _ |- _]  => invert H
         end.
 
-    - destruct c, addr, args; simplify; rt; t; simplify.
+      Opaque Nat.div.
+
+    - destruct c, chunk, addr, args; simplify; rt; simplify.
 
       + admit. (* FIXME: Alignment *)
+      + admit.
+      + admit.
 
+      + invert MARR. simplify.
 
-      + unfold Op.eval_addressing in *.
-        (* destruct (Archi.ptr64); simplify; *)
-        (*   destruct (Registers.Regmap.get r0 rs); simplify. *)
-        admit.
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
 
-        (* eexists. split. *)
-        (* eapply Smallstep.plus_one. *)
-        (* eapply HTL.step_module; eauto. *)
-        (* econstructor. econstructor. econstructor. simpl. *)
-        (* econstructor. econstructor. econstructor. econstructor. econstructor. *)
-        (* econstructor. econstructor. econstructor. econstructor. econstructor. *)
-        (* econstructor. econstructor. econstructor. simpl. *)
+        (* Out of bounds reads are undefined behaviour. *)
+        assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr ->
+                         Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v ->
+                         v = Values.Vundef) as INVALID_READ by admit.
 
-        (* inversion MARR; subst; clear MARR. simpl in *. *)
-        (* unfold Verilog.arr_assocmap_lookup. *)
-        (* rewrite H3. *)
+        (* Case split on whether read is out of bounds. *)
+        destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND.
+        * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. {
+            apply Zle_bool_imp_le. assumption.
+          }
+          eapply INVALID_READ in OUT_OF_BOUNDS.
+          2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. }
 
-        (* admit. *)
+          eexists. split.
+          eapply Smallstep.plus_one.
+          eapply HTL.step_module; eauto.
+          econstructor. econstructor. econstructor. simplify.
+          econstructor. econstructor. econstructor. econstructor. simplify.
 
-      + unfold Op.eval_addressing in *.
-        (* destruct (Archi.ptr64); simplify; *)
-        (* destruct (Registers.Regmap.get r0 rs); *)
-        (*   destruct (Registers.Regmap.get r1 rs); simplify; *)
-        (*     destruct (Archi.ptr64); simplify. *)
-        admit.
+          unfold Verilog.arr_assocmap_lookup. rewrite H3.
+          reflexivity.
 
-      + admit.
+          simplify. unfold_merge. apply AssocMap.gss.
+
+          simplify. rewrite assumption_32bit.
+          constructor.
+
+          unfold_merge.
+          apply regs_lessdef_add_greater.
+          apply greater_than_max_func.
+
+          apply regs_lessdef_add_match.
+          rewrite OUT_OF_BOUNDS.
+          constructor. assumption.
+
+          assumption.
+
+          unfold state_st_wf. inversion 1. simplify.
+          unfold_merge. apply AssocMap.gss.
+
+          assumption.
+
+          econstructor; simplify; try reflexivity; eassumption.
+
+        * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. {
+            rewrite Z.leb_antisym in BOUND.
+            rewrite negb_false_iff in BOUND.
+            apply Zlt_is_lt_bool. assumption.
+          }
+
+          eexists. split.
+          eapply Smallstep.plus_one.
+          eapply HTL.step_module; eauto.
+          econstructor. econstructor. econstructor. simplify.
+          econstructor. econstructor. econstructor. econstructor. simplify.
+
+          unfold Verilog.arr_assocmap_lookup. rewrite H3.
+          reflexivity.
+
+          simplify. unfold_merge. apply AssocMap.gss.
+
+          simplify. rewrite assumption_32bit.
+          constructor.
+
+          unfold_merge.
+          apply regs_lessdef_add_greater.
+          apply greater_than_max_func.
+
+          apply regs_lessdef_add_match.
+
+          assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4))))
+                 by admit.
+          simplify. rewrite <- H5.
+          specialize (H4 x).
+          assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit.
+          apply H4 in H0.
+          invert H0.
+          assert (Integers.Ptrofs.repr x = i0) by admit.
+          rewrite H0 in H6.
+          rewrite H1 in H6.
+          invert H6.
+          assumption.
+
+          assumption.
+
+          assumption.
+
+          unfold state_st_wf. inversion 1. simplify.
+          unfold_merge. apply AssocMap.gss.
+
+          assumption.
+
+          econstructor; simplify; try reflexivity; eassumption.
 
     - admit.
 
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 845d706..0e999de 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -56,10 +56,10 @@ Definition merge_associations {A : Type} (assoc : associations A) :=
   mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
                  (AssocMap.empty A).
 
-Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
+Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value :=
   match a ! r with
-  | None => None
-  | Some arr => nth_error arr i
+  | None => natToValue 32 0
+  | Some arr => nth i arr (natToValue 32 0)
   end.
 
 Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
@@ -297,7 +297,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
   | erun_Vvari :
       forall fext reg stack v iexp i r,
       expr_runp fext reg stack iexp i ->
-      arr_assocmap_lookup stack r (valueToNat i) = Some v ->
+      arr_assocmap_lookup stack r (valueToNat i) = v ->
       expr_runp fext reg stack (Vvari r iexp) v
   | erun_Vinputvar :
       forall fext reg stack r v,