Changeset 1233


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (8 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1224 r1233  
    22
    33definition lin_params: params ≝
    4  mk_params
    5    unit unit unit unit registers_move Register
    6      unit unit unit unit.
     4 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
    75
    8 definition pre_lin_statement ≝
    9  λglobals: list ident. joint_statement lin_params globals.
    10 
    11 definition lin_statement ≝
    12   λglobals.
    13     option ident × (pre_lin_statement globals).
     6definition lin_statement ≝ joint_statement lin_params.
    147
    158definition well_formed_P ≝
     
    2114      match \fst hd with
    2215      [ Some lbl ⇒ False
    23       | None ⇒ True
    24       ]
    25     ].
     16      | None ⇒ True]].
    2617
     18(*
    2719definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
    2820 λglobals.
     
    3123cases daemon
    3224qed.
     25*)
    3326
    34 definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals).
    35 
    36 inductive lin_function_definition (globals: list ident): Type[0] ≝
    37   lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
    38 | lin_fu_external: external_function → lin_function_definition globals.
    39 
    40 record lin_program: Type[0] ≝
    41 {
    42   lin_pr_vars: list (ident × nat);
    43   lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
    44   lin_pr_main: option ident
    45 }.
     27definition ltl_program ≝ joint_program lin_params.
  • src/LTL/LTL.ma

    r1222 r1233  
    33
    44definition ltl_params: params ≝
    5  mk_params
    6    unit unit unit unit registers_move Register
    7      unit unit unit unit.
     5 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
    86
    9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
     7definition ltl_statement ≝ joint_statement ltl_params.
    108
    11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
     9(*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    1210 λglobals.
    13   mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).
     11  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
    1412
    15 definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals).
    16 (*
    17  
    18 record ltl_internal_function (globals: list ident): Type[0] ≝
    19 {
    20   ltl_if_luniverse: universe LabelTag;
    21   ltl_if_runiverse: universe RegisterTag;
    22   ltl_if_stacksize: nat;
    23   ltl_if_graph: ltl_statement_graph globals;
    24   ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
    25   ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
    26 }.
    27 
    28 inductive ltl_function_definition (globals: list ident): Type[0] ≝
    29   | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
    30   | ltl_fu_external_function: external_function → ltl_function_definition globals.
    31  
    32 record ltl_program (globals: list (ident × nat)): Type[0] ≝
    33 {
    34   ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
    35   ltl_pr_main: option ident
    36 }.
    37 *)
     13definition ltl_program ≝ joint_program ltl_params.
  • src/LTL/LTLToLIN.ma

    r1224 r1233  
    33include "utilities/BitVectorTrieSet.ma".
    44
    5 axiom LTLTag: String.
    6 
    7 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
     5definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
    86  λglobals: list ident.
    97  λs: ltl_statement globals.
    108  match s with
    11   [ joint_st_return ⇒ joint_st_return lin_params globals
    12   | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
    13   | joint_st_goto l ⇒ joint_st_goto lin_params globals l
    14   | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
     9  [ joint_st_return ⇒ joint_st_return
     10  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
     11  | joint_st_goto l ⇒ joint_st_goto l
     12  | joint_st_extension ext ⇒ joint_st_extension lin_params ext
    1513  ].
    16    
    17 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: label.
    19   λg: BitVectorTrieSet 16.
    20     set_insert ? (word_of_identifier ? l) g.
    21    
    22 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: label.
    24   λg: BitVectorTrieSet 16.
    25     set_insert ? (word_of_identifier ? l) g.
    26    
    27 definition marked: label → BitVectorTrieSet 16 → bool ≝
    28   λl: label.
    29   λg: BitVectorTrieSet 16.
    30     set_member ? (word_of_identifier ? l) g.
    31    
    32 definition graph_lookup ≝
    33   λglobals: list ident.
    34   λl: label.
    35   λgr: graph (ltl_statement globals).
    36     lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    37    
    38 definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝
    39   λglobals,l,g.graph_lookup globals l g.
    4014
    41 definition foo ≝
    42   λl2, visited, required, globals, generated, g, n.
    43   λvisit:
    44   ∀globals: list ident.
    45   ∀g: graph (ltl_statement globals).
    46   ∀required: BitVectorTrieSet 16.
    47   ∀visited: BitVectorTrieSet 16.
    48   ∀generated: list (pre_lin_statement globals).
    49   ∀l: label.
    50   ∀n: nat.
    51     BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    52   if marked l2 visited then
    53     〈require l2 required, (joint_st_goto … globals l2) :: generated〉
    54   else
    55    visit globals g required visited generated l2 n.
    56 
    57 (* XXX: look at this.  way too complicated to understand whether it is correct,
    58    in my opinion.
    59 *)
     15(* Invariant: l has not been visited yet the very first time the
     16   function is called and in the true branch of a conditional call.
     17   This avoid useless gotos.
     18   
     19   Note: the OCaml code contains some useful explanatory comments. *)
    6020let rec visit
    6121  (globals: list ident) (g: graph (ltl_statement globals))
    6222  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    63   (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
    64     on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
     23  (generated: list (lin_statement globals)) (l: label) (n: nat)
     24    on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
    6525  match n with
    66   [ O ⇒ 〈required, generated〉
     26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    6727  | S n' ⇒
    68     let visited' ≝ mark l visited in
    69     match fetch globals l g with
    70     [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
    71     | Some statement ⇒
    72       let translated_statement ≝ translate_statement globals statement in
    73       let generated'' ≝ translated_statement :: generated in
    74       match statement with
    75       [ joint_st_sequential instr l2 ⇒
    76         match instr with
    77         [ joint_instr_cond acc_a_reg l1 ⇒
    78               let required' ≝
    79                 if marked l2 visited' then
    80                   require l2 required
    81                 else
    82                   required in
    83               let 〈required', generated''〉 ≝
    84                foo l2 visited' required' globals generated'' g n' visit (*
    85                 if marked l2 visited' then
    86                   〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    87                 else
    88                   visit globals g required' visited' generated'' l2 n'*) in
    89               let required'' ≝ require l1 required' in
    90                 if ¬(marked l1 visited') then
    91                   visit globals g required'' visited' generated'' l1 n'
    92                 else
    93                   〈required', generated''〉
    94           | _ ⇒
    95             let required' ≝
    96               if marked l2 visited' then
    97                 require l2 required
    98               else
    99                 required in
    100             if marked l2 visited' then
    101               〈required', joint_st_goto … globals l2 :: generated''〉
    102             else
    103               visit globals g required' visited' generated'' l2 n'
    104           ]
    105     | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    106     | joint_st_goto l ⇒
    107       let required' ≝
    108         if marked l visited' then
    109          require l required
    110         else
    111          required
    112       in
    113         if marked l visited' then
    114           〈required', joint_st_goto … globals l :: generated''〉
    115         else
    116           visit globals g required' visited' generated'' l n'
    117     | joint_st_extension ext ⇒ 〈required, generated〉
    118     ]
    119   ]
    120 ].
     28    if set_member … (word_of_identifier … l) visited then
     29     〈set_insert ? (word_of_identifier ? l) required, joint_st_goto … globals l :: generated〉
     30    else
     31     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
     32     match lookup LabelTag ? g (an_identifier LabelTag (word_of_identifier … l)) with
     33     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
     34     | Some statement ⇒
     35       let translated_statement ≝ translate_statement globals statement in
     36       let generated' ≝ translated_statement :: generated in
     37       match statement with
     38       [ joint_st_sequential instr l2 ⇒
     39         match instr with
     40         [ joint_instr_cond acc_a_reg l1 ⇒
     41            let 〈required', generated''〉 ≝
     42             visit globals g required visited' generated' l2 n' in
     43            let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
     44             if set_member … (word_of_identifier … l1) visited' then
     45               〈required', generated''〉
     46             else
     47               visit globals g required'' visited' generated'' l1 n'
     48         | _ ⇒ visit globals g required visited' generated' l2 n']
     49     | joint_st_return ⇒ 〈required, generated'〉
     50     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
     51     | joint_st_extension ext ⇒ ⊥ ]]].
     52[3: @ext
     53|1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
     54qed.
    12155
    122 (*
     56(* CSC: The branch compression (aka tunneling) optimization is not implemented
     57   in Matita *)
     58definition branch_compress ≝ λglobals.λa:graph (ltl_statement globals).a.
     59
    12360definition translate_graph ≝
    12461  λglobals: list Identifier.
    125   λg: LTLStatementGraph globals.
    126   λentry: Identifier.
     62  λg: graph (ltl_statement globals).
     63  λentry: label.
     64    let g ≝ branch_compress ? g in
    12765    let visited ≝ set_empty ? in
    128     let required ≝ set_insert ? entry (set_empty ?) in
     66    let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
    12967    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
    13068    let reversed ≝ rev ? translated in
    13169      filter (λs: PreLINStatement globals. ?) reversed.
    132 *)
  • src/RTL/semantics.ma

    r1141 r1233  
    264264     [ nil ⇒ Some ? (smerge2 v)
    265265     | _ ⇒ None ? ]].
    266 
     266(*
    267267definition RTL_exec : execstep io_out io_in ≝
    268268  mk_execstep … ? is_final mem_of_state eval_statement.
    269 
     269*)
    270270(* CSC: XXX the program type does not fit with the globalenv and init_mem
    271271definition make_initial_state : rtl_program → res (genv × state) ≝
  • src/common/SmallstepExec.ma

    r1231 r1233  
    44include "common/Events.ma".
    55
    6 record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    7 { global : Type[0]
     6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
     7{ global : Type[1]
    88; state  : global → Type[0]
    99; is_final : ∀g. state g → option int
     
    8080*)
    8181
    82 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     82record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
    8383{ program : Type[0]
    8484; es1 :> trans_system outty inty
  • src/joint/Joint.ma

    r1228 r1233  
    55include "common/Graphs.ma".
    66
     7record params_: Type[1] ≝
     8 { acc_a_reg: Type[0]
     9 ; acc_b_reg: Type[0]
     10 ; dpl_reg: Type[0]
     11 ; dph_reg: Type[0]
     12 ; pair_reg: Type[0]
     13 ; generic_reg: Type[0]
     14 
     15 ; extend_statements: Type[0]
     16 
     17 ; resultT: Type[0]
     18 ; localsT: Type[0]
     19 ; paramsT: Type[0]
     20 }.
     21
    722record 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];
    15  
    16   extend_statements: Type[0];
    17  
    18   resultT: Type[0];
    19   localsT: Type[0];
    20   paramsT: Type[0]
    21 }.
     23 { pars_:> params_
     24 ; succ: Type[0]
     25 }.
    2226
    23 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     27inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
    2428  | joint_instr_comment: String → joint_instruction p globals
    2529  | joint_instr_cost_label: costlabel → joint_instruction p globals
     
    4044
    4145inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    42   | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
     46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4347  | joint_st_goto: label → joint_statement p globals
    4448  | joint_st_return: joint_statement p globals
    4549  | joint_st_extension: extend_statements p → joint_statement p globals.
    4650
    47 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    48  { pmemoryT: Type[0]
    49  ; lookup: pmemoryT → label → option (joint_statement preparams globals)
    50  }.
    51 
    52 record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     51record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    5352{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5453  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
    5554(*  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;
     55  joint_if_result   : resultT p;
     56  joint_if_params   : paramsT p;
     57  joint_if_locals   : localsT p;
    5958  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 ?
     59  joint_if_lookup   : label → option (joint_statement p globals);
     60  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
     61  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
    6362}.
    6463
    6564definition set_luniverse ≝
     65  λp:params.
    6666  λglobals  : list ident.
    67   λpre.
    68   λp: sem_params_ pre globals.
    69   λint_fun  : joint_internal_function globals … p.
     67  λint_fun  : joint_internal_function p globals.
    7068  λluniverse: universe LabelTag.
    7169  let runiverse ≝ joint_if_runiverse … int_fun in
     
    7472  let result    ≝ joint_if_result … int_fun in
    7573  let stacksize ≝ joint_if_stacksize … int_fun in
    76   let graph     ≝ joint_if_graph … int_fun in
     74  let lookup    ≝ joint_if_lookup … int_fun in
    7775  let entry     ≝ joint_if_entry … int_fun in
    7876  let exit      ≝ joint_if_exit … int_fun in
    79     mk_joint_internal_function globals ? p
     77    mk_joint_internal_function … globals
    8078      luniverse runiverse result params locals
    81       stacksize graph entry exit.
     79      stacksize lookup entry exit.
    8280
    83 definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     81definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
    8482
    85 definition joint_program ≝
    86   λglobals: list ident.
    87   λpre.
    88   λp: sem_params_ pre globals.
    89     program (λx. joint_function globals pre p) nat.
     83definition joint_program ≝ λp:params. program (joint_function p) nat.
    9084
    9185(****************************************************************************)
  • src/joint/semantics.ma

    r1220 r1233  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record sem_params: Type[1] ≝
    20  { p:> params
    21  ; framesT: Type[0]
     19record more_sem_params (p:params): Type[1] ≝
     20 { framesT: Type[0]
    2221 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
    23  
     22
     23 ; succ_pc: succ p → address → address
    2424 ; pop_frame_: framesT → res framesT
    2525 ; save_frame_: framesT → regsT → framesT
     
    4040 }.
    4141
    42 definition address_of_label: sem_params → label → address.
    43  #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label p l)))
    44  cases (beval_pair_of_pointer (pointer_of_label p l)) in ⊢ (???% → ?)
    45   [ #res #_ @res
    46   | #msg cases (pointer_of_label p l) * * #q #com #off #E1 #E2 destruct ]
    47 qed.
     42record sem_params: Type[1] ≝
     43 { spp :> params
     44 ; more_sem_pars :> more_sem_params spp
     45 }.
    4846
    4947record state (p: sem_params): Type[0] ≝
    50  { st_frms: framesT p
     48 { st_frms: framesT ? p
    5149 ; pc: address
    5250 ; sp: pointer
    5351 ; carry: beval
    54  ; regs: regsT p
     52 ; regs: regsT ? p
    5553 ; m: bemem
    5654 }.
    5755
    58 definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
     56definition genv ≝ λp:params.λglobals. (genv_t Genv) (joint_function p globals).
     57
     58(*
     59CSC: fetch_statement credo sia implementabile ⇒ globals non e' necessario ⇒ niente
     60casino e posso back-trackare il cambiamento in SmallstepExec!!! Togliere del
     61tutto il parametro a exec_extended.
     62CSC: NO! RTL ha come exec_extended tail_call e (tail_)call_ptr che usa genv
     63*)
     64
     65record more_sem_params2 (p: params) (globals: list ident): Type[1] ≝
     66 { more_sparams:> more_sem_params p
     67 
     68 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     69 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
     70 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     71 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
     72
     73 ; exec_extended: genv p globals → 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)))
     74 }.
    5975
    6076record sem_params2 (globals: list ident): Type[1] ≝
    61  { sparams:> sem_params
    62  ; pre_sem_params:> sem_params_ sparams globals
    63  
    64  ; fetch_statement: state sparams → res (joint_statement sparams globals)
    65  ; fetch_external_args: external_function → state sparams → res (list val)
    66  ; set_result: list val → state sparams → res (state sparams)
    67  ; fetch_result: state sparams → nat → res val
    68 
    69  ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
    70  }.
     77 { p2:> params
     78 ; more_sparams2:> more_sem_params2 p2 globals
     79 }.
     80
     81definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
     82coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
     83 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
     84
     85unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
     86   S ≟ sem_params_of_sem_params2 globals p
     87(* ---------------------------------------- *) ⊢
     88   pars_ (spp (mk_sem_params (p2 globals p)
     89    (more_sparams (p2 globals p) globals
     90    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
     91
     92definition address_of_label: sem_params → label → address.
     93 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
     94 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
     95  [ #res #_ @res
     96  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
     97qed.
    7198
    7299definition set_m: ∀p. bemem → state p → state p ≝
    73100 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
    74101
    75 definition set_regs: ∀p. regsT p → state p → state p ≝
     102definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    76103 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
    77104
     
    85112 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
    86113
    87 definition set_frms: ∀p. framesT p → state p → state p ≝
     114definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    88115 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
    89116
     
    91118 λp,l,st. set_pc … (address_of_label p l) st.
    92119
     120definition next: ∀p:sem_params. succ … p → state p → state p ≝
     121 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
     122
    93123definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
    94124 λp,dst,v,st.
     
    135165
    136166definition save_frame: ∀p:sem_params. state p → state p ≝
    137  λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
     167 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
    138168
    139169(* removes the top frame from the frames list *)
    140170definition pop_frame: ∀p. state p → res (state p) ≝
    141171 λp,st.
    142   do frames ← pop_frame_ p (st_frms … st);
     172  do frames ← pop_frame_ p (st_frms … st);
    143173  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
    144174
     
    160190  OK ? 〈st,v〉.
    161191
    162 definition save_ra : ∀p. state p → label → res (state p) ≝
     192definition save_ra : ∀p. state p → succ p → res (state p) ≝
    163193 λp,st,l.
    164   let 〈addrl,addrh〉 ≝ address_of_label p l in
     194  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
    165195  do st ← push … st addrl;
    166196  push … st addrh.
     
    181211coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    182212
    183 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)) ≝
    184   λglobals,p. λge,st.
    185   ! s ← fetch_statement globals p st;
     213definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals → state p → IO io_out io_in (trace × (state p)) ≝
     214 λglobals,p,ge,st.
     215  ! s ← fetch_statement st;
    186216  match s with
    187217    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
    188218    | joint_st_sequential seq l ⇒
    189219      match seq with
    190       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto … l st〉
    191       | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
     220      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, next … l st〉
     221      | joint_instr_comment c ⇒ ret ? 〈E0, next … l st〉
    192222      | joint_instr_int dest v ⇒
    193         ! st ← greg_store dest (BVByte v) st;
    194           ret ? 〈E0, goto … l st〉
     223        ! st ← greg_store ? dest (BVByte v) st;
     224          ret ? 〈E0, next … l st〉
    195225      | joint_instr_load dst addrl addrh ⇒
    196226        ! vaddrh ← dph_retrieve … st addrh;
     
    199229        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    200230        ! st ← acca_store … dst v st;
    201           ret ? 〈E0, goto … l st〉
     231          ret ? 〈E0, next … l st〉
    202232      | joint_instr_store addrl addrh src ⇒
    203233        ! vaddrh ← dph_retrieve … st addrh;
     
    206236        ! v ← acca_retrieve … st src;
    207237        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    208           ret ? 〈E0, goto … l (set_m … m' st)〉
     238          ret ? 〈E0, next … l (set_m … m' st)〉
    209239      | joint_instr_cond src ltrue ⇒
    210240        ! v ← acca_retrieve … st src;
    211241        ! b ← bool_of_beval v;
    212           ret ? 〈E0, goto … (if b then ltrue else l) st〉
     242          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
    213243      | joint_instr_address ident prf ldest hdest ⇒
    214244        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     
    216246        ! st ← dpl_store … ldest laddr st;
    217247        ! st ← dph_store … hdest haddr st;
    218           ret ? 〈E0, goto … l st〉
     248          ret ? 〈E0, next … l st〉
    219249      | joint_instr_op1 op acc_a ⇒
    220250        ! v ← acca_retrieve … st acc_a;
     
    222252          let v' ≝ BVByte (op1 eval op v) in
    223253        ! st ← acca_store … acc_a v' st;
    224           ret ? 〈E0, goto … l st〉
     254          ret ? 〈E0, next … l st〉
    225255      | joint_instr_op2 op acc_a src ⇒
    226256        ! v1 ← acca_retrieve … st acc_a;
     
    233263          let carry ≝ beval_of_bool carry in
    234264        ! st ← acca_store … acc_a v' st;
    235           ret ? 〈E0, goto … l (set_carry … carry st)〉
    236       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVfalse st)〉
    237       | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVtrue st)〉
     265          ret ? 〈E0, next … l (set_carry … carry st)〉
     266      | joint_instr_clear_carry ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
     267      | joint_instr_set_carry ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
    238268      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    239269        ! v1 ← acca_retrieve … st acc_a_reg;
     
    246276        ! st ← acca_store … acc_a_reg v1' st;
    247277        ! st ← accb_store … acc_b_reg v2' st;
    248           ret ? 〈E0, goto … l st〉
     278          ret ? 〈E0, next … l st〉
    249279      | joint_instr_pop dst ⇒
    250280        ! 〈st,v〉 ← pop … st;
    251281        ! st ← acca_store … dst v st;
    252           ret ? 〈E0, goto … l st〉
     282          ret ? 〈E0, next … l st〉
    253283      | joint_instr_push src ⇒
    254284        ! v ← acca_retrieve … st src;
    255285        ! st ← push … st v;
    256           ret ? 〈E0, goto … l st〉
     286          ret ? 〈E0, next … l st〉
    257287      | joint_instr_move dst_src ⇒
    258           ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
     288          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
    259289      | joint_instr_call_id id argsno ⇒
    260290        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    264294            ! st ← save_ra … st l;
    265295              let st ≝ save_frame … st in
    266               let regs ≝ init_locals p (joint_if_locals … fn) in
     296              let regs ≝ init_locals (sem_params_of_sem_params2 globals p) … (joint_if_locals … fn) in
    267297              let l' ≝ joint_if_entry … fn in
    268298             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
     
    275305              let vs ≝ [mk_val ? evres] in
    276306            ! st ← set_result … vs st;
    277               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
     307              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
    278308          ]]
    279309    | joint_st_return ⇒
     
    287317
    288318definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
    289   λglobals,p,exit,registersno,st. res_to_opt … (
     319 λglobals,p,exit,registersno,st. res_to_opt … (
    290320  do s ← fetch_statement … st;
    291321  match s with
     
    293323      do 〈st,l〉 ← fetch_ra … st;
    294324      if eq_address l exit then
    295        do val ← fetch_result globals p st registersno;
     325       do val ← fetch_result st registersno;
    296326       match val with
    297327        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
     
    301331   | _ ⇒ Error ? []]).
    302332
    303 definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
    304   λglobals,p.
    305   λexit.
    306   λregistersno.
    307   mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).
     333record evaluation_parameters : Type[1] ≝
     334 { globals: list ident
     335 ; sparams2: sem_params2 globals
     336 ; exit: address
     337 ; registersno: nat
     338 ; genv2: genv sparams2 globals
     339 }.
     340
     341definition joint_exec: trans_system io_out io_in ≝
     342  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
     343   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
     344   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
     345
     346definition make_global :
     347 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     348  joint_program pars → evaluation_parameters
     349
     350 λpars,sparams.
     351  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
     352[1,2: cases daemon ]
     353qed.
    308354
    309355definition make_initial_state :
    310  ∀globals:list ident.∀sparams: sem_params2 globals. joint_program ?? (pre_sem_params ? sparams) →
    311    res ((genv ?? (pre_sem_params ? sparams)) × (state sparams)) ≝
    312 λglobals,par,p.
    313   do ge ← globalenv Genv … (λx.[Init_space x]) p;
     356 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     357 ∀p: joint_program … pars. res (state (mk_sem_params pars (sparams p))) ≝
     358λpars,sparams,p.
     359  let ge ≝ genv2 (make_global pars sparams p) in
    314360  do m ← init_mem Genv … (λx.[Init_space x]) p;
    315361  let main ≝ prog_main … p in
    316362  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    317363  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    318   ?(*
    319   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉*).
     364  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
     365cases daemon qed.
    320366(*
    321367RTL:
     
    328374 change_carry: a 0
    329375*)
     376
    330377definition joint_fullexec :
    331  ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
    332  λglobals,p,program.
    333   let exit ≝ ? in
    334   let registersno ≝ ? in
    335   mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).
     378 ∀pars:params.
     379 ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     380 fullexec io_out io_in ≝
     381 λpars,sparams.
     382  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracChangeset for help on using the changeset viewer.