make inlining optional and allow multiple files

src/analyzer.py

@@ -132,11 +132,13 @@ def _preprocess(self):
 
         # Check if the additional files to be analyzed exists.
         additional_files = self.project_config.location_additional_files
-        project_temp_dir = self.project_config.location_temp_dir
-        if not os.path.exists(additional_files):
-            shutil.rmtree(project_temp_dir)
-            err_msg = "File to analyze not found: %s" % additional_files
-            raise GameTimeError(err_msg)
+        if additional_files:
+            for additional_file in additional_files:
+                project_temp_dir = self.project_config.location_temp_dir
+                if not os.path.exists(additional_file):
+                    shutil.rmtree(project_temp_dir)
+                    err_msg = "File to analyze not found: %s" % additional_file
+                    raise GameTimeError(err_msg)
 
         # Remove any temporary directory created during a previous run
         # of the same GameTime project, and create a fresh new
@@ -164,17 +166,19 @@ def _preprocess(self):
         processing = clang_helper.compile_to_llvm_for_analysis(self.project_config.location_orig_file, self.project_config.location_temp_dir,
                                                           f"{self.project_config.name_orig_no_extension}gt", self.project_config.included, self.project_config.compile_flags)
 
-        additional_files_processing = clang_helper.compile_to_llvm_for_analysis(self.project_config.location_additional_files, self.project_config.location_temp_dir,
-                                                          f"{self.project_config.location_additional_files[:-2]}gt", self.project_config.included, self.project_config.compile_flags)
+        if additional_files:
+            additional_files_processing = clang_helper.compile_list_to_llvm_for_analysis(self.project_config.location_additional_files, self.project_config.location_temp_dir,
+                                                        self.project_config.included, self.project_config.compile_flags)
 
         # Preprocessing pass: inline functions.
-        if self.project_config.inlined:  # Note: This is made into a bool rather than a list
+        if self.project_config.inlined and additional_files:  # Note: This is made into a bool rather than a list
             processing = self._run_inliner(input_file=processing, additional_files=additional_files_processing)
 
         # Preprocessing pass: unroll loops.
         if self.project_config.UNROLL_LOOPS:
             processing = self._run_loop_unroller(compiled_file=processing)
-
+        print("PROCESSING", processing)
+        print("LOCATION", self.project_config.location_temp_dir)
         self.dag_path: str = clang_helper.generate_dot_file(processing, self.project_config.location_temp_dir)
         self.preprocessed_path: str = processing
         # We are done with the preprocessing.
@@ -238,7 +242,7 @@ def _run_inliner(self, input_file: str, additional_files: str):
         # inlined_file = clang_helper.inline_functions(input_file, self.project_config.location_temp_dir,
         #                                              f"{self.project_config.name_orig_no_extension}gt-inlined")
 
-        input_files = [input_file, additional_files]
+        input_files = [input_file] + additional_files
         inlined_file = inliner.inline_functions(input_files, self.project_config.location_temp_dir,
                                                      f"{self.project_config.name_orig_no_extension}gt-inlined")
 

src/clang_helper.py

