source: driver/exec_all.ml @ 2813

Last change on this file since 2813 was 2813, checked in by sacerdot, 7 years ago

RTLabs now printed too

File size: 2.3 KB
Line 
1open Extracted.Errors
2
3let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
4
5let string_of_intensional_event =
6 function
7    Extracted.StructuredTraces.IEVcost cl ->
8     "COST(k_" ^ string_of_pos cl ^") "
9  | Extracted.StructuredTraces.IEVcall id ->
10     "CALL(fun_" ^ string_of_pos id ^ ") "
11  | Extracted.StructuredTraces.IEVtailcall _ -> assert false
12  | Extracted.StructuredTraces.IEVret id ->
13     "RET(fun_" ^ string_of_pos id ^ ") "
14;;
15
16let run_and_print label pre_classified_system prog =
17 let prog = Obj.magic prog in
18 let fullexec = Extracted.Measurable.pcs_exec pre_classified_system in
19 let g = Extracted.SmallstepExec.make_global fullexec prog in
20 let classified_system=Extracted.Measurable.pcs_to_cs pre_classified_system g in
21 let s0 =
22   match Extracted.SmallstepExec.make_initial_state fullexec prog with
23   | OK o -> o
24   | Error m -> failwith (Error.errormsg m)
25 in
26 let rec infinity = Extracted.Nat.S infinity in
27 print_string label;
28 let {Extracted.Types.fst = trace; snd = res} =
29  Extracted.Measurable.observe_all_in_measurable infinity
30   classified_system
31   (fun ie -> print_string (string_of_intensional_event ie); Extracted.Types.It)
32   Extracted.List.Nil s0
33 in
34  match res with
35     OK n ->
36      let n = Extracted.Glue.int_of_bitvector n in
37      print_endline ("EXIT(" ^ string_of_int n ^")"); n
38   | Error m -> print_endline (Error.errormsg m); -1
39;;
40
41let cl = ClightParser.process Sys.argv.(1) in
42let clsr = Extracted.SwitchRemoval.program_switch_removal cl in
43let {Extracted.Types.fst=acl;snd=init_cost}=Extracted.Label.clight_label clsr in
44let acl' = Extracted.SimplifyCasts.simplify_program acl in
45let cm =
46 match Extracted.ToCminor.clight_to_cminor acl' with
47  | OK o -> o
48  | Error m -> failwith (Error.errormsg m) in
49let rtla = Extracted.ToRTLabs.cminor_to_rtlabs init_cost cm in
50run_and_print "Clight:   " Extracted.Clight_classified_system.clight_pcs cl;
51run_and_print "ClightSR: " Extracted.Clight_classified_system.clight_pcs clsr;
52run_and_print "LClight:  " Extracted.Clight_classified_system.clight_pcs acl;
53run_and_print "SClight:  " Extracted.Clight_classified_system.clight_pcs acl';
54run_and_print "Cminor:   " Extracted.Cminor_classified_system.cminor_pcs cm;
55let res =
56run_and_print "RTLabs:   " Extracted.RTLabs_classified_system.rTLabs_pcs rtla
57in exit res
Note: See TracBrowser for help on using the repository browser.