Require Import Coqlib AST Maps.
Require Import Op Registers.
Require Import RTL BTL.
Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.

Require Import Impure.ImpHCons.
Import Notations.
Import HConsing.

Local Open Scope option_monad_scope.
Local Open Scope impure.

Import ListNotations.
Local Open Scope list_scope.

(** Tactics *)

Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps.

(** Notations to make lemmas more readable *)
Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
  (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.

Local Open Scope hse.

Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
  (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse.

Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
  (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse.

(** Debug printer *)
Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)

Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).

(** * Implementation of Data-structure use in Hash-consing *)

Definition sval_get_hid (sv: sval): hashcode :=
  match sv with
  | Sundef hid => hid
  | Sinput _ hid => hid
  | Sop _ _ hid => hid
  | Sload _ _ _ _ _ hid => hid
  end.

Definition list_sval_get_hid (lsv: list_sval): hashcode :=
  match lsv with
  | Snil hid => hid
  | Scons _ _ hid => hid
  end.

Definition smem_get_hid (sm: smem): hashcode :=
  match sm with
  | Sinit hid => hid
  | Sstore _ _ _ _ _ hid => hid
  end.

Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
  match sv with
  | Sundef _ => Sundef hid
  | Sinput r _ => Sinput r hid
  | Sop o lsv _ => Sop o lsv hid
  | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid
  end.

Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval :=
  match lsv with
  | Snil _ => Snil hid
  | Scons sv lsv _ => Scons sv lsv hid
  end.

Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
  match sm with
  | Sinit _ => Sinit hid
  | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
  end.

(** * Implementation of symbolic execution *)
Section CanonBuilding.

Variable hC_sval: hashinfo sval -> ?? sval.

Hypothesis hC_sval_correct: forall s,
  WHEN hC_sval s ~> s' THEN forall ctx,
    sval_refines ctx (hdata s) s'.

Variable hC_list_sval: hashinfo list_sval -> ?? list_sval.
Hypothesis hC_list_sval_correct: forall lh,
  WHEN hC_list_sval lh ~> lh' THEN forall ctx,
    list_sval_refines ctx (hdata lh) lh'.

Variable hC_smem: hashinfo smem -> ?? smem.
Hypothesis hC_smem_correct: forall hm,
  WHEN hC_smem hm ~> hm' THEN forall ctx,
    smem_refines ctx (hdata hm) hm'.

(* First, we wrap constructors for hashed values !*)

Definition reg_hcode := 1.
Definition op_hcode := 2.
Definition load_hcode := 3.
Definition undef_code := 4.

Definition hSinput_hcodes (r: reg) :=
   DO hc <~ hash reg_hcode;;
   DO hv <~ hash r;;
   RET [hc;hv].
Extraction Inline hSinput_hcodes.

Definition hSinput (r:reg): ?? sval :=
   DO hv <~ hSinput_hcodes r;;
   hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}.

Lemma hSinput_correct r:
  WHEN hSinput r ~> hv THEN forall ctx,
    sval_refines ctx hv (Sinput r unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSinput.
Local Hint Resolve hSinput_correct: wlp.

Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
   DO hc <~ hash op_hcode;;
   DO hv <~ hash op;;
   RET [hc;hv;list_sval_get_hid lsv].
Extraction Inline hSop_hcodes.

Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
   DO hv <~ hSop_hcodes op lsv;;
   hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=hv |}.

Lemma hSop_fSop_correct op lsv:
  WHEN hSop op lsv ~> hv THEN forall ctx,
    sval_refines ctx hv (fSop op lsv).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSop.
Local Hint Resolve hSop_fSop_correct: wlp_raw.

Lemma hSop_correct op lsv1:
  WHEN hSop op lsv1 ~> hv THEN forall ctx lsv2
   (LR: list_sval_refines ctx lsv1 lsv2),
   sval_refines ctx hv (Sop op lsv2 unknown_hid).
Proof.
  wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
  rewrite <- LR. erewrite H; eauto.
