Module BTL_SEimpl_SE

Require Import Coqlib AST.
Require Import Op Registers.
Require Import BTL.
Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
Require Import BTL_SEsimplify BTL_SEsimplifyproof BTL_SEsimplifyMem BTL_SEimpl_prelude.

Import Notations.
Import HConsing.
Import SvalNotations.

Import ListNotations.
Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Local Open Scope impure.

Section SymbolicExecution.

  Context `{HCF : HashConsingFcts}.
  Context `{HC : HashConsingHyps HCF}.
  Context `{RRULES: rrules_set}.

Additional okclauses

Definition adp_op_okset (op : operation) (sargs : list_sval) (iinfo : inst_info)
  : ?? OKset.t :=
  match is_promotable_op iinfo.(inst_promotion) with
  | Some prom =>
      DO ok <~ hOKpromotableOp op prom sargs;;
      RET (OKset.singleton (`ok))
  | _ =>
      RET OKset.empty
  end.

Lemma adp_op_okset_correct ctx op sargs iinfo
  (ALIVE : alive (eval_list_sval ctx sargs)):
  WHEN adp_op_okset op sargs iinfo ~> ok THEN
  OKset.eval ctx ok <-> proj1_sig (adp_op_okpred op sargs iinfo) ctx.

Global Opaque adp_op_okset.


