Changeset 761


Ignore:
Timestamp:
Apr 19, 2011, 12:22:32 PM (9 years ago)
Author:
campbell
Message:

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

Location:
src
Files:
2 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r726 r761  
    11include "basics/types.ma".
    22
     3include "utilities/option.ma".
    34include "ASM/BitVector.ma".
    45
     
    7576  ]
    7677qed.
     78
     79let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
     80  (match b with
     81    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
     82                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
     83                   | Stub _ ⇒ λ_. None ?
     84                   | Node _ _ _ ⇒ λprf. ⊥
     85                   ] (refl ? O)
     86    | VCons o hd tl ⇒ λt.
     87          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
     88            [ Leaf l ⇒ λprf.⊥
     89            | Node p l r ⇒ λprf.
     90               match hd with
     91                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
     92                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
     93                ]
     94            | Stub p ⇒ λprf. None ?
     95            ] (refl ? (S o))
     96    ]).
     97  [ 1,2: destruct
     98  |*:
     99    @ injective_S @sym_eq @prf
     100  ]
     101qed.
  • src/Cminor/semantics.ma

    r760 r761  
    134134].
    135135
     136definition init_locals : env → list ident → env ≝
     137foldr ?? (λid,en. add ?? en id Vundef).
     138
    136139definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    137140λge,st.
     
    149152    | St_assign id e ⇒
    150153        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    151         ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
     154        ! en' ← update ?? en id v;
     155        ret ? 〈tr, State f St_skip en' m sp k〉
    152156    | St_store chunk edst e ⇒
    153157        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
     
    204208        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    205209        ! en ← bind_params args (f_params f);
    206         ret ? 〈E0, State f (f_body f) en m' sp k〉
     210        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
    207211    | External fn ⇒
    208212        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     
    217221                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
    218222                | Some v ⇒ match dst with [ None ⇒ Error ?
    219                                           | Some id ⇒ OK ? (add ?? en id v) ]
     223                                          | Some id ⇒ update ?? en id v ]
    220224                ];
    221225        ret ? 〈E0, State f St_skip en' m sp k'〉
  • src/RTLabs/RTLabs-sem.ma

    r751 r761  
    4848definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    4949
     50definition init_locals : list register → register_env val ≝
     51foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     52
    5053definition reg_store ≝
    5154λreg,v,locals.
    52   OK ? (add RegisterTag val locals reg v)
    53 .
     55  update RegisterTag val locals reg v.
    5456
    5557let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
     
    5759[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
    5860| cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
    59   do locals' ← reg_store r v locals;
     61  let locals' ≝ add RegisterTag val locals r v in
    6062  params_store rst vst locals'
    6163] ].
     
    182184    match fd with
    183185    [ Internal fn ⇒
    184         ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
     186        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
    185187        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    186188        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
  • src/common/Identifiers.ma

    r757 r761  
    7070                              (match m with [ an_id_map m' ⇒ m' ]).
    7171
     72(* Always adds the identifier to the map. *)
    7273definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
    7374λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    7475                                           (match m with [ an_id_map m' ⇒ m' ])).
    7576
     77(* Only updates an existing entry; fails with an error otherwise. *)
     78definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
     79λtag,A,m,l,a.
     80  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
     81                    (match m with [ an_id_map m' ⇒ m' ]) with
     82  [ None ⇒ Error ? (* missing identifier *)
     83  | Some m' ⇒ OK ? (an_id_map tag A m')
     84  ].
    7685
  • src/utilities/Coqlib.ma

    r747 r761  
    599599(* * Mapping a function over an option type. *)
    600600
    601 definition option_map ≝ λA,B.λf:A→B.λv:option A.
    602   match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ].
     601include "utilities/option.ma".
    603602
    604603(*
Note: See TracChangeset for help on using the changeset viewer.