Changeset 2899 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (7 years ago)
Author:
sacerdot
Message:
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2781 r2899  
    10441044     (foldr … (λi,l. assembly1 i @ l) [ ] p) 〈Stub …, Stub …〉〉).
    10451045*)
     1046
     1047definition ticks_of_instruction ≝
     1048  λi.
     1049    let trivial_code_memory ≝ assembly1 i in
     1050    let trivial_status ≝ load_code_memory trivial_code_memory in
     1051      \snd (fetch trivial_status (zero ?)).
     1052
     1053definition ticks_of0:
     1054    ∀p:pseudo_assembly_program.
     1055      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     1056  λprogram: pseudo_assembly_program.
     1057  λlookup_labels: Identifier → Word.
     1058  λsigma.
     1059  λpolicy.
     1060  λppc: Word.
     1061  λfetched.
     1062    match fetched with
     1063    [ Instruction instr ⇒
     1064      match instr with
     1065      [ JC lbl ⇒
     1066        let lookup_address ≝ sigma (lookup_labels lbl) in
     1067        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1068        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1069          if sj_possible then
     1070            〈2, 2〉
     1071          else
     1072            〈4, 4〉
     1073      | JMP _ ⇒ ? (*CSC: To be implemented*)
     1074      | JNC lbl ⇒
     1075        let lookup_address ≝ sigma (lookup_labels lbl) in
     1076        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1077        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1078          if sj_possible then
     1079            〈2, 2〉
     1080          else
     1081            〈4, 4〉
     1082      | JB bit lbl ⇒
     1083        let lookup_address ≝ sigma (lookup_labels lbl) in
     1084        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1085        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1086          if sj_possible then
     1087            〈2, 2〉
     1088          else
     1089            〈4, 4〉
     1090      | JNB bit lbl ⇒
     1091        let lookup_address ≝ sigma (lookup_labels lbl) in
     1092        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1093        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1094          if sj_possible then
     1095            〈2, 2〉
     1096          else
     1097            〈4, 4〉
     1098      | JBC bit lbl ⇒
     1099        let lookup_address ≝ sigma (lookup_labels lbl) in
     1100        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1101        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1102          if sj_possible then
     1103            〈2, 2〉
     1104          else
     1105            〈4, 4〉
     1106      | JZ lbl ⇒
     1107        let lookup_address ≝ sigma (lookup_labels lbl) in
     1108        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1109        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1110          if sj_possible then
     1111            〈2, 2〉
     1112          else
     1113            〈4, 4〉
     1114      | JNZ lbl ⇒
     1115        let lookup_address ≝ sigma (lookup_labels lbl) in
     1116        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1117        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1118          if sj_possible then
     1119            〈2, 2〉
     1120          else
     1121            〈4, 4〉
     1122      | CJNE arg lbl ⇒
     1123        let lookup_address ≝ sigma (lookup_labels lbl) in
     1124        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1125        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1126          if sj_possible then
     1127            〈2, 2〉
     1128          else
     1129            〈4, 4〉
     1130      | DJNZ arg lbl ⇒
     1131        let lookup_address ≝ sigma (lookup_labels lbl) in
     1132        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1133        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1134          if sj_possible then
     1135            〈2, 2〉
     1136          else
     1137            〈4, 4〉
     1138      | ADD arg1 arg2 ⇒
     1139        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     1140         〈ticks, ticks〉
     1141      | ADDC arg1 arg2 ⇒
     1142        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
     1143         〈ticks, ticks〉
     1144      | SUBB arg1 arg2 ⇒
     1145        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
     1146         〈ticks, ticks〉
     1147      | INC arg ⇒
     1148        let ticks ≝ ticks_of_instruction (INC ? arg) in
     1149         〈ticks, ticks〉
     1150      | DEC arg ⇒
     1151        let ticks ≝ ticks_of_instruction (DEC ? arg) in
     1152         〈ticks, ticks〉
     1153      | MUL arg1 arg2 ⇒
     1154        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
     1155         〈ticks, ticks〉
     1156      | DIV arg1 arg2 ⇒
     1157        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
     1158         〈ticks, ticks〉
     1159      | DA arg ⇒
     1160        let ticks ≝ ticks_of_instruction (DA ? arg) in
     1161         〈ticks, ticks〉
     1162      | ANL arg ⇒
     1163        let ticks ≝ ticks_of_instruction (ANL ? arg) in
     1164         〈ticks, ticks〉
     1165      | ORL arg ⇒
     1166        let ticks ≝ ticks_of_instruction (ORL ? arg) in
     1167         〈ticks, ticks〉
     1168      | XRL arg ⇒
     1169        let ticks ≝ ticks_of_instruction (XRL ? arg) in
     1170         〈ticks, ticks〉
     1171      | CLR arg ⇒
     1172        let ticks ≝ ticks_of_instruction (CLR ? arg) in
     1173         〈ticks, ticks〉
     1174      | CPL arg ⇒
     1175        let ticks ≝ ticks_of_instruction (CPL ? arg) in
     1176         〈ticks, ticks〉
     1177      | RL arg ⇒
     1178        let ticks ≝ ticks_of_instruction (RL ? arg) in
     1179         〈ticks, ticks〉
     1180      | RLC arg ⇒
     1181        let ticks ≝ ticks_of_instruction (RLC ? arg) in
     1182         〈ticks, ticks〉
     1183      | RR arg ⇒
     1184        let ticks ≝ ticks_of_instruction (RR ? arg) in
     1185         〈ticks, ticks〉
     1186      | RRC arg ⇒
     1187        let ticks ≝ ticks_of_instruction (RRC ? arg) in
     1188         〈ticks, ticks〉
     1189      | SWAP arg ⇒
     1190        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
     1191         〈ticks, ticks〉
     1192      | MOV arg ⇒
     1193        let ticks ≝ ticks_of_instruction (MOV ? arg) in
     1194         〈ticks, ticks〉
     1195      | MOVX arg ⇒
     1196        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
     1197         〈ticks, ticks〉
     1198      | SETB arg ⇒
     1199        let ticks ≝ ticks_of_instruction (SETB ? arg) in
     1200         〈ticks, ticks〉
     1201      | PUSH arg ⇒
     1202        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
     1203         〈ticks, ticks〉
     1204      | POP arg ⇒
     1205        let ticks ≝ ticks_of_instruction (POP ? arg) in
     1206         〈ticks, ticks〉
     1207      | XCH arg1 arg2 ⇒
     1208        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
     1209         〈ticks, ticks〉
     1210      | XCHD arg1 arg2 ⇒
     1211        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
     1212         〈ticks, ticks〉
     1213      | RET ⇒
     1214        let ticks ≝ ticks_of_instruction (RET ?) in
     1215         〈ticks, ticks〉
     1216      | RETI ⇒
     1217        let ticks ≝ ticks_of_instruction (RETI ?) in
     1218         〈ticks, ticks〉
     1219      | NOP ⇒
     1220        let ticks ≝ ticks_of_instruction (NOP ?) in
     1221         〈ticks, ticks〉
     1222      ]
     1223    | Comment comment ⇒ 〈0, 0〉
     1224    | Cost cost ⇒ 〈0, 0〉
     1225    | Jnz _ _ _ ⇒ ? (*CSC: To be implemented*)
     1226    | MovSuccessor _ _ _ ⇒ ? (*CSC: To be implemented *)
     1227    | Jmp jmp ⇒
     1228      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1229      let do_a_long ≝ policy ppc in
     1230      let lookup_address ≝ sigma (lookup_labels jmp) in
     1231      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1232        if sj_possible ∧ ¬ do_a_long then
     1233          〈2, 2〉 (* XXX: SJMP *)
     1234        else
     1235        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1236          if mj_possible ∧ ¬ do_a_long then
     1237            〈2, 2〉 (* XXX: AJMP *)
     1238          else
     1239            〈2, 2〉 (* XXX: LJMP *)
     1240    | Call call ⇒
     1241      (* XXX: collapse the branches as they are identical? *)
     1242      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1243      let lookup_address ≝ sigma (lookup_labels call) in
     1244      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1245      let do_a_long ≝ policy ppc in
     1246      if mj_possible ∧ ¬ do_a_long then
     1247        〈2, 2〉 (* ACALL *)
     1248      else
     1249        〈2, 2〉 (* LCALL *)
     1250    | Mov dptr tgt ⇒ 〈2, 2〉
     1251    ].
     1252cases daemon (*CSC: The three new pseudoinstruction cases*)
     1253qed.
     1254
     1255definition ticks_of:
     1256    ∀p:pseudo_assembly_program.
     1257    ∀sigma:Word → Word. ∀policy:Word → bool.
     1258     ∀ppc:Word.
     1259      nat_of_bitvector … ppc < |code p| → nat × nat ≝
     1260  λprogram: pseudo_assembly_program.
     1261  λsigma.
     1262  λpolicy.
     1263  λppc: Word. λppc_ok.
     1264    let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
     1265    let addr_of ≝ λid.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
     1266    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
     1267     ticks_of0 program addr_of sigma policy ppc fetched.
Note: See TracChangeset for help on using the changeset viewer.