Changeset 2324


Ignore:
Timestamp:
Sep 5, 2012, 5:17:49 PM (7 years ago)
Author:
tranquil
Message:

semantics of blocks: function to produce trace from execution of sequences of (sequential) instructions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2186 r2324  
    88  ].*)
    99
    10 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
     10lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer.
    1111  ∀fn,pt,s.
    1212  fetch_function … ge ptr = OK … fn →
    13   point_of_pointer ? p … ptr = OK … pt →
     13  point_of_pointer ? p … ptr = pt →
    1414  stmt_at … (joint_if_code … fn) pt = Some ? s →
    15   fetch_statement ? p … ge ptr = OK … s.
     15  fetch_statement ? p … ge ptr = OK … 〈fn, s〉.
    1616#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
    17 whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind
    18 >EQ1 >m_return_bind >EQ3 %
     17whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
     18>EQ2 >EQ3 >m_return_bind %
    1919qed.
    2020
     
    4343
    4444let rec repeat_eval_seq_no_pc
    45   (p : evaluation_params) env
     45  (p : evaluation_params) env curr_fn
    4646  (l : list (joint_seq p (globals p))) on l :
    4747  state p → res (state p) ≝
     
    4949  [ nil ⇒ return st
    5050  | cons hd tl ⇒
    51     ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ;
    52     repeat_eval_seq_no_pc p env tl st'
     51    ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ;
     52    repeat_eval_seq_no_pc p env curr_fn tl st'
    5353  ].
    5454
     
    7070∀st : state p. ∀s.
    7171no_call_nor_label p (globals p) s →
    72 eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???.
     72eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.
    7373#p #st * // [ #f #args #dest | #c ] *
    7474qed.
     
    8686qed.
    8787
     88definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝
     89  λp,g,c.code_closed … c∧
     90    ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.
     91
     92definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.
     93  ∀c,pc,step,dst.
     94  code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →
     95  Σpc'.pointer_of_point p p pc dst = return pc' ≝
     96  λp,g,c,pc,step,dst,c_compact,step_in.
     97  match pointer_of_point p p pc dst
     98  return λx.pointer_of_point p p pc dst = x → ?
     99  with
     100  [ OK pc' ⇒ mk_Sig ?? pc'
     101  | Error e ⇒ λEQ.⊥
     102  ] (refl …).
     103cases step_in #nxt * #EQ1 #EQ2
     104cases c_compact -c_compact #c_closed #c_compact
     105elim (c_compact dst pc ?)
     106[ >EQ #pc' normalize #ABS destruct(ABS)
     107| elim (c_closed … EQ1) #_ whd in ⊢ (%→?);
     108  >EQ2 #H @H
     109]
     110qed.
     111
     112let rec pointer_of_point_in_code
     113  p g c pc dst b on b :
     114  ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →
     115  Σpc'.pointer_of_point p p pc dst = return pc' ≝
     116match b
     117return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'
     118with
     119[ nil ⇒
     120  λl,c_compact,in_code.
     121  match pointer_of_point p p pc dst
     122  return λx.pointer_of_point p p pc dst = x → ? with
     123  [ OK ptr' ⇒ mk_Sig ?? ptr'
     124  | Error e ⇒ λEQ.⊥
     125  ] (refl …)
     126| cons hd tl ⇒
     127  λl.match l return λl.? → ? → Σptr'.? with
     128  [ nil ⇒ λc_compact,in_code.⊥
     129  | cons mid rest ⇒ λc_compact,in_code.
     130    let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in
     131    pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)
     132  ]
     133].
     134[ cases l in in_code; [2: #mid #rest * ]
     135  whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]
     136  normalize #ABS destruct(ABS)
     137| cases (pointer_of_point_in_code ?????????)
     138  #ptr' >pointer_of_point_uses_block
     139  [ #H @H |*:]
     140  cases mid_pc -mid_pc #mid_pc @pointer_of_point_block
     141| elim in_code
     142| cases mid_pc -mid_pc #mid_pc #EQ
     143  >(point_of_pointer_of_point … EQ)
     144  cases in_code #_ #H @H
     145| cases in_code #H #_ @H
     146]
     147qed.
     148
    88149let rec produce_trace_any_any
    89150  (p : evaluation_params)
    90151  (st : state_pc p) fd
    91   (src : code_point p)
    92152  (b : list (joint_seq p (globals p))) on b :
    93153  ∀l : list (code_point p).
     
    95155  ∀st' : state p.
    96156  fetch_function p ? (ev_genv p) (pc … st) = return fd →
    97   point_of_pointer p p (pc … st) = return src →
     157  ∀prf1 : code_compact p (globals p) (joint_if_code … fd).
     158  let src ≝ point_of_pointer p p (pc … st) in
    98159  if list_not_empty ? b then
    99160    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
    100161  else
    101162    True →
    102   src ~❨b, l❩~> dst in joint_if_code … fd →
     163  ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.
    103164  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
    104   repeat_eval_seq_no_pc p (io_env p) b st = return st' →
     165  repeat_eval_seq_no_pc p (io_env p) fd b st = return st' →
    105166  trace_any_any (joint_abstract_status p) st
    106     (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
     167    (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝
    107168  match b
    108   return λx.?→?→?→?→?→?→?→?→?→?
     169  return λx.∀l,dst.?→?→?→?→?→?→?→?
    109170  with
    110171  [ nil ⇒
    111     λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
     172    λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
    112173    (taa_base (joint_abstract_status p) st)
    113       ⌈trace_any_any (joint_abstract_status p) st st ↦
    114        trace_any_any (joint_abstract_status p) st
    115         (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
     174      ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉
    116175  | cons hd tl ⇒
    117176    λl.
    118177    match l return λx.?→?→?→?→?→?→?→?→? with
    119     [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
     178    [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥
    120179    | cons mid rest ⇒
    121       λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
    122       match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
    123       return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
     180      λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
     181      let mid_pc ≝
     182        pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st)
     183          hd mid c_compact ? in
     184      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd)
     185      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ?
    124186      with
    125187      [ OK st_mid ⇒ λEQ2.
    126         taa_step (joint_abstract_status p) st ?
    127           (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
    128           (produce_trace_any_any ?
    129             (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
    130             fd mid tl rest dst ???????)
     188        let tr_tl ≝ produce_trace_any_any ?
     189            (mk_state_pc ? st_mid mid_pc)
     190            fd tl rest dst ??????? in
     191        (* works fast only in interactive mode:
     192        taa_step … tr_tl *) ?
    131193      | Error _ ⇒ λEQ2.⊥
    132194      ] (refl …)
    133195    ]
    134   ].
    135   [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
    136     cases st in src_prf EQ1; -st #st #pc
    137     #src_prf normalize in ⊢ (%→?); #EQ1 destruct
    138     >(pointer_of_point_of_pointer … src_prf) %
    139   | elim in_code
    140   |12: lapply EQ1 whd in ⊢ (??%?→?);
    141     >EQ2 normalize #ABS destruct(ABS)
    142   |*:
    143     elim in_code
    144     * #nxt * #EQ3 #EQ4 #Hrest
    145     elim all_other
    146     #hd_other #tl_other
    147     [ whd whd in match eval_state; normalize nodelta
    148       >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind
    149       whd in match eval_statement; normalize nodelta
    150       whd in match eval_step; normalize nodelta
    151       >m_bind_bind
    152       >(no_call_nor_label_proceed … hd_other) >m_return_bind
    153       >m_bind_bind
    154       >io_evaluate_bind >EQ2 >m_return_bind
    155       >m_return_bind
    156       whd in match succ_pc; normalize nodelta
    157       >m_bind_bind >src_prf >m_return_bind >m_return_bind
    158       whd in match eval_step_flow; normalize nodelta
    159       whd in ⊢ (??%%); >EQ4
    160       >EQ2 %
    161     | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
    162       cases all_other #hd_other #_
    163       whd in match stmt_classifier; normalize nodelta
    164       @no_call_nor_label_other assumption
    165     | %* #H @H -H whd in ⊢ (??%?);
    166       cases tl in Hrest tl_other;
    167       [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
    168         lapply dst_prf
    169         whd in match (as_pc_of ??);
    170         whd in match fetch_statement; normalize nodelta
    171         whd in match point_of_pointer; normalize nodelta
    172         >point_of_offset_of_point
    173         >m_return_bind
    174         >fetch_function_from_block_eq
    175         [ >fd_prf
    176           >m_return_bind
    177           cases (stmt_at ????)
    178           [ #_ %
    179           | #stmt #H @H
    180           ]
    181         | %
    182         |
    183         ]
    184       | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
    185         #_ * #hd_other' #_
    186         >fetch_statement_eq try assumption
    187         [ @no_call_nor_label_uncosted assumption
    188         | whd in match (as_pc_of ??);
    189           whd in ⊢ (??%?);
    190           >point_of_offset_of_point %
    191         ]
    192       ]
    193     | change with (! x ← ?;?) in EQ1 : (??%?);
    194       >EQ2 in EQ1; #H @H
    195     | assumption
    196     | assumption
    197     | cases (list_not_empty ??) [ assumption | % ]
    198     | @point_of_pointer_of_point
    199     | <fd_prf @fetch_function_from_block_eq %
    200     ]
    201   ]
    202 qed.
     196  ].[3: @(taa_step … tr_tl) |*:]
     197try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc)
     198try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code)
     199try (cases all_other #hd_other #tl_other)
     200[ whd whd in match eval_state; normalize nodelta
     201  >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
     202  >m_return_bind
     203  whd in match eval_statement; normalize nodelta
     204  whd in match eval_step; normalize nodelta
     205  >m_bind_bind
     206  >(no_call_nor_label_proceed … hd_other) >m_return_bind
     207  >m_bind_bind
     208  >io_evaluate_bind >EQ2 >m_return_bind
     209  >m_return_bind
     210  whd in match succ_pc; normalize nodelta
     211  >EQ_mid >EQ_mid_pc >m_return_bind %
     212| whd %{fd} %{(sequential … hd nxt)}
     213  %{(no_call_nor_label_other … hd_other)}
     214  @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
     215|4: cases (pointer_of_point_in_code ?????????)
     216  #dst_pc
     217  cases l in in_code; [2: #mid #rest * ]
     218  whd in ⊢ (%→?); #EQ' <EQ'
     219  >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1
     220  normalize in ⊢ (%→%→?);
     221  #EQ1 #EQ'' destruct cases st //
     222|5: >fetch_function_from_block_eq [ @fd_prf |*: ]
     223  @(pointer_of_point_block … EQ_mid_pc)
     224|6: cases tl [ % ] #hd' #tl' @dst_prf
     225|7: assumption
     226|8,9:
     227  lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta
     228  [ #H @H
     229  | normalize #ABS destruct(ABS)
     230  ]
     231|3:
     232  %* #H @H -H
     233  lapply tl_other lapply rest_in_code
     234  (* BUG? cases tl causes "Ill formed pattern" *)
     235  @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?])
     236  cases rest [2,4: #mid' #rest']
     237  [1,4: * ]
     238  [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
     239  | ** #nxt' * #at_mid #_ #_ * #mid_other #_
     240  ]
     241  whd in ⊢ (??%?);
     242  [ lapply dst_prf ]
     243  whd in match as_label;
     244  whd in match (as_pc_of ??);
     245  whd in match fetch_statement;
     246  normalize nodelta
     247  >(point_of_pointer_of_point … EQ_mid_pc)
     248  >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc))
     249  >fd_prf >m_return_bind
     250  [ cases (stmt_at ????) [ #_ % ]
     251    #stmt #H @H
     252  | >at_mid >m_return_bind normalize nodelta
     253    @(no_call_nor_label_uncosted … mid_other)
     254  ]
     255]
     256qed.
Note: See TracChangeset for help on using the changeset viewer.