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:
3 edited
3 copied

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(****************************************************************************)
  • Deliverables/D3.3/id-lookup-branch/joint/semantics.ma

    r1186 r1311  
    44include "common/SmallstepExec.ma".
    55include "joint/Joint.ma".
    6 (*
     6include "joint/BEMem.ma".
     7
    78(* CSC: external functions never fail (??) and always return something of the
    89   size of one register, both in the frontend and in the backend.
     
    1011   only the head is kept (or Undef if the list is empty) ??? *)
    1112
    12 (* CSC: carries are values and booleans are not values; so we use integers.
    13    But why using values at all? To have undef? *)
    14 (* CSC: ???????????? *)
    15 *)
    16 axiom smerge: val → val → res val.
    17 (* CSC: ???????????? In OCaml: IntValue.Int32.merge
    18    Note also that the translation can fail; so it should be a res int! *)
    19 axiom smerge2: list val → int.
    20 (* CSC: I have a byte, I need a value, but it is complex to do so *)
    21 axiom val_of_Byte: Byte → val.
    22 axiom Byte_of_val: val → res Byte.
    23 (*
    24 axiom val_of_nat: nat → val.
    25 (* Map from the front-end memory model to the back-end memory model *)
    26 *)
    27 axiom represent_block: block → val × val.
    28 (* CSC: fixed size chunk *)
    29 axiom chunk: memory_chunk.
    30 axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
    31 axiom address: Type[0].
    32 axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    33 axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    34 (* CSC: ??? *)
    35 axiom address_of_label: mem → label → address.
    36 axiom address_chunks_of_label: mem → label → Byte × Byte.
    37 axiom label_of_address_chunks: Byte → Byte → label.
    38 axiom address_of_address_chunks: Byte → Byte → address.
    39 
    40 record sem_params: Type[1] ≝
    41  { p:> params
    42  ; framesT: Type[0]
    43  ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
    44  
     13definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)
     14
     15definition eq_address: address → address → bool ≝
     16 λaddr1,addr2.
     17  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
     18
     19record more_sem_params (p:params_): Type[1] ≝
     20 { framesT: Type[0]
     21 ; regsT: Type[0]
     22
     23 ; succ_pc: succ p → address → address
    4524 ; pop_frame_: framesT → res framesT
    4625 ; save_frame_: framesT → regsT → framesT
    47  ; greg_store_: generic_reg p → val → regsT → res regsT
    48  ; greg_retrieve_: regsT → generic_reg p → res val
    49  ; acca_store_: acc_a_reg p → val → regsT → res regsT
    50  ; acca_retrieve_: regsT → acc_a_reg p → res val
    51  ; accb_store_: acc_b_reg p → val → regsT → res regsT
    52  ; accb_retrieve_: regsT → acc_b_reg p → res val
    53  ; dpl_store_: dpl_reg p → val → regsT → res regsT
    54  ; dpl_retrieve_: regsT → dpl_reg p → res val
    55  ; dph_store_: dph_reg p → val → regsT → res regsT
    56  ; dph_retrieve_: regsT → dph_reg p → res val
     26 ; greg_store_: generic_reg p → beval → regsT → res regsT
     27 ; greg_retrieve_: regsT → generic_reg p → res beval
     28 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
     29 ; acca_retrieve_: regsT → acc_a_reg p → res beval
     30 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
     31 ; accb_retrieve_: regsT → acc_b_reg p → res beval
     32 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
     33 ; dpl_retrieve_: regsT → dpl_reg p → res beval
     34 ; dph_store_: dph_reg p → beval → regsT → res regsT
     35 ; dph_retrieve_: regsT → dph_reg p → res beval
    5736 ; pair_reg_move_: regsT → pair_reg p → regsT
    5837 
    59  ; init_locals : localsT p → regsT
     38 ; pointer_of_label: label → Σp:pointer. ptype p = Code
     39 }.
     40
     41record sem_params: Type[1] ≝
     42 { spp :> params_
     43 ; more_sem_pars :> more_sem_params spp
    6044 }.
    6145
    6246record state (p: sem_params): Type[0] ≝
    63  { st_frms: framesT p
     47 { st_frms: framesT ? p
    6448 ; pc: address
    65  ; sp: address
    66  ; carry: val
    67  ; regs: regsT p
    68  ; m: mem
    69  }.
    70 
    71 definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
     49 ; sp: pointer
     50 ; carry: beval
     51 ; regs: regsT ? p
     52 ; m: bemem
     53 }.
     54
     55definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
     56
     57record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
     58 { more_sparams:> more_sem_params p
     59
     60 ; init_locals : localsT p → regsT … more_sparams
     61 
     62 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     63 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
     64 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     65 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
     66
     67 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     68 }.
    7269
    7370record sem_params2 (globals: list ident): Type[1] ≝
    74  { sparams:> sem_params
    75  ; pre_sem_params:> sem_params_ sparams globals
    76  
    77  ; fetch_statement: state sparams → res (joint_statement sparams globals)
    78  ; fetch_external_args: external_function → state sparams → res (list val)
    79  ; set_result: list val → state sparams → res (state sparams)
    80  ; fetch_result: state sparams → nat → res (list val)
    81 
    82  ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
    83  }.
    84 
    85 definition set_m: ∀p. mem → state p → state p ≝
     71 { p2:> params globals
     72 ; more_sparams2:> more_sem_params2 globals p2
     73 }.
     74
     75definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
     76coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
     77 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
     78(*
     79unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
     80   S ≟ sem_params_of_sem_params2 globals p
     81(* ---------------------------------------- *) ⊢
     82   pars_ (spp (mk_sem_params (p2 globals p)
     83    (more_sparams (p2 globals p) globals
     84    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
     85*)
     86definition address_of_label: sem_params → label → address.
     87 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
     88 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
     89  [ #res #_ @res
     90  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
     91qed.
     92
     93definition set_m: ∀p. bemem → state p → state p ≝
    8694 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
    8795
    88 definition set_regs: ∀p. regsT p → state p → state p ≝
     96definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    8997 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
    9098
    91 definition set_sp: ∀p. address → state p → state p ≝
     99definition set_sp: ∀p. pointer → state p → state p ≝
    92100 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
    93101
    94 definition set_carry: ∀p. val → state p → state p ≝
     102definition set_carry: ∀p. beval → state p → state p ≝
    95103 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
    96104
     
    98106 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
    99107
    100 definition set_frms: ∀p. framesT p → state p → state p ≝
     108definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    101109 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
    102110
    103 (* CSC: was build_state in RTL *)
    104111definition goto: ∀p:sem_params. label → state p → state p ≝
    105  λp,l,st. set_pc … (address_of_label … (m … st) l) st.
    106 
    107 definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
    108  λp,dst,v,st.
    109   (*CSC: monadic notation missing here *)
    110   bind ?? (greg_store_ … dst v (regs … st)) (λregs.
    111   OK ? (set_regs … regs st)).
    112 
    113 definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res val ≝
     112 λp,l,st. set_pc … (address_of_label p l) st.
     113
     114definition next: ∀p:sem_params. succ … p → state p → state p ≝
     115 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
     116
     117definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
     118 λp,dst,v,st.
     119  do regs  ← greg_store_ … dst v (regs … st);
     120  OK ? (set_regs … regs st).
     121
     122definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
    114123 λp,st,dst.greg_retrieve_ … (regs … st) dst.
    115124
    116 definition acca_store: ∀p:sem_params. acc_a_reg p → val → state p → res (state p) ≝
    117  λp,dst,v,st.
    118   (*CSC: monadic notation missing here *)
    119   bind ?? (acca_store_ … dst v (regs … st)) (λregs.
    120   OK ? (set_regs … regs st)).
    121 
    122 definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res val ≝
     125definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
     126 λp,dst,v,st.
     127  do regs ← acca_store_ … dst v (regs … st);
     128  OK ? (set_regs … regs st).
     129
     130definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
    123131 λp,st,dst.acca_retrieve_ … (regs … st) dst.
    124132
    125 definition accb_store: ∀p:sem_params. acc_b_reg p → val → state p → res (state p) ≝
    126  λp,dst,v,st.
    127   (*CSC: monadic notation missing here *)
    128   bind ?? (accb_store_ … dst v (regs … st)) (λregs.
    129   OK ? (set_regs … regs st)).
    130 
    131 definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res val ≝
     133definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
     134 λp,dst,v,st.
     135  do regs ← accb_store_ … dst v (regs … st);
     136  OK ? (set_regs … regs st).
     137
     138definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
    132139 λp,st,dst.accb_retrieve_ … (regs … st) dst.
    133140
    134 definition dpl_store: ∀p:sem_params. dpl_reg p → val → state p → res (state p) ≝
    135  λp,dst,v,st.
    136   (*CSC: monadic notation missing here *)
    137   bind ?? (dpl_store_ … dst v (regs … st)) (λregs.
    138   OK ? (set_regs … regs st)).
    139 
    140 definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res val ≝
     141definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
     142 λp,dst,v,st.
     143  do regs ← dpl_store_ … dst v (regs … st);
     144  OK ? (set_regs … regs st).
     145
     146definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
    141147 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
    142148
    143 definition dph_store: ∀p:sem_params. dph_reg p → val → state p → res (state p) ≝
    144  λp,dst,v,st.
    145   (*CSC: monadic notation missing here *)
    146   bind ?? (dph_store_ … dst v (regs … st)) (λregs.
    147   OK ? (set_regs … regs st)).
    148 
    149 definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res val ≝
     149definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
     150 λp,dst,v,st.
     151  do regs ← dph_store_ … dst v (regs … st);
     152  OK ? (set_regs … regs st).
     153
     154definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
    150155 λp,st,dst.dph_retrieve_ … (regs … st) dst.
    151156
     
    154159
    155160definition save_frame: ∀p:sem_params. state p → state p ≝
    156  λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
     161 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
    157162
    158163(* removes the top frame from the frames list *)
    159164definition pop_frame: ∀p. state p → res (state p) ≝
    160  (* CSC: monadic notation missing here *)
    161165 λp,st.
    162   bind ?? (pop_frame_ p (st_frms … st)) (λframes.
    163   OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st))).
     166  do frames ← pop_frame_ … p (st_frms … st);
     167  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
    164168
    165169axiom FailedStore: String.
    166170
    167 definition push: ∀p. state p → Byte → res (state p) ≝
     171definition push: ∀p. state p → beval → res (state p) ≝
    168172 λp,st,v.
    169   let sp ≝ val_of_address (sp … st) in
    170   (*CSC: no monadic notation here *)
    171   bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m … st) sp (val_of_Byte v)))
    172    (λm.
    173     let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    174     OK ? (set_m ? m (set_sp … sp st))).
    175 
    176 definition pop: ∀p. state p → res (state p × Byte) ≝
     173  let sp ≝ sp … st in
     174  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
     175  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
     176  OK … (set_m … m (set_sp … sp st)).
     177
     178definition pop: ∀p. state p → res (state p × beval) ≝
    177179 λp,st.
    178   let sp ≝ val_of_address (sp … st) in
    179   let sp ≝ sub sp (val_of_memory_chunk chunk) in
    180   let st ≝ set_sp … (address_of_val sp) st in
    181   (*CSC: no monadic notation here *)
    182   bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))
    183    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    184 
    185 definition save_ra : ∀p. state p → label → res (state p) ≝
     180  let sp ≝ sp ? st in
     181  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
     182  let st ≝ set_sp … sp st in
     183  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
     184  OK ? 〈st,v〉.
     185
     186definition save_ra : ∀p. state p → succ p → res (state p) ≝
    186187 λp,st,l.
    187   let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
    188   (* No monadic notation here *)
    189   bind ?? (push … st addrl) (λst.push … st addrh).
    190 
    191 definition fetch_ra : ∀p.state p → res (state p × label) ≝
     188  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
     189  do st ← push … st addrl;
     190  push … st addrh.
     191
     192definition fetch_ra : ∀p.state p → res (state p × address) ≝
    192193 λp,st.
    193   (* No monadic notation here *)
    194   bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in
    195   bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in
    196    OK ? 〈st, label_of_address_chunks addrl addrh〉)).
     194  do 〈st,addrh〉 ← pop … st;
     195  do 〈st,addrl〉 ← pop … st;
     196  OK ? 〈st, 〈addrl,addrh〉〉.
    197197
    198198axiom MissingSymbol : String.
     
    200200axiom BadFunction : String.
    201201
    202 (*CSC: move elsewhere *)
    203 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    204  λA,P,c. match c with [ dp w _ ⇒ w ].
    205 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    206 
    207 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
    208   λglobals,p. λge,st.
    209   ! s ← fetch_statement globals p st;
     202definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
     203 λglobals,p,ge,st.
     204  ! s ← fetch_statement … st;
    210205  match s with
    211     [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
    212     | joint_st_sequential seq l ⇒
     206    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     207    | sequential seq l ⇒
    213208      match seq with
    214       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto … l st〉
    215       | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
    216       | joint_instr_int dest v ⇒
    217         ! st ← greg_store … dest (val_of_Byte v) st;
    218           ret ? 〈E0, goto … l st〉
    219       | joint_instr_load dst addrl addrh ⇒
     209      [ extension c ⇒ exec_extended … p ge c st
     210      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
     211      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
     212      | INT dest v ⇒
     213        ! st ← greg_store p dest (BVByte v) st;
     214          ret ? 〈E0, next … l st〉
     215      | LOAD dst addrl addrh ⇒
    220216        ! vaddrh ← dph_retrieve … st addrh;
    221217        ! vaddrl ← dpl_retrieve … st addrl;
    222         ! vaddr ← smerge vaddrl vaddrh;
    223         ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m … st) vaddr);
    224         ! st ← acca_store … dst v st;
    225           ret ? 〈E0, goto … l st〉
    226       | joint_instr_store addrl addrh src ⇒
     218        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
     219        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     220        ! st ← acca_store p … dst v st;
     221          ret ? 〈E0, next … l st〉
     222      | STORE addrl addrh src ⇒
    227223        ! vaddrh ← dph_retrieve … st addrh;
    228224        ! vaddrl ← dpl_retrieve … st addrl;
    229         ! vaddr ← smerge vaddrl vaddrh;
     225        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
    230226        ! v ← acca_retrieve … st src;
    231         ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m … st) vaddr v);
    232           ret ? 〈E0, goto … l (set_m … m' st)〉
    233       | joint_instr_cond src ltrue ⇒
     227        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     228          ret ? 〈E0, next … l (set_m … m' st)〉
     229      | COND src ltrue ⇒
    234230        ! v ← acca_retrieve … st src;
    235         ! b ← eval_bool_of_val v;
    236           ret ? 〈E0, goto … (if b then ltrue else l) st〉
    237       | joint_instr_address ident prf ldest hdest ⇒
     231        ! b ← bool_of_beval v;
     232          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
     233      | ADDRESS ident prf ldest hdest ⇒
    238234        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
    239           let 〈laddr,haddr〉 ≝ represent_block addr in
    240         ! st ← dpl_store ldest laddr st;
    241         ! st ← dph_store hdest haddr st;
    242           ret ? 〈E0, goto … l st〉
    243       | joint_instr_op1 op acc_a ⇒
    244         ! v ← acca_retrieve … st acc_a;
     235        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
     236        ! st ← dpl_store p ldest laddr st;
     237        ! st ← dph_store p hdest haddr st;
     238          ret ? 〈E0, next … l st〉
     239      | OP1 op dacc_a sacc_a ⇒
     240        ! v ← acca_retrieve … st sacc_a;
    245241        ! v ← Byte_of_val v;
    246           let v' ≝ val_of_Byte (op1 eval op v) in
    247         ! st ← acca_store acc_a v' st;
    248           ret ? 〈E0, goto … l st〉
    249       | joint_instr_op2 op acc_a src ⇒
    250         ! v1 ← acca_retrieve … st acc_a;
     242          let v' ≝ BVByte (op1 eval op v) in
     243        ! st ← acca_store p dacc_a v' st;
     244          ret ? 〈E0, next … l st〉
     245      | OP2 op dacc_a sacc_a src ⇒
     246        ! v1 ← acca_retrieve … st sacc_a;
    251247        ! v1 ← Byte_of_val v1;
    252248        ! v2 ← greg_retrieve … st src;
    253249        ! v2 ← Byte_of_val v2;
    254         ! carry ← eval_bool_of_val (carry … st);
     250        ! carry ← bool_of_beval (carry … st);
    255251          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    256           let v' ≝ val_of_Byte v' in
    257           let carry ≝ of_bool carry in
    258         ! st ← acca_store acc_a v' st;
    259           ret ? 〈E0, goto … l (set_carry … carry st)〉
    260       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vfalse st)〉
    261       | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue st)〉
    262       | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    263         ! v1 ← acca_retrieve … st acc_a_reg;
     252          let v' ≝ BVByte v' in
     253          let carry ≝ beval_of_bool carry in
     254        ! st ← acca_store p dacc_a v' st;
     255          ret ? 〈E0, next … l (set_carry … carry st)〉
     256      | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
     257      | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
     258      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     259        ! v1 ← acca_retrieve … st sacc_a_reg;
    264260        ! v1 ← Byte_of_val v1;
    265         ! v2 ← accb_retrieve … st acc_b_reg;
     261        ! v2 ← accb_retrieve … st sacc_b_reg;
    266262        ! v2 ← Byte_of_val v2;
    267263          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    268           let v1' ≝ val_of_Byte v1' in
    269           let v2' ≝ val_of_Byte v2' in
    270         ! st ← acca_store acc_a_reg v1' st;
    271         ! st ← accb_store acc_b_reg v2' st;
    272           ret ? 〈E0, goto … l st〉
    273       | joint_instr_pop dst ⇒
     264          let v1' ≝ BVByte v1' in
     265          let v2' ≝ BVByte v2' in
     266        ! st ← acca_store p dacc_a_reg v1' st;
     267        ! st ← accb_store p dacc_b_reg v2' st;
     268          ret ? 〈E0, next … l st〉
     269      | POP dst ⇒
    274270        ! 〈st,v〉 ← pop … st;
    275         ! st ← acca_store … dst (val_of_Byte v) st;
    276           ret ? 〈E0, goto … l st〉
    277       | joint_instr_push src ⇒
     271        ! st ← acca_store p dst v st;
     272          ret ? 〈E0, next … l st〉
     273      | PUSH src ⇒
    278274        ! v ← acca_retrieve … st src;
    279         ! v ← Byte_of_val v;
    280275        ! st ← push … st v;
    281           ret ? 〈E0, goto … l st〉
    282       | joint_instr_move dst_src ⇒
    283           ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
    284       | joint_instr_call_id id argsno ⇒
     276          ret ? 〈E0, next … l st〉
     277      | MOVE dst_src ⇒
     278          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
     279      (*CSC: XXX bug here dest unused *)
     280      | CALL_ID id argsno dest ⇒
    285281        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    286282        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     
    289285            ! st ← save_ra … st l;
    290286              let st ≝ save_frame … st in
    291               let regs ≝ init_locals p (joint_if_locals … fn) in
     287              let regs ≝ init_locals (joint_if_locals … fn) in
    292288              let l' ≝ joint_if_entry … fn in
    293              ret ? 〈 E0, goto … l' (set_regs regs st)〉
     289             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
    294290          | External fn ⇒
    295291            ! params ← fetch_external_args … fn st;
     
    300296              let vs ≝ [mk_val ? evres] in
    301297            ! st ← set_result … vs st;
    302               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
    303           ]
    304       ]
    305     | joint_st_return ⇒
     298              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
     299          ]]
     300    | RETURN ⇒
    306301      ! st ← pop_frame … st;
    307302      ! 〈st,pch〉 ← pop … st;
    308303      ! 〈st,pcl〉 ← pop … st;
    309         let pc ≝ address_of_address_chunks pcl pch in
    310         ret ? 〈E0,set_pc … pc st〉
    311     | joint_st_extension c ⇒ exec_extended … p ge c st
    312     ].
    313 
    314 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. label → nat → state p → option ((*CSC: why not res*) int) ≝
    315   λglobals: list ident.
    316   λp.
    317   λexit.
    318   λregistersno.
    319   λst.
    320  (* CSC: monadic notation missing here *)
    321   match fetch_statement … st with
    322   [ Error _ ⇒ None ?
    323   | OK s ⇒
    324     match s with
    325       [ joint_st_return ⇒
    326         match fetch_ra … st with
    327          [ Error _ ⇒ None ?
    328          | OK st_l ⇒
    329            let 〈st,l〉 ≝ st_l in
    330            match label_eq l exit with
    331            [ inl _ ⇒
    332              (* CSC: monadic notation missing here *)
    333              match fetch_result … st registersno with
    334              [ Error _ ⇒ None ?
    335              | OK vals ⇒ Some ? (smerge2 vals)
    336              ]
    337            | inr _ ⇒ None ?
    338            ]
    339          ]
    340       | _ ⇒ None ?
    341       ]
    342   ].
    343 
    344 definition joint_exec: ∀globals:list ident. sem_params2 globals → label → nat → execstep io_out io_in ≝
    345   λglobals,p.
    346   λexit.
    347   λregistersno.
    348   mk_execstep ? ? ? ? (is_final globals p exit registersno) (m p) (eval_statement globals p).
    349 
    350 (* CSC: XXX the program type does not fit with the globalenv and init_mem *)
    351 axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝
    352 λp.
    353   do ge ← globalenv Genv ?? p;
    354   do m ← init_mem Genv ?? p;
    355   let main ≝ rtl_pr_main ?? p in
     304        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
     305cases addr //
     306qed.
     307
     308definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
     309 λglobals,p,exit,registersno,st. res_to_opt … (
     310  do s ← fetch_statement … st;
     311  match s with
     312   [ RETURN ⇒
     313      do 〈st,l〉 ← fetch_ra … st;
     314      if eq_address l exit then
     315       do val ← fetch_result … st registersno;
     316       match val with
     317        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
     318        | _ ⇒ Error ? []]
     319      else
     320       Error ? []
     321   | _ ⇒ Error ? []]).
     322
     323record evaluation_parameters : Type[1] ≝
     324 { globals: list ident
     325 ; sparams2: sem_params2 globals
     326 ; exit: address
     327 ; registersno: nat
     328 ; genv2: genv globals sparams2
     329 }.
     330
     331definition joint_exec: trans_system io_out io_in ≝
     332  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
     333   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
     334   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
     335
     336definition make_global :
     337 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     338  joint_program pars → evaluation_parameters
     339
     340 λpars,sparams.
     341  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
     342[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
     343qed.
     344
     345definition make_initial_state :
     346 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     347 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
     348λpars,sparams,p.
     349  let ge ≝ genv2 (make_global pars sparams p) in
     350  do m ← init_mem Genv … (λx.[Init_space x]) p;
     351  let main ≝ prog_main … p in
    356352  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    357353  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    358   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
     354  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
     355cases daemon qed.
     356(*
     357RTL:
     358 init_prog == init_mem
     359 init_sp: inizializzare lo stack pointer
     360 init_isp: inizializzare l'altro stack pointer
     361 init_renv: inizializzare i registri fisici
     362 init_main_call: chiamata di funzione
     363   --- init_fun_call: cambia fra ERTL e LTL
     364 change_carry: a 0
    359365*)
    360366
    361367definition joint_fullexec :
    362  ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
    363  λglobals,p,program.
    364   let exit ≝ ? in
    365   let registersno ≝ ? in
    366   mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).
     368 ∀pars:∀globals.params globals.
     369 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     370 fullexec io_out io_in ≝
     371 λpars,sparams.
     372  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracChangeset for help on using the changeset viewer.