Changeset 1381


Ignore:
Timestamp:
Oct 14, 2011, 10:29:54 PM (8 years ago)
Author:
sacerdot
Message:

Old commented out code removed.

Location:
src
Files:
3 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 *)
  • src/LTL/semantics.ma

    r1380 r1381  
    44definition ltl_fullexec ≝
    55 ltl_lin_fullexec … (graph_succ_p …) … (graph_fetch_statement … (ltl_lin_sem_params …)).
    6 
    7 (*
    8 (* CSC: external functions never fail (??) and always return something of the
    9    size of one register, both in the frontend and in the backend.
    10    Is this reasonable??? In OCaml it always return a list, but in the frontend
    11    only the head is kept (or Undef if the list is empty) ??? *)
    12 
    13 (* CSC: carries are values and booleans are not values; so we use integers.
    14    But why using values at all? To have undef? *)
    15 (* CSC: ???????????? *)
    16 axiom smerge: val → val → res val.
    17 (* CSC: ???????????? In OCaml: IntValue.Int32.merge
    18    Note also that the translation can fail; so it should be a res int! *)
    19 axiom smerge2: list val → int.
    20 (* CSC: I have a byte, I need a value, but it is complex to do so *)
    21 axiom val_of_Byte: Byte → val.
    22 axiom Byte_of_val: val → res Byte.
    23 axiom val_of_nat: nat → val.
    24 (* Map from the front-end memory model to the back-end memory model *)
    25 axiom represent_block: block → val × val.
    26 (* CSC: fixed size chunk *)
    27 axiom chunk: memory_chunk.
    28 axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
    29 
    30 axiom address: Type[0].
    31 axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    32 axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    33 axiom addr_sub: address → nat → address.
    34 axiom addr_add: address → nat → address.
    35 (* CSC: ??? *)
    36 axiom address_of_label: mem → label → address.
    37 axiom address_chunks_of_label: mem → label → Byte × Byte.
    38 axiom label_of_address_chunks: Byte → Byte → label.
    39 axiom address_of_address_chunks: Byte → Byte → address.
    40 axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    41 axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    42 axiom hwreg_retrieve : mRegisterMap → Register → res val.
    43 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    44 
    45 definition genv ≝ λglobals. (genv_t Genv) (fundef (ltl_internal_function globals)).
    46 
    47 (* CSC: frame reduced to this
    48 definition frame: Type[0] ≝ unit.
    49 *)
    50 
    51 record state : Type[0] ≝
    52  { st_frms: unit (* CSC: frames are no longer useful *)
    53  ; pc: address
    54  ; sp: address
    55  ; locals: unit (* CSC: no more locals *)
    56  ; carry: val
    57  ; regs: mRegisterMap
    58  ; m: mem
    59  }.
    60 
    61 definition set_m: mem → state → state ≝
    62  λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
    63 
    64 definition set_locals: (*CSC *) unit → state → state ≝
    65  λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
    66 
    67 definition set_regs: mRegisterMap → state → state ≝
    68  λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
    69 
    70 definition set_sp: address → state → state ≝
    71  λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
    72 
    73 definition set_carry: val → state → state ≝
    74  λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
    75 
    76 definition set_pc: address → state → state ≝
    77  λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
    78 
    79 (* CSC: was build_state in RTL *)
    80 definition goto: label → state → state ≝
    81  λl,st. set_pc (address_of_label (m st) l) st.
    82 
    83 definition save_frame: state → state ≝ λst.st. (* CSC *)
    84 
    85 axiom FailedPopFrame: String.
    86 
    87 (* removes the top frame from the frames list *)
    88 definition pop_frame: state → res state ≝ λst.OK ? st. (* CSC *)
    89 
    90 axiom FailedStore: String.
    91 
    92 definition push: state → Byte → res state ≝
    93  λst,v.
    94   let sp ≝ val_of_address (sp st) in
    95   (*CSC: no monadic notation here *)
    96   bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
    97    (λm.
    98     let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    99     OK ? (set_m m (set_sp sp st))).
    100 
    101 
    102 definition pop: state → res (state × Byte) ≝
    103  λst:state.
    104   let sp ≝ val_of_address (sp st) in
    105   let sp ≝ sub sp (val_of_memory_chunk chunk) in
    106   let st ≝ set_sp (address_of_val sp) st in
    107   (*CSC: no monadic notation here *)
    108   bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
    109    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    110 
    111 definition save_ra : state → label → res state ≝
    112  λst,l.
    113   let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
    114   (* No monadic notation here *)
    115   bind ?? (push st addrl) (λst.push st addrh).
    116 
    117 (*CSC: unused now
    118 definition fetch_ra : state → res (state × label) ≝
    119  λst.
    120   (* No monadic notation here *)
    121   bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
    122   bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
    123    OK ? 〈st, label_of_address_chunks addrl addrh〉)). *)
    124 
    125 (*CSC: To be implemented *)
    126 
    127 axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
    128 axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
    129 
    130 definition init_locals : list register → register_env val ≝
    131 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    132 
    133 definition reg_store ≝
    134 λreg,v,locals. update RegisterTag val locals reg v.
    135 
    136 axiom BadRegister : String.
    137 
    138 definition reg_retrieve : register_env val → register → res val ≝
    139 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    140 
    141 axiom MissingSymbol : String.
    142 axiom FailedLoad : String.
    143 axiom BadFunction : String.
    144 
    145 (*CSC: to be implemented *)
    146 axiom fetch_external_args: external_function → state → res (list val).(* ≝
    147  λfn,st.
    148   let registerno ≝ ? fn in
    149   ! vs ←
    150    mmap …
    151     (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
    152   (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
    153   ?.*)
    154 
    155 (*CSC: to be implemented; fails if the first list is longer *)
    156 axiom fold_left2_first_not_longer:
    157  ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
    158   ∀acc:C. ∀l1:list A. ∀l2: list B.
    159    res C.
    160 
    161 (* CSC: the list should be a vector or have an upper bounded length *)
    162 definition set_result: list val → state → res state ≝
    163  λvs,st.
    164   (* CSC: monadic notation not used *)
    165   bind ?? (
    166    fold_left2_first_not_longer …
    167     (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
    168   (λregs.OK ? (set_regs regs st)).
    169 
    170 definition fetch_result: state → nat → res (list val) ≝
    171  λst,registersno.
    172   let retregs ≝ prefix … registersno RegisterRets in
    173   mmap … (λr. hwreg_retrieve (regs st) r) retregs.
    174 
    175 definition framesize: list ident → state → res nat ≝
    176   λglobals: list ident.
    177   λst.
    178   (* CSC: monadic notation missing here *)
    179     bind ?? (fetch_function globals st) (λf.
    180     OK ? (ltl_if_stacksize globals f)).
    181 
    182 definition get_hwsp : state → res address ≝
    183  λst.
    184   (* CSC: monadic notation missing here *)
    185   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
    186   (* CSC: monadic notation missing here *)
    187   bind ?? (Byte_of_val spl) (λspl.
    188   (* CSC: monadic notation missing here *)
    189   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
    190   (* CSC: monadic notation missing here *)
    191   bind ?? (Byte_of_val sph) (λsph.
    192   OK ? (address_of_address_chunks spl sph))))).
    193 
    194 definition set_hwsp : address → state → res state ≝
    195  λsp,st.
    196   let 〈spl,sph〉 ≝ address_chunks_of_address sp in
    197   (* CSC: monadic notation missing here *) 
    198   bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
    199   (* CSC: monadic notation missing here *) 
    200   bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
    201   OK ? (set_regs regs st))).
    202 
    203 (*
    204 (* CSC: completely different because different type for registers_move *)
    205 definition retrieve: state → registers_move → res val ≝
    206   λst.
    207   λr.
    208   match r with
    209   [ pseudo   src ⇒ reg_retrieve (locals st) src
    210   | from_acc src ⇒ hwreg_retrieve (regs st) src
    211   ].
    212 
    213 definition store ≝
    214   λst.
    215   λv.
    216   λr.
    217   match r with
    218   [ pseudo   dst ⇒
    219     ! locals ← reg_store dst v (locals st);
    220       ret ? (set_locals locals st)
    221   | hardware dst ⇒
    222     ! regs ← hwreg_store dst v (regs st);
    223       ret ? (set_regs regs st)
    224   ].
    225 *)
    226 
    227 definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
    228   λglobals. λge,st.
    229   ! s ← fetch_statement globals st;
    230   match s with
    231     [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
    232     | joint_st_sequential seq l ⇒
    233       match seq with
    234       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
    235       | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
    236       | joint_instr_int dest v ⇒
    237         ! locals ← reg_store dest (val_of_Byte v) (locals st);
    238           ret ? 〈E0, goto l (set_locals locals st)〉
    239       | joint_instr_load addrl addrh dst ⇒
    240         ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
    241         ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
    242         ! vaddr ← smerge vaddrl vaddrh;
    243         ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    244         ! regs ← hwreg_store dst v (regs st); (*CSC*)
    245           ret ? 〈E0, goto l (set_regs regs st)〉
    246       | joint_instr_store addrl addrh src ⇒
    247         ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
    248         ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
    249         ! vaddr ← smerge vaddrl vaddrh;
    250         ! v ← hwreg_retrieve (regs st) src; (*CSC*)
    251         ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    252           ret ? 〈E0, goto l (set_m m' st)〉
    253       | joint_instr_cond src ltrue ⇒
    254         ! v ← hwreg_retrieve (regs st) src; (*CSC*)
    255         ! b ← eval_bool_of_val v;
    256           ret ? 〈E0, goto (if b then ltrue else l) st〉
    257       | joint_instr_address ident prf ldest hdest ⇒
    258         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    259           let 〈laddr,haddr〉 ≝ represent_block addr in
    260         ! locals ← reg_store ldest laddr (locals st);
    261         ! locals ← reg_store hdest haddr locals;
    262           ret ? 〈E0, goto l (set_locals locals st)〉
    263       | joint_instr_op1 op acc_a ⇒
    264         ! v ← reg_retrieve (locals st) acc_a;
    265         ! v ← Byte_of_val v;
    266           let v' ≝ val_of_Byte (op1 eval op v) in
    267         ! locals ← reg_store acc_a v' (locals st);
    268           ret ? 〈E0, goto l (set_locals locals st)〉
    269       | joint_instr_op2 op acc_a_reg dest ⇒
    270         ! v1 ← reg_retrieve (locals st) acc_a_reg;
    271         ! v1 ← Byte_of_val v1;
    272         ! v2 ← reg_retrieve (locals st) acc_a_reg;
    273         ! v2 ← Byte_of_val v2;
    274         ! carry ← eval_bool_of_val (carry st);
    275           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    276           let v' ≝ val_of_Byte v' in
    277           let carry ≝ of_bool carry in
    278         ! locals ← reg_store dest v' (locals st);
    279           ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    280       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
    281       | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
    282       | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    283         ! v1 ← reg_retrieve (locals st) acc_a_reg;
    284         ! v1 ← Byte_of_val v1;
    285         ! v2 ← reg_retrieve (locals st) acc_b_reg;
    286         ! v2 ← Byte_of_val v2;
    287           let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    288           let v1' ≝ val_of_Byte v1' in
    289           let v2' ≝ val_of_Byte v2' in
    290         ! locals ← reg_store acc_a_reg v1' (locals st);
    291         ! locals ← reg_store acc_b_reg v2' locals;
    292           ret ? 〈E0, goto l (set_locals locals st)〉
    293       | joint_instr_pop dst ⇒
    294         ! 〈st,v〉 ← pop st;
    295         ! locals ← reg_store dst (val_of_Byte v) (locals st);
    296           ret ? 〈E0, goto l (set_locals locals st)〉
    297       | joint_instr_push src ⇒
    298         ! v ← reg_retrieve (locals st) src;
    299         ! v ← Byte_of_val v;
    300         ! st ← push st v;
    301           ret ? 〈E0, goto l st〉
    302       | joint_instr_move dst_src ⇒
    303         let 〈dst, src〉 ≝ dst_src in
    304         ! v ← retrieve st src;
    305         ! st ← store st v dst;
    306           ret ? 〈E0, goto l st〉
    307 (*
    308       | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
    309         ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    310         ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    311           match fd with
    312           [ Internal fn ⇒
    313             ! st ← save_ra st l;
    314               let st ≝ save_frame st in
    315               let locals ≝ init_locals (ertl_if_locals globals fn) in
    316               let l' ≝ ertl_if_entry globals fn in
    317               ret ? 〈 E0, goto l' (set_locals locals st)〉
    318           | External fn ⇒
    319             ! params ← fetch_external_args fn st;
    320             ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    321             ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    322             (* CSC: XXX bug here; I think I should split it into Byte-long
    323                components; instead I am making a singleton out of it *)
    324               let vs ≝ [mk_val ? evres] in
    325             ! st ← set_result vs st;
    326               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    327           ]
    328 *)
    329       | _ ⇒ ?
    330       ]
    331     (* CSC: changed, where the meat is *)
    332     | joint_st_return ⇒
    333       ! st ← pop_frame st;
    334       ! 〈st,pch〉 ← pop st;
    335       ! 〈st,pcl〉 ← pop st;
    336         let pc ≝ address_of_address_chunks pcl pch in
    337         ret ? 〈E0,set_pc pc st〉
    338     ].
    339   ].
    340      
    341 axiom WrongReturnValueType: String.
    342 
    343 definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
    344   λglobals: list ident.
    345   λexit.
    346   λregistersno.
    347   λst.
    348  (* CSC: monadic notation missing here *)
    349   match fetch_statement globals st with
    350   [ Error _ ⇒ None ?
    351   | OK s ⇒
    352     match s with
    353     [ ertl_st_lift_pre pre ⇒
    354       match pre with
    355       [ joint_st_return ⇒
    356         match fetch_ra st with
    357          [ Error _ ⇒ None ?
    358          | OK st_l ⇒
    359            let 〈st,l〉 ≝ st_l in
    360            match label_eq l exit with
    361            [ inl _ ⇒
    362              (* CSC: monadic notation missing here *)
    363              match fetch_result st registersno with
    364              [ Error _ ⇒ None ?
    365              | OK vals ⇒ Some ? (smerge2 vals)
    366              ]
    367            | inr _ ⇒ None ?
    368            ]
    369          ]
    370       | _ ⇒ None ?
    371       ]
    372     | _ ⇒ None ?
    373     ]
    374   ].
    375 
    376 definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
    377   λglobals.
    378   λexit.
    379   λregistersno.
    380   mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    381 
    382 (* CSC: XXX the program type does not fit with the globalenv and init_mem
    383 definition make_initial_state : rtl_program → res (genv × state) ≝
    384 λp.
    385   do ge ← globalenv Genv ?? p;
    386   do m ← init_mem Genv ?? p;
    387   let main ≝ rtl_pr_main ?? p in
    388   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    389   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    390   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
    391 
    392 definition RTL_fullexec : fullexec io_out io_in ≝
    393   mk_fullexec … (λ_.RTL_exec) ? make_initial_state.
    394 *)
    395 *)
  • src/RTL/semantics.ma

    r1377 r1381  
    11include "joint/SemanticUtils.ma".
    2 (*
    3 include "utilities/lists.ma".
    4 include "common/Errors.ma".
    5 include "common/Globalenvs.ma".
    6 include "common/IO.ma".
    7 include "common/SmallstepExec.ma".
    8 *)
    92include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    103include alias "common/Identifiers.ma".
     
    123116definition rtl_fullexec ≝
    124117 joint_fullexec … (λp. rtl_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 (* Map from the front-end memory model to the back-end memory model *)
    143 axiom represent_block: block → val × val.
    144 (* CSC: fixed size chunk *)
    145 axiom chunk: memory_chunk.
    146 
    147 definition genv ≝ (genv_t Genv) (fundef rtl_internal_function).
    148 
    149 (* CSC: added carry *)
    150 record frame : Type[0] ≝
    151 { func   : rtl_internal_function
    152 ; locals : register_env val
    153 ; next   : label
    154 ; sp     : block
    155 ; retdst : list register
    156 ; carry  : val
    157 }.
    158 
    159 (* CSC: added carry *)
    160 definition adv : label → frame → frame ≝
    161 λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f) (carry f).
    162 
    163 inductive state : Type[0] ≝
    164 | State :
    165    ∀   f : frame.
    166    ∀  fs : list frame.
    167    ∀   m : mem.
    168    state
    169 | Callstate :
    170    ∀  fd : fundef rtl_internal_function.
    171    ∀args : list val.
    172    ∀ dst : list register. (* CSC: changed from option to list *)
    173    ∀ stk : list frame.
    174    ∀   m : mem.
    175    state
    176 | Returnstate :
    177    (* CSC: the two lists should have the same length, but this is
    178       enforced only by the semantics *)
    179    ∀ rtv : list val. (* CSC: changed from option to list *)
    180    ∀ dst : list register. (* CSC: changed from option to list *)
    181    ∀ stk : list frame.
    182    ∀   m : mem.
    183    state.
    184 
    185 definition mem_of_state : state → mem ≝
    186 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
    187 
    188 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    189 
    190 (* CSC: modified to take in input a list of registers (untyped) *)
    191 definition init_locals : list register → register_env val ≝
    192 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    193 
    194 definition reg_store ≝
    195 λreg,v,locals.
    196   update RegisterTag val locals reg v.
    197 
    198 axiom WrongNumberOfParameters : String.
    199 
    200 (* CSC: modified to take in input a list of registers (untyped) *)
    201 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    202 match rs with
    203 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    204 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    205   let locals' ≝ add RegisterTag val locals r v in
    206   params_store rst vst locals'
    207 ] ].
    208 
    209 axiom BadRegister : String.
    210 
    211 definition reg_retrieve : register_env ? → register → res val ≝
    212 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    213 
    214 axiom FailedOp : String.
    215 axiom MissingSymbol : String.
    216 
    217 axiom MissingStatement : String.
    218 axiom FailedConstant : String.
    219 axiom FailedLoad : String.
    220 axiom FailedStore : String.
    221 axiom BadFunction : String.
    222 axiom BadJumpTable : String.
    223 axiom BadJumpValue : String.
    224 axiom FinalState : String.
    225 axiom ReturnMismatch : String.
    226 
    227 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    228 λge,st.
    229 match st with
    230 [ State f fs m ⇒
    231   ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (rtl_if_graph (func f)) (next f));
    232   match s with
    233   [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    234   | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    235   | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
    236       ! vaddrh ← reg_retrieve (locals f) addrh;
    237       ! vaddrl ← reg_retrieve (locals f) addrl;
    238       ! vaddr ← smerge vaddrl vaddrh;
    239       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    240       ! locals ← reg_store dst v (locals f);
    241       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    242   | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
    243       ! vaddrh ← reg_retrieve (locals f) addrh;
    244       ! vaddrl ← reg_retrieve (locals f) addrl;
    245       ! vaddr ← smerge vaddrl vaddrh;
    246       ! v ← reg_retrieve (locals f) src;
    247       ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    248       ret ? 〈E0, build_state f fs m' l〉
    249   | rtl_st_call_id id args dst l ⇒
    250       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    251       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    252       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    253       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    254   | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
    255       ! hfv ← reg_retrieve (locals f) hfrs;
    256       ! lfv ← reg_retrieve (locals f) lfrs;
    257       ! fv  ← smerge lfv hfv;
    258       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    259       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    260       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    261   | rtl_st_tailcall_id id args ⇒
    262       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    263       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    264       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    265       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    266   | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
    267       ! hfv ← reg_retrieve (locals f) hfrs;
    268       ! lfv ← reg_retrieve (locals f) lfrs;
    269       ! fv  ← smerge lfv hfv;
    270       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    271       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    272       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    273   | rtl_st_return ⇒
    274       (* CSC: rtl_if_result/f_result; list vs option *)
    275       let dest ≝ rtl_if_result (func f) in
    276       ! v ←  mmap … (reg_retrieve (locals f)) dest;
    277       ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    278   | rtl_st_cond src ltrue lfalse ⇒
    279       ! v ← reg_retrieve (locals f) src;
    280       ! b ← eval_bool_of_val v;
    281       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    282   (* CSC: mismatch between the memory models and failures for the next two opx *)
    283   | rtl_st_op1 op dst src l ⇒
    284      ! v ← reg_retrieve (locals f) src;
    285      ! v ← Byte_of_val v;
    286      let v' ≝ val_of_Byte (op1 eval op v) in
    287      ! locals ← reg_store dst v' (locals f);
    288      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    289   | rtl_st_op2 op dst src1 src2 l ⇒
    290      ! v1 ← reg_retrieve (locals f) src1;
    291      ! v1 ← Byte_of_val v1;
    292      ! v2 ← reg_retrieve (locals f) src2;
    293      ! v2 ← Byte_of_val v2;
    294      ! carry ← eval_bool_of_val (carry f);
    295      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    296      let v' ≝ val_of_Byte v' in
    297      let carry ≝ of_bool carry in
    298      ! locals ← reg_store dst v' (locals f);
    299      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
    300 
    301   (* CSC: Removed: St_jumptable *)
    302   (* CSC: Added: *)
    303  
    304   (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
    305   | rtl_st_addr ldest hdest id l ⇒
    306      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    307      let 〈laddr,haddr〉 ≝ represent_block addr in
    308      ! locals ← reg_store ldest laddr (locals f);
    309      ! locals ← reg_store hdest haddr locals;
    310      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    311   | rtl_st_stack_addr ldest hdest l ⇒
    312      let 〈laddr,haddr〉 ≝ represent_block (sp f) in
    313      ! locals ← reg_store ldest laddr (locals f);
    314      ! locals ← reg_store hdest haddr locals;
    315      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    316   | rtl_st_int dest v l ⇒
    317      ! locals ← reg_store dest (val_of_Byte v) (locals f);
    318      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    319 
    320   (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
    321   | rtl_st_move dst src l ⇒
    322      ! v ← reg_retrieve (locals f) src;
    323      ! locals ← reg_store dst v (locals f);
    324      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    325   (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
    326   | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    327      ! v1 ← reg_retrieve (locals f) sacc;
    328      ! v1 ← Byte_of_val v1;
    329      ! v2 ← reg_retrieve (locals f) sbacc;
    330      ! v2 ← Byte_of_val v2;
    331      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    332      let v1' ≝ val_of_Byte v1' in
    333      let v2' ≝ val_of_Byte v2' in
    334      ! locals ← reg_store dacc v1' (locals f);
    335      ! locals ← reg_store dbacc v2' locals;
    336      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    337  
    338   | rtl_st_clear_carry l ⇒
    339     ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
    340   | rtl_st_set_carry l ⇒
    341     ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
    342   ]
    343 | Callstate fd params dst fs m ⇒
    344     match fd with
    345     [ Internal fn ⇒
    346         ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
    347         let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
    348         (* CSC: added carry *)
    349         ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
    350     | External fn ⇒
    351         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    352         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    353         (* CSC: return type changed from option to list *)
    354         (* CSC: XXX bug here; I think I should split it into Byte-long
    355            components; instead I am making a singleton out of it *)
    356         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    357     ]
    358 | Returnstate v dst fs m ⇒
    359     match fs with
    360     [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    361     | cons f fs' ⇒
    362        ! locals ←
    363          mfold_left2 ???
    364           (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
    365         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
    366     ]
    367 ].
    368 
    369 axiom WrongReturnValueType: String.
    370 
    371 definition is_final : state → option ((*CSC: why not res*) int) ≝
    372 λs. match s with
    373 [ State _ _ _ ⇒ None ?
    374 | Callstate _ _ _ _ _ ⇒ None ?
    375 | Returnstate v _ fs _ ⇒
    376     match fs with
    377      [ nil ⇒ Some ? (smerge2 v)
    378      | _ ⇒ None ? ]].
    379 (*
    380 definition RTL_exec : execstep io_out io_in ≝
    381   mk_execstep … ? is_final mem_of_state eval_statement.
    382 *)
    383 (* CSC: XXX the program type does not fit with the globalenv and init_mem
    384 definition make_initial_state : rtl_program → res (genv × state) ≝
    385 λp.
    386   do ge ← globalenv Genv ?? p;
    387   do m ← init_mem Genv ?? p;
    388   let main ≝ rtl_pr_main ?? p in
    389   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    390   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    391   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
    392 
    393 definition RTL_fullexec : fullexec io_out io_in ≝
    394   mk_fullexec … RTL_exec ? make_initial_state.
    395 *)
    396 *)
Note: See TracChangeset for help on using the changeset viewer.