Fix loop unrolling and support array inputs

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):
     """
@@ -68,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]
@@ -309,7 +342,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 +388,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} }};"

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)

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}")

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):

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)