Changeset 2834


Ignore:
Timestamp:
Mar 8, 2013, 11:45:29 PM (6 years ago)
Author:
sacerdot
Message:

Execution integrated in the compiler, as it was in the prototype.
Syntaxes:

cerco filename.c it only compiles
cerco -exec filename.c it executes after each pass

Location:
driver
Files:
1 deleted
2 edited

Legend:

Unmodified
Added
Removed
  • driver/build

    r2815 r2834  
    1212ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml
    1313ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml
    14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo error.cmo exec_all.cmo -o exec_all
    1514ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo clightPrinter.cmo IntelHex.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco
  • driver/cerco.ml

    r2791 r2834  
    22open ClightPrinter
    33
    4 let 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)
     4let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
    125
    13 let convBool = function
    14 | Extracted.Bool.True -> true
    15 | Extracted.Bool.False -> false
    16 
    17 let 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
     6let string_of_intensional_event =
     7 function
     8    Extracted.StructuredTraces.IEVcost cl ->
     9     "COST(k_" ^ string_of_pos cl ^") "
     10  | Extracted.StructuredTraces.IEVcall id ->
     11     "CALL(fun_" ^ string_of_pos id ^ ") "
     12  | Extracted.StructuredTraces.IEVtailcall _ -> assert false
     13  | Extracted.StructuredTraces.IEVret id ->
     14     "RET(fun_" ^ string_of_pos id ^ ") "
    2315;;
    2416
    25 let cl = ClightParser.process Sys.argv.(1) in
     17let string_of_pass =
     18 function
     19 | Extracted.Compiler.Clight_pass                -> "Clight_pass"
     20 | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass"
     21 | Extracted.Compiler.Clight_label_pass          -> "Clight_label_pass"
     22 | Extracted.Compiler.Clight_simplified_pass     -> "Clight_simplified_pass"
     23 | Extracted.Compiler.Cminor_pass                -> "Cminor_pass"
     24 | Extracted.Compiler.Rtlabs_pass                -> "Rtlabs_pass"
     25 | Extracted.Compiler.Rtl_separate_pass          -> "Rtl_separate_pass"
     26 | Extracted.Compiler.Rtl_uniq_pass              -> "Rtl_uniq_pass"
     27 | Extracted.Compiler.Ertl_pass                  -> "Ertl_pass"
     28 | Extracted.Compiler.Ertlptr_pass               -> "Ertlptr_pass"
     29 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass"
     30 | Extracted.Compiler.Lin_pass                   -> "Lin_pass"
     31;;
     32
     33let argv1 = Sys.argv.(1) in
     34let do_print,filename =
     35 if argv1 = "-exec" then
     36  true,Sys.argv.(2)
     37 else
     38  false,argv1 in
     39let cl = ClightParser.process filename in
     40let observe =
     41 if do_print then
     42  let rec infinity = Extracted.Nat.S infinity in
     43  (fun pass prog ->
     44    Extracted.Semantics.run_and_print pass prog infinity
     45     (fun p -> print_endline ("\n" ^ string_of_pass p ^ ":"); Extracted.Types.It)
     46     (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
     47     (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
     48     (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
     49 else (fun _ _ -> Extracted.Types.It)
     50in
    2651let output =
    27   match Extracted.Compiler.compile cl with
     52  match Extracted.Compiler.compile observe cl with
    2853  | OK o -> o
    2954  | Error m -> failwith (Error.errormsg m)
Note: See TracChangeset for help on using the changeset viewer.