Changeset 2762 for src/ASM


Ignore:
Timestamp:
Mar 2, 2013, 2:37:43 AM (7 years ago)
Author:
sacerdot
Message:

All repaired up to compiler.ma.

Note: one daemon is left for one final property of a pseudo-program
(code < 216). James implemented a check, but the commit was partial.
I will put the property in the record together with the other and, if
James commit the check, use it in the LINToASM pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2745 r2762  
    655655 ]
    656656qed.
    657  
     657
    658658(* The glue between Policy and Assembly. *)
    659659definition jump_expansion':
    660 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     660∀program:(Σp:pseudo_assembly_program.S (|code p|) < 2^16).
    661661 option (Σsigma_policy:(Word → Word) × (Word → bool).
    662662   let 〈sigma,policy〉≝ sigma_policy in
    663    sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
     663   sigma_policy_specification program sigma policy)
    664664   ≝
    665665 λprogram.
    666   let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
     666  let program' ≝ «code program,?» in
     667  let f: option ppc_pc_map ≝ je_fixpoint program' in
    667668  match f return λx.f = x → ? with
    668669  [ None ⇒ λp.None ?
     
    673674          jmpeqb jl long_jump)〉,?»
    674675  ] (refl ? f).
     676[2: % [@(pi2 … program) | @well_labelled_p ]]
    675677normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
    676 lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
     678lapply (pi2 ?? (je_fixpoint «code program,?»)) [2: >p | skip] normalize nodelta cases x
    677679#fpc #fpol #Hfpol cases Hfpol ** #Hfpol1 #Hfpol2 #Hfpol3 #Hfpol4
    678680@conj
    679681[ >Hfpol1 %
    680682| #ppc #ppc_ok normalize nodelta
    681   >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
    682        \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉))
     683  >(?:\fst (fetch_pseudo_instruction (code program) ppc ppc_ok) =
     684       \snd (nth (nat_of_bitvector … ppc) ? (code program) 〈None ?, Comment EmptyString〉))
    683685  [2: whd in match fetch_pseudo_instruction; normalize nodelta
    684686   >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
    685    cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)
     687   cases (nth (nat_of_bitvector ? ppc) ? (code program) 〈None ?, Comment EmptyString〉)
    686688   #lbl #ins % ]
    687689  lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok)
     
    709711      >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
    710712      >nat_of_bitvector_bitvector_of_nat_inverse
    711       [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     713      [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|code program|) (code program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    712714          >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
    713715          #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
    714       lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     716      lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|code program|) (code program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    715717      >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X
    716718    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
    717719       * until the end of the program *)
    718       elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
     720      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|code program|) (code program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
    719721      [ >bitvector_of_nat_inverse_nat_of_bitvector
    720722        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta
    721723        >nat_of_bitvector_bitvector_of_nat_inverse
    722724        [2: <Hfpc >Hfpol2 @Hpc ]
    723         elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
     725        elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|code program|) (code program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
    724726        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc
    725727        [ %1 >Hcompact in HSpc; #X @X
     
    740742              | * #Sxpc #Sxjl #SXEQ normalize nodelta
    741743                #Hpcompact
    742                 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
     744                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (code program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
    743745                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    744                 lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
     746                lapply (pc_increases (nat_of_bitvector ? ppc') (|code program|) (code program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
    745747                <Hfpol2 >Hfpc #Hle2
    746748                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
    747749                >bitvector_of_nat_inverse_nat_of_bitvector
    748750                >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
    749                 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
     751                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (code program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
    750752                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    751                 lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
     753                lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|code program|) (code program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
    752754                <Hfpol2 >Hfpc #Hle2
    753755                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
     
    756758                @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
    757759                normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
    758                 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H;
     760                cases (nth (nat_of_bitvector ? ppc') ? (code program) 〈None ?, Comment EmptyString〉) in H;
    759761                #lbl #ins normalize nodelta #X @sym_eq @X
    760762              ]
Note: See TracChangeset for help on using the changeset viewer.