source: driver/exec_all.ml @ 2805

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

Now also prints the trace for the labelled Clight.

File size: 1.7 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 mid =
43  match Extracted.Compiler.front_end cl with
44  | OK o -> o
45  | Error m -> failwith (Error.errormsg m) in
46let acl = Extracted.Types.snd (Extracted.Types.fst mid) in
47run_and_print "Clight:  " Extracted.Clight_classified_system.clight_pcs cl;
48run_and_print "LClight: " Extracted.Clight_classified_system.clight_pcs cl
Note: See TracBrowser for help on using the repository browser.