Changeset 2218 for src/RTLabs/Traces.ma
 Timestamp:
 Jul 19, 2012, 6:45:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2184 r2218 1 1 2 2 include "RTLabs/semantics.ma". 3 include "RTLabs/CostSpec.ma". 3 4 include "common/StructuredTraces.ma". 4 5 … … 91 92 ] qed. 92 93 93 (*94 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.95 eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝96 λge,s,s',t.97 match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge with98 [ State f fs m ⇒ λEX. mk_RTLabs_state ge (State f fs m) (Ras_fn_stack … s) ?99  Callstate fd args dst fs m ⇒ λEX. mk_RTLabs_state ge (Callstate fd args dst fs m) (func_block_of_exec … EX::Ras_fn_stack … s) ?100  Returnstate rtv dst fs m ⇒ λEX. mk_RTLabs_state ge (Returnstate rtv dst fs m) (tail … (Ras_fn_stack … s)) ?101  Finalstate r ⇒ λEX. mk_RTLabs_state ge (Finalstate r) [ ] ?102 ].103 [ cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX)104 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct105 whd cases stk in mtc ⊢ %; [ * ]106 #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //107  @M2 ]108  #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct109  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct110 whd cases stk in mtc ⊢ %; [ * ]111 #hd #tl #H @H112  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct113  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct114 cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %115 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ]116  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct117 ]118  cases (func_block_of_exec … EX) #func_block #FFP119 whd % // func_block cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX)120 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct121  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct122 cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %123 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ]124  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct125  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct126  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct127  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct128 ]129  cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX)130 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct131  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct132  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct133  #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct134 cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H135  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct136  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct137 ]138  whd @refl139 ] qed.*)140 94 141 95 (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps … … 155 109 ]. 156 110 157 (* We define a straight "is this a cost label" pair of functions, which is 158 convenient for most of our uses here (because we can make a hypothesis of 159 it without naming the label), and a pair which return the label to fit the 160 definition of abstract_status. *) 161 162 definition is_cost_label : statement → bool ≝ 163 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ]. 111 (* As with is_cost_label/cost_label_of we define a boolean function as well 112 as one which extracts the cost label so that we can use it in hypotheses 113 without naming the cost label. *) 164 114 165 115 definition RTLabs_cost : state → bool ≝ … … 170 120 ]. 171 121 172 definition cost_label_of : statement → option costlabel ≝173 λs. match s with [ St_cost s _ ⇒ Some ? s  _ ⇒ None ? ].174 175 122 definition RTLabs_cost_label : state → option costlabel ≝ 176 123 λs. match s with … … 180 127 ]. 181 128 129 (* "Program counters" need to identify the current state, either as a pair of 130 the function and current instruction, or the function being entered or 131 left. Functions are identified by their function pointer block because 132 this avoids introducing functions to map back pointers to function ids using 133 the global environment. (See the comment at the start of this file, too.) *) 134 182 135 inductive RTLabs_pc : Type[0] ≝ 183 136  rapc_state : block → label → RTLabs_pc … … 186 139  rapc_fin : RTLabs_pc 187 140 . 188 189 definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.190 #x #y @eq_block_elim191 [ #E destruct /2/192  * #NE % #E destruct cases (NE (refl ??))193 ] qed.194 141 195 142 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝ … … 697 644 ] 698 645 ] qed. 699 700 (* We require that labels appear after branch instructions and at the start of701 functions. The first is required for preciseness, the latter for soundness.702 We will make a separate requirement for there to be a finite number of steps703 between labels to catch loops for soundness (is this sufficient?). *)704 705 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝706 λf,s. match s return λs. labels_present ? s → Prop with707 [ St_cond _ l1 l2 ⇒ λH.708 is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧709 is_cost_label (lookup_present … (f_graph f) l2 ?) = true710  St_jumptable _ ls ⇒ λH.711 (* I did have a dependent version of All here, but it's a pain. *)712 All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls713  _ ⇒ λ_. True714 ]. whd in H;715 [ @(proj1 … H)716  @(proj2 … H)717 ] qed.718 719 definition well_cost_labelled_fn : internal_function → Prop ≝720 λf. (∀l. ∀H:present … (f_graph f) l.721 well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧722 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.723 [ @lookup_lookup_present  cases (f_entry f) // ] qed.724 646 725 647 (* We need to ensure that any code we come across is wellcostlabelled. We may … … 1406 1328  witness : T → inhabited T. 1407 1329 1408 (* We also require that program's traces are soundly labelled: for any state1409 in the execution, we can give a distance to a labelled state or termination.1410 1411 Note that this differs from the syntactic notions in earlier languages1412 because it is a global property. In principle, we would have a loop broken1413 only by a call to a function (which necessarily has a label) and no local1414 cost label.1415 *)1416 1417 let rec nth_state ge s1418 (trace: flat_trace io_out io_in ge s)1419 n1420 on n : option state ≝1421 match n with1422 [ O ⇒ Some ? s1423  S n' ⇒1424 match trace with1425 [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'1426  _ ⇒ None ?1427 ]1428 ].1429 1430 definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝1431 λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.1432 1433 lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.1434 soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →1435 soundly_labelled_trace ge s' trace'.1436 #ge #s #tr #s' #EV #trace' #H1437 #n cases (H (S n)) #m #H' %{m} @H'1438 qed.1439 1330 1440 1331 (* Define a notion of sound labellings of RTLabs programs. *) 1441 1442 let rec successors (s : statement) : list label ≝1443 match s with1444 [ St_skip l ⇒ [l]1445  St_cost _ l ⇒ [l]1446  St_const _ _ _ l ⇒ [l]1447  St_op1 _ _ _ _ _ l ⇒ [l]1448  St_op2 _ _ _ _ _ _ _ l ⇒ [l]1449  St_load _ _ _ l ⇒ [l]1450  St_store _ _ _ l ⇒ [l]1451  St_call_id _ _ _ l ⇒ [l]1452  St_call_ptr _ _ _ l ⇒ [l]1453 (*1454  St_tailcall_id _ _ ⇒ [ ]1455  St_tailcall_ptr _ _ ⇒ [ ]1456 *)1457  St_cond _ l1 l2 ⇒ [l1; l2]1458  St_jumptable _ ls ⇒ ls1459  St_return ⇒ [ ]1460 ].1461 1332 1462 1333 definition actual_successor : state → option label ≝ … … 1506 1377  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl 1507 1378 ] qed. 1508 1509 definition steps_for_statement : statement → nat ≝1510 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1  St_call_ptr _ _ _ _ ⇒ 1  St_return ⇒ 1  _ ⇒ 0 ]).1511 1512 inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝1513  bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n1514  bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n1515 with bound_on_steps_to_cost1 : label → nat → Prop ≝1516  bostc_step : ∀l,n,H.1517 let stmt ≝ lookup_present … g l H in1518 (∀l'. Exists label (λl0. l0 = l') (successors stmt) →1519 bound_on_steps_to_cost g l' n) →1520 bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).1521 1379 1522 1380 (* … … 1687 1545 1688 1546 1689 1690 definition soundly_labelled_fn : internal_function → Prop ≝1691 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.1692 1547 1693 1548 definition soundly_labelled_ge : genv → Prop ≝ … … 2115 1970 ] qed. 2116 1971 2117 definition well_cost_labelled_program : RTLabs_program → Prop ≝2118 λp. All ? (λx. let 〈id,fd〉 ≝ x in2119 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn  _ ⇒ True]) (prog_funct … p).2120 1972 (* 2121 1973 theorem program_trace_exists :
Note: See TracChangeset
for help on using the changeset viewer.