CN-exec: Add mapping of globals to main

backend/cn/executable_spec.ml

@@ -163,21 +163,10 @@ let main ?(with_ownership_checking=false) ?(copy_source_dir=false) filename ((_,
   let cn_utils_header_pair = ("cn-executable/utils.h", true) in
   let cn_utils_header = Executable_spec_utils.generate_include_header cn_utils_header_pair in
 
-  (* Ownership checking *)
-  (* if with_ownership_checking then 
-    (let ownership_oc = Stdlib.open_out (prefix ^ "ownership.c") in 
-    let ownership_globals = generate_ownership_globals ~is_extern:false () in 
-    Stdlib.output_string ownership_oc cn_utils_header;
-    Stdlib.output_string ownership_oc "\n";
-    Stdlib.output_string ownership_oc ownership_globals;
-    )
-  ; *)
-
   let ownership_function_defs, ownership_function_decls = generate_ownership_functions with_ownership_checking Cn_internal_to_ail.ownership_ctypes sigm in
   let (c_struct_defs, _c_struct_decls) = print_c_structs sigm.tag_definitions in
   let (cn_converted_struct_defs, _cn_converted_struct_decls) = generate_cn_versions_of_structs sigm.tag_definitions in
 
-
 
   (* let (records_str, record_equality_fun_strs, record_equality_fun_prot_strs) = generate_all_record_strs sigm in *)
   let (record_defs_str, _record_decls_str, record_equality_fun_strs, record_equality_fun_prot_strs) = c_records in
@@ -265,7 +254,7 @@ let main ?(with_ownership_checking=false) ?(copy_source_dir=false) filename ((_,
   let fns_and_ocs = 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 in 
+    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

backend/cn/executable_spec_internal.ml

@@ -309,23 +309,14 @@ let generate_conversion_and_equality_functions (sigm : CF.GenTypes.genTypeCatego
   (comment ^ CF.Pp_utils.to_plain_pretty_string doc1, comment ^ CF.Pp_utils.to_plain_pretty_string doc2)
 
 
-(* Ownership *)
-
-let generate_ownership_globals ?(is_extern=false) () = 
-  let ownership_decls = Ownership_exec.create_ail_ownership_global_decls () in 
-  let docs = List.map (fun (sym, ty) ->
-     let maybe_extern = if is_extern then PPrint.(!^) "extern " else PPrint.empty in
-     maybe_extern ^^ 
-     CF.Pp_ail.pp_ctype_declaration ~executable_spec:true (CF.Pp_ail.pp_id_obj sym) empty_qualifiers ty) ownership_decls 
-  in
-  let doc = PPrint.concat_map (fun d -> d ^^ PPrint.semi ^^ PPrint.hardline) docs in
-  CF.Pp_utils.to_plain_pretty_string doc
-
-let generate_ownership_global_assignments (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma) = 
+let generate_ownership_global_assignments (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma) (prog5: unit Mucore.mu_file) = 
   let main_fn_sym_list = List.filter (fun (fn_sym, _) -> String.equal "main" (Sym.pp_string fn_sym)) sigm.function_definitions in 
   match main_fn_sym_list with 
     | [] -> failwith "CN-exec: No main function so ownership globals cannot be initialised"
     | (main_sym, _) :: _ ->
+      let globals = extract_global_variables prog5.mu_globs in 
+      let global_map_fcalls = List.map Ownership_exec.generate_c_local_ownership_entry_fcall globals in 
+      let global_map_stmts_ = List.map (fun e -> A.AilSexpr e) global_map_fcalls in 
       let assignments = Ownership_exec.get_ownership_global_init_stats () in
-      let assignments_str = generate_ail_stat_strs ([], assignments) in
-      [(main_sym, (assignments_str, []))]
+      let init_and_mapping_str = generate_ail_stat_strs ([], assignments @ global_map_stmts_) in
+      [(main_sym, (init_and_mapping_str, []))]

backend/cn/ownership_exec.ml

@@ -141,14 +141,11 @@ let rec get_c_control_flow_block_unmaps_aux break_vars continue_vars return_vars
   match s_ with 
     | A.(AilSdeclaration _) -> []
     | (AilSblock (bs, ss)) ->
-      (* let injs = [] in  *)
       let injs = List.mapi (fun i s ->
         let ss_ = take (i + 1) ss in 
         let visibles = collect_visibles (bs @ bindings) ss_ in 
         get_c_control_flow_block_unmaps_aux (visibles @ break_vars) (visibles @ continue_vars) (visibles @ return_vars) (bs @ bindings) s 
       ) ss in 
-      (* let vars_and_injs = List.map (get_c_control_flow_block_unmaps_aux break_vars continue_vars return_vars bs) ss in  *)
-      (* let (_, injs) = List.split vars_and_injs in  *)
       List.concat injs
     | (AilSif (_, s1, s2)) -> 
       let injs = get_c_control_flow_block_unmaps_aux break_vars continue_vars return_vars bindings s1 in