Changeset 1156


Ignore:
Timestamp:
Aug 31, 2011, 11:41:21 AM (8 years ago)
Author:
sacerdot
Message:

ERTL semantics completed up to initialization and memory model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1151 r1156  
    2727axiom val_of_Byte: Byte → val.
    2828axiom Byte_of_val: val → res Byte.
     29axiom val_of_nat: nat → val.
    2930(* Map from the front-end memory model to the back-end memory model *)
    3031axiom represent_block: block → val × val.
     
    3637axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    3738axiom address_of_val: val → address. (* CSC: only to shift the sp *)
     39axiom addr_sub: address → nat → address.
     40axiom addr_add: address → nat → address.
    3841(* CSC: ??? *)
    3942axiom address_of_label: mem → label → address.
     
    4144axiom label_of_address_chunks: Byte → Byte → label.
    4245axiom address_of_address_chunks: Byte → Byte → address.
     46axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    4347axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4448axiom hwreg_retrieve : mRegisterMap → Register → res val.
     
    133137
    134138(*CSC: To be implemented *)
     139axiom fetch_function: state → res ertl_internal_function.
    135140axiom fetch_statement: state → res ertl_statement.
    136141
     
    141146λreg,v,locals. update RegisterTag val locals reg v.
    142147
    143 (*
    144 axiom WrongNumberOfParameters : String.
    145 
    146 (* CSC: modified to take in input a list of registers (untyped) *)
    147 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    148 match rs with
    149 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    150 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    151   let locals' ≝ add RegisterTag val locals r v in
    152   params_store rst vst locals'
    153 ] ].
    154 *)
    155 
    156148axiom BadRegister : String.
    157149
     
    159151λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    160152
    161 (*
    162 axiom FailedOp : String.
    163 *)
    164153axiom MissingSymbol : String.
    165 (*
    166 axiom MissingStatement : String.
    167 axiom FailedConstant : String. *)
    168154axiom FailedLoad : String.
    169155axiom BadFunction : String.
    170 (*axiom BadJumpTable : String.
    171 axiom BadJumpValue : String.
    172 axiom FinalState : String.
    173 axiom ReturnMismatch : String.
    174 *)
    175156
    176157(*CSC: to be implemented *)
     
    203184  let retregs ≝ prefix … registersno RegisterRets in
    204185  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
     186
     187definition framesize: state → res nat ≝
     188 λst.
     189  (* CSC: monadic notation missing here *)
     190  bind ?? (fetch_function st) (λf.
     191  OK ? (ertl_if_stacksize f)).
     192
     193definition get_hwsp : state → res address ≝
     194 λst.
     195  (* CSC: monadic notation missing here *)
     196  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
     197  (* CSC: monadic notation missing here *)
     198  bind ?? (Byte_of_val spl) (λspl.
     199  (* CSC: monadic notation missing here *)
     200  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
     201  (* CSC: monadic notation missing here *)
     202  bind ?? (Byte_of_val sph) (λsph.
     203  OK ? (address_of_address_chunks spl sph))))).
     204
     205definition set_hwsp : address → state → res state ≝
     206 λsp,st.
     207  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
     208  (* CSC: monadic notation missing here *) 
     209  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
     210  (* CSC: monadic notation missing here *) 
     211  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
     212  OK ? (set_regs regs st))).
    205213
    206214definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     
    325333  (* CSC: new stuff *)
    326334  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    327   | ertl_st_new_frame _ ⇒ ?
    328   | ertl_st_del_frame _ ⇒ ?
    329   | ertl_st_frame_size _ _ ⇒ ?
     335  | ertl_st_new_frame l ⇒
     336     ! v ← framesize st;
     337     ! sp ← get_hwsp st;
     338     let newsp ≝ addr_sub sp v in
     339     ! st ← set_hwsp newsp st;
     340     ret ? 〈E0,goto l st〉
     341  | ertl_st_del_frame l ⇒
     342     ! v ← framesize st;
     343     ! sp ← get_hwsp st;
     344     let newsp ≝ addr_add sp v in
     345     ! st ← set_hwsp newsp st;
     346     ret ? 〈E0,goto l st〉
     347  | ertl_st_frame_size dst l ⇒
     348     ! v ← framesize st;
     349     ! locals ← reg_store dst (val_of_nat v) (locals st);
     350     ret ? 〈E0, goto l (set_locals locals st)〉
    330351  | ertl_st_pop dst l ⇒
    331352     ! 〈st,v〉 ← pop st;
     
    338359     ret ? 〈E0, goto l st〉
    339360  ].
    340 cases daemon. qed.
    341361
    342362axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.