source: src/ERTL/semantics.ma @ 1363

include "joint/SemanticUtils.ma".
include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
include alias "common/Identifiers.ma".

definition ps_reg_store ≝
 λr,v.λlocal_env:(register_env beval) × hw_register_env.
  do res ← reg_store r v (\fst local_env) ;
  OK … 〈res, \snd local_env〉.

definition ps_reg_retrieve ≝
 λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).

definition hw_reg_store ≝
 λr,v.λlocal_env:(register_env beval) × hw_register_env.
  do res ← hwreg_store r v (\snd local_env) ;
  OK … 〈\fst local_env,res〉.

definition hw_reg_retrieve ≝
 λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env).

definition ertl_more_sem_params: more_sem_params ertl_params_ :=
 mk_more_sem_params ertl_params_
  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     (λlocals,dest_src.
       do v ←
        match \snd dest_src with
        [ pseudo reg ⇒ ps_reg_retrieve locals reg
        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
       match \fst dest_src with
       [ pseudo reg ⇒ ps_reg_store reg v locals
       | hardware reg ⇒ hw_reg_store reg v locals])
     pointer_of_label.
definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.

definition ertl_init_locals :
 list register →
  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
 λlocals,lenv.
  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.

(*CSC: could we use here a dependent type to avoid the Error case? *)
axiom EmptyStack: String.
definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
 λ_.λst.
  let frms ≝ st_frms ? st in
  match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].

definition ertl_save_frame: unit → state … ertl_sem_params → state … ertl_sem_params ≝
 λ_.λst.
  set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.

definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
 mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
  ertl_init_locals ertl_pop_frame ertl_save_frame.

(*CSC: XXXXX, for is_final only *)
axiom ertl_fetch_result: state ertl_sem_params → res (list beval).

(*CSC: XXXX, for external functions only*)
axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).

(*CSC: XXXX *)
axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝
  λglobals: list ident.
  λst.
   do f ← fetch_function globals st ;
   OK ? (joint_if_stacksize globals … f).*)

definition get_hwsp : state ertl_sem_params → res address ≝
 λst.
  do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ;
  do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ;
  OK ? 〈spl,sph〉.

definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝
 λsp,st.
  let 〈spl,sph〉 ≝ sp in
  do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ;
  do hwregs ← hwreg_store RegisterSPH sph hwregs ;
  OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st).

definition ertl_exec_extended:
 ∀globals. genv globals (ertl_params globals) →
  ertl_statement_extension → label → state ertl_sem_params →
   IO io_out io_in (trace × (state ertl_sem_params)) ≝
 λglobals,ge,stm,l,st.
  match stm with
   [ ertl_st_ext_new_frame ⇒
      ! v ← framesize globals st;
      ! sp ← get_hwsp st;
      ! newsp ← addr_sub sp v;
      ! st ← set_hwsp newsp st;
        ret ? 〈E0,goto … l st〉
   | ertl_st_ext_del_frame ⇒
      ! v ← framesize globals st;
      ! sp ← get_hwsp st;
      ! newsp ← addr_add sp v;
      ! st ← set_hwsp newsp st;
        ret ? 〈E0,goto … l st〉
   | ertl_st_ext_frame_size dst ⇒
      ! v ← framesize globals st;
      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
        ret ? 〈E0, goto … l st〉
   ].

definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
 λglobals.
  mk_more_sem_params2 … ertl_more_sem_params1
   (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
    (ertl_exec_extended …).

definition ertl_fullexec ≝
 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).

(*
(* CSC: external functions never fail (??) and always return something of the
   size of one register, both in the frontend and in the backend.
   Is this reasonable??? In OCaml it always return a list, but in the frontend
   only the head is kept (or Undef if the list is empty) ??? *)

(* CSC: carries are values and booleans are not values; so we use integers.
   But why using values at all? To have undef? *)
(* CSC: ???????????? *)
axiom smerge: val → val → res val.
(* CSC: ???????????? In OCaml: IntValue.Int32.merge
   Note also that the translation can fail; so it should be a res int! *)
axiom smerge2: list val → int.
(* CSC: I have a byte, I need a value, but it is complex to do so *)
axiom val_of_Byte: Byte → val.
axiom Byte_of_val: val → res Byte.
axiom val_of_nat: nat → val.
(* Map from the front-end memory model to the back-end memory model *)
axiom represent_block: block → val × val.
(* CSC: fixed size chunk *)
axiom chunk: memory_chunk.
axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)

