Changeset 2652 for src/ASM


Ignore:
Timestamp:
Feb 8, 2013, 11:49:55 AM (7 years ago)
Author:
sacerdot
Message:

String type changed definition.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2318 r2652  
    312312lemma measure_full: ∀program.∀policy.
    313313  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    314   is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
     314  is_jump (\snd (nth i ? program 〈None ?,Comment EmptyString〉)) →
    315315  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
    316316#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
     
    570570            #H @H ]
    571571            #i #Hi
    572             inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     572            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    573573            [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
    574574              >Feq in Geq; normalize nodelta cases Fno_ch
     
    675675| #ppc #ppc_ok normalize nodelta
    676676  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
    677        \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))
     677       \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉))
    678678  [2: whd in match fetch_pseudo_instruction; normalize nodelta
    679    >(nth_safe_nth … 〈None ?, Comment []〉)
    680    cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     679   >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
     680   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)
    681681   #lbl #ins % ]
    682682  lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok)
     
    750750                >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
    751751                @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
    752                 normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
    753                 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
     752                normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
     753                cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H;
    754754                #lbl #ins normalize nodelta #X @sym_eq @X
    755755              ]
  • src/ASM/PolicyFront.ma

    r2318 r2652  
    2020  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
    2121  ∀i:ℕ.i < |prefix| →
    22   ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
     22  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment EmptyString〉)) →
    2323  \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump.
    2424 
     
    175175    [ None ⇒ False
    176176    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    177        pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))
     177       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment EmptyString〉))
    178178    ]
    179179  ].
     
    193193         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    194194         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    195          (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
     195         (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment EmptyString〉))
    196196    ]
    197197  ].
     
    227227  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
    228228  ∀i.i < |prefix| →
    229   let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment []〉 in
     229  let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in
    230230  (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump →
    231231    bool_to_Prop (¬is_call instr)) ∧
     
    565565definition nec_plus_ultra ≝
    566566  λprogram:list labelled_instruction.λp:ppc_pc_map.
    567   ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
     567  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) →
    568568  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
    569569 
     
    627627        type *)
    628628      cut (instruction_size_jmplen jl
    629        (\snd (nth i ? program 〈None ?, Comment []〉)) =
     629       (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) =
    630630       instruction_size … (bitvector_of_nat ? i)
    631        (\snd (nth i ? program 〈None ?, Comment []〉)))
     631       (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    632632      [6: #H <H @Hcp_unsafe
    633633      |5: whd in match (instruction_size_jmplen ??);
     
    635635          whd in match (assembly_1_pseudoinstruction …);
    636636          whd in match (expand_pseudo_instruction …);
    637           normalize nodelta inversion (nth i ? program 〈None ?,Comment []〉) in Hsafe;
     637          normalize nodelta inversion (nth i ? program 〈None ?,Comment EmptyString〉) in Hsafe;
    638638          #lbl #instr cases instr
    639639          [1: #pi normalize nodelta cases pi
     
    696696                [1,5,9,13,17,21,25,29,33,37,41:
    697697                  whd in match fetch_pseudo_instruction; normalize nodelta
    698                   >(nth_safe_nth … 〈None ?, Comment []〉) >nat_of_bitvector_bitvector_of_nat_inverse
     698                  >(nth_safe_nth … 〈None ?, Comment EmptyString〉) >nat_of_bitvector_bitvector_of_nat_inverse
    699699                  [1: >Hnth_eq in ⊢ (??%?);
    700700                  |3: >Hnth_eq in ⊢ (??%?);
  • src/ASM/PolicyStep.ma

    r2317 r2652  
    927927 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    928928 [ >nth_append_first [2: @Hi] lapply (Hsigma_safe i Hi)
    929    inversion (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins #Heq normalize nodelta
     929   inversion (nth i ? prefix 〈None ?, Comment EmptyString〉) #lbl #ins #Heq normalize nodelta
    930930   #Hsafe #dest #Hjump lapply (Hsafe dest Hjump) -Hsafe
    931931   inversion (leb (lookup_def … labels dest 0) i) #Hle normalize nodelta
     
    12011201  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    12021202    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    1203     inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     1203    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    12041204    [ #Hj
    12051205      (* USE: policy_increase (from fold) *)
Note: See TracChangeset for help on using the changeset viewer.