Changeset 3039 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Mar 29, 2013, 5:45:14 PM (7 years ago)
Author:
tranquil
Message:
  • merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

  • JMP now correctly uses ACCDPTR argument
  • LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2714 r3039  
    7171 | <Heq2 >Hi >lookup_insert_miss
    7272   [ >lookup_insert_hit cases instr in Heq1;
    73      [2,3,8: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    74      |5,6: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ %
    75      |4,7: #x normalize nodelta #Heq1 >nth_append_second try %
     73     [2,3: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     74     |5,7: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ %
     75     |4,6: #x normalize nodelta #Heq1 >nth_append_second try %
    7676           <minus_n_n #abs cases abs
    7777     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     
    148148   |Cost (_:costlabel)⇒None jump_length
    149149   |Jnz _ _ _ ⇒ None ?
    150    |MovSuccessor _ _ _ ⇒ None ?
    151150   |Jmp (j:Identifier)⇒
    152151    Some jump_length
     
    155154    Some jump_length
    156155    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    157    |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
     156   |Mov _ _ _ ⇒ None jump_length]
    158157    in option
    159158    return λ_:(option jump_length).(jump_length×ℕ)
     
    206205        [ >lookup_insert_hit normalize nodelta
    207206          inversion instr in Heq1; normalize nodelta
    208           [4,7: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     207          [4,6: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    209208          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
    210209            lapply (destination_of_None_to_is_jump_false pi)
     
    214213            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    215214            ]
    216           |5,6: #x #y #z #Heqi
    217           |2,3,8: #x [3: #y] #Heqi ]
     215          |5,7: #x #y #z #Heqi
     216          |2,3: #x [3: #y] #Heqi ]
    218217          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
    219218          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
     
    266265   |Cost (_:costlabel)⇒None jump_length
    267266   |Jnz _ _ _ ⇒ None ?
    268    |MovSuccessor _ _ _ ⇒ None ?
    269267   |Jmp (j:Identifier)⇒
    270268    Some jump_length
     
    273271    Some jump_length
    274272    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    275    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     273   |Mov _ _ _⇒None jump_length]
    276274    in option
    277275    return λ_:(option jump_length).(jump_length×ℕ)
     
    432430    >Hpolicy1
    433431    [ cases instr in Heq1 Heq;
    434       [2,3,8: #x [3: #y] normalize nodelta #_ #_ %
    435       |5,6: #x #y #z #_ #_ %
     432      [2,3: #x [3: #y] normalize nodelta #_ #_ %
     433      |5,7: #x #y #z #_ #_ %
    436434      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
    437435          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
     
    585583            try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X)
    586584            <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone
    587             [1,3,4,6,7,9: @instruction_size_irrelevant try %
     585            [1,3,4,6,8: @instruction_size_irrelevant try %
    588586              whd in match is_jump; normalize nodelta >dest_None %
    589587            |*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
     
    738736    (* USE[pass]: lookup p = lookup old_sigma + added *)
    739737    >Hpolicy2
    740     [1,3,4,6,7,9:
     738    [1,3,4,6,8:
    741739      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    742740      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     
    746744      @plus_right_monotone @instruction_size_irrelevant try %
    747745      whd in match is_jump; normalize nodelta >y %
    748     |2,5,6,8:
     746    |*:
    749747      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
    750748      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
     
    828826   Some jump_length
    829827   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    830   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     828  |Mov _ _ _⇒None jump_length] *)
    831829 ∀inc_pc : ℕ.
    832830 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     
    869867   |Cost (_:costlabel)⇒None jump_length
    870868   |Jnz _ _ _ ⇒ None ?
    871    |MovSuccessor _ _ _ ⇒ None ?
    872869   |Jmp (j:Identifier)⇒
    873870    Some jump_length
     
    876873    Some jump_length
    877874    (select_call_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) c)
    878    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     875   |Mov _ _ _⇒None jump_length]
    879876    in option
    880877    return λ_:(option jump_length).(jump_length×ℕ)
     
    904901    Some jump_length
    905902    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    906    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     903   |Mov _ _ _⇒None jump_length]
    907904    in option
    908905    return λ_:(option jump_length).ℕ
     
    1002999      ]
    10031000      normalize nodelta cases instr in Hjump Heq1;
    1004       [1,9: #pi normalize nodelta cases pi
     1001      [1,8: #pi normalize nodelta cases pi
    10051002        try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    10061003        try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    1007       |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
    1008       |5,6,13,14: #x #y #z #abs cases abs
     1004      |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs
     1005      |5,12: #x #y #z #abs cases abs
    10091006      ]
    10101007      #id #Hjump normalize nodelta #Heq1
     
    10521049          #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    10531050          >p1 cases instr in Hjump Heq1;
    1054           [1,9: #pi normalize nodelta cases pi
     1051          [1,8: #pi normalize nodelta cases pi
    10551052            try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    10561053            try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    1057           |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
    1058           |5,6,13,14: #x #y #z #abs cases abs
     1054          |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs
     1055          |5,12: #x #y #z #abs cases abs
    10591056          ]
    10601057          #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1))
Note: See TracChangeset for help on using the changeset viewer.