source: driver/compiler.ml @ 2758

Last change on this file since 2758 was 2758, checked in by campbell, 8 years ago

Adapt prototype's Clight printer.
Doesn't use cost map yet.

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