source: src/joint/semantics.ma @ 1303

Last change on this file since 1303 was 1303, checked in by sacerdot, 8 years ago
  1. LTL/semantics.ma added (work in progress)
  2. init_locals fixed to take in input the old register environment, since physical registers should just be left untouched
File size: 15.6 KB
RevLine 
[1173]1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint.ma".
[1213]6include "joint/BEMem.ma".
7
[1173]8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
[1213]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).
[1215]18
[1289]19record more_sem_params (p:params_): Type[1] ≝
[1233]20 { framesT: Type[0]
[1281]21 ; regsT: Type[0]
[1233]22
23 ; succ_pc: succ p → address → address
[1173]24 ; pop_frame_: framesT → res framesT
[1174]25 ; save_frame_: framesT → regsT → framesT
[1213]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
[1294]36 ; pair_reg_move_: regsT → pair_reg p → res regsT
[1186]37 
[1217]38 ; pointer_of_label: label → Σp:pointer. ptype p = Code
[1173]39 }.
40
[1233]41record sem_params: Type[1] ≝
[1247]42 { spp :> params_
[1233]43 ; more_sem_pars :> more_sem_params spp
44 }.
[1217]45
[1173]46record state (p: sem_params): Type[0] ≝
[1233]47 { st_frms: framesT ? p
[1173]48 ; pc: address
[1215]49 ; sp: pointer
[1213]50 ; carry: beval
[1233]51 ; regs: regsT ? p
[1213]52 ; m: bemem
[1173]53 }.
54
[1247]55definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
[1176]56
[1247]57record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
[1233]58 { more_sparams:> more_sem_params p
[1289]59
[1303]60 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
[1186]61 
[1298]62 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
[1294]63 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
64
[1233]65 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
66 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
[1186]67
[1247]68 ; 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)))
[1176]69 }.
70
[1233]71record sem_params2 (globals: list ident): Type[1] ≝
[1247]72 { p2:> params globals
73 ; more_sparams2:> more_sem_params2 globals p2
[1233]74 }.
75
76definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
77coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
78 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
[1247]79(*
[1233]80unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
81   S ≟ sem_params_of_sem_params2 globals p
82(* ---------------------------------------- *) ⊢
83   pars_ (spp (mk_sem_params (p2 globals p)
84    (more_sparams (p2 globals p) globals
85    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
[1247]86*)
[1233]87definition address_of_label: sem_params → label → address.
88 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
89 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
90  [ #res #_ @res
91  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
92qed.
93
[1213]94definition set_m: ∀p. bemem → state p → state p ≝
[1173]95 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
96
[1233]97definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
[1173]98 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
99
[1215]100definition set_sp: ∀p. pointer → state p → state p ≝
[1173]101 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
102
[1213]103definition set_carry: ∀p. beval → state p → state p ≝
[1174]104 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
[1173]105
106definition set_pc: ∀p. address → state p → state p ≝
107 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
108
[1233]109definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
[1174]110 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
111
[1182]112definition goto: ∀p:sem_params. label → state p → state p ≝
[1217]113 λp,l,st. set_pc … (address_of_label p l) st.
[1173]114
[1233]115definition next: ∀p:sem_params. succ … p → state p → state p ≝
116 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
117
[1213]118definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
[1173]119 λp,dst,v,st.
[1213]120  do regs  ← greg_store_ … dst v (regs … st);
121  OK ? (set_regs … regs st).
[1173]122
[1213]123definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
[1173]124 λp,st,dst.greg_retrieve_ … (regs … st) dst.
125
[1213]126definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
[1173]127 λp,dst,v,st.
[1213]128  do regs ← acca_store_ … dst v (regs … st);
129  OK ? (set_regs … regs st).
[1173]130
[1213]131definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
[1173]132 λp,st,dst.acca_retrieve_ … (regs … st) dst.
133
[1213]134definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
[1173]135 λp,dst,v,st.
[1213]136  do regs ← accb_store_ … dst v (regs … st);
137  OK ? (set_regs … regs st).
[1173]138
[1213]139definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
[1173]140 λp,st,dst.accb_retrieve_ … (regs … st) dst.
141
[1213]142definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
[1173]143 λp,dst,v,st.
[1213]144  do regs ← dpl_store_ … dst v (regs … st);
145  OK ? (set_regs … regs st).
[1173]146
[1213]147definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
[1173]148 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
149
[1213]150definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
[1173]151 λp,dst,v,st.
[1213]152  do regs ← dph_store_ … dst v (regs … st);
153  OK ? (set_regs … regs st).
[1173]154
[1213]155definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
[1173]156 λp,st,dst.dph_retrieve_ … (regs … st) dst.
157
[1294]158definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
159 λp,st,rs.
160  do regs ← pair_reg_move_ … (regs … st) rs;
161  OK … (set_regs … regs st).
[1173]162
[1174]163definition save_frame: ∀p:sem_params. state p → state p ≝
[1233]164 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
[1173]165
166(* removes the top frame from the frames list *)
167definition pop_frame: ∀p. state p → res (state p) ≝
168 λp,st.
[1233]169  do frames ← pop_frame_ … p (st_frms … st);
[1213]170  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
[1173]171
172axiom FailedStore: String.
173
[1215]174definition push: ∀p. state p → beval → res (state p) ≝
[1173]175 λp,st,v.
[1215]176  let sp ≝ sp … st in
177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
178  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
179  OK … (set_m … m (set_sp … sp st)).
[1173]180
[1215]181definition pop: ∀p. state p → res (state p × beval) ≝
[1173]182 λp,st.
[1215]183  let sp ≝ sp ? st in
184  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
185  let st ≝ set_sp … sp st in
186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
187  OK ? 〈st,v〉.
[1173]188
[1233]189definition save_ra : ∀p. state p → succ p → res (state p) ≝
[1174]190 λp,st,l.
[1233]191  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
[1214]192  do st ← push … st addrl;
193  push … st addrh.
[1173]194
[1213]195definition fetch_ra : ∀p.state p → res (state p × address) ≝
[1176]196 λp,st.
[1214]197  do 〈st,addrh〉 ← pop … st;
198  do 〈st,addrl〉 ← pop … st;
199  OK ? 〈st, 〈addrl,addrh〉〉.
[1176]200
[1173]201axiom MissingSymbol : String.
202axiom FailedLoad : String.
203axiom BadFunction : String.
204
[1247]205definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
[1233]206 λglobals,p,ge,st.
[1298]207  ! s ← fetch_statement … ge st;
[1173]208  match s with
[1289]209    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
210    | sequential seq l ⇒
[1173]211      match seq with
[1289]212      [ extension c ⇒ exec_extended … p ge c st
213      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
214      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
215      | INT dest v ⇒
216        ! st ← greg_store p dest (BVByte v) st;
[1233]217          ret ? 〈E0, next … l st〉
[1289]218      | LOAD dst addrl addrh ⇒
[1173]219        ! vaddrh ← dph_retrieve … st addrh;
220        ! vaddrl ← dpl_retrieve … st addrl;
[1213]221        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
222        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
[1289]223        ! st ← acca_store p … dst v st;
[1233]224          ret ? 〈E0, next … l st〉
[1289]225      | STORE addrl addrh src ⇒
[1174]226        ! vaddrh ← dph_retrieve … st addrh;
227        ! vaddrl ← dpl_retrieve … st addrl;
[1213]228        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
[1174]229        ! v ← acca_retrieve … st src;
[1213]230        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
[1233]231          ret ? 〈E0, next … l (set_m … m' st)〉
[1289]232      | COND src ltrue ⇒
[1174]233        ! v ← acca_retrieve … st src;
[1213]234        ! b ← bool_of_beval v;
[1233]235          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
[1289]236      | ADDRESS ident prf ldest hdest ⇒
[1173]237        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
[1213]238        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
[1289]239        ! st ← dpl_store p ldest laddr st;
240        ! st ← dph_store p hdest haddr st;
[1233]241          ret ? 〈E0, next … l st〉
[1289]242      | OP1 op dacc_a sacc_a ⇒
243        ! v ← acca_retrieve … st sacc_a;
[1173]244        ! v ← Byte_of_val v;
[1213]245          let v' ≝ BVByte (op1 eval op v) in
[1289]246        ! st ← acca_store p dacc_a v' st;
[1233]247          ret ? 〈E0, next … l st〉
[1289]248      | OP2 op dacc_a sacc_a src ⇒
249        ! v1 ← acca_retrieve … st sacc_a;
[1173]250        ! v1 ← Byte_of_val v1;
[1176]251        ! v2 ← greg_retrieve … st src;
[1173]252        ! v2 ← Byte_of_val v2;
[1213]253        ! carry ← bool_of_beval (carry … st);
[1173]254          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
[1213]255          let v' ≝ BVByte v' in
256          let carry ≝ beval_of_bool carry in
[1289]257        ! st ← acca_store p dacc_a v' st;
[1233]258          ret ? 〈E0, next … l (set_carry … carry st)〉
[1289]259      | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
260      | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
261      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
262        ! v1 ← acca_retrieve … st sacc_a_reg;
[1173]263        ! v1 ← Byte_of_val v1;
[1289]264        ! v2 ← accb_retrieve … st sacc_b_reg;
[1173]265        ! v2 ← Byte_of_val v2;
266          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
[1213]267          let v1' ≝ BVByte v1' in
268          let v2' ≝ BVByte v2' in
[1289]269        ! st ← acca_store p dacc_a_reg v1' st;
270        ! st ← accb_store p dacc_b_reg v2' st;
[1233]271          ret ? 〈E0, next … l st〉
[1289]272      | POP dst ⇒
[1174]273        ! 〈st,v〉 ← pop … st;
[1289]274        ! st ← acca_store p dst v st;
[1233]275          ret ? 〈E0, next … l st〉
[1289]276      | PUSH src ⇒
[1174]277        ! v ← acca_retrieve … st src;
278        ! st ← push … st v;
[1233]279          ret ? 〈E0, next … l st〉
[1289]280      | MOVE dst_src ⇒
[1294]281        ! st ← pair_reg_move … st dst_src ;
282          ret ? 〈E0, next … l st〉
[1289]283      (*CSC: XXX bug here dest unused *)
284      | CALL_ID id argsno dest ⇒
[1173]285        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
286        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
287          match fd with
288          [ Internal fn ⇒
[1176]289            ! st ← save_ra … st l;
[1174]290              let st ≝ save_frame … st in
[1303]291              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
[1176]292              let l' ≝ joint_if_entry … fn in
[1289]293             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
[1173]294          | External fn ⇒
[1176]295            ! params ← fetch_external_args … fn st;
[1173]296            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
297            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
298            (* CSC: XXX bug here; I think I should split it into Byte-long
299               components; instead I am making a singleton out of it *)
300              let vs ≝ [mk_val ? evres] in
[1176]301            ! st ← set_result … vs st;
[1233]302              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
[1217]303          ]]
[1289]304    | RETURN ⇒
[1173]305      ! st ← pop_frame … st;
306      ! 〈st,pch〉 ← pop … st;
307      ! 〈st,pcl〉 ← pop … st;
[1289]308        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
[1213]309cases addr //
310qed.
[1173]311
[1298]312definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → nat → state p → option int ≝
313 λglobals,p,ge,exit,registersno,st.res_to_opt … (
314  do s ← fetch_statement … ge st;
[1214]315  match s with
[1289]316   [ RETURN ⇒
[1214]317      do 〈st,l〉 ← fetch_ra … st;
318      if eq_address l exit then
[1233]319       do val ← fetch_result … st registersno;
[1214]320       match val with
321        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
322        | _ ⇒ Error ? []]
323      else
324       Error ? []
325   | _ ⇒ Error ? []]).
[1173]326
[1233]327record evaluation_parameters : Type[1] ≝
328 { globals: list ident
329 ; sparams2: sem_params2 globals
330 ; exit: address
331 ; registersno: nat
[1247]332 ; genv2: genv globals sparams2
[1233]333 }.
[1173]334
[1233]335definition joint_exec: trans_system io_out io_in ≝
336  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
[1298]337   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G) (registersno G))
[1233]338   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
339
340definition make_global :
[1247]341 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
[1233]342  joint_program pars → evaluation_parameters
343
344 λpars,sparams.
345  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
[1247]346[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
[1233]347qed.
348
[1220]349definition make_initial_state :
[1247]350 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
351 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
[1233]352λpars,sparams,p.
353  let ge ≝ genv2 (make_global pars sparams p) in
[1220]354  do m ← init_mem Genv … (λx.[Init_space x]) p;
355  let main ≝ prog_main … p in
[1173]356  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
357  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
[1233]358  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
359cases daemon qed.
[1220]360(*
361RTL:
362 init_prog == init_mem
363 init_sp: inizializzare lo stack pointer
364 init_isp: inizializzare l'altro stack pointer
365 init_renv: inizializzare i registri fisici
366 init_main_call: chiamata di funzione
367   --- init_fun_call: cambia fra ERTL e LTL
368 change_carry: a 0
[1186]369*)
[1233]370
[1186]371definition joint_fullexec :
[1247]372 ∀pars:∀globals.params globals.
373 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
[1233]374 fullexec io_out io_in ≝
375 λpars,sparams.
[1294]376  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.