source: driver/compiler.ml @ 2769

Last change on this file since 2769 was 2759, checked in by campbell, 7 years ago

Print out costs, with choice of style.
Note small anti-assertion patch to extracted ASMCosts.
No stack space yet.

File size: 1.6 KB
Line 
1open Extracted.Errors
2open ClightPrinter
3
4let rec run g s =
5  (match Extracted.RTLabs_semantics.rTLabs_is_final s with
6  | Extracted.Types.None ->
7    (match Extracted.RTLabs_semantics.eval_statement g s with
8    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
9    | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m)
10    | _ -> failwith "oh dear")
11  | Extracted.Types.Some r -> r)
12
13let convBool = function
14| Extracted.Bool.True -> true
15| Extracted.Bool.False -> false
16
17let bv_to_int v =
18  let rec aux i v =
19    match v with
20    | Extracted.Vector.VEmpty -> i
21    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
22  in aux 0 v
23;;
24
25let cl = ClightParser.process Sys.argv.(1) in
26let OK {Extracted.Types.fst = oc; snd = acl} = Extracted.Compiler.compile cl in
27let {Extracted.Types.dpi1 = labelled; Extracted.Types.dpi2 = l_costmap} = acl in
28let style =
29  match try Sys.argv.(2) with _ -> "instrumented" with
30  | "plain" -> Cost_plain
31  | "numbered" -> Cost_numbered l_costmap
32  | "instrumented" -> Cost_instrumented l_costmap
33  | x -> failwith ("I have no idea what " ^ x ^ " means")
34in
35print_endline (ClightPrinter.print_program style labelled)
36(*
37let OK mid = Extracted.Compiler.front_end cl in
38let rtlabs = Extracted.Types.snd mid in
39let g = Extracted.RTLabs_semantics.make_global0 rtlabs in
40let OK s0 = Extracted.RTLabs_semantics.make_initial_state0 rtlabs in
41let r = run g s0 in
42exit (bv_to_int r)
43
44val compile :
45  Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
46  (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
47  Errors.res
48*)
Note: See TracBrowser for help on using the repository browser.