Changeset 1070 for src/Cminor


Ignore:
Timestamp:
Jul 15, 2011, 12:56:48 PM (8 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1056 r1070  
    2626  mk_internal_function (f_labgen f) (f_reggen f)
    2727                       (f_result f) (f_params f) (f_locals f)
    28                        (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
     28                       (f_stacksize f) (add ?? (f_graph f) l s)
     29                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
     30@lookup_add_oblivious [ cases (f_entry f) | cases (f_exit f) ] //
     31qed.
    2932
    3033(* Add a statement to the graph, making it the entry label. *)
     
    3336  mk_internal_function (f_labgen f) (f_reggen f)
    3437                       (f_result f) (f_params f) (f_locals f)
    35                        (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
     38                       (f_stacksize f) (add ?? (f_graph f) l s)
     39                       (dp ?? l ?) (dp ?? (f_exit f) ?).
     40[ %{s} @lookup_add_hit
     41| @lookup_add_oblivious cases (f_exit f) //
     42] qed.
    3643
    3744(* Add a statement with a fresh label to the start of the function.  The
     
    4350    (mk_internal_function g (f_reggen f)
    4451                       (f_result f) (f_params f) (f_locals f)
    45                        (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
    46 
     52                       (f_stacksize f) (add ?? (f_graph f) l s')
     53                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
     54[ %{s'} @lookup_add_hit
     55| @lookup_add_oblivious cases (f_exit f) //
     56] qed.
     57(*
    4758(* Generate a fresh label and use it as a dangling entry point, to be filled in
    4859   later with the loop head. *)
     
    5364                       (f_result f) (f_params f) (f_locals f)
    5465                       (f_stacksize f) (f_graph f) l (f_exit f)).
    55 
     66*)
    5667definition fresh_reg : internal_function → typ → register × internal_function ≝
    5768λf,ty.
     
    189200    add_expr env ? e r f
    190201| St_loop s ⇒
    191     let f ≝ add_loop_label_to_graph f in
     202    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    192203    let l_loop ≝ f_entry f in
    193204    do f ← add_stmt env label_env s exits f;
     
    235246[ @(λ_. St_skip l_next)
    236247| @(St_skip (f_entry f))
     248| @St_skip
    237249| @(λ_. St_skip l)
    238250| @(λ_. St_skip l_default)
     
    284296OK ? f
    285297.
     298% [2,4: @lookup_add_hit | *: skip ]
     299qed.
    286300
    287301definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
Note: See TracChangeset for help on using the changeset viewer.