diff --git a/src/analyzer.py b/src/analyzer.py index 36abb55..90bef6f 100644 --- a/src/analyzer.py +++ b/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") diff --git a/src/clang_helper.py b/src/clang_helper.py index d8812c3..eceb3ad 100644 --- a/src/clang_helper.py +++ b/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. diff --git a/src/project_configuration.py b/src/project_configuration.py index dbbae8d..9eae0ef 100644 --- a/src/project_configuration.py +++ b/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 = "" diff --git a/src/project_configuration_parser.py b/src/project_configuration_parser.py index 319b9b7..8b04241 100644 --- a/src/project_configuration_parser.py +++ b/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, diff --git a/src/smt_solver/smt.py b/src/smt_solver/smt.py index d81427d..4db2a0a 100644 --- a/src/smt_solver/smt.py +++ b/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)