Changeset 2534


Ignore:
Timestamp:
Dec 5, 2012, 7:20:27 PM (7 years ago)
Author:
campbell
Message:

Tweak measurable definition to stop at the return from a function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2511 r2534  
    2323    ! 〈pre,x''〉 ← split_trace FE g x' n';
    2424    Some ? 〈〈tr,s〉::pre,x''〉
     25    (* Necessary for a measurable trace at the end of the program *)
     26  | e_stop tr r s ⇒
     27    match n' with
     28    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
     29    | _ ⇒ None ?
     30    ]
    2531  | _ ⇒ None ?
    2632  ]
    2733].
    2834
    29 definition trace_labelled : ∀C. execution_prefix (cs_state … C) → Prop ≝
    30 λC,x. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ bool_to_Prop (cs_labelled C s2).
     35(* Ideally we would also allow measurable traces to be from one cost label to
     36   another (in the same function call), but due to time constraints we'll stick
     37   to ending measurable traces at the end of the function only.
     38 *)
     39
     40definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝
     41λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    3142
    3243definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
     
    4960λC,x. \snd (measure_stack C x).
    5061
     62(* Check that the trace ends with the return from the starting function and one
     63   further state. *)
     64
    5165let rec will_return_aux C (depth:nat)
    5266                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
    5367match trace with
    54 [ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
     68[ nil ⇒ false
    5569| cons h tl ⇒
    5670  let 〈tr,s〉 ≝ h in
     
    5973  | cl_return ⇒
    6074      match depth with
    61       [ O ⇒ false
     75       (* We need to see the state after the return to build the structured
     76          trace. *)
     77      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
    6278      | S d ⇒ will_return_aux C d tl
    6379      ]
     
    8298  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
    8399  nat → Prop ≝
    84 λC,p,m,n,stack_cost,max_allowed_stack.  prefix,suffix,interesting,remainder.
     100λC,p,m,n,stack_cost,max_allowed_stack.  prefix,suffix,interesting,remainder.
    85101  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
    86102  let cl_trace ≝ exec_inf … (cs_exec … C') p in
    87103  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
    88104  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
    89   trace_labelled C' interesting ∧
     105  trace_is_label_to_return C' interesting ∧
    90106  bool_to_Prop (will_return' C' interesting) ∧
    91107  le (max_stack C' (prefix@interesting)) max_allowed_stack.
Note: See TracChangeset for help on using the changeset viewer.