Changeset 1162


Ignore:
Timestamp:
Sep 1, 2011, 11:32:25 AM (8 years ago)
Author:
mulligan
Message:

changes committed to ertl semantics based on our new combined syntax for ertl, ltl and lin

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1161 r1162  
    139139
    140140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    141 axiom fetch_function: state → res ertl_internal_function.
     141axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
    142142
    143143definition init_locals : list register → register_env val ≝
     
    186186  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
    187187
    188 definition framesize: state → res nat ≝
    189  λst.
     188definition framesize: list ident → state → res nat ≝
     189  λglobals: list ident.
     190  λst.
    190191  (* CSC: monadic notation missing here *)
    191   bind ?? (fetch_function st) (λf.
    192   OK ? (ertl_if_stacksize f)).
     192    bind ?? (fetch_function globals st) (λf.
     193    OK ? (ertl_if_stacksize globals f)).
    193194
    194195definition get_hwsp : state → res address ≝
     
    275276        ! regs ← hwreg_store dst v (regs st);
    276277          ret ? 〈E0, goto l (set_regs regs st)〉
    277 (* XXX: examine: where is the result being stored?
    278278      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    279279        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     
    284284          let v1' ≝ val_of_Byte v1' in
    285285          let v2' ≝ val_of_Byte v2' in
    286         ! locals ← reg_store dacc v1' (locals st);
    287         ! locals ← reg_store dbacc v2' locals;
    288           ret ? 〈E0, goto l (set_locals locals st)〉
    289 *)
     286        ! locals ← reg_store acc_a_reg v1' (locals st);
     287        ! locals ← reg_store acc_b_reg v2' locals;
     288          ret ? 〈E0, goto l (set_locals locals st)〉
    290289      | joint_instr_pop dst ⇒
    291290        ! 〈st,v〉 ← pop st;
     
    297296        ! st ← push st v;
    298297          ret ? 〈E0, goto l st〉
     298      (* CSC: changed, where the meat is *)
    299299      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
    300300        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    304304            ! st ← save_ra st l;
    305305              let st ≝ save_frame st in
    306               let locals ≝ init_locals (ertl_if_locals fn) in
    307               let l' ≝ ertl_if_entry fn in
     306              let locals ≝ init_locals (ertl_if_locals globals fn) in
     307              let l' ≝ ertl_if_entry globals fn in
    308308              ret ? 〈 E0, goto l' (set_locals locals st)〉
    309309          | External fn ⇒
     
    346346     ret ? 〈E0, goto l (set_locals locals st)〉
    347347  ].
    348  
    349  
    350   match s with
    351348
    352349  (* CSC: Dropped:
     
    354351      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    355352      - rtl_st_call_ptr (unimplemented ATM) *)
     353  cases daemon
     354qed.
    356355     
    357   (* CSC: changed, where the meat is *)
    358  
    359   (* CSC: new stuff *)
    360   | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    361 <<<<<<< .mine  ].
    362 
    363356axiom WrongReturnValueType: String.
    364357
    365 definition is_final : label → nat → state → option ((*CSC: why not res*) int) ≝
    366 λexit,registersno,st.
     358definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     359  λglobals: list ident.
     360  λexit.
     361  λregistersno.
     362  λst.
    367363 (* CSC: monadic notation missing here *)
    368  match fetch_statement st with
     364  match fetch_statement globals st with
    369365  [ Error _ ⇒ None ?
    370366  | OK s ⇒
    371      match s with
    372       [ ertl_st_return ⇒
    373        (* CSC: monadic notation missing here *)
     367    match s with
     368    [ ertl_st_lift_pre pre ⇒
     369      match pre with
     370      [ joint_st_return ⇒
    374371        match fetch_ra st with
    375372         [ Error _ ⇒ None ?
    376          | OK st_l ⇒ let 〈st,l〉 ≝ st_l in
    377             match label_eq l exit with
    378              [ inl _ ⇒
    379                (* CSC: monadic notation missing here *)
    380                 match fetch_result st registersno with
    381                  [ Error _ ⇒ None ?
    382                  | OK vals ⇒ Some ? (smerge2 vals) ]
    383              | inr _ ⇒ None ? ]]
    384       | _ ⇒ None … ]].
    385 
    386 definition ERTL_exec : label → nat → execstep io_out io_in ≝
    387  λexit,registersno.
    388   mk_execstep … ? (is_final exit registersno) m eval_statement.
     373         | OK st_l ⇒
     374           let 〈st,l〉 ≝ st_l in
     375           match label_eq l exit with
     376           [ inl _ ⇒
     377             (* CSC: monadic notation missing here *)
     378             match fetch_result st registersno with
     379             [ Error _ ⇒ None ?
     380             | OK vals ⇒ Some ? (smerge2 vals)
     381             ]
     382           | inr _ ⇒ None ?
     383           ]
     384         ]
     385      | _ ⇒ None ?
     386      ]
     387    | _ ⇒ None ?
     388    ]
     389  ].
     390
     391definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
     392  λglobals.
     393  λexit.
     394  λregistersno.
     395  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    389396
    390397(* CSC: XXX the program type does not fit with the globalenv and init_mem
Note: See TracChangeset for help on using the changeset viewer.