CN-exec: Add with-test-gen CLI flag for generating executable spec of…

… the right format for test-gen

backend/cn/bin/main.ml

@@ -255,6 +255,7 @@ let verify
   output_decorated_dir
   output_decorated
   with_ownership_checking
+  with_test_gen
   copy_source_dir
   astprints
   use_vip
@@ -311,6 +312,7 @@ let verify
           (fun () ->
             Executable_spec.main
               ~with_ownership_checking
+              ~with_test_gen
               ~copy_source_dir
               filename
               ail_prog
@@ -625,6 +627,14 @@ module Executable_spec_flags = struct
     Arg.(value & flag & info [ "with-ownership-checking" ] ~doc)
 
 
+  let with_test_gen =
+    let doc =
+      "Generate CN executable specifications in the correct format for feeding into \n\
+      \  the CN test generation tool."
+    in
+    Arg.(value & flag & info [ "with-test-gen" ] ~doc)
+
+
   let copy_source_dir =
     let doc =
       "Copy non-CN annotated files into output_decorated_dir for CN runtime testing"
@@ -700,6 +710,7 @@ let verify_t : unit Term.t =
   $ Executable_spec_flags.output_decorated_dir
   $ Executable_spec_flags.output_decorated
   $ Executable_spec_flags.with_ownership_checking
+  $ Executable_spec_flags.with_test_gen
   $ Executable_spec_flags.copy_source_dir
   $ Common_flags.astprints
   $ Verify_flags.use_vip

backend/cn/lib/executable_spec.ml

@@ -195,6 +195,7 @@ open Executable_spec_internal
 
 let main
   ?(with_ownership_checking = false)
+  ?(with_test_gen = false)
   ?(copy_source_dir = false)
   filename
   ((_, sigm) as ail_prog)
@@ -368,11 +369,19 @@ let main
     open_auxilliary_files filename prefix included_filenames' []
   in
   let pre_post_pairs =
-    if with_ownership_checking then (
-      let global_ownership_init_pair = generate_ownership_global_assignments sigm prog5 in
-      global_ownership_init_pair @ executable_spec.pre_post)
-    else
-      executable_spec.pre_post
+    if with_test_gen then 
+      (if not (has_main sigm) then 
+        executable_spec.pre_post
+      else 
+        failwith "Input file cannot have predefined main function when passing to CN test-gen tooling"
+      )
+    else 
+      (if with_ownership_checking then (
+        (* Inject ownership init function calls and mapping and unmapping of globals into provided main function *)
+        let global_ownership_init_pair = generate_ownership_global_assignments sigm prog5 in
+        global_ownership_init_pair @ executable_spec.pre_post)
+      else
+        executable_spec.pre_post)
   in
   (match
      Source_injection.(

backend/cn/lib/executable_spec_internal.ml

@@ -661,6 +661,14 @@ let generate_conversion_and_equality_functions
   ( comment ^ CF.Pp_utils.to_plain_pretty_string doc1,
     comment ^ CF.Pp_utils.to_plain_pretty_string doc2 )
 
+let has_main (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma) = 
+  let main_fn_sym_list =
+    List.filter
+      (fun (fn_sym, _) -> String.equal "main" (Sym.pp_string fn_sym))
+      sigm.function_definitions
+  in
+  List.non_empty main_fn_sym_list
+
 
 let generate_ownership_global_assignments
   (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma)