Changeset 2562 for src/joint


Ignore:
Timestamp:
Dec 19, 2012, 10:38:43 AM (7 years ago)
Author:
piccolo
Message:

linearise modified

Location:
src/joint
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2561 r2562  
    136136
    137137inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    138   | step_seq : joint_seq p globals → joint_step p globals
    139138  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    140   | COND: acc_a_reg p → label → joint_step p globals.
     139  | COND: acc_a_reg p → label → joint_step p globals
     140  | step_seq : joint_seq p globals → joint_step p globals.
    141141
    142142coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
  • src/joint/Traces.ma

    r2561 r2562  
    7979  (* use exit_pc as ra and call_dest_for_main as dest *)
    8080  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    81   ! st0_no_pc ← save_frame ?? sem_globals call_id (call_dest_for_main … pars) st0' ;
     81  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    8282  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8383  ! bl ← block_of_call … ge (inl … main) st0'';
     
    160160    normalize nodelta ]
    161161  #ABS destruct(ABS) ]
    162 * [ #s | #f' #args #dest | #a #lbl ] #nxt #fetch >m_return_bind
     162* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    163163normalize nodelta
    164 [1,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     164[2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    165165whd in match joint_classify_step;
    166166normalize nodelta
  • src/joint/linearise.ma

    r2547 r2562  
    1414      if nxt ∈ visited then FCOND … I a ltrue nxt else
    1515      sequential (mk_lin_params p) … c it
    16     | _ ⇒ sequential … c it
     16    | _ ⇒ sequential (mk_lin_params p) … c it
    1717    ]
    1818  | final c ⇒ final … c
     
    8888               [ sequential s' nxt ⇒
    8989                 match s' with
    90                  [ step_seq _ ⇒
     90                 [ COND a ltrue ⇒
     91                   Or
     92                    (And (nth_opt … n (rev … generated') =
     93                            Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
     94                         (lookup … visited' nxt = Some ? (S n)))
     95                    (nth_opt … n (rev … generated') =
     96                            Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     97                 |  _ ⇒
    9198                   And
    9299                     (nth_opt … n (rev … generated') =
     
    95102                      (nth_opt … (S n) (rev … generated') =
    96103                       Some ? 〈None ?, GOTO … nxt〉))
    97                  | COND a ltrue ⇒
    98                    Or
    99                     (And (nth_opt … n (rev … generated') =
    100                             Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
    101                          (lookup … visited' nxt = Some ? (S n)))
    102                     (nth_opt … n (rev … generated') =
    103                             Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     104               
    104105                 ]
    105106               | final s' ⇒
     
    140141       [ sequential s' nxt ⇒
    141142         match s' with
    142          [ step_seq _ ⇒
    143            And
    144              (nth_opt … n (rev … generated) =
    145                 Some ? 〈Some ? l, sequential … s' it〉)
    146              (match lookup … visited nxt with
    147               [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉)
    148               | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
    149               ])
    150          | COND a ltrue ⇒
     143         [ COND a ltrue ⇒
    151144           Or
    152145            (And (nth_opt … n (rev … generated) =
     
    158151            (nth_opt … n (rev … generated) =
    159152                    Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     153         | _ ⇒
     154           And
     155             (nth_opt … n (rev … generated) =
     156                Some ? 〈Some ? l, sequential … s' it〉)
     157             (match lookup … visited nxt with
     158              [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉)
     159              | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
     160              ])
    160161         ]
    161162       | final s' ⇒
     
    220221           match s with [ COND _ _ ⇒ True | _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ]
    221222         | _ ⇒ True] → P 〈0,∅,[ ]〉) →
    222         (∀s,nxt.
    223           statement = sequential … (step_seq … s) nxt →
    224           nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) →
     223        (∀nxt.match statement with
     224         [ sequential s nxt' ⇒
     225          match s with [ COND _ _ ⇒ False | _ ⇒
     226            nxt = nxt']
     227         | _ ⇒ False]
     228         → nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) →
    225229        P add_req_gen ≝ hide_prf ?? in
    226230      graph_visit ???
     
    233237    ] n_prf
    234238  ] (chop_ok ? (λx.x∈visited) visiting).
    235 cases daemon qed. (*)
    236239whd
    237240[ (* base case, visiting is all visited *)
     
    253256    cases s in H3; [3: *]
    254257    [ * ] normalize nodelta
    255     [ #s' #nxt * #EQnth_opt #H %{EQnth_opt}
     258    [1,3: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    256259      inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
    257260      normalize nodelta *
     
    323326|12: (* add_req_gen utility *)
    324327  #P whd in match add_req_gen;
    325   cases statement [ * ] [|*: [ #a #ltrue #lfalse | #s | * ] #H #_ @(H I) ]
    326   #s #nxt normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
    327   #H1 #H2 [ @(H2 … (refl …)) >EQ % | @H1 % * ]
     328  cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
     329[2,4: normalize nodelta #H #_ @(H I) ]
     330  normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
     331  #H1 #H2 [1,3: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
    328332|3: elim H #pre ** #H1 #H2 #_
    329333  #i >mem_set_union
    330334  #H elim (orb_Prop_true … H) -H
    331335  [ @add_req_gen_prf [ #_ >mem_set_empty * ]
    332     #s #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
     336    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    333337  | >mem_set_union
    334338    #H elim (orb_Prop_true … H) -H
    335339    [ #i_expl %1 @Exists_append_l
    336340      lapply i_expl whd in match translated_statement;
    337       cases statement [ * [ #s | #a #ltrue ] #nxt | #s | *] normalize nodelta #H
     341      cases statement [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | *] normalize nodelta #H
    338342      lapply (mem_list_as_set … H) -H #H
    339       [1,3: @Exists_append_r assumption ]
     343      [1,3,4: @Exists_append_r assumption ]
    340344      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
    341345      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
     
    386390        #i_l @orb_Prop_r @orb_Prop_l assumption
    387391      | @add_req_gen_prf
    388         [ #_ | #s #next #_ #next_vis *
     392        [ #_ | #next #_ #next_vis *
    389393          [ whd in ⊢ (??%?→?);
    390394            #EQ' destruct(EQ') whd %{I} >mem_set_union
     
    405409        @add_req_gen_prf
    406410        [ #_
    407         | #s #next #_ #next_vis
     411        | #next #_ #next_vis
    408412          change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    409413          <associative_append >occurs_exactly_once_None
     
    420424          change with statement in match (lookup_safe ?????);
    421425          cases statement;
    422           [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    423           [1,2: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
    424           [1,2: % | %2 | %1 % ]
    425           [1,3,5,6,8:
     426          [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     427          [1,2,3: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
     428          [1,2,5,6: % | %2 | %1 % ]
     429          [1,3,5,7,9,10,12:
    426430            >nth_opt_append_r >rev_length <gen_length_prf try %
    427431            <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta
     
    429433          |*:
    430434            lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta
    431             [ * #n' ] #EQlookup >EQlookup normalize nodelta
    432             [ %2 >nth_opt_append_r >rev_length <gen_length_prf [2: %2 %1 ]
     435            [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta
     436            [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ]
    433437              <minus_Sn_n %
    434438            |*: %%
     
    448452          normalize nodelta >lin_code_has_label in G1; #K @K
    449453        | @add_req_gen_prf
    450           [ #_ % | #s' #next #_ #_ % ]
     454          [ #_ % |  #next #_ #_ % ]
    451455        ]
    452456      | %{s}
    453457        %{G2}
    454458        cases s in G3;
    455         [ * [ #s | #a #ltrue ] #nxt | #s | * ]
    456         [ * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
    457         [1,3,5,6: @nth_opt_append_hit_l assumption
    458         |*: @(eq_identifier_elim … nxt vis_hd)
     459        [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
     460        [1,3: * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
     461        [1,3,5,7: @nth_opt_append_hit_l assumption
     462        |2,4,6: @(eq_identifier_elim … nxt vis_hd)
    459463          [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ]
    460464            lapply (in_map_domain … visited vis_hd)
     
    506510|
    507511]
    508 qed. *)
     512qed.
    509513
    510514(* CSC: The branch compression (aka tunneling) optimization is not implemented
  • src/joint/semantics.ma

    r2561 r2562  
    153153
    154154inductive call_kind : Type[0] ≝
    155 | call_ptr : call_kind
    156 | call_id : call_kind.
     155| PTR : call_kind
     156| ID : call_kind.
    157157
    158158definition kind_of_call :
    159159  ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝
    160   λp,f.match f with [ inl _ ⇒ call_id | inr _ ⇒ call_ptr ].
     160  λp,f.match f with [ inl _ ⇒ ID | inr _ ⇒ PTR ].
    161161
    162162record sem_unserialized_params
Note: See TracChangeset for help on using the changeset viewer.