99 open Hints_declaration
127 (** val mk_trans_system_of_abstract_status :
128 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
129 (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
130 let mk_trans_system_of_abstract_status s as_eval =
131 { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
132 SmallstepExec.step = (fun x status ->
134 match StructuredTraces.as_label s status with
135 | Types.None -> Events.e0
136 | Types.Some cst -> Events.echarge cst
139 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (as_eval status)
141 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = tr;
142 Types.snd = status' }))) }
144 (** val mk_fullexec_of_abstract_status :
145 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
146 __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
147 let mk_fullexec_of_abstract_status s as_eval as_init =
148 { SmallstepExec.es1 = (mk_trans_system_of_abstract_status s as_eval);
149 SmallstepExec.make_global = (fun x -> Obj.magic Types.It);
150 SmallstepExec.make_initial_state = (fun x ->
151 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) as_init)) }
153 (** val mk_preclassified_system_of_abstract_status :
154 StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
155 __ -> Measurable.preclassified_system **)
156 let mk_preclassified_system_of_abstract_status s as_eval as_init =
157 { Measurable.pcs_exec = (mk_fullexec_of_abstract_status s as_eval as_init);
158 Measurable.pcs_labelled = (fun x st ->
159 Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
160 Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
161 Measurable.pcs_callee = (fun x st _ ->
162 s.StructuredTraces.as_call_ident st) }
164 (** val oC_preclassified_system :
165 ASM.labelled_object_code -> Measurable.preclassified_system **)
166 let oC_preclassified_system c =
167 mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
169 Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
170 (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
171 (Obj.magic (Status.initialise_status c.ASM.cm))
175 (** val execute_1_pseudo_instruction' :
176 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
177 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
178 -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
179 Status.pseudoStatus **)
180 let execute_1_pseudo_instruction' cm addr_of_label addr_of_symbol sigma policy status =
181 Interpret.execute_1_pseudo_instruction cm (fun x _ ->
182 Assembly.ticks_of cm addr_of_label sigma policy x) addr_of_label
183 addr_of_symbol status
185 (** val classify_pseudo_instruction :
186 ASM.pseudo_instruction -> StructuredTraces.status_class **)
187 let classify_pseudo_instruction = function
188 | ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
189 | ASM.Comment x -> StructuredTraces.Cl_other
190 | ASM.Cost x -> StructuredTraces.Cl_other
191 | ASM.Jmp x -> StructuredTraces.Cl_other
192 | ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
193 | ASM.Call x -> StructuredTraces.Cl_call
194 | ASM.Mov (x, x0, x1) -> StructuredTraces.Cl_other
196 (** val aSM_classify :
197 ASM.pseudo_assembly_program -> Status.pseudoStatus ->
198 StructuredTraces.status_class **)
199 let aSM_classify cm s =
200 classify_pseudo_instruction
201 (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
203 (** val aSM_as_label_of_pc :
204 ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
206 let aSM_as_label_of_pc prog pc =
207 match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
208 | ASM.Instruction x -> Types.None
209 | ASM.Comment x -> Types.None
210 | ASM.Cost label -> Types.Some label
211 | ASM.Jmp x -> Types.None
212 | ASM.Jnz (x, x0, x1) -> Types.None
213 | ASM.Call x -> Types.None
214 | ASM.Mov (x, x0, x1) -> Types.None
216 (** val aSM_as_result :
217 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
218 Status.pseudoStatus -> Integers.int Types.option **)
219 let aSM_as_result prog addr_of_labels st =
220 let finaladdr = addr_of_labels prog.ASM.final_label in
221 ASMCosts.as_result_of_finaladdr prog st finaladdr
225 (** val aSM_as_call_ident :
226 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
227 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
228 -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
230 let aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy s0 =
232 execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol sigma
233 policy (Types.pi1 s0)
235 let { Types.fst = lbl; Types.snd = instr } =
237 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
238 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
239 Nat.O)))))))))))))))) st.Status.program_counter) prog.ASM.code
242 | Types.None -> assert false (* absurd case *)
244 (match AssocList.assoc_list_lookup lbl'
245 (Identifiers.eq_identifier PreIdentifiers.ASMTag)
246 prog.ASM.renamed_symbols with
247 | Types.None -> assert false (* absurd case *)
248 | Types.Some id -> id))
250 (** val aSM_abstract_status :
251 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
252 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
253 -> (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
254 let aSM_abstract_status prog addr_of_label addr_of_symbol sigma policy =
255 { StructuredTraces.as_pc = AbstractStatus.word_deqset;
256 StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
257 StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
258 StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
259 StructuredTraces.as_result =
260 (Obj.magic (aSM_as_result prog addr_of_label));
261 StructuredTraces.as_call_ident =
263 (aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy));
264 StructuredTraces.as_tailcall_ident = (fun clearme ->
266 (match (ASM.fetch_pseudo_instruction prog.ASM.code
267 (Obj.magic st).Status.program_counter).Types.fst with
268 | ASM.Instruction clearme0 ->
272 Obj.magic StructuredTraces.status_class_discr
273 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
276 Obj.magic StructuredTraces.status_class_discr
277 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
280 Obj.magic StructuredTraces.status_class_discr
281 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
284 Obj.magic StructuredTraces.status_class_discr
285 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
288 Obj.magic StructuredTraces.status_class_discr
289 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
292 Obj.magic StructuredTraces.status_class_discr
293 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
296 Obj.magic StructuredTraces.status_class_discr
297 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
300 Obj.magic StructuredTraces.status_class_discr
301 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
304 Obj.magic StructuredTraces.status_class_discr
305 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
308 Obj.magic StructuredTraces.status_class_discr
309 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
312 Obj.magic StructuredTraces.status_class_discr
313 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
316 Obj.magic StructuredTraces.status_class_discr
317 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
320 Obj.magic StructuredTraces.status_class_discr
321 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
324 Obj.magic StructuredTraces.status_class_discr
325 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
328 Obj.magic StructuredTraces.status_class_discr
329 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
332 Obj.magic StructuredTraces.status_class_discr
333 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
336 Obj.magic StructuredTraces.status_class_discr
337 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
340 Obj.magic StructuredTraces.status_class_discr
341 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
344 Obj.magic StructuredTraces.status_class_discr
345 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
348 Obj.magic StructuredTraces.status_class_discr
349 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
352 Obj.magic StructuredTraces.status_class_discr
353 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
356 Obj.magic StructuredTraces.status_class_discr
357 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
360 Obj.magic StructuredTraces.status_class_discr
361 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
364 Obj.magic StructuredTraces.status_class_discr
365 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
368 Obj.magic StructuredTraces.status_class_discr
369 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
372 Obj.magic StructuredTraces.status_class_discr
373 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
376 Obj.magic StructuredTraces.status_class_discr
377 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
380 Obj.magic StructuredTraces.status_class_discr
381 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
384 Obj.magic StructuredTraces.status_class_discr
385 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
388 Obj.magic StructuredTraces.status_class_discr
389 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
392 Obj.magic StructuredTraces.status_class_discr
393 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
396 Obj.magic StructuredTraces.status_class_discr
397 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
400 Obj.magic StructuredTraces.status_class_discr
401 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
404 Obj.magic StructuredTraces.status_class_discr
405 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
408 Obj.magic StructuredTraces.status_class_discr
409 StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
412 Obj.magic StructuredTraces.status_class_discr
413 StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
416 Obj.magic StructuredTraces.status_class_discr
417 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
420 Obj.magic StructuredTraces.status_class_discr
421 StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
424 Obj.magic StructuredTraces.status_class_discr
425 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
428 Obj.magic StructuredTraces.status_class_discr
429 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
432 Obj.magic StructuredTraces.status_class_discr
433 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
434 | ASM.Jnz (x, y, abs) ->
436 Obj.magic StructuredTraces.status_class_discr
437 StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
440 Obj.magic StructuredTraces.status_class_discr
441 StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
442 | ASM.Mov (x, y, abs) ->
444 Obj.magic StructuredTraces.status_class_discr
445 StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
447 (** val aSM_preclassified_system :
448 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
449 (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
450 let aSM_preclassified_system c sigma policy =
451 let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
452 let symbol_map = Status.construct_datalabels c.ASM.preamble in
453 let addr_of_label = fun x ->
454 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456 Nat.O))))))))))))))))
457 (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
459 let addr_of_symbol = fun x ->
460 Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
463 mk_preclassified_system_of_abstract_status
464 (aSM_abstract_status c addr_of_label addr_of_symbol sigma policy)
466 Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
467 (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
468 policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
471 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
472 (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
473 let aSM_status c sigma policy =
474 let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
475 let symbol_map = Status.construct_datalabels c.ASM.preamble in
476 let addr_of_label = fun x ->
477 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
478 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
479 Nat.O))))))))))))))))
480 (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
482 let addr_of_symbol = fun x ->
483 Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
486 aSM_abstract_status c addr_of_label addr_of_symbol sigma policy