Changeset 1126


Ignore:
Timestamp:
Aug 29, 2011, 3:07:53 PM (8 years ago)
Author:
sacerdot
Message:

Semantics completed up to initial state creation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1122 r1126  
    2121(* CSC: ???????????? *)
    2222axiom smerge: val → val → res val.
     23(* CSC: ???????????? In OCaml: IntValue.Int32.merge
     24   Note also that the translation can fail; so it should be a res int! *)
     25axiom smerge2: list val → int.
    2326(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2427axiom val_of_Byte: Byte → val.
     
    5962   state
    6063| Returnstate :
     64   (* CSC: the two lists should have the same length, but this is
     65      enforced only by the semantics *)
    6166   ∀ rtv : list val. (* CSC: changed from option to list *)
    6267   ∀ dst : list register. (* CSC: changed from option to list *)
     
    236241        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    237242    ]
    238 | Returnstate v dst fs m ⇒ ? (* CSC: XXXXXXXXXXXXXXXXXX
     243| Returnstate v dst fs m ⇒
    239244    match fs with
    240245    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    241246    | cons f fs' ⇒
    242         ! locals ← match dst with
    243                    [ None ⇒ match v with [ None ⇒ OK ? (locals f)
    244                                          | _ ⇒ Error ? (msg ReturnMismatch) ]
    245                    | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
    246                                            | Some v' ⇒ reg_store d v' (locals f) ] ];
    247         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    248     ] *)
     247       ! locals ←
     248         mfold_left2 ???
     249          (λlocals,dst,v. reg_store dst v locals) (OK ? (locals f)) dst v;
     250        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f) (carry f)) fs' m〉
     251    ]
    249252].
    250253
    251 definition is_final : state → option int ≝
     254axiom WrongReturnValueType: String.
     255
     256definition is_final : state → option ((*CSC: why not res*) int) ≝
    252257λs. match s with
    253258[ State _ _ _ ⇒ None ?
    254259| Callstate _ _ _ _ _ ⇒ None ?
    255260| Returnstate v _ fs _ ⇒
    256     match fs with [ nil ⇒
    257       match v with [ Some v' ⇒
    258         match v' with
    259         [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    260         | _ ⇒ None ? ]
    261       | None ⇒ None ? ]
    262     | cons _ _ ⇒ None ? ]
    263 ].
    264 
    265 definition RTLabs_exec : execstep io_out io_in ≝
     261    match fs with
     262     [ nil ⇒ Some ? (smerge2 v)
     263     | _ ⇒ None ? ]].
     264
     265definition RTL_exec : execstep io_out io_in ≝
    266266  mk_execstep … ? is_final mem_of_state eval_statement.
    267267
    268 definition make_initial_state : RTLabs_program → res (genv × state) ≝
     268(* CSC: XXX the program type does not fit with the globalenv and init_mem
     269definition make_initial_state : rtl_program → res (genv × state) ≝
    269270λp.
    270271  do ge ← globalenv Genv ?? p;
    271272  do m ← init_mem Genv ?? p;
    272   let main ≝ prog_main ?? p in
     273  let main ≝ rtl_pr_main ?? p in
    273274  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    274275  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    275   OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
    276 
    277 definition RTLabs_fullexec : fullexec io_out io_in ≝
    278   mk_fullexec … RTLabs_exec ? make_initial_state.
    279 
     276  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
     277
     278definition RTL_fullexec : fullexec io_out io_in ≝
     279  mk_fullexec … RTL_exec ? make_initial_state.
     280*)
Note: See TracChangeset for help on using the changeset viewer.