adding support for --pp=core and --ast=core when running from a C…

…ore object file.

backend/bmc/main.ml

@@ -12,11 +12,11 @@ let io, get_progress =
   let open Pipeline in
   default_io_helpers, get_progress
 
-let frontend (conf, io) filename core_std =
+let frontend (conf, io) ~is_lib filename core_std =
   if not (Sys.file_exists filename) then
     error ("The file `" ^ filename ^ "' doesn't exist.");
   if Filename.check_suffix filename ".co" || Filename.check_suffix filename ".o" then
-    return @@ read_core_object core_std filename
+    read_core_object (conf, io) ~is_lib core_std filename
   else if Filename.check_suffix filename ".c" then
     c_frontend_and_elaboration (conf, io) core_std ~filename >>= fun (_, _, core_file) ->
     core_passes (conf, io) ~filename core_file
@@ -46,7 +46,7 @@ let core_libraries incl lib_paths libs =
   let lib_paths = if incl then in_runtime "libc" :: lib_paths else lib_paths in
   let libs = if incl then "c" :: libs else libs in
   List.map (fun lib ->
-      match List.fold_left (fun acc path ->
+      true, match List.fold_left (fun acc path ->
           match acc with
           | Some _ -> acc
           | None ->
@@ -114,9 +114,10 @@ let cerberus debug_level progress core_obj
     return (core_stdlib, core_impl)
   in
   let main core_std =
-    Exception.except_foldlM (fun core_files file ->
-        frontend (conf, io) file core_std >>= fun core_file ->
-        return (core_file::core_files)) [] (core_libraries (not nolibc && not core_obj) link_lib_path link_core_obj @ files)
+    Exception.except_foldlM (fun core_files (is_lib, file) ->
+      frontend (conf, io) ~is_lib file core_std >>= fun core_file ->
+      return (core_file::core_files)
+    ) [] (core_libraries (not nolibc && not core_obj) link_lib_path link_core_obj @ (List.map (fun z -> (false, z)) files))
   in
   let epilogue n =
     if batch = `Batch then
@@ -186,7 +187,7 @@ let cerberus debug_level progress core_obj
       else
         Pp_errors.fatal "no input file"
     | [file] when core_obj ->
-      prelude >>= frontend (conf, io) file >>= fun core_file ->
+      prelude >>= frontend (conf, io) ~is_lib:false file >>= fun core_file ->
       begin match output_name with
         | Some output_file ->
           write_core_object core_file output_file
@@ -237,7 +238,7 @@ let cerberus debug_level progress core_obj
       else if core_obj then
         prelude >>= fun core_std ->
         Exception.except_foldlM (fun () file ->
-          frontend (conf, io) file core_std >>= fun core_file ->
+          frontend (conf, io) ~is_lib:false file core_std >>= fun core_file ->
           let output_file = Filename.remove_extension file ^ ".co" in
           write_core_object core_file output_file;
           return ()

backend/common/pipeline.ml

@@ -604,16 +604,16 @@ let version_info =
     (Version.version)
     (Impl_mem.name)
 
-let read_core_object (core_stdlib, core_impl) fname =
+let read_core_object (conf, io) ?(is_lib=false) (core_stdlib, core_impl) filename =
   let open Core in
-  let ic = open_in_bin fname in
+  let ic = open_in_bin filename in
   let v = input_line ic in
   if v <> version_info
   then
     Cerb_debug.warn [] (fun () -> "read core_object file produced with a different version of Cerberus => " ^ v);
   let dump = Marshal.from_channel ic in
   close_in ic;
-  { main=    dump.main;
+  let core_file = { main=    dump.main;
     tagDefs= map_from_assoc sym_compare dump.dump_tagDefs;
     stdlib=  snd core_stdlib;
     impl=    core_impl;
@@ -623,7 +623,11 @@ let read_core_object (core_stdlib, core_impl) fname =
     funinfo= map_from_assoc sym_compare dump.dump_funinfo;
     loop_attributes0= Pmap.empty compare(* map_from_assoc compare dump.dump_loop_attributes *);
     visible_objects_env= Pmap.empty compare
-  }
+  } in
+  if not is_lib then
+    print_core (conf, io) ~filename core_file
+  else
+    return core_file
 
 let write_core_object core_file fname =
   let open Core in

backend/common/pipeline.mli

@@ -90,8 +90,10 @@ val ocaml_backend:
    *)
 
 val read_core_object:
+  (configuration * io_helpers) -> ?is_lib:bool ->
   (((string, Symbol.sym) Pmap.map * (unit, unit) Core.generic_fun_map) * unit Core.generic_impl) ->
-  string -> unit Core.file
+  string ->
+  (unit Core.file, Cerb_location.t * Errors.cause) Exception.exceptM
 val write_core_object: unit Core.file -> string -> unit
 
 

backend/driver/main.ml

@@ -21,11 +21,11 @@ let is_cheri_memory () =
       | Invalid_argument _ -> false in
   starts_with ~prefix:"cheri" Impl_mem.name
 
-let frontend (conf, io) filename core_std =
+let frontend (conf, io) ~is_lib filename core_std =
   if not (Sys.file_exists filename) then
     error ("The file `" ^ filename ^ "' doesn't exist.");
   if Filename.check_suffix filename ".co" || Filename.check_suffix filename ".o" then
-    return @@ read_core_object core_std filename
+    read_core_object (conf, io) ~is_lib core_std filename
   else if Filename.check_suffix filename ".c" then
     c_frontend_and_elaboration (conf, io) core_std ~filename >>= fun (_, _, core_file) ->
     core_passes (conf, io) ~filename core_file
@@ -65,7 +65,7 @@ let core_libraries incl lib_paths libs =
         "c" :: libs
     else libs in
   List.map (fun lib ->
-      match List.fold_left (fun acc path ->
+      true, match List.fold_left (fun acc path ->
           match acc with
           | Some _ -> acc
           | None ->
@@ -144,9 +144,10 @@ let cerberus debug_level progress core_obj
     return (core_stdlib, core_impl)
   in
   let main core_std =
-    Exception.except_foldlM (fun core_files file ->
-        frontend (conf, io) file core_std >>= fun core_file ->
-        return (core_file::core_files)) [] (core_libraries (not nolibc && not core_obj) link_lib_path link_core_obj @ files)
+    Exception.except_foldlM (fun core_files (is_lib, file) ->
+      frontend ~is_lib (conf, io) file core_std >>= fun core_file ->
+      return (core_file::core_files)
+    ) [] (core_libraries (not nolibc && not core_obj) link_lib_path link_core_obj @ (List.map (fun z -> (false, z)) files))
   in
   let epilogue n =
     if batch = `Batch then
@@ -214,7 +215,7 @@ let cerberus debug_level progress core_obj
     | [] ->
       Pp_errors.fatal "no input file"
     | [file] when core_obj ->
-      prelude >>= frontend (conf, io) file >>= fun core_file ->
+      prelude >>= frontend (conf, io) ~is_lib:false file >>= fun core_file ->
       begin match output_name with
         | Some output_file ->
           write_core_object core_file output_file
@@ -236,7 +237,7 @@ let cerberus debug_level progress core_obj
       else if core_obj then
         prelude >>= fun core_std ->
         Exception.except_foldlM (fun () file ->
-          frontend (conf, io) file core_std >>= fun core_file ->
+          frontend (conf, io) ~is_lib:false file core_std >>= fun core_file ->
           let output_file = Filename.remove_extension file ^ ".co" in
           write_core_object core_file output_file;
           return ()

backend/web/instance.ml

@@ -215,7 +215,7 @@ let execute ~conf ~filename (mode: Cerb_global.execution_mode) =
     elaborate ~is_bmc:false ~conf ~filename
     >>= fun (core_std, core_lib, cabs, ail, core) ->
     begin if conf.instance.link_libc then
-      let libc = Pipeline.read_core_object (core_std, core_lib) @@ in_runtime "libc/libc.co" in
+      Pipeline.read_core_object (conf.pipeline, conf.io) ~is_lib:true (core_std, core_lib) @@ in_runtime "libc/libc.co" >>= fun libc ->
       Core_linking.link [core; libc]
     else
       return core
@@ -608,7 +608,7 @@ let step ~conf ~filename (active_node_opt: Instance_api.active_node option) =
     let core     = set_uid core in
     let ranges   = create_expr_range_list core in
     begin if conf.instance.link_libc then
-      let libc = Pipeline.read_core_object (core_std, core_lib) @@ in_runtime "libc/libc.co" in
+      Pipeline.read_core_object (conf.pipeline, conf.io) ~is_lib:true (core_std, core_lib) @@ in_runtime "libc/libc.co" >>= fun libc ->
       Core_linking.link [core; libc]
     else
       return core