Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (8 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1976 r2155  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
    9 include "basics/deqsets.ma".
    10 include "basics/finset.ma". (* for DeqNat *)
     9include "common/StructuredTraces.ma".
    1110
    1211(* Here is the structure of parameter records (downward edges are coercions,
     
    3736params : adds type of code and related properties *)
    3837
     38inductive possible_flows : Type[0] ≝
     39| Labels : list label → possible_flows
     40| Call : possible_flows.
     41
    3942record step_params : Type[1] ≝
    4043 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
     
    5053 ; call_args: Type[0] (* arguments of function calls *)
    5154 ; call_dest: Type[0] (* possible destination of function computation *)
    52  ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
    53  ; ext_step_labels : ext_step → list label
    54  ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
    55  ; ext_fin_stmt_labels : ext_fin_stmt → list label
     55 (* other instructions not fitting in the general framework *)
     56 ; ext_seq : Type[0]
     57(* ; ext_branch : Type[0]
     58 ; ext_branch_labels : ext_branch → list label*)
     59 ; ext_call : Type[0]
     60 ; ext_tailcall : Type[0]
     61 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    5662 }.
    57  
    58 inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
    59   | COMMENT: String → joint_step p globals
    60   | COST_LABEL: costlabel → joint_step p globals
    61   | MOVE: pair_move p → joint_step p globals
    62   | POP: acc_a_reg p → joint_step p globals
    63   | PUSH: acc_a_arg p → joint_step p globals
    64   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
    65   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
    66   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
    67   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
     63
     64inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
     65  | COMMENT: String → joint_seq p globals
     66  | COST_LABEL: costlabel → joint_seq p globals
     67  | MOVE: pair_move p → joint_seq p globals
     68  | POP: acc_a_reg p → joint_seq p globals
     69  | PUSH: acc_a_arg p → joint_seq p globals
     70  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     71  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
     72  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     73  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
    6874  (* int done with generic move *)
    69 (*| INT: generic_reg p → Byte → joint_step p globals *)
    70   | CLEAR_CARRY: joint_step p globals
    71   | SET_CARRY: joint_step p globals
    72   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
    73   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
    74   | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
    75   | COND: acc_a_reg p → label → joint_step p globals
    76   | extension: ext_step p → joint_step p globals.
     75(*| INT: generic_reg p → Byte → joint_seq p globals *)
     76  | CLEAR_CARRY: joint_seq p globals
     77  | SET_CARRY: joint_seq p globals
     78  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
     79  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
     80  | extension_seq : ext_seq p → joint_seq p globals.
    7781
    7882axiom EmptyString : String.
     
    9296interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9397
    94 coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
    95   extension on _s : ext_step ? to joint_step ??.
     98coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     99  extension_seq on _s : ext_seq ? to joint_seq ??.
     100
     101inductive joint_call (p : step_params) : Type[0] ≝
     102  | CALL_ID: ident → call_args p → call_dest p → joint_call p
     103  | extension_call : ext_call p → joint_call p.
     104
     105coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
     106  extension_call on _s : ext_call ? to joint_call ?.
     107 
     108inductive joint_branch (p : step_params) : Type[0] ≝
     109  | COND: acc_a_reg p → label → joint_branch p
     110  (*| extension_branch : ext_branch p → joint_branch p*).
     111
     112(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     113  extension_branch on _s : ext_branch ? to joint_branch ?.*)
     114
     115inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
     116  | step_seq : joint_seq p globals → joint_step p globals
     117  | step_call : joint_call p → joint_step p globals
     118  | step_branch : joint_branch p → joint_step p globals.
     119
     120coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     121  step_seq on _s : joint_seq ?? to joint_step ??.
     122coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
     123  step_call on _s : joint_call ? to joint_step ??.
     124coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
     125  step_branch on _s : joint_branch ? to joint_step ??.
     126
     127definition step_flows ≝ λp,globals.λs : joint_step p globals.
     128  match s with
     129  [ step_seq _ ⇒ Labels … [ ]
     130  | step_call _ ⇒ Call
     131  | step_branch s ⇒
     132    match s with
     133    [ COND _ l ⇒ Labels … [l]
     134    (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
     135    ]
     136  ].
    96137
    97138definition step_labels ≝
    98139  λp, globals.λs : joint_step p globals.
    99     match s with
    100     [ COND _ l ⇒ [l]
    101     | extension ext_s ⇒ ext_step_labels ? ext_s
    102     | _ ⇒ [ ]
     140    match step_flows … s with
     141    [ Labels lbls ⇒ lbls
     142    | Call ⇒ [ ]
    103143    ].
    104144
     
    106146    (label → Prop) → joint_step p globals → Prop ≝
    107147λp,g,P,inst. All … P (step_labels … inst).
    108  
     148
     149definition step_classifier :
     150  ∀p : step_params.∀globals.
     151    joint_step p globals → status_class ≝ λp,g,s.
     152  match s with
     153  [ step_seq _ ⇒ cl_other
     154  | step_call _ ⇒ cl_call
     155  | step_branch _ ⇒ cl_jump
     156  ].
     157
    109158record funct_params : Type[1] ≝
    110159  { resultT : Type[0]
     
    117166 }.
    118167
    119 
    120168record unserialized_params : Type[1] ≝
    121169 { u_inst_pars :> step_params
     
    129177  }.
    130178
    131 inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
    132   | GOTO: label → joint_fin_step p globals
    133   | RETURN: joint_fin_step p globals
    134   | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
     179inductive joint_fin_step (p: step_params): Type[0] ≝
     180  | GOTO: label → joint_fin_step p
     181  | RETURN: joint_fin_step p
     182  | tailcall : ext_tailcall p → joint_fin_step p.
     183
     184definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     185  match s with
     186  [ GOTO l ⇒ Labels … [l]
     187  | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
     188  ].
     189
     190definition fin_step_labels ≝
     191  λp.λs : joint_fin_step p.
     192    match fin_step_flows … s with
     193    [ Labels lbls ⇒ lbls
     194    | Call ⇒ [ ]
     195    ].
     196
     197definition fin_step_classifier :
     198  ∀p : stmt_params.
     199    joint_fin_step p → status_class
     200  ≝ λp,s.
     201  match s with
     202  [ GOTO _ ⇒ cl_other
     203  | _ ⇒ cl_return
     204  ].
    135205
    136206inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    137207  | sequential: joint_step p globals → succ p → joint_statement p globals
    138   | final: joint_fin_step p globals → joint_statement p globals.
    139 
    140 coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
    141   ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
    142   extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
     208  | final: joint_fin_step p → joint_statement p globals.
     209
     210definition stmt_classifier :
     211  ∀p : stmt_params.∀globals.
     212    joint_statement p globals → status_class
     213  ≝ λp,g,s.
     214  match s with
     215  [ sequential stp _ ⇒ step_classifier p g stp
     216  | final stp ⇒ fin_step_classifier p stp
     217  ].
     218
     219coercion extension_fin_to_fin_step : ∀p : stmt_params.
     220  ∀s : ext_tailcall p.joint_fin_step p ≝
     221  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
    143222
    144223coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
    145   ∀s : joint_fin_step p globals.joint_statement p globals ≝
    146   final on _s : joint_fin_step ?? to joint_statement ??.
     224  ∀s : joint_fin_step p.joint_statement p globals ≝
     225  final on _s : joint_fin_step ? to joint_statement ??.
    147226
    148227record params : Type[1] ≝
    149228 { stmt_pars :> stmt_params
    150229 ; codeT: list ident → Type[0]
    151  ; code_point : DeqSet
     230 ; code_point : Type[0]
    152231 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    153232 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    192271  [ Some pt ⇒ code_has_point … c pt
    193272  | None ⇒ false
    194   ].
    195 
    196 definition fin_step_labels ≝
    197   λp,globals.λs : joint_fin_step p globals.
    198   match s with
    199   [ GOTO l ⇒ [ l ]
    200   | RETURN ⇒ [ ]
    201   | extension_fin c ⇒ ext_fin_stmt_labels … c
    202273  ].
    203274
     
    254325
    255326record lin_params : Type[1] ≝
    256   { l_u_pars :> unserialized_params }.
     327  { l_u_pars : unserialized_params }.
    257328 
    258329lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     
    290361  λlp : lin_params.
    291362     mk_params
    292       (mk_stmt_params lp unit (λ_.None ?))
     363      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
    293364    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    294     (* code_point ≝ *)DeqNat
     365    (* code_point ≝ *)
    295366    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    296367    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325396
    326397record graph_params : Type[1] ≝
    327   { g_u_pars :> unserialized_params }.
     398  { g_u_pars : unserialized_params }.
    328399
    329400(* One common instantiation of params via Graphs of joint_statements
     
    332403  λgp : graph_params.
    333404     mk_params
    334       (mk_stmt_params gp label (Some ?))
     405      (mk_stmt_params (g_u_pars gp) label (Some ?))
    335406    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    336     (* code_point ≝ *)(Deq_identifier LabelTag)
     407    (* code_point ≝ *)label
    337408    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    338409    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
Note: See TracChangeset for help on using the changeset viewer.