Changeset 761

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:

• ASM/BitVectorTrie.ma (modified) (2 diffs)
• Cminor/semantics.ma (modified) (4 diffs)
• Cminor/test/sum-bad.ma (added)
• RTLabs/RTLabs-sem.ma (modified) (3 diffs)
• common/Identifiers.ma (modified) (1 diff)
• utilities/Coqlib.ma (modified) (1 diff)
• utilities/option.ma (added)

src/ASM/BitVectorTrie.ma

@@ -1 +1 @@
 include "basics/types.ma".
 
+include "utilities/option.ma".
 include "ASM/BitVector.ma".
 
@@ -75 +76 @@
   ]
 qed.
+
+let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
+  (match b with
+    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
+                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
+                   | Stub _ ⇒ λ_. None ?
+                   | Node _ _ _ ⇒ λprf. ⊥
+                   ] (refl ? O)
+    | VCons o hd tl ⇒ λt.
+          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
+            [ Leaf l ⇒ λprf.⊥
+            | Node p l r ⇒ λprf.
+               match hd with
+                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
+                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
+                ]
+            | Stub p ⇒ λprf. None ?
+            ] (refl ? (S o))
+    ]).
+  [ 1,2: destruct
+  |*:
+    @ injective_S @sym_eq @prf
+  ]
+qed.

src/Cminor/semantics.ma

@@ -134 +134 @@
 ].
 
+definition init_locals : env → list ident → env ≝
+foldr ?? (λid,en. add ?? en id Vundef).
+
 definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
 λge,st.
@@ -149 +152 @@
     | St_assign id e ⇒
         ! 〈tr,v〉 ← eval_expr ge e en sp m;
-        ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
+        ! en' ← update ?? en id v;
+        ret ? 〈tr, State f St_skip en' m sp k〉
     | St_store chunk edst e ⇒
         ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
@@ -204 +208 @@
         let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
         ! en ← bind_params args (f_params f);
-        ret ? 〈E0, State f (f_body f) en m' sp k〉
+        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
     | External fn ⇒
         ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
@@ -217 +221 @@
                 [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
                 | Some v ⇒ match dst with [ None ⇒ Error ?
-                                          | Some id ⇒ OK ? (add ?? en id v) ]
+                                          | Some id ⇒ update ?? en id v ]
                 ];
         ret ? 〈E0, State f St_skip en' m sp k'〉

src/RTLabs/RTLabs-sem.ma

@@ -48 +48 @@
 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
 
+definition init_locals : list register → register_env val ≝
+foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
+
 definition reg_store ≝
 λreg,v,locals.
-  OK ? (add RegisterTag val locals reg v)
-.
+  update RegisterTag val locals reg v.
 
 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
@@ -57 +59 @@
 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
 | cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
-  do locals' ← reg_store r v locals;
+  let locals' ≝ add RegisterTag val locals r v in
   params_store rst vst locals'
 ] ].
@@ -182 +184 @@
     match fd with
     [ Internal fn ⇒
-        ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
+        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉

src/common/Identifiers.ma

@@ -70 +70 @@
                               (match m with [ an_id_map m' ⇒ m' ]).
 
+(* Always adds the identifier to the map. *)
 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
                                            (match m with [ an_id_map m' ⇒ m' ])).
 
+(* Only updates an existing entry; fails with an error otherwise. *)
+definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
+λtag,A,m,l,a.
+  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
+                    (match m with [ an_id_map m' ⇒ m' ]) with
+  [ None ⇒ Error ? (* missing identifier *)
+  | Some m' ⇒ OK ? (an_id_map tag A m')
+  ].
 

src/utilities/Coqlib.ma

@@ -599 +599 @@
 (* * Mapping a function over an option type. *)
 
-definition option_map ≝ λA,B.λf:A→B.λv:option A.
-  match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ].
+include "utilities/option.ma".
 
 (*