Changeset 2317 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Sep 3, 2012, 11:36:43 AM (7 years ago)
Author:
boender
Message:
  • small changes to make things compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2316 r2317  
    752752qed.
    753753
    754 (*definition sigma_safe_weak ≝
    755  λprefix:list labelled_instruction.λlabels:label_map.
    756  λsigma:ppc_pc_map.
    757  ∀i.i < |prefix| →
    758  let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
    759  ∀lbl.is_jump_to instr lbl →
    760  let paddr ≝ lookup_def … labels lbl 0 in
    761  let 〈j,src,dest〉 ≝
    762    let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
    763    let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
    764    let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
    765    〈j,pc_plus_jmp_length,addr〉 in     
    766  i < paddr →
    767  match j with
    768  [ short_jump ⇒ \fst (short_jump_cond src dest) = true
    769  | absolute_jump ⇒  \fst (absolute_jump_cond src dest) = true (*∧
    770       \fst (short_jump_cond src dest) = false*)
    771  | long_jump   ⇒ True (* do not talk about long jump *)
    772  ].*)
    773 
    774 (*lemma sigma_safe_weak_sigma_safe:
    775   ∀program.∀labels.∀old_sigma.∀sigma.
    776   sigma_safe program labels old_sigma sigma →
    777   sigma_safe_weak program labels sigma.
    778  #program #labels #old_sigma #sigma #Hsigma_safe
    779  #i #Hi lapply (Hsigma_safe i Hi)
    780  cases (nth i ? program 〈None ?, Comment []〉) #label #instr normalize nodelta
    781  #Hsigma_safe #dest #Hjump lapply (Hsigma_safe dest Hjump) -Hsigma_safe
    782  cases (lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) #pc #j
    783  normalize nodelta #Hsigma_safe #Hle
    784  >(not_le_to_leb_false … (lt_to_not_le … Hle)) in Hsigma_safe; normalize nodelta
    785  
    786 qed.*)
    787 
    788 lemma length_of_is_isize: ∀i.is_jump (Instruction i) →
    789   length_of i = instruction_size_jmplen short_jump (Instruction i).
    790  #i cases i
    791  try (#x #y #Hj) try (#x #Hj) try (#Hj) try (cases Hj) try (%)
    792  try ( @(subaddressing_mode_elim … x) #w )  try (%)
    793  cases x * #a1 #a2 normalize nodelta
    794  @(subaddressing_mode_elim … a1) try (#w %)
    795  @(subaddressing_mode_elim … a2) #w %
    796 qed.
    797 
    798754lemma jump_expansion_step9:
    799755 ∀program : list labelled_instruction.
Note: See TracChangeset for help on using the changeset viewer.