Changeset 1161


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (8 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1159 r1161  
    1717 with precedence 10
    1818for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     19
     20(*
     21notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
     22 with precedence 10
     23for @{
     24  match $t with
     25  [ pair ${ident x} y' ⇒
     26    match y' with
     27    [ pair ${ident y} ${ident z} ⇒ $s ]
     28  ]
     29}.
     30*)
    1931
    2032definition ltb ≝
  • src/ERTL/ERTL.ma

    r1138 r1161  
    11include "ASM/I8051.ma".
     2include "LIN/JointLTLLIN.ma".
    23include "utilities/BitVectorTrieSet.ma".
    34include "utilities/IdentifierTools.ma".
     
    89definition registers ≝ list register.
    910
     11definition pre_ertl_statement ≝
     12  λglobals: list ident.
     13  joint_statement label globals register
     14                  register register register
     15                  register (Register × Register).
     16                 
     17inductive ertl_statement (globals: list ident): Type[0] ≝
     18  | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
     19  | ertl_st_new_frame: label → ertl_statement globals
     20  | ertl_st_del_frame: label → ertl_statement globals
     21  | ertl_st_frame_size: register → label → ertl_statement globals
     22  | ertl_st_move: register → register → label → ertl_statement globals
     23  | ertl_st_get_hdw: register → Register → label → ertl_statement globals
     24  | ertl_st_set_hdw: Register → register → label → ertl_statement globals.
     25
     26(*
    1027inductive ertl_statement: Type[0] ≝
    1128  | ertl_st_skip: label → ertl_statement
     
    2138  | ertl_st_push: register → label → ertl_statement
    2239  | ertl_st_addr: register → register → ident → label → ertl_statement
    23 (* XXX: changed from O'Caml
    24   | ertl_st_addr_h: register → ident → label → ertl_statement
    25   | ertl_st_addr_l: register → ident → label → ertl_statement
    26 *)
    2740  | ertl_st_int: register → Byte → label → ertl_statement
    2841  | ertl_st_move: register → register → label → ertl_statement
    2942  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    30 (* XXX: changed from O'Caml
    31   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    32   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    33 *)
    3443  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    3544  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
     
    4150  | ertl_st_cond: register → label → label → ertl_statement
    4251  | ertl_st_return: ertl_statement.
     52*)
    4353
    44 definition ertl_statement_graph ≝ graph ertl_statement.
     54definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
    4555
    46 record ertl_internal_function: Type[0] ≝
     56record ertl_internal_function (globals: list ident): Type[0] ≝
    4757{
    4858  ertl_if_luniverse: universe LabelTag;
     
    5161  ertl_if_locals: registers;
    5262  ertl_if_stacksize: nat;
    53   ertl_if_graph: ertl_statement_graph;
     63  ertl_if_graph: ertl_statement_graph globals;
    5464  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    5565  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5666}.
    5767
    58 definition ertl_function ≝ fundef ertl_internal_function.
     68definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    5969 
    60 record ertl_program: Type[0] ≝
     70record ertl_program (globals: list ident): Type[0] ≝
    6171{
    6272  ertl_pr_vars: list (ident × nat);
    63   ertl_pr_funcs: list (ident × ertl_function);
     73  ertl_pr_funcs: list (ident × (ertl_function globals));
    6474  ertl_pr_main: option ident
    6575}.
     76
     77
     78(* XXX: changed from O'Caml
     79  | ertl_st_addr_h: register → ident → label → ertl_statement
     80  | ertl_st_addr_l: register → ident → label → ertl_statement
     81*)
     82
     83(* XXX: changed from O'Caml
     84  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     85  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     86*)
  • src/ERTL/ERTLToLTL.ma

    r1160 r1161  
    5757    let off ≝ adjust_off int_fun off in
    5858    let luniv ≝ ertl_if_luniverse int_fun in
    59     let 〈l, 〈graph, luniv〉〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
    60     let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    61     let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    62     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    63     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    64     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    65     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    66       〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉.
     59    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     60    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
     61    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     63    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     66      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
    6767
    6868definition set_stack ≝
     
    7474  λl.
    7575  let off ≝ adjust_off int_fun off in
    76   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
    77   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
    78   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    79   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    80   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    81   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    82   let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    83     〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉.
     76  let luniv ≝ ertl_if_luniverse int_fun in
     77  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
     78  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
     79  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     80  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     81  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     82  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     83  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     84    〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
    8485
    8586definition write ≝
     
    9192  match lookup r with
    9293  [ decision_spill off ⇒
    93     let 〈stmt, graph〉 ≝ set_stack int_fun globals graph off RegisterSST l in
    94       〈RegisterSST, generate globals graph stmt〉
    95   | decision_colour hwr ⇒ 〈hwr, 〈l, graph〉〉
     94    let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in
     95    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     96      〈RegisterSST, 〈l, 〈graph, luniv〉〉〉
     97  | decision_colour hwr ⇒
     98    let luniv ≝ ertl_if_luniverse int_fun in
     99      〈hwr, 〈l, 〈graph, luniv〉〉〉
    96100  ].
    97101
  • src/ERTL/semantics.ma

    r1156 r1161  
    4949axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    5050
    51 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
    5252
    5353(* CSC: frame reduced to this *)
     
    137137
    138138(*CSC: To be implemented *)
     139
     140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    139141axiom fetch_function: state → res ertl_internal_function.
    140 axiom fetch_statement: state → res ertl_statement.
    141142
    142143definition init_locals : list register → register_env val ≝
     
    212213  OK ? (set_regs regs st))).
    213214
    214 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    215 λge,st.
    216   ! s ← fetch_statement st;
     215definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
     216  λglobals. λge,st.
     217  ! s ← fetch_statement globals st;
    217218  match s with
    218   [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
    219   | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
    220   | ertl_st_int dest v l ⇒
    221      ! locals ← reg_store dest (val_of_Byte v) (locals st);
    222      ret ? 〈E0, goto l (set_locals locals st)〉
    223   | ertl_st_load addrl addrh dst l ⇒
    224       ! vaddrh ← reg_retrieve (locals st) addrh;
    225       ! vaddrl ← reg_retrieve (locals st) addrl;
    226       ! vaddr ← smerge vaddrl vaddrh;
    227       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    228       ! locals ← reg_store dst v (locals st);
    229       ret ? 〈E0, goto l (set_locals locals st)〉
    230   | ertl_st_store addrl addrh src l ⇒
    231       ! vaddrh ← reg_retrieve (locals st) addrh;
    232       ! vaddrl ← reg_retrieve (locals st) addrl;
    233       ! vaddr ← smerge vaddrl vaddrh;
    234       ! v ← reg_retrieve (locals st) src;
    235       ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    236       ret ? 〈E0, goto l (set_m m' st)〉
    237   | ertl_st_cond src ltrue lfalse ⇒
    238       ! v ← reg_retrieve (locals st) src;
    239       ! b ← eval_bool_of_val v;
    240       ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    241   | ertl_st_addr ldest hdest id l ⇒
    242      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    243      let 〈laddr,haddr〉 ≝ represent_block addr in
    244      ! locals ← reg_store ldest laddr (locals st);
    245      ! locals ← reg_store hdest haddr locals;
    246      ret ? 〈E0, goto l (set_locals locals st)〉
    247   | ertl_st_op1 op dst src l ⇒
    248      ! v ← reg_retrieve (locals st) src;
    249      ! v ← Byte_of_val v;
    250      let v' ≝ val_of_Byte (op1 eval op v) in
    251      ! locals ← reg_store dst v' (locals st);
    252      ret ? 〈E0, goto l (set_locals locals st)〉
    253   | ertl_st_op2 op dst src1 src2 l ⇒
    254      ! v1 ← reg_retrieve (locals st) src1;
    255      ! v1 ← Byte_of_val v1;
    256      ! v2 ← reg_retrieve (locals st) src2;
    257      ! v2 ← Byte_of_val v2;
    258      ! carry ← eval_bool_of_val (carry st);
    259      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    260      let v' ≝ val_of_Byte v' in
    261      let carry ≝ of_bool carry in
    262      ! locals ← reg_store dst v' (locals st);
    263      ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    264   | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    265      ! v1 ← reg_retrieve (locals st) sacc;
    266      ! v1 ← Byte_of_val v1;
    267      ! v2 ← reg_retrieve (locals st) sbacc;
    268      ! v2 ← Byte_of_val v2;
    269      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    270      let v1' ≝ val_of_Byte v1' in
    271      let v2' ≝ val_of_Byte v2' in
    272      ! locals ← reg_store dacc v1' (locals st);
    273      ! locals ← reg_store dbacc v2' locals;
    274      ret ? 〈E0, goto l (set_locals locals st)〉
    275   | ertl_st_clear_carry l ⇒
    276     ret ? 〈E0, goto l (set_carry Vfalse st)〉
    277   | ertl_st_set_carry l ⇒
    278     ret ? 〈E0, goto l (set_carry Vtrue st)〉
    279      
    280   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    281          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    282          be more than enough... *)
    283   | ertl_st_move dst src l ⇒
    284      ! v ← reg_retrieve (locals st) src;
    285      ! locals ← reg_store dst v (locals st);
    286      ret ? 〈E0, goto l (set_locals locals st)〉
    287   | ertl_st_hdw_to_hdw dst src l ⇒
    288      ! v ← hwreg_retrieve (regs st) src;
    289      ! regs ← hwreg_store dst v (regs st);
    290      ret ? 〈E0, goto l (set_regs regs st)〉
     219  [ ertl_st_lift_pre pre ⇒
     220    match pre with
     221    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
     222    | joint_st_sequential seq l ⇒
     223      match seq with
     224      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
     225      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
     226      | joint_instr_int dest v ⇒
     227        ! locals ← reg_store dest (val_of_Byte v) (locals st);
     228          ret ? 〈E0, goto l (set_locals locals st)〉
     229      | joint_instr_load addrl addrh dst ⇒
     230        ! vaddrh ← reg_retrieve (locals st) addrh;
     231        ! vaddrl ← reg_retrieve (locals st) addrl;
     232        ! vaddr ← smerge vaddrl vaddrh;
     233        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
     234        ! locals ← reg_store dst v (locals st);
     235          ret ? 〈E0, goto l (set_locals locals st)〉
     236      | joint_instr_store addrl addrh src ⇒
     237        ! vaddrh ← reg_retrieve (locals st) addrh;
     238        ! vaddrl ← reg_retrieve (locals st) addrl;
     239        ! vaddr ← smerge vaddrl vaddrh;
     240        ! v ← reg_retrieve (locals st) src;
     241        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     242          ret ? 〈E0, goto l (set_m m' st)〉
     243      | joint_instr_cond src ltrue ⇒
     244        ! v ← reg_retrieve (locals st) src;
     245        ! b ← eval_bool_of_val v;
     246          ret ? 〈E0, goto (if b then ltrue else l) st〉
     247      | joint_instr_address ident prf ldest hdest ⇒
     248        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     249          let 〈laddr,haddr〉 ≝ represent_block addr in
     250        ! locals ← reg_store ldest laddr (locals st);
     251        ! locals ← reg_store hdest haddr locals;
     252          ret ? 〈E0, goto l (set_locals locals st)〉
     253      | joint_instr_op1 op acc_a ⇒
     254        ! v ← reg_retrieve (locals st) acc_a;
     255        ! v ← Byte_of_val v;
     256          let v' ≝ val_of_Byte (op1 eval op v) in
     257        ! locals ← reg_store acc_a v' (locals st);
     258          ret ? 〈E0, goto l (set_locals locals st)〉
     259      | joint_instr_op2 op acc_a_reg dest ⇒
     260        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     261        ! v1 ← Byte_of_val v1;
     262        ! v2 ← reg_retrieve (locals st) acc_a_reg;
     263        ! v2 ← Byte_of_val v2;
     264        ! carry ← eval_bool_of_val (carry st);
     265          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     266          let v' ≝ val_of_Byte v' in
     267          let carry ≝ of_bool carry in
     268        ! locals ← reg_store dest v' (locals st);
     269          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
     270      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
     271      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     272      | joint_instr_hdw_to_hdw dst_src ⇒
     273          let 〈dst, src〉 ≝ dst_src in
     274        ! v ← hwreg_retrieve (regs st) src;
     275        ! regs ← hwreg_store dst v (regs st);
     276          ret ? 〈E0, goto l (set_regs regs st)〉
     277(* XXX: examine: where is the result being stored?
     278      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
     279        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     280        ! v1 ← Byte_of_val v1;
     281        ! v2 ← reg_retrieve (locals st) acc_b_reg;
     282        ! v2 ← Byte_of_val v2;
     283          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     284          let v1' ≝ val_of_Byte v1' in
     285          let v2' ≝ val_of_Byte v2' in
     286        ! locals ← reg_store dacc v1' (locals st);
     287        ! locals ← reg_store dbacc v2' locals;
     288          ret ? 〈E0, goto l (set_locals locals st)〉
     289*)
     290      | joint_instr_pop dst ⇒
     291        ! 〈st,v〉 ← pop st;
     292        ! locals ← reg_store dst (val_of_Byte v) (locals st);
     293          ret ? 〈E0, goto l (set_locals locals st)〉
     294      | joint_instr_push src ⇒
     295        ! v ← reg_retrieve (locals st) src;
     296        ! v ← Byte_of_val v;
     297        ! st ← push st v;
     298          ret ? 〈E0, goto l st〉
     299      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     300        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     301        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     302          match fd with
     303          [ Internal fn ⇒
     304            ! st ← save_ra st l;
     305              let st ≝ save_frame st in
     306              let locals ≝ init_locals (ertl_if_locals fn) in
     307              let l' ≝ ertl_if_entry fn in
     308              ret ? 〈 E0, goto l' (set_locals locals st)〉
     309          | External fn ⇒
     310            ! params ← fetch_external_args fn st;
     311            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     312            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     313            (* CSC: XXX bug here; I think I should split it into Byte-long
     314               components; instead I am making a singleton out of it *)
     315              let vs ≝ [mk_val ? evres] in
     316            ! st ← set_result vs st;
     317              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     318      ]
     319      | _ ⇒ ?
     320      ]
     321    | joint_st_return ⇒
     322      ! st ← pop_frame st;
     323      ! 〈st,pch〉 ← pop st;
     324      ! 〈st,pcl〉 ← pop st;
     325        let pc ≝ address_of_address_chunks pcl pch in
     326        ret ? 〈E0,set_pc pc st〉
     327    | _ ⇒ ?
     328    ]
    291329  | ertl_st_get_hdw dst src l ⇒
    292330     ! v ← hwreg_retrieve (regs st) src;
     
    297335     ! regs ← hwreg_store dst v (regs st);
    298336     ret ? 〈E0, goto l (set_regs regs st)〉
     337  | ertl_st_new_frame _ ⇒ ?
     338  | ertl_st_del_frame _ ⇒ ?
     339  | ertl_st_frame_size _ _ ⇒ ?
     340  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
     341         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
     342         be more than enough... *)
     343  | ertl_st_move dst src l ⇒
     344     ! v ← reg_retrieve (locals st) src;
     345     ! locals ← reg_store dst v (locals st);
     346     ret ? 〈E0, goto l (set_locals locals st)〉
     347  ].
     348 
     349 
     350  match s with
    299351
    300352  (* CSC: Dropped:
     
    304356     
    305357  (* CSC: changed, where the meat is *)
    306   | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    307       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    308       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    309       match fd with
    310       [ Internal fn ⇒
    311         ! st ← save_ra st l;
    312         let st ≝ save_frame st in
    313         let locals ≝ init_locals (ertl_if_locals fn) in
    314         let l' ≝ ertl_if_entry fn in
    315          ret ? 〈 E0, goto l' (set_locals locals st)〉
    316       | External fn ⇒
    317         ! params ← fetch_external_args fn st;
    318         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    319         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    320         (* CSC: XXX bug here; I think I should split it into Byte-long
    321            components; instead I am making a singleton out of it *)
    322         let vs ≝ [mk_val ? evres] in
    323         ! st ← set_result vs st;
    324         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    325       ]
    326   | ertl_st_return ⇒
    327       ! st ← pop_frame st;
    328       ! 〈st,pch〉 ← pop st;
    329       ! 〈st,pcl〉 ← pop st;
    330       let pc ≝ address_of_address_chunks pcl pch in
    331       ret ? 〈E0,set_pc pc st〉
    332358 
    333359  (* CSC: new stuff *)
    334360  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    335   | ertl_st_new_frame l ⇒
    336      ! v ← framesize st;
    337      ! sp ← get_hwsp st;
    338      let newsp ≝ addr_sub sp v in
    339      ! st ← set_hwsp newsp st;
    340      ret ? 〈E0,goto l st〉
    341   | ertl_st_del_frame l ⇒
    342      ! v ← framesize st;
    343      ! sp ← get_hwsp st;
    344      let newsp ≝ addr_add sp v in
    345      ! st ← set_hwsp newsp st;
    346      ret ? 〈E0,goto l st〉
    347   | ertl_st_frame_size dst l ⇒
    348      ! v ← framesize st;
    349      ! locals ← reg_store dst (val_of_nat v) (locals st);
    350      ret ? 〈E0, goto l (set_locals locals st)〉
    351   | ertl_st_pop dst l ⇒
    352      ! 〈st,v〉 ← pop st;
    353      ! locals ← reg_store dst (val_of_Byte v) (locals st);
    354      ret ? 〈E0, goto l (set_locals locals st)〉
    355   | ertl_st_push src l ⇒
    356      ! v ← reg_retrieve (locals st) src;
    357      ! v ← Byte_of_val v;
    358      ! st ← push st v;
    359      ret ? 〈E0, goto l st〉
    360   ].
     361<<<<<<< .mine  ].
    361362
    362363axiom WrongReturnValueType: String.
  • src/LIN/JointLTLLIN.ma

    r1132 r1161  
    66include "common/Registers.ma".
    77
    8 inductive joint_instruction (globals: list ident): Type[0] ≝
    9   | joint_instr_comment: String → joint_instruction globals
    10   | joint_instr_cost_label: costlabel → joint_instruction globals
    11   | joint_instr_int: Register → Byte → joint_instruction globals
    12   | joint_instr_pop: joint_instruction globals
    13   | joint_instr_push: joint_instruction globals
    14   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
    15   | joint_instr_from_acc: Register → joint_instruction globals
    16   | joint_instr_to_acc: Register → joint_instruction globals
    17   | joint_instr_opaccs: OpAccs → joint_instruction globals
    18   | joint_instr_op1: Op1 → joint_instruction globals
    19   | joint_instr_op2: Op2 → Register → joint_instruction globals
    20   | joint_instr_clear_carry: joint_instruction globals
    21   | joint_instr_set_carry: joint_instruction globals
    22   | joint_instr_load: joint_instruction globals
    23   | joint_instr_store: joint_instruction globals
    24   | joint_instr_call_id: ident → joint_instruction globals
    25   | joint_instr_cond_acc: label → joint_instruction globals.
     8inductive joint_instruction
     9  (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
     10  (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0])
     11  (pair_reg: Type[0]): Type[0] ≝
     12  | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     13  | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     14  | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     15  | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     16  | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     17  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     18  | joint_instr_hdw_to_hdw: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     19  | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     20  | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     21  | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     22  | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     23  | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     24  | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     25  | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     26  | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     27  | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
    2628
    27 inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
    28   | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
    29   | joint_st_goto: label → joint_statement A globals
    30   | joint_st_return: joint_statement A globals.
     29inductive joint_statement
     30  (A: Type[0]) (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
     31  (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0]) (pair_reg: Type[0]): Type[0] ≝
     32  | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     33  | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     34  | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
  • src/LTL/LTL.ma

    r1132 r1161  
    33include "LIN/LIN.ma".
    44
    5 definition ltl_statement ≝ joint_statement label.
     5definition ltl_statement ≝
     6  λglobals.
     7    joint_statement label globals .
    68 
    79definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.