source: src/joint/Traces.ma @ 2442

Last change on this file since 2442 was 2442, checked in by piccolo, 8 years ago

Traces repaired. (By Paolo)
Statement of lineariseProof in place.

File size: 5.6 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 …) spp ispp (BBbit false) (empty_regsT … spp) m in
54  (* use exit sem_globals as ra and call_dest_for_main as dest *)
55  ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
56  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
57  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
58  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
59  match main_fd with
60  [ Internal fn ⇒
61    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
62  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
63  ].
64  [ %
65  | cases ispb
66  | cases spb
67  ] normalize //
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
116let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
117  match c with
118  [ Value x ⇒ OK … x
119  | Interact o f ⇒
120    ! i ← env o ;
121    io_evaluate O I X env (f i)
122  | Wrong e ⇒ Error … e
123  ].
124
125definition cost_label_of_stmt :
126  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
127  λp,s.match s with
128  [ sequential s _ ⇒
129    match s with
130    [ step_seq s ⇒
131      match s with
132      [ COST_LABEL lbl ⇒ Some ? lbl
133      | _ ⇒ None ?
134      ]
135    | _ ⇒ None ?
136    ]
137  | _ ⇒ None ?
138  ].
139
140definition joint_abstract_status :
141 ∀p : evaluation_params.
142 abstract_status ≝
143 λp.
144 mk_abstract_status
145   (* as_status ≝ *) (state_pc p)
146   (* as_execute ≝ *)
147    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
148   (* as_pc ≝ *) cpointerDeq
149   (* as_pc_of ≝ *) (pc …)
150   (* as_classify ≝ *)
151    (λs.
152      match (
153        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
154        match stmt with
155        [ sequential stp nxt ⇒
156          ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
157          return step_flow_classifier … flow
158        | final stp ⇒
159          ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
160          return fin_step_flow_classifier … flow
161        ]) with
162      [ OK c ⇒ c
163      | Error _ ⇒ cl_other
164      ])
165   (* as_label_of_pc ≝ *)
166    (λpc.
167      match fetch_statement ? p … (ev_genv p) pc with
168      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
169      | _ ⇒ None ?
170      ])
171   (* as_after_return ≝ *)
172    (λs1,s2.
173      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
174      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
175      succ_pc p p (pc … s1) nxt = return pc … s2)
176   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
177   (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
Note: See TracBrowser for help on using the repository browser.