remove dep of exec_arith_instr on memory.

TODO:
 - prove admitted lemma in Asmblockdeps.
 - remove axioms in Asmblock if possible.

3 files changed, 77 insertions, 66 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3305bf95..0d6c2e79 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -902,20 +902,29 @@ Definition cmpu_for_btest (bt: btest) :=
   | _ => (None, Int)
   end.
 
-(* FIXME: move these axioms and definitions in a separate file (e.g. PatchMemoryModel). *)
-Axiom Val_cmpu_bool: comparison -> val -> val -> option bool.
+(* FIXME: put this stuff related to the memory model in a distinct module *)
+(* FIXME: currently, only deal with the special case with Archi.ptr64 = true *)
+Definition Val_cmpu_bool c v1 v2: option bool :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2)
+  | _, _ => None
+  end.
 
-Axiom Val_cmpu_bool_correct: forall (m:mem) (cmp: comparison) (v1 v2: val) b,
+Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
    (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
    -> (Val_cmpu_bool cmp v1 v2) = Some b.
+Proof.
+  unfold Val.cmpu_bool, Val_cmpu_bool. 
+  destruct v1, v2; try congruence; vm_compute; try congruence.
+Qed.
 
 Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
 
-Lemma Val_cmpu_correct: forall (m:mem) (cmp: comparison) (v1 v2: val),
+Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
    Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
                (Val_cmpu cmp v1 v2).
 Proof.
-  intros; unfold Val.cmpu, Val_cmpu.
+  unfold Val.cmpu, Val_cmpu.
   remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
   destruct ob; simpl.
   - erewrite Val_cmpu_bool_correct; eauto.
@@ -923,6 +932,27 @@ Proof.
   - econstructor.
 Qed.
 
+Axiom Val_cmplu_bool: forall (cmp: comparison) (v1 v2: val), option bool.
+
+Axiom Val_cmplu_bool_correct: forall (m:mem) (cmp: comparison) (v1 v2: val) b,
+   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmplu_bool cmp v1 v2) = Some b.
+
+Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
+
+Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
+               (Val_cmplu cmp v1 v2).
+Proof.
+  unfold Val.cmplu, Val_cmplu.
+  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite Val_cmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
+
 (** Comparing integers *)
 Definition compare_int (t: itest) (v1 v2: val): val :=
   match t with
@@ -944,7 +974,7 @@ Definition compare_int (t: itest) (v1 v2: val): val :=
   | ITnone => Vundef
   end.
 
-Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
+Definition compare_long (t: itest) (v1 v2: val): val :=
   let res := match t with
   | ITne  => Val.cmpl Cne v1 v2
   | ITeq  => Val.cmpl Ceq v1 v2
@@ -952,12 +982,12 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
   | ITge  => Val.cmpl Cge v1 v2
   | ITle  => Val.cmpl Cle v1 v2
   | ITgt  => Val.cmpl Cgt v1 v2
-  | ITneu => Val.cmplu (Mem.valid_pointer m) Cne v1 v2
-  | ITequ => Val.cmplu (Mem.valid_pointer m) Ceq v1 v2
-  | ITltu => Val.cmplu (Mem.valid_pointer m) Clt v1 v2
-  | ITgeu => Val.cmplu (Mem.valid_pointer m) Cge v1 v2
-  | ITleu => Val.cmplu (Mem.valid_pointer m) Cle v1 v2
-  | ITgtu => Val.cmplu (Mem.valid_pointer m) Cgt v1 v2
+  | ITneu => Some (Val_cmplu Cne v1 v2)
+  | ITequ => Some (Val_cmplu Ceq v1 v2)
+  | ITltu => Some (Val_cmplu Clt v1 v2)
+  | ITgeu => Some (Val_cmplu Cge v1 v2)
+  | ITleu => Some (Val_cmplu Cle v1 v2)
+  | ITgtu => Some (Val_cmplu Cgt v1 v2)
   | ITall
   | ITnall
   | ITany
@@ -995,14 +1025,12 @@ Definition compare_float (t: ftest) (v1 v2: val): val :=
 
 TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma...
 
-FIXME: replace parameter "m" by a function corresponding to the resul of "(Mem.valid_pointer m)"
-
 *)
 
 Variable ge: genv.
 
 
-Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset :=
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR n d =>
       match n with
@@ -1060,7 +1088,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
   | PArithRRR n d s1 s2 =>
       match n with
       | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2)
-      | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m)
+      | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2)
       | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2)
       | Pfcompl c => rs#d <- (compare_float c rs#s1 rs#s2)
       | Paddw  => rs#d <- (Val.add  rs#s1 rs#s2)
@@ -1108,7 +1136,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
 
   | PArithRRI64 n d s i =>
       match n with
-      | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i) m)
+      | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i))
       | Paddil  => rs#d <- (Val.addl rs#s (Vlong i))
       | Pandil  => rs#d <- (Val.andl rs#s (Vlong i))
       | Poril   => rs#d <- (Val.orl  rs#s (Vlong i))
@@ -1156,7 +1184,7 @@ Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
 
 Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :=
  match bi with
- | PArith ai => Next (exec_arith_instr ai rs m) m
+ | PArith ai => Next (exec_arith_instr ai rs) m
 
  | PLoadRRO n d a ofs =>
       match n with
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index fa21d3b1..fc012557 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -154,7 +154,7 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
   | OArithRRR n, [Val v1; Val v2; Memstate m] =>
       match n with
       | Pcompw c => Some (Val (compare_int c v1 v2))
-      | Pcompl c => Some (Val (compare_long c v1 v2 m))
+      | Pcompl c => Some (Val (compare_long c v1 v2))
       | _ => None
       end
 
@@ -193,14 +193,9 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
       | _ => None
       end
 
-  | OArithRRI32 n i, [Val v; Memstate m] =>
-      match n with
-      | Pcompiw c => Some (Val (compare_int c v (Vint i)))
-      | _ => None
-      end
-
   | OArithRRI32 n i, [Val v] =>
       match n with
+      | Pcompiw c => Some (Val (compare_int c v (Vint i)))
       | Paddiw  => Some (Val (Val.add   v (Vint i)))
       | Pandiw  => Some (Val (Val.and   v (Vint i)))
       | Poriw   => Some (Val (Val.or    v (Vint i)))
@@ -211,22 +206,15 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
       | Psllil  => Some (Val (Val.shll  v (Vint i)))
       | Psrlil  => Some (Val (Val.shrlu v (Vint i)))
       | Psrail  => Some (Val (Val.shrl  v (Vint i)))
-      | _ => None
-      end
-
-  | OArithRRI64 n i, [Val v; Memstate m] =>
-      match n with
-      | Pcompil c => Some (Val (compare_long c v (Vlong i) m))
-      | _ => None
       end
 
   | OArithRRI64 n i, [Val v] =>
       match n with
+      | Pcompil c => Some (Val (compare_long c v (Vlong i)))
       | Paddil  => Some (Val (Val.addl v (Vlong i)))
       | Pandil  => Some (Val (Val.andl v (Vlong i)))
       | Poril   => Some (Val (Val.orl  v (Vlong i)))
       | Pxoril  => Some (Val (Val.xorl  v (Vlong i)))
-      | _ => None
       end
 
   | _, _ => None
@@ -796,7 +784,7 @@ Qed.
 
 Lemma trans_arith_correct:
   forall ge fn i rs m rs' s,
-  exec_arith_instr ge i rs m = rs' ->
+  exec_arith_instr ge i rs = rs' ->
   match_states (State rs m) s ->
   exists s',
      macro_run (Genv ge fn) (trans_arith i) s s = Some s'
@@ -851,9 +839,11 @@ Proof.
       destruct (ireg_eq g rd); subst; Simpl ].
 (* PArithRRI32 *)
   - destruct i.
+Admitted.
+(* FIXME: A FINIR
     all: inv H; inv H0;
     eexists; split; try split;
-    [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity
+    [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); auto
     | Simpl
     | intros rr; destruct rr; Simpl;
       destruct (ireg_eq g rd); subst; Simpl ].
@@ -866,6 +856,7 @@ Proof.
     | intros rr; destruct rr; Simpl;
       destruct (ireg_eq g rd); subst; Simpl ].
 Qed.
