Changeset 1070 for src/Cminor/toRTLabs.ma

Timestamp:

Jul 15, 2011, 12:56:48 PM (10 years ago)

Author:

campbell

Message:

Show that entry and exit labels are in the RTLabs graph.

File:

• src/Cminor/toRTLabs.ma (modified) (7 diffs)

src/Cminor/toRTLabs.ma

@@ -26 +26 @@
   mk_internal_function (f_labgen f) (f_reggen f)
                        (f_result f) (f_params f) (f_locals f)
-                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
+                       (f_stacksize f) (add ?? (f_graph f) l s)
+                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
+@lookup_add_oblivious [ cases (f_entry f) | cases (f_exit f) ] //
+qed.
 
 (* Add a statement to the graph, making it the entry label. *)
@@ -33 +36 @@
   mk_internal_function (f_labgen f) (f_reggen f)
                        (f_result f) (f_params f) (f_locals f)
-                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
+                       (f_stacksize f) (add ?? (f_graph f) l s)
+                       (dp ?? l ?) (dp ?? (f_exit f) ?).
+[ %{s} @lookup_add_hit
+| @lookup_add_oblivious cases (f_exit f) //
+] qed.
 
 (* Add a statement with a fresh label to the start of the function.  The
@@ -43 +50 @@
     (mk_internal_function g (f_reggen f)
                        (f_result f) (f_params f) (f_locals f)
-                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
-
+                       (f_stacksize f) (add ?? (f_graph f) l s')
+                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
+[ %{s'} @lookup_add_hit
+| @lookup_add_oblivious cases (f_exit f) //
+] qed.
+(*
 (* Generate a fresh label and use it as a dangling entry point, to be filled in
    later with the loop head. *)
@@ -53 +64 @@
                        (f_result f) (f_params f) (f_locals f)
                        (f_stacksize f) (f_graph f) l (f_exit f)).
-
+*)
 definition fresh_reg : internal_function → typ → register × internal_function ≝
 λf,ty.
@@ -189 +200 @@
     add_expr env ? e r f
 | St_loop s ⇒
-    let f ≝ add_loop_label_to_graph f in
+    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
     let l_loop ≝ f_entry f in
     do f ← add_stmt env label_env s exits f;
@@ -235 +246 @@
 [ @(λ_. St_skip l_next)
 | @(St_skip (f_entry f))
+| @St_skip
 | @(λ_. St_skip l)
 | @(λ_. St_skip l_default)
@@ -284 +296 @@
 OK ? f
 .
+% [2,4: @lookup_add_hit | *: skip ]
+qed.
 
 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