Changeset 2700


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (6 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2688 r2700  
    11include "ASM/BitVector.ma".
    22include "ASM/Util.ma".
    3 (* include "arithmetics/exp.ma". <-- this does not make it compile on latest matita + Cerco *)
     3include "arithmetics/exp.ma".
    44
    55definition addr16_of_addr11: Word → Word11 → Word ≝
     
    185185 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/
    186186 |1,3: @(transitive_le … (2 * (S m)))
    187   [2,4: /2 by le_times/
     187  [2,4: whd in ⊢ (??%); /2 by le_plus/
    188188  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
    189189qed. 
  • src/ASM/Policy.ma

    r2653 r2700  
    322322      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    323323      normalize nodelta
    324       [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     324      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le
     325        @monotonic_lt_times_r [/2/] %
    325326      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    326327        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
     
    333334    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    334335    normalize nodelta
    335     [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     336    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le
     337      @monotonic_lt_times_r try % /2/
    336338    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    337339      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
  • src/ASM/Util.ma

    r2673 r2700  
    784784    mk_Prod … (m ÷ n) (modulus m n).
    785785   
    786 let rec exponential (m: nat) (n: nat) on n ≝
    787   match n with
    788     [ O ⇒ S O
    789     | S o ⇒ m * exponential m o
    790     ].
    791 
    792 interpretation "Nat exponential" 'exp n m = (exponential n m).
    793    
    794786notation "hvbox(a break ⊎ b)"
    795787 left associative with precedence 55
  • src/ERTLptr/ERTLptrToLTL.ma

    r2697 r2700  
    418418  ]〉).
    419419
    420 definition translate_data : ∀globals.
     420definition translate_data :
     421 fixpoint_computer → coloured_graph_computer →
     422 ∀globals.
    421423  joint_closed_internal_function ERTLptr globals →
    422424  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
    423 λglobals,int_fun.
     425λthe_fixpoint,build,globals,int_fun.
    424426(* colour registers *)
    425 let after ≝ analyse_liveness globals int_fun in
     427let after ≝ analyse_liveness the_fixpoint globals int_fun in
    426428let coloured_graph ≝ build after in
    427429(* compute new stack size *)
     
    441443qed.
    442444
    443 definition ertlptr_to_ltl: ertlptr_program → ltl_program ≝
    444   b_graph_transform_program … translate_data.
     445definition ertlptr_to_ltl:
     446 fixpoint_computer → coloured_graph_computer → ertlptr_program → ltl_program ≝
     447  λthe_fixpoint,build.
     448   b_graph_transform_program … (translate_data the_fixpoint build).
  • src/ERTLptr/Interference.ma

    r2693 r2700  
    1919}.
    2020
    21 axiom build: ∀valuation. coloured_graph valuation.
     21definition coloured_graph_computer ≝ ∀valuation. coloured_graph valuation.
  • src/ERTLptr/liveness.ma

    r2693 r2700  
    279279
    280280definition analyse_liveness ≝
    281   λglobals.
    282   λint_fun.
    283     the_fixpoint ? (liveafter globals int_fun).
     281  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
     282   the_fixpoint ? (liveafter globals int_fun).
    284283
    285284definition vertex ≝ register + Register.
  • src/compiler.ma

    r2697 r2700  
    2626   axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2727
    28 (* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
    29 axiom the_fixpoint : fixpoint.
    30 axiom build : ∀valuation. coloured_graph valuation.
    31 *)
     28axiom compute_fixpoint : fixpoint_computer.
     29axiom colour_graph : coloured_graph_computer.
    3230
    3331definition back_end : RTLabs_program → pseudo_assembly_program ≝
     
    3634  let p ≝ rtl_to_ertl p in
    3735  let p ≝ ertl_to_ertlptr p in
    38   let p ≝ ertlptr_to_ltl p in (* TODO: abstract over colouring *)
     36  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    3937  let p ≝ ltl_to_lin p in
    4038          lin_to_asm p.
     
    4846axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
    4947
    50 (* include "ASM/Policy.ma".
     48(* Only sloow include "ASM/Policy.ma".
     49*)include "ASM/PolicyStep.ma". include "arithmetics/nat.ma". axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     50 option (Σsigma_policy:(Word → Word) × (Word → bool).
     51   let 〈sigma,policy〉≝ sigma_policy in
     52   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy).
    5153
    5254definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     
    6163cases daemon
    6264qed.
    63 *)
    6465
    6566include "ASM/ASMCosts.ma".
  • src/utilities/fixpoints.ma

    r2174 r2700  
    2222}.
    2323
    24 axiom the_fixpoint : ∀latt.fixpoint latt.
     24definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
Note: See TracChangeset for help on using the changeset viewer.