Definition adp_cond_okset (cond : condition) (sargs : list_sval) (iinfo : inst_info)
  : ?? OKset.t :=
  match is_promotable_cond iinfo.(inst_promotion) with
  | Some prom =>
      DO ok <~ hOKpromotableCond cond prom sargs;;
      RET (OKset.singleton (`ok))
  | _ =>
      RET OKset.empty
  end.

Lemma adp_cond_okset_correct ctx cond sargs iinfo
  (ALIVE : alive (eval_list_sval ctx sargs)):
  WHEN adp_cond_okset cond sargs iinfo ~> ok THEN
  OKset.eval ctx ok <-> proj1_sig (adp_cond_okpred cond sargs iinfo) ctx.

Global Opaque adp_cond_okset.

Normalization and rewritings

Definition cbranch_expanse (cond: condition) (args: list_sval) (iinfo: inst_info)
  : ?? (condition * list_sval * OKset.t) :=
  match rewrite_cbranches RRULES cond (list_of_lsv args) iinfo with
  | Some ((cond', vargs), pre) =>
      DO vargs' <~ @fsval_list_proj HCF HC vargs;;
      DO pre' <~ imp_map (@fokclause_proj HCF HC) pre;;
      RET (cond', vargs', OKset.of_list pre')
  | None =>
      RET (cond, args, OKset.empty)
  end.

Lemma cbranch_expanse_spec ctx c l iinfo:
  WHEN cbranch_expanse c l iinfo ~> r THEN
  let '(c', l', pre) := r in
  forall (PRE : OKset.eval ctx pre)
         (ALIVE : alive (eval_list_sval ctx l)),
  eval_scondition ctx c' l' = eval_scondition ctx c l.
Global Opaque cbranch_expanse.

Assignment of memory

Definition hrexec_store m chk addr args src iinfo hrs: ?? ristate :=
  DO hargs <~ @hrs_lr_get HCF hrs args;;
  DO hsrc <~ @hrs_sreg_get HCF hrs src;;
  @hrs_set_store HCF HC RRULES m (ris_smem hrs) chk addr hargs hsrc (BTL.store_info_of_iinfo iinfo) hrs.

Lemma hrexec_store_spec ctx sis m chunk addr args src iinfo hrs
  (RR: ris_refines_ok ctx hrs sis):
  WHEN hrexec_store m chunk addr args src iinfo hrs ~> hrs' THEN
  exists sis',
    sexec_store chunk addr args src iinfo sis = Some sis' /\
    ris_refines m ctx hrs' sis'.

Lemma hrexec_store_rel m chunk addr args aaddr src hrs:
  WHEN hrexec_store m chunk addr args aaddr src hrs ~> rst THEN
  ris_rel m hrs rst.
Global Opaque hrexec_store.

Evaluation of builtins

Fixpoint hbuiltin_arg (hrs: ristate) (arg : builtin_arg reg): ?? builtin_arg sval :=
  match arg with
  | BA r =>
         DO v <~ @hrs_sreg_get HCF hrs r;;
         RET (BA v)
  | BA_int n => RET (BA_int n)
  | BA_long n => RET (BA_long n)
  | BA_float f0 => RET (BA_float f0)
  | BA_single s => RET (BA_single s)
  | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr)
  | BA_addrstack ptr => RET (BA_addrstack ptr)
  | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr)
  | BA_addrglobal id ptr => RET (BA_addrglobal id ptr)
  | BA_splitlong ba1 ba2 =>
    DO v1 <~ hbuiltin_arg hrs ba1;;
    DO v2 <~ hbuiltin_arg hrs ba2;;
    RET (BA_splitlong v1 v2)
  | BA_addptr ba1 ba2 =>
    DO v1 <~ hbuiltin_arg hrs ba1;;
    DO v2 <~ hbuiltin_arg hrs ba2;;
    RET (BA_addptr v1 v2)
  end.

Lemma hbuiltin_arg_spec hrs arg:
  WHEN hbuiltin_arg hrs arg ~> hargs THEN
  forall ctx sis
  (RR: ris_refines_ok ctx hrs sis),
  exists sarg,
    map_builtin_arg_opt sis arg = Some sarg /\
    eval_builtin_sval ctx hargs = eval_builtin_sval ctx sarg.
Global Opaque hbuiltin_arg.


Definition hbuiltin_args hrs : list (builtin_arg reg) -> ?? list (builtin_arg sval) :=
  imp_map (hbuiltin_arg hrs).

Lemma hbuiltin_args_spec hrs args:
  WHEN hbuiltin_args hrs args ~> hargs THEN
  forall ctx sis
  (RR: ris_refines_ok ctx hrs sis),
  exists sargs,
    map_opt (map_builtin_arg_opt sis) args = Some sargs /\
    bargs_simu ctx hargs sargs.
Global Opaque hbuiltin_args.

Evaluation of final instructions

Definition hsum_left_optmap {A B C} (f: A -> ?? B) (x: A + C): ?? (B + C) :=
  match x with
  | inl r => DO hr <~ f r;; RET (inl hr)
  | inr s => RET (inr s)
  end.

Lemma hsum_left_optmap_spec hrs (ros: reg + qualident):
  WHEN hsum_left_optmap (@hrs_sreg_get HCF hrs) ros ~> hsi THEN forall ctx (sis: sistate)
  (RR: ris_refines_ok ctx hrs sis),
  exists svi,
    map_sum_left_opt sis ros = Some svi /\
    svident_simu ctx hsi svi.
Global Opaque hsum_left_optmap.


Definition hrexec_final_sfv (i: final) hrs: ?? rfval :=
  match i with
  | Bgoto pc => RET (Sgoto pc)
  | Bcall sig ros args res pc =>
      DO svos <~ hsum_left_optmap (@hrs_sreg_get HCF hrs) ros;;
      DO sargs <~ @hrs_lr_get HCF hrs args;;
      RET (Scall sig svos sargs res pc)
  | Btailcall sig ros args =>
      DO svos <~ hsum_left_optmap (@hrs_sreg_get HCF hrs) ros;;
      DO sargs <~ @hrs_lr_get HCF hrs args;;
      RET (Stailcall sig svos sargs)
  | Bbuiltin ef args res pc =>
      DO sargs <~ hbuiltin_args hrs args;;
      RET (Sbuiltin ef sargs res pc)
  | Breturn or =>
      match or with
      | Some r => DO hr <~ @hrs_sreg_get HCF hrs r;; RET (Sreturn (Some hr))
      | None => RET (Sreturn None)
      end
  | Bjumptable reg tbl =>
      DO sv <~ @hrs_sreg_get HCF hrs reg;;
      RET (Sjumptable sv tbl)
  end.

Lemma hrexec_final_sfv_spec ctx sis fi hrs
  (RR: ris_refines_ok ctx hrs sis):
  WHEN hrexec_final_sfv fi hrs ~> rfv THEN
  exists sfv,
    sexec_final_sfv fi sis = Some sfv /\
    rfv_refines ctx rfv sfv.
Global Opaque hrexec_final_sfv.

Symbolic execution of the whole block

Fixpoint hrexec_rec (m : se_mode) ib hrs (k: ristate -> ?? rstate): ?? rstate :=
  match ib with
  | BF fin iinfo =>
      DO sfv <~ hrexec_final_sfv fin hrs;;
      RET (Sfinal hrs sfv iinfo.(meminv_annot))
  | Bnop _ => k hrs
  | Bop op args dst iinfo =>
      DO lsv <~ @hrs_lr_get HCF hrs args;;
      DO ok <~ adp_op_okset op lsv iinfo;;
      DO hrs1 <~ hrs_add_okset m false hrs ok;;
      DO next <~ @hrs_rsv_set HCF HC RRULES m dst (Rop op) lsv (Some iinfo) hrs1.(ris_smem) hrs1;;
      k next
  | Bload trap chunk addr args dst iinfo =>
      DO lsv <~ @hrs_lr_get HCF hrs args;;
      DO next <~ @hrs_rsv_set HCF HC RRULES m dst
                    (Rload trap chunk addr iinfo.(addr_aval)) lsv (Some iinfo) hrs.(ris_smem) hrs;;
      k next
  | Bstore chunk addr args src iinfo =>
      DO next <~ hrexec_store m chunk addr args src iinfo hrs;;
      k next
  | Bseq ib1 ib2 =>
      hrexec_rec m ib1 hrs (fun hrs2 => hrexec_rec m ib2 hrs2 k)
  | Bcond cond args ifso ifnot iinfo =>
      DO lsv <~ @hrs_lr_get HCF hrs args;;
      DO ok <~ adp_cond_okset cond lsv iinfo;;
      DO hrs1 <~ hrs_add_okset m false hrs ok;;
      DO res <~ cbranch_expanse cond lsv iinfo;;
      let '(cond, vargs, pre) := res in
      DO hrs2 <~ hrs_add_okset m true hrs1 pre;;
      DO ifso <~ hrexec_rec m ifso hrs2 k;;
      DO ifnot <~ hrexec_rec m ifnot hrs2 k;;
      RET (Scond cond vargs ifso ifnot)
  end.

Definition hrexec m ib hrinit :=
  hrexec_rec m ib hrinit (fun _ => RET error_rstate).


Lemma hrexec_rec_okpreserv m ctx hrsf rfv ib
  (ROK: ris_ok ctx hrsf):
  forall k
  (CONT: forall hrs,
    WHEN k hrs ~> rst THEN
    get_routcome ctx rst = sout hrsf rfv ->
    ris_ok ctx hrs)
  hrs,
  WHEN hrexec_rec m ib hrs k ~> rst THEN forall
  (ROUT: get_routcome ctx rst = sout hrsf rfv),
  ris_ok ctx hrs.

Lemma hrexec_rec_spec m ctx ib hrs sis:
  forall rk k
  (STRICT_R: forall hrs hrsf rfv,
    ris_ok ctx hrsf ->
    WHEN rk hrs ~> rst THEN
    get_routcome ctx rst = sout hrsf rfv ->
    ris_ok ctx hrs)
  (STRICT_S: forall sis sisf sfv,
    get_soutcome ctx (k sis) = sout sisf sfv ->
    sis_rel sis sisf)
  (CONT: forall hrs sis,
    ris_refines m ctx hrs sis ->
    WHEN rk hrs ~> rst THEN
    rst_refines m ctx rst (k sis))
  (RR: ris_refines m ctx hrs sis),
  WHEN hrexec_rec m ib hrs rk ~> rst THEN
  rst_refines m ctx rst (sexec_rec ib sis k).
Global Opaque hrexec_rec.

Theorem hrexec_spec m ctx ib hrs sis
  (RR: ris_refines m ctx hrs sis):
  WHEN hrexec m ib hrs ~> rst THEN
  rst_refines m ctx rst (sexec ib sis).
Global Opaque hrexec.

End SymbolicExecution.