Qed.
Local Hint Resolve hSop_correct: wlp.

Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):=
   DO hc <~ hash load_hcode;;
   DO hv1 <~ hash trap;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc; smem_get_hid sm; hv1; hv2; hv3; list_sval_get_hid lsv].
Extraction Inline hSload_hcodes.

Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval :=
   DO hv <~ hSload_hcodes sm trap chunk addr lsv;;
   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.

Lemma hSload_correct sm1 trap chunk addr lsv1:
  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2
    (LR: list_sval_refines ctx lsv1 lsv2)
    (MR: smem_refines ctx sm1 sm2),
    sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR.
  auto.
Qed.
Global Opaque hSload.
Local Hint Resolve hSload_correct: wlp.

Definition hSundef_hcodes :=
   DO hc <~ hash undef_code;;
   RET [hc].
Extraction Inline hSundef_hcodes.

Definition hSundef : ?? sval :=
   DO hv <~ hSundef_hcodes;;
   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}.

Lemma hSundef_correct:
  WHEN hSundef ~> hv THEN forall ctx,
    sval_refines ctx hv (Sundef unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSundef.
Local Hint Resolve hSundef_correct: wlp.

Definition hSnil (_: unit): ?? list_sval :=
   hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}.

Lemma hSnil_correct:
  WHEN hSnil() ~> hv THEN forall ctx,
    list_sval_refines ctx hv (Snil unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSnil.
Local Hint Resolve hSnil_correct: wlp.

Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval :=
   hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}.

Lemma hScons_correct sv1 lsv1:
  WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2
    (VR: sval_refines ctx sv1 sv2)
    (LR: list_sval_refines ctx lsv1 lsv2),
    list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- VR, <- LR.
  auto.
Qed.
Global Opaque hScons.
Local Hint Resolve hScons_correct: wlp.

Definition hSinit (_: unit): ?? smem :=
   hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}.

Lemma hSinit_correct:
  WHEN hSinit() ~> hm THEN forall ctx,
    smem_refines ctx hm (Sinit unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSinit.
Local Hint Resolve hSinit_correct: wlp.

Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):=
   DO hv1 <~ hash chunk;;
   DO hv2 <~ hash addr;;
   RET [smem_get_hid sm; hv1; hv2; list_sval_get_hid lsv; sval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem :=
   DO hv <~ hSstore_hcodes sm chunk addr lsv srce;;
   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}.

Lemma hSstore_correct sm1 chunk addr lsv1 sv1:
  WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
    (LR: list_sval_refines ctx lsv1 lsv2)
    (MR: smem_refines ctx sm1 sm2)
    (VR: sval_refines ctx sv1 sv2),
    smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR, <- VR.
  auto.
Qed.
Global Opaque hSstore.
Local Hint Resolve hSstore_correct: wlp.

Definition hrs_sreg_eval ctx hrs r := eval_sval ctx (ris_sreg_get hrs r).

Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
   match PTree.get r hrs with
   | None => if ris_input_init hrs then hSinput r else hSundef
   | Some sv => RET sv
   end.
Coercion hrs_sreg_get: ristate >-> Funclass.