axiom address: Type[0].
axiom val_of_address: address → val. (* CSC: only to shift the sp *)
axiom address_of_val: val → address. (* CSC: only to shift the sp *)
axiom addr_sub: address → nat → address.
axiom addr_add: address → nat → address.
(* CSC: ??? *)
axiom address_of_label: mem → label → address.
axiom address_chunks_of_label: mem → label → Byte × Byte.
axiom label_of_address_chunks: Byte → Byte → label.
axiom address_of_address_chunks: Byte → Byte → address.
axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
axiom hwreg_retrieve : mRegisterMap → Register → res val.
axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.

definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).

(* CSC: frame reduced to this *)
definition frame: Type[0] ≝ register_env val.

(* CSC: exit not put in the state, like in OCaml. It is constant througout
   execution *)
record state : Type[0] ≝
 { st_frms: list frame
 ; pc: address
 ; sp: address
 ; locals: register_env val
 ; carry: val
 ; regs: mRegisterMap
 ; m: mem
 }.

definition set_m: mem → state → state ≝
 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.

definition set_locals: register_env val → state → state ≝
 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).

definition set_regs: mRegisterMap → state → state ≝
 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).

definition set_sp: address → state → state ≝
 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).

definition set_carry: val → state → state ≝
 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).

definition set_pc: address → state → state ≝
 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).

(* CSC: was build_state in RTL *)
definition goto: label → state → state ≝
 λl,st. set_pc (address_of_label (m st) l) st.

(* pushes the locals (i.e. the current frame) on top of the frames list *)
definition save_frame: state → state ≝
 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).

axiom FailedPopFrame: String.

(* removes the top frame from the frames list *)
definition pop_frame: state → res state ≝
 λst.
  match st_frms st with
   [ nil ⇒ Error ? (msg FailedPopFrame)
   | cons _ frms ⇒
      OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].

axiom FailedStore: String.

definition push: state → Byte → res state ≝
 λst,v.
  let sp ≝ val_of_address (sp st) in
  (*CSC: no monadic notation here *)
  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
   (λm.
    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    OK ? (set_m m (set_sp sp st))).


definition pop: state → res (state × Byte) ≝
 λst:state.
  let sp ≝ val_of_address (sp st) in
  let sp ≝ sub sp (val_of_memory_chunk chunk) in
  let st ≝ set_sp (address_of_val sp) st in
  (*CSC: no monadic notation here *)
  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).

definition save_ra : state → label → res state ≝
 λst,l.
  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
  (* No monadic notation here *)
  bind ?? (push st addrl) (λst.push st addrh).

definition fetch_ra : state → res (state × label) ≝
 λst.
  (* No monadic notation here *)
  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
   OK ? 〈st, label_of_address_chunks addrl addrh〉)).

(*CSC: To be implemented *)

axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).

definition init_locals : list register → register_env val ≝
foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).

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

axiom BadRegister : String.

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

axiom MissingSymbol : String.
axiom FailedLoad : String.
axiom BadFunction : String.

(*CSC: to be implemented *)
axiom fetch_external_args: external_function → state → res (list val).(* ≝
 λfn,st.
  let registerno ≝ ? fn in
  ! vs ←
   mmap …
    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
  ?.*)

(*CSC: to be implemented; fails if the first list is longer *)
axiom fold_left2_first_not_longer:
 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
  ∀acc:C. ∀l1:list A. ∀l2: list B.
   res C.

