Changeset 1381 for src/ERTL


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/ERTL/semantics.ma

    r1377 r1381  
    123123definition ertl_fullexec ≝
    124124 joint_fullexec … (λp. ertl_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 axiom val_of_nat: nat → val.
    143 (* Map from the front-end memory model to the back-end memory model *)
    144 axiom represent_block: block → val × val.
    145 (* CSC: fixed size chunk *)
    146 axiom chunk: memory_chunk.
    147 axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
    148 
    149 axiom address: Type[0].
    150 axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    151 axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    152 axiom addr_sub: address → nat → address.
    153 axiom addr_add: address → nat → address.
    154 (* CSC: ??? *)
    155 axiom address_of_label: mem → label → address.
    156 axiom address_chunks_of_label: mem → label → Byte × Byte.
    157 axiom label_of_address_chunks: Byte → Byte → label.
    158 axiom address_of_address_chunks: Byte → Byte → address.
    159 axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    160 axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    161 axiom hwreg_retrieve : mRegisterMap → Register → res val.
    162 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    163 
    164 definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
    165 
    166 (* CSC: frame reduced to this *)
    167 definition frame: Type[0] ≝ register_env val.
    168 
    169 (* CSC: exit not put in the state, like in OCaml. It is constant througout
    170    execution *)
    171 record state : Type[0] ≝
    172  { st_frms: list frame
    173  ; pc: address
    174  ; sp: address
    175  ; locals: register_env val
    176  ; carry: val
    177  ; regs: mRegisterMap
    178  ; m: mem
    179  }.
    180 
    181 definition set_m: mem → state → state ≝
    182  λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
    183 
    184 definition set_locals: register_env val → state → state ≝
    185  λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
    186 
    187 definition set_regs: mRegisterMap → state → state ≝
    188  λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
    189 
    190 definition set_sp: address → state → state ≝
    191  λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
    192 
    193 definition set_carry: val → state → state ≝
    194  λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
    195 
    196 definition set_pc: address → state → state ≝
    197  λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
    198 
    199 (* CSC: was build_state in RTL *)
    200 definition goto: label → state → state ≝
    201  λl,st. set_pc (address_of_label (m st) l) st.
    202 
    203 (* pushes the locals (i.e. the current frame) on top of the frames list *)
    204 definition save_frame: state → state ≝
    205  λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
    206 
    207 axiom FailedPopFrame: String.
    208 
    209 (* removes the top frame from the frames list *)
    210 definition pop_frame: state → res state ≝
    211  λst.
    212   match st_frms st with
    213    [ nil ⇒ Error ? (msg FailedPopFrame)
    214    | cons _ frms ⇒
    215       OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].
    216 
    217 axiom FailedStore: String.
    218 
    219 definition push: state → Byte → res state ≝
    220  λst,v.
    221   let sp ≝ val_of_address (sp st) in
    222   (*CSC: no monadic notation here *)
    223   bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
    224    (λm.
    225     let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    226     OK ? (set_m m (set_sp sp st))).
    227 
    228 
    229 definition pop: state → res (state × Byte) ≝
    230  λst:state.
    231   let sp ≝ val_of_address (sp st) in
    232   let sp ≝ sub sp (val_of_memory_chunk chunk) in
    233   let st ≝ set_sp (address_of_val sp) st in
    234   (*CSC: no monadic notation here *)
    235   bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
    236    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    237 
    238 definition save_ra : state → label → res state ≝
    239  λst,l.
    240   let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
    241   (* No monadic notation here *)
    242   bind ?? (push st addrl) (λst.push st addrh).
    243 
    244 definition fetch_ra : state → res (state × label) ≝
    245  λst.
    246   (* No monadic notation here *)
    247   bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
    248   bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
    249    OK ? 〈st, label_of_address_chunks addrl addrh〉)).
    250 
    251 (*CSC: To be implemented *)
    252 
    253 axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    254 axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
    255 
    256 definition init_locals : list register → register_env val ≝
    257 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    258 
    259 definition reg_store ≝
    260 λreg,v,locals. update RegisterTag val locals reg v.
    261 
    262 axiom BadRegister : String.
    263 
    264 definition reg_retrieve : register_env val → register → res val ≝
    265 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    266 
    267 axiom MissingSymbol : String.
    268 axiom FailedLoad : String.
    269 axiom BadFunction : String.
    270 
    271 (*CSC: to be implemented *)
    272 axiom fetch_external_args: external_function → state → res (list val).(* ≝
    273  λfn,st.
    274   let registerno ≝ ? fn in
    275   ! vs ←
    276    mmap …
    277     (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
    278   (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
    279   ?.*)
    280 
    281 (*CSC: to be implemented; fails if the first list is longer *)
    282 axiom fold_left2_first_not_longer:
    283  ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
    284   ∀acc:C. ∀l1:list A. ∀l2: list B.
    285    res C.
    286 
    287 (* CSC: the list should be a vector or have an upper bounded length *)
    288 definition set_result: list val → state → res state ≝
    289  λvs,st.
    290   (* CSC: monadic notation not used *)
    291   bind ?? (
    292    fold_left2_first_not_longer …
    293     (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
    294   (λregs.OK ? (set_regs regs st)).
    295 
    296 definition fetch_result: state → nat → res (list val) ≝
    297  λst,registersno.
    298   let retregs ≝ prefix … registersno RegisterRets in
    299   mmap … (λr. hwreg_retrieve (regs st) r) retregs.
    300 
    301 definition framesize: list ident → state → res nat ≝
    302   λglobals: list ident.
    303   λst.
    304   (* CSC: monadic notation missing here *)
    305     bind ?? (fetch_function globals st) (λf.
    306     OK ? (joint_if_stacksize globals … f)).
    307 
    308 definition get_hwsp : state → res address ≝
    309  λst.
    310   (* CSC: monadic notation missing here *)
    311   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
    312   (* CSC: monadic notation missing here *)
    313   bind ?? (Byte_of_val spl) (λspl.
    314   (* CSC: monadic notation missing here *)
    315   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
    316   (* CSC: monadic notation missing here *)
    317   bind ?? (Byte_of_val sph) (λsph.
    318   OK ? (address_of_address_chunks spl sph))))).
    319 
    320 definition set_hwsp : address → state → res state ≝
    321  λsp,st.
    322   let 〈spl,sph〉 ≝ address_chunks_of_address sp in
    323   (* CSC: monadic notation missing here *) 
    324   bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
    325   (* CSC: monadic notation missing here *) 
    326   bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
    327   OK ? (set_regs regs st))).
    328 
    329 definition retrieve: state → move_registers → res val ≝
    330   λst.
    331   λr.
    332   match r with
    333   [ pseudo   src ⇒ reg_retrieve (locals st) src
    334   | hardware src ⇒ hwreg_retrieve (regs st) src
    335   ].
    336 
    337 definition store ≝
    338   λst.
    339   λv.
    340   λr.
    341   match r with
    342   [ pseudo   dst ⇒
    343     ! locals ← reg_store dst v (locals st);
    344       ret ? (set_locals locals st)
    345   | hardware dst ⇒
    346     ! regs ← hwreg_store dst v (regs st);
    347       ret ? (set_regs regs st)
    348   ].
    349 
    350 definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
    351   λglobals. λge,st.
    352   ! s ← fetch_statement globals st;
    353   match s with
    354   [ ertl_st_lift_pre pre ⇒
    355     match pre with
    356     [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
    357     | joint_st_sequential seq l ⇒
    358       match seq with
    359       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
    360       | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
    361       | joint_instr_int dest v ⇒
    362         ! locals ← reg_store dest (val_of_Byte v) (locals st);
    363           ret ? 〈E0, goto l (set_locals locals st)〉
    364       | joint_instr_load addrl addrh dst ⇒
    365         ! vaddrh ← reg_retrieve (locals st) addrh;
    366         ! vaddrl ← reg_retrieve (locals st) addrl;
    367         ! vaddr ← smerge vaddrl vaddrh;
    368         ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    369         ! locals ← reg_store dst v (locals st);
    370           ret ? 〈E0, goto l (set_locals locals st)〉
    371       | joint_instr_store addrl addrh src ⇒
    372         ! vaddrh ← reg_retrieve (locals st) addrh;
    373         ! vaddrl ← reg_retrieve (locals st) addrl;
    374         ! vaddr ← smerge vaddrl vaddrh;
    375         ! v ← reg_retrieve (locals st) src;
    376         ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    377           ret ? 〈E0, goto l (set_m m' st)〉
    378       | joint_instr_cond src ltrue ⇒
    379         ! v ← reg_retrieve (locals st) src;
    380         ! b ← eval_bool_of_val v;
    381           ret ? 〈E0, goto (if b then ltrue else l) st〉
    382       | joint_instr_address ident prf ldest hdest ⇒
    383         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    384           let 〈laddr,haddr〉 ≝ represent_block addr in
    385         ! locals ← reg_store ldest laddr (locals st);
    386         ! locals ← reg_store hdest haddr locals;
    387           ret ? 〈E0, goto l (set_locals locals st)〉
    388       | joint_instr_op1 op acc_a ⇒
    389         ! v ← reg_retrieve (locals st) acc_a;
    390         ! v ← Byte_of_val v;
    391           let v' ≝ val_of_Byte (op1 eval op v) in
    392         ! locals ← reg_store acc_a v' (locals st);
    393           ret ? 〈E0, goto l (set_locals locals st)〉
    394       | joint_instr_op2 op acc_a_reg dest ⇒
    395         ! v1 ← reg_retrieve (locals st) acc_a_reg;
    396         ! v1 ← Byte_of_val v1;
    397         ! v2 ← reg_retrieve (locals st) acc_a_reg;
    398         ! v2 ← Byte_of_val v2;
    399         ! carry ← eval_bool_of_val (carry st);
    400           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    401           let v' ≝ val_of_Byte v' in
    402           let carry ≝ of_bool carry in
    403         ! locals ← reg_store dest v' (locals st);
    404           ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    405       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
    406       | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
    407       | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    408         ! v1 ← reg_retrieve (locals st) acc_a_reg;
    409         ! v1 ← Byte_of_val v1;
    410         ! v2 ← reg_retrieve (locals st) acc_b_reg;
    411         ! v2 ← Byte_of_val v2;
    412           let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    413           let v1' ≝ val_of_Byte v1' in
    414           let v2' ≝ val_of_Byte v2' in
    415         ! locals ← reg_store acc_a_reg v1' (locals st);
    416         ! locals ← reg_store acc_b_reg v2' locals;
    417           ret ? 〈E0, goto l (set_locals locals st)〉
    418       | joint_instr_pop dst ⇒
    419         ! 〈st,v〉 ← pop st;
    420         ! locals ← reg_store dst (val_of_Byte v) (locals st);
    421           ret ? 〈E0, goto l (set_locals locals st)〉
    422       | joint_instr_push src ⇒
    423         ! v ← reg_retrieve (locals st) src;
    424         ! v ← Byte_of_val v;
    425         ! st ← push st v;
    426           ret ? 〈E0, goto l st〉
    427       | joint_instr_move dst_src ⇒
    428         let 〈dst, src〉 ≝ dst_src in
    429         ! v ← retrieve st src;
    430         ! st ← store st v dst;
    431           ret ? 〈E0, goto l st〉
    432       (* CSC: changed, where the meat is *)
    433       | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
    434         ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    435         ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    436           match fd with
    437           [ Internal fn ⇒
    438             ! st ← save_ra st l;
    439               let st ≝ save_frame st in
    440               let locals ≝ init_locals (ertl_if_locals globals fn) in
    441               let l' ≝ ertl_if_entry globals fn in
    442               ret ? 〈 E0, goto l' (set_locals locals st)〉
    443           | External fn ⇒
    444             ! params ← fetch_external_args fn st;
    445             ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    446             ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    447             (* CSC: XXX bug here; I think I should split it into Byte-long
    448                components; instead I am making a singleton out of it *)
    449               let vs ≝ [mk_val ? evres] in
    450             ! st ← set_result vs st;
    451               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    452           ]
    453       ]
    454     (* CSC: changed, where the meat is *)
    455     | joint_st_return ⇒
    456       ! st ← pop_frame st;
    457       ! 〈st,pch〉 ← pop st;
    458       ! 〈st,pcl〉 ← pop st;
    459         let pc ≝ address_of_address_chunks pcl pch in
    460         ret ? 〈E0,set_pc pc st〉
    461     | _ ⇒ ?
    462     ]
    463   | ertl_st_new_frame l ⇒
    464     ! v ← framesize globals st;
    465     ! sp ← get_hwsp st;
    466       let newsp ≝ addr_sub sp v in
    467     ! st ← set_hwsp newsp st;
    468       ret ? 〈E0,goto l st〉
    469   | ertl_st_del_frame l ⇒
    470     ! v ← framesize globals st;
    471     ! sp ← get_hwsp st;
    472       let newsp ≝ addr_add sp v in
    473     ! st ← set_hwsp newsp st;
    474       ret ? 〈E0,goto l st〉
    475   | ertl_st_frame_size dst l ⇒
    476     ! v ← framesize globals st;
    477     ! locals ← reg_store dst (val_of_nat v) (locals st);
    478       ret ? 〈E0, goto l (set_locals locals st)〉
    479   (* CSC: Dropped:
    480       - rtl_st_stackaddr (becomes two get_hdw)
    481       - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    482       - rtl_st_call_ptr (unimplemented ATM) *)
    483   ].
    484      
    485 axiom WrongReturnValueType: String.
    486 
    487 definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
    488   λglobals: list ident.
    489   λexit.
    490   λregistersno.
    491   λst.
    492  (* CSC: monadic notation missing here *)
    493   match fetch_statement globals st with
    494   [ Error _ ⇒ None ?
    495   | OK s ⇒
    496     match s with
    497     [ ertl_st_lift_pre pre ⇒
    498       match pre with
    499       [ joint_st_return ⇒
    500         match fetch_ra st with
    501          [ Error _ ⇒ None ?
    502          | OK st_l ⇒
    503            let 〈st,l〉 ≝ st_l in
    504            match label_eq l exit with
    505            [ inl _ ⇒
    506              (* CSC: monadic notation missing here *)
    507              match fetch_result st registersno with
    508              [ Error _ ⇒ None ?
    509              | OK vals ⇒ Some ? (smerge2 vals)
    510              ]
    511            | inr _ ⇒ None ?
    512            ]
    513          ]
    514       | _ ⇒ None ?
    515       ]
    516     | _ ⇒ None ?
    517     ]
    518   ].
    519 
    520 definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
    521   λglobals.
    522   λexit.
    523   λregistersno.
    524   mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    525 
    526 (* CSC: XXX the program type does not fit with the globalenv and init_mem
    527 definition make_initial_state : rtl_program → res (genv × state) ≝
    528 λp.
    529   do ge ← globalenv Genv ?? p;
    530   do m ← init_mem Genv ?? p;
    531   let main ≝ rtl_pr_main ?? p in
    532   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    533   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    534   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
    535 
    536 definition RTL_fullexec : fullexec io_out io_in ≝
    537   mk_fullexec … RTL_exec ? make_initial_state.
    538 *)
    539 *)
Note: See TracChangeset for help on using the changeset viewer.