From 57c46bc8d0554ef1f0118fec40d9163097564271 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Thu, 6 Apr 2023 13:19:55 +1000
Subject: [PATCH] bitfield_gen: comment for original source file

Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.

Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 CMakeLists.txt         | 1 +
 libsel4/CMakeLists.txt | 1 +
 tools/bitfield_gen.py  | 4 ++++
 tools/helpers.cmake    | 3 ++-
 4 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 222e847f9..98818cf2e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -587,6 +587,7 @@ foreach(bf_dec ${bf_declarations})
         "${pbf_target}"
         "kernel_all_pp_prune.c"
         "kernel_all_pp_prune_wrapper"
+        "${bf_file}"
     )
     GenDefsBFTarget(
         "${bf_gen_target}_def"
diff --git a/libsel4/CMakeLists.txt b/libsel4/CMakeLists.txt
index 66b30dd69..568c924d3 100644
--- a/libsel4/CMakeLists.txt
+++ b/libsel4/CMakeLists.txt
@@ -101,6 +101,7 @@ function(genbf target_prefix pbf_location bf_location header_output)
         ${target_prefix}_pbf
         ""
         ""
+        "${bf_location}"
     )
 endfunction(genbf)
 
diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py
index 3bd98ef2a..5efca4689 100755
--- a/tools/bitfield_gen.py
+++ b/tools/bitfield_gen.py
@@ -2851,6 +2851,8 @@ if __name__ == '__main__':
     parser.add_option('--skip_modifies', action='store_true', default=False)
     parser.add_option('--showclasses', action='store_true', default=False)
     parser.add_option('--debug', action='store_true', default=False)
+    parser.add_option('--from_file', action='store', default=None,
+                      help="Original source file before preprocessing.")
 
     options, args = parser.parse_args()
     DEBUG = options.debug
@@ -3057,6 +3059,8 @@ if __name__ == '__main__':
 
                 print("end", file=out_file)
     else:
+        if options.from_file:
+            print(f"/* generated from {options.from_file} */\n", file=out_file)
         print("#pragma once\n", file=out_file)
         print('\n'.join(map(lambda x: '#include <%s>' % x,
                             INCLUDES[options.environment])), file=out_file)
diff --git a/tools/helpers.cmake b/tools/helpers.cmake
index 672bff173..2f8c0674c 100644
--- a/tools/helpers.cmake
+++ b/tools/helpers.cmake
@@ -132,7 +132,7 @@ endfunction(GenBFTarget)
 # environment is empty for kernel generation and "libsel4" for generating non kernel headers
 # prunes is an optional list of files that will be passed as --prune options to the bitfield
 # generator
-function(GenHBFTarget environment target_name target_file pbf_path pbf_target prunes deps)
+function(GenHBFTarget environment target_name target_file pbf_path pbf_target prunes deps orig_file)
     set(args "")
     if(NOT "${environment}" STREQUAL "")
         list(APPEND args --environment "${environment}")
@@ -141,6 +141,7 @@ function(GenHBFTarget environment target_name target_file pbf_path pbf_target pr
         get_absolute_source_or_binary(prune_absolute "${prune}")
         list(APPEND args "--prune" "${prune_absolute}")
     endforeach()
+    list(APPEND args --from_file "${orig_file}")
     list(APPEND deps ${prunes})
     GenBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}")
 endfunction(GenHBFTarget)