source: src/joint/Traces.ma @ 2443

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

changed joint's stack pointer and internal stack

File size: 5.7 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.
40
41definition make_initial_state :
42 ∀pars: prog_params.res (state_pc pars) ≝
43λpars.let p ≝ prog pars in
44  let sem_globals : evaluation_params ≝ pars in
45  let ge ≝ ev_genv sem_globals in
46  let m ≝ alloc_mem … p in
47  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
48  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
49  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
50  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
51(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
52  let main ≝ prog_main … p in
53  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
54  let st0' ≝ set_sp … spp st0 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 spb normalize //
67  ]
68qed.
69
70definition step_flow_classifier :
71  ∀p : evaluation_params.∀F,flows.
72  step_flow p F flows → status_class ≝
73  λp,F,flows,flow.match flow with
74  [ Redirect _ _ ⇒ cl_jump
75  | Init bl _ _ _ ⇒
76    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
77    [ Some f ⇒ cl_call
78    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
79    ]
80  | Proceed flows ⇒
81    match flows with
82    [ Labels lbls ⇒
83      match lbls with
84      [ nil ⇒ cl_other
85      | _ ⇒ cl_jump
86      ]
87    | _ ⇒ cl_other
88    ]
89  ].
90
91definition fin_step_flow_classifier :
92  ∀p : evaluation_params.∀F,flows.
93  fin_step_flow p F flows → status_class ≝
94  λp,F,flows,flow.match flow with
95  [ FRedirect lbls _ ⇒
96    match lbls with
97    [ nil ⇒ (* not really possible, we don't care *) cl_other
98    | cons _ tl ⇒
99      match tl with
100      [ nil ⇒ (* only one label *) cl_other
101      | _ ⇒ (* fork *) cl_jump
102      ]
103    ]
104  | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
105    cl_other
106  | _ ⇒ cl_return
107  ].
108
109definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
110*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
111[ #EQ destruct % #H %
112| * #NEQ % #ABS destruct elim (NEQ ?) %
113]
114qed.
115
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*)
126
127definition cost_label_of_stmt :
128  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
129  λp,s.match s with
130  [ sequential s _ ⇒
131    match s with
132    [ step_seq s ⇒
133      match s with
134      [ COST_LABEL lbl ⇒ Some ? lbl
135      | _ ⇒ None ?
136      ]
137    | _ ⇒ None ?
138    ]
139  | _ ⇒ None ?
140  ].
141
142definition joint_abstract_status :
143 ∀p : evaluation_params.
144 abstract_status ≝
145 λp.
146 mk_abstract_status
147   (* as_status ≝ *) (state_pc p)
148   (* as_execute ≝ *)
149    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
150   (* as_pc ≝ *) cpointerDeq
151   (* as_pc_of ≝ *) (pc …)
152   (* as_classify ≝ *)
153    (λs.
154      match (
155        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
156        match stmt with
157        [ sequential stp nxt ⇒
158          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
159          return step_flow_classifier … flow
160        | final stp ⇒
161          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
162          return fin_step_flow_classifier … flow
163        ]) with
164      [ Value c ⇒ c
165      | _ ⇒ cl_other
166      ])
167   (* as_label_of_pc ≝ *)
168    (λpc.
169      match fetch_statement ? p … (ev_genv p) pc with
170      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
171      | _ ⇒ None ?
172      ])
173   (* as_after_return ≝ *)
174    (λs1,s2.
175      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
176      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
177      succ_pc p p (pc … s1) nxt = return pc … s2)
178   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
179   (* as_call_ident_≝ *)
180   (λst.?). cases daemon (* TODO *) qed.
Note: See TracBrowser for help on using the repository browser.