Changeset 2808


Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (6 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2806 r2808  
    4646
    4747definition get_stack:
    48  ∀globals.Register → nat → list (joint_seq LTL globals) ≝
    49  λglobals,r,off.
     48 ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝
     49 λglobals,localss,r,off.
     50 let off ≝ localss + off in
    5051 set_dp_by_offset ? off @
    5152 [ LOAD … A it it ] @
     
    5354
    5455definition set_stack_not_a :
    55  ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    56  λglobals,off,r.
     56 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
     57 λglobals,localss,off,r.
     58 let off ≝ localss + off in
    5759 set_dp_by_offset ? off @
    5860 [ A ← r
     
    6062
    6163definition set_stack_a :
    62  ∀globals.nat → list (joint_seq LTL globals) ≝
    63  λglobals,off.
     64 ∀globals.nat → nat → list (joint_seq LTL globals) ≝
     65 λglobals,localss,off.
    6466 [ RegisterST1 ← A ] @
    65  set_stack_not_a ? off RegisterST1.
     67 set_stack_not_a ? localss off RegisterST1.
    6668
    6769definition set_stack :
    68  ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    69  λglobals,off,r.
     70 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
     71 λglobals,localss,off,r.
    7072 if eq_Register r RegisterA then
    71    set_stack_a ? off
     73   set_stack_a ? localss off
    7274 else
    73    set_stack_not_a ? off r.
     75   set_stack_not_a ? localss off r.
    7476 
    7577definition set_stack_int :
    76   ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
    77   λglobals,off,int.
     78  ∀globals.nat → nat → Byte →  list (joint_seq LTL globals) ≝
     79  λglobals,localss,off,int.
     80  let off ≝ localss + off in
    7881  set_dp_by_offset ? off @
    7982  [ A ← int
     
    8184
    8285definition move :
    83   ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
    84   λglobals,carry_lives_after,dst,src.
     86  ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝
     87  λglobals,localss,carry_lives_after,dst,src.
    8588  match dst with
    8689  [ decision_colour dstr ⇒
     
    9396    | arg_decision_spill srco ⇒
    9497      preserve_carry_bit ? carry_lives_after
    95         (get_stack ? dstr srco)
     98        (get_stack ? localss dstr srco)
    9699    | arg_decision_imm int ⇒
    97100      [ A ← int ] @
     
    103106    [ arg_decision_colour srcr ⇒
    104107      preserve_carry_bit ? carry_lives_after
    105         (set_stack ? dsto srcr)
     108        (set_stack ? localss dsto srcr)
    106109    | arg_decision_spill srco ⇒
    107110      if eqb srco dsto then [ ] else
    108111      preserve_carry_bit ? carry_lives_after
    109         (get_stack ? RegisterA srco @
    110          set_stack ? dsto RegisterA)
     112        (get_stack ? localss RegisterA srco @
     113         set_stack ? localss dsto RegisterA)
    111114    | arg_decision_imm int ⇒
    112115      preserve_carry_bit ? carry_lives_after
    113         (set_stack_int ? dsto int)
     116        (set_stack_int ? localss dsto int)
    114117    ]
    115118  ].
     
    169172
    170173definition translate_op2 :
    171   ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    172   λglobals,carry_lives_after,op,dst,arg1,arg2.
     174  ∀globals.nat → bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     175  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
    173176  (* this won't preserve the carry bit if op does not set it: left to next function *)
    174177  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
    175178  (preserve_carry_bit ?
    176179    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
    177     (move ? false RegisterB arg2 @
    178      move ? false RegisterA arg1) @
     180    (move ? localss false RegisterB arg2 @
     181     move ? localss false RegisterA arg1) @
    179182    [ A ← A .op. RegisterB ] @
    180183    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    181     move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
     184    move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA).
    182185
    183186definition translate_op2_smart :
    184   ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    185   λglobals,carry_lives_after,op,dst,arg1,arg2.
     187  ∀globals.nat → bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     188  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
    186189  (* if op does not set carry bit (⇒ it does not use it either) then it must be
    187190    preserved *)
     
    191194    (match arg2 with
    192195    [ arg_decision_colour arg2r ⇒
    193       move ? (uses_carry op) RegisterA arg1 @
     196      move ? localss (uses_carry op) RegisterA arg1 @
    194197      [ A ← A .op. arg2r ] @
    195       move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     198      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    196199    | arg_decision_imm arg2i ⇒
    197       move ? (uses_carry op) RegisterA arg1 @
     200      move ? localss (uses_carry op) RegisterA arg1 @
    198201      [ A ← A .op. arg2i ] @
    199       move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     202      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    200203    | _ ⇒
    201204      if commutative op then
    202205        match arg1 with
    203206        [ arg_decision_colour arg1r ⇒
    204           move ? (uses_carry op) RegisterA arg2 @
     207          move ? localss (uses_carry op) RegisterA arg2 @
    205208          [ A ← A .op. arg1r ] @
    206           move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     209          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    207210        | arg_decision_imm arg1i ⇒
    208           move ? (uses_carry op) RegisterA arg2 @
     211          move ? localss (uses_carry op) RegisterA arg2 @
    209212          [ A ← A .op. arg1i ] @
    210           move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     213          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    211214        | _ ⇒
    212           translate_op2 ? carry_lives_after op dst arg1 arg2
     215          translate_op2 ? localss carry_lives_after op dst arg1 arg2
    213216        ]
    214217      else
    215         translate_op2 ? carry_lives_after op dst arg1 arg2
     218        translate_op2 ? localss carry_lives_after op dst arg1 arg2
    216219    ]).
    217220
     
    225228
    226229definition translate_op1 :
    227   ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
    228   λglobals,carry_lives_after,op,dst,arg.
     230  ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
     231  λglobals,localss,carry_lives_after,op,dst,arg.
    229232  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
    230233  preserve_carry_bit ? preserve_carry
    231     (move ? false RegisterA arg @
     234    (move ? localss false RegisterA arg @
    232235     OP1 … op it it ::
    233      move ? false dst RegisterA).
     236     move ? localss false dst RegisterA).
    234237
    235238definition translate_opaccs :
    236   ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    237   λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
     239  ∀globals.nat → bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     240  λglobals,localss,carry_lives_after,op,dst1,dst2,arg1,arg2.
    238241  (* OPACCS always has dead carry bit and sets it to zero *)
    239   move ? false RegisterB arg2 @
    240   move ? false RegisterA arg1 @
     242  move ? localss false RegisterB arg2 @
     243  move ? localss false RegisterA arg1 @
    241244  OPACCS … op it it it it ::
    242   move ? false dst1 RegisterA @
    243   move ? false dst2 RegisterB @
     245  move ? localss false dst1 RegisterA @
     246  move ? localss false dst2 RegisterB @
    244247  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
    245248    [CLEAR_CARRY ??]
     
    248251(* does not preserve carry bit *)
    249252definition move_to_dp :
    250   ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    251   λglobals,arg1,arg2.
     253  ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     254  λglobals,localss,arg1,arg2.
    252255  if ¬arg_is_spilled arg1 then
    253     move ? false RegisterDPH arg2 @
     256    move ? localss false RegisterDPH arg2 @
    254257    (* does not change dph because arg1 is not spilled *)
    255     move ? false RegisterDPL arg1
     258    move ? localss false RegisterDPL arg1
    256259  else if ¬arg_is_spilled arg2 then
    257     move ? false RegisterDPL arg1 @
     260    move ? localss false RegisterDPL arg1 @
    258261    (* does not change dpl because arg2 is not spilled *)
    259     move ? false RegisterDPH arg2
     262    move ? localss false RegisterDPH arg2
    260263  else
    261264    (* using B as temporary, as moving spilled registers tampers with DPTR *)
    262     move ? false RegisterB arg1 @
    263     move ? false RegisterDPH arg2 @
    264     move ? false RegisterDPL RegisterB.
     265    move ? localss false RegisterB arg1 @
     266    move ? localss false RegisterDPH arg2 @
     267    move ? localss false RegisterDPL RegisterB.
    265268
    266269definition translate_store : 
    267   ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    268   λglobals,carry_lives_after,addr1,addr2,src.
     270  ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     271  λglobals,localss,carry_lives_after,addr1,addr2,src.
    269272  (* requires src != RegisterA and RegisterB *)
    270273  preserve_carry_bit ? (carry_lives_after ∧
    271274    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
    272     (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
     275    (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in
    273276     (if arg_is_spilled src then
    274         move ? false RegisterST0 src @
     277        move ? localss false RegisterST0 src @
    275278        move_to_dptr @
    276279        [ A ← RegisterST0]
     
    279282
    280283definition translate_load : 
    281   ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    282   λglobals,carry_lives_after,dst,addr1,addr2.
     284  ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     285  λglobals,localss,carry_lives_after,dst,addr1,addr2.
    283286  preserve_carry_bit ? (carry_lives_after ∧
    284287    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    285     (move_to_dp ? addr1 addr2 @
     288    (move_to_dp ? localss addr1 addr2 @
    286289     [ LOAD … A it it ] @
    287      move ? false dst RegisterA).
     290     move ? localss false dst RegisterA).
    288291
    289292definition translate_address :
    290   ∀globals.bool → ∀i.i ∈ globals → decision → decision →
     293  ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision →
    291294  list (joint_seq LTL globals) ≝
    292   λglobals,carry_lives_after,id,prf,addr1,addr2.
     295  λglobals,localss,carry_lives_after,id,prf,addr1,addr2.
    293296  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    294297    (ADDRESS LTL ? id prf it it ::
    295      move ? false addr1 RegisterDPL @
    296      move ? false addr2 RegisterDPH).
     298     move ? localss false addr1 RegisterDPL @
     299     move ? localss false addr2 RegisterDPH).
    297300
    298301definition translate_low_address :
    299   ∀globals.bool → decision → label →
     302  ∀globals.nat → bool → decision → label →
    300303  list (joint_seq LTL globals) ≝
    301   λglobals,carry_lives_after,dst,lbl.
     304  λglobals,localss,carry_lives_after,dst,lbl.
    302305  match dst return λ_.list (joint_seq LTL globals) with
    303306  [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
    304307  | _ ⇒
    305     LOW_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     308    LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    306309  ].
    307310
    308311definition translate_high_address :
    309   ∀globals.bool → decision → label →
     312  ∀globals.nat → bool → decision → label →
    310313  list (joint_seq LTL globals) ≝
    311   λglobals,carry_lives_after,dst,lbl.
     314  λglobals,localss,carry_lives_after,dst,lbl.
    312315  match dst return λ_.list (joint_seq LTL globals) with
    313316  [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
    314317  | _ ⇒
    315     HIGH_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     318    HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    316319  ].
    317320
    318321definition translate_step:
    319   ∀globals.∀after : valuation register_lattice.
     322  ∀globals.nat → ∀after : valuation register_lattice.
    320323  coloured_graph after →
    321324  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
    322   λglobals,after,grph,stack_sz,lbl,s.
     325  λglobals,localss,after,grph,stack_sz,lbl,s.
    323326  bret … (
    324327  let lookup ≝ λr.colouring … grph (inl … r) in
     
    328331    ] in
    329332  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
    330   let move ≝ move globals carry_lives_after in
     333  let move ≝ move globals localss carry_lives_after in
    331334  match s with
    332335  [ step_seq s' ⇒
     
    340343      [ PUSH … A ]
    341344    | STORE addr1 addr2 srcr ⇒
    342       translate_store ? carry_lives_after
     345      translate_store ? localss carry_lives_after
    343346        (lookup_arg addr1)
    344347        (lookup_arg addr2)
    345348        (lookup_arg srcr)
    346349    | LOAD dstr addr1 addr2 ⇒
    347       translate_load ? carry_lives_after
     350      translate_load ? localss carry_lives_after
    348351        (lookup dstr)
    349352        (lookup_arg addr1)
     
    352355    | SET_CARRY ⇒ [CLEAR_CARRY ??]
    353356    | OP2 op dst arg1 arg2 ⇒
    354       translate_op2_smart ? carry_lives_after op
     357      translate_op2_smart ? localss carry_lives_after op
    355358        (lookup dst)
    356359        (lookup_arg arg1)
    357360        (lookup_arg arg2)
    358361    | OP1 op dst arg ⇒
    359       translate_op1 ? carry_lives_after op
     362      translate_op1 ? localss carry_lives_after op
    360363        (lookup dst)
    361364        (lookup arg)
     
    373376      move dst src
    374377    | ADDRESS lbl prf dpl dph ⇒
    375       translate_address ? carry_lives_after
     378      translate_address ? localss carry_lives_after
    376379        lbl prf (lookup dpl) (lookup dph)
    377380    | OPACCS op dst1 dst2 arg1 arg2 ⇒
    378       translate_opaccs ? carry_lives_after op
     381      translate_opaccs ? localss carry_lives_after op
    379382        (lookup dst1) (lookup dst2)
    380383        (lookup_arg arg1) (lookup_arg arg2)
     
    389392          ]
    390393        | LOW_ADDRESS r1 l ⇒
    391            translate_low_address ? carry_lives_after (lookup r1) l
     394           translate_low_address ? localss carry_lives_after (lookup r1) l
    392395        | HIGH_ADDRESS r1 l ⇒
    393            translate_high_address ? carry_lives_after (lookup r1) l       
     396           translate_high_address ? localss carry_lives_after (lookup r1) l       
    394397        ]
    395398    ]
     
    403406      | inr dp ⇒
    404407        let 〈dpl, dph〉 ≝ dp in
    405         〈add_dummy_variance … (move_to_dp (lookup_arg dpl) (lookup_arg dph)),
     408        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)),
    406409         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    407410      ]
     
    436439    (* added_prologue ≝ *) [ ]
    437440    (* new_regs ≝ *) [ ]
    438     (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
     441    (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    439442    (* f_fin ≝ *) (translate_fin_step globals)
    440443    ????).
  • src/RTLabs/RTLabsToRTL.ma

    r2774 r2808  
    124124    mk_joint_internal_function RTL globals
    125125      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
    126       params' (joint_if_stacksize … def')
     126      params' (joint_if_stacksize … def') (joint_if_local_stacksize … def')
    127127      (joint_if_code … def') (joint_if_entry … def') in
    128128   〈def'', lenv〉. @hide_prf
     
    284284  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    285285    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    286     [ADDRESS RTL globals id ? r1 r2]
     286    [ADDRESS RTL globals id ? r1 r2 ;
     287     r1 ← r1 .Add. byte_of_nat … offset ;
     288     r2 ← r2 .Addc. zero_byte ]
    287289  | Oaddrstack offset ⇒ λcst_prf,prf.
    288290    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    289     [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
     291    [(rtl_stack_address r1 r2 : joint_seq RTL globals);
     292     r1 ← r1 .Add. byte_of_nat … offset ;
     293     r2 ← r2 .Addc. zero_byte ]
    290294  ] (pi2 … cst_sig).
    291295  @hide_prf
     
    10321036  let entry' ≝ f_entry def in
    10331037  let init ≝ mk_joint_internal_function RTL globals
    1034     luniverse' runiverse' [ ] [ ] stack_size'
     1038    luniverse' runiverse' [ ] [ ] stack_size' stack_size'
    10351039    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
    10361040  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
  • src/joint/Joint.ma

    r2783 r2808  
    475475  joint_if_result   : call_dest p;
    476476  joint_if_params   : paramsT p;
    477 (*CSC: XXXXX stacksize unused for LTL-...*)
    478477  joint_if_stacksize: nat;
     478  joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions
     479    (that are already on stack in the front end) *)
    479480  joint_if_code     : codeT p globals ;
    480481  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     
    552553      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    553554      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
     555       (joint_if_local_stacksize … int_fun)
    554556      graph entry (*exit*).
    555557
     
    571573   mk_joint_internal_function globals pars
    572574    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    573     (joint_if_params … p) (joint_if_stacksize … p)
     575    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    574576    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    575577
     
    580582   mk_joint_internal_function globals pars
    581583    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    582     (joint_if_params … p) (joint_if_stacksize … p)
     584    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    583585    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    584586   
     
    590592    mk_joint_internal_function …
    591593     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    592      (joint_if_params … p) (joint_if_stacksize … p)
     594     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    593595     code
    594596     (pi1 … (joint_if_entry … p))
  • src/joint/TranslateUtils.ma

    r2806 r2808  
    571571    runiv
    572572    (init_ret … data) (init_params … data) (init_stack_size … data)
     573    (joint_if_local_stacksize … def)
    573574    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
    574575    («pi1 … entry, mem_set_add_id …») in
  • src/joint/linearise.ma

    r2784 r2808  
    237237    ] n_prf
    238238  ] (chop_ok ? (λx.x∈visited) visiting).
     239(* cases daemon *)
    239240whd
    240241[ (* base case, visiting is all visited *)
     
    517518|
    518519]
     520(**)
    519521qed.
    520522
     
    703705| >commutative_plus change with (? ≤ |g|) %
    704706]
     707(* cases daemon *)
    705708**
    706709#visited #required #generated normalize nodelta ****
     
    810813  ]
    811814]
     815(**)
    812816qed.
    813817
     
    846850   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    847851   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    848    (joint_if_stacksize ?? f_sig) code entry (* exit is dummy! *), hide_prf ??»,
     852   (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
     853   code entry (* exit is dummy! *), hide_prf ??»,
    849854   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
    850855[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
  • src/joint/lineariseProof.ma

    r2570 r2808  
    209209definition graph_prog_params ≝
    210210λp,p',prog,stack_sizes.
    211 mk_prog_params (make_sem_graph_params p p') prog stack_sizes.
     211mk_prog_params (mk_sem_graph_params p p') prog stack_sizes.
    212212
    213213definition graph_abstract_status:
     
    223223definition lin_prog_params ≝
    224224λp,p',prog,stack_sizes.
    225 mk_prog_params (make_sem_lin_params p p') prog stack_sizes.
     225mk_prog_params (mk_sem_lin_params p p') prog stack_sizes.
    226226
    227227definition lin_abstract_status:
     
    296296 ≝
    297297  λp,p',prog,sigma,pc.
    298   let pars ≝ make_sem_graph_params p p' in
     298  let pars ≝ mk_sem_graph_params p p' in
    299299  let ge ≝ globalenv_noinit … prog in
    300300  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
     
    304304    ! lin_point ← sigma fd (point_of_pc pars pc) ;
    305305    return pc_of_point
    306     (make_sem_lin_params ? p') (pc_block pc) lin_point.
     306    (mk_sem_lin_params ? p') (pc_block pc) lin_point.
    307307
    308308definition well_formed_pc:
     
    574574  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    575575  (sigma : sigma_map p graph_prog) : Type[0] ≝
    576 { well_formed_frames : framesT (make_sem_graph_params p p') → Prop
    577 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
     576{ well_formed_frames : framesT (mk_sem_graph_params p p') → Prop
     577; sigma_frames : ∀frms.well_formed_frames frms → framesT (mk_sem_lin_params p p')
    578578; sigma_empty_frames_commute :
    579579  ∃prf.
    580   empty_framesT (make_sem_lin_params p p') =
    581   sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
    582 
    583 ; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
    584 ; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
     580  empty_framesT (mk_sem_lin_params p p') =
     581  sigma_frames (empty_framesT (mk_sem_graph_params p p')) prf
     582
     583; well_formed_regs : regsT (mk_sem_graph_params p p') → Prop
     584; sigma_regs : ∀regs.well_formed_regs regs → regsT (mk_sem_lin_params p p')
    585585; sigma_empty_regsT_commute :
    586586  ∀ptr.∃ prf.
    587   empty_regsT (make_sem_lin_params p p') ptr =
    588   sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
     587  empty_regsT (mk_sem_lin_params p p') ptr =
     588  sigma_regs (empty_regsT (mk_sem_graph_params p p') ptr) prf
    589589; sigma_load_sp_commute :
    590590  preserving … res_preserve …
     
    593593    sigma_regs
    594594    (λx.λ_.x)
    595     (load_sp (make_sem_graph_params p p'))
    596     (load_sp (make_sem_lin_params p p'))
     595    (load_sp (mk_sem_graph_params p p'))
     596    (load_sp (mk_sem_lin_params p p'))
    597597; sigma_save_sp_commute :
    598598  ∀reg,ptr,prf1. ∃prf2.
    599   save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
    600   sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
     599  save_sp (mk_sem_lin_params p p') (sigma_regs reg prf1) ptr =
     600  sigma_regs (save_sp (mk_sem_graph_params p p') reg ptr) prf2
    601601}.
    602602
     
    605605 ∀sigma.
    606606 good_sem_state_sigma p p' graph_prog sigma →
    607  state (make_sem_graph_params p p') → Prop ≝
     607 state (mk_sem_graph_params p p') → Prop ≝
    608608λp,p',graph_prog,sigma,gsss,st.
    609609well_formed_frames … gsss (st_frms … st) ∧
     
    616616 ∀sigma.
    617617 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    618  ∀st : state (make_sem_graph_params p p').
     618 ∀st : state (mk_sem_graph_params p p').
    619619 well_formed_state … gsss st →
    620  state (make_sem_lin_params p p') ≝
     620 state (mk_sem_lin_params p p') ≝
    621621λp,p',graph_prog,sigma,gsss,st,prf.
    622622mk_state …
     
    694694 ∀p,p',graph_prog,sigma.
    695695  good_sem_state_sigma p p' graph_prog sigma →
    696   state_pc (make_sem_graph_params p p') → Prop ≝
     696  state_pc (mk_sem_graph_params p p') → Prop ≝
    697697 λp,p',prog,sigma,gsss,st.
    698698 well_formed_pc p p' prog sigma (last_pop … st) ∧
     
    707707(*   let lin_prog ≝ linearise ? graph_prog in *)
    708708  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    709     ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     709    ∀s:state_pc (mk_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
    710710     well_formed_state_pc p p' graph_prog sigma gsss s →
    711       state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
     711      state_pc (mk_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
    712712
    713713 λp,p',graph_prog,sigma,gsss,s,prf.
     
    796796    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    797797    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    798 ; allocate_locals__commute :
    799   ∀loc, r1, prf1. ∃ prf2.
    800   allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
    801   sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
    802798; save_frame_commute :
    803799  ∀dest,fl.
     
    12211217    (joint_closed_internal_function
    12221218     (graph_prog_params p p' graph_prog
    1223       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1219      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12241220       (linearise_int_fun p) graph_prog stack_sizes))
    12251221     (globals
    12261222      (graph_prog_params p p' graph_prog
    1227        (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1223       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12281224        (linearise_int_fun p) graph_prog stack_sizes)))))
    12291225   (ev_genv
    12301226    (graph_prog_params p p' graph_prog
    1231      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1227     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12321228      (linearise_int_fun p) graph_prog stack_sizes)))
    1233    (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
     1229   (pblock (pc (mk_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
    12341230 
    12351231
     
    12401236    (joint_closed_internal_function
    12411237     (graph_prog_params p p' graph_prog
    1242       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1238      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12431239       (linearise_int_fun p) graph_prog stack_sizes))
    12441240     (globals
    12451241      (graph_prog_params p p' graph_prog
    1246        (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1242       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12471243        (linearise_int_fun p) graph_prog stack_sizes)))))
    12481244   (ev_genv
    12491245    (graph_prog_params p p' graph_prog
    1250      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     1246     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
    12511247      (linearise_int_fun p) graph_prog stack_sizes)))
    1252    (pblock (pc (make_sem_graph_params p p') st))) in H;
     1248   (pblock (pc (mk_sem_graph_params p p') st))) in H;
    12531249
    12541250
     
    13581354  fetch_internal_function …
    13591355    (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 →
    1360   let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in
     1356  let pc' ≝ pc_of_point (mk_sem_graph_params p p') … bl lbl in
    13611357  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
    1362   ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1358  ∃prf'.pc_of_label (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog)
    13631359    bl lbl =
    13641360        return sigma_pc p p' graph_prog sigma pc' prf'.
     
    14061402  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    14071403 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
    1408  sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
    1409  point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     1404 sigma fn (point_of_pc (mk_sem_graph_params p p') pc) = return n →
     1405 point_of_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) = n.
    14101406#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
    14111407whd in match sigma_pc; normalize nodelta
     
    14311427  ∀sigma.good_sigma p graph_prog sigma →
    14321428  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1433   fetch_statement (make_sem_graph_params p p') …
     1429  fetch_statement (mk_sem_graph_params p p') …
    14341430    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    14351431  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
    1436       (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
    1437       pc_of_label (make_sem_lin_params p p') …
     1432      (pc_of_point (mk_sem_graph_params p p') (pc_block pc) lbl).
     1433      pc_of_label (mk_sem_lin_params p p') …
    14381434          (globalenv_noinit … lin_prog)
    14391435          (pc_block pc)
     
    14441440        match s with
    14451441        [ step_seq x ⇒
    1446           fetch_statement (make_sem_lin_params p p') …
     1442          fetch_statement (mk_sem_lin_params p p') …
    14471443          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14481444              return 〈f, \fst (linearise_int_fun … fn),
    14491445                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
    14501446          ∃prf'.
    1451             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
    1452             let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1447            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
     1448            let nxt_pc ≝ succ_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) it in
    14531449            (nxt_pc = sigma_nxt ∨
    1454               (fetch_statement (make_sem_lin_params p p') …
     1450              (fetch_statement (mk_sem_lin_params p p') …
    14551451                (globalenv_noinit … lin_prog) nxt_pc =
    14561452                return 〈f, \fst (linearise_int_fun … fn),
    14571453                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
    1458               (pc_of_label (make_sem_lin_params p p') …
     1454              (pc_of_label (mk_sem_lin_params p p') …
    14591455                (globalenv_noinit … lin_prog)
    14601456                (pc_block pc)
     
    14621458        | COND a ltrue ⇒
    14631459            ∃prf'.
    1464             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1460            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
    14651461            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
    1466             (fetch_statement (make_sem_lin_params p p') …
     1462            (fetch_statement (mk_sem_lin_params p p') …
    14671463            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14681464              return 〈f, \fst (linearise_int_fun … fn),
    14691465                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
    14701466             nxt_pc = sigma_nxt)) ∨
    1471             (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
     1467            (fetch_statement (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
    14721468             =
    14731469             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
    1474             pc_of_label (make_sem_lin_params p p') …
     1470            pc_of_label (mk_sem_lin_params p p') …
    14751471                (globalenv_noinit … lin_prog)
    14761472                (pc_block pc)
    14771473                nxt = return sigma_nxt)
    14781474         ]
    1479     | final z ⇒   fetch_statement (make_sem_lin_params p p') …
     1475    | final z ⇒   fetch_statement (mk_sem_lin_params p p') …
    14801476                   (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    14811477                   return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉
     
    21802176 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
    21812177 ∀prf : well_formed_state_pc … gss st.
    2182    fetch_statement (make_sem_graph_params p p') …
     2178   fetch_statement (mk_sem_graph_params p p') …
    21832179    (globalenv_noinit ? graph_prog) (pc … st) =
    21842180      return 〈f, fn,  sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 →
     
    22472243   (sigma_state p p' graph_prog sigma gss)
    22482244   (λx.λ_ : True .x)
    2249    (block_of_call (make_sem_graph_params p p') …
     2245   (block_of_call (mk_sem_graph_params p p') …
    22502246      (globalenv_noinit ? graph_prog) cl)   
    2251    (block_of_call (make_sem_lin_params p p') …
     2247   (block_of_call (mk_sem_lin_params p p') …
    22522248      (globalenv_noinit ? (linearise ? graph_prog)) cl).
    22532249#p #p' #graph_prog #sigma #gss #cl #st #prf
     
    22952291∃prf.
    22962292sigma_pc p p' graph_prog sigma
    2297    (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
    2298       pc_of_point (make_sem_lin_params p p') bl 0.
     2293   (pc_of_point (mk_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
     2294      pc_of_point (mk_sem_lin_params p p') bl 0.
    22992295#p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec
    23002296cases (good fn1) * #entry_in #_ #_
     
    23182314 ∀st,st',f,fn,called,args,dest,nxt.
    23192315 ∀prf : well_formed_state_pc … gss st.
    2320   fetch_statement (make_sem_graph_params p p') …
     2316  fetch_statement (mk_sem_graph_params p p') …
    23212317    (globalenv_noinit ? graph_prog) (pc … st) =
    23222318      return 〈f, fn,
     
    23252321    return st' →
    23262322(* let st_pc' ≝ mk_state_pc ? st'
    2327   (succ_pc (make_sem_graph_params p p') …
     2323  (succ_pc (mk_sem_graph_params p p') …
    23282324    (pc … st) nxt) in
    23292325 ∀prf'.
    2330  fetch_statement (make_sem_lin_params p p') …
     2326 fetch_statement (mk_sem_lin_params p p') …
    23312327   (globalenv_noinit … lin_prog)
    2332      (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
     2328     (succ_pc (mk_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
    23332329   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
    2334  pc_of_label (make_sem_lin_params p p') ?
     2330 pc_of_label (mk_sem_lin_params p p') ?
    23352331                (globalenv_noinit ? (linearise p … graph_prog))
    23362332                (pc_block (pc … st))
    23372333                nxt = return sigma_pc p p' graph_prog sigma
    2338     (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*)
     2334    (succ_pc (mk_sem_graph_params p p') (pc … st) nxt) prf' →*)
    23392335  let st2_pre_call ≝ sigma_state_pc … gss st prf in
    23402336  ∃is_call, is_call'.
     
    24322428 ∀st,st',f,fn,nxt.
    24332429 ∀prf : well_formed_state_pc … gss st.
    2434    fetch_statement (make_sem_graph_params p p') …
     2430   fetch_statement (mk_sem_graph_params p p') …
    24352431    (globalenv_noinit ? graph_prog) (pc … st) =
    24362432      return 〈f, fn,  final … (GOTO (mk_graph_params p) … nxt)〉 →
     
    24802476∀st,st',f,fn,a,ltrue,lfalse.
    24812477∀prf : well_formed_state_pc … gss st.
    2482  fetch_statement (make_sem_graph_params p p') …
     2478 fetch_statement (mk_sem_graph_params p p') …
    24832479  (globalenv_noinit ? graph_prog) (pc … st) =
    24842480    return 〈f, fn,  sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 →
     
    25512547∀st,st',f,fn.
    25522548∀prf : well_formed_state_pc … gss st.
    2553  fetch_statement (make_sem_graph_params p p') …
     2549 fetch_statement (mk_sem_graph_params p p') …
    25542550  (globalenv_noinit ? graph_prog) (pc … st) =
    25552551    return 〈f, fn,  final … (RETURN (mk_graph_params p) … )〉 →
     
    26592655∀st,st',f,fn,fl,called,args.
    26602656∀prf : well_formed_state_pc … gss st.
    2661  fetch_statement (make_sem_graph_params p p') …
     2657 fetch_statement (mk_sem_graph_params p p') …
    26622658  (globalenv_noinit ? graph_prog) (pc … st) =
    26632659    return 〈f, fn,  final … (TAILCALL (mk_graph_params p) … fl called args)〉 →
     
    27332729qed.
    27342730   
    2735    
    2736    
    2737 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    2738     ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
    2739 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
    27402731
    27412732lemma linearise_ok:
     
    27442735 ∀stack_sizes.
    27452736 (∀sigma.good_state_sigma p p' graph_prog sigma) →
    2746    ex_Type1 … (λR.
     2737   ∃[1] R.
    27472738   status_simulation
    27482739    (graph_abstract_status p p' graph_prog stack_sizes)
     
    27682759whd in ⊢ (%→?);
    27692760change with
    2770   (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
     2761  (eval_state (mk_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
    27712762#EQeval
    27722763@('bind_inversion EQeval)
Note: See TracChangeset for help on using the changeset viewer.