@@ -50,7 +50,13 @@ def compile_to_llvm_for_exec(c_filepath: str, output_file_folder: str, output_na
 
     return output_file
 
-def compile_to_llvm_for_analysis(c_filepath: str, output_file_folder: str, output_name: str, extra_libs: List[str]=[], extra_flags: List[str]=[], readable: bool = True) -> str:
+def compile_list_to_llvm_for_analysis(c_filepaths: List[str] , output_file_folder: str, extra_libs: List[str]=[], extra_flags: List[str]=[], readable: bool = True) -> List[str]:
+    compiled_files = []
+    for c_filepath in c_filepaths:
+        compiled_files.append(compile_to_llvm_for_analysis(c_filepath, output_file_folder, f"{c_filepath[:-2]}gt", extra_libs, extra_flags, readable))
+    return compiled_files
+
+def compile_to_llvm_for_analysis(c_filepath: str , output_file_folder: str, output_name: str, extra_libs: List[str]=[], extra_flags: List[str]=[], readable: bool = True) -> str:
     """
     Compile the C program into bitcode in OUTPUT_FILE_FOLDER using -O0 option to preserve maximum structure.
 

src/project_configuration.py

@@ -62,7 +62,7 @@ class ProjectConfiguration(object):
     Stores information necessary to configure a GameTime project.
     """
 
-    def __init__(self, location_file, location_additional_files, func,
+    def __init__(self, location_file,  func, location_additional_files=None,
                  start_label="", end_label="", included=None, merged=None,
                  inlined=None, unroll_loops=False, randomize_initial_basis=False,
                  maximum_error_scale_factor=10,
@@ -78,7 +78,7 @@ def __init__(self, location_file, location_additional_files, func,
         self.location_orig_file = location_file
 
         # Location of the additional files to be analyzed.
-        self.location_additional_files = location_additional_files
+        self.location_additional_files = location_additional_files or []
 
         # Location of the file to be analyzed, without the extension.
         self.location_orig_no_extension = ""

src/project_configuration_parser.py

@@ -76,7 +76,7 @@ def parse(configuration_file_path: str) -> ProjectConfiguration:
         # Initialize the instantiation variables for
         # the ProjectConfiguration object.
         location_file, func = "", ""
-        location_additional_files = ""
+        location_additional_files = []
         start_label, end_label = "", ""
         included, merged, inlined, unroll_loops = [], [], [], False
         randomize_initial_basis = False
@@ -95,7 +95,7 @@ def parse(configuration_file_path: str) -> ProjectConfiguration:
                 case "location":
                     location_file = os.path.normpath(os.path.join(project_config_dir, file_configs[key]))
                 case "additional-files":
-                    location_additional_files = os.path.normpath(os.path.join(project_config_dir, file_configs[key]))
+                    location_additional_files = [os.path.normpath(os.path.join(project_config_dir, additional_file)) for additional_file in file_configs[key]]
                 case "analysis-function":
                     func = file_configs[key]
                 case "start-label":
@@ -191,7 +191,7 @@ def parse(configuration_file_path: str) -> ProjectConfiguration:
                                                                      dump_all_queries, keep_parser_output,
                                                                      keep_simulator_output)
 
-        project_config: ProjectConfiguration = ProjectConfiguration(location_file, location_additional_files, func,
+        project_config: ProjectConfiguration = ProjectConfiguration(location_file, func, location_additional_files,
                                                                     start_label, end_label, included,
                                                                     merged, inlined, unroll_loops,
                                                                     randomize_initial_basis,

src/smt_solver/smt.py

@@ -5,8 +5,9 @@
 from defaults import logger
 import clang_helper
 import inliner
+from project_configuration import ProjectConfiguration
 
-def compile_and_run_cplusplus(modify_bit_code_cpp_file, modify_bit_code_exec_file, input_c_file, additional_files, c_filename, labels_file, all_labels_file, func_name, output_dir, project_config):
+def compile_and_run_cplusplus(modify_bit_code_cpp_file, modify_bit_code_exec_file, input_c_file, additional_files, c_filename, labels_file, all_labels_file, func_name, output_dir, project_config: ProjectConfiguration):
     """
     Compile and run a C++ file that modifies LLVM bitcode, then process the C file through several steps.
 
@@ -40,9 +41,12 @@ def compile_and_run_cplusplus(modify_bit_code_cpp_file, modify_bit_code_exec_fil
 
     #TODO: add extra flag and includes through project configuration
     compiled_file = clang_helper.compile_to_llvm_for_analysis(input_c_file, output_dir, c_filename, project_config.included, project_config.compile_flags)
-    compiled_additional_file = clang_helper.compile_to_llvm_for_analysis(additional_files, output_dir, "helper_smt", project_config.included, project_config.compile_flags)
-    compiled_files = [compiled_file, compiled_additional_file]
-    input_bc_file = inliner.inline_functions(compiled_files, output_dir, f"{c_filename}-inlined")
+    if project_config.inlined and additional_files:
+        compiled_additional_files = clang_helper.compile_list_to_llvm_for_analysis(additional_files, output_dir, "helper_smt", project_config.included, project_config.compile_flags)
+        compiled_files = [compiled_file] + compiled_additional_files
+        input_bc_file = inliner.inline_functions(compiled_files, output_dir, f"{c_filename}_inlined")
+    else: 
+        input_bc_file = compiled_file
     # input_bc_file = clang_helper.unroll_loops(inlined_file, output_dir,
                                                        # f"{c_filename}-unrolled", project_config)
 
@@ -85,7 +89,7 @@ def extract_labels_from_file(filename):
                 print(f"Ignoring non-numeric value: {line.strip()}")
     return labels
 
-def run_smt(project_config, labels_file, output_dir, total_number_of_labels):
+def run_smt(project_config: ProjectConfiguration, labels_file: str, output_dir: str, total_number_of_labels: int):
     """
     This function generates the input for the program to be analzed to drive down the given path.
     The input is generated by utilizing the symbolic execution engine KLEE, which uses SMT-Solvers like Z3
@@ -123,7 +127,11 @@ def run_smt(project_config, labels_file, output_dir, total_number_of_labels):
     modify_bit_code_cpp_file = '../../src/smt_solver/modify_bitcode.cpp'
     modify_bit_code_exec_file = '../../src/smt_solver/modify_bitcode'
     compile_and_run_cplusplus(modify_bit_code_cpp_file, modify_bit_code_exec_file, klee_file_path, additional_files_path, c_file + "_klee_format", labels_file, os.path.join(project_config.location_temp_dir, "labels_0.txt"), project_config.func, output_dir, project_config)
-    modified_klee_file_bc = klee_file_path[:-2] + "-inlined" + "_mod.bc"
+    inline_str = ""
+    if project_config.inlined and additional_files_path:
+        inline_str = "_inlined"
+
+    modified_klee_file_bc = klee_file_path[:-2] + inline_str + "_mod.bc"
 
     # run klee
     run_klee(modified_klee_file_bc)