source: src/RTLabs/semantics.ma @ 1352

(* 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 "RTLabs/syntax.ma".

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

record frame : Type[0] ≝
{ func   : internal_function
; locals : register_env val
; next   : label
; sp     : block
; retdst : option register
}.

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

inductive state : Type[0] ≝
| State : 
   ∀   f : frame.
   ∀  fs : list frame.
   ∀   m : mem.
   state
| Callstate :
   ∀  fd : fundef internal_function.
   ∀args : list val.
   ∀ dst : option register.
   ∀ stk : list frame.
   ∀   m : mem.
   state
| Returnstate :
   ∀ rtv : option val.
   ∀ dst : option register.
   ∀ 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 ?? (f_graph (func f)) (next f)); 
  match s with
  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
  | St_const r cst l ⇒
      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
      ! locals ← reg_store r v (locals f);
      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
  | St_op1 op dst src l ⇒
      ! v ← reg_retrieve (locals f) src;
      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
      ! locals ← reg_store dst v' (locals f);
      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
  | St_op2 op dst src1 src2 l ⇒
      ! v1 ← reg_retrieve (locals f) src1;
      ! v2 ← reg_retrieve (locals f) src2;
      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
      ! locals ← reg_store dst v' (locals f);
      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
  | St_load chunk addr dst l ⇒
      ! vaddr ← reg_retrieve (locals f) addr;
      ! 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)) fs m〉
  | St_store chunk addr src l ⇒
      ! vaddr ← reg_retrieve (locals f) addr;
      ! 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〉
  | 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〉
  | St_call_ptr frs args dst l ⇒
      ! fv ← reg_retrieve (locals f) frs;
      ! 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〉
  | 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))〉
  | St_tailcall_ptr frs args ⇒
      ! fv ← reg_retrieve (locals f) frs;
      ! 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))〉

  | 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)〉

  | St_jumptable r ls ⇒
      ! v ← reg_retrieve (locals f) r;
      match v with
      [ Vint _ i ⇒
          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
          ret ? 〈E0, build_state f fs m l〉
      | _ ⇒ Wrong ??? (msg BadJumpValue)
      ]

  | St_return ⇒
      ! v ← match f_result (func f) with
            [ None ⇒ ret ? (None ?)
            | Some rt ⇒
                let 〈r,ty〉 ≝ rt in
                ! v ← reg_retrieve (locals f) r;
                ret ? (Some ? v)
            ];
      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
  ]
| Callstate fd params dst fs m ⇒
    match fd with
    [ Internal fn ⇒
        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
           here *)
        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) 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));
        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    ]
| Returnstate v dst fs m ⇒
    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 : trans_system io_out io_in ≝
  mk_trans_system … ? (λ_.is_final) eval_statement.

definition make_global : RTLabs_program → genv ≝
λp. globalenv Genv ?? (λx.[Init_space x]) p.

definition make_initial_state : RTLabs_program → res state ≝
λp.
  let ge ≝ make_global p in
  do m ← init_mem Genv ?? (λx.[Init_space x]) 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 ? (Callstate f (nil ?) (None ?) (nil ?) m).

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