Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (8 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/AssemblyProof.ma

    r2516 r2899  
    4646  ]
    4747qed.
    48 
    49 definition ticks_of_instruction ≝
    50   λi.
    51     let trivial_code_memory ≝ assembly1 i in
    52     let trivial_status ≝ load_code_memory trivial_code_memory in
    53       \snd (fetch trivial_status (zero ?)).
    5448
    5549lemma fetch_assembly:
     
    146140  ∀sigma: Word → Word.
    147141  ∀policy: Word → bool.
    148   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     142  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
    149143  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    150144  ∀ppc.∀ppc_ok.
    151145  ∀code_memory.
    152   let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    153   let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
     146  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (preamble program)) x (zero 16) in
     147  let pi ≝  \fst  (fetch_pseudo_instruction (code program) ppc ppc_ok) in
    154148  let pc ≝ sigma ppc in
    155149  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     
    186180   sigma in the out-of-bounds region too. *)     
    187181lemma assembly_ok:
    188   ∀program.
    189   ∀length_proof: |\snd program| ≤ 2^16.
     182  ∀program: pseudo_assembly_program.
     183  ∀length_proof: |code program| ≤ 2^16.
    190184  ∀sigma: Word → Word.
    191185  ∀policy: Word → bool.
    192186  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    193   ∀assembled.
     187  ∀assembled: object_code.
    194188  ∀costs': BitVectorTrie costlabel 16.
    195   let 〈preamble, instr_list〉 ≝ program in
     189  let preamble ≝ preamble program in
     190  let instr_list ≝ code program in
    196191  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
    197192  let datalabels ≝ construct_datalabels preamble in
    198193  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    199     〈assembled,costs'〉 = assembly program sigma policy →
     194    let loc ≝ pi1 … (assembly program sigma policy) in
     195    let assembled ≝ oc loc in
     196    let costs' ≝ costlabels loc in
    200197      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    201198        let code_memory ≝ load_code_memory assembled in
    202199        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    203200          ∀ppc.∀ppc_ok.
    204             let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
     201            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in     
    205202            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    206203            let pc ≝ sigma ppc in
     
    209206                  sigma newppc = add … pc (bitvector_of_nat … len).
    210207  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    211   cases (assembly program sigma policy) * #assembled' #costs''
    212   @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
    213   cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
     208  cases (assembly program sigma policy) * #assembled' #costs'' #symbol_table #fpc #inj
     209  cut (|code program| ≤ 2^16) [ // ] #instr_list_ok
    214210  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
    215211  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    216   * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     212  * * #assembly_ok1 #assembly_ok3 #assembly_ok2
    217213  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    218214  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     
    225221  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
    226222      >snd_fetch_pseudo_instruction
    227       cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
     223      cases sigma_policy_witness #_ #H cases (H ? ppc_ok) -H
    228224      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
    229225      >eq_fetch_pseudo_instruction whd in match instruction_size;
     
    261257lemma fetch_assembly_pseudo2:
    262258  ∀program.
    263   ∀length_proof: |\snd program| ≤ 2^16.
     259  ∀length_proof: |code program| ≤ 2^16.
    264260  ∀sigma.
    265261  ∀policy.
    266262  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    267263  ∀ppc.∀ppc_ok.
    268   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    269   let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
     264  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
     265  let res ≝ pi1 … (assembly program sigma policy) in
     266  let assembled ≝ oc res in
     267  let cost' ≝ costlabels res in
    270268  let code_memory ≝ load_code_memory assembled in
    271   let data_labels ≝ construct_datalabels (\fst program) in
     269  let data_labels ≝ construct_datalabels (preamble program) in
    272270  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    273271  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    274   let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
     272  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
    275273  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    276274    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    277   * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
     275  * #preamble #instr_list #code_size_ok #renamed_symbol #final_label
     276  #inj #well_labelled #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
    278277  @pair_elim #labels #costs #create_label_map_refl
    279   @pair_elim #assembled #costs' #assembled_refl
     278  letin res ≝ (assembly ???)
     279  letin assembled ≝ (oc ?)
     280  letin costs' ≝ (costlabels ?)
    280281  letin code_memory ≝ (load_code_memory ?)
    281282  letin data_labels ≝ (construct_datalabels ?)
    282283  letin lookup_labels ≝ (λx. ?)
    283284  letin lookup_datalabels ≝ (λx. ?)
    284   @pair_elim #pi #newppc #fetch_pseudo_refl
    285   lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
     285  lapply (assembly_ok ?? sigma policy sigma_policy_specification_witness assembled costs')
    286286  normalize nodelta try assumption
    287287  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
    288   lapply (H (sym_eq … assembled_refl)) -H
     288  lapply (H … ppc_ok) -H
     289  @pair_elim #pi #newppc #EQpi_neqppc
     290(*CSC: was working, to be repaired after change in datatypes representation
    289291  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
    290292  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
     
    295297  >EQ4 #H1 cases (H ppc_ok)
    296298  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    297   >fetch_pseudo_refl in H1; #assm @assm assumption
     299  >fetch_pseudo_refl in H1; #assm @assm assumption *) cases daemon
    298300qed.
    299301
     
    740742    | Cost _ ⇒ Some … M
    741743    | Jmp _ ⇒ Some … M
     744    | Jnz _ _ _ ⇒ Some … M
     745    | MovSuccessor _ _ _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
    742746    | Call a ⇒
    743747      let a' ≝ addr_of a s in
     
    789793           None ?
    790794       | JC addr1 ⇒ Some ? M
     795       | JMP _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
    791796       | JNC addr1 ⇒ Some ? M
    792797       | JB addr1 addr2 ⇒ Some ? M
     
    12631268(* XXX: check values returned for conditional jumps below! They are wrong,
    12641269        find correct values *)
    1265 definition ticks_of0:
    1266     ∀p:pseudo_assembly_program.
    1267       (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
    1268   λprogram: pseudo_assembly_program.
    1269   λlookup_labels: Identifier → Word.
    1270   λsigma.
    1271   λpolicy.
    1272   λppc: Word.
    1273   λfetched.
    1274     match fetched with
    1275     [ Instruction instr ⇒
    1276       match instr with
    1277       [ JC lbl ⇒
    1278         let lookup_address ≝ sigma (lookup_labels lbl) in
    1279         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1280         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1281           if sj_possible then
    1282             〈2, 2〉
    1283           else
    1284             〈4, 4〉
    1285       | JNC lbl ⇒
    1286         let lookup_address ≝ sigma (lookup_labels lbl) in
    1287         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1288         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1289           if sj_possible then
    1290             〈2, 2〉
    1291           else
    1292             〈4, 4〉
    1293       | JB bit lbl ⇒
    1294         let lookup_address ≝ sigma (lookup_labels lbl) in
    1295         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1296         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1297           if sj_possible then
    1298             〈2, 2〉
    1299           else
    1300             〈4, 4〉
    1301       | JNB bit lbl ⇒
    1302         let lookup_address ≝ sigma (lookup_labels lbl) in
    1303         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1304         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1305           if sj_possible then
    1306             〈2, 2〉
    1307           else
    1308             〈4, 4〉
    1309       | JBC bit lbl ⇒
    1310         let lookup_address ≝ sigma (lookup_labels lbl) in
    1311         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1312         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1313           if sj_possible then
    1314             〈2, 2〉
    1315           else
    1316             〈4, 4〉
    1317       | JZ lbl ⇒
    1318         let lookup_address ≝ sigma (lookup_labels lbl) in
    1319         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1320         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1321           if sj_possible then
    1322             〈2, 2〉
    1323           else
    1324             〈4, 4〉
    1325       | JNZ lbl ⇒
    1326         let lookup_address ≝ sigma (lookup_labels lbl) in
    1327         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1328         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1329           if sj_possible then
    1330             〈2, 2〉
    1331           else
    1332             〈4, 4〉
    1333       | CJNE arg lbl ⇒
    1334         let lookup_address ≝ sigma (lookup_labels lbl) in
    1335         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1336         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1337           if sj_possible then
    1338             〈2, 2〉
    1339           else
    1340             〈4, 4〉
    1341       | DJNZ arg lbl ⇒
    1342         let lookup_address ≝ sigma (lookup_labels lbl) in
    1343         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1344         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1345           if sj_possible then
    1346             〈2, 2〉
    1347           else
    1348             〈4, 4〉
    1349       | ADD arg1 arg2 ⇒
    1350         let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
    1351          〈ticks, ticks〉
    1352       | ADDC arg1 arg2 ⇒
    1353         let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
    1354          〈ticks, ticks〉
    1355       | SUBB arg1 arg2 ⇒
    1356         let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
    1357          〈ticks, ticks〉
    1358       | INC arg ⇒
    1359         let ticks ≝ ticks_of_instruction (INC ? arg) in
    1360          〈ticks, ticks〉
    1361       | DEC arg ⇒
    1362         let ticks ≝ ticks_of_instruction (DEC ? arg) in
    1363          〈ticks, ticks〉
    1364       | MUL arg1 arg2 ⇒
    1365         let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
    1366          〈ticks, ticks〉
    1367       | DIV arg1 arg2 ⇒
    1368         let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
    1369          〈ticks, ticks〉
    1370       | DA arg ⇒
    1371         let ticks ≝ ticks_of_instruction (DA ? arg) in
    1372          〈ticks, ticks〉
    1373       | ANL arg ⇒
    1374         let ticks ≝ ticks_of_instruction (ANL ? arg) in
    1375          〈ticks, ticks〉
    1376       | ORL arg ⇒
    1377         let ticks ≝ ticks_of_instruction (ORL ? arg) in
    1378          〈ticks, ticks〉
    1379       | XRL arg ⇒
    1380         let ticks ≝ ticks_of_instruction (XRL ? arg) in
    1381          〈ticks, ticks〉
    1382       | CLR arg ⇒
    1383         let ticks ≝ ticks_of_instruction (CLR ? arg) in
    1384          〈ticks, ticks〉
    1385       | CPL arg ⇒
    1386         let ticks ≝ ticks_of_instruction (CPL ? arg) in
    1387          〈ticks, ticks〉
    1388       | RL arg ⇒
    1389         let ticks ≝ ticks_of_instruction (RL ? arg) in
    1390          〈ticks, ticks〉
    1391       | RLC arg ⇒
    1392         let ticks ≝ ticks_of_instruction (RLC ? arg) in
    1393          〈ticks, ticks〉
    1394       | RR arg ⇒
    1395         let ticks ≝ ticks_of_instruction (RR ? arg) in
    1396          〈ticks, ticks〉
    1397       | RRC arg ⇒
    1398         let ticks ≝ ticks_of_instruction (RRC ? arg) in
    1399          〈ticks, ticks〉
    1400       | SWAP arg ⇒
    1401         let ticks ≝ ticks_of_instruction (SWAP ? arg) in
    1402          〈ticks, ticks〉
    1403       | MOV arg ⇒
    1404         let ticks ≝ ticks_of_instruction (MOV ? arg) in
    1405          〈ticks, ticks〉
    1406       | MOVX arg ⇒
    1407         let ticks ≝ ticks_of_instruction (MOVX ? arg) in
    1408          〈ticks, ticks〉
    1409       | SETB arg ⇒
    1410         let ticks ≝ ticks_of_instruction (SETB ? arg) in
    1411          〈ticks, ticks〉
    1412       | PUSH arg ⇒
    1413         let ticks ≝ ticks_of_instruction (PUSH ? arg) in
    1414          〈ticks, ticks〉
    1415       | POP arg ⇒
    1416         let ticks ≝ ticks_of_instruction (POP ? arg) in
    1417          〈ticks, ticks〉
    1418       | XCH arg1 arg2 ⇒
    1419         let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
    1420          〈ticks, ticks〉
    1421       | XCHD arg1 arg2 ⇒
    1422         let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
    1423          〈ticks, ticks〉
    1424       | RET ⇒
    1425         let ticks ≝ ticks_of_instruction (RET ?) in
    1426          〈ticks, ticks〉
    1427       | RETI ⇒
    1428         let ticks ≝ ticks_of_instruction (RETI ?) in
    1429          〈ticks, ticks〉
    1430       | NOP ⇒
    1431         let ticks ≝ ticks_of_instruction (NOP ?) in
    1432          〈ticks, ticks〉
    1433       ]
    1434     | Comment comment ⇒ 〈0, 0〉
    1435     | Cost cost ⇒ 〈0, 0〉
    1436     | Jmp jmp ⇒
    1437       let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1438       let do_a_long ≝ policy ppc in
    1439       let lookup_address ≝ sigma (lookup_labels jmp) in
    1440       let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1441         if sj_possible ∧ ¬ do_a_long then
    1442           〈2, 2〉 (* XXX: SJMP *)
    1443         else
    1444         let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    1445           if mj_possible ∧ ¬ do_a_long then
    1446             〈2, 2〉 (* XXX: AJMP *)
    1447           else
    1448             〈2, 2〉 (* XXX: LJMP *)
    1449     | Call call ⇒
    1450       (* XXX: collapse the branches as they are identical? *)
    1451       let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1452       let lookup_address ≝ sigma (lookup_labels call) in
    1453       let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    1454       let do_a_long ≝ policy ppc in
    1455       if mj_possible ∧ ¬ do_a_long then
    1456         〈2, 2〉 (* ACALL *)
    1457       else
    1458         〈2, 2〉 (* LCALL *)
    1459     | Mov dptr tgt ⇒ 〈2, 2〉
    1460     ].
    1461 
    1462 definition ticks_of:
    1463     ∀p:pseudo_assembly_program.
    1464       (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
    1465        nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    1466   λprogram: pseudo_assembly_program.
    1467   λlookup_labels.
    1468   λsigma.
    1469   λpolicy.
    1470   λppc: Word. λppc_ok.
    1471     let pseudo ≝ \snd program in
    1472     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    1473      ticks_of0 program lookup_labels sigma policy ppc fetched.
    14741270
    14751271(*
Note: See TracChangeset for help on using the changeset viewer.