Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (10 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

    r1153 r1197  
    2121(* CSC: ???????????? *)
    2222axiom smerge: val → val → res val.
    23 (*
    2423(* CSC: ???????????? In OCaml: IntValue.Int32.merge
    2524   Note also that the translation can fail; so it should be a res int! *)
    2625axiom smerge2: list val → int.
    27 *)
    2826(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2927axiom val_of_Byte: Byte → val.
    3028axiom Byte_of_val: val → res Byte.
     29axiom val_of_nat: nat → val.
    3130(* Map from the front-end memory model to the back-end memory model *)
    3231axiom represent_block: block → val × val.
     
    3837axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    3938axiom address_of_val: val → address. (* CSC: only to shift the sp *)
     39axiom addr_sub: address → nat → address.
     40axiom addr_add: address → nat → address.
    4041(* CSC: ??? *)
    4142axiom address_of_label: mem → label → address.
     
    4344axiom label_of_address_chunks: Byte → Byte → label.
    4445axiom address_of_address_chunks: Byte → Byte → address.
     46axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    4547axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4648axiom hwreg_retrieve : mRegisterMap → Register → res val.
    4749axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    4850
    49 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
    5052
    5153(* CSC: frame reduced to this *)
    5254definition frame: Type[0] ≝ register_env val.
    5355
     56(* CSC: exit not put in the state, like in OCaml. It is constant througout
     57   execution *)
    5458record state : Type[0] ≝
    5559 { st_frms: list frame
    5660 ; pc: address
    5761 ; sp: address
    58 (* ; exit: address *)
    5962 ; locals: register_env val
    6063 ; carry: val
     
    134137
    135138(*CSC: To be implemented *)
    136 axiom fetch_statement: state → res ertl_statement.
     139
     140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
     141axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
    137142
    138143definition init_locals : list register → register_env val ≝
     
    142147λreg,v,locals. update RegisterTag val locals reg v.
    143148
    144 (*
    145 axiom WrongNumberOfParameters : String.
    146 
    147 (* CSC: modified to take in input a list of registers (untyped) *)
    148 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    149 match rs with
    150 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    151 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    152   let locals' ≝ add RegisterTag val locals r v in
    153   params_store rst vst locals'
    154 ] ].
    155 *)
    156 
    157149axiom BadRegister : String.
    158150
     
    160152λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    161153
    162 (*
    163 axiom FailedOp : String.
    164 *)
    165154axiom MissingSymbol : String.
    166 (*
    167 axiom MissingStatement : String.
    168 axiom FailedConstant : String. *)
    169155axiom FailedLoad : String.
    170156axiom BadFunction : String.
    171 (*axiom BadJumpTable : String.
    172 axiom BadJumpValue : String.
    173 axiom FinalState : String.
    174 axiom ReturnMismatch : String.
    175 *)
    176157
    177158(*CSC: to be implemented *)
     
    200181  (λregs.OK ? (set_regs regs st)).
    201182
    202 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    203 λge,st.
    204   ! s ← fetch_statement st;
     183definition fetch_result: state → nat → res (list val) ≝
     184 λst,registersno.
     185  let retregs ≝ prefix … registersno RegisterRets in
     186  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
     187
     188definition framesize: list ident → state → res nat ≝
     189  λglobals: list ident.
     190  λst.
     191  (* CSC: monadic notation missing here *)
     192    bind ?? (fetch_function globals st) (λf.
     193    OK ? (ertl_if_stacksize globals f)).
     194
     195definition get_hwsp : state → res address ≝
     196 λst.
     197  (* CSC: monadic notation missing here *)
     198  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
     199  (* CSC: monadic notation missing here *)
     200  bind ?? (Byte_of_val spl) (λspl.
     201  (* CSC: monadic notation missing here *)
     202  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
     203  (* CSC: monadic notation missing here *)
     204  bind ?? (Byte_of_val sph) (λsph.
     205  OK ? (address_of_address_chunks spl sph))))).
     206
     207definition set_hwsp : address → state → res state ≝
     208 λsp,st.
     209  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
     210  (* CSC: monadic notation missing here *) 
     211  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
     212  (* CSC: monadic notation missing here *) 
     213  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
     214  OK ? (set_regs regs st))).
     215
     216definition retrieve: state → move_registers → res val ≝
     217  λst.
     218  λr.
     219  match r with
     220  [ pseudo   src ⇒ reg_retrieve (locals st) src
     221  | hardware src ⇒ hwreg_retrieve (regs st) src
     222  ].
     223
     224definition store ≝
     225  λst.
     226  λv.
     227  λr.
     228  match r with
     229  [ pseudo   dst ⇒
     230    ! locals ← reg_store dst v (locals st);
     231      ret ? (set_locals locals st)
     232  | hardware dst ⇒
     233    ! regs ← hwreg_store dst v (regs st);
     234      ret ? (set_regs regs st)
     235  ].
     236
     237definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
     238  λglobals. λge,st.
     239  ! s ← fetch_statement globals st;
    205240  match s with
    206   [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
    207   | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
    208   | ertl_st_int dest v l ⇒
    209      ! locals ← reg_store dest (val_of_Byte v) (locals st);
    210      ret ? 〈E0, goto l (set_locals locals st)〉
    211   | ertl_st_load addrl addrh dst l ⇒
    212       ! vaddrh ← reg_retrieve (locals st) addrh;
    213       ! vaddrl ← reg_retrieve (locals st) addrl;
    214       ! vaddr ← smerge vaddrl vaddrh;
    215       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    216       ! locals ← reg_store dst v (locals st);
     241  [ ertl_st_lift_pre pre ⇒
     242    match pre with
     243    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
     244    | joint_st_sequential seq l ⇒
     245      match seq with
     246      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
     247      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
     248      | joint_instr_int dest v ⇒
     249        ! locals ← reg_store dest (val_of_Byte v) (locals st);
     250          ret ? 〈E0, goto l (set_locals locals st)〉
     251      | joint_instr_load addrl addrh dst ⇒
     252        ! vaddrh ← reg_retrieve (locals st) addrh;
     253        ! vaddrl ← reg_retrieve (locals st) addrl;
     254        ! vaddr ← smerge vaddrl vaddrh;
     255        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
     256        ! locals ← reg_store dst v (locals st);
     257          ret ? 〈E0, goto l (set_locals locals st)〉
     258      | joint_instr_store addrl addrh src ⇒
     259        ! vaddrh ← reg_retrieve (locals st) addrh;
     260        ! vaddrl ← reg_retrieve (locals st) addrl;
     261        ! vaddr ← smerge vaddrl vaddrh;
     262        ! v ← reg_retrieve (locals st) src;
     263        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     264          ret ? 〈E0, goto l (set_m m' st)〉
     265      | joint_instr_cond src ltrue ⇒
     266        ! v ← reg_retrieve (locals st) src;
     267        ! b ← eval_bool_of_val v;
     268          ret ? 〈E0, goto (if b then ltrue else l) st〉
     269      | joint_instr_address ident prf ldest hdest ⇒
     270        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     271          let 〈laddr,haddr〉 ≝ represent_block addr in
     272        ! locals ← reg_store ldest laddr (locals st);
     273        ! locals ← reg_store hdest haddr locals;
     274          ret ? 〈E0, goto l (set_locals locals st)〉
     275      | joint_instr_op1 op acc_a ⇒
     276        ! v ← reg_retrieve (locals st) acc_a;
     277        ! v ← Byte_of_val v;
     278          let v' ≝ val_of_Byte (op1 eval op v) in
     279        ! locals ← reg_store acc_a v' (locals st);
     280          ret ? 〈E0, goto l (set_locals locals st)〉
     281      | joint_instr_op2 op acc_a_reg dest ⇒
     282        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     283        ! v1 ← Byte_of_val v1;
     284        ! v2 ← reg_retrieve (locals st) acc_a_reg;
     285        ! v2 ← Byte_of_val v2;
     286        ! carry ← eval_bool_of_val (carry st);
     287          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     288          let v' ≝ val_of_Byte v' in
     289          let carry ≝ of_bool carry in
     290        ! locals ← reg_store dest v' (locals st);
     291          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
     292      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
     293      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     294      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
     295        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     296        ! v1 ← Byte_of_val v1;
     297        ! v2 ← reg_retrieve (locals st) acc_b_reg;
     298        ! v2 ← Byte_of_val v2;
     299          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     300          let v1' ≝ val_of_Byte v1' in
     301          let v2' ≝ val_of_Byte v2' in
     302        ! locals ← reg_store acc_a_reg v1' (locals st);
     303        ! locals ← reg_store acc_b_reg v2' locals;
     304          ret ? 〈E0, goto l (set_locals locals st)〉
     305      | joint_instr_pop dst ⇒
     306        ! 〈st,v〉 ← pop st;
     307        ! locals ← reg_store dst (val_of_Byte v) (locals st);
     308          ret ? 〈E0, goto l (set_locals locals st)〉
     309      | joint_instr_push src ⇒
     310        ! v ← reg_retrieve (locals st) src;
     311        ! v ← Byte_of_val v;
     312        ! st ← push st v;
     313          ret ? 〈E0, goto l st〉
     314      | joint_instr_move dst_src ⇒
     315        let 〈dst, src〉 ≝ dst_src in
     316        ! v ← retrieve st src;
     317        ! st ← store st v dst;
     318          ret ? 〈E0, goto l st〉
     319      (* CSC: changed, where the meat is *)
     320      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     321        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     322        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     323          match fd with
     324          [ Internal fn ⇒
     325            ! st ← save_ra st l;
     326              let st ≝ save_frame st in
     327              let locals ≝ init_locals (ertl_if_locals globals fn) in
     328              let l' ≝ ertl_if_entry globals fn in
     329              ret ? 〈 E0, goto l' (set_locals locals st)〉
     330          | External fn ⇒
     331            ! params ← fetch_external_args fn st;
     332            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     333            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     334            (* CSC: XXX bug here; I think I should split it into Byte-long
     335               components; instead I am making a singleton out of it *)
     336              let vs ≝ [mk_val ? evres] in
     337            ! st ← set_result vs st;
     338              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     339          ]
     340      ]
     341    (* CSC: changed, where the meat is *)
     342    | joint_st_return ⇒
     343      ! st ← pop_frame st;
     344      ! 〈st,pch〉 ← pop st;
     345      ! 〈st,pcl〉 ← pop st;
     346        let pc ≝ address_of_address_chunks pcl pch in
     347        ret ? 〈E0,set_pc pc st〉
     348    | _ ⇒ ?
     349    ]
     350  | ertl_st_new_frame l ⇒
     351    ! v ← framesize globals st;
     352    ! sp ← get_hwsp st;
     353      let newsp ≝ addr_sub sp v in
     354    ! st ← set_hwsp newsp st;
     355      ret ? 〈E0,goto l st〉
     356  | ertl_st_del_frame l ⇒
     357    ! v ← framesize globals st;
     358    ! sp ← get_hwsp st;
     359      let newsp ≝ addr_add sp v in
     360    ! st ← set_hwsp newsp st;
     361      ret ? 〈E0,goto l st〉
     362  | ertl_st_frame_size dst l ⇒
     363    ! v ← framesize globals st;
     364    ! locals ← reg_store dst (val_of_nat v) (locals st);
    217365      ret ? 〈E0, goto l (set_locals locals st)〉
    218   | ertl_st_store addrl addrh src l ⇒
    219       ! vaddrh ← reg_retrieve (locals st) addrh;
    220       ! vaddrl ← reg_retrieve (locals st) addrl;
    221       ! vaddr ← smerge vaddrl vaddrh;
    222       ! v ← reg_retrieve (locals st) src;
    223       ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    224       ret ? 〈E0, goto l (set_m m' st)〉
    225   | ertl_st_cond src ltrue lfalse ⇒
    226       ! v ← reg_retrieve (locals st) src;
    227       ! b ← eval_bool_of_val v;
    228       ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    229   | ertl_st_addr ldest hdest id l ⇒
    230      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    231      let 〈laddr,haddr〉 ≝ represent_block addr in
    232      ! locals ← reg_store ldest laddr (locals st);
    233      ! locals ← reg_store hdest haddr locals;
    234      ret ? 〈E0, goto l (set_locals locals st)〉
    235   | ertl_st_op1 op dst src l ⇒
    236      ! v ← reg_retrieve (locals st) src;
    237      ! v ← Byte_of_val v;
    238      let v' ≝ val_of_Byte (op1 eval op v) in
    239      ! locals ← reg_store dst v' (locals st);
    240      ret ? 〈E0, goto l (set_locals locals st)〉
    241   | ertl_st_op2 op dst src1 src2 l ⇒
    242      ! v1 ← reg_retrieve (locals st) src1;
    243      ! v1 ← Byte_of_val v1;
    244      ! v2 ← reg_retrieve (locals st) src2;
    245      ! v2 ← Byte_of_val v2;
    246      ! carry ← eval_bool_of_val (carry st);
    247      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    248      let v' ≝ val_of_Byte v' in
    249      let carry ≝ of_bool carry in
    250      ! locals ← reg_store dst v' (locals st);
    251      ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    252   | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    253      ! v1 ← reg_retrieve (locals st) sacc;
    254      ! v1 ← Byte_of_val v1;
    255      ! v2 ← reg_retrieve (locals st) sbacc;
    256      ! v2 ← Byte_of_val v2;
    257      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    258      let v1' ≝ val_of_Byte v1' in
    259      let v2' ≝ val_of_Byte v2' in
    260      ! locals ← reg_store dacc v1' (locals st);
    261      ! locals ← reg_store dbacc v2' locals;
    262      ret ? 〈E0, goto l (set_locals locals st)〉
    263   | ertl_st_clear_carry l ⇒
    264     ret ? 〈E0, goto l (set_carry Vfalse st)〉
    265   | ertl_st_set_carry l ⇒
    266     ret ? 〈E0, goto l (set_carry Vtrue st)〉
    267      
    268   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    269          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    270          be more than enough... *)
    271   | ertl_st_move dst src l ⇒
    272      ! v ← reg_retrieve (locals st) src;
    273      ! locals ← reg_store dst v (locals st);
    274      ret ? 〈E0, goto l (set_locals locals st)〉
    275   | ertl_st_hdw_to_hdw dst src l ⇒
    276      ! v ← hwreg_retrieve (regs st) src;
    277      ! regs ← hwreg_store dst v (regs st);
    278      ret ? 〈E0, goto l (set_regs regs st)〉
    279   | ertl_st_get_hdw dst src l ⇒
    280      ! v ← hwreg_retrieve (regs st) src;
    281      ! locals ← reg_store dst v (locals st);
    282      ret ? 〈E0, goto l (set_locals locals st)〉
    283   | ertl_st_set_hdw dst src l ⇒
    284      ! v ← reg_retrieve (locals st) src;
    285      ! regs ← hwreg_store dst v (regs st);
    286      ret ? 〈E0, goto l (set_regs regs st)〉
    287 
    288366  (* CSC: Dropped:
    289367      - rtl_st_stackaddr (becomes two get_hdw)
    290368      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    291369      - rtl_st_call_ptr (unimplemented ATM) *)
     370  ].
    292371     
    293   (* CSC: changed, where the meat is *)
    294   | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    295       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    296       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    297       match fd with
    298       [ Internal fn ⇒
    299         ! st ← save_ra st l;
    300         let st ≝ save_frame st in
    301         let locals ≝ init_locals (ertl_if_locals fn) in
    302         let l' ≝ ertl_if_entry fn in
    303          ret ? 〈 E0, goto l' (set_locals locals st)〉
    304       | External fn ⇒
    305         ! params ← fetch_external_args fn st;
    306         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    307         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    308         (* CSC: XXX bug here; I think I should split it into Byte-long
    309            components; instead I am making a singleton out of it *)
    310         let vs ≝ [mk_val ? evres] in
    311         ! st ← set_result vs st;
    312         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     372axiom WrongReturnValueType: String.
     373
     374definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     375  λglobals: list ident.
     376  λexit.
     377  λregistersno.
     378  λst.
     379 (* CSC: monadic notation missing here *)
     380  match fetch_statement globals st with
     381  [ Error _ ⇒ None ?
     382  | OK s ⇒
     383    match s with
     384    [ ertl_st_lift_pre pre ⇒
     385      match pre with
     386      [ joint_st_return ⇒
     387        match fetch_ra st with
     388         [ Error _ ⇒ None ?
     389         | OK st_l ⇒
     390           let 〈st,l〉 ≝ st_l in
     391           match label_eq l exit with
     392           [ inl _ ⇒
     393             (* CSC: monadic notation missing here *)
     394             match fetch_result st registersno with
     395             [ Error _ ⇒ None ?
     396             | OK vals ⇒ Some ? (smerge2 vals)
     397             ]
     398           | inr _ ⇒ None ?
     399           ]
     400         ]
     401      | _ ⇒ None ?
    313402      ]
    314   | ertl_st_return ⇒
    315       ! st ← pop_frame st;
    316       ! 〈st,pch〉 ← pop st;
    317       ! 〈st,pcl〉 ← pop st;
    318       let pc ≝ address_of_address_chunks pcl pch in
    319       ret ? 〈E0,set_pc pc st〉
    320  
    321   (* CSC: new stuff *)
    322   | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    323   | ertl_st_new_frame _ ⇒ ?
    324   | ertl_st_del_frame _ ⇒ ?
    325   | ertl_st_frame_size _ _ ⇒ ?
    326   | ertl_st_pop dst l ⇒
    327      ! 〈st,v〉 ← pop st;
    328      ! locals ← reg_store dst (val_of_Byte v) (locals st);
    329      ret ? 〈E0, goto l (set_locals locals st)〉
    330   | ertl_st_push src l ⇒
    331      ! v ← reg_retrieve (locals st) src;
    332      ! v ← Byte_of_val v;
    333      ! st ← push st v;
    334      ret ? 〈E0, goto l st〉
     403    | _ ⇒ None ?
     404    ]
    335405  ].
    336406
    337 axiom WrongReturnValueType: String.
    338 
    339 definition is_final : state → option ((*CSC: why not res*) int) ≝
    340 λs. match s with
    341 [ State _ _ _ ⇒ None ?
    342 | Callstate _ _ _ _ _ ⇒ None ?
    343 | Returnstate v _ fs _ ⇒
    344     match fs with
    345      [ nil ⇒ Some ? (smerge2 v)
    346      | _ ⇒ None ? ]].
    347 
    348 definition RTL_exec : execstep io_out io_in ≝
    349   mk_execstep … ? is_final mem_of_state eval_statement.
     407definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
     408  λglobals.
     409  λexit.
     410  λregistersno.
     411  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    350412
    351413(* CSC: XXX the program type does not fit with the globalenv and init_mem
Note: See TracChangeset for help on using the changeset viewer.