source: src/joint/Traces.ma @ 2422

Last change on this file since 2422 was 2422, checked in by tranquil, 8 years ago

adapted joint to cl_call f

File size: 5.5 KB
Line 
1include "joint/semantics.ma".
2include "common/StructuredTraces.ma".
3
4record evaluation_params : Type[1] ≝
5 { globals: list ident
6 ; sparams:> sem_params
7 ; exit: cpointer
8 ; ev_genv: genv sparams globals
9 ; io_env : state sparams → ∀o:io_out.res (io_in o)
10 }.
11 
12record prog_params : Type[1] ≝
13 { prog_spars : sem_params
14 ; prog : joint_program prog_spars
15 ; prog_io : state prog_spars → ∀o.res (io_in o)
16 }.
17
18definition make_global : prog_params → evaluation_params
19
20λpars.
21(* Invariant: a -1 block is unused in common/Globalenvs *)
22let b ≝ mk_block Code (-1) in
23let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
24let p ≝ prog pars in
25mk_evaluation_params
26  (prog_var_names … p)
27  (prog_spars pars)
28  «ptr, refl …»
29  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
30  (prog_io pars).
31(* TODO or TOBEFOUND *)
32cases daemon
33qed.
34
35coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
36≝ make_global on _p : prog_params to evaluation_params.
37
38
39axiom ExternalMain : String.
40check save_frame
41
42definition make_initial_state :
43 ∀pars: prog_params.res (state_pc pars) ≝
44λpars.let p ≝ prog pars in
45  let sem_globals : evaluation_params ≝ pars in
46  let ge ≝ ev_genv sem_globals in
47  let m ≝ alloc_mem … p in
48  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
49  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
50  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
51  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
52  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
53  let main ≝ prog_main … p in
54  let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
55  (* use exit sem_globals as ra and call_dest_for_main as dest *)
56  ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
57  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
58  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
59  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
60  match main_fd with
61  [ Internal fn ⇒
62    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
63  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
64  ].
65  [ %
66  | cases ispb
67  | cases spb
68  ] normalize //
69qed.
70
71definition step_flow_classifier :
72  ∀p : evaluation_params.∀F,flows.
73  step_flow p F flows → status_class ≝
74  λp,F,flows,flow.match flow with
75  [ Redirect _ _ ⇒ cl_jump
76  | Init bl _ _ _ ⇒
77    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
78    [ Some f ⇒ cl_call f
79    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
80    ]
81  | Proceed flows ⇒
82    match flows with
83    [ Labels lbls ⇒
84      match lbls with
85      [ nil ⇒ cl_other
86      | _ ⇒ cl_jump
87      ]
88    | _ ⇒ cl_other
89    ]
90  ].
91
92definition fin_step_flow_classifier :
93  ∀p : evaluation_params.∀F,flows.
94  fin_step_flow p F flows → status_class ≝
95  λp,F,flows,flow.match flow with
96  [ FRedirect lbls _ ⇒
97    match lbls with
98    [ nil ⇒ (* not really possible, we don't care *) cl_other
99    | cons _ tl ⇒
100      match tl with
101      [ nil ⇒ (* only one label *) cl_other
102      | _ ⇒ (* fork *) cl_jump
103      ]
104    ]
105  | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
106    cl_other
107  | _ ⇒ cl_return
108  ].
109
110definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
111*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
112[ #EQ destruct % #H %
113| * #NEQ % #ABS destruct elim (NEQ ?) %
114]
115qed.
116
117let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
118  match c with
119  [ Value x ⇒ OK … x
120  | Interact o f ⇒
121    ! i ← env o ;
122    io_evaluate O I X env (f i)
123  | Wrong e ⇒ Error … e
124  ].
125
126definition cost_label_of_stmt :
127  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
128  λp,s.match s with
129  [ sequential s _ ⇒
130    match s with
131    [ step_seq s ⇒
132      match s with
133      [ COST_LABEL lbl ⇒ Some ? lbl
134      | _ ⇒ None ?
135      ]
136    | _ ⇒ None ?
137    ]
138  | _ ⇒ None ?
139  ].
140
141definition joint_abstract_status :
142 ∀p : evaluation_params.
143 abstract_status ≝
144 λp.
145 mk_abstract_status
146   (* as_status ≝ *) (state_pc p)
147   (* as_execute ≝ *)
148    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
149   (* as_pc ≝ *) cpointerDeq
150   (* as_pc_of ≝ *) (pc …)
151   (* as_classifier ≝ *)
152    (λs,cl.∃fn,stmt.
153      fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
154      match stmt with
155      [ sequential stp nxt ⇒
156        ∃flow,s'.
157        io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) = return 〈flow, s'〉 ∧
158        step_flow_classifier … flow = cl
159      | final stp ⇒
160        ∃flow.io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) = return flow ∧
161        fin_step_flow_classifier … flow = cl
162      ])
163   (* as_label_of_pc ≝ *)
164    (λpc.
165      match fetch_statement ? p … (ev_genv p) pc with
166      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
167      | _ ⇒ None ?
168      ])
169   (* as_after_return ≝ *)
170    (λs1,s2.
171      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
172      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
173      succ_pc p p (pc … s1) nxt = return pc … s2)
174   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
Note: See TracBrowser for help on using the repository browser.