From b59a2e2913aa7ad010c0652e909ae790c07c7281 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 17:47:21 +0100
Subject: Enforce stack size alignment to fix proof.

---
 src/translation/HTLgen.v      |  4 +++-
 src/translation/HTLgenproof.v | 25 +++++++++++++++++--------
 src/translation/HTLgenspec.v  |  3 ++-
 3 files changed, 22 insertions(+), 10 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 73f2b63..f661aa6 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -436,6 +436,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
               (create_arr_state_incr s sz ln i).
 
 Definition transf_module (f: function) : mon module :=
+  if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then
   do fin <- create_reg (Some Voutput) 1;
   do rtrn <- create_reg (Some Voutput) 32;
   do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
@@ -459,7 +460,8 @@ Definition transf_module (f: function) : mon module :=
          rst
          clk
          current_state.(st_scldecls)
-         current_state.(st_arrdecls)).
+         current_state.(st_arrdecls))
+  else error (Errors.msg "Stack size misalignment.").
 
 Definition max_state (f: function) : state :=
   let st := Pos.succ (max_reg_function f) in
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index a5396af..77a11dc 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -482,8 +482,8 @@ Section CORRECTNESS.
 
         (** Here we are assuming that any stack read will be within the bounds
             of the activation record. *)
-        assert (0 <= Integers.Ptrofs.unsigned i0 / 4) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.unsigned i0 / 4 < f.(RTL.fn_stacksize) / 4) as READ_BOUND_HIGH by admit.
+        assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
+        assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
         eexists. split.
         eapply Smallstep.plus_one.
@@ -509,16 +509,25 @@ Section CORRECTNESS.
         (** Equality proof *)
         (* FIXME: 32-bit issue. *)
         assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit.
-        assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) as MOD_IDENTITY.
-        {
-          rewrite Z.mul_comm.
-          rewrite ZLib.div_mul_undo; lia.
-        }
         rewrite VALUE_IDENTITY.
         specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)).
         rewrite Z2Nat.id in H5; try lia.
         exploit H5; auto; intros.
-        rewrite MOD_IDENTITY in H0.
+        1: {
+          split.
+          - apply Z.div_pos; lia.
+          - apply Zmult_lt_reg_r with (p := 4); try lia.
+            repeat rewrite ZLib.div_mul_undo; lia.
+        }
+        2: {
+          assert (0 < RTL.fn_stacksize f) by lia.
+          apply Z.div_pos; 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.
         rewrite H1 in H0.
         invert H0. assumption.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 1a9144c..a916cb5 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -188,6 +188,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop :=
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
+      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
@@ -451,7 +452,7 @@ Proof.
   inversion s; subst.
 
   unfold transf_module in *.
-  monadInv Heqr.
+  destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr.
 
   (* TODO: We should be able to fold this into the automation. *)
   pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN.
-- 
cgit