Changeset 2834 for driver

Timestamp:

Mar 8, 2013, 11:45:29 PM (7 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:

• build (modified) (1 diff)
• cerco.ml (modified) (1 diff)
• exec_all.ml (deleted)

driver/build

@@ -12 +12 @@
 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml
 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml
-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
 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 clightPrinter.cmo IntelHex.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco

driver/cerco.ml

@@ -2 +2 @@
 open ClightPrinter
 
-let rec run g s =
-  (match Extracted.RTLabs_semantics.rTLabs_is_final s with
-  | Extracted.Types.None ->
-    (match Extracted.RTLabs_semantics.eval_statement g s with
-    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
-    | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m)
-    | _ -> failwith "oh dear")
-  | Extracted.Types.Some r -> r)
+let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
 
-let convBool = function
-| Extracted.Bool.True -> true
-| Extracted.Bool.False -> false
-
-let bv_to_int v =
-  let rec aux i v =
-    match v with
-    | Extracted.Vector.VEmpty -> i
-    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
-  in aux 0 v
+let string_of_intensional_event =
+ function
+    Extracted.StructuredTraces.IEVcost cl ->
+     "COST(k_" ^ string_of_pos cl ^") "
+  | Extracted.StructuredTraces.IEVcall id ->
+     "CALL(fun_" ^ string_of_pos id ^ ") "
+  | Extracted.StructuredTraces.IEVtailcall _ -> assert false
+  | Extracted.StructuredTraces.IEVret id ->
+     "RET(fun_" ^ string_of_pos id ^ ") "
 ;;
 
-let cl = ClightParser.process Sys.argv.(1) in
+let string_of_pass =
+ function
+ | Extracted.Compiler.Clight_pass                -> "Clight_pass"
+ | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass"
+ | Extracted.Compiler.Clight_label_pass          -> "Clight_label_pass"
+ | Extracted.Compiler.Clight_simplified_pass     -> "Clight_simplified_pass"
+ | Extracted.Compiler.Cminor_pass                -> "Cminor_pass"
+ | Extracted.Compiler.Rtlabs_pass                -> "Rtlabs_pass"
+ | Extracted.Compiler.Rtl_separate_pass          -> "Rtl_separate_pass"
+ | Extracted.Compiler.Rtl_uniq_pass              -> "Rtl_uniq_pass"
+ | Extracted.Compiler.Ertl_pass                  -> "Ertl_pass"
+ | Extracted.Compiler.Ertlptr_pass               -> "Ertlptr_pass"
+ | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass"
+ | Extracted.Compiler.Lin_pass                   -> "Lin_pass"
+;;
+
+let argv1 = Sys.argv.(1) in
+let do_print,filename =
+ if argv1 = "-exec" then
+  true,Sys.argv.(2)
+ else
+  false,argv1 in
+let cl = ClightParser.process filename in
+let observe =
+ if do_print then
+  let rec infinity = Extracted.Nat.S infinity in
+  (fun pass prog ->
+    Extracted.Semantics.run_and_print pass prog infinity
+     (fun p -> print_endline ("\n" ^ string_of_pass p ^ ":"); Extracted.Types.It)
+     (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
+     (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
+     (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
+ else (fun _ _ -> Extracted.Types.It) 
+in
 let output = 
-  match Extracted.Compiler.compile cl with
+  match Extracted.Compiler.compile observe cl with
   | OK o -> o
   | Error m -> failwith (Error.errormsg m)