Module BTL_BlockSimulation

Require Import Coqlib Maps.
Require Import AST Errors Linking Smallstep.
Require Import RTL Registers OptionMonad BTL.

Require Import BTL_SEtheory BTL_SEsimuref BTL_SEimpl_check.
Require BTL_ResetAnnots BTL_AnalysisLib.

Require ValueDomain ValueAnalysis.

Module Type BTL_BlockSimulationConfig.

  Parameter btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Parameter btl_rrules: unit -> rrules_set.

End BTL_BlockSimulationConfig.

Module BTL_BlockSimulation (B: BTL_BlockSimulationConfig).

Export B.

Record match_function (f f': BTL.function) : Prop := {
  preserv_fnsig: fn_sig f = fn_sig f';
  preserv_fnparams: fn_params f = fn_params f';
  preserv_fnstacksize: fn_stacksize f = fn_stacksize f';
  preserv_entrypoint: fn_entrypoint f = fn_entrypoint f';
  trivial_histinv_entrypoint: only_liveness (history (f'.(fn_gm) (fn_entrypoint f)));
  trivial_glueinv_entrypoint: only_liveness (glue (f'.(fn_gm) (fn_entrypoint f)));
  trivial_meminv_entrypoint : meminv (f'.(fn_gm) (fn_entrypoint f)) = nil;
  match_sexec_ok: forall pc ib, (fn_code f)!pc = Some ib ->
                  exists ib', (fn_code f')!pc = Some ib' /\
                  match_sexec_si_all_ctx f'.(fn_gm) (entry ib) (entry ib') pc;
}.

Inductive match_fundef: fundef -> fundef -> Prop :=
  | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
  | match_External ef: match_fundef (External ef) (External ef).

Local Open Scope option_monad_scope.

Inductive match_stackframes (ge: genv): stackframe -> stackframe -> Prop :=
  | match_stackframe_intro
      sp res f pc rs rs' f'
      (TRANSF: match_function f f')
      (MATCHI: forall v m bc,
      match_invs (Bcctx ge sp (rs#res <- v) (rs'#res <- v) m bc) (f'.(fn_gm) pc) m)
      : match_stackframes ge (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').

Inductive match_states (ge: genv): state -> state -> Prop :=
  | match_states_intro
      stk f pc sp rs rs' m m' bc stk' f'
      (TRANSF: match_function f f')
      (MATCHI: match_invs (Bcctx ge sp rs rs' m' bc) (f'.(fn_gm) pc) m)
      (STACKS: list_forall2 (match_stackframes ge) stk stk')
      : match_states ge (State stk f sp pc rs m bc) (State stk' f' sp pc rs' m' bc)
  | match_states_call
      stk stk' f f' args m bc
      (STACKS: list_forall2 (match_stackframes ge) stk stk')
      (TRANSF: match_fundef f f')
      : match_states ge (Callstate stk f args m bc) (Callstate stk' f' args m bc)
  | match_states_return
      stk stk' v m bc
      (STACKS: list_forall2 (match_stackframes ge) stk stk')
      : match_states ge (Returnstate stk v m bc) (Returnstate stk' v m bc)
   .

Local Open Scope error_monad_scope.
Local Open Scope lazy_bool_scope.

Definition check_only_liveness f: res unit :=
  let gm_entry := fn_gm f (fn_entrypoint f) in
  if test_only_liveness (history gm_entry) &&
     test_only_liveness (glue gm_entry) &&
     is_nil (meminv gm_entry)
  then OK tt
  else Error (msg "check_only_liveness: some non-liveness-only invariant at entrypoint").

Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=
  match lpc with
  | nil => OK tt
  | pc :: lpc' =>
      match (fn_code f1)!pc, (fn_code f2)!pc with
      | Some ibf1, Some ibf2 =>
          do dummy <- simu_check (btl_rrules tt) f1 f2 ibf1 ibf2 (fn_gm f2) pc;
          check_symbolic_simu_rec f1 f2 lpc'
      | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch")
      end
  end.

Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
  check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).

Definition transf_function (f: BTL.function) :=
  let (tcfi, gm) := btl_optim_oracle f in
  let (tc, fi) := tcfi in
  let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc (fn_entrypoint f) (fn_attr f) gm fi in
  do dummy1 <- check_only_liveness tf;
  do dummy2 <- check_symbolic_simu f tf;
  OK tf.

Local Hint Resolve test_only_liveness_correct: core.

Lemma transf_function_only_liveness f tf:
  transf_function f = OK tf ->
  only_liveness (history (tf.(fn_gm) (fn_entrypoint f))) /\
  only_liveness (glue (tf.(fn_gm) (fn_entrypoint f))) /\
  meminv (tf.(fn_gm) (fn_entrypoint f)) = nil.

Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
  check_symbolic_simu_rec f1 f2 lpc = OK x ->
  forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc ->
    exists ib2, (fn_code f2)!pc = Some ib2 /\
    match_sexec_si_all_ctx (fn_gm f2) (entry ib1) (entry ib2) pc.

Lemma check_symbolic_simu_correct x f1 f2:
  check_symbolic_simu f1 f2 = OK x ->
  forall pc ib1, (fn_code f1)!pc = Some ib1 ->
    exists ib2, (fn_code f2)!pc = Some ib2 /\
    match_sexec_si_all_ctx (fn_gm f2) (entry ib1) (entry ib2) pc.

Definition transf_fundef (f: fundef) : res fundef :=
  transf_partial_fundef (fun f => transf_function f) f.

Definition transf_program (p: program) : res program :=
  transform_partial_program transf_fundef p.

End BTL_BlockSimulation.