source: src/joint/semantics.ma @ 1385

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