Changeset 1381 for src/RTL


Ignore:
Timestamp:
Oct 14, 2011, 10:29:54 PM (9 years ago)
Author:
sacerdot
Message:

Old commented out code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1377 r1381  
    11include "joint/SemanticUtils.ma".
    2 (*
    3 include "utilities/lists.ma".
    4 include "common/Errors.ma".
    5 include "common/Globalenvs.ma".
    6 include "common/IO.ma".
    7 include "common/SmallstepExec.ma".
    8 *)
    92include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    103include alias "common/Identifiers.ma".
     
    123116definition rtl_fullexec ≝
    124117 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
    125 
    126 (*
    127 (* CSC: external functions never fail (??) and always return something of the
    128    size of one register, both in the frontend and in the backend.
    129    Is this reasonable??? In OCaml it always return a list, but in the frontend
    130    only the head is kept (or Undef if the list is empty) ??? *)
    131 
    132 (* CSC: carries are values and booleans are not values; so we use integers.
    133    But why using values at all? To have undef? *)
    134 (* CSC: ???????????? *)
    135 axiom smerge: val → val → res val.
    136 (* CSC: ???????????? In OCaml: IntValue.Int32.merge
    137    Note also that the translation can fail; so it should be a res int! *)
    138 axiom smerge2: list val → int.
    139 (* CSC: I have a byte, I need a value, but it is complex to do so *)
    140 axiom val_of_Byte: Byte → val.
    141 axiom Byte_of_val: val → res Byte.
    142 (* Map from the front-end memory model to the back-end memory model *)
    143 axiom represent_block: block → val × val.
    144 (* CSC: fixed size chunk *)
    145 axiom chunk: memory_chunk.
    146 
    147 definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
    148 
    149 (* CSC: added carry *)
    150 record frame : Type[0] ≝
    151 { func   : rtl_internal_function
    152 ; locals : register_env val
    153 ; next   : label
    154 ; sp     : block
    155 ; retdst : list register
    156 ; carry  : val
    157 }.
    158 
    159 (* CSC: added carry *)
    160 definition adv : label → frame → frame ≝
    161 λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
    162 
    163 inductive state : Type[0] ≝
    164 | State :
    165    ∀   f : frame.
    166    ∀  fs : list frame.
    167    ∀   m : mem.
    168    state
    169 | Callstate :
    170    ∀  fd : fundef rtl_internal_function.
    171    ∀args : list val.
    172    ∀ dst : list register. (* CSC: changed from option to list *)
    173    ∀ stk : list frame.
    174    ∀   m : mem.
    175    state
    176 | Returnstate :
    177    (* CSC: the two lists should have the same length, but this is
    178       enforced only by the semantics *)
    179    ∀ rtv : list val. (* CSC: changed from option to list *)
    180    ∀ dst : list register. (* CSC: changed from option to list *)
    181    ∀ stk : list frame.
    182    ∀   m : mem.
    183    state.
    184 
    185 definition mem_of_state : state → mem ≝
    186 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
    187 
    188 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    189 
    190 (* CSC: modified to take in input a list of registers (untyped) *)
    191 definition init_locals : list register → register_env val ≝
    192 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    193 
    194 definition reg_store ≝
    195 λreg,v,locals.
    196   update RegisterTag val locals reg v.
    197 
    198 axiom WrongNumberOfParameters : String.
    199 
    200 (* CSC: modified to take in input a list of registers (untyped) *)
    201 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    202 match rs with
    203 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    204 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    205   let locals' ≝ add RegisterTag val locals r v in
    206   params_store rst vst locals'
    207 ] ].
    208 
    209 axiom BadRegister : String.
    210 
    211 definition reg_retrieve : register_env ? → register → res val ≝
    212 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    213 
    214 axiom FailedOp : String.
    215 axiom MissingSymbol : String.
    216 
    217 axiom MissingStatement : String.
    218 axiom FailedConstant : String.
    219 axiom FailedLoad : String.
    220 axiom FailedStore : String.
    221 axiom BadFunction : String.
    222 axiom BadJumpTable : String.
    223 axiom BadJumpValue : String.
    224 axiom FinalState : String.
    225 axiom ReturnMismatch : String.
    226 
    227 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    228 λge,st.
    229 match st with
    230 [ State f fs m ⇒
    231   ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
    232   match s with
    233   [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    234   | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    235   | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
    236       ! vaddrh ← reg_retrieve (locals f) addrh;
    237       ! vaddrl ← reg_retrieve (locals f) addrl;
    238       ! vaddr ← smerge vaddrl vaddrh;
    239       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    240       ! locals ← reg_store dst v (locals f);
    241       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    242   | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
    243       ! vaddrh ← reg_retrieve (locals f) addrh;
    244       ! vaddrl ← reg_retrieve (locals f) addrl;
    245       ! vaddr ← smerge vaddrl vaddrh;
    246       ! v ← reg_retrieve (locals f) src;
    247       ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    248       ret ? 〈E0, build_state f fs m' l〉
    249   | rtl_st_call_id id args dst l ⇒
    250       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    251       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    252       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    253       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    254   | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
    255       ! hfv ← reg_retrieve (locals f) hfrs;
    256       ! lfv ← reg_retrieve (locals f) lfrs;
    257       ! fv  ← smerge lfv hfv;
    258       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    259       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    260       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    261   | rtl_st_tailcall_id id args ⇒
    262       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    263       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    264       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    265       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    266   | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
    267       ! hfv ← reg_retrieve (locals f) hfrs;
    268       ! lfv ← reg_retrieve (locals f) lfrs;
    269       ! fv  ← smerge lfv hfv;
    270       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    271       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    272       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    273   | rtl_st_return ⇒
    274       (* CSC: rtl_if_result/f_result; list vs option *)
    275       let dest ≝ rtl_if_result (func f) in
    276       ! v ←  mmap … (reg_retrieve (locals f)) dest;
    277       ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    278   | rtl_st_cond src ltrue lfalse ⇒
    279       ! v ← reg_retrieve (locals f) src;
    280       ! b ← eval_bool_of_val v;
    281       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    282   (* CSC: mismatch between the memory models and failures for the next two opx *)
    283   | rtl_st_op1 op dst src l ⇒
    284      ! v ← reg_retrieve (locals f) src;
    285      ! v ← Byte_of_val v;
    286      let v' ≝ val_of_Byte (op1 eval op v) in
    287      ! locals ← reg_store dst v' (locals f);
    288      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    289   | rtl_st_op2 op dst src1 src2 l ⇒
    290      ! v1 ← reg_retrieve (locals f) src1;
    291      ! v1 ← Byte_of_val v1;
    292      ! v2 ← reg_retrieve (locals f) src2;
    293      ! v2 ← Byte_of_val v2;
    294      ! carry ← eval_bool_of_val (carry f);
    295      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    296      let v' ≝ val_of_Byte v' in
    297      let carry ≝ of_bool carry in
    298      ! locals ← reg_store dst v' (locals f);
    299      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
    300 
    301   (* CSC: Removed: St_jumptable *)
    302   (* CSC: Added: *)
    303  
    304   (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
    305   | rtl_st_addr ldest hdest id l ⇒
    306      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    307      let 〈laddr,haddr〉 ≝ represent_block addr in
    308      ! locals ← reg_store ldest laddr (locals f);
    309      ! locals ← reg_store hdest haddr locals;
    310      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    311   | rtl_st_stack_addr ldest hdest l ⇒
    312      let 〈laddr,haddr〉 ≝ represent_block (sp f) in
    313      ! locals ← reg_store ldest laddr (locals f);
    314      ! locals ← reg_store hdest haddr locals;
    315      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    316   | rtl_st_int dest v l ⇒
    317      ! locals ← reg_store dest (val_of_Byte v) (locals f);
    318      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    319 
    320   (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
    321   | rtl_st_move dst src l ⇒
    322      ! v ← reg_retrieve (locals f) src;
    323      ! locals ← reg_store dst v (locals f);
    324      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    325   (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
    326   | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    327      ! v1 ← reg_retrieve (locals f) sacc;
    328      ! v1 ← Byte_of_val v1;
    329      ! v2 ← reg_retrieve (locals f) sbacc;
    330      ! v2 ← Byte_of_val v2;
    331      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    332      let v1' ≝ val_of_Byte v1' in
    333      let v2' ≝ val_of_Byte v2' in
    334      ! locals ← reg_store dacc v1' (locals f);
    335      ! locals ← reg_store dbacc v2' locals;
    336      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    337  
    338   | rtl_st_clear_carry l ⇒
    339     ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
    340   | rtl_st_set_carry l ⇒
    341     ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
    342   ]
    343 | Callstate fd params dst fs m ⇒
    344     match fd with
    345     [ Internal fn ⇒
    346         ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
    347         let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
    348         (* CSC: added carry *)
    349         ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
    350     | External fn ⇒
    351         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    352         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    353         (* CSC: return type changed from option to list *)
    354         (* CSC: XXX bug here; I think I should split it into Byte-long
    355            components; instead I am making a singleton out of it *)
    356         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    357     ]
    358 | Returnstate v dst fs m ⇒
    359     match fs with
    360     [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    361     | cons f fs' ⇒
    362        ! locals ←
    363          mfold_left2 ???
    364           (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
    365         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
    366     ]
    367 ].
    368 
    369 axiom WrongReturnValueType: String.
    370 
    371 definition is_final : state → option ((*CSC: why not res*) int) ≝
    372 λs. match s with
    373 [ State _ _ _ ⇒ None ?
    374 | Callstate _ _ _ _ _ ⇒ None ?
    375 | Returnstate v _ fs _ ⇒
    376     match fs with
    377      [ nil ⇒ Some ? (smerge2 v)
    378      | _ ⇒ None ? ]].
    379 (*
    380 definition RTL_exec : execstep io_out io_in ≝
    381   mk_execstep … ? is_final mem_of_state eval_statement.
    382 *)
    383 (* CSC: XXX the program type does not fit with the globalenv and init_mem
    384 definition make_initial_state : rtl_program → res (genv × state) ≝
    385 λp.
    386   do ge ← globalenv Genv ?? p;
    387   do m ← init_mem Genv ?? p;
    388   let main ≝ rtl_pr_main ?? p in
    389   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    390   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    391   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
    392 
    393 definition RTL_fullexec : fullexec io_out io_in ≝
    394   mk_fullexec … RTL_exec ? make_initial_state.
    395 *)
    396 *)
Note: See TracChangeset for help on using the changeset viewer.