Changeset 2762


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.

Location:
src
Files:
2 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              ]
  • src/compiler.ma

    r2754 r2762  
    5252definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    5353λp.
    54   let 〈preamble, list_instr〉 ≝ p in
    55   ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*);
    56   let p' ≝ 〈preamble, list_instr〉 in
    57   ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
     54(*  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *)
     55  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    5856  let sigma ≝ λppc. \fst sigma_pol ppc in
    5957  let pol ≝ λppc. \snd sigma_pol ppc in
    6058  OK ? (assembly p sigma pol).
    61   (* % [1: @list_instr_ok | cases daemon] *) cases daemon
     59  cases daemon
    6260qed.
    6361
     
    9088  ∀clight, code_memory, lbls.
    9189    let abstat ≝ ASM_abstract_status code_memory lbls in
    92 (*   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *)
    9390  as_cost_map abstat → clight_cost_map clight ≝
    94   λclight,code_memory,lbls,(*dec,*)k,asm_cost_map.
     91  λclight,code_memory,lbls,k,asm_cost_map.
    9592  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    96     (strong_decidable_in_codomain …) (* (* dec *) now eliminated as a hypothesis *)
    97     k asm_cost_map.
     93    (strong_decidable_in_codomain …) k asm_cost_map.
    9894
    9995include "ASM/ASMCostsSplit.ma".
     
    105101  let p ≝ back_end p in
    106102    ! p ← assembler p;
    107   let k ≝ ASM_cost_map p ? in
    108   let k' ≝ lift_cost_map_back_to_front
    109     p'
    110     (load_code_memory (\fst p))
    111     (\fst (\snd p))
    112     k
    113     in
     103  let k ≝ ASM_cost_map p in
     104  let k' ≝
     105   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
    114106  return 〈p, ❬p', k'❭〉.
    115  cases daemon
    116 qed.
Note: See TracChangeset for help on using the changeset viewer.