From daf1e49862cfd0fff4fea9736815e14f335ff2c8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 9 Jun 2022 09:33:15 +0100 Subject: Work on the if-conversion proof --- src/hls/IfConversion.v | 30 ++++++++++++++------------ src/hls/IfConversionproof.v | 51 ++++++++++++++++++++++++++++----------------- 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. -- cgit