Revert "Modifying RTLpath in order to allow for stopping at Icond"

This reverts commit b6a6e7b783cc59f2efd2fc2470f6676d88d3f58f.

1 files changed, 11 insertions, 23 deletions

diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index 4ade0ad1..228bc95b 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -49,12 +49,7 @@ Definition default_succ (i: instruction): option node :=
   | Iop op args res s => Some s
   | Iload _ chunk addr args dst s => Some s
   | Istore chunk addr args src s => Some s
-  | Icond cond args ifso ifnot pred =>
-      match pred with
-      | None => None
-      | Some true => None (* TODO rework RTL and Duplicate so that pred is a boolean ? *)
-      | Some false => Some ifnot
-      end
+  | Icond cond args ifso ifnot _ => Some ifnot
   | _ => None (* TODO: we could choose a successor for jumptable ? *)
   end.
 
@@ -146,6 +141,7 @@ Coercion program_RTL: program >-> RTL.program.
 
 Record istate := mk_istate { icontinue: bool; ipc: node; irs: regset; imem: mem }.
 
+(* FIXME - prediction *)
 (* Internal step through the path *)
 Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate :=
   match i with
@@ -170,14 +166,9 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem)
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
       Some (mk_istate true pc' rs m')
-  | Icond cond args ifso ifnot pred =>
+  | Icond cond args ifso ifnot _ =>
       SOME b <- eval_condition cond rs##args m IN
-      let nc := match pred with
-      | None => false
-      | Some true => false
-      | Some false => negb b
-      end
-      in Some (mk_istate nc (if b then ifso else ifnot) rs m)
+      Some (mk_istate (negb b) (if b then ifso else ifnot) rs m)
   | _ => None (* TODO jumptable ? *)
   end.
 
@@ -720,7 +711,7 @@ Proof.
   Local Hint Resolve Icond_early_exit: core.
   destruct i; simpl; try congruence; simplify_SOME b; simpl; try congruence.
   all: explore_destruct; simplify_SOME b; try discriminate.
-Abort. (* this lemma isn't true anymore *)
+Qed.
 
 Section COMPLETENESS.
 
@@ -881,9 +872,7 @@ Proof.
       econstructor; eauto.
       * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
       * simpl; eauto.
-    - (* Icond *)
-      admit.
-    - (* Ijumptable *)
+   - (* Ijumptable *)
       intros; exploit exec_Ijumptable; eauto.
       eexists; intuition eauto.
       unfold match_states, match_inst_states; simpl.
@@ -892,11 +881,11 @@ Proof.
       econstructor; eauto.
       * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
       * simpl; eauto.
-    - (* Ireturn *)
+  - (* Ireturn *)
       intros; exploit exec_Ireturn; eauto.
       eexists; intuition eauto.
       eexists O; unfold match_states, match_inst_states; simpl; intuition eauto.
-Admitted. (* TODO - prove Icond *)
+Qed.
 
 Lemma path_step_complete stack f sp rs m pc t s1' idx path st:
   isteps ge (path.(psize)-idx) f sp rs m pc = Some st ->
@@ -933,8 +922,7 @@ Proof.
     { clear RSTEP.
       exploit isteps_inversion_early; eauto.
       intros (st0 & i & path0 & BOUND0 & PSTEP0 & CONT0 & PC0 & STEP0).
-      admit.
-(*       exploit istep_early_exit; eauto.
+      exploit istep_early_exit; eauto.
       intros (X1 & X2 & EARLY_EXIT).
       destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst.
       exploit (internal_node_path path0); omega || eauto.
@@ -943,7 +931,7 @@ Proof.
       erewrite isteps_normal_exit in Hi'; eauto.
       clear pc' Hpc' STEP0 PSTEP0 BOUND0; try_simplify_someHyps; intros.
       destruct EARLY_EXIT as [cond args ifnot]; simpl in ENTRY;
-      destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto. *)
+      destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto.
     }
     destruct HPATH0 as (path1  & Hpath1).
     destruct (path1.(psize)) as [|ps] eqn:Hpath1size.
@@ -965,7 +953,7 @@ Proof.
       - simpl; eauto.
       - intuition subst.
         repeat eexists; intuition eauto.
-Admitted.
+Qed.
 
 Lemma step_noninst_complete s1 t s1' s2:
   is_inst s1 = false ->