Lemma hrs_sreg_get_correct hrs r:
  WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval)
  (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
  sval_refines ctx sv (f r).
Proof.
  unfold hrs_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
  rewrite H0, H1; simpl; auto.
Qed.
Global Opaque hrs_sreg_get.
Local Hint Resolve hrs_sreg_get_correct: wlp.

Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval :=
  match l with
  | nil => hSnil()
  | r::l =>
    DO v <~ hrs_sreg_get hrs r;;
    DO lsv <~ hlist_args hrs l;;
    hScons v lsv
  end.

Lemma hlist_args_correct hrs l:
  WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval)
    (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
    list_sval_refines ctx lsv (list_sval_inj (List.map f l)).
Proof.
  induction l; wlp_simplify.
Qed.
Global Opaque hlist_args.
Local Hint Resolve hlist_args_correct: wlp.

(** Convert a "fake" hash-consed term into a "real" hash-consed term *)

Fixpoint fsval_proj sv: ?? sval :=
  match sv with
  | Sundef hc =>
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSundef else RET sv
  | Sinput r hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSinput r (* was not yet really hash-consed *)
      else RET sv (* already hash-consed *)
  | Sop op hl hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then (* was not yet really hash-consed *) 
        DO hl' <~ fsval_list_proj hl;;
        hSop op hl'
      else RET sv (* already hash-consed *)
  | Sload hm t chk addr hl _ => RET sv (* FIXME TODO gourdinl ? *)
  end
with fsval_list_proj sl: ?? list_sval :=
  match sl with
  | Snil hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSnil() (* was not yet really hash-consed *)
      else RET sl (* already hash-consed *)
  | Scons hv hl hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then (* was not yet really hash-consed *)
        DO hv' <~ fsval_proj hv;;
        DO hl' <~ fsval_list_proj hl;;
        hScons hv' hl' 
      else RET sl (* already hash-consed *)
  end.

Lemma fsval_proj_correct sv:
  WHEN fsval_proj sv ~> sv' THEN forall ctx,
  eval_sval ctx sv = eval_sval ctx sv'.
Proof.
 induction sv using sval_mut 
 with (P0 := fun lsv => 
       WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
         eval_list_sval ctx lsv = eval_list_sval ctx lsv')
       (P1 := fun sm => True); try (wlp_simplify; tauto).
 - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp).
   rewrite H, H0; auto.
 - wlp_simplify; erewrite H0, H1; eauto.
Qed.
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.

Lemma fsval_list_proj_correct lsv:
  WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
  eval_list_sval ctx lsv = eval_list_sval ctx lsv'.
Proof.
  induction lsv; wlp_simplify.
  erewrite H0, H1; eauto.
Qed.
Global Opaque fsval_list_proj.
Local Hint Resolve fsval_list_proj_correct: wlp.

(** ** Assignment of memory *)

Definition hrexec_store chunk addr args src hrs: ?? ristate :=
  DO hargs <~ hlist_args hrs args;;
  DO hsrc <~ hrs_sreg_get hrs src;;
  DO hm <~ hSstore hrs chunk addr hargs hsrc;;
  RET (rset_smem hm hrs).

Lemma hrexec_store_correct chunk addr args src hrs:
  WHEN hrexec_store chunk addr args src hrs ~> hrs' THEN forall ctx sis
  (REF: ris_refines ctx hrs sis),
  ris_refines ctx hrs' (sexec_store chunk addr args src sis).
Proof.
  wlp_simplify.
  eapply rset_mem_correct; simpl; eauto.
  - intros X; erewrite H1; eauto.
    rewrite X. simplify_SOME z.
  - intros X; inversion REF.
    erewrite H1; eauto.
Qed.

(** ** Assignment of registers *)

(** locally new symbolic values during symbolic execution *)
Inductive root_sval: Type :=
| Rop (op: operation)
| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
.

Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate): sval :=
  let lsv := list_sval_inj (List.map (si_sreg st) lr) in
  let sm := si_smem st in
  match rsv with
  | Rop op => fSop op lsv
  | Rload trap chunk addr => fSload sm trap chunk addr lsv
  end.
Coercion root_apply: root_sval >-> Funclass.

Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
  DO lsv <~ hlist_args hrs lr;;
  match rsv with
  | Rop op => hSop op lsv
  | Rload trap chunk addr => hSload hrs trap chunk addr lsv
  end.

Lemma root_happly_correct (rsv: root_sval) lr hrs:
  WHEN root_happly rsv lr hrs ~> sv THEN forall ctx st
  (REF: ris_refines ctx hrs st)
  (OK: ris_ok ctx hrs),
  sval_refines ctx sv (rsv lr st).
Proof.
  unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF;
  erewrite H0, H; eauto.
Qed.
Global Opaque root_happly.
Hint Resolve root_happly_correct: wlp.

Local Open Scope lazy_bool_scope.

(* NB: return [false] if the rsv cannot fail *)
Definition may_trap (rsv: root_sval) (lr: list reg): bool :=
  match rsv with 
  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
  | Rload TRAP _ _  => true
  | _ => false
  end.

Lemma lazy_orb_negb_false (b1 b2:bool):
  (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true).
