Changeset 1381 for src/LTL


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

Old commented out code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 *)
Note: See TracChangeset for help on using the changeset viewer.