source: src/RTL/semantics.ma @ 1121

(* XXX NB: I haven't checked all of these semantics against the prototype
           compilers yet! *)

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: 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: 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 :
   ∀ 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.

definition init_locals : list (register × typ) → register_env val ≝
foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).

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

axiom WrongNumberOfParameters : String.

let rec params_store (rs:list (register × typ)) (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 rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
  let 〈r,ty〉 ≝ rt in
  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 (f_params fn) params (init_locals (f_locals fn));
        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
        ret ? 〈E0, State (mk_frame fn locals (f_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 *)
        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    ]
| Returnstate v dst fs m ⇒ ? (* CSC: XXXXXXXXXXXXXXXXXX
    match fs with
    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    | cons f fs' ⇒
        ! locals ← match dst with
                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    ] *)
].

definition is_final : state → option int ≝
λs. match s with
[ State _ _ _ ⇒ None ?
| Callstate _ _ _ _ _ ⇒ None ?
| Returnstate v _ fs _ ⇒
    match fs with [ nil ⇒
      match v with [ Some v' ⇒
        match v' with
        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
        | _ ⇒ None ? ]
      | None ⇒ None ? ]
    | cons _ _ ⇒ None ? ]
].

definition RTLabs_exec : execstep io_out io_in ≝
  mk_execstep … ? is_final mem_of_state eval_statement.

definition make_initial_state : RTLabs_program → res (genv × state) ≝
λp.
  do ge ← globalenv Genv ?? p;
  do m ← init_mem Genv ?? p;
  let main ≝ prog_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 ?) (None ?) (nil ?) m〉.

definition RTLabs_fullexec : fullexec io_out io_in ≝
  mk_fullexec … RTLabs_exec ? make_initial_state.