Proof.
  unfold negb. repeat autodestruct; simpl; intuition (try congruence).
Qed.

Lemma eval_list_sval_length ctx (f: reg -> sval) (l:list reg):
  forall l', eval_list_sval ctx (list_sval_inj (List.map f l)) = Some l' ->
  Datatypes.length l = Datatypes.length l'.
Proof.
  induction l.
  - simpl. intros. inv H. reflexivity.
  - simpl. intros. destruct (eval_sval _ _); [|discriminate].
    destruct (eval_list_sval _ _) eqn:SLS; [|discriminate]. inv H. simpl.
    erewrite IHl; eauto.
Qed.

Lemma may_trap_correct ctx (rsv: root_sval) (lr: list reg) st:
  may_trap rsv lr = false -> 
  eval_list_sval ctx (list_sval_inj (List.map (si_sreg st) lr)) <> None ->
  eval_smem ctx (si_smem st) <> None ->
  eval_sval ctx (rsv lr st) <> None.
Proof.
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & LEN) OK1 OK2.
    autodestruct; try congruence. intros.
    eapply is_trapping_op_sound; eauto.
    erewrite <- eval_list_sval_length; eauto.
    apply Nat.eqb_eq in LEN.
    assumption.
  - intros X OK1 OK2.
    repeat autodestruct; try congruence.
Qed.

(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
  match rsv with
  | Rop op =>
     match is_move_operation op lr with
     | Some arg => hrs_sreg_get hrs arg (* optimization of Omove *)
     | None =>
         DO lsv <~ hlist_args hrs lr;;
         hSop op lsv
        (* TODO gourdinl
       match target_op_simplify op lr hst with
       | Some fhv => fsval_proj fhv
       | None =>
         hSop op lhsv
           end*)
     end
  | Rload _ chunk addr => 
       DO lhsv <~ hlist_args hrs lr;;
       hSload hrs NOTRAP chunk addr lhsv
  end.

Lemma simplify_correct rsv lr hrs:
  WHEN simplify rsv lr hrs ~> hv THEN forall ctx st
    (REF: ris_refines ctx hrs st)
    (OK0: ris_ok ctx hrs)
    (OK1: eval_sval ctx (rsv lr st) <> None),
    sval_refines ctx hv (rsv lr st).
Proof.
  destruct rsv; simpl; auto.
  - (* Rop *)
    destruct (is_move_operation _ _) eqn: Hmove.
    { wlp_simplify; exploit is_move_operation_correct; eauto.
      intros (Hop & Hlsv); subst; simpl in *. inv REF.
      simplify_SOME z; erewrite H; eauto. }
    wlp_simplify; inv REF. erewrite H0; eauto.
  - (* Rload *)
    destruct trap; wlp_simplify; inv REF.
    + erewrite H0, H, MEM_EQ; eauto.
      repeat simplify_SOME z.
      * destruct (Memory.Mem.loadv _ _ _); try congruence.
      * rewrite H1 in OK1; congruence.
    + erewrite H0; eauto.
Qed.

Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
  match o with
  | Some x => RET x
  | None => FAILWITH msg
  end.

Definition hris_init: ?? ristate
  := DO hm <~ hSinit ();;
     RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.

Lemma ris_init_correct:
  WHEN hris_init ~> hris THEN
  forall ctx, ris_refines ctx hris sis_init.
Proof.
  unfold hris_init, sis_init; wlp_simplify.
  econstructor; simpl in *; eauto.
  + split; destruct 1; econstructor; simpl in *;
    try rewrite H; try congruence; trivial.
  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
    intros; rewrite PTree.gempty; eauto.
Qed.

(*
Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort).

Definition hsexec (f: function) (pc:node): ?? ristate :=
  DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";;
  DO hinit <~ init_ristate;;
  DO hst <~ hsiexec_path path.(psize) f hinit;;
  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
  DO ohst <~ hsiexec_inst i hst;;
  match ohst with
  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
            RET {| hinternal := hst; hfinal := hsvf |}
   end.*)

End CanonBuilding.