Changeset 1161 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (9 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1156 r1161  
    4949axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    5050
    51 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
    5252
    5353(* CSC: frame reduced to this *)
     
    137137
    138138(*CSC: To be implemented *)
     139
     140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    139141axiom fetch_function: state → res ertl_internal_function.
    140 axiom fetch_statement: state → res ertl_statement.
    141142
    142143definition init_locals : list register → register_env val ≝
     
    212213  OK ? (set_regs regs st))).
    213214
    214 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    215 λge,st.
    216   ! s ← fetch_statement st;
     215definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
     216  λglobals. λge,st.
     217  ! s ← fetch_statement globals st;
    217218  match s with
    218   [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
    219   | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
    220   | ertl_st_int dest v l ⇒
    221      ! locals ← reg_store dest (val_of_Byte v) (locals st);
    222      ret ? 〈E0, goto l (set_locals locals st)〉
    223   | ertl_st_load addrl addrh dst l ⇒
    224       ! vaddrh ← reg_retrieve (locals st) addrh;
    225       ! vaddrl ← reg_retrieve (locals st) addrl;
    226       ! vaddr ← smerge vaddrl vaddrh;
    227       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    228       ! locals ← reg_store dst v (locals st);
    229       ret ? 〈E0, goto l (set_locals locals st)〉
    230   | ertl_st_store addrl addrh src l ⇒
    231       ! vaddrh ← reg_retrieve (locals st) addrh;
    232       ! vaddrl ← reg_retrieve (locals st) addrl;
    233       ! vaddr ← smerge vaddrl vaddrh;
    234       ! v ← reg_retrieve (locals st) src;
    235       ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    236       ret ? 〈E0, goto l (set_m m' st)〉
    237   | ertl_st_cond src ltrue lfalse ⇒
    238       ! v ← reg_retrieve (locals st) src;
    239       ! b ← eval_bool_of_val v;
    240       ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    241   | ertl_st_addr ldest hdest id l ⇒
    242      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    243      let 〈laddr,haddr〉 ≝ represent_block addr in
    244      ! locals ← reg_store ldest laddr (locals st);
    245      ! locals ← reg_store hdest haddr locals;
    246      ret ? 〈E0, goto l (set_locals locals st)〉
    247   | ertl_st_op1 op dst src l ⇒
    248      ! v ← reg_retrieve (locals st) src;
    249      ! v ← Byte_of_val v;
    250      let v' ≝ val_of_Byte (op1 eval op v) in
    251      ! locals ← reg_store dst v' (locals st);
    252      ret ? 〈E0, goto l (set_locals locals st)〉
    253   | ertl_st_op2 op dst src1 src2 l ⇒
    254      ! v1 ← reg_retrieve (locals st) src1;
    255      ! v1 ← Byte_of_val v1;
    256      ! v2 ← reg_retrieve (locals st) src2;
    257      ! v2 ← Byte_of_val v2;
    258      ! carry ← eval_bool_of_val (carry st);
    259      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    260      let v' ≝ val_of_Byte v' in
    261      let carry ≝ of_bool carry in
    262      ! locals ← reg_store dst v' (locals st);
    263      ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    264   | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    265      ! v1 ← reg_retrieve (locals st) sacc;
    266      ! v1 ← Byte_of_val v1;
    267      ! v2 ← reg_retrieve (locals st) sbacc;
    268      ! v2 ← Byte_of_val v2;
    269      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    270      let v1' ≝ val_of_Byte v1' in
    271      let v2' ≝ val_of_Byte v2' in
    272      ! locals ← reg_store dacc v1' (locals st);
    273      ! locals ← reg_store dbacc v2' locals;
    274      ret ? 〈E0, goto l (set_locals locals st)〉
    275   | ertl_st_clear_carry l ⇒
    276     ret ? 〈E0, goto l (set_carry Vfalse st)〉
    277   | ertl_st_set_carry l ⇒
    278     ret ? 〈E0, goto l (set_carry Vtrue st)〉
    279      
    280   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    281          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    282          be more than enough... *)
    283   | ertl_st_move dst src l ⇒
    284      ! v ← reg_retrieve (locals st) src;
    285      ! locals ← reg_store dst v (locals st);
    286      ret ? 〈E0, goto l (set_locals locals st)〉
    287   | ertl_st_hdw_to_hdw dst src l ⇒
    288      ! v ← hwreg_retrieve (regs st) src;
    289      ! regs ← hwreg_store dst v (regs st);
    290      ret ? 〈E0, goto l (set_regs regs st)〉
     219  [ ertl_st_lift_pre pre ⇒
     220    match pre with
     221    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
     222    | joint_st_sequential seq l ⇒
     223      match seq with
     224      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
     225      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
     226      | joint_instr_int dest v ⇒
     227        ! locals ← reg_store dest (val_of_Byte v) (locals st);
     228          ret ? 〈E0, goto l (set_locals locals st)〉
     229      | joint_instr_load addrl addrh dst ⇒
     230        ! vaddrh ← reg_retrieve (locals st) addrh;
     231        ! vaddrl ← reg_retrieve (locals st) addrl;
     232        ! vaddr ← smerge vaddrl vaddrh;
     233        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
     234        ! locals ← reg_store dst v (locals st);
     235          ret ? 〈E0, goto l (set_locals locals st)〉
     236      | joint_instr_store addrl addrh src ⇒
     237        ! vaddrh ← reg_retrieve (locals st) addrh;
     238        ! vaddrl ← reg_retrieve (locals st) addrl;
     239        ! vaddr ← smerge vaddrl vaddrh;
     240        ! v ← reg_retrieve (locals st) src;
     241        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     242          ret ? 〈E0, goto l (set_m m' st)〉
     243      | joint_instr_cond src ltrue ⇒
     244        ! v ← reg_retrieve (locals st) src;
     245        ! b ← eval_bool_of_val v;
     246          ret ? 〈E0, goto (if b then ltrue else l) st〉
     247      | joint_instr_address ident prf ldest hdest ⇒
     248        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     249          let 〈laddr,haddr〉 ≝ represent_block addr in
     250        ! locals ← reg_store ldest laddr (locals st);
     251        ! locals ← reg_store hdest haddr locals;
     252          ret ? 〈E0, goto l (set_locals locals st)〉
     253      | joint_instr_op1 op acc_a ⇒
     254        ! v ← reg_retrieve (locals st) acc_a;
     255        ! v ← Byte_of_val v;
     256          let v' ≝ val_of_Byte (op1 eval op v) in
     257        ! locals ← reg_store acc_a v' (locals st);
     258          ret ? 〈E0, goto l (set_locals locals st)〉
     259      | joint_instr_op2 op acc_a_reg dest ⇒
     260        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     261        ! v1 ← Byte_of_val v1;
     262        ! v2 ← reg_retrieve (locals st) acc_a_reg;
     263        ! v2 ← Byte_of_val v2;
     264        ! carry ← eval_bool_of_val (carry st);
     265          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     266          let v' ≝ val_of_Byte v' in
     267          let carry ≝ of_bool carry in
     268        ! locals ← reg_store dest v' (locals st);
     269          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
     270      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
     271      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     272      | joint_instr_hdw_to_hdw dst_src ⇒
     273          let 〈dst, src〉 ≝ dst_src in
     274        ! v ← hwreg_retrieve (regs st) src;
     275        ! regs ← hwreg_store dst v (regs st);
     276          ret ? 〈E0, goto l (set_regs regs st)〉
     277(* XXX: examine: where is the result being stored?
     278      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
     279        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     280        ! v1 ← Byte_of_val v1;
     281        ! v2 ← reg_retrieve (locals st) acc_b_reg;
     282        ! v2 ← Byte_of_val v2;
     283          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     284          let v1' ≝ val_of_Byte v1' in
     285          let v2' ≝ val_of_Byte v2' in
     286        ! locals ← reg_store dacc v1' (locals st);
     287        ! locals ← reg_store dbacc v2' locals;
     288          ret ? 〈E0, goto l (set_locals locals st)〉
     289*)
     290      | joint_instr_pop dst ⇒
     291        ! 〈st,v〉 ← pop st;
     292        ! locals ← reg_store dst (val_of_Byte v) (locals st);
     293          ret ? 〈E0, goto l (set_locals locals st)〉
     294      | joint_instr_push src ⇒
     295        ! v ← reg_retrieve (locals st) src;
     296        ! v ← Byte_of_val v;
     297        ! st ← push st v;
     298          ret ? 〈E0, goto l st〉
     299      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     300        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     301        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     302          match fd with
     303          [ Internal fn ⇒
     304            ! st ← save_ra st l;
     305              let st ≝ save_frame st in
     306              let locals ≝ init_locals (ertl_if_locals fn) in
     307              let l' ≝ ertl_if_entry fn in
     308              ret ? 〈 E0, goto l' (set_locals locals st)〉
     309          | External fn ⇒
     310            ! params ← fetch_external_args fn st;
     311            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     312            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     313            (* CSC: XXX bug here; I think I should split it into Byte-long
     314               components; instead I am making a singleton out of it *)
     315              let vs ≝ [mk_val ? evres] in
     316            ! st ← set_result vs st;
     317              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     318      ]
     319      | _ ⇒ ?
     320      ]
     321    | joint_st_return ⇒
     322      ! st ← pop_frame st;
     323      ! 〈st,pch〉 ← pop st;
     324      ! 〈st,pcl〉 ← pop st;
     325        let pc ≝ address_of_address_chunks pcl pch in
     326        ret ? 〈E0,set_pc pc st〉
     327    | _ ⇒ ?
     328    ]
    291329  | ertl_st_get_hdw dst src l ⇒
    292330     ! v ← hwreg_retrieve (regs st) src;
     
    297335     ! regs ← hwreg_store dst v (regs st);
    298336     ret ? 〈E0, goto l (set_regs regs st)〉
     337  | ertl_st_new_frame _ ⇒ ?
     338  | ertl_st_del_frame _ ⇒ ?
     339  | ertl_st_frame_size _ _ ⇒ ?
     340  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
     341         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
     342         be more than enough... *)
     343  | ertl_st_move dst src l ⇒
     344     ! v ← reg_retrieve (locals st) src;
     345     ! locals ← reg_store dst v (locals st);
     346     ret ? 〈E0, goto l (set_locals locals st)〉
     347  ].
     348 
     349 
     350  match s with
    299351
    300352  (* CSC: Dropped:
     
    304356     
    305357  (* CSC: changed, where the meat is *)
    306   | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    307       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    308       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    309       match fd with
    310       [ Internal fn ⇒
    311         ! st ← save_ra st l;
    312         let st ≝ save_frame st in
    313         let locals ≝ init_locals (ertl_if_locals fn) in
    314         let l' ≝ ertl_if_entry fn in
    315          ret ? 〈 E0, goto l' (set_locals locals st)〉
    316       | External fn ⇒
    317         ! params ← fetch_external_args fn st;
    318         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    319         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    320         (* CSC: XXX bug here; I think I should split it into Byte-long
    321            components; instead I am making a singleton out of it *)
    322         let vs ≝ [mk_val ? evres] in
    323         ! st ← set_result vs st;
    324         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    325       ]
    326   | ertl_st_return ⇒
    327       ! st ← pop_frame st;
    328       ! 〈st,pch〉 ← pop st;
    329       ! 〈st,pcl〉 ← pop st;
    330       let pc ≝ address_of_address_chunks pcl pch in
    331       ret ? 〈E0,set_pc pc st〉
    332358 
    333359  (* CSC: new stuff *)
    334360  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    335   | ertl_st_new_frame l ⇒
    336      ! v ← framesize st;
    337      ! sp ← get_hwsp st;
    338      let newsp ≝ addr_sub sp v in
    339      ! st ← set_hwsp newsp st;
    340      ret ? 〈E0,goto l st〉
    341   | ertl_st_del_frame l ⇒
    342      ! v ← framesize st;
    343      ! sp ← get_hwsp st;
    344      let newsp ≝ addr_add sp v in
    345      ! st ← set_hwsp newsp st;
    346      ret ? 〈E0,goto l st〉
    347   | ertl_st_frame_size dst l ⇒
    348      ! v ← framesize st;
    349      ! locals ← reg_store dst (val_of_nat v) (locals st);
    350      ret ? 〈E0, goto l (set_locals locals st)〉
    351   | ertl_st_pop dst l ⇒
    352      ! 〈st,v〉 ← pop st;
    353      ! locals ← reg_store dst (val_of_Byte v) (locals st);
    354      ret ? 〈E0, goto l (set_locals locals st)〉
    355   | ertl_st_push src l ⇒
    356      ! v ← reg_retrieve (locals st) src;
    357      ! v ← Byte_of_val v;
    358      ! st ← push st v;
    359      ret ? 〈E0, goto l st〉
    360   ].
     361<<<<<<< .mine  ].
    361362
    362363axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.