Changeset 1289


Ignore:
Timestamp:
Oct 4, 2011, 1:57:19 AM (8 years ago)
Author:
sacerdot
Message:

semantics ported to latest Joint version

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1281 r1289  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record more_sem_params (p:params1): Type[1] ≝
     19record more_sem_params (p:params_): Type[1] ≝
    2020 { framesT: Type[0]
    2121 ; regsT: Type[0]
     
    3636 ; pair_reg_move_: regsT → pair_reg p → regsT
    3737 
    38  ; init_locals : localsT p → regsT
    3938 ; pointer_of_label: label → Σp:pointer. ptype p = Code
    4039 }.
     
    5857record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    5958 { more_sparams:> more_sem_params p
     59
     60 ; init_locals : localsT p → regsT … more_sparams
    6061 
    6162 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     
    203204  ! s ← fetch_statement … st;
    204205  match s with
    205     [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
    206     | joint_st_sequential seq l ⇒
     206    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     207    | sequential seq l ⇒
    207208      match seq with
    208       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, next … l st〉
    209       | joint_instr_comment c ⇒ ret ? 〈E0, next … l st〉
    210       | joint_instr_int dest v ⇒
    211         ! st ← greg_store ? dest (BVByte v) st;
    212           ret ? 〈E0, next … l st〉
    213       | joint_instr_load dst addrl addrh ⇒
     209      [ extension c ⇒ exec_extended … p ge c st
     210      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
     211      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
     212      | INT dest v ⇒
     213        ! st ← greg_store p dest (BVByte v) st;
     214          ret ? 〈E0, next … l st〉
     215      | LOAD dst addrl addrh ⇒
    214216        ! vaddrh ← dph_retrieve … st addrh;
    215217        ! vaddrl ← dpl_retrieve … st addrl;
    216218        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
    217219        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    218         ! st ← acca_store … dst v st;
    219           ret ? 〈E0, next … l st〉
    220       | joint_instr_store addrl addrh src ⇒
     220        ! st ← acca_store p … dst v st;
     221          ret ? 〈E0, next … l st〉
     222      | STORE addrl addrh src ⇒
    221223        ! vaddrh ← dph_retrieve … st addrh;
    222224        ! vaddrl ← dpl_retrieve … st addrl;
     
    225227        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    226228          ret ? 〈E0, next … l (set_m … m' st)〉
    227       | joint_instr_cond src ltrue ⇒
     229      | COND src ltrue ⇒
    228230        ! v ← acca_retrieve … st src;
    229231        ! b ← bool_of_beval v;
    230232          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
    231       | joint_instr_address ident prf ldest hdest ⇒
     233      | ADDRESS ident prf ldest hdest ⇒
    232234        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    233235        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
    234         ! st ← dpl_store ldest laddr st;
    235         ! st ← dph_store hdest haddr st;
    236           ret ? 〈E0, next … l st〉
    237       | joint_instr_op1 op acc_a ⇒
    238         ! v ← acca_retrieve … st acc_a;
     236        ! st ← dpl_store p ldest laddr st;
     237        ! st ← dph_store p hdest haddr st;
     238          ret ? 〈E0, next … l st〉
     239      | OP1 op dacc_a sacc_a ⇒
     240        ! v ← acca_retrieve … st sacc_a;
    239241        ! v ← Byte_of_val v;
    240242          let v' ≝ BVByte (op1 eval op v) in
    241         ! st ← acca_store acc_a v' st;
    242           ret ? 〈E0, next … l st〉
    243       | joint_instr_op2 op acc_a src ⇒
    244         ! v1 ← acca_retrieve … st acc_a;
     243        ! st ← acca_store p dacc_a v' st;
     244          ret ? 〈E0, next … l st〉
     245      | OP2 op dacc_a sacc_a src ⇒
     246        ! v1 ← acca_retrieve … st sacc_a;
    245247        ! v1 ← Byte_of_val v1;
    246248        ! v2 ← greg_retrieve … st src;
     
    250252          let v' ≝ BVByte v' in
    251253          let carry ≝ beval_of_bool carry in
    252         ! st ← acca_store acc_a v' st;
     254        ! st ← acca_store p dacc_a v' st;
    253255          ret ? 〈E0, next … l (set_carry … carry st)〉
    254       | joint_instr_clear_carry ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
    255       | joint_instr_set_carry ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
    256       | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    257         ! v1 ← acca_retrieve … st acc_a_reg;
     256      | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
     257      | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
     258      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     259        ! v1 ← acca_retrieve … st sacc_a_reg;
    258260        ! v1 ← Byte_of_val v1;
    259         ! v2 ← accb_retrieve … st acc_b_reg;
     261        ! v2 ← accb_retrieve … st sacc_b_reg;
    260262        ! v2 ← Byte_of_val v2;
    261263          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    262264          let v1' ≝ BVByte v1' in
    263265          let v2' ≝ BVByte v2' in
    264         ! st ← acca_store acc_a_reg v1' st;
    265         ! st ← accb_store acc_b_reg v2' st;
    266           ret ? 〈E0, next … l st〉
    267       | joint_instr_pop dst ⇒
     266        ! st ← acca_store p dacc_a_reg v1' st;
     267        ! st ← accb_store p dacc_b_reg v2' st;
     268          ret ? 〈E0, next … l st〉
     269      | POP dst ⇒
    268270        ! 〈st,v〉 ← pop … st;
    269         ! st ← acca_store dst v st;
    270           ret ? 〈E0, next … l st〉
    271       | joint_instr_push src ⇒
     271        ! st ← acca_store p dst v st;
     272          ret ? 〈E0, next … l st〉
     273      | PUSH src ⇒
    272274        ! v ← acca_retrieve … st src;
    273275        ! st ← push … st v;
    274276          ret ? 〈E0, next … l st〉
    275       | joint_instr_move dst_src ⇒
     277      | MOVE dst_src ⇒
    276278          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
    277       | joint_instr_call_id id argsno ⇒
     279      (*CSC: XXX bug here dest unused *)
     280      | CALL_ID id argsno dest ⇒
    278281        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    279282        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     
    282285            ! st ← save_ra … st l;
    283286              let st ≝ save_frame … st in
    284               let regs ≝ init_locals (sem_params_of_sem_params2 globals p) … (joint_if_locals … fn) in
     287              let regs ≝ init_locals … (joint_if_locals … fn) in
    285288              let l' ≝ joint_if_entry … fn in
    286              ret ? 〈 E0, goto … l' (set_regs regs st)〉
     289             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
    287290          | External fn ⇒
    288291            ! params ← fetch_external_args … fn st;
     
    295298              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
    296299          ]]
    297     | joint_st_return
     300    | RETURN
    298301      ! st ← pop_frame … st;
    299302      ! 〈st,pch〉 ← pop … st;
    300303      ! 〈st,pcl〉 ← pop … st;
    301         ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
    302     | joint_st_extension c ⇒ exec_extended … p ge c st ].
     304        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
    303305cases addr //
    304306qed.
     
    308310  do s ← fetch_statement … st;
    309311  match s with
    310    [ joint_st_return
     312   [ RETURN
    311313      do 〈st,l〉 ← fetch_ra … st;
    312314      if eq_address l exit then
Note: See TracChangeset for help on using the changeset viewer.