Changeset 2412
 Timestamp:
 Oct 22, 2012, 4:21:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2399 r2412 75 75 λsc,x. \snd (measure_stack sc x). 76 76 77 (* TODO: cost labels *) 78 79 let rec will_return_aux (stack_cost:Clight_stack_T) (depth:nat) (current_stack:nat) 80 (max_stack:nat) (trace:execution_prefix) on trace : option nat ≝ 77 let rec will_return_aux (depth:nat) 78 (trace:execution_prefix) on trace : bool ≝ 81 79 match trace with 82 [ nil ⇒ match depth with [ O ⇒ Some ? max_stack  _ ⇒ None ?]80 [ nil ⇒ match depth with [ O ⇒ true  _ ⇒ false ] 83 81  cons h tl ⇒ 84 82 let 〈tr,s〉 ≝ h in 85 match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with 86 [ cl_call ⇒ λsc. 87 let new_stack ≝ current_stack + sc I in 88 will_return_aux stack_cost (S depth) new_stack (max max_stack new_stack) tl 89  cl_return ⇒ λsc. 83 match Clight_classify s with 84 [ cl_call ⇒ will_return_aux (S depth) tl 85  cl_return ⇒ 90 86 match depth with 91 [ O ⇒ None ?92  S d ⇒ will_return_aux stack_cost d (current_stack  sc I) max_stacktl87 [ O ⇒ false 88  S d ⇒ will_return_aux d tl 93 89 ] 94  _ ⇒ λ_. will_return_aux stack_cost depth current_stack max_stacktl95 ] (stack_cost s)90  _ ⇒ will_return_aux depth tl 91 ] 96 92 ]. 97 definition will_return' : Clight_stack_T → nat → execution_prefix → option nat ≝ 98 λstack_cost,current_stack,trace. will_return_aux stack_cost O current_stack current_stack trace. 93 definition will_return' : execution_prefix → bool ≝ will_return_aux O. 99 94 100 95 definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝ 101 λp,m,n,stack_cost,max_allowed_stack. ∀prefix,suffix,interesting,remainder ,max_stack.96 λp,m,n,stack_cost,max_allowed_stack. ∀prefix,suffix,interesting,remainder. 102 97 let cl_trace ≝ exec_inf … clight_fullexec p in 103 98 split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧ 104 99 split_trace suffix n = Some ? 〈interesting,remainder〉 ∧ 105 trace_labelled interesting →106 will_return' stack_cost (stack_after stack_cost prefix) interesting = Some ? max_stack∧107 max_stack < max_allowed_stack.100 trace_labelled interesting ∧ 101 bool_to_Prop (will_return' interesting) ∧ 102 max_stack stack_cost (prefix@interesting) < max_allowed_stack. 108 103 109 104 (* From measurable on Clight, we will end up with an RTLabs flat trace where
Note: See TracChangeset
for help on using the changeset viewer.