Changeset 1535 for src/RTLabs


Ignore:
Timestamp:
Nov 23, 2011, 12:07:01 PM (9 years ago)
Author:
campbell
Message:

Make RTLabs semantics use knowledge that the next instruction always
exists. (Makes statements involving RTLabs execution easier.)

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/semantics.ma

    r1369 r1535  
    1818; locals : register_env val
    1919; next   : label
     20; next_ok: present ?? (f_graph func) next
    2021; sp     : block
    2122; retdst : option register
    2223}.
    2324
    24 definition adv : label → frame → frame ≝
    25 λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f).
     25definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝
     26λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f).
    2627
    2728inductive state : Type[0] ≝
    … …  
    4849λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
    4950
    50 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
     51definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
    5152
    5253definition init_locals : list (register × typ) → register_env val ≝
    … …  
    9091match st with
    9192[ State f fs m ⇒
    92   ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (f_graph (func f)) (next f));
    93   match s with
    94   [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    95   | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    96   | St_const r cst l ⇒
     93  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
     94  match s return λs. labels_present ? s → ? with
     95  [ St_skip l ⇒ λH. ret ? 〈E0, build_state f fs m l ?〉
     96  | St_cost cl l ⇒ λH. ret ? 〈Echarge cl, build_state f fs m l ?〉
     97  | St_const r cst l ⇒ λH.
    9798      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    9899      ! locals ← reg_store r v (locals f);
    99       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    100   | St_op1 _ _ op dst src l ⇒
     100      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     101  | St_op1 _ _ op dst src l ⇒ λH.
    101102      ! v ← reg_retrieve (locals f) src;
    102103      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    103104      ! locals ← reg_store dst v' (locals f);
    104       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    105   | St_op2 op dst src1 src2 l ⇒
     105      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     106  | St_op2 op dst src1 src2 l ⇒ λH.
    106107      ! v1 ← reg_retrieve (locals f) src1;
    107108      ! v2 ← reg_retrieve (locals f) src2;
    108109      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    109110      ! locals ← reg_store dst v' (locals f);
    110       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    111   | St_load chunk addr dst l ⇒
     111      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     112  | St_load chunk addr dst l ⇒ λH.
    112113      ! vaddr ← reg_retrieve (locals f) addr;
    113114      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    114115      ! locals ← reg_store dst v (locals f);
    115       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    116   | St_store chunk addr src l ⇒
     116      ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     117  | St_store chunk addr src l ⇒ λH.
    117118      ! vaddr ← reg_retrieve (locals f) addr;
    118119      ! v ← reg_retrieve (locals f) src;
    119120      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    120       ret ? 〈E0, build_state f fs m' l〉
    121   | St_call_id id args dst l ⇒
     121      ret ? 〈E0, build_state f fs m' l ?〉
     122  | St_call_id id args dst l ⇒ λH.
    122123      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    123124      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    124125      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    125       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    126   | St_call_ptr frs args dst l ⇒
     126      ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     127  | St_call_ptr frs args dst l ⇒ λH.
    127128      ! fv ← reg_retrieve (locals f) frs;
    128129      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    129130      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    130       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    131   | St_tailcall_id id args ⇒
     131      ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     132  | St_tailcall_id id args ⇒ λH.
    132133      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    133134      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    134135      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    135136      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    136   | St_tailcall_ptr frs args ⇒
     137  | St_tailcall_ptr frs args ⇒ λH.
    137138      ! fv ← reg_retrieve (locals f) frs;
    138139      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    … …  
    140141      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    141142
    142   | St_cond src ltrue lfalse ⇒
     143  | St_cond src ltrue lfalse ⇒ λH.
    143144      ! v ← reg_retrieve (locals f) src;
    144145      ! b ← eval_bool_of_val v;
    145       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    146 
    147   | St_jumptable r ls ⇒
     146      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
     147
     148  | St_jumptable r ls ⇒ λH.
    148149      ! v ← reg_retrieve (locals f) r;
    149150      match v with
    150151      [ Vint _ i ⇒
    151           ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
    152           ret ? 〈E0, build_state f fs m l〉
     152          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
     153          [ None ⇒ λ_. Wrong ??? (msg BadJumpTable)
     154          | Some l ⇒ λE. ret ? 〈E0, build_state f fs m l ?〉
     155          ] (refl ??)
    153156      | _ ⇒ Wrong ??? (msg BadJumpValue)
    154157      ]
    155158
    156   | St_return ⇒
     159  | St_return ⇒ λH.
    157160      ! v ← match f_result (func f) with
    158161            [ None ⇒ ret ? (None ?)
    … …  
    163166            ];
    164167      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    165   ]
     168  ] (f_closed (func f) (next f) s ?)
    166169| Callstate fd params dst fs m ⇒
    167170    match fd with
    … …  
    171174           here *)
    172175        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    173         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
     176        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    174177    | External fn ⇒
    175178        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    … …  
    186189                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
    187190                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
    188         ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
     191        ret ? 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
    189192    ]
    190 ].
     193]. try @(next_ok f) try @lookup_lookup_present try @H
     194[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
     195| whd in H; @(All_nth … H ? E)
     196| cases (f_entry fn) //
     197] qed.
    191198
    192199definition is_final : state → option int ≝
Note: See TracChangeset for help on using the changeset viewer.