Check chunk size during translation.

2 files changed, 33 insertions, 19 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 65b6627..04de548 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -442,17 +442,25 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
         do _ <- declare_reg None dst 32;
         add_instr n n' (nonblock dst instr)
       else error (Errors.msg "State is larger than 2^32.")
-    | Iload mem addr args dst n' =>
-      if Z.leb (Z.pos n') Integers.Int.max_unsigned
-      then do addr' <- translate_eff_addressing addr args;
-           do _ <- declare_reg None dst 32;
-           add_instr n n' $ create_single_cycle_load stack addr' dst
-      else error (Errors.msg "State is larger than 2^32.")
-    | Istore mem addr args src n' =>
-      if Z.leb (Z.pos n') Integers.Int.max_unsigned
-      then do addr' <- translate_eff_addressing addr args;
-           add_instr n n' $ create_single_cycle_store stack addr' src
-      else error (Errors.msg "State is larger than 2^32.")
+    | Iload chunk addr args dst n' =>
+      match chunk with
+      | Mint32 =>
+        if Z.leb (Z.pos n') Integers.Int.max_unsigned
+        then do addr' <- translate_eff_addressing addr args;
+             do _ <- declare_reg None dst 32;
+             add_instr n n' $ create_single_cycle_load stack addr' dst
+        else error (Errors.msg "State is larger than 2^32.")
+      | _ => error (Errors.msg "Iload invalid chunk size.")
+      end
+    | Istore chunk addr args src n' =>
+      match chunk with
+      | Mint32 =>
+        if Z.leb (Z.pos n') Integers.Int.max_unsigned
+        then do addr' <- translate_eff_addressing addr args;
+             add_instr n n' $ create_single_cycle_store stack addr' src
+        else error (Errors.msg "State is larger than 2^32.")
+      | _ => error (Errors.msg "Istore invalid chunk size.")
+      end
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index aba5d0c..dda91ca 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -138,16 +138,18 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
-    forall mem addr args s s' i e dst n,
+    forall chunk addr args s s' i e dst n,
       Z.pos n <= Int.max_unsigned ->
+      chunk = AST.Mint32 ->
       translate_eff_addressing addr args s = OK e s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n)
+      tr_instr fin rtrn st stk (RTL.Iload chunk addr args dst n)
                                (create_single_cycle_load stk e dst) (state_goto st n)
 | tr_instr_Istore :
-    forall mem addr args s s' i e src n,
+    forall chunk addr args s s' i e src n,
       Z.pos n <= Int.max_unsigned ->
+      chunk = AST.Mint32 ->
       translate_eff_addressing addr args s = OK e s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n)
+      tr_instr fin rtrn st stk (RTL.Istore chunk addr args src n)
                                (create_single_cycle_store stk e src) (state_goto st n)
 | tr_instr_Ijumptable :
     forall cexpr tbl r,
@@ -415,10 +417,12 @@ Proof.
   destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
   - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - monadInv H. apply add_instr_freshreg_trans in EQ2.
+  - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate.
+    monadInv H. apply add_instr_freshreg_trans in EQ2.
     apply translate_eff_addressing_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - monadInv H. apply add_instr_freshreg_trans in EQ0.
+  - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate.
+    monadInv H. apply add_instr_freshreg_trans in EQ0.
     apply translate_eff_addressing_freshreg_trans in EQ. congruence.
   - monadInv H. apply translate_condition_freshreg_trans in EQ.
     apply add_branch_instr_freshreg_trans in EQ0.
@@ -491,7 +495,8 @@ Proof.
   destruct (peq pc pc1).
   - subst.
     destruct instr1 eqn:?; try discriminate;
-      try destruct_optional; inv_add_instr; econstructor; try assumption.
+      try destruct_optional; try (destruct m; try discriminate);
+        inv_add_instr; econstructor; try assumption.
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
@@ -508,6 +513,7 @@ Proof.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence.
       econstructor. apply Z.leb_le; assumption.
+      reflexivity.
       apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
@@ -516,7 +522,7 @@ Proof.
       * inversion H2.
         replace (st_st s2) with (st_st s0) by congruence.
         econstructor. apply Z.leb_le; assumption.
-        eauto with htlspec.
+        eauto with htlspec. eassumption.
       * apply in_map with (f := fst) in H2. contradiction.
 
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.