Changeset 2102 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Jun 20, 2012, 4:51:35 PM (8 years ago)
Author:
boender
Message:
  • some small changes
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2101 r2102  
    116116      ]
    117117    | #Hnj
    118       (* USE: jump_not_in_policy (from fold and old_sigma) *)
     118      (* USE: not_jump_default (from fold and old_sigma) *)
    119119      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)
    120120      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
     
    127127  >H2 in H; normalize nodelta -H2 -x #H @conj
    128128  [ @conj [ @conj [ @conj [ @conj [ @conj
    129   [ (* USE[pass]: out_of_program_none, jump_not_in_policy, policy_increase (from fold) *)
     129  [ (* USE[pass]: out_of_program_none, not_jump_default, policy_increase (from fold) *)
    130130    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
    131131  | (* policy_compact_unsafe → policy_compact (in the end) *)
     
    165165                (* USE: added = 0 → policy_pc_equal *)
    166166                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    167                 [2,4,6,8: lapply ((pi2 ?? labels) x)
    168                   whd in match address_of_word_labels_code_mem;
    169                   normalize nodelta cases daemon (* XXX *) ]
     167                [2,4,6,8: @(label_in_program program labels x)
     168                  cases daemon (* XXX this has to come from somewhere else *)
     169                ]
    170170                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
    171171                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     
    185185                (* USE: added = 0 → policy_pc_equal *)
    186186                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    187                 [2,4,6,8: cases daemon (* XXX *)]
     187                [2,4,6,8: @(label_in_program program labels x)
     188                  cases daemon (* XXX this has to come from somewhere else *)]
    188189                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    189190                normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     
    199200                normalize nodelta
    200201                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    201                 [2,4,6,8: cases daemon (* XXX *)]
     202                [2,4,6,8: @(label_in_program program labels x)
     203                  cases daemon (* XXX this has to come from somewhere else *)]
    202204                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    203205                normalize nodelta
     
    224226               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    225227               <(plus_n_Sm i 0) <plus_n_O
    226                cases daemon (* XXX *)
     228               cases daemon (* XXX this needs subadressing mode magic, see above *)
    227229             ]
    228230           ]
     
    286288      ]
    287289    ]
    288   | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
     290  | (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi;
    289291    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    290292    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    291293      [ >lookup_insert_miss
    292294        [ >(nth_append_first ? i prefix ?? Hi)
    293           (* USE: jump_not_in_policy *)
     295          (* USE: not_jump_default *)
    294296          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
    295297        | @bitvector_of_nat_abs
     
    381383                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    382384                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    383                 (* USE: jump_not_in_policy (from old_sigma) *)
     385                (* USE: not_jump_default (from old_sigma) *)
    384386                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    385387                [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
     
    401403              ]
    402404            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    403               (* USE: jump_not_in_policy (from old_sigma) *)
     405              (* USE: not_jump_default (from old_sigma) *)
    404406              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    405407              [1,4,7: >prf >nth_append_second
Note: See TracChangeset for help on using the changeset viewer.