Changeset 3500
Legend:
- Unmodified
- Added
- Removed
-
LTS/Vm.ma
r3499 r3500 335 335 | STATE : vm_state p p' → vm_ass_state p p'. 336 336 337 definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p → abstract_status ≝ 338 λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in 339 let end_act ≝ cost_act (Some ? (in_act … prog)) in 340 mk_abstract_status 341 (vm_ass_state p p') 342 (λl.λs1,s2 : vm_ass_state p p'. 337 definition ass_vmstep ≝ 338 λp,p',prog. 339 λl.λs1,s2 : vm_ass_state p p'. 343 340 match s1 with 344 341 [ STATE st1 ⇒ … … 347 344 (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2 348 345 | INITIAL ⇒ False 349 | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act 346 | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ 347 l = cost_act (Some … (in_act … prog)) 350 348 ] 351 349 | INITIAL ⇒ match s2 with 352 [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act 350 [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ 351 l = cost_act (Some … (in_act … prog)) 353 352 | _ ⇒ False 354 353 ] 355 354 | FINAL ⇒ False 356 ]) 355 ]. 356 357 definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p → abstract_status ≝ 358 λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in 359 let end_act ≝ cost_act (Some ? (in_act … prog)) in 360 mk_abstract_status 361 (vm_ass_state p p') 362 (ass_vmstep … prog) 357 363 (λ_.λ_.True) 358 364 (λst.match st with … … 458 464 λp,p',prog,st.fetch … prog (pc … st). 459 465 460 definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. 461 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p)) 462 (λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then 466 record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝ 467 { aabs_d : abstract_transition_sys (m … p') 468 ; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d 469 }. 470 471 definition galois_connection_of_asm_galois_connection: 472 ∀p,p',prog. asm_galois_connection p p' prog → galois_connection ≝ 473 λp,p',prog,agc. 474 mk_galois_connection 475 (asm_concrete_trans_sys p p' prog) 476 (aabs_d … agc) 477 (agalois_rel … agc). 478 479 coercion galois_connection_of_asm_galois_connection. 480 481 definition ass_fetch ≝ 482 λp,p',prog. 483 λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then 463 484 Some ? (None ?) 464 485 else ! x ← fetch_state p p' prog st; Some ? (Some ? x) 465 | INITIAL ⇒ Some ? (None ?) 466 | FINAL ⇒ None ? ]) instr_m. 486 | INITIAL ⇒ Some ? (None ?) 487 | FINAL ⇒ None ? ]. 488 489 definition ass_instr_map ≝ 490 λp,p',prog.λasm_galois_conn: asm_galois_connection p p' prog. 491 λinstr_map: AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn)). 492 (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]). 493 494 record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝ 495 { asm_galois_conn: asm_galois_connection p p' prog 496 ; instr_map : AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn)) 497 ; instr_map_ok : 498 ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i. 499 as_execute … l s s' → 500 ass_fetch … prog s = Some ? i → 501 ∀I. ass_instr_map … instr_map i = (*Some ?*) I → 502 asm_galois_conn s a → asm_galois_conn s' (〚I〛 a) 503 }. 504 505 definition abstract_interpretation_of_asm_abstract_interpretation: 506 ∀p,p',prog. asm_abstract_interpretation p p' prog → abstract_interpretation 507 ≝ 508 λp,p',prog,aai. 509 mk_abstract_interpretation 510 (asm_galois_conn … aai) (option (AssemblerInstr p)) (ass_fetch p p' prog) 511 (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai). 512 513 coercion abstract_interpretation_of_asm_abstract_interpretation. 467 514 468 515 definition non_empty_list : ∀A.list A → bool ≝ … … 883 930 qed. 884 931 885 notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.886 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).887 888 932 coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?. 889 933 … … 893 937 894 938 (* Given a Galois connection to an abstract transition system *) 895 ∀abs_t : abstract_transition_sys (m … p'). 896 ∀instr_m : (AssemblerInstr p) → abs_instr … abs_t. 897 ∀R : static_galois … (asm_static_analisys_data … prog … 898 (λi.match i with [None ⇒ e … 899 |Some x ⇒ instr_m x 900 ])). 939 ∀R: asm_abstract_interpretation p p' prog. 901 940 902 941 (* If the static analysis does not fail *) 903 ∀mT,map1. ∀EQmap : static_analisys … instr_mmT prog = return map1.942 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1. 904 943 905 944 (* For every pre_measurable, terminated trace *) … … 912 951 (* Let k be the statically computed abstract action of the prefix of the trace 913 952 up to the first label *) 914 ∀k.block_cost p prog … instr_m(get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →953 ∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k → 915 954 916 955 (* Let abs_actions be the list of statically computed abstract actions … … 933 972 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 934 973 ] 935 #p #p' #prog # abs_t #instr_m #good#mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *974 #p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * 936 975 #l1 * #prf1 * #EQ destruct #Hlabelled 937 976 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) … … 943 982 |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels 944 983 #a1 #rel_fin 945 lapply(instr_map_ok … good … prf …rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *984 lapply(instr_map_ok … R … prf … (refl …) rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] * 946 985 #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H; 947 986 <(act_neutral … (act_abs …) a1) @H … … 951 990 normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct 952 991 #EQ destruct whd in EQc : (??%%); destruct 953 lapply(instr_map_ok … good … good_st_a1) 954 [5: @(FINAL …) 955 |2: whd % [ >EQpc @eqb_elim // * #ABS @⊥ @ABS %] % 956 | whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption 957 ] 958 #_ normalize nodelta % | | | whd in ⊢ (% → ?); >act_neutral // 959 ] 992 lapply(instr_map_ok … R … (refl …) good_st_a1) 993 [5: @(FINAL …) 994 |2: whd % [2: % | // ] 995 | whd whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption | #_ % ] 996 |3,4: skip] 997 whd in ⊢ (% → ?); >act_neutral #H @H 960 998 | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf 961 999 normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim … … 982 1020 whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1 983 1021 >neutral_r >act_neutral 984 lapply(instr_map_ok … good … good_st_a1)1022 lapply(instr_map_ok R … (refl …) good_st_a1) 985 1023 [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta 986 1024 [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state; … … 989 1027 | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); 990 1028 | >EQfetch in ⊢ (??%?); ] % 991 |3,9,15,21,27,33,39: skip |*: try assumption // ] 992 ] 993 ] 1029 |3,9,15,21,27,33,39: skip |*: try assumption // ]]] 994 1030 | -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3 995 1031 [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p')) … … 1022 1058 [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??); 1023 1059 >neutral_l assumption 1024 |3,6: [ >neutral_r] lapply(instr_map_ok … good …good_a1)1060 |3,6: [ >neutral_r] lapply(instr_map_ok R … (refl …) good_a1) 1025 1061 [1,7: whd in ⊢ (??%?); @eqb_elim 1026 1062 [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state; … … 1060 1096 [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ] 1061 1097 #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption 1062 | lapply(instr_map_ok … good …good_a1)1098 | lapply(instr_map_ok R … (refl …) good_a1) 1063 1099 [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H 1064 1100 ] -
LTS/costs.ma
r3458 r3500 43 43 }. 44 44 45 record galois_conn (C : concrete_transition_sys) 45 notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }. 46 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x). 47 48 record galois_rel (C : concrete_transition_sys) 46 49 (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝ 47 50 { rel_galois :2> C → A → Prop 48 51 ; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s 49 ; rel_galois_prop : ∀s,s' : C.∀a : A.∀l.as_execute … l s s' → rel_galois … s a →50 ∃i : abs_instr … A.∃a' : A.rel_galois … s' a' ∧51 act_abs ?? i a = a'52 52 }. 53 53 54 record static_analysis_data: Type[2] ≝54 record galois_connection : Type[2] ≝ 55 55 { concr : concrete_transition_sys 56 56 ; abs_d : abstract_transition_sys (cost_mon concr) 57 ; instr_t : Type[0] 58 ; fetch : concr → option instr_t 59 ; instr_map : instr_t → abs_instr … abs_d 57 ; galois_rel:> galois_rel concr abs_d 60 58 }. 61 59 62 63 record static_galois (p : static_analysis_data) : Type[0] ≝ 64 { good :> galois_conn (concr … p) (abs_d … p) 65 ; instr_map_ok : ∀s,s' : (concr … p).∀a : (abs_d … p).∀l,i.as_execute … l s s' → 66 fetch … p s = Some ? i → 67 rel_galois … good s a → 68 rel_galois … good s' (act_abs … (instr_map … p i) a) 60 record abstract_interpretation : Type[2] ≝ 61 { galois_conn:> galois_connection 62 ; instr_t : Type[0] 63 ; fetch : concr galois_conn → option instr_t 64 ; instr_map : instr_t → abs_instr … (abs_d galois_conn) 65 ; instr_map_ok : 66 ∀s,s': concr … galois_conn. ∀a: abs_d … galois_conn.∀l,i. 67 as_execute … l s s' → 68 fetch … s = Some ? i → 69 ∀I. instr_map … i = I → 70 galois_conn s a → galois_conn s' (〚I〛 a) 69 71 }. 70 71 72 73
Note: See TracChangeset
for help on using the changeset viewer.