source: driver/exec_all.ml @ 2804

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

New executable exec_all. It contains a function to run and print all the
observables of a measurable program, given the program and its
pre_classified_system.

At the moment the executable runs the Clight program in input.

File size: 1.6 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 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 let {Extracted.Types.fst = trace; snd = res} =
28  Extracted.Measurable.observe_all_in_measurable infinity
29   classified_system
30   (fun ie -> print_string (string_of_intensional_event ie); Extracted.Types.It)
31   Extracted.List.Nil s0
32 in
33  match res with
34     OK n ->
35      let n = Extracted.Glue.int_of_bitvector n in
36      print_endline ("EXIT(" ^ string_of_int n ^")"); n
37   | Error m -> print_endline (Error.errormsg m); -1
38;;
39
40let cl = ClightParser.process Sys.argv.(1) in
41let mid =
42  match Extracted.Compiler.front_end cl with
43  | OK o -> Extracted.Types.snd o
44  | Error m -> failwith (Error.errormsg m)
45in
46run_and_print Extracted.Clight_classified_system.clight_pcs cl
Note: See TracBrowser for help on using the repository browser.