Changeset 1070


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.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1052 r1070  
    358358qed.
    359359
     360lemma lookup_opt_prepare_trie_for_insertion_miss:
     361 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.
     362  (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?.
     363 #A #v #n #c elim c
     364  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     365  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     366    cases hd cases hd' normalize
     367    [2,3: #_ cases tl' //
     368    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]]
     369qed.
     370
    360371lemma lookup_opt_insert_hit:
    361372 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     
    374385 ]
    375386qed.
    376    
     387
     388lemma lookup_opt_insert_miss:
     389 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     390  (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t.
     391 #A #v #n #c elim c -c -n
     392  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     393  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     394    #t cases(BitVectorTrie_Sn … t)
     395    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     396     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     397    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     398     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     399     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
     400qed.
     401
    377402lemma forall_insert_inv1:
    378403  ∀A.∀n.∀b.∀a.∀t.∀P.
  • 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 ≝
  • src/RTLabs/syntax.ma

    r1056 r1070  
    3535; f_stacksize : nat
    3636; f_graph     : graph statement
    37 ; f_entry     : label
    38 ; f_exit      : label
     37; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
     38; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
    3939}.
    4040
  • src/common/Identifiers.ma

    r1068 r1070  
    4343  else OK ? it.
    4444
    45 definition eq_identifier ≝
    46   λt.
    47   λl, r: identifier t.
     45definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     46  λt,l,r.
    4847  match l with
    4948  [ an_identifier l' ⇒
     
    5352    ]
    5453  ].
     54
     55lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
     56  (x = y → P true) → (x ≠ y → P false) →
     57  P (eq_identifier t x y).
     58#P #t * #x * #y #T #F
     59change with (P (eq_bv ???))
     60@eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
     61qed.
    5562   
    5663definition word_of_identifier ≝
     
    9097λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    9198                                           (match m with [ an_id_map m' ⇒ m' ])).
     99
     100lemma lookup_add_hit : ∀tag,A,m,i,a.
     101  lookup tag A (add tag A m i a) i = Some ? a.
     102#tag #A * #m * #i #a
     103@lookup_opt_insert_hit
     104qed.
     105
     106lemma lookup_add_miss : ∀tag,A,m,i,j,a.
     107  (notb (eq_identifier tag i j)) →
     108  lookup tag A (add tag A m j a) i = lookup tag A m i.
     109#tag #A * #m * #i * #j #a
     110change with (notb (eq_bv ???) → ?)
     111@lookup_opt_insert_miss
     112qed.
     113
     114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
     115  (∃v. lookup tag A m i = Some ? v) →
     116  ∃v. lookup tag A (add tag A m j a) i = Some ? v.
     117#tag #A #m #i #j #a * #v #H
     118lapply (lookup_add_miss … m i j a)
     119@eq_identifier_elim
     120[ #E #_ %{a} >E @lookup_add_hit
     121| #_ #H' %{v} <H @H' %
     122] qed.
    92123
    93124(* Extract every identifier, value pair from the map. *)
Note: See TracChangeset for help on using the changeset viewer.