Work on the if-conversion proof

2 files changed, 49 insertions, 32 deletions

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 7f6b59e..53ca944 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -59,13 +59,13 @@ Definition map_if_convert (p: option pred_op) (i: instr) :=
   | _ => i
   end.
 
-Definition if_convert_block (next: node) (b_next: SeqBB.t) (u: unit) (i: instr) :=
+Definition if_convert_block (next: node) (b_next: SeqBB.t) (_: unit) (i: instr) :=
   match i with
   | RBexit p (RBgoto next') =>
       if (next =? next')%positive
-      then (u, map (map_if_convert p) b_next)
-      else (u, i::nil)
-  | _ => (u, i::nil)
+      then (tt, map (map_if_convert p) b_next)
+      else (tt, i::nil)
+  | _ => (tt, i::nil)
   end.
 
 Definition predicated_store i :=
@@ -89,7 +89,7 @@ Definition if_convert (c: code) (main next: node) :=
   | _, _ => c
   end.
 
-Definition get_unconditional_exit (bb: SeqBB.t) := List.nth_error bb (length bb - 1).
+Definition get_unconditional_exit (bb: SeqBB.t) := nth_error bb (length bb - 1).
 
 (* Definition if_convert_block (c: code) (p: predicate) (bb: SeqBB.t) : SeqBB.t := *)
 (*   match get_unconditional_exit bb with *)
@@ -134,7 +134,7 @@ Definition find_backedge (nb: node * SeqBB.t) :=
   filter (fun x => Pos.ltb n x) succs.
 
 Definition find_all_backedges (c: code) : list node :=
-  List.concat (List.map find_backedge (PTree.elements c)).
+  concat (map find_backedge (PTree.elements c)).
 
 Definition has_backedge (entry: node) (be: list node) :=
   any (fun x => Pos.eqb entry x) be.
@@ -166,11 +166,11 @@ Definition is_flat (c: code) (succ: node) :=
 
 Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * SeqBB.t) :=
   let backedges := find_all_backedges c in
-  List.filter (fun x => is_cond_cfi (snd x) &&
-                        (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) &&
-                        all (fun x' => is_flat c x')
-                            (all_successors (snd x))
-              ) (PTree.elements c).
+  filter (fun x => is_cond_cfi (snd x) &&
+                     (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) &&
+                     all (fun x' => is_flat c x')
+                         (all_successors (snd x))
+         ) (PTree.elements c).
 
 Module TupOrder <: TotalLeBool.
   Definition t : Type := positive * positive.
@@ -200,12 +200,16 @@ Definition ifconv_list (headers: list node) (c: code) :=
 (*   let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in *)
 (*   (S (fst p), PTree.set (fst nb) nbb (snd p)). *)
 
+Definition transf_function' (f: function) (n: node * node) : function :=
+  mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize)
+             (if_convert f.(fn_code) (fst n) (snd n))
+             f.(fn_entrypoint).
+
 Definition transf_function (f: function) : function :=
   let (b, _) := build_bourdoncle f in
   let b' := get_loops b in
   let iflist := ifconv_list b' f.(fn_code) in
-  let c := fold_left (fun c n => if_convert c (fst n) (snd n)) iflist f.(fn_code) in
-  mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint).
+  fold_left transf_function' iflist f.
 
 Definition transf_fundef (fd: fundef) : fundef :=
   transf_fundef transf_function fd.
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index b8ed617..c303da9 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -49,24 +49,10 @@ Variant match_stackframe : stackframe -> stackframe -> Prop :=
            (TF: transf_function f = tf),
       match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p).
 
-Variant match_states : state -> state -> Prop :=
-  | match_state :
-    forall stk stk' f tf sp pc rs p m
-           (TF: transf_function f = tf)
-           (STK: Forall2 match_stackframe stk stk'),
-      match_states (State stk f sp pc rs p m) (State stk' tf sp pc rs p m)
-  | match_callstate :
-    forall cs cs' f tf args m
-           (TF: transf_fundef f = tf)
-           (STK: Forall2 match_stackframe cs cs'),
-      match_states (Callstate cs f args m) (Callstate cs' tf args m)
-  | match_returnstate :
-    forall cs cs' v m
-           (STK: Forall2 match_stackframe cs cs'),
-      match_states (Returnstate cs v m) (Returnstate cs' v m).
-
-Definition match_prog (p: program) (tp: program) :=
-  Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+(* c ! pc = fc ! pc *)
+(* \/ (c ! pc = a ++ fc ! pc' ++ b /\ fc ! pc = a ++ if p goto pc' ++ b) *)
+
+Definition bool_order (b: bool): nat := if b then 1 else 0.
 
 Section CORRECTNESS.
 
@@ -75,9 +61,36 @@ Section CORRECTNESS.
   Let ge : genv := Globalenvs.Genv.globalenv prog.
   Let tge : genv := Globalenvs.Genv.globalenv tprog.
 
+  Definition sem_extrap f pc sp in_s in_s' block :=
+    forall out_s block2,
+      SeqBB.step tge sp in_s block out_s ->
+      f.(fn_code) ! pc = Some block2 ->
+      SeqBB.step tge sp in_s' block2 out_s.
+
+  Variant match_states : option SeqBB.t -> state -> state -> Prop :=
+    | match_state_true :
+      forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0
+             (TF: transf_function f = tf)
+             (STK: Forall2 match_stackframe stk stk')
+             (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b)
+             (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)),
+        match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0)
+    | match_callstate :
+      forall cs cs' f tf args m
+             (TF: transf_fundef f = tf)
+             (STK: Forall2 match_stackframe cs cs'),
+        match_states None (Callstate cs f args m) (Callstate cs' tf args m)
+    | match_returnstate :
+      forall cs cs' v m
+             (STK: Forall2 match_stackframe cs cs'),
+        match_states None (Returnstate cs v m) (Returnstate cs' v m).
+
+  Definition match_prog (p: program) (tp: program) :=
+    Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
   Context (TRANSL : match_prog prog tprog).
 
-    Lemma symbols_preserved:
+  Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
   Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.