source: src/RTL/semantics.ma @ 1324

include "joint/SemanticUtils.ma".
(*
include "utilities/lists.ma".
include "common/Errors.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
*)
include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)

(* CSC: a streamlined version of the ERTL state *)
record frame: Type[0] ≝
 { fr_pc: address
 ; fr_sp: pointer
 ; fr_carry: beval
 ; fr_regs: register_env beval
 }.

definition rtl_more_sem_params: more_sem_params rtl_params_ :=
 mk_more_sem_params rtl_params_
  (list frame) (register_env beval) graph_succ_p
   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    reg_store reg_retrieve reg_store reg_retrieve
     (λlocals,dest_src.
       do v ← reg_retrieve locals (\snd dest_src) ;
       reg_store (\fst dest_src) v locals)
     pointer_of_label.
definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.

definition rtl_init_locals :
 list register → register_env beval → register_env beval ≝
 λlocals.λ_.
  foldl ?? (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals.

(*CSC: could we use here a dependent type to avoid the Error case? *)
axiom EmptyStack: String.
definition rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params) ≝
 λst.
  let frms ≝ st_frms ? st in
  match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
     OK …
      (set_frms rtl_sem_params tl
       (set_regs rtl_sem_params (fr_regs hd)
        (set_sp … (fr_sp hd)
         (set_pc … (fr_pc hd)
          (set_carry … (fr_carry hd) st))))) ].

definition rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params ≝
 λst.
  set_frms rtl_sem_params
   (mk_frame (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.

definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
  rtl_init_locals rtl_pop_frame rtl_save_frame.


(*CSC: XXXXX, for is_final only *)
axiom rtl_fetch_result: state rtl_sem_params → nat → res val.

(*CSC: XXXX, for external functions only*)
axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).

definition rtl_exec_extended:
 ∀globals. genv globals (rtl_params globals) →
  rtl_statement_extension → label → state rtl_sem_params →
   IO io_out io_in (trace × (state rtl_sem_params)) ≝
 λglobals,ge,stm,l,st.
  match stm with
   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
      let sp ≝ sp ? st in
      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
      ! regs ← reg_store dreg1 dpl (regs ? st) ;
      ! regs ← reg_store dreg2 dph regs ;
       ret ? 〈E0, goto … l (set_regs rtl_sem_params regs st)〉
   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
   | rtl_st_ext_tailcall_id id regs ⇒ ?
   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
   ].
[1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
qed.

definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
 λglobals.
  mk_more_sem_params2 … rtl_more_sem_params1
   (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
    (rtl_exec_extended …).

definition rtl_fullexec ≝
 joint_fullexec … (λp. rtl_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.
(* 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.

definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).

(* CSC: added carry *)
record frame : Type[0] ≝
{ func   : rtl_internal_function
; locals : register_env val
; next   : label
; sp     : block
; retdst : list register
; carry  : val
}.

(* CSC: added carry *)
definition adv : label → frame → frame ≝
λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).

inductive state : Type[0] ≝
| State : 
   ∀   f : frame.
   ∀  fs : list frame.
   ∀   m : mem.
   state
| Callstate :
   ∀  fd : fundef rtl_internal_function.
   ∀args : list val.
   ∀ dst : list register. (* CSC: changed from option to list *)
   ∀ stk : list frame.
   ∀   m : mem.
   state
| Returnstate :
   (* CSC: the two lists should have the same length, but this is
      enforced only by the semantics *)
   ∀ rtv : list val. (* CSC: changed from option to list *)
   ∀ dst : list register. (* CSC: changed from option to list *)
   ∀ stk : list frame.
   ∀   m : mem.
   state.

definition mem_of_state : state → mem ≝
λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].

definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.

(* CSC: modified to take in input a list of registers (untyped) *)
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 WrongNumberOfParameters : String.

(* CSC: modified to take in input a list of registers (untyped) *)
let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
match rs with
[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
  let locals' ≝ add RegisterTag val locals r v in
  params_store rst vst locals'
] ].

axiom BadRegister : String.

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

axiom FailedOp : String.
axiom MissingSymbol : String.

axiom MissingStatement : String.
axiom FailedConstant : String.
axiom FailedLoad : String.
axiom FailedStore : String.
axiom BadFunction : String.
axiom BadJumpTable : String.
axiom BadJumpValue : String.
axiom FinalState : String.
axiom ReturnMismatch : String.

definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
λge,st.
match st with
[ State f fs m ⇒
  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f)); 
  match s with
  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
      ! vaddrh ← reg_retrieve (locals f) addrh;
      ! vaddrl ← reg_retrieve (locals f) addrl;
      ! vaddr ← smerge vaddrl vaddrh;
      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
      ! locals ← reg_store dst v (locals f);
      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
      ! vaddrh ← reg_retrieve (locals f) addrh;
      ! vaddrl ← reg_retrieve (locals f) addrl;
      ! vaddr ← smerge vaddrl vaddrh;
      ! v ← reg_retrieve (locals f) src;
      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
      ret ? 〈E0, build_state f fs m' l〉
  | rtl_st_call_id id args dst l ⇒
      ! 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);
      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
      ! hfv ← reg_retrieve (locals f) hfrs;
      ! lfv ← reg_retrieve (locals f) lfrs;
      ! fv  ← smerge lfv hfv;
      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
  | rtl_st_tailcall_id id args ⇒
      ! 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);
      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
      ! hfv ← reg_retrieve (locals f) hfrs;
      ! lfv ← reg_retrieve (locals f) lfrs;
      ! fv  ← smerge lfv hfv;
      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
  | rtl_st_return ⇒
      (* CSC: rtl_if_result/f_result; list vs option *)
      let dest ≝ rtl_if_result (func f) in
      ! v ←  mmap … (reg_retrieve (locals f)) dest;
      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
  | rtl_st_cond src ltrue lfalse ⇒
      ! v ← reg_retrieve (locals f) src;
      ! b ← eval_bool_of_val v;
      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
  (* CSC: mismatch between the memory models and failures for the next two opx *)
  | rtl_st_op1 op dst src l ⇒
     ! v ← reg_retrieve (locals f) src;
     ! v ← Byte_of_val v;
     let v' ≝ val_of_Byte (op1 eval op v) in
     ! locals ← reg_store dst v' (locals f);
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
  | rtl_st_op2 op dst src1 src2 l ⇒
     ! v1 ← reg_retrieve (locals f) src1;
     ! v1 ← Byte_of_val v1;
     ! v2 ← reg_retrieve (locals f) src2;
     ! v2 ← Byte_of_val v2;
     ! carry ← eval_bool_of_val (carry f);
     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 dst v' (locals f);
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉 

  (* CSC: Removed: St_jumptable *)
  (* CSC: Added: *)
  
  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
  | rtl_st_addr ldest hdest id l ⇒
     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
     let 〈laddr,haddr〉 ≝ represent_block addr in
     ! locals ← reg_store ldest laddr (locals f);
     ! locals ← reg_store hdest haddr locals;
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
  | rtl_st_stack_addr ldest hdest l ⇒
     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
     ! locals ← reg_store ldest laddr (locals f);
     ! locals ← reg_store hdest haddr locals;
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
  | rtl_st_int dest v l ⇒
     ! locals ← reg_store dest (val_of_Byte v) (locals f);
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉

  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
  | rtl_st_move dst src l ⇒
     ! v ← reg_retrieve (locals f) src;
     ! locals ← reg_store dst v (locals f);
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *)  
  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
     ! v1 ← reg_retrieve (locals f) sacc;
     ! v1 ← Byte_of_val v1;
     ! v2 ← reg_retrieve (locals f) sbacc;
     ! 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 dacc v1' (locals f);
     ! locals ← reg_store dbacc v2' locals;
     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 
  
  | rtl_st_clear_carry l ⇒
    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
  | rtl_st_set_carry l ⇒
    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
  ]
| Callstate fd params dst fs m ⇒
    match fd with
    [ Internal fn ⇒
        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
        (* CSC: added carry *)
        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
    | External fn ⇒
        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
        (* CSC: return type changed from option to list *)
        (* CSC: XXX bug here; I think I should split it into Byte-long
           components; instead I am making a singleton out of it *)
        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    ]
| Returnstate v dst fs m ⇒
    match fs with
    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    | cons f fs' ⇒
       ! locals ←
         mfold_left2 ???
          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
    ]
].

axiom WrongReturnValueType: String.

definition is_final : state → option ((*CSC: why not res*) int) ≝
λs. match s with
[ State _ _ _ ⇒ None ?
| Callstate _ _ _ _ _ ⇒ None ?
| Returnstate v _ fs _ ⇒
    match fs with
     [ nil ⇒ Some ? (smerge2 v)
     | _ ⇒ None ? ]].
(*
definition RTL_exec : execstep io_out io_in ≝
  mk_execstep … ? is_final mem_of_state eval_statement.
*)
(* 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.
*)
*)