fix bug and forward in proofs

2 files changed, 18 insertions, 2 deletions

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 0e71b6b5..660d0458 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -250,13 +250,14 @@ Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
 Definition apply_instr instr x :=
   match instr with
   | Inop _
+  | Icond _ _ _ _
   | Istore _ _ _ _ _ => Some x
   | Iop Omove (src :: nil) dst _ => Some (move src dst x)
   | Iop _ _ dst _
   | Iload _ _ _ _ dst _
   | Icall _ _ _ dst _ => Some (kill dst x)
   | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
-  | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
+  | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
   end.
 
 Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 99b546c7..aa516df4 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -403,7 +403,22 @@ Proof.
   rewrite subst_args_ok; eassumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    destruct b; tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* jumptbl *)
 - econstructor; split.