Changeset 2757


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2754 r2757  
    44include "common/LabelledObjects.ma".
    55include "joint/String.ma".
     6
     7(* move! *)
     8definition partial_injection : ∀A,B.(A → option B) → Prop ≝
     9λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y.
    610
    711definition Identifier ≝ identifier ASMTag.
     
    987991   The second associative list assigns to Identifiers meant to be entry points
    988992   of functions the name of the function (that lives in a different namespace) *)
    989 definition preamble ≝ list (Identifier × Word) × (list (Identifier × ident)).
     993
    990994definition assembly_program ≝ list instruction.
    991 definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
    992 
    993 definition object_code ≝ list Byte.
    994 definition costlabel_map ≝ BitVectorTrie costlabel 16.
    995 definition symboltable_type ≝ BitVectorTrie ident 16.
    996 definition labelled_object_code ≝ object_code × (costlabel_map × symboltable_type).
     995
     996definition fetch_pseudo_instruction:
     997 ∀code_mem:list labelled_instruction. ∀pc:Word.
     998  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
     999  λcode_mem.
     1000  λpc: Word.
     1001  λpc_ok.
     1002    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
     1003    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
     1004      〈instr, new_pc〉.
     1005
     1006lemma snd_fetch_pseudo_instruction:
     1007 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
     1008 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
     1009 #lft #rgt #_ %
     1010qed.
     1011
     1012lemma fetch_pseudo_instruction_vsplit:
     1013 ∀instr_list,ppc,ppc_ok.
     1014  ∃pre,suff,lbl.
     1015   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
     1016#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
     1017cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
     1018lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
     1019#EQ %{lbl0} @EQ
     1020qed.
     1021
     1022lemma fetch_pseudo_instruction_append:
     1023 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
     1024  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
     1025  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
     1026  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
     1027 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     1028 cut (|l1| + nat_of_bitvector … ppc < 2^16)
     1029 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
     1030 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
     1031 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1032 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
     1033 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
     1034 #lbl #instr normalize nodelta >add_associative %
     1035qed.
    9971036
    9981037(* labels & instructions *)
     
    10191058  ].
    10201059
     1060definition is_jump_to ≝
     1061  λx:pseudo_instruction.λd:Identifier.
     1062  match x with
     1063  [ Instruction i ⇒ match i with
     1064    [ JC j ⇒ d = j
     1065    | JNC j ⇒ d = j
     1066    | JZ j ⇒ d = j
     1067    | JNZ j ⇒ d = j
     1068    | JB _ j ⇒ d = j
     1069    | JNB _ j ⇒ d = j
     1070    | JBC _ j ⇒ d = j
     1071    | CJNE _ j ⇒ d = j
     1072    | DJNZ _ j ⇒ d = j
     1073    | _ ⇒ False
     1074    ]
     1075  | Call c ⇒ d = c
     1076  | Jmp j ⇒ d = j
     1077  | _ ⇒ False
     1078  ].
     1079
     1080definition is_well_labelled_p ≝
     1081  λinstr_list.
     1082  ∀id: Identifier.
     1083  ∀ppc.
     1084  ∀ppc_ok.
     1085  ∀i.
     1086    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
     1087      (instruction_has_label id i →
     1088        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
     1089      (is_jump_to i id →
     1090        occurs_exactly_once ASMTag pseudo_instruction id instr_list).
     1091
     1092definition asm_cost_label : ∀mem : list labelled_instruction.
     1093  (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
     1094λmem,w_prf.
     1095match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
     1096[ Cost c ⇒ Some ? c
     1097| _ ⇒ None ?
     1098].
     1099
     1100record pseudo_assembly_program : Type[0] ≝
     1101{ preamble : list (Identifier × Word)
     1102; code : list labelled_instruction
     1103; renamed_symbols : list (Identifier × ident)
     1104; final_index : Word
     1105(* properties *)
     1106; asm_injective_costlabels :
     1107  partial_injection … (asm_cost_label code)
     1108; well_labelled_p : is_well_labelled_p code
     1109}.
     1110
     1111definition object_code ≝ list Byte.
     1112definition costlabel_map ≝ BitVectorTrie costlabel 16.
     1113definition symboltable_type ≝ BitVectorTrie ident 16.
     1114record labelled_object_code : Type[0] ≝
     1115{ oc :> object_code
     1116; costlabels : costlabel_map
     1117; symboltable : symboltable_type
     1118; final_pc : Word
     1119(* properties *)
     1120; oc_injective_costlabels :
     1121  partial_injection … (λpc.lookup_opt … pc costlabels)
     1122}.
     1123
    10211124
    10221125(* If instruction i is a jump, then there will be something in the policy at
     
    10601163  ].
    10611164 
    1062 definition is_jump_to ≝
    1063   λx:pseudo_instruction.λd:Identifier.
    1064   match x with
    1065   [ Instruction i ⇒ match i with
    1066     [ JC j ⇒ d = j
    1067     | JNC j ⇒ d = j
    1068     | JZ j ⇒ d = j
    1069     | JNZ j ⇒ d = j
    1070     | JB _ j ⇒ d = j
    1071     | JNB _ j ⇒ d = j
    1072     | JBC _ j ⇒ d = j
    1073     | CJNE _ j ⇒ d = j
    1074     | DJNZ _ j ⇒ d = j
    1075     | _ ⇒ False
    1076     ]
    1077   | Call c ⇒ d = c
    1078   | Jmp j ⇒ d = j
    1079   | _ ⇒ False
    1080   ].
  • src/ASM/Status.ma

    r2754 r2757  
    10281028qed.
    10291029
    1030 definition fetch_pseudo_instruction:
    1031  ∀code_mem:list labelled_instruction. ∀pc:Word.
    1032   nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
    1033   λcode_mem.
    1034   λpc: Word.
    1035   λpc_ok.
    1036     let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
    1037     let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
    1038       〈instr, new_pc〉.
    1039 
    1040 lemma snd_fetch_pseudo_instruction:
    1041  ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
    1042  #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
    1043  #lft #rgt #_ %
    1044 qed.
    1045 
    1046 lemma fetch_pseudo_instruction_vsplit:
    1047  ∀instr_list,ppc,ppc_ok.
    1048   ∃pre,suff,lbl.
    1049    (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
    1050 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
    1051 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
    1052 lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
    1053 #EQ %{lbl0} @EQ
    1054 qed.
    1055 
    1056 lemma fetch_pseudo_instruction_append:
    1057  ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
    1058   let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
    1059   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
    1060   〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
    1061  #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
    1062  cut (|l1| + nat_of_bitvector … ppc < 2^16)
    1063  [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
    1064  -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
    1065  >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    1066  [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
    1067  #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
    1068  #lbl #instr normalize nodelta >add_associative %
    1069 qed.
    1070 
    1071 definition is_well_labelled_p ≝
    1072   λinstr_list.
    1073   ∀id: Identifier.
    1074   ∀ppc.
    1075   ∀ppc_ok.
    1076   ∀i.
    1077     \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
    1078       (instruction_has_label id i →
    1079         occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
    1080       (is_jump_to i id →
    1081         occurs_exactly_once ASMTag pseudo_instruction id instr_list).
    1082 
    1083 definition construct_datalabels: preamble → ? ≝
    1084   λthe_preamble: preamble.
     1030definition construct_datalabels: list (Identifier × Word) → ? ≝
     1031  λthe_preamble.
    10851032    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    10861033    λt. λpreamble.
     
    10891036      let 〈carry, sum〉 ≝ half_add … addr size in
    10901037        〈add ? ? datalabels name addr, sum〉)
    1091           〈empty_map …, zero 16〉 (\fst the_preamble)).
     1038          〈empty_map …, zero 16〉 (the_preamble)).
  • src/RTLabs/RTLabs_abstract.ma

    r2724 r2757  
    201201 *)
    202202
    203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝
     203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
    204204λge,s,s'.
    205205  match s with
    206206  [ mk_Sig s p ⇒
    207     match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
     207    match s return λs. RTLabs_classify s = cl_call → ? with
    208208    [ Callstate _ fd args dst stk m ⇒
    209209      λ_. match s' with
     
    219219   ] p
    220220 ].
    221 [ whd in H:(??(??%)?);
     221[ whd in H:(??%?);
    222222  cases (next_instruction f) in H;
    223223  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    226226] qed.
    227227
    228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
     228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → ident ≝
    229229λge,s.
    230230  match s with
    231231  [ mk_Sig s p ⇒
    232     match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     232    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     234      match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
    235235      [ Callstate _ fd _ _ _ _ ⇒
    236236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
     
    243243    ] p
    244244  ].
    245 [ whd in H:(??(??%)?);
     245[ whd in H:(??%?);
    246246  cases (next_instruction f) in H;
    247247  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    261261(* Roughly corresponding to as_classifier *)
    262262lemma RTLabs_notail' : ∀s.
    263   Some ? (RTLabs_classify s) = Some ? cl_tailcall →
     263  RTLabs_classify s = cl_tailcall →
    264264  False.
    265265#s #E @(RTLabs_notail … s)
     
    275275    RTLabs_deqset
    276276    (RTLabs_ext_state_to_pc ge)
    277     (λs. Some ? (RTLabs_classify s))
     277    (RTLabs_classify)
    278278    (RTLabs_pc_to_cost_label ge)
    279279    (RTLabs_after_return ge)
    280     (λs. RTLabs_is_final s ≠ None ?)
     280    (RTLabs_is_final)
    281281    (RTLabs_call_ident ge)
    282282    (λs. ⊥).
  • src/RTLabs/RTLabs_traces.ma

    r2728 r2757  
    726726qed.
    727727
    728 definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E.
    729 
    730728lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
    731729  ∀CL : RTLabs_classify s1 = cl_call.
    732730  as_execute (RTLabs_status ge) s1 s2 →
    733731  stack_preserved ge ends_with_ret s2 s3 →
    734   as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
     732  as_after_return (RTLabs_status ge) «s1,CL» s3.
    735733#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
    736734cases (rtlabs_call_inv … CL) #vf * #fn * #args * #dst * #stk * #m #E destruct
     
    840838(* Small syntax hack to avoid ambiguous input problems. *)
    841839definition myge : nat → nat → Prop ≝ ge.
    842 
    843 (* RTLabs_classify isn't exactly as_classifier *)
    844 definition lift_cl ≝ eq_f ?? (Some status_class).
    845840
    846841let rec make_label_return ge depth (s:RTLabs_ext_state ge)
     
    971966            (mk_trace_result ge …
    972967              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
    973                 ? (lift_cl … CL) ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
     968                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
    974969        (* otherwise use step case *)
    975970        | false ⇒ λCS.
     
    979974            replace_sub_trace … r' ?
    980975              (tal_step_call (RTLabs_status ge) (ends … r')
    981                 start' next' (new_state … r) (new_state … r') ? (lift_cl … CL) ?
     976                start' next' (new_state … r) (new_state … r') ? CL ?
    982977                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
    983978        ] (refl ??)
     
    990985            trace'
    991986            ?
    992             (tal_base_return (RTLabs_status ge) start' next' ? (lift_cl … CL))
     987            (tal_base_return (RTLabs_status ge) start' next' ? CL)
    993988            ?
    994989            ?)
     
    10351030| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10361031| %{tr} %{EV} %
    1037 | %1 whd @(lift_cl … CL)
     1032| %1 whd @CL
    10381033| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    10391034| @(well_cost_labelled_state_step  … EV) //
     
    10781073| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    10791074| %{tr} %{EV} %
    1080 | %2 whd @(lift_cl … CL)
     1075| %2 whd @CL
    10811076| @(well_cost_labelled_state_step  … EV) //
    10821077| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
    10831078| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
    1084 | @(lift_cl … CL)
     1079| @CL
    10851080| %{tr} %{EV} %
    10861081| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     
    12731268  state_bound_on_steps_to_cost s (S n) →
    12741269  ∀CL:RTLabs_classify s = cl_call.
    1275   as_after_return (RTLabs_status ge) «s, lift_cl … CL» s' →
     1270  as_after_return (RTLabs_status ge) «s, CL» s' →
    12761271  RTLabs_cost s' = false →
    12771272  state_bound_on_steps_to_cost s' n.
     
    14601455match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
    14611456[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    1462     (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
     1457    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    14631458    rem rok
    14641459| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
    1465     (tac_step_default (RTLabs_status ge) ??? EVAL TAC (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
     1460    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
    14661461    WCL2 EV rem rok
    14671462].
     
    14721467  finite_prefix ge s'' →
    14731468  trace_label_return (RTLabs_status ge) s1 s'' →
    1474   as_after_return (RTLabs_status ge) «s, lift_cl … CALL» s'' →
     1469  as_after_return (RTLabs_status ge) «s, CALL» s'' →
    14751470  RTLabs_cost s'' = false →
    14761471  finite_prefix ge s ≝
     
    14781473match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
    14791474[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    1480     (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAL)
     1475    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    14811476    rem rok
    14821477| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
    1483     (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
     1478    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    14841479    WCL2 EV rem rok
    14851480].
     
    15331528                let TRACE_OK' ≝ ? in
    15341529                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
    1535                 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (lift_cl … CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
     1530                [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
    15361531                | false ⇒ λCS.
    15371532                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    15401535              ]
    15411536            | or_intror NO_TERMINATION ⇒
    1542                 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (lift_cl … CL))) ?? trace' ?
     1537                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (CL))) ?? trace' ?
    15431538            ]
    15441539        | cl_return ⇒ λCL. ⊥
     
    15531548     %{0} % @wr_base //
    15541549| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1555 | %1 @(lift_cl … CL)
     1550| %1 @(CL)
    15561551| 6,9,10,11: /3/
    15571552| cases TRACE_OK #H1 #H2 #H3 #H4
     
    16021597    ]
    16031598| @(RTLabs_notail … CL)
    1604 | %2 @(lift_cl … CL)
     1599| %2 @(CL)
    16051600| 21,22: %{tr} %{EV} %
    16061601| cases (bound_after_step … LABEL_LIMIT EV ?)
     
    17581753        [ witness TERMINATES ⇒
    17591754          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    1760           twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (lift_cl … IS_CALL) ? (new_trace … tlr) ?
     1755          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (IS_CALL) ? (new_trace … tlr) ?
    17611756        ]
    17621757    | or_intror NO_TERMINATION ⇒
    1763         twp_diverges (RTLabs_status ge) s' next' (lift_cl … IS_CALL) ?
     1758        twp_diverges (RTLabs_status ge) s' next' (IS_CALL) ?
    17641759         (make_label_diverges ge next' trace' ORACLE ?
    17651760            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
     
    23562351    cases EX #tr * #EV #NX
    23572352    cases (eval_successor … EV)
    2358     [ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct
     2353    [ * #CL' @⊥ cases (tal_return … (CL') tal') #EX' * #CL'' * #E1 #E2 destruct
    23592354      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
    23602355      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
     
    23902385cases (eval_successor … EV)
    23912386[ * #CL2 #SC
    2392   cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
     2387  cases (tal_return … (CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
    23932388  @notb_Prop % whd in match (tal_pc_list ?????); #IN
    23942389  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
     
    26032598  [ >FN cases (state_fn_other … CL3' EX3)
    26042599    [ #CL3'' @⊥
    2605       cases (tal_return … (lift_cl … CL3'') tal3')
     2600      cases (tal_return … (CL3'') tal3')
    26062601      #EX3' * #CL3''' * #E1 #E2 destruct
    26072602      whd in IN:(?%); lapply IN @eqb_elim
     
    26562651    cases (state_fn_other … CL2' EX2)
    26572652    [ #CL3 @⊥
    2658       cases (tal_return … (lift_cl … CL3) tal3)
     2653      cases (tal_return … (CL3) tal3)
    26592654      #EX3 * #CL3' * #E1 #E2 destruct
    26602655      lapply (simplify_cl … CL3') #CL3''
  • src/common/StructuredTraces.ma

    r2756 r2757  
    1717record abstract_status : Type[1] ≝
    1818  { as_status :> Type[0]
    19   ; as_eval : as_status → IO io_out io_in as_status
    20   ; as_init : res as_status
     19  ; as_execute : relation as_status
    2120  ; as_pc : DeqSet
    2221  ; as_pc_of : as_status → as_pc
     
    3231definition as_call ≝ λS,s,f.as_call_ident S s = f.
    3332definition as_final ≝ λS,s.as_result S s ≠ None ?.
    34 definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2.
    3533
    3634definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
  • src/joint/Traces.ma

    r2688 r2757  
    117117
    118118definition joint_classify :
    119   ∀p : evaluation_params.state_pc p → option status_class ≝
     119  ∀p : evaluation_params.state_pc p → status_class ≝
    120120  λp,st.
    121   ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
    122   match s with
    123   [ sequential s _ ⇒ Some ? (joint_classify_step p s)
    124   | final s ⇒ Some ? (joint_classify_final p s)
    125   | FCOND _ _ _ _ ⇒ Some ? cl_jump
     121  match fetch_statement … (ev_genv p) (pc … st) with
     122  [ OK i_fn_s ⇒
     123    match \snd i_fn_s with
     124    [ sequential s _ ⇒ joint_classify_step p s
     125    | final s ⇒ joint_classify_final p s
     126    | FCOND _ _ _ _ ⇒ cl_jump
     127    ]
     128  | _ ⇒ cl_other
    126129  ].
    127130
    128131lemma joint_classify_call : ∀p : evaluation_params.∀st.
    129   joint_classify p st = Some ? cl_call →
     132  joint_classify p st = cl_call →
    130133  ∃i_f,f',args,dest,next.
    131134  fetch_statement … (ev_genv p) (pc … st) =
     
    137140* #i_f *
    138141[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    139   >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
    140 ]
    141 * [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
     142  normalize nodelta normalize in ⊢ (%→?); #ABS destruct
     143]
     144* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta
    142145normalize in ⊢ (%→?); #EQ destruct
    143146%[|%[|%[|%[|%[| %]]]]]
     
    145148
    146149definition joint_after_ret : ∀p:evaluation_params.
    147   (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
     150  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
    148151λp,s1,s2.
    149152match fetch_statement … (ev_genv p) (pc … s1) with
     
    159162
    160163definition joint_call_ident : ∀p:evaluation_params.
    161   (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
     164  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
    162165(* this is a definition without a dummy ident :
    163166λp,st.
     
    215218
    216219definition joint_tailcall_ident : ∀p:evaluation_params.
    217   (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
     220  (Σs : state_pc p.joint_classify p s = cl_tailcall) → ident ≝
    218221λp,st.
    219222let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     
    267270
    268271definition joint_abstract_status :
    269  ∀p : evaluation_params.
     272 ∀p : prog_params.
    270273 abstract_status ≝
    271274 λp.
     
    273276   (* as_status ≝ *) (state_pc p)
    274277   (* as_execute ≝ *)
    275     (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
     278    (λs1,s2.eval_state … (ev_genv p) s1 = return s2)
     279   (* (* as_init ≝ *) (make_initial_state p) *)
    276280   (* as_pc ≝ *) pcDeq
    277281   (* as_pc_of ≝ *) (pc …)
     
    284288      ])
    285289   (* as_after_return ≝ *) (joint_after_ret p)
    286    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
     290   (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
    287291   (* as_call_ident ≝ *) (joint_call_ident p)
    288    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 
     292   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracChangeset for help on using the changeset viewer.