From 01b16de1aefebefacec86f9896ff0252632df0bf Mon Sep 17 00:00:00 2001 From: Shaokai Lin Date: Mon, 2 Feb 2026 22:37:24 -0800 Subject: [PATCH 1/5] Add WIP --- src/nx_helper.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/nx_helper.py b/src/nx_helper.py index a26f8044..b3ccab96 100644 --- a/src/nx_helper.py +++ b/src/nx_helper.py @@ -70,9 +70,23 @@ def remove_back_edges_to_make_dag(G, root): except StopIteration: stack.pop() + # Find original sink before removing back edges. + original_sink = [node for node in G.nodes() if G.out_degree(node) == 0][0] + # Remove identified back edges print(f"num_edges pre = {G.number_of_edges()}") G.remove_edges_from(back_edges) + + # Removing back edges can create new sink nodes (nodes with no outgoing edges). + # Connect these to the original sink to maintain the single-sink property + # required by the basis path analysis. + new_sinks = [ + node for node in G.nodes() + if G.out_degree(node) == 0 and node != original_sink + ] + for node in new_sinks: + G.add_edge(node, original_sink) + # Update num_edges after edge removal G.num_edges = G.number_of_edges() print(f"num_edges post = {G.num_edges}") From b79bfbf2fbb2324214927a6303777c83bfe25922 Mon Sep 17 00:00:00 2001 From: Shaokai Lin Date: Sun, 8 Feb 2026 16:05:02 -0800 Subject: [PATCH 2/5] When drawing redirected edges, also look for named blocks rather than just numbered blocks. --- src/unroller.py | 56 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 38 insertions(+), 18 deletions(-) diff --git a/src/unroller.py b/src/unroller.py index 5a49d1ba..9697b1c0 100644 --- a/src/unroller.py +++ b/src/unroller.py @@ -53,7 +53,27 @@ def modify_loop_branches_to_next_block(input_file_path, output_file_path): """ Modifies an LLVM IR file to replace branches with `!llvm.loop` annotations to point to the block that appears immediately after the block containing - the `!llvm.loop` expression. + the `!llvm.loop` expression. This breaks loop back edges so the IR becomes + a DAG suitable for WCET path analysis. + + Handles both numbered blocks (e.g., "243:") and named blocks + (e.g., "bsort_return.exit:", ".loopexit:"). + + Example: + Given this IR where block 243 branches back to the loop header %201: + + 243: + store i32 %247, ptr %4, align 4 + br label %201, !llvm.loop !10 <-- back edge + + bsort_return.exit: <-- next sequential block + %248 = load i32, ptr %3, align 4 + + The back edge is redirected to the next sequential block: + + 243: + store i32 %247, ptr %4, align 4 + br label %bsort_return.exit, !llvm.loop !10 <-- redirected Args: input_file_path (str): Path to the input LLVM IR file. @@ -62,14 +82,14 @@ def modify_loop_branches_to_next_block(input_file_path, output_file_path): with open(input_file_path, "r") as file: llvm_ir_code = file.read() - # Define regex patterns for identifying branch instructions with !llvm.loop and block labels + # Match both numbered blocks (e.g., "243:") and named blocks (e.g., "bsort_return.exit:", ".loopexit:") block_pattern = re.compile( - r"^(\d+):", re.MULTILINE - ) # Matches lines with block labels (e.g., "3:") - branch_with_loop_pattern = re.compile(r"br label %(\d+), !llvm.loop") + r"^(\d+|[a-zA-Z_.]\S*)\s*:", re.MULTILINE + ) + branch_with_loop_pattern = re.compile(r"br label %(\S+), !llvm.loop") - # Find all blocks in the order they appear - blocks = [int(match.group(1)) for match in block_pattern.finditer(llvm_ir_code)] + # Find all blocks in the order they appear (as strings) + blocks = [match.group(1) for match in block_pattern.finditer(llvm_ir_code)] # Split the code into lines for processing lines = llvm_ir_code.splitlines() @@ -81,22 +101,22 @@ def modify_loop_branches_to_next_block(input_file_path, output_file_path): # Check if the line starts a new block block_match = block_pattern.match(line) if block_match: - current_block = int(block_match.group(1)) + current_block = block_match.group(1) # If a `!llvm.loop` branch is found, modify it to point to the next block loop_branch_match = branch_with_loop_pattern.search(line) if loop_branch_match and current_block is not None: # Find the index of the current block in the blocks list - current_block_index = blocks.index(current_block) - # Ensure there is a next block after the current one - if current_block_index + 1 < len(blocks): - # Get the label of the next block - next_block_num = blocks[current_block_index + 1] - # Replace the branch target to point to this next block - line = line.replace( - f"br label %{loop_branch_match.group(1)}", - f"br label %{next_block_num}", - ) + if current_block in blocks: + current_block_index = blocks.index(current_block) + # Ensure there is a next block after the current one + if current_block_index + 1 < len(blocks): + next_block_label = blocks[current_block_index + 1] + old_target = loop_branch_match.group(1) + line = line.replace( + f"br label %{old_target}", + f"br label %{next_block_label}", + ) # Append the modified or unmodified line to the result new_lines.append(line) From 81fd58622a851574a40c82b6fcb549d973435fb5 Mon Sep 17 00:00:00 2001 From: Shaokai Lin Date: Sun, 8 Feb 2026 17:06:19 -0800 Subject: [PATCH 3/5] Save final results to a text file --- src/cli.py | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/cli.py b/src/cli.py index d442268d..adbfb169 100644 --- a/src/cli.py +++ b/src/cli.py @@ -173,6 +173,46 @@ def run_gametime( logger.info("=" * 60) + # Save results to result.txt in the temp (output) directory + result_file_path = os.path.join( + project_config.location_temp_dir, "result.txt" + ) + os.makedirs(project_config.location_temp_dir, exist_ok=True) + with open(result_file_path, "w") as result_file: + result_file.write("=" * 60 + "\n") + result_file.write("GAMETIME ANALYSIS RESULTS\n") + result_file.write("=" * 60 + "\n") + backend_name = ( + project_config.backend if project_config.backend else "default" + ) + result_file.write(f"Function analyzed: {project_config.func}\n") + result_file.write(f"Backend: {backend_name}\n") + result_file.write(f"Number of basis paths: {len(basis_paths)}\n") + result_file.write( + f"Number of generated paths: {len(generated_paths)}\n" + ) + result_file.write("\nBasis Paths:\n") + for i, path in enumerate(basis_paths): + result_file.write( + f" {i}: {path.name} = {path.get_measured_value()}\n" + ) + if results: + result_file.write("\nGenerated Paths:\n") + for i, (name, predicted_value, measured_value) in enumerate( + results + ): + marker = " *WCET*" if measured_value == max_value else "" + result_file.write( + f" {i}: {name} = predicted: {predicted_value}, " + f"measured: {measured_value}{marker}\n" + ) + result_file.write( + f"\nWorst-Case Execution Time (WCET): {max_value}\n" + ) + result_file.write(f"WCET Path: {max_path}\n") + result_file.write("=" * 60 + "\n") + logger.info(f"Results saved to: {result_file_path}") + # Visualize weighted graph if requested if visualize_weights: logger.info("\n" + "=" * 60) From 0a3c81b021e1914d9032672557c30b39858ea3af Mon Sep 17 00:00:00 2001 From: Shaokai Lin Date: Sun, 8 Feb 2026 17:09:04 -0800 Subject: [PATCH 4/5] Parse inputs from KLEE considering host machine's endianness, and generate C inputs using the correct C integer literal --- src/backend/generate_executable.py | 55 +++++++++++++++++++++++++--- src/smt_solver/extract_klee_input.py | 22 ++++------- 2 files changed, 57 insertions(+), 20 deletions(-) diff --git a/src/backend/generate_executable.py b/src/backend/generate_executable.py index 7f9f0a2b..66e3b418 100644 --- a/src/backend/generate_executable.py +++ b/src/backend/generate_executable.py @@ -22,10 +22,41 @@ Typename, ) import os +import sys import pycparser_fake_libc pycparser_utils_path = pycparser_fake_libc.directory +# Map C type names to their sizes in bytes (for little-endian byte reordering) +TYPE_SIZES = { + "int": 4, "unsigned int": 4, "int32_t": 4, "uint32_t": 4, + "short": 2, "unsigned short": 2, "int16_t": 2, "uint16_t": 2, + "char": 1, "unsigned char": 1, "int8_t": 1, "uint8_t": 1, + "long": 8, "unsigned long": 8, "long long": 8, "unsigned long long": 8, + "int64_t": 8, "uint64_t": 8, +} + + +def _mem_bytes_to_literal_hex(hex_str): + """Convert raw memory-order hex bytes to C integer literal hex (no 0x prefix). + + KLEE outputs bytes in host memory order. On little-endian machines, bytes + need to be reversed to produce the correct C integer literal. On big-endian + machines, bytes are already in the right order. + + Note: The endianness that matters here is that of the machine running KLEE, + not the target machine that runs the WCET tests. KLEE's byte output reflects + the host it ran on; C integer literals are endianness-agnostic. + + Example (little-endian): "01000000" (LE bytes for 1) -> "00000001" (0x00000001 = 1) + Example (big-endian): "00000001" -> "00000001" (no change needed) + """ + if sys.byteorder == "little": + byte_pairs = [hex_str[i:i+2] for i in range(0, len(hex_str), 2)] + byte_pairs.reverse() + return "".join(byte_pairs) + return hex_str + class ExecutableTransformer(object): """ @@ -309,7 +340,14 @@ def generate_primitive_declaration(self, name, type_node, value): """ generator = c_generator.CGenerator() type_str = generator.visit(type_node) - # Use __builtin_bswap32 to convert KLEE's little endian value to big endian. + # Reverse bytes from KLEE's little-endian memory order to correct integer literal + hex_str = value.strip() + if hex_str.startswith("0x"): + raw = hex_str[2:] + type_name = " ".join(type_node.type.names) if hasattr(type_node, 'type') and hasattr(type_node.type, 'names') else "int" + elem_size = TYPE_SIZES.get(type_name, len(raw) // 2) + raw = raw[:elem_size * 2] + value = "0x" + _mem_bytes_to_literal_hex(raw) return f"{type_str} {name} = {value};" def generate_struct_declaration(self, name, struct_type_node, value_dict): @@ -348,12 +386,17 @@ def generate_array_declaration(self, name, array_type_node, values): """ # TODO: see how KLEE output nested array element_type_str = self.get_element_type_str(array_type_node) - # -2 to skip 0x and -1 to remove the trailing space - values_hex = values[2:-1] - # 8 here because integer 32bit are 8 heximal degits + elem_size = TYPE_SIZES.get(element_type_str, 4) + hex_digits_per_elem = elem_size * 2 + # Strip 0x prefix and trailing whitespace + values_hex = values.strip() + if values_hex.startswith("0x"): + values_hex = values_hex[2:] + # Chunk by element size and reverse bytes within each element values_chunk = [] - for i in range(0, len(values_hex), 8): - values_chunk.append("0x" + values_hex[i : i + 8]) + for i in range(0, len(values_hex), hex_digits_per_elem): + chunk = values_hex[i : i + hex_digits_per_elem] + values_chunk.append("0x" + _mem_bytes_to_literal_hex(chunk)) values_str = ", ".join(values_chunk) return f"{element_type_str} {name}[] = {{ {values_str} }};" diff --git a/src/smt_solver/extract_klee_input.py b/src/smt_solver/extract_klee_input.py index ff5dc7d0..2d535fcc 100644 --- a/src/smt_solver/extract_klee_input.py +++ b/src/smt_solver/extract_klee_input.py @@ -6,7 +6,10 @@ def write_klee_input_to_file(filename): """ - Extract hexadecimal values from a KLEE test input file, convert them from little endian to big endian, and write them to a new file. + Extract raw hexadecimal values from a KLEE test input file and write them + to a new file. The hex values are in memory byte order of the host machine + where KLEE runs; per-element byte reversal is handled downstream in + generate_executable.py where the element type size is known. Parameters: filename : str @@ -22,23 +25,14 @@ def write_klee_input_to_file(filename): # Find all hex values using regex hex_values = pattern.findall(data) print(hex_values) - # Convert each value from little endian to big endian - big_endian_values = [] - for value in hex_values: - hex_str = value[2:] # remove '0x' - if len(hex_str) % 2 != 0: - hex_str = "0" + hex_str # pad to even length - bytes_list = [hex_str[i : i + 2] for i in range(0, len(hex_str), 2)] - bytes_list.reverse() - big_endian = "".join(bytes_list) - big_endian_values.append("0x" + big_endian) - # Write big endian hex values to a new text file + + # Write raw hex values to a new text file (no byte reordering here) values_filename = filename[:-4] + "_values.txt" with open(values_filename, "w") as outfile: - for value in big_endian_values: + for value in hex_values: outfile.write(value + "\n") - print(f"Big endian hex values extracted and written to {values_filename}") + print(f"Hex values extracted and written to {values_filename}") def find_test_file(klee_last_dir): From f330ac523a9d4e1ab1c87752fde38339f1afa48d Mon Sep 17 00:00:00 2001 From: Shaokai Lin Date: Sun, 8 Feb 2026 17:13:00 -0800 Subject: [PATCH 5/5] Support test functions that do not have parameters --- src/backend/generate_executable.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/backend/generate_executable.py b/src/backend/generate_executable.py index 66e3b418..d672910b 100644 --- a/src/backend/generate_executable.py +++ b/src/backend/generate_executable.py @@ -99,6 +99,8 @@ def visit(self, node): (argument types of function being analyzed, argument names of function being analyzed) """ if isinstance(node, FuncDef) and node.decl.name == self.function_name: + if node.decl.type.args is None: + return [], [] params = node.decl.type.args.params arg_types = [param.type for param in params] arg_names = [param.name for param in params]