diff options
Diffstat (limited to 'src/hls/IfConversionproof.v')
-rw-r--r-- | src/hls/IfConversionproof.v | 51 |
1 files changed, 32 insertions, 19 deletions
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. |