Changeset 2532


Ignore:
Timestamp:
Dec 5, 2012, 6:57:16 PM (7 years ago)
Author:
tranquil
Message:

added FCOND in LIN, and rewritten linearise so that it never adds a GOTO after a COND (writes in FCOND instead)
LIN to ASM is broken atm

Location:
src/joint
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2490 r2532  
    8080 ; snd_arg : Type[0]  (* second argument of binary op *)
    8181 ; pair_move: Type[0] (* argument of move instructions *)
     82 ; call_spec: Type[0] (* type of call (ident/pointer) *)
    8283 ; call_args: Type[0] (* arguments of function calls *)
    8384 ; call_dest: Type[0] (* possible destination of function computation *)
    8485 (* other instructions not fitting in the general framework *)
    8586 ; ext_seq : Type[0]
     87 ; ext_seq_labels : ext_seq → list label
    8688 ; has_tailcalls : bool
    8789 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     
    106108  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    107109  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    108   | CALL: (ident + dpl_arg p×(dph_arg p)) → call_args p → call_dest p → joint_seq p globals
     110  | CALL: call_spec p → call_args p → call_dest p → joint_seq p globals
    109111  | extension_seq : ext_seq p → joint_seq p globals.
    110112
     
    145147  λp, globals.λs : joint_step p globals.
    146148  match s with
    147   [ step_seq s ⇒ [ ]
     149  [ step_seq s ⇒
     150    match s with
     151    [ extension_seq ext ⇒ ext_seq_labels … ext
     152    | _ ⇒ [ ]
     153    ]
    148154  | COND _ l ⇒ [l]
    149155  ].
     
    157163  ; succ : Type[0]
    158164  ; succ_label : succ → option label
    159   }.
     165  ; has_fcond : bool
     166  }.
    160167
    161168inductive joint_fin_step (p: unserialized_params): Type[0] ≝
     
    163170  | RETURN: joint_fin_step p
    164171  | TAILCALL :
    165     has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p))
     172    has_tailcalls p → call_spec p
    166173    call_args p → joint_fin_step p.
    167174
     
    174181inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    175182  | sequential: joint_step p globals → succ p → joint_statement p globals
    176   | final: joint_fin_step p → joint_statement p globals.
     183  | final: joint_fin_step p → joint_statement p globals
     184  | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals.
    177185
    178186coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     
    193201
    194202(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
    195 
     203(*
    196204definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
    197205unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
     
    206214  ]. normalize in pt_prf;
    207215    >abs in pt_prf; // qed.
     216*)
    208217
    209218definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     
    234243  [ sequential c _ ⇒ step_labels … c
    235244  | final c ⇒ fin_step_labels … c
     245  | FCOND _ _ l1 l2 ⇒ [l1 ; l2]
    236246  ].
    237247
     
    316326  λlp : lin_params.
    317327     mk_params
    318       (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
     328      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true)
    319329    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    320330    (* code_point ≝ *)ℕ
     
    358368  λgp : graph_params.
    359369     mk_params
    360       (mk_stmt_params (g_u_pars gp) label (Some ?))
     370      (mk_stmt_params (g_u_pars gp) label (Some ?) false)
    361371    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    362372    (* code_point ≝ *)label
     
    403413  joint_if_stacksize: nat;
    404414  joint_if_code     : codeT p globals ;
    405   joint_if_entry : point_in_code … joint_if_code ;
    406   joint_if_exit : point_in_code … joint_if_code
     415  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;
     416  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt)
    407417}.
    408418
  • src/joint/TranslateUtils.ma

    r2443 r2532  
    270270    | final inst ⇒
    271271      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
     272    | FCOND abs _ _ _ ⇒ Ⓧabs
    272273    ] in
    273274  foldi … f (joint_if_code … def) empty.
     
    297298    | final inst ⇒
    298299      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
     300    | FCOND abs _ _ _ ⇒ Ⓧabs
    299301    ] in
    300302  foldi … f (joint_if_code … def) empty.
  • src/joint/linearise.ma

    r2529 r2532  
    1 include "joint/TranslateUtils.ma".
    2 include "common/extraGlobalenvs.ma".
     1(* include "joint/TranslateUtils.ma". *)
     2include "joint/Joint.ma".
    33include "utilities/hide.ma".
    44
    55definition graph_to_lin_statement :
    66  ∀p : unserialized_params.∀globals.
     7  ∀A.identifier_map LabelTag A →
    78  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
    8   λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params ?) ? with
    9   [ sequential c _ ⇒ sequential … c it
     9  λp,globals,A,visited,stmt.
     10  match stmt return λ_.joint_statement (mk_lin_params ?) ? with
     11  [ sequential c nxt ⇒
     12    match c with
     13    [ COND a ltrue ⇒
     14      if nxt ∈ visited then FCOND … I a ltrue nxt else
     15      sequential (mk_lin_params p) … c it
     16    | _ ⇒ sequential … c it
     17    ]
    1018  | final c ⇒ final … c
     19  | FCOND abs _ _ _ ⇒ Ⓧabs
    1120  ].
    1221
     22(*
    1323lemma graph_to_lin_labels :
    1424  ∀p : unserialized_params.∀globals,s.
     
    1727#p#globals * [//] * //
    1828qed.
     29*)
    1930
    2031(* discard all elements passing test, return first element failing it *)
     
    5970list lo ≡ codeT lp globals.
    6071
    61 
    6272definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
    6373  λentry : label.
     
    6878        (lookup ?? visited' entry = Some ? 0)
    6979        (required' ⊆ visited'))
    70         (∃last.stmt_at … generated' 0 = Some ? (final … last)))
     80        ((∃last.stmt_at … generated' 0 = Some ? (final … last)) ∨
     81         (∃a,ltrue,lfalse.stmt_at … generated' 0 = Some ? (FCOND … I a ltrue lfalse))))
    7182        (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated')))
    7283        (∀l,n.lookup ?? visited' l = Some ? n →
    7384          And (bool_to_Prop (code_has_label … (rev ? generated') l))
    74             (∃s.And (And
     85            (∃s.And
    7586              (lookup … g l = Some ? s)
    76               (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
    77               (opt_All ?
    78                 (λnext.Or (lookup … visited' next = Some ? (S n))
    79                   (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
    80                 (stmt_implicit_label … s)))))).
     87              (match s with
     88               [ sequential s' nxt ⇒
     89                 match s' with
     90                 [ step_seq _ ⇒
     91                   And
     92                     (nth_opt … n (rev … generated') =
     93                        Some ? 〈Some ? l, sequential … s' it〉)
     94                     (Or (lookup … visited' nxt = Some ? (S n))
     95                      (nth_opt … (S n) (rev … generated') =
     96                       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                 ]
     105               | final s' ⇒
     106                  nth_opt … n (rev … generated') =
     107                            Some ? 〈Some ? l, final … s'〉
     108               | FCOND abs _ _ _ ⇒ Ⓧabs
     109               ]))))).
    81110               
    82111unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
     
    85114
    86115lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
    87   (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
    88 #tag #A #P #m #i #prf #H @H @lookup_eq_safe qed.
     116  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf) ≝
     117λtag,A,P,m,i,prf,H.(H … (lookup_eq_safe …)).
    89118
    90119let rec graph_visit
     
    106135  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
    107136    And (bool_to_Prop (code_has_label … (rev ? generated) l))
    108     (∃s.And (And
     137    (∃s.And
    109138      (lookup … g l = Some ? s)
    110       (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
    111       (opt_All ? (λnext.match lookup … visited next with
    112                      [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
    113                      | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
     139      (match s with
     140       [ sequential s' nxt ⇒
     141         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 ⇒
     151           Or
     152            (And (nth_opt … n (rev … generated) =
     153                    Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
     154                 (match lookup … visited nxt with
     155                  [ Some n' ⇒ n' = S n
     156                  | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
     157                  ]))
     158            (nth_opt … n (rev … generated) =
     159                    Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     160         ]
     161       | final s' ⇒
     162          nth_opt … n (rev … generated) =
     163                    Some ? 〈Some ? l, final … s'〉
     164       | FCOND abs _ _ _ ⇒ Ⓧabs
     165       ]))))
    114166  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
    115167  (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨
     168     (∃a,ltrue,lfalse.stmt_at … generated 0 = Some ? (FCOND … a ltrue lfalse)) ∨
    116169     (¬All ? (λx.bool_to_Prop (x∈visited)) visiting))
    117170  (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting)
     
    138191      let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in 
    139192      (* translate it to its linear version *)
    140       let translated_statement ≝ graph_to_lin_statement p globals statement in
     193      let translated_statement ≝ graph_to_lin_statement … visited' statement in
    141194      (* add the translated statement to the code (which will be reversed later) *)
    142195      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
    143       let required' ≝ union_set ??? (set_from_list … (stmt_explicit_labels … statement)) required in
     196      let required' ≝ union_set ???
     197        (set_from_list … (stmt_explicit_labels … translated_statement))
     198        required in
    144199      (* put successors in the visiting worklist *)
    145200      let visiting' ≝ stmt_labels … statement @ vis_tl in
     
    147202      (* if it has been already visited, we need to add a GOTO *)
    148203      let add_req_gen ≝
    149         match stmt_implicit_label … statement
    150         with
    151         [ Some next ⇒
    152           if next ∈ visited' then
    153             〈1, {(next)}, [〈None label, (GOTO … next : joint_statement ??)〉]〉
    154           else 〈0, ∅, [ ]〉
    155         | None ⇒ 〈0, ∅, [ ]〉
     204        match statement with
     205        [ sequential s nxt ⇒
     206          match s with
     207          [ COND _ _ ⇒ 〈0, ∅, [ ]〉
     208          | _ ⇒
     209            if nxt ∈ visited' then
     210              〈1, {(nxt)}, [〈None label, (GOTO … nxt : joint_statement ??)〉]〉
     211            else 〈0, ∅, [ ]〉
     212          ]
     213        | _ ⇒ 〈0, ∅, [ ]〉
    156214        ] in
    157215      (* prepare a common utility to deal with add_req_gen *)
    158216      let add_req_gen_prf :
    159217        ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop.
    160         (opt_All ? (λnext.¬bool_to_Prop (next ∈ visited')) (stmt_implicit_label … statement) →
    161          P 〈0,∅,[ ]〉) →
    162         (∀next.stmt_implicit_label … statement = Some ? next →
    163           next ∈ visited' →
    164           P 〈1, {(next)}, [〈None ?, GOTO (mk_lin_params p) next〉]〉) →
     218        (match statement with
     219         [ sequential s nxt ⇒
     220           match s with [ COND _ _ ⇒ True | _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ]
     221         | _ ⇒ 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〉]〉) →
    165225        P add_req_gen ≝ hide_prf ?? in
    166226      graph_visit ???
     
    186246    | assumption
    187247    ]
    188   | cases generated_prf3 [//]
     248  | cases generated_prf3 [/2 by /]
    189249    * #ABS @⊥ @ABS assumption
    190250  | assumption
    191   | #l #n #H elim (generated_prf1 … H)
    192     #H1 * #s ** #H2 #H3 #H4
    193     % [assumption] %{s} %
    194     [% assumption
    195     | @(opt_All_mp … H4) -l #l
    196       lapply (in_map_domain … visited l)
    197       elim (true_or_false_Prop (l∈visited)) #l_vis >l_vis
    198       normalize nodelta [ * #n' ] #EQlookup >EQlookup
     251  | #l #n #H elim (generated_prf1 … H) -H
     252    #H1 * #s * #H2 #H3 %{H1} %{s} %{H2}
     253    cases s in H3; [3: *]
     254    [ * ] normalize nodelta
     255    [ #s' #nxt * #EQnth_opt #H %{EQnth_opt}
     256      inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
    199257      normalize nodelta *
    200       [ #EQn' % >EQn' %
     258      [ #EQn' %1 >EQn' %
    201259      | #H %2{H}
    202       | #H' lapply (All_nth … H … H') >l_vis *
     260      | #H' lapply (All_nth … H … H')
     261        whd in ⊢ (?%→?); >EQlookup *
    203262      ]
     263    | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
     264      inversion (lookup … visited lfalse) in H2;
     265      [ #ABS * #H' lapply (All_nth … H … H')
     266        whd in ⊢ (?%→?); >ABS *
     267      | #n' #_ normalize nodelta #EQ >EQ %
     268      ]
     269    | #s #H @H
    204270    ]
    205271  ]
     
    220286    #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) %
    221287  | #l #H
    222     elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s ** #s_in_g #_ #_
     288    elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s * #s_in_g #_
    223289    whd in ⊢ (?%); >s_in_g %
    224290  ]
     
    228294  [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2
    229295    @(All_append … G1)
    230     whd in G2; lapply G2 elim statement normalize nodelta #s [2: #_ %]
    231     #l #G' %{G'} %
     296    cases statement in G2; [2: // |3: * ]
     297    #s #nxt #G' %{G'} %
    232298  | >H2 in visiting_prf;
    233299    #H' lapply (All_append_r … H') -H' * #_ //
     
    257323|12: (* add_req_gen utility *)
    258324  #P whd in match add_req_gen;
    259   elim (stmt_implicit_label ???)
    260   [ #H #_ @H % ]
    261   #next normalize nodelta elim (true_or_false_Prop (next ∈ visited')) #next_vis
    262   >next_vis normalize nodelta
    263   [ #_ #H @H [% | assumption]
    264   | #H #_ @H whd >next_vis % *
    265   ]
    266 | elim H #pre ** #H1 #H2 #_
     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|3: elim H #pre ** #H1 #H2 #_
    267329  #i >mem_set_union
    268330  #H elim (orb_Prop_true … H) -H
    269331  [ @add_req_gen_prf [ #_ >mem_set_empty * ]
    270     #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
     332    #s #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    271333  | >mem_set_union
    272334    #H elim (orb_Prop_true … H) -H
    273     [ #i_expl %1 @Exists_append_l @Exists_append_r
    274       @mem_list_as_set
    275       @i_expl
     335    [ #i_expl %1 @Exists_append_l
     336      lapply i_expl whd in match translated_statement;
     337      cases statement [ * [ #s | #a #ltrue ] #nxt | #s | *] normalize nodelta #H
     338      lapply (mem_list_as_set … H) -H #H
     339      [1,3: @Exists_append_r assumption ]
     340      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
     341      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
    276342    | (* i was already required *)
    277343      #i_req
     
    280346        [ (* i in preamble → i∈visited *)
    281347          #i_pre %2 >mem_set_add @orb_Prop_r
    282           lapply (All_In … H1 i_pre) #H @H
     348          @(All_In … H1 i_pre)
    283349        | *
    284350          [ (* i is vis_hd *)
     
    307373      cases (pt - ?)
    308374      [ whd in match (nth_opt ???); whd in ⊢ (??%?→?);
    309         #EQ destruct(EQ) whd
    310         >graph_to_lin_labels in ⊢ (???%);
     375        #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) whd
    311376        whd in match required';
    312         generalize in match (stmt_explicit_labels … statement);
     377        cut (∀p : lin_params.∀globals.∀s.
     378          stmt_implicit_label p globals s = None ?)
     379        [ #p #globals * normalize // ]
     380        #lin_implicit_label change with (? @ ?) in match (stmt_labels ???);
     381        >lin_implicit_label
     382        change with (All ?? (stmt_explicit_labels ???))
     383        generalize in match (stmt_explicit_labels … translated_statement);
    313384        #l @list_as_set_All
    314385        #i >mem_set_union >mem_set_union
    315         #i_l @orb_Prop_r @orb_Prop_l @i_l
     386        #i_l @orb_Prop_r @orb_Prop_l assumption
    316387      | @add_req_gen_prf
    317         [ #_ | #next #_ #next_vis *
     388        [ #_ | #s #next #_ #next_vis *
    318389          [ whd in ⊢ (??%?→?);
    319390            #EQ' destruct(EQ') whd %{I} >mem_set_union
     
    326397    @(eq_identifier_elim … i vis_hd)
    327398    [ #EQi >EQi -i #pos
    328       >lookup_add_hit #EQpos (* too slow: destruct(EQpos) *)
     399      >lookup_add_hit in ⊢ (%→?); #EQpos (* too slow: destruct(EQpos) *)
    329400      cut (gen_length = pos)
    330       [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
     401      [ -visited destruct(EQpos) %]
    331402      -EQpos #EQpos <EQpos -pos
    332403      %
     
    334405        @add_req_gen_prf
    335406        [ #_
    336         | #next #_ #next_vis
     407        | #s #next #_ #next_vis
    337408          change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    338409          <associative_append >occurs_exactly_once_None
     
    344415        >H3 normalize nodelta //
    345416      | %{statement}
    346         % [ % ]
     417        %
    347418        [ @lookup_eq_safe
    348         | <associative_append @nth_opt_append_hit_l
    349           >nth_opt_append_r
    350           >rev_length
    351           <gen_length_prf
    352           [<minus_n_n] %
    353         | @add_req_gen_prf
    354           [ lapply (refl … (stmt_implicit_label ?? statement))
    355             cases (stmt_implicit_label ???) in ⊢ (???%→%);
    356             [#_ #_ %]
    357             #next #K change with (¬bool_to_Prop (?∈?)→?) #next_vis
    358           | #next #K >K #next_vis
    359           ] whd
    360           >mem_set_add in next_vis;
    361           @eq_identifier_elim
    362           [1,3: #EQnext >EQnext * [#ABS elim(ABS I)]
    363             >lookup_add_hit
    364           |*: #NEQ >(lookup_add_miss … visited … NEQ)
    365             change with (?∈?) in match (false∨?);
    366             #next_vis lapply(in_map_domain … visited next) >next_vis
    367             whd in ⊢ (% → ?); [2: * #s ]
    368             #EQlookup >EQlookup
    369           ] whd
    370           [1,2: %2 <associative_append
    371             >nth_opt_append_r >append_length >rev_length >commutative_plus
    372             <gen_length_prf
    373             [1,3: <minus_n_n ] %
    374           | % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
    375             >K %
     419        | normalize nodelta
     420          change with statement in match (lookup_safe ?????);
     421          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            >nth_opt_append_r >rev_length <gen_length_prf try %
     427            <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta
     428            >nxt_vis %
     429          |*:
     430            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 ]
     433              <minus_Sn_n %
     434            |*: %%
     435            ]
    376436          ]
    377437        ]
     
    379439    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
    380440      #Hlookup elim (generated_prf1 … Hlookup)
    381       #G1 * #s ** #G2 #G3 #G4
     441      #G1 * #s * #G2 #G3
    382442      %
    383443      [ >lin_code_has_label <associative_append
     
    388448          normalize nodelta >lin_code_has_label in G1; #K @K
    389449        | @add_req_gen_prf
    390           [ #_ % | #next #_ #_ % ]
     450          [ #_ % | #s' #next #_ #_ % ]
    391451        ]
    392452      | %{s}
    393         % [ % ]
    394         [ assumption
    395         | @nth_opt_append_hit_l assumption
    396         | @(opt_All_mp … G4)
    397           #x
    398           @(eq_identifier_elim … x vis_hd) #Heq
    399           [ >Heq
     453        %{G2}
     454        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          [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ]
    400460            lapply (in_map_domain … visited vis_hd)
    401             >H3 normalize nodelta in ⊢ (%→?);
    402             #EQlookup >EQlookup * #nth_opt_visiting #gen_length_eq
    403             >lookup_add_hit %1 >gen_length_eq %
    404           | >(lookup_add_miss ?????? Heq)
    405             lapply (in_map_domain … visited x)
    406             elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis
    407             normalize nodelta in ⊢ (%→?); [ * #n' ]
    408             #EQlookupx >EQlookupx whd in ⊢ (%→%); *
    409             [ #G %1{G}
    410             | #G %2 @nth_opt_append_hit_l
    411               assumption
    412             | #G elim(absurd ?? Heq)
    413               (* BUG (but useless): -required -g -generated *)
    414               >H2 in G; lapply H1 cases pre
    415               [ #_
    416               | #hd #tl * #hd_vis #_
    417               ] normalize #EQ' destruct(EQ')
    418               [ %
    419               | >x_vis in hd_vis; *
     461            >H3 #EQ >EQ in next_spec; * #_ #OK >OK %
     462          |*: #NEQ' >(lookup_add_miss … visited … NEQ')
     463            lapply (in_map_domain … visited nxt)
     464            inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup'
     465            >EQlookup' in next_spec; whd in ⊢ (%→%);
     466            [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
     467            | #H @H
     468            |*: * >H2
     469              cases pre in H1;
     470              [1,3: #_
     471              |*: #frst #pre_tl * #ABS #_
     472              ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
     473              [1,2: cases NEQ' #ABS cases (ABS ?) %
     474              |*: >nxt_vis in ABS; *
    420475              ]
    421476            ]
     
    433488    | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?))
    434489      >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ]
    435       @add_req_gen_prf [ #_ | #next #_ #_ ] %
     490      @add_req_gen_prf [ #_ | #s #next #_ #_ ] %
    436491    ]
    437492  ]
    438493| @add_req_gen_prf
    439   [ #K | #next #K #next_vis %1 %{(GOTO … next)} % ]
     494  [ #K | #s #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
    440495  whd in match generated'; whd in match translated_statement;
    441   lapply K whd in match visiting';
    442   whd in match (stmt_labels ???); cases statement #last
    443   [2: #_ %1 %{last} % ] #next whd in ⊢ (%→?); #next_vis
    444   %2 % * >next_vis *
     496  normalize nodelta
     497  change with statement in match (lookup_safe ?????);
     498  cases statement in K;
     499  [ * [ #s | #a #ltrue ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
     500  [2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
     501    [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ]
     502  | #nxt_vis ]
     503  %2 % * >nxt_vis *
    445504| whd in match generated';
    446   @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf %
     505  @add_req_gen_prf [ #_ | #s #next #_ #_ ] normalize >gen_length_prf %
     506|
    447507]
    448508qed.
     
    567627    ∀l,n.sigma l = Some ? n →
    568628      ∃s. stmt_at … g l = Some ? s ∧
    569         All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
    570         opt_All ?
    571             (λnext.Or (sigma next = Some ? (S n))
    572             (stmt_at … c (S n) = Some ? (GOTO … next)))
    573             (stmt_implicit_label … s) ∧
    574         stmt_at … c n = Some ? (graph_to_lin_statement … s).
     629          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
     630          (match s with
     631           [ sequential s' nxt ⇒
     632             match s' with
     633             [ step_seq _ ⇒
     634               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     635                  ((sigma nxt = Some ? (S n)) ∨
     636                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
     637             | COND a ltrue ⇒
     638               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
     639               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     640             ]
     641           | final s' ⇒
     642             stmt_at … c n = Some ? (final … s')
     643           | FCOND abs _ _ _ ⇒ Ⓧabs
     644           ]).
    575645
    576646definition linearise_code:
     
    633703    lapply (in_map_domain … visited lbl) >(req_vis … H2)
    634704    * #n_lbl #EQsigma
    635     elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_
    636     >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H)
    637     [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
    638     | >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
     705    elim (sigma_prop … EQsigma) #_ * #stmt * #_
     706    cases stmt [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     707    [ * #EQnth_opt #_ | * [ * ] #EQnth_opt [ #_ ] | #EQnth_opt ]
     708    >(nth_opt_index_of_label ???? n_lbl ? H)
     709    [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
     710    |3: @(sequential … s it) |6: @(sequential … (COND … a ltrue) it)
     711    |9: @(FCOND … I a ltrue nxt) |12: @(final … s)
     712    |2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
    639713      >H2 %
    640714    ]
    641715  | #eq_lookup elim (sigma_prop ?? eq_lookup)
    642     #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
    643     % [2: % [ % [ % [ assumption ]]] |]
     716    #lbl_in_gen * #stmt * #stmt_in_g #stmt_spec
     717    % [2: % [ % [ assumption ]] |]
    644718    [ @All_append
    645       [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ]
    646         #nxt #nxt_spec % [2: %] cases nxt_spec -nxt_spec
    647         [ #EQ >EQ % #ABS destruct(ABS)
    648         | #goto_in lapply (in_map_domain … visited nxt)
    649           >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ]
    650           @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
    651           whd in ⊢ (??%?); >goto_in %
     719      [ cases stmt in stmt_spec;
     720        [ * [ #s | #a #ltrue ] #nxt | #s #_ % | * ]
     721        normalize nodelta * [ #stmt_at_EQ * #nxt_spec | * #stmt_at_EQ #nxt_spec | #stmt_at_EQ ]
     722        %{I}
     723        [1,3: >nxt_spec % #ABS destruct(ABS)
     724        |*: lapply (in_map_domain … visited nxt)
     725          >req_vis
     726          [1,3: * #x #EQ >EQ % #ABS destruct(ABS)
     727          |2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
     728            whd in ⊢ (??%?); >nxt_spec %
     729          |4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
     730            whd in ⊢ (??%?); >stmt_at_EQ %
     731          ]
    652732        ]
    653       | <graph_to_lin_labels @(All_mp … (labels_in_req …))
    654         [ #lbl #H
    655           lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS)
    656         | whd in ⊢ (??%?); >nth_opt_is_stmt % |
     733      | cases stmt in stmt_spec;
     734        [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     735        [ * #EQ #_ | * [ * #EQ #_ | #EQ ] | #EQ ]
     736        whd in match stmt_explicit_labels; normalize nodelta
     737        [ @(All_mp … (labels_in_req n (sequential … s it) ?))
     738        | @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?))
     739        | cases (labels_in_req n (FCOND … I a ltrue nxt) ?)
     740          [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue)
     741            >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ]
     742        | @(All_mp … (labels_in_req n (final … s) ?))
     743        ]
     744        [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS)
     745        |*: whd in ⊢ (??%?); >EQ %
    657746        ]
    658747      ]
    659     | lapply succ_is_in
    660       cases (stmt_implicit_label … stmt) [#_ %]
    661       #next *
    662       [ #H %1{H} ]
    663       #H %2
    664       >stmt_at_filter_labels whd in ⊢ (??%?); >H %
    665     | >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt %
     748    | cases stmt in stmt_spec;
     749      [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     750      [ * #EQ #H | * [ * #EQ #H | #EQ ] | #EQ ]
     751      >stmt_at_filter_labels
     752      whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta
     753      [ % [%] cases H -H [#H %1{H} | #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ]
     754      | %1 %{H} %
     755      | %2 %
     756      | %
     757      ]
    666758    ]
    667759  ]
     
    676768    elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req)))
    677769    >lin_code_has_label #H #_ @H
    678   | lapply EQ cases s #s' [2: #_ % ]
    679     * -EQ #EQ change with (bool_to_Prop (code_has_point ????))
     770  | lapply EQ cases s [ #s' * | #s' #_ % | * #a #ltrue #lfalse #_ % ]
     771    -EQ #EQ change with (bool_to_Prop (code_has_point ????))
    680772    whd in match (point_of_succ ???);
    681773    >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse
     
    687779      @(nth_opt_hit_length … EQ1)
    688780    ] #EQ_length
    689     elim last_fin #fin #EQ'
     781    elim last_fin * [ #fin | #a * #ltrue * #lfalse ] #EQ'
    690782    lapply EQ whd in match (stmt_at ????);
    691     >nth_opt_reverse_hit >EQ_length [2: % ] <minus_n_n
     783    >nth_opt_reverse_hit >EQ_length [2,4: % ] <minus_n_n
    692784    change with (stmt_at ???? = ? → ?)
    693785    >EQ' #ABS destruct(ABS)
     
    737829| @H1
    738830| cases H1 * #H3 #H4 #H5 elim (H5 … H3)
    739   #s *** #_ #_ #_ >lin_code_has_point cases code
    740   [ #ABS normalize in ABS; destruct(ABS) | #hd #tl #_ % ]
     831  #s ** #_ #_ >lin_code_has_point cases code
     832  [ cases s [ * [ #s' | #a #ltrue ] #nxt | #s' | * ]
     833    [ * #ABS #_ | * [ * #ABS #_ | #ABS ] | #ABS ] normalize in ABS; destruct(ABS)
     834  | #hd #tl #_ %
     835  ]
    741836]
    742837qed.
  • src/joint/semantics.ma

    r2529 r2532  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
    7 include "common/extraGlobalenvs.ma".
     7(* include "common/extraGlobalenvs.ma". *)
    88
    99(* CSC: external functions never fail (??) and always return something of the
     
    162162  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    163163  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    164 
     164 
    165165  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    166166  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
     
    177177
    178178  (* from now on, parameters that use the type of functions *)
    179   ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
     179  ; block_of_call : ∀globals.genv_t (fundef (F globals)) → call_spec uns_pars →
     180      state st_pars →  res (Σbl.block_region bl = Code)
     181  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars →
     182      state st_pars → res (list beval)
    180183  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    181184    ident → F globals (* current *) → state st_pars → res (state st_pars)
     
    374377  ] (refl …).
    375378
    376 definition block_of_call ≝ λp:sem_params.λglobals.
    377   λge: genv_t (joint_function p globals).λst : state p.λf.
    378   ! bl ← match f with
    379     [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id)
    380     | inr addr ⇒
    381       ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    382       ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    383       ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
    384       if eq_bv … (bv_zero …) (offv (poff ptr)) then
    385         return (pblock … ptr)
    386       else
    387         Error … [MSG BadFunction; MSG BadPointer]
    388     ] ;
    389   opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl).
     379(* to be used in implementations *)
     380definition block_of_call_id ≝  λF.λsp:sem_state_params.
     381  λge: genv_t F.λid.λst:state sp.
     382  opt_to_res … [MSG BadFunction; CTX … id] (
     383    ! bl ← find_symbol … ge id;
     384    code_block_of_block bl).
     385 
     386definition block_of_call_id_ptr ≝ λp,F.λsp : sem_unserialized_params p F.
     387  λglobals.λge: genv_t (F globals).λf.λst : state sp.
     388  match f with
     389  [ inl id ⇒ block_of_call_id … ge id st
     390  | inr addr ⇒
     391    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     392    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     393    ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
     394    if eq_bv … (bv_zero …) (offv (poff ptr)) then
     395      opt_to_res … [MSG BadFunction; MSG BadPointer]
     396        (code_block_of_block (pblock … ptr))
     397    else
     398      Error … [MSG BadFunction; MSG BadPointer]
     399  ].
    390400
    391401(* Paolo: why external calls do not need args?? *)
     
    488498λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
    489499λst : state_pc p.
    490 ! bl ← block_of_call … ge st f : IO ???;
     500! bl ← block_of_call … ge f st : IO ???;
    491501! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
    492502match fd with
     
    523533    | COND a l ⇒ return st
    524534    ]
    525   | final s ⇒ return st
     535  | _ ⇒ return st
    526536  ].
    527537
     
    538548λcurr_fn : joint_closed_internal_function ??.
    539549λst : state_pc p.
    540 ! bl ← block_of_call … ge st f : IO ???;
     550! bl ← block_of_call … ge f st : IO ???;
    541551! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
    542552match fd with
     
    557567  IO io_out io_in (state_pc p) ≝
    558568  λp,g,ge,curr_id,curr_fn,s,st.
    559   match s with
     569  match s return λ_.IO ??? with
    560570  [ sequential s nxt ⇒
    561571    match s return λ_.IO ??? with
     
    577587      eval_tailcall … ge f args curr_id curr_fn st
    578588    ]
     589  | FCOND _ a lbltrue lblfalse ⇒
     590    ! v ← acca_retrieve … st a ;
     591    ! b ← bool_of_beval … v ;
     592    if b then
     593      goto … ge lbltrue st
     594    else
     595      goto … ge lblfalse st
    579596  ].
    580597
Note: See TracChangeset for help on using the changeset viewer.