Changeset 1174


Ignore:
Timestamp:
Sep 2, 2011, 4:09:02 PM (8 years ago)
Author:
sacerdot
Message:

Semantics of most instructions completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1173 r1174  
    3333axiom val_of_nat: nat → val.
    3434(* Map from the front-end memory model to the back-end memory model *)
     35*)
    3536axiom represent_block: block → val × val.
    36 *)
    3737(* CSC: fixed size chunk *)
    3838axiom chunk: memory_chunk.
     
    4747(* CSC: ??? *)
    4848axiom address_of_label: mem → label → address.
    49 (*
    5049axiom address_chunks_of_label: mem → label → Byte × Byte.
     50(*
    5151axiom label_of_address_chunks: Byte → Byte → label.
    5252*)
     
    7070 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
    7171 ; pop_frame_: framesT → res framesT
     72 ; save_frame_: framesT → regsT → framesT
    7273 ; greg_store_: generic_reg p → val → regsT → res regsT
    7374 ; greg_retrieve_: regsT → generic_reg p → res val
     
    8081 ; dph_store_: dph_reg p → val → regsT → res regsT
    8182 ; dph_retrieve_: regsT → dph_reg p → res val
     83 ; pair_reg_move_: regsT → pair_reg p → regsT
    8284 }.
    8385
     
    100102 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
    101103
    102 (*
    103 definition set_carry: val → state → state ≝
    104  λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
    105 *)
     104definition set_carry: ∀p. val → state p → state p ≝
     105 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
    106106
    107107definition set_pc: ∀p. address → state p → state p ≝
    108108 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
     109
     110definition set_frms: ∀p. framesT p → state p → state p ≝
     111 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
    109112
    110113(* CSC: was build_state in RTL *)
     
    157160 λp,st,dst.dph_retrieve_ … (regs … st) dst.
    158161
    159 (*
    160 definition save_frame: state → state ≝ λst.st. (* CSC *)
    161 
    162 axiom FailedPopFrame: String.
    163 *)
     162definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
     163 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
     164
     165definition save_frame: ∀p:sem_params. state p → state p ≝
     166 λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
    164167
    165168(* removes the top frame from the frames list *)
     
    191194   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    192195
    193 (*
    194 definition save_ra : state → label → res state ≝
    195  λst,l.
    196   let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
     196definition save_ra : ∀p. state p → label → res (state p) ≝
     197 λp,st,l.
     198  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
    197199  (* No monadic notation here *)
    198   bind ?? (push st addrl) (λst.push st addrh).
    199 
     200  bind ?? (push … st addrl) (λst.push … st addrh).
     201
     202(*
    200203(*CSC: unused now
    201204definition fetch_ra : state → res (state × label) ≝
     
    211214axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
    212215axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
    213 
    214 definition init_locals : list register → register_env val ≝
     216*)
     217
     218definition init_locals : ∀p.list register → regsT p ≝
    215219foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    216220
     221(*
    217222definition reg_store ≝
    218223λreg,v,locals. update RegisterTag val locals reg v.
     
    222227definition reg_retrieve : register_env val → register → res val ≝
    223228λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
     229*)
    224230
    225231axiom MissingSymbol : String.
    226 *)
     232
    227233axiom FailedLoad : String.
    228 (*
     234
    229235axiom BadFunction : String.
    230236
     237(*
    231238(*CSC: to be implemented *)
    232239axiom fetch_external_args: external_function → state → res (list val).(* ≝
     
    286293  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
    287294  OK ? (set_regs regs st))).
    288 
    289 (*
    290 (* CSC: completely different because different type for registers_move *)
    291 definition retrieve: state → registers_move → res val ≝
    292   λst.
    293   λr.
    294   match r with
    295   [ pseudo   src ⇒ reg_retrieve (locals st) src
    296   | from_acc src ⇒ hwreg_retrieve (regs st) src
    297   ].
    298 
    299 definition store ≝
    300   λst.
    301   λv.
    302   λr.
    303   match r with
    304   [ pseudo   dst ⇒
    305     ! locals ← reg_store dst v (locals st);
    306       ret ? (set_locals locals st)
    307   | hardware dst ⇒
    308     ! regs ← hwreg_store dst v (regs st);
    309       ret ? (set_regs regs st)
    310   ].
    311 *)
    312295*)
    313296
     
    333316        ! st ← acca_store … dst v st;
    334317          ret ? 〈E0, goto … l st〉
    335 (*      | joint_instr_store addrl addrh src ⇒
    336         ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
    337         ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
     318      | joint_instr_store addrl addrh src ⇒
     319        ! vaddrh ← dph_retrieve … st addrh;
     320        ! vaddrl ← dpl_retrieve … st addrl;
    338321        ! vaddr ← smerge vaddrl vaddrh;
    339         ! v ← hwreg_retrieve (regs st) src; (*CSC*)
    340         ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    341           ret ? 〈E0, goto l (set_m m' st)〉
     322        ! v ← acca_retrieve … st src;
     323        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     324          ret ? 〈E0, goto … l (set_m … m' st)〉
    342325      | joint_instr_cond src ltrue ⇒
    343         ! v ← hwreg_retrieve (regs st) src; (*CSC*)
     326        ! v ← acca_retrieve … st src;
    344327        ! b ← eval_bool_of_val v;
    345           ret ? 〈E0, goto (if b then ltrue else l) st〉
     328          ret ? 〈E0, goto (if b then ltrue else l) st〉
    346329      | joint_instr_address ident prf ldest hdest ⇒
    347330        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    348331          let 〈laddr,haddr〉 ≝ represent_block addr in
    349         ! locals ← reg_store ldest laddr (locals st);
    350         ! locals ← reg_store hdest haddr locals;
    351           ret ? 〈E0, goto l (set_locals locals st)
     332        ! st ← dpl_store … ldest laddr st;
     333        ! st ← dph_store … hdest haddr st;
     334          ret ? 〈E0, goto … l st
    352335      | joint_instr_op1 op acc_a ⇒
    353         ! v ← reg_retrieve (locals st) acc_a;
     336        ! v ← acca_retrieve … st acc_a;
    354337        ! v ← Byte_of_val v;
    355338          let v' ≝ val_of_Byte (op1 eval op v) in
    356         ! locals ← reg_store acc_a v' (locals st);
    357           ret ? 〈E0, goto l (set_locals locals st)
    358       | joint_instr_op2 op acc_a_reg dest
    359         ! v1 ← reg_retrieve (locals st) acc_a_reg;
     339        ! st ← acca_store … acc_a v' st;
     340          ret ? 〈E0, goto … l st
     341      | joint_instr_op2 op acc_a src
     342        ! v1 ← acca_retrieve … st acc_a;
    360343        ! v1 ← Byte_of_val v1;
    361         ! v2 ← reg_retrieve (locals st) acc_a_reg;
     344        ! v2 ← greg_retrieve … src;
    362345        ! v2 ← Byte_of_val v2;
    363         ! carry ← eval_bool_of_val (carry st);
     346        ! carry ← eval_bool_of_val (carry st);
    364347          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    365348          let v' ≝ val_of_Byte v' in
    366349          let carry ≝ of_bool carry in
    367         ! locals ← reg_store dest v' (locals st);
    368           ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    369       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
    370       | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     350        ! st ← acca_store … acc_a v' st;
     351          ret ? 〈E0, goto … l (set_carry … carry st)〉
     352      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vfalse st)〉
     353      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue st)〉
    371354      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    372         ! v1 ← reg_retrieve (locals st) acc_a_reg;
     355        ! v1 ← acca_retrieve … st acc_a_reg;
    373356        ! v1 ← Byte_of_val v1;
    374         ! v2 ← reg_retrieve (locals st) acc_b_reg;
     357        ! v2 ← accb_retrieve … st acc_b_reg;
    375358        ! v2 ← Byte_of_val v2;
    376359          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    377360          let v1' ≝ val_of_Byte v1' in
    378361          let v2' ≝ val_of_Byte v2' in
    379         ! locals ← reg_store acc_a_reg v1' (locals st);
    380         ! locals ← reg_store acc_b_reg v2' locals;
    381           ret ? 〈E0, goto l (set_locals locals st)
     362        ! st ← acca_store … acc_a_reg v1' st;
     363        ! st ← accb_store … acc_b_reg v2' st;
     364          ret ? 〈E0, goto … l st
    382365      | joint_instr_pop dst ⇒
    383         ! 〈st,v〉 ← pop st;
    384         ! locals ← reg_store dst (val_of_Byte v) (locals st);
    385           ret ? 〈E0, goto l (set_locals locals st)
     366        ! 〈st,v〉 ← pop st;
     367        ! st ← acca_store … dst (val_of_Byte v) st;
     368          ret ? 〈E0, goto … l st
    386369      | joint_instr_push src ⇒
    387         ! v ← reg_retrieve (locals st) src;
     370        ! v ← acca_retrieve … st src;
    388371        ! v ← Byte_of_val v;
    389         ! st ← push st v;
    390           ret ? 〈E0, goto l st〉
     372        ! st ← push st v;
     373          ret ? 〈E0, goto l st〉
    391374      | joint_instr_move dst_src ⇒
    392         let 〈dst, src〉 ≝ dst_src in
    393         ! v ← retrieve st src;
    394         ! st ← store st v dst;
    395           ret ? 〈E0, goto l st〉
     375          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
    396376      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
    397377        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    400380          [ Internal fn ⇒
    401381            ! st ← save_ra st l;
    402               let st ≝ save_frame st in
    403               let locals ≝ init_locals (ertl_if_locals globals fn) in
     382              let st ≝ save_frame st in
     383              let regs ≝ init_locals … (ertl_if_locals globals fn) in
    404384              let l' ≝ ertl_if_entry globals fn in
    405               ret ? 〈 E0, goto l' (set_locals locals st)〉
     385              ret ? 〈 E0, goto … l' (set_regs … regs st)〉
    406386          | External fn ⇒
    407387            ! params ← fetch_external_args fn st;
     
    413393            ! st ← set_result vs st;
    414394              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    415 *)
    416           | _ ⇒ ?
    417395          ]
     396      ]
    418397    | joint_st_return ⇒
    419398      ! st ← pop_frame … st;
Note: See TracChangeset for help on using the changeset viewer.