Changeset 1182


Ignore:
Timestamp:
Sep 5, 2011, 1:23:20 PM (8 years ago)
Author:
mulligan
Message:

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1176 r1182  
    66
    77record params: Type[1] ≝
    8  { next: Type[0]
     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];
    915 
    10  ; acc_a_reg: Type[0]
    11  ; acc_b_reg: Type[0]
    12  ; dpl_reg: Type[0]
    13  ; dph_reg: Type[0]
    14  ; pair_reg: Type[0]
    15  ; generic_reg: Type[0]
     16  extend_statements: Type[0];
    1617 
    17  ; extend_statements: Type[0]
    18  
    19  ; resultT: Type[0]
    20  ; localsT: Type[0]
    21  ; paramsT: Type[0]
    22  }.
     18  resultT: Type[0];
     19  localsT: Type[0];
     20  paramsT: Type[0]
     21}.
    2322
    2423inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     
    3837  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    3938  | joint_instr_call_id: ident → nat → joint_instruction p globals
    40   | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
     39  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    4140
    4241inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    43   | joint_st_sequential: joint_instruction p globals → next p → joint_statement p globals
    44   | joint_st_goto: next p → joint_statement p globals
     42  | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
     43  | joint_st_goto: label → joint_statement p globals
    4544  | joint_st_return: joint_statement p globals
    4645  | joint_st_extension: extend_statements p → joint_statement p globals.
     
    4847record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    4948 { pmemoryT: Type[0]
    50  ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
     49 ; lookup: pmemoryT → label → option (joint_statement preparams globals)
    5150 }.
    5251
     
    6059  joint_if_stacksize: nat;
    6160  joint_if_graph    : pmemoryT … p;
    62   joint_if_entry    : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;
    63   joint_if_exit     : Σl: next pre. lookup … p joint_if_graph l ≠ None ?
     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 ?
    6463}.
    6564
  • src/joint/semantics.ma

    r1177 r1182  
    3737*)
    3838(* CSC: ??? *)
    39 axiom address_of_label: ∀p. mem → next p → address.
    40 axiom address_chunks_of_label: ∀p. mem → next p → Byte × Byte.
     39axiom address_of_label: mem → label → address.
     40axiom address_chunks_of_label: mem → label → Byte × Byte.
    4141axiom label_of_address_chunks: Byte → Byte → label.
    4242axiom address_of_address_chunks: Byte → Byte → address.
     
    106106
    107107(* CSC: was build_state in RTL *)
    108 definition goto: ∀p:sem_params. next p → state p → state p ≝
     108definition goto: ∀p:sem_params. label → state p → state p ≝
    109109 λp,l,st. set_pc … (address_of_label … (m … st) l) st.
    110110
     
    188188   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    189189
    190 definition save_ra : ∀p. state p → next p → res (state p) ≝
     190definition save_ra : ∀p. state p → label → res (state p) ≝
    191191 λp,st,l.
    192192  let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
Note: See TracChangeset for help on using the changeset viewer.