(* CSC: the list should be a vector or have an upper bounded length *)
definition set_result: list val → state → res state ≝
 λvs,st.
  (* CSC: monadic notation not used *)
  bind ?? ( 
   fold_left2_first_not_longer …
    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
  (λregs.OK ? (set_regs regs st)).

definition fetch_result: state → nat → res (list val) ≝
 λst,registersno.
  let retregs ≝ prefix … registersno RegisterRets in
  mmap … (λr. hwreg_retrieve (regs st) r) retregs.

definition framesize: list ident → state → res nat ≝
  λglobals: list ident.
  λst.
  (* CSC: monadic notation missing here *)
    bind ?? (fetch_function globals st) (λf.
    OK ? (joint_if_stacksize globals … f)).

definition get_hwsp : state → res address ≝
 λst.
  (* CSC: monadic notation missing here *)
  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
  (* CSC: monadic notation missing here *)
  bind ?? (Byte_of_val spl) (λspl.
  (* CSC: monadic notation missing here *)
  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
  (* CSC: monadic notation missing here *)
  bind ?? (Byte_of_val sph) (λsph.
  OK ? (address_of_address_chunks spl sph))))).

definition set_hwsp : address → state → res state ≝
 λsp,st.
  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
  (* CSC: monadic notation missing here *)  
  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
  (* CSC: monadic notation missing here *)  
  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
  OK ? (set_regs regs st))).

definition retrieve: state → move_registers → res val ≝
  λst.
  λr.
  match r with
  [ pseudo   src ⇒ reg_retrieve (locals st) src 
  | hardware src ⇒ hwreg_retrieve (regs st) src
  ].

definition store ≝
  λst.
  λv.
  λr.
  match r with
  [ pseudo   dst ⇒
    ! locals ← reg_store dst v (locals st);
      ret ? (set_locals locals st)
  | hardware dst ⇒
    ! regs ← hwreg_store dst v (regs st);
      ret ? (set_regs regs st)
  ].

definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
  λglobals. λge,st.
  ! s ← fetch_statement globals st; 
  match s with
  [ ertl_st_lift_pre pre ⇒
    match pre with
    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
    | joint_st_sequential seq l ⇒
      match seq with
      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
      | joint_instr_int dest v ⇒
        ! locals ← reg_store dest (val_of_Byte v) (locals st);
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_load addrl addrh dst ⇒
        ! vaddrh ← reg_retrieve (locals st) addrh;
        ! vaddrl ← reg_retrieve (locals st) addrl;
        ! vaddr ← smerge vaddrl vaddrh;
        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
        ! locals ← reg_store dst v (locals st);
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_store addrl addrh src ⇒
        ! vaddrh ← reg_retrieve (locals st) addrh;
        ! vaddrl ← reg_retrieve (locals st) addrl;
        ! vaddr ← smerge vaddrl vaddrh;
        ! v ← reg_retrieve (locals st) src;
        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
          ret ? 〈E0, goto l (set_m m' st)〉
      | joint_instr_cond src ltrue ⇒
        ! v ← reg_retrieve (locals st) src;
        ! b ← eval_bool_of_val v;
          ret ? 〈E0, goto (if b then ltrue else l) st〉
      | joint_instr_address ident prf ldest hdest ⇒
        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
          let 〈laddr,haddr〉 ≝ represent_block addr in
        ! locals ← reg_store ldest laddr (locals st);
        ! locals ← reg_store hdest haddr locals;
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_op1 op acc_a ⇒
        ! v ← reg_retrieve (locals st) acc_a;
        ! v ← Byte_of_val v;
          let v' ≝ val_of_Byte (op1 eval op v) in
        ! locals ← reg_store acc_a v' (locals st);
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_op2 op acc_a_reg dest ⇒
        ! v1 ← reg_retrieve (locals st) acc_a_reg;
        ! v1 ← Byte_of_val v1;
        ! v2 ← reg_retrieve (locals st) acc_a_reg;
        ! v2 ← Byte_of_val v2;
        ! carry ← eval_bool_of_val (carry st);
          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
          let v' ≝ val_of_Byte v' in
          let carry ≝ of_bool carry in
        ! locals ← reg_store dest v' (locals st);
          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
        ! v1 ← reg_retrieve (locals st) acc_a_reg;
        ! v1 ← Byte_of_val v1;
        ! v2 ← reg_retrieve (locals st) acc_b_reg;
        ! v2 ← Byte_of_val v2;
          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
          let v1' ≝ val_of_Byte v1' in
          let v2' ≝ val_of_Byte v2' in
        ! locals ← reg_store acc_a_reg v1' (locals st);
        ! locals ← reg_store acc_b_reg v2' locals;
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_pop dst ⇒
        ! 〈st,v〉 ← pop st;
        ! locals ← reg_store dst (val_of_Byte v) (locals st);
          ret ? 〈E0, goto l (set_locals locals st)〉
      | joint_instr_push src ⇒
        ! v ← reg_retrieve (locals st) src;
        ! v ← Byte_of_val v; 
        ! st ← push st v;
          ret ? 〈E0, goto l st〉
      | joint_instr_move dst_src ⇒
        let 〈dst, src〉 ≝ dst_src in
        ! v ← retrieve st src;
        ! st ← store st v dst;
          ret ? 〈E0, goto l st〉
      (* CSC: changed, where the meat is *)
      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
          match fd with
          [ Internal fn ⇒
            ! st ← save_ra st l;
              let st ≝ save_frame st in
              let locals ≝ init_locals (ertl_if_locals globals fn) in
              let l' ≝ ertl_if_entry globals fn in
              ret ? 〈 E0, goto l' (set_locals locals st)〉
          | External fn ⇒
            ! params ← fetch_external_args fn st;
            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
            (* CSC: XXX bug here; I think I should split it into Byte-long
               components; instead I am making a singleton out of it *)
              let vs ≝ [mk_val ? evres] in
            ! st ← set_result vs st; 
              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
          ]
      ]
    (* CSC: changed, where the meat is *)
    | joint_st_return ⇒
      ! st ← pop_frame st;
      ! 〈st,pch〉 ← pop st;
      ! 〈st,pcl〉 ← pop st;
        let pc ≝ address_of_address_chunks pcl pch in
        ret ? 〈E0,set_pc pc st〉
    | _ ⇒ ?
    ]
  | ertl_st_new_frame l ⇒
    ! v ← framesize globals st;
    ! sp ← get_hwsp st;
      let newsp ≝ addr_sub sp v in
    ! st ← set_hwsp newsp st;
      ret ? 〈E0,goto l st〉
  | ertl_st_del_frame l ⇒
    ! v ← framesize globals st;
    ! sp ← get_hwsp st;
      let newsp ≝ addr_add sp v in
    ! st ← set_hwsp newsp st;
      ret ? 〈E0,goto l st〉
  | ertl_st_frame_size dst l ⇒
    ! v ← framesize globals st;
    ! locals ← reg_store dst (val_of_nat v) (locals st);
      ret ? 〈E0, goto l (set_locals locals st)〉
  (* CSC: Dropped:
      - rtl_st_stackaddr (becomes two get_hdw)
      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
      - rtl_st_call_ptr (unimplemented ATM) *)
  ].
      
axiom WrongReturnValueType: String.

definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
  λglobals: list ident.
  λexit.
  λregistersno.
  λst.
 (* CSC: monadic notation missing here *)
  match fetch_statement globals st with
  [ Error _ ⇒ None ?
  | OK s ⇒
    match s with
    [ ertl_st_lift_pre pre ⇒
      match pre with
      [ joint_st_return ⇒
        match fetch_ra st with
         [ Error _ ⇒ None ?
         | OK st_l ⇒
           let 〈st,l〉 ≝ st_l in
           match label_eq l exit with
           [ inl _ ⇒
             (* CSC: monadic notation missing here *)
             match fetch_result st registersno with
             [ Error _ ⇒ None ?
             | OK vals ⇒ Some ? (smerge2 vals)
             ]
           | inr _ ⇒ None ?
           ]
         ]
      | _ ⇒ None ?
      ]
    | _ ⇒ None ?
    ]
  ].

definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
  λglobals.
  λexit.
  λregistersno.
  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).

(* CSC: XXX the program type does not fit with the globalenv and init_mem
definition make_initial_state : rtl_program → res (genv × state) ≝
λp.
  do ge ← globalenv Genv ?? p;
  do m ← init_mem Genv ?? p;
  let main ≝ rtl_pr_main ?? p in
  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.

definition RTL_fullexec : fullexec io_out io_in ≝
  mk_fullexec … RTL_exec ? make_initial_state.
*)
*)