Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/joint/Joint.ma

    r1182 r1311  
    33include "common/AST.ma".
    44include "common/Registers.ma".
     5include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
    56include "common/Graphs.ma".
    67
    7 record params: Type[1] ≝
    8 {
    9   acc_a_reg: Type[0];
    10   acc_b_reg: Type[0];
    11   dpl_reg: Type[0];
    12   dph_reg: Type[0];
    13   pair_reg: Type[0];
    14   generic_reg: Type[0];
     8record params__: Type[1] ≝
     9 { acc_a_reg: Type[0]
     10 ; acc_b_reg: Type[0]
     11 ; dpl_reg: Type[0]
     12 ; dph_reg: Type[0]
     13 ; pair_reg: Type[0]
     14 ; generic_reg: Type[0]
     15 ; call_args: Type[0]
     16 ; call_dest: Type[0]
    1517 
    16   extend_statements: Type[0];
    17  
    18   resultT: Type[0];
    19   localsT: Type[0];
    20   paramsT: Type[0]
    21 }.
    22 
    23 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
    24   | joint_instr_comment: String → joint_instruction p globals
    25   | joint_instr_cost_label: costlabel → joint_instruction p globals
    26   | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
    27   | joint_instr_move: pair_reg p → joint_instruction p globals
    28   | joint_instr_pop: acc_a_reg p → joint_instruction p globals
    29   | joint_instr_push: acc_a_reg p → joint_instruction p globals
    30   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    31   | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    32   | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
    33   | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
    34   | joint_instr_clear_carry: joint_instruction p globals
    35   | joint_instr_set_carry: joint_instruction p globals
    36   | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    37   | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    38   | joint_instr_call_id: ident → nat → joint_instruction p globals
    39   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    40 
    41 inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    42   | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
    43   | joint_st_goto: label → joint_statement p globals
    44   | joint_st_return: joint_statement p globals
    45   | joint_st_extension: extend_statements p → joint_statement p globals.
    46 
    47 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    48  { pmemoryT: Type[0]
    49  ; lookup: pmemoryT → label → option (joint_statement preparams globals)
     18 ; extend_statements: Type[0]
    5019 }.
    5120
    52 record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     21record params_: Type[1] ≝
     22 { pars__:> params__
     23 ; succ: Type[0]
     24 }.
     25
     26(* One common instantiation of params via Graphs of joint_statements
     27   (all languages but LIN) *)
     28definition graph_params_ : params__ → params_ ≝
     29 λpars__. mk_params_ pars__ label.
     30
     31inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
     32  | COMMENT: String → joint_instruction p globals
     33  | COST_LABEL: costlabel → joint_instruction p globals
     34  | INT: generic_reg p → Byte → joint_instruction p globals
     35  | MOVE: pair_reg p → joint_instruction p globals
     36  | POP: acc_a_reg p → joint_instruction p globals
     37  | PUSH: acc_a_reg p → joint_instruction p globals
     38  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
     39  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
     40  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     41  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
     42  | CLEAR_CARRY: joint_instruction p globals
     43  | SET_CARRY: joint_instruction p globals
     44  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
     45  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
     46  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
     47  | COND: acc_a_reg p → label → joint_instruction p globals
     48  | extension: extend_statements p → joint_instruction p globals.
     49
     50inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
     51  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     52  | GOTO: label → joint_statement p globals
     53  | RETURN: joint_statement p globals.
     54
     55record params0: Type[1] ≝
     56 { pars__' :> params__
     57 ; resultT: Type[0]
     58 ; paramsT: Type[0]
     59 }.
     60
     61record params1 : Type[1] ≝
     62 { pars0 :> params0
     63 ; localsT: Type[0]
     64 }.
     65
     66record params (globals: list ident): Type[1] ≝
     67 { succ_ : Type[0]
     68 ; pars1 :> params1
     69 ; codeT: Type[0]
     70 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
     71 }.
     72 
     73definition params__of_params: ∀globals. params globals → params_ ≝
     74 λglobals,pars. mk_params_ pars (succ_ … pars).
     75coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
     76 on _p: params ? to params_.
     77
     78include alias "common/Graphs.ma". (* To pick the right lookup *)
     79
     80(* One common instantiation of params via Graphs of joint_statements
     81   (all languages but LIN) *)
     82definition graph_params: params1 → ∀globals: list ident. params globals ≝
     83 λpars1,globals.
     84  mk_params globals label pars1
     85   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
     86
     87
     88(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
     89definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
     90definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
     91
     92record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
    5393{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5494  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
    5595(*  joint_if_sig: signature;  -- dropped in front end *)
    56   joint_if_result   : resultT pre;
    57   joint_if_params   : paramsT pre;
    58   joint_if_locals   : localsT pre;
     96  joint_if_result   : resultT p;
     97  joint_if_params   : paramsT p;
     98  joint_if_locals   : localsT p;
     99(*CSC: XXXXX stacksize unused for LTL-...*)
    59100  joint_if_stacksize: nat;
    60   joint_if_graph    : pmemoryT … p;
    61   joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
    62   joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
     101  joint_if_code     : codeT … p;
     102(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
     103  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
     104(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
     105  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
    63106}.
    64107
    65 definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     108(* Currified form *)
     109definition set_joint_if_exit ≝
     110  λglobals,pars.
     111  λexit: label.
     112  λp:joint_internal_function globals pars.
     113  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
     114   mk_joint_internal_function globals pars
     115    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     116    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     117    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    66118
    67 record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
    68 {
    69   joint_pr_vars: list (ident × nat);
    70   joint_pr_functs: list (ident × (joint_function … p));
    71   joint_pr_main: option ident
    72 }.
     119definition set_joint_if_graph ≝
     120  λglobals,pars.
     121  λgraph.
     122  λp:joint_internal_function globals pars.
     123  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
     124  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
     125   mk_joint_internal_function globals pars
     126    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     127    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     128    graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     129
     130definition set_luniverse ≝
     131  λglobals,pars.
     132  λp : joint_internal_function globals pars.
     133  λluniverse: universe LabelTag.
     134   mk_joint_internal_function globals pars
     135    luniverse (joint_if_runiverse … p) (joint_if_result … p)
     136    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     137    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     138
     139definition set_runiverse ≝
     140  λglobals,pars.
     141  λp : joint_internal_function globals pars.
     142  λruniverse: universe RegisterTag.
     143   mk_joint_internal_function globals pars
     144    (joint_if_luniverse … p) runiverse (joint_if_result … p)
     145    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     146    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     147
     148(* Specialized for graph_params *)
     149definition add_graph ≝
     150  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
     151   let code ≝ add … (joint_if_code ?? p) l stmt in
     152    mk_joint_internal_function … (graph_params … globals)
     153     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     154     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     155     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
     156  normalize nodelta;
     157  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
     158  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
     159qed.
     160
     161definition set_locals ≝
     162  λglobals,pars.
     163  λp : joint_internal_function globals pars.
     164  λlocals.
     165   mk_joint_internal_function globals pars
     166    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     167    (joint_if_params … p) locals (joint_if_stacksize … p)
     168    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     169
     170definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
     171
     172definition joint_program ≝
     173 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
    73174
    74175(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.