Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import AsmX.
Require Import Conventions.
Require Import Machregs.
Require Import liblayers.lib.Decision.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.PTreeSemantics.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import CompCertBuiltins.
Require Import LAsm.
Require Import MemoryExtra.

Section ModuleSemantics.

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.

  Definition ef_errmsg (ef: external_function) :=
    match ef with
      | EF_external i sg ⇒ MSG "EF_external " :: CTX i :: nil
      | EF_builtin i sg ⇒ MSG "EF_builtin " :: CTX i :: nil
      | EF_vload chunk ⇒ MSG "EF_vload" :: nil
      | EF_vstore chunk ⇒ MSG "EF_vstore" :: nil
      | EF_vload_global chunk i _ ⇒ MSG "EF_vload_global " :: CTX i :: nil
      | EF_vstore_global chunk i _ ⇒ MSG "EF_vstore_global " :: CTX i :: nil
      | EF_malloc ⇒ MSG "EF_malloc" :: nil
      | EF_free ⇒ MSG "EF_free" :: nil
      | EF_memcpy _ _ ⇒ MSG "EF_memcpy" :: nil
      | EF_annot i _ ⇒ MSG "EF_annot " :: CTX i :: nil
      | EF_annot_val i _ ⇒ MSG "EF_annot_val " :: CTX i :: nil
      | EF_inline_asm i ⇒ MSG "EF_inline_asm " :: CTX i :: nil
    end.

  Definition ef_OK (ef : external_function) : res unit :=
    match ef with
      | EF_annot _ _ ⇒ Error (ef_errmsg ef)
      | EF_annot_val _ _ ⇒ Error (ef_errmsg ef)
      | _ ⇒ OK tt
    end.

  Definition instr_OK (i : instruction) : res unit :=
    match i with
      | asm_instruction i ⇒
        match i with
          | Pbuiltin ef _ _ ⇒
            match ef_OK ef with
              | Error e ⇒ Error (MSG "Pbuiltin " :: e)
              | _ ⇒ OK tt
            end
          | Pannot ef _ ⇒
            match ef_OK ef with
              | Error e ⇒ Error (MSG "Pannot " :: e)
              | _ ⇒ OK tt
            end
          | _ ⇒ OK tt
        end
      | _ ⇒ OK tt
    end.

  Fixpoint instrs_OK (c : code) : res unit :=
    match c with
      | i::c ⇒
        match instr_OK i with
          | OK _ ⇒ instrs_OK c
          | Error msg ⇒ Error (MSG "Forbidden instruction: " :: msg)
        end
      | nil ⇒ OK tt
    end.

  Global Instance lasm_program_format_ops:
    ProgramFormatOps function Ctypes.type fundef unit :=
    {
      make_internal κ :=
        match instrs_OK (fn_code κ) with
          | OK _ ⇒ OK (AST.Internal κ)
          | Error msg ⇒ Error msg
        end;
      make_external D i σ := OK (AST.External (EF_external i (compatsem_sig σ)));
      make_varinfo τ := tt
    }.

  Lemma instrs_OK_in :
    ∀ c i,
      In i c → instrs_OK c = OK tt → instr_OK i = OK tt.
  Proof.
    induction c; simpl; intros; [intuition|].
    destruct H; subst.
    destruct (instr_OK i) as [[] | ]; auto; discriminate.
    apply IHc; auto.
    destruct (instrs_OK c) as [[] | ]; auto; destruct (instr_OK a); discriminate.
  Qed.

  Lemma find_instr_in :
    ∀ c ofs i,
      find_instr ofs c = Some i → In i c.
  Proof.
    induction c; simpl; intros; [discriminate|].
    destruct (zeq ofs 0).
    inv H; auto.
    right; eapply IHc; eauto.
  Qed.

  Global Instance lasm_program_format_prf:
    ProgramFormat function Ctypes.type fundef unit.
  Proof.
    split.
    × intros D i1 i2 Hi σ1 σ2 Hσ; subst.
      simpl.
      f_equal.
      f_equal.
      inversion Hσ; subst.
      + destruct H as [[Hstep Hsig Hvalid] Hinvs].
        destruct x; simpl in *; subst.
        destruct y; simpl in *; subst.
        unfold sextcall_sig.
        rewrite Hsig.
        reflexivity.
      + destruct H as [[Hstep Hsig Hvalid] Hinvs].
        destruct x; destruct y; simpl in *; subst; simpl in ×.
        rewrite Hsig.
        reflexivity.
  Qed.

  Global Instance lasm_make_external_sim_monotonic:
    Proper
      (∀ R, - ==> sim R ++> res_le eq)
      (fun D ⇒ make_external (D := D)).
  Proof.
    intros D1 D2 R i p1 p2 Hsim.
    destruct R; try solve_monotonic.
    inversion Hsim; subst.
    × destruct H as [Hstep Hcsig Hvalid Hinvs]; simpl.
      unfold sextcall_sig.
      rewrite Hcsig.
      reflexivity.
    × destruct H as [Hstep Hsig Hvalid Hinvs]; simpl.
      rewrite Hsig.
      reflexivity.
    × destruct H as [Hstep Hsig Hvalid Hinvs]; simpl.
      rewrite Hsig.
      reflexivity.
  Qed.

  Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
  Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

  Lemma make_program_globalenv :
    ∀ {D} s M L p,
      make_program (D:=D) s M L = OK p →
      make_globalenv (D:=D) s M L = OK (Genv.globalenv p).
  Proof.
    unfold make_globalenv; intros.
    simpl in *; rewrite H; auto.
  Qed.

  Lemma make_globalenv_program :
    ∀ {D} (ge:genv) s M L,
      make_globalenv (D:=D) s M L = OK ge →
      ∃ p, make_program (D:=D) s M L = OK p.
  Proof.
    unfold make_globalenv; intros.
    inv_monad H; eauto.
  Qed.

  Lemma make_globalenv_instrs_OK :
    ∀ {D} (ge:genv) b f s M L,
      make_globalenv (D:=D) s M L = ret ge →
      Genv.find_funct_ptr ge b = Some (Internal f) →
      instrs_OK (fn_code f) = OK tt.
  Proof.
    intros until 0; intros Hmakege Hfp.
    eapply make_globalenv_find_funct_ptr in Hmakege; [|eassumption].
    destruct Hmakege as [i [_ [[fi [_ Hmi]] | [? [_ ?]]]]]; [|discriminate].
    simpl in *; destruct (instrs_OK (fn_code fi)) as [[]|] eqn:Heq; congruence.
  Qed.

  Lemma make_globalenv_instr_OK :
    ∀ {D} (ge:genv) b f ofs i s M L,
      make_globalenv (D:=D) s M L = ret ge →
      Genv.find_funct_ptr ge b = Some (Internal f) →
      find_instr (Int.unsigned ofs) (fn_code f) = Some i →
      instr_OK i = OK tt.
  Proof.
    intros; eapply instrs_OK_in.
    eapply find_instr_in; eassumption.
    eapply make_globalenv_instrs_OK; eassumption.
  Qed.

  Lemma make_program_instrs_OK :
    ∀ {D} b f s M L p,
      make_program (D:=D) s M L = OK p →
      Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal f) →
      instrs_OK (fn_code f) = OK tt.
  Proof.
    intros until 0; intros Hmakep Hfp.
    eapply make_globalenv_instrs_OK; eauto.
    eapply make_program_globalenv; eauto.
  Qed.

  Lemma make_program_instr_OK :
    ∀ {D} b f ofs i s M L p,
      make_program (D:=D) s M L = OK p →
      Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal f) →
      find_instr (Int.unsigned ofs) (fn_code f) = Some i →
      instr_OK i = OK tt.
  Proof.
    intros; eapply instrs_OK_in.
    eapply find_instr_in; eassumption.
    eapply make_program_instrs_OK; eassumption.
  Qed.

  Instance LC: ∀ {D} (L: compatlayer D)
                      `{acc_def_prf: !AccessorsDefined L},
                 LAsm.LayerConfigurationOps (ec_ops := compatlayer_extcall_ops L).
  Proof.
    intros. eapply compatlayer_configuration_ops; assumption.
  Defined.

  Inductive lasm_step {D}
            (M: module)
            (L: compatlayer D)
            (i: ident) (s: stencil)
            (rs: regset) (m: mwd D) (rs´: regset) (m´: mwd D): Prop :=
  | lasm_step_intro

      

      (acc_def_prf: AccessorsDefined L)

      

      (ge: genv)
      (b: block)
      (Hsymb: find_symbol s i = Some b)
      (Hge: make_globalenv s M L = ret ge)
      (PC_VAL: rs PC = Values.Vptr b Integers.Int.zero)

    

    (STAR: plus (LAsm.step (lcfg_ops := LC L))
                ge (State rs m) E0 (State rs´ m´))
  .

  Local Existing Instance extcall_invariants_defined_dec.
  Local Existing Instance primcall_invariants_defined_dec.

  Local Existing Instance prim_valid_dec.


  Definition accessors_weak_defined `{D: compatdata} (L: compatlayer D) : bool :=
    match cl_exec_load L with
      | Errors.OK _ ⇒
        match cl_exec_store L with
          | Errors.OK _ ⇒ true
          | _ ⇒ false
        end
      | _ ⇒ false
    end.

  Definition lasm_primsem {D: compatdata} (M: module) (L: compatlayer D) (i: ident) (f: function): compatsem D :=
    inr {|
        sprimcall_primsem_step :=
          {|
            sprimcall_step := lasm_step M L i;
            sprimcall_sig := fn_sig f;
            sprimcall_valid s :=
              if decide (ExtcallInvariantsDefined L) then
                if decide (PrimcallInvariantsDefined L) then
                 if decide (LayerNamesMatch D L) then
                  if decide (get_layer_prim_valid L s) then
                    if accessors_weak_defined L then
                      match make_program s M L with
                        | OK _ ⇒
                          true
                        | Error _ ⇒ false
                      end
                    else false
                  else false
                 else false
                else false
              else false
          |};
        sprimcall_name := Some i;
        sprimcall_props := Error nil;
        sprimcall_invs := Error nil
      |}.

  Global Instance lasm_ptree_sem_ops: FunctionSemanticsOps _ _ _ _ _ _ :=
    {
      semof_fundef D M L i f := OK (lasm_primsem M L i f)
    }.

End ModuleSemantics.