Changeset 2317


Ignore:
Timestamp:
Sep 3, 2012, 11:36:43 AM (7 years ago)
Author:
boender
Message:
  • small changes to make things compile
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2316 r2317  
    566566        ]
    567567        | @(equal_compact_unsafe_compact ? Fp)
    568           [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
    569             #H @H #i #Hi
     568          [1,2:
     569            [1: lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
     570            #H @H ]
     571            #i #Hi
    570572            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    571             [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
     573            [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
    572574              >Feq in Geq; normalize nodelta cases Fno_ch
    573               [ normalize nodelta #Heq
     575              [1,3: normalize nodelta #Heq
    574576                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
    575               | normalize nodelta cases (jump_expansion_step ???)
     577              |2,4: normalize nodelta cases (jump_expansion_step ???)
    576578                #x cases x -x #stch #sto normalize nodelta cases sto
    577                 [ normalize nodelta #_ #X destruct (X)
    578                 | -sto #stp normalize nodelta #Hst #Heq
     579                [1,3: normalize nodelta #_ #X destruct (X)
     580                |2,4: -sto #stp normalize nodelta #Hst #Heq
    579581                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
    580582                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
    581                    lapply (Hfull i Hi ?) [>Hj %]
     583                   lapply (Hfull i Hi ?) [1,3: >Hj %]
    582584                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    583585                   #fp #fj #Hfj >Hfj normalize nodelta
    584586                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
    585587                   #stp #stj cases stj normalize nodelta
    586                    [1,2: #H cases H #H2 cases H2 destruct (H2)
    587                    |3: #_ @refl
     588                   [1,2,4,5: #H cases H #H2 cases H2 destruct (H2)
     589                   |3,6: #_ @refl
    588590                   ]
    589                  ]
    590                ]
    591              | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %]
    592                 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] %
     591                ]
    593592              ]
    594             | cases daemon (* true, but have to add to properties in some way *)
    595             | @(proj2 ?? (proj1 ?? HGp))
     593            |2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %]
     594              >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] %
    596595            ]
    597           ]
    598           | @(proj2 ?? HGp)
     596          | cases daemon (* true, but have to add to properties in some way *)
     597          | cases daemon
     598          | @(proj2 ?? (proj1 ?? HGp))
    599599          ]
    600600        ]
     601        | @(proj2 ?? HGp)
     602        ]
    601603      ]
    602604    ]
    603   | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
    604     #x cases x -x #nch #npol normalize nodelta #Hnpol
    605     #x cases x -x #Sch #Spol normalize nodelta #HSpol
    606     cases npol in Hnpol; cases Spol in HSpol;
    607     [ #Hnpol #HSpol %1 //
    608     |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    609       #H destruct (H)
    610     |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
    611         cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    612         #x1 #x2
    613         cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    614         #y1 #y2 normalize nodelta
    615         @dec_eq_jump_length
    616     ]
    617   ]
     605  ]
     606| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     607  #x cases x -x #nch #npol normalize nodelta #Hnpol
     608  #x cases x -x #Sch #Spol normalize nodelta #HSpol
     609  cases npol in Hnpol; cases Spol in HSpol;
     610  [ #Hnpol #HSpol %1 //
     611  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
     612    #H destruct (H)
     613  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
     614      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     615      #x1 #x2
     616      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     617      #y1 #y2 normalize nodelta
     618      @dec_eq_jump_length
     619  ]
     620]
    618621qed.
    619622
  • 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.