121 open MemoryInjections
243 open Hints_declaration
269 open Clight_classified_system
271 open Cminor_semantics
275 open Cminor_classified_system
277 open RTLabs_semantics
281 open RTLabs_classified_system
303 open Joint_LTL_LIN_semantics
311 type preclassified_system_pass =
312 Measurable.preclassified_system
313 (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
315 (** val preclassified_system_pass_rect_Type4 :
316 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
317 preclassified_system_pass -> 'a1 **)
318 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
319 let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
321 (** val preclassified_system_pass_rect_Type5 :
322 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
323 preclassified_system_pass -> 'a1 **)
324 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
325 let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
327 (** val preclassified_system_pass_rect_Type3 :
328 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
329 preclassified_system_pass -> 'a1 **)
330 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
331 let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
333 (** val preclassified_system_pass_rect_Type2 :
334 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
335 preclassified_system_pass -> 'a1 **)
336 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
337 let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
339 (** val preclassified_system_pass_rect_Type1 :
340 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
341 preclassified_system_pass -> 'a1 **)
342 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
343 let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
345 (** val preclassified_system_pass_rect_Type0 :
346 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
347 preclassified_system_pass -> 'a1 **)
348 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
349 let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
352 Compiler.pass -> preclassified_system_pass ->
353 Measurable.preclassified_system **)
354 let rec pcs_pcs p xxx =
357 (** val preclassified_system_pass_inv_rect_Type4 :
358 Compiler.pass -> preclassified_system_pass ->
359 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
360 let preclassified_system_pass_inv_rect_Type4 x1 hterm h1 =
361 let hcut = preclassified_system_pass_rect_Type4 x1 h1 hterm in hcut __
363 (** val preclassified_system_pass_inv_rect_Type3 :
364 Compiler.pass -> preclassified_system_pass ->
365 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
366 let preclassified_system_pass_inv_rect_Type3 x1 hterm h1 =
367 let hcut = preclassified_system_pass_rect_Type3 x1 h1 hterm in hcut __
369 (** val preclassified_system_pass_inv_rect_Type2 :
370 Compiler.pass -> preclassified_system_pass ->
371 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
372 let preclassified_system_pass_inv_rect_Type2 x1 hterm h1 =
373 let hcut = preclassified_system_pass_rect_Type2 x1 h1 hterm in hcut __
375 (** val preclassified_system_pass_inv_rect_Type1 :
376 Compiler.pass -> preclassified_system_pass ->
377 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
378 let preclassified_system_pass_inv_rect_Type1 x1 hterm h1 =
379 let hcut = preclassified_system_pass_rect_Type1 x1 h1 hterm in hcut __
381 (** val preclassified_system_pass_inv_rect_Type0 :
382 Compiler.pass -> preclassified_system_pass ->
383 (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
384 let preclassified_system_pass_inv_rect_Type0 x1 hterm h1 =
385 let hcut = preclassified_system_pass_rect_Type0 x1 h1 hterm in hcut __
387 (** val pcs_pcs__o__pcs_exec :
388 Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
389 SmallstepExec.fullexec **)
390 let pcs_pcs__o__pcs_exec x0 x1 =
391 (pcs_pcs x0 x1).Measurable.pcs_exec
393 (** val pcs_pcs__o__pcs_exec__o__es1 :
394 Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
395 SmallstepExec.trans_system **)
396 let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
397 Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
399 (** val preclassified_system_of_pass :
400 Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
401 let preclassified_system_of_pass = function
402 | Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
403 | Compiler.Clight_switch_removed_pass ->
404 (fun x -> Clight_classified_system.clight_pcs)
405 | Compiler.Clight_label_pass ->
406 (fun x -> Clight_classified_system.clight_pcs)
407 | Compiler.Clight_simplified_pass ->
408 (fun x -> Clight_classified_system.clight_pcs)
409 | Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
410 | Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
411 | Compiler.Rtl_separate_pass ->
413 Joint_fullexec.joint_preclassified_system
414 (SemanticsUtils.sem_graph_params_to_sem_params
415 RTL_semantics.rTL_semantics_separate))
416 | Compiler.Rtl_uniq_pass ->
418 Joint_fullexec.joint_preclassified_system
419 (SemanticsUtils.sem_graph_params_to_sem_params
420 RTL_semantics.rTL_semantics_unique))
421 | Compiler.Ertl_pass ->
423 Joint_fullexec.joint_preclassified_system
424 (SemanticsUtils.sem_graph_params_to_sem_params
425 ERTL_semantics.eRTL_semantics))
426 | Compiler.Ltl_pass ->
428 Joint_fullexec.joint_preclassified_system
429 (SemanticsUtils.sem_graph_params_to_sem_params
430 LTL_semantics.lTL_semantics))
431 | Compiler.Lin_pass ->
433 Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
434 | Compiler.Assembly_pass ->
436 let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in
437 let { Types.fst = code; Types.snd = sigma } = eta4 in
438 Interpret2.aSM_preclassified_system code sigma policy)
439 | Compiler.Object_code_pass ->
440 (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
442 (** val run_and_print :
443 Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
444 Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
445 (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
447 let run_and_print pass prog n print_pass print_event print_error print_exit =
449 let pcs = preclassified_system_of_pass pass prog in
451 let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0
453 Monad.m_bind0 (Monad.max_def Errors.res0)
455 ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
457 let i = print_pass pass in
458 let { Types.fst = trace; Types.snd = res } =
459 Measurable.observe_all_in_measurable n
460 (Measurable.pcs_to_cs (pcs_pcs pass pcs)
461 ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
462 print_event List.Nil s0
466 (match Obj.magic res with
467 | Errors.OK n0 -> print_exit n0
468 | Errors.Error msg -> print_error msg)