Fix Inop

1 files changed, 22 insertions, 8 deletions

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index a9626c4..f0508bd 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -17,7 +17,7 @@
  *)
 
 From compcert Require RTL Op Maps Errors.
-From compcert Require Import Maps.
+From compcert Require Import Maps Integers.
 From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap.
 Require Import Lia.
 
@@ -117,13 +117,17 @@ translations for each of the elements *)
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
+      Z.pos n <= Int.max_unsigned ->
       tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
     forall n op args dst s s' e i,
+      Z.pos n <= Int.max_unsigned ->
       translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
+      Z.pos n1 <= Int.max_unsigned ->
+      Z.pos n2 <= Int.max_unsigned ->
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
@@ -135,10 +139,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
                (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
+      Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i c src n,
+      Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
                (state_goto st n)
@@ -415,12 +421,12 @@ Lemma transf_instr_freshreg_trans :
 Proof.
   intros. destruct instr eqn:?. subst. unfold transf_instr in H.
   destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
+  - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
+  - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
-  - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
+  - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
+  - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
     congruence.
   - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.
 Qed.
@@ -445,13 +451,16 @@ Ltac rewrite_states :=
 
 Ltac inv_add_instr' H :=
   match type of H with
+  | ?f _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H
   end; repeat unfold_match H; inversion H.
 
 Ltac inv_add_instr :=
-  lazymatch goal with
+  match goal with
+  | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr
   | H: context[add_instr_skip _ _ _] |- _ =>
     inv_add_instr' H
   | H: context[add_instr_skip _ _] |- _ =>
@@ -491,23 +500,27 @@ Proof.
     + 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.
+      apply Z.leb_le. assumption.
       eapply in_map with (f := fst) in H9. contradiction.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence.
-      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
+      econstructor. apply Z.leb_le; assumption.
+      apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + 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 EQ1. eapply in_map with (f := fst) in H14. contradiction.
+      econstructor. apply Z.leb_le; assumption.
+      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.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct H2.
       * inversion H2.
         replace (st_st s2) with (st_st s0) by congruence.
+        econstructor. apply Z.leb_le; assumption.
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.
 
@@ -516,6 +529,7 @@ Proof.
     + destruct H2.
       * inversion H2.
         replace (st_st s2) with (st_st s0) by congruence.
+        econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN).
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.