Changeset 1408


Ignore:
Timestamp:
Oct 19, 2011, 11:30:24 AM (9 years ago)
Author:
sacerdot
Message:
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
Location:
src
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1390 r1408  
    2121definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2222 mk_more_sem_params ertl_params_
    23   (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
     23  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
     24   〈empty_map …,empty_hw_register_env〉 0 it
     25   graph_succ_p
    2426   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2527    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1390 r1408  
    66 λsuccT,succ,pointer_of_label.
    77 mk_more_sem_params ?
    8   unit hw_register_env succ
     8  unit it hw_register_env empty_hw_register_env 0 it succ
    99   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    1010    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
  • src/LIN/semantics.ma

    r1383 r1408  
    55 λ_.λaddr. addr_add addr 1.
    66
     7(*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
    78axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
    89
    9 axiom NotFound: String.
     10(*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
     11axiom BadProgramCounter: String.
    1012axiom lin_fetch_statement:
    11  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝
    12  λglobals,ge,st.
    13   let pc ≝ pc … st in
    14  ?.
    15   let fn ≝ ? in
    16   opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)).
    17 *)
     13 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).
     14(* λglobals,ge,st.
     15  do p ← pointer_of_address (pc … st) ;
     16  let b ≝ pblock p in
     17  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     18  [ Internal def' ⇒
     19     let off ≝ poff p in
     20     opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off))
     21  | External _ ⇒ Error … [MSG BadProgramCounter]].*)
    1822
    1923definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
  • src/RTL/semantics.ma

    r1396 r1408  
    1414definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    1515 mk_more_sem_params rtl_params_
    16   (list frame) (register_env beval) graph_succ_p
     16  (list frame) [] (register_env beval) (empty_map …) [] [](*dummy*) graph_succ_p
    1717   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    1818    reg_store reg_retrieve reg_store reg_retrieve
  • src/RTLabs/RTLabsToRTL.ma

    r1358 r1408  
    439439  λdef: rtl_internal_function globals.
    440440  match op1 with
    441   [ Ocastint src_sign src_size
     441  [ Ocastint src_sign src_size _ _
    442442    let dest_size ≝ |destrs| * 8 in
    443443    let src_size ≝ bitsize_of_intsize src_size in
  • src/joint/SemanticUtils.ma

    r1395 r1408  
    1414
    1515axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
     16axiom empty_hw_register_env: hw_register_env.
    1617axiom hwreg_retrieve : hw_register_env → Register → res beval.
    1718axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
  • src/joint/semantics.ma

    r1395 r1408  
    11include "utilities/lists.ma".
    2 include "common/Globalenvs.ma".
     2include "joint/BEGlobalenvs.ma".
    33include "common/IO.ma".
    44include "common/SmallstepExec.ma".
    55include "joint/Joint.ma".
    6 include "joint/BEMem.ma".
    76
    87(* CSC: external functions never fail (??) and always return something of the
     
    1312record more_sem_params (p:params_): Type[1] ≝
    1413 { framesT: Type[0]
     14 ; empty_framesT: framesT
    1515 ; regsT: Type[0]
     16 ; empty_regsT: regsT
     17 ; call_args_for_main: call_args p
     18 ; call_dest_for_main: call_dest p
    1619
    1720 (*CSC: XXXX succ_pc and pointer_of_label deal with fetching; same for
     
    4851 }.
    4952
     53(*
     54definition empty_state: ∀p. more_sem_params p → state p ≝
     55 mk_state … (empty_framesT …)
     56*)
     57
    5058definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    5159
     
    185193axiom FailedLoad : String.
    186194axiom BadFunction : String.
    187 
     195axiom BadPointer : String.
     196
     197definition eval_call_block:
     198 ∀globals.∀p:sem_params2 globals. genv globals p → state p →
     199  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
     200 λglobals,p,ge,st,b,args,dest,ra.
     201  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
     202    match fd with
     203    [ Internal fn ⇒
     204      ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
     205      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     206      let l' ≝ joint_if_entry … fn in
     207       ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     208    | External fn ⇒
     209      ! params ← fetch_external_args … fn st;
     210      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     211      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     212      (* CSC: XXX bug here; I think I should split it into Byte-long
     213         components; instead I am making a singleton out of it. To be
     214         fixed once we fully implement external functions. *)
     215        let vs ≝ [mk_val ? evres] in
     216      ! st ← set_result … vs st;
     217      let st ≝ set_pc … ra st in
     218        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     219     ].
     220
     221definition eval_call_id:
     222 ∀globals.∀p:sem_params2 globals. genv globals p → state p →
     223  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
     224 λglobals,p,ge,st,id,args,dest,ra.
     225  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     226  eval_call_block … ge st b args dest ra.
     227 
    188228definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    189229 λglobals,p,ge,st.
     
    289329          ret ? 〈E0, st〉
    290330      | CALL_ID id args dest ⇒
    291         ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    292         ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    293           match fd with
    294           [ Internal fn ⇒
    295             ! l ← succ_pc … (more_sem_pars p) l (pc … st) ;
    296             ! st ← save_frame … l (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    297             let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    298             let l' ≝ joint_if_entry … fn in
    299              ret ? 〈 E0, goto … l' (set_regs p regs st)〉
    300           | External fn ⇒
    301             ! params ← fetch_external_args … fn st;
    302             ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    303             ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    304             (* CSC: XXX bug here; I think I should split it into Byte-long
    305                components; instead I am making a singleton out of it *)
    306               let vs ≝ [mk_val ? evres] in
    307             ! st ← set_result … vs st;
    308             ! st ← next … l st ;
    309               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    310           ]]
     331        ! ra ← succ_pc … (more_sem_pars p) l (pc … st) ;         
     332          eval_call_id … ge st id args dest ra ]
    311333    | RETURN ⇒
    312334      ! 〈st,ra〉 ← fetch_ra … st;
     
    351373 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    352374 let addr ≝ address_of_code_pointer ptr in
    353   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … (λx.[Init_space x]) p)).
     375  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … p)).
    354376% qed.
    355377
     378axiom ExternalMain: String.
    356379definition make_initial_state :
    357380 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    358381 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
    359382λpars,sparams,p.
    360   let ge ≝ genv2 (make_global pars sparams p) in
    361   do m ← init_mem Genv … (λx.[Init_space x]) p;
     383  let sem_globals ≝ make_global pars sparams p in
     384  let ge ≝ genv2 sem_globals in
     385  let m ≝ init_mem Genv … p in
     386  let dummy_pc ≝ 〈BVundef,BVundef〉 in
     387  let sp ≝ ? in
    362388  let main ≝ prog_main … p in
    363   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    364   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    365   ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
     389  let st0 ≝ mk_state … (empty_framesT …) dummy_pc sp BVfalse (empty_regsT …) m in
     390  let trace_state ≝
     391   eval_call_id … ge st0 main (call_args_for_main … (sparams2 …))
     392    (call_dest_for_main … (sparams2 …)) (exit sem_globals) in
     393  match trace_state with
     394  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
     395  | Wrong msg ⇒ Error … msg
     396  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     397  ].
    366398cases daemon qed.
    367399(*
Note: See TracChangeset for help on using the changeset viewer.