Changeset 2757 for src/ASM/ASM.ma
 Timestamp:
 Mar 1, 2013, 7:13:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2754 r2757 4 4 include "common/LabelledObjects.ma". 5 5 include "joint/String.ma". 6 7 (* move! *) 8 definition 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. 6 10 7 11 definition Identifier ≝ identifier ASMTag. … … 987 991 The second associative list assigns to Identifiers meant to be entry points 988 992 of functions the name of the function (that lives in a different namespace) *) 989 definition preamble ≝ list (Identifier × Word) × (list (Identifier × ident)). 993 990 994 definition 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 996 definition 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 1006 lemma 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 #_ % 1010 qed. 1011 1012 lemma 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 ???); 1017 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff} 1018 lapply EQ EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta 1019 #EQ %{lbl0} @EQ 1020 qed. 1021 1022 lemma 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 % 1035 qed. 997 1036 998 1037 (* labels & instructions *) … … 1019 1058 ]. 1020 1059 1060 definition 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 1080 definition 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 1092 definition asm_cost_label : ∀mem : list labelled_instruction. 1093 (Σw : Word.nat_of_bitvector … w < mem) → option costlabel ≝ 1094 λmem,w_prf. 1095 match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with 1096 [ Cost c ⇒ Some ? c 1097  _ ⇒ None ? 1098 ]. 1099 1100 record 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 1111 definition object_code ≝ list Byte. 1112 definition costlabel_map ≝ BitVectorTrie costlabel 16. 1113 definition symboltable_type ≝ BitVectorTrie ident 16. 1114 record 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 1021 1124 1022 1125 (* If instruction i is a jump, then there will be something in the policy at … … 1060 1163 ]. 1061 1164 1062 definition is_jump_to ≝1063 λx:pseudo_instruction.λd:Identifier.1064 match x with1065 [ Instruction i ⇒ match i with1066 [ JC j ⇒ d = j1067  JNC j ⇒ d = j1068  JZ j ⇒ d = j1069  JNZ j ⇒ d = j1070  JB _ j ⇒ d = j1071  JNB _ j ⇒ d = j1072  JBC _ j ⇒ d = j1073  CJNE _ j ⇒ d = j1074  DJNZ _ j ⇒ d = j1075  _ ⇒ False1076 ]1077  Call c ⇒ d = c1078  Jmp j ⇒ d = j1079  _ ⇒ False1080 ].
Note: See TracChangeset
for help on using the changeset viewer.