include "joint/semantics_paolo.ma".
include alias "common/Identifiers.ma".

(*** Store/retrieve on pseudo-registers ***)

axiom BadRegister : String.

definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.

definition reg_retrieve : register_env beval → register → res beval ≝
 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).

(*** Store/retrieve on hardware registers ***)

definition init_hw_register_env: address → hw_register_env ≝
 λaddr.
  let 〈dpl,dph〉 ≝ addr in
  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
   hwreg_store RegisterDPL dpl env.

(******************************** GRAPHS **************************************)

definition graph_pointer_of_label0:
 pointer → label → Σp:pointer. ptype p = Code ≝
 λoldpc,l.
  mk_pointer Code
   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))). 
// qed.

definition graph_pointer_of_label :
  ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
    res (Σp:pointer. ptype p = Code) ≝
 λ_.λ_.λ_.λoldpc,l.
  OK ? (graph_pointer_of_label0 oldpc l). 

definition graph_label_of_pointer: pointer → res label ≝
 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).

(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
 But I can't use it directly because this one uses a concrete definition of
 pointer_of_label and it is used to istantiate the more_sem_params record
 where the abstract version is declared as a field. Is there a better way
 to organize the code? *)
definition graph_succ_p: label → address → res address ≝
 λl,old.
  do ptr ← pointer_of_address old ;
  let newptr ≝ graph_pointer_of_label0 ptr l in
  address_of_pointer newptr.

definition graph_fetch_statement:
 ∀pars : graph_params.
 ∀sem_pars : sem_state_params.
 ∀globals.
  genv globals pars →
  state sem_pars →
  res (joint_statement pars globals) ≝
 λpars,sem_pars,globals,ge,st.
  do p ← code_pointer_of_address (pc … st) ;
  do f ← fetch_function … ge p ;
  do l ← graph_label_of_pointer p;
  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).

definition make_sem_graph_params :
  ∀pars : graph_params.
  ∀g_pars : more_sem_genv_params pars.
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      graph_succ_p
      (graph_pointer_of_label ?)
      (graph_fetch_statement ? ?)
    ).
    
(******************************** LINEAR **************************************)

definition lin_succ_p: unit → address → res address :=
 λ_.λaddr. addr_add addr 1.


axiom BadLabel: String.

definition lin_pointer_of_label:
 ∀pars : lin_params.
 ∀globals. genv globals pars → pointer → label →
  res (Σp:pointer. ptype p = Code) ≝
 λpars,globals,ge,old,l.
  do fn ← fetch_function … ge old ;
  do pos ←
   opt_to_res ? [MSG BadLabel]
    (position_of ?
      (λs. let 〈l',x〉 ≝ s in
        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
     (joint_if_code … pars fn)) ;
  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
// qed.

definition lin_fetch_statement:
 ∀pars : lin_params.
 ∀sem_pars : sem_state_params.
 ∀globals.
 genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
 λpars,sem_pars,globals,ge,st.
  do ppc ← pointer_of_address (pc … st) ;
  do fn ← fetch_function … ge ppc ;
  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
  return (\snd found).

definition make_sem_lin_params :
  ∀pars : lin_params.
  ∀g_pars : more_sem_genv_params pars.
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      lin_succ_p
      (lin_pointer_of_label ?)
      (lin_fetch_statement ? ?)
    ).