include "joint/semantics.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 ***)

axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
axiom hwreg_retrieve : hw_register_env → Register → res beval.
axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.

(****************************************************************************)

(*CSC: XXXX; do we need to create a brand new chunk per label, so that
  pointer operations on labels are not semantically valid?
  ATM, the pointers are not valid (they do not point to allocated regions)
  and, moreover, they conflict with function blocks and with other pointers
  in other functions. However, there could be simpler ways to invalidate
  pointer arithmetics on Code pointers.
*)
definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
 λl.
  mk_pointer Code
   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
   ? (mk_offset OZ). 
// qed.

(*CSC: XXXX; inverse of the previous function, but it does not check that
  the offset is zero and thus it never fails. *)
definition label_of_pointer: pointer → res label ≝
 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).

(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
  Maybe there is a better way to organize the code!!! *)
definition graph_succ_p: label → address → address.
 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
  [ #res #_ @res
  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct normalize in E2; destruct ]
qed.

axiom BadProgramCounter: String.
definition graph_fetch_statement:
 ∀params1,sem_params,globals.
  genv … (graph_params params1 globals) →
   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
 λparams1,sem_params,globals,ge,st.
  do p ← pointer_of_address (pc … st) ;
  let b ≝ pblock p in
  do l ← label_of_pointer p;
  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
  match def with
  [ Internal def' ⇒
     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
  | External _ ⇒ Error … [MSG BadProgramCounter]].