+*)
 
 Lemma forward_simu_basic:
   forall ge fn b rs m rs' m' s,
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index e6e5d11e..d9ce95ab 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -374,7 +374,7 @@ Lemma transl_compu_correct:
   exists rs',
      exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ (Val_cmpu_bool (*Mem.valid_pointer m*) cmp rs#r1 rs#r2 = Some b ->
+  /\ (Val_cmpu_bool cmp rs#r1 rs#r2 = Some b ->
        exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -390,7 +390,7 @@ Proof.
       assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val_cmpu_bool (*Mem.valid_pointer m*) cmp rs#r1 rs#r2) as cmpubool.
+      remember (Val_cmpu_bool cmp rs#r1 rs#r2) as cmpubool.
       destruct cmp; simpl; unfold Val_cmpu;
         rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
       destruct b0; simpl; auto.
@@ -413,16 +413,16 @@ Proof.
 - split.
   + intros; Simpl.
   + intros.
-    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)) as rs'.
     simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
     { 
-      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
       remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool.
       destruct cmp; simpl;
-      unfold compare_long;
-      unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      unfold compare_long, Val.cmpl;
+      rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
       destruct b0; simpl; auto.
     }
     rewrite H0. simpl; auto.
@@ -433,7 +433,7 @@ Lemma transl_complu_correct:
   exists rs',
      exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
-  /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2 = Some b ->
+  /\ ( Val_cmplu_bool cmp rs#r1 rs#r2 = Some b ->
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
@@ -443,16 +443,15 @@ Proof.
 - split.
   + intros; Simpl.
   + intros.
-    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)) as rs'.
     simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
     { 
-      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)).
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
       { rewrite Heqrs'. auto. }
       rewrite H0. rewrite <- H.
-      remember (Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2) as cmpbool.
+      remember (Val_cmplu_bool cmp rs#r1 rs#r2) as cmpbool.
       destruct cmp; simpl;
-      unfold compare_long;
-      unfold Val.cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
       destruct b0; simpl; auto.
     }
     rewrite H0. simpl; auto.
@@ -608,7 +607,7 @@ Proof.
     destruct cmp; discriminate.
 Qed.
 
-Local Hint Resolve Val_cmpu_bool_correct.
+Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct.
 
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m' tbb,
@@ -701,7 +700,7 @@ Proof.
   exists rs', (Pcb BTwnez RTMP lbl).
   split.
   + constructor. eexact A.
-  + split; auto. apply C; auto.
+  + split; auto. apply C; eauto.
 (* Ccomplimm *)
 - remember (Int64.eq n Int64.zero) as eqz.
   destruct eqz.
@@ -862,12 +861,12 @@ Lemma transl_cond_int64u_correct:
   forall cmp rd r1 r2 k rs m,
   exists rs',
      exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
-  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 rs#r2)
+  /\ rs'#rd = Val_cmplu cmp rs#r1 rs#r2
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
   intros. destruct cmp; simpl. 
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
+  split; intros; Simpl. 
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
@@ -903,7 +902,7 @@ Proof.
   split; intros; Simpl.
 Qed.
 
-Local Hint Resolve Val_cmpu_correct.
+Local Hint Resolve Val_cmpu_correct Val_cmplu_correct.
 
 Lemma transl_condimm_int32u_correct:
   forall cmp rd r1 n k rs m,
@@ -959,19 +958,10 @@ Lemma transl_condimm_int64u_correct:
   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
 Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
-  split; intros; Simpl.
+  intros. destruct cmp; simpl;
+  (econstructor; split; 
+  [ apply exec_straight_one; [simpl; eauto] | 
+    split; intros; Simpl; unfold compare_long; eauto]).
 Qed.
 
 Lemma swap_comparison_cmpfs:
@@ -1000,7 +990,8 @@ Proof.
   split; intros; Simpl. apply swap_comparison_cmpfs.
 - econstructor; split. apply exec_straight_one; [simpl; eauto].
   split; intros; Simpl. apply swap_comparison_cmpfs.
-- econstructor; split. apply exec_straight_one; [simpl; eauto].
+- econstructor; split. apply exec_straight_one; [simpl;
+ eauto].
   split; intros; Simpl.
 Qed.
 
@@ -1133,6 +1124,7 @@ Proof.
 + (* cmplu *)
   exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C).
   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
+  eapply Val_cmplu_correct.
 + (* cmplimm *)
   exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. 
   intros (rs' & A & B & C).