a bit more cleaning

5 files changed, 21 insertions, 44 deletions

diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index 7855d375..9f646ad0 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -46,7 +46,6 @@ Proof.
   inversion_ASSERT; try_simplify_someHyps.
 Qed.
 
-(* FIXME - what about trap? *)
 Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node)  :=
   match i with
   | Inop pc' => Some (alive, pc')
@@ -63,7 +62,7 @@ Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): opti
   | Icond cond args ifso ifnot _ =>
       ASSERT list_mem args alive IN
       exit_checker pm alive ifso (alive, ifnot)
-  | _ => None (* TODO jumptable ? *)
+  | _ => None
   end.
 
 
@@ -109,6 +108,20 @@ Proof.
   * intros; eapply iinst_checker_path_entry; eauto.
 Qed.
 
+
+Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
+  ipath_checker path f (fn_path f) alive pc = Some res
+  -> nth_default_succ (fn_code f) path pc = Some (snd res).
+Proof.
+  induction path; simpl.
+  + try_simplify_someHyps.
+  + intros alive pc res.
+    inversion_SOME i; intros INST.
+    inversion_SOME res0; intros ICHK IPCHK.
+    rewrite INST.
+    erewrite iinst_checker_default_succ; eauto.
+Qed.
+
 Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
   match or with None => true | Some r => Regset.mem r alive end.
 
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index bd26171d..bdd4bda8 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -764,7 +764,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
       DO vargs <~ hlist_args prev args ;;
       let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
       RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
-  | _ => RET None (* TODO jumptable ? *)
+  | _ => RET None
   end.
 
 
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index eec0bc51..aa8db342 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -345,31 +345,13 @@ Qed.
 
 Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m':
   ssem_local ge sp loc rs m rs' m' ->
-(*   all_fallthrough ge sp (si_exits st) rs m -> *)
   sabort_local ge sp loc rs m ->
   False.
 Proof.
-  intros SIML (* ALLF *) ABORT. inv SIML. destruct H0 as (H0 & H0').
+  intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0').
   inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
 Qed.
 
-(* TODO: remove this JUNK ?
-Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m':
-  ssem_local ge sp (si_local st) rs m rs' m' ->
-  all_fallthrough ge sp (si_exits st) rs m ->
-  is_tail (ext :: lx) (si_exits st) ->
-  sabort_exit ge sp ext rs m ->
-  False.
-Proof.
-  intros SSEML ALLF TAIL ABORT.
-  inv ABORT.
-  - exploit ALLF; eauto. congruence.
-  - (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions,
-    but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove
-    a lack of abort on the si_elocal.. We must change the definitions *)
-Abort.
-*)
-
 Lemma ssem_local_exclude_sabort ge sp st rs m rs' m':
   ssem_local ge sp (si_local st) rs m rs' m' ->
   all_fallthrough ge sp (si_exits st) rs m ->
@@ -497,7 +479,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate :=
       let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
       let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in
       Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |}
-  | _ => None (* TODO jumptable ? *)
+  | _ => None
   end.
 
 Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 72a4ee01..a9c2fa76 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -260,19 +260,6 @@ Proof.
     + rewrite <- H. erewrite <- seval_preserved; eauto.
 Qed.
 
-Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
-  ipath_checker path f (fn_path f) alive pc = Some res
-  -> nth_default_succ (fn_code f) path pc = Some (snd res).
-Proof.
-  induction path; simpl.
-  + try_simplify_someHyps.
-  + intros alive pc res.
-    inversion_SOME i; intros INST.
-    inversion_SOME res0; intros ICHK IPCHK.
-    rewrite INST.
-    erewrite iinst_checker_default_succ; eauto.
-Qed.
-
 Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
   (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
           (irs is) (imem is) t s)
@@ -331,17 +318,14 @@ Qed.
 Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
   (liveness_ok_function f) ->
   (fn_path f) ! pc0 = Some path0 ->
-  (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *)  (* NB: should be useless *)
   sexec f pc0 = Some st -> 
-  (* icontinue is = true -> *)
   list_forall2 match_stackframes stk stk' ->
-  (* ssem_internal ge sp st rs0 m0 is -> *)
   ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
   eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
   exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
 Proof.
   Local Hint Resolve eqlive_stacks_refl: core.
-  intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
+  intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE.
   (* start decomposing path_checker *)
   generalize (LIVE pc0 path0 PATH0).
   unfold path_checker.
@@ -413,7 +397,6 @@ Qed.
 (* The main theorem on simulation of symbolic states ! *)
 Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
   (fn_path f) ! pc0 = Some path0 ->
-  (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *)
   sexec f pc0 = Some st -> 
   match_function dm f f' ->
   liveness_ok_function f ->
@@ -422,7 +405,7 @@ Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
   (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
   exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
 Proof.
-  intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
+  intros PATH0 SEXEC MFUNC LIVE STACKS SEM SIMU.
   destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
   destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
   - (* sem_early *)
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v
index 0ddc3142..63b914ec 100644
--- a/scheduling/RTLpathWFcheck.v
+++ b/scheduling/RTLpathWFcheck.v
@@ -31,14 +31,13 @@ Proof.
   inversion_SOME path; try_simplify_someHyps.
 Qed.
 
-(* FIXME - what about trap? *)
 Definition iinst_checker (pm: path_map) (i: instruction): option (node)  :=
   match i with
   | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc'
   | Istore _ _ _ _ pc' => Some (pc')
   | Icond cond args ifso ifnot _ =>
       exit_checker pm ifso ifnot
-  | _ => None (* TODO jumptable ? *)
+  | _ => None
   end.
 
 Local Hint Resolve exit_checker_path_entry: core.