Changeset 1423 for src/ERTL


Ignore:
Timestamp:
Oct 19, 2011, 6:05:50 PM (9 years ago)
Author:
sacerdot
Message:
  • spill no longer used
  • BUG IN Interference: generating the destruct principle takes too long
  • ERTLToLTL not compiling ATM
Location:
src/ERTL
Files:
1 deleted
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1352 r1423  
    11include "ERTL/ERTL.ma".
    22include "LTL/LTL.ma".
    3 include "ERTL/spill.ma".
    43include "ASM/Arithmetic.ma".
    54
     
    3029
    3130definition num_locals ≝
    32   λglobals.
    33   λint_fun.
    34     colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
     31  λspilled_no.
     32  λglobals.
     33  λint_fun.
     34    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    3535
    3636definition stacksize ≝
    37   λglobals.
    38   λint_fun.
    39     colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
     37  λspilled_no.
     38  λglobals.
     39  λint_fun.
     40    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    4041
    4142definition adjust_off ≝
     43  λspilled_no.
    4244  λglobals.
    4345  λint_fun.
    4446  λoff.
    4547  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    46   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
     48  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in
    4749    sub.
    4850
    4951definition get_stack:
    50  ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
     52 nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
     53  λspilled_no.
    5154  λglobals: list ident.
    5255  λint_fun.
     
    5659  λl.
    5760  λoriginal_label.
    58     let off ≝ adjust_off globals int_fun off in
     61    let off ≝ adjust_off spilled_no globals int_fun off in
    5962    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    6063    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
     
    6871
    6972definition set_stack:
    70   ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
     73  nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    7174    → Register → label → ? ≝
     75  λspilled_no.
    7276  λglobals: list ident.
    7377  λint_fun.
     
    7781  λl.
    7882  λoriginal_label.
    79   let off ≝ adjust_off globals int_fun off in
     83  let off ≝ adjust_off spilled_no globals int_fun off in
    8084  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    8185  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
  • src/ERTL/Interference.ma

    r1282 r1423  
    11include "ERTL/ERTL.ma".
    22include "ERTL/liveness.ma".
     3include "basics/jmeq.ma".
    34
    45definition vertex ≝ register ⊎ Register.
     
    1718  ].
    1819
     20(* prop_colouring is the non interferece
     21   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
     22   registers *)
     23(* Wilmer: the generation of the destruct principle diverges;
     24   Ctr-C make the file pass *)
    1925record coloured_graph (v: valuation): Type[1] ≝
    20 {
    21   colouring: vertex → decision;
    22   prop_colouring: ∀l. ∀v1, v2: vertex.
    23     is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
     26{ colouring: vertex → decision
     27; spilled_no: nat
     28; prop_colouring: ∀l. ∀v1, v2: vertex.
     29   is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
     30; prop_colouring2:
     31   ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
     32; prop_colouring3:
     33   spilled_no = 0 ∨
     34    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
    2435}.
    2536
Note: See TracChangeset for help on using the changeset viewer.