diff --git a/.gitignore b/.gitignore index 139bafb6..64796f3c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,10 @@ test/**/*gt/* **/__pycache__ /Dockerfile* -env +env.bash build **/*.bc **/*.ll -.venv \ No newline at end of file +.venv +*.egg-info/ +src/custom_passes/*.so \ No newline at end of file diff --git a/README.md b/README.md index 114e7626..7811dfd3 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,6 @@ Welcome to the setup guide for the Gametime project! This document provides instructions for setting up and running the Gametime project on both Linux and macOS. Follow the steps below to install the required dependencies and configure your environment for development and testing. ---- ## Setup Instructions @@ -95,23 +94,41 @@ If you are having trouble installing pygraphviz on macOS try the following: [Sta To use KLEE with Gametime, follow the installation instructions on the [KLEE official website](https://klee.github.io/). -Add the KLEE header files to yout `C_INCLUDE_PATH`: +### 5. Install the FlexPRET Emulator (Recommended) + +To use the FlexPRET emulator with GameTime, follow the installation instructions on the [FlexPRET Github Page](https://github.com/pretis/flexpret). + +### 6. Configure Environment Variables + +After installing KLEE and FlexPRET, you need to set up environment variables so GameTime can find these dependencies. Create or edit the `env.bash` file in the GameTime project root: ```bash +# Add KLEE include path export C_INCLUDE_PATH="/include:$C_INCLUDE_PATH" + +# Source FlexPRET environment (sets up PATH and other variables) +source /env.bash ``` -### 5. Install the FlexPRET Emulator (Recommended): +**Example `env.bash` file:** -To use the FlexPRET emulator with GameTime, follow the installation instructions on the [FlexPRET Github Page](https://github.com/pretis/flexpret). +```bash +# KLEE headers +export C_INCLUDE_PATH=/opt/homebrew/Cellar/klee/3.1_4/include:$C_INCLUDE_PATH + +# FlexPRET environment (includes fp-emu in PATH) +source /Users/username/Documents/projects/flexpret/env.bash +``` -Add fp-emu to `PATH`: +**Note:** Replace the paths with your actual installation locations. The FlexPRET `env.bash` file typically adds the emulator (`fp-emu`) to your `PATH` automatically. + +You'll need to source this file before using GameTime: ```bash -export PATH="$PATH:/flexpret/build/emulator" +source env.bash ``` -### 6. Compile LLVM Passes +### 7. Compile LLVM Passes From the project root directory run: @@ -119,57 +136,201 @@ From the project root directory run: clang++ -shared -fPIC src/custom_passes/custom_inline_pass.cpp -o src/custom_passes/custom_inline_pass.so `llvm-config --cxxflags --ldflags --libs` -Wl,-rpath,$(llvm-config --libdir) ``` +## Using GameTime + +Once the setup is complete, you can use GameTime to analyze the worst-case execution time (WCET) of your C programs. + +### Command Line Interface + +GameTime provides a command-line interface for easy WCET analysis: + +```bash +gametime [options] +``` + +**Options:** +- `-b, --backend {flexpret,x86,arm}` - Choose execution backend (required if not in config) +- `--no-clean` - Keep temporary files for debugging +- `-h, --help` - Show help message + +**Note:** Make sure to source the environment file before running gametime: + +```bash +source env.bash +``` + +### Preparing a Test Case + +To analyze a C program with GameTime, you need: + +1. **A C source file** containing the function you want to analyze +2. **A configuration file** (`config.yaml`) in the same directory + +#### Configuration File Template + +Create a `config.yaml` file in your program's directory: + +```yaml +--- +gametime-project: + file: + location: your_program.c # Your C source file + analysis-function: function_to_analyze # Function name to analyze + additional-files: [helper.c] # Optional: additional source files + start-label: null # Optional: start analysis at label + end-label: null # Optional: end analysis at label + + preprocess: + include: null # Optional: directories with headers + merge: null # Optional: files to merge + inline: yes # Inline function calls (recommended) + unroll-loops: yes # Unroll loops (recommended) + + analysis: + maximum-error-scale-factor: 10 + determinant-threshold: 0.001 + max-infeasible-paths: 100 + ilp-solver: glpk # ILP solver to use + backend: flexpret # Backend: flexpret, x86, or arm +``` + +#### Example: Simple C Program + +Create a directory with your program and config: + +``` +my_program/ +├── example.c +└── config.yaml +``` + +**example.c:** +```c +int compute(int x) { + if (x > 10) { + return x * 2; + } else if (x > 5) { + return x + 10; + } else { + return x; + } +} +``` + +**config.yaml:** +```yaml --- +gametime-project: + file: + location: example.c + analysis-function: compute + + preprocess: + inline: yes + unroll-loops: yes + + analysis: + ilp-solver: glpk + backend: flexpret +``` + +### Running Analysis -## Running Tests +After preparing your test case, run the analysis: -Once the setup is complete, you can run tests within the Gametime environment. Follow these steps to configure and execute your tests: +```bash +# Make sure to source the environment first +source env.bash -### 1. Configure the YAML File +# Run analysis +gametime my_program --backend flexpret +``` -Each test requires a YAML configuration file. Ensure that your YAML file is correctly set up with all the necessary test configurations. +### Understanding the Output -### 2. Create a Test Class +GameTime will display: -Navigate to the `wcet_test.py` file and create a new test class based on one of the available backend configurations. Specify the path to your YAML configuration file in the `config_path` attribute. +1. **Preprocessing progress**: Compilation, inlining, loop unrolling +2. **DAG generation**: Control flow graph construction +3. **Basis paths**: Initial set of representative paths +4. **Path generation**: Additional paths discovered +5. **Measurements**: Execution time for each path +6. **Final results**: WCET and the worst-case path -#### Example: +Example output: -```python -class TestBinarysearchARM(TestARMBackend): - config_path = "./programs/binarysearch/config.yaml" ``` +============================================================ +GAMETIME ANALYSIS RESULTS +============================================================ +Function analyzed: compute +Backend: flexpret +Number of basis paths: 3 +Number of generated paths: 8 + +Basis Paths: + 0: gen-basis-path-row0-attempt0 = 62 + 1: gen-basis-path-row1-attempt1 = 61 + 2: gen-basis-path-row2-attempt2 = 38 + +Generated Paths: + 0: path0 = 62 *WCET* + 1: path1 = 62 *WCET* + 2: path2 = 61 + 3: path3 = 61 + 4: path4 = 38 + 5: path5 = 38 + 6: path6 = 38 + 7: path7 = 38 + +Worst-Case Execution Time (WCET): 62 +WCET Path: path0 +============================================================ + +Analysis completed successfully! +``` + +### Available Backends -### 3. Add the Test Class to the Main Function +- **flexpret**: Uses the FlexPRET RISC-V emulator for precise timing measurements (recommended for embedded systems) +- **x86**: Uses the x86 host machine for timing measurements +- **arm**: Uses the ARM host machine for timing measurements -In the `main` function of `wcet_test.py`, add your newly created test class to the suite for execution. +### Example Commands -#### Example: +```bash +# Analyze with FlexPRET backend +gametime test/tacle_test/programs/if_elif_else --backend flexpret + +# Keep temporary files for debugging +gametime test/tacle_test/programs/if_elif_else --backend flexpret --no-clean -```python -suite.addTests(loader.loadTestsFromTestCase(TestBinarysearchARM)) +# Specify config file directly +gametime test/tacle_test/programs/if_elif_else/config.yaml --backend flexpret ``` -### 4. Run the Test +### Exploring Example Programs -Run the test using the following command: +GameTime includes several example programs in the `test` directory: ```bash -python wcet_test.py +# List available examples +ls test/tacle_test/programs/ +ls test/flexpret_test/programs/ + +# Run an example +gametime test/tacle_test/programs/if_elif_else --backend flexpret ``` ---- ## License This project is licensed under the terms of the [MIT License](LICENSE). ---- ## Contact If you have any questions or encounter any issues, please open an issue on the GitHub repository or reach out to the project maintainers. ---- By following these instructions, you should be able to get Gametime up and running on your machine. Happy coding! diff --git a/setup.py b/setup.py index 0a9cdaad..19f64eab 100644 --- a/setup.py +++ b/setup.py @@ -5,4 +5,15 @@ version='0.1.0', packages=find_packages(where='src'), package_dir={'': 'src'}, + entry_points={ + 'console_scripts': [ + 'gametime=cli:main', + ], + }, + python_requires='>=3.10', + author='Berkeley Learn and Verify Group', + description='Worst-Case Execution Time (WCET) Analysis Tool', + long_description=open('README.md').read(), + long_description_content_type='text/markdown', + license='MIT', ) \ No newline at end of file diff --git a/src/analyzer.py b/src/analyzer.py index d507b118..24b8666f 100644 --- a/src/analyzer.py +++ b/src/analyzer.py @@ -104,7 +104,15 @@ def __init__(self, project_config: ProjectConfiguration): self.dag_path: str = "" - backend_dict = {"Flexpret": FlexpretBackend, "X86": X86Backend, "ARM": ArmBackend} + backend_dict = { + "flexpret": FlexpretBackend, + "x86": X86Backend, + "arm": ArmBackend, + # Keep legacy capitalized names for backward compatibility + "Flexpret": FlexpretBackend, + "X86": X86Backend, + "ARM": ArmBackend + } if self.project_config.backend not in backend_dict: raise GameTimeError("No valid backend specified") diff --git a/src/cli.py b/src/cli.py new file mode 100644 index 00000000..e55ef4c8 --- /dev/null +++ b/src/cli.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python +""" +GameTime Command Line Interface + +This module provides a command-line interface for running GameTime analysis +on C programs to determine worst-case execution time (WCET). +""" + +import argparse +import os +import sys +import shutil +from typing import Optional + +# Add the src directory to the path to allow imports +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) + +from project_configuration import ProjectConfiguration +from project_configuration_parser import YAMLConfigurationParser +from analyzer import Analyzer +from defaults import logger +from gametime_error import GameTimeError + + +def find_config_file(path: str) -> Optional[str]: + """ + Find the config.yaml file in the given path. + + Parameters: + path: str + Path to search for config file (can be a directory or a file) + + Returns: + Optional[str]: Path to config.yaml if found, None otherwise + """ + # If path is a file and it's a yaml file, return it + if os.path.isfile(path) and path.endswith(('.yaml', '.yml')): + return path + + # If path is a directory, look for config.yaml + if os.path.isdir(path): + config_path = os.path.join(path, 'config.yaml') + if os.path.exists(config_path): + return config_path + + # Also try config.yml + config_path = os.path.join(path, 'config.yml') + if os.path.exists(config_path): + return config_path + + return None + + +def run_gametime(config_path: str, clean_temp: bool = True, backend: str = None) -> int: + """ + Run GameTime analysis on the specified configuration. + + Parameters: + config_path: str + Path to the configuration file + clean_temp: bool + Whether to clean temporary files before running (default: True) + backend: str + Override backend from config (default: None, use config value) + + Returns: + int: Exit code (0 for success, non-zero for failure) + """ + try: + # Parse the configuration file + logger.info(f"Loading configuration from: {config_path}") + project_config: ProjectConfiguration = YAMLConfigurationParser.parse(config_path) + + # Override backend if specified + if backend: + logger.info(f"Overriding backend with: {backend}") + project_config.backend = backend + + # Check if backend is specified + if not project_config.backend: + logger.error("Error: No backend specified!") + logger.error("Please specify a backend in the config file or use --backend option") + logger.error("Available backends: flexpret, x86, arm") + return 1 + + # Clean temporary directory if requested + if clean_temp and os.path.exists(project_config.location_temp_dir): + logger.info(f"Cleaning temporary directory: {project_config.location_temp_dir}") + shutil.rmtree(project_config.location_temp_dir) + + # Create the analyzer + logger.info("Creating analyzer...") + analyzer: Analyzer = Analyzer(project_config) + + # Create the DAG + logger.info("Creating control flow graph (DAG)...") + analyzer.create_dag() + + # Generate basis paths + logger.info("Generating basis paths...") + basis_paths = analyzer.generate_basis_paths() + + if not basis_paths or len(basis_paths) == 0: + logger.error("No basis paths were found!") + return 1 + + logger.info(f"Found {len(basis_paths)} basis path(s)") + + # Measure basis paths + logger.info("Measuring basis paths...") + for i, path in enumerate(basis_paths): + value = path.get_measured_value() + logger.info(f" Basis path {i}: {path.name} = {value}") + + # Generate additional paths for analysis + logger.info("Generating additional paths for analysis...") + generated_paths = analyzer.generate_paths() + logger.info(f"Generated {len(generated_paths)} path(s) for measurement") + + # Measure generated paths + logger.info("Measuring generated paths...") + results = [] + for i, path in enumerate(generated_paths): + output_name: str = f'path{i}' + value = analyzer.measure_path(path, output_name) + results.append((path.name, value)) + + # Display results + logger.info("\n" + "="*60) + logger.info("GAMETIME ANALYSIS RESULTS") + logger.info("="*60) + logger.info(f"Function analyzed: {project_config.func}") + logger.info(f"Backend: {project_config.backend if project_config.backend else 'default'}") + logger.info(f"Number of basis paths: {len(basis_paths)}") + logger.info(f"Number of generated paths: {len(generated_paths)}") + + logger.info("\nBasis Paths:") + for i, path in enumerate(basis_paths): + logger.info(f" {i}: {path.name} = {path.get_measured_value()}") + + if results: + logger.info("\nGenerated Paths:") + max_value = max(value for _, value in results) + max_path = [name for name, value in results if value == max_value][0] + + for i, (name, value) in enumerate(results): + marker = " *WCET*" if value == max_value else "" + logger.info(f" {i}: {name} = {value}{marker}") + + logger.info(f"\nWorst-Case Execution Time (WCET): {max_value}") + logger.info(f"WCET Path: {max_path}") + + logger.info("="*60) + logger.info("\nAnalysis completed successfully!") + + return 0 + + except GameTimeError as e: + logger.error(f"GameTime Error: {str(e)}") + return 1 + except Exception as e: + logger.error(f"Unexpected error: {str(e)}") + import traceback + traceback.print_exc() + return 1 + + +def main(): + """Main entry point for the GameTime CLI.""" + parser = argparse.ArgumentParser( + description='GameTime - Worst-Case Execution Time (WCET) Analysis Tool', + formatter_class=argparse.RawDescriptionHelpFormatter, + epilog=""" +Examples: + # Run analysis on a folder containing config.yaml + gametime /path/to/test/folder + + # Run analysis with a specific config file + gametime /path/to/config.yaml + + # Run analysis with a specific backend + gametime /path/to/test/folder --backend x86 + + # Run analysis without cleaning temporary files + gametime /path/to/test/folder --no-clean + """ + ) + + parser.add_argument( + 'path', + help='Path to test folder (containing config.yaml) or path to config file' + ) + + parser.add_argument( + '--no-clean', + action='store_true', + help='Do not clean temporary files before running' + ) + + parser.add_argument( + '-b', '--backend', + choices=['flexpret', 'x86', 'arm'], + help='Backend to use for execution (overrides config file)' + ) + + parser.add_argument( + '--version', + action='version', + version='GameTime 0.1.0' + ) + + args = parser.parse_args() + + # Validate the path + if not os.path.exists(args.path): + logger.error(f"Error: Path does not exist: {args.path}") + return 1 + + # Find the config file + config_path = find_config_file(args.path) + if not config_path: + logger.error(f"Error: Could not find config.yaml in: {args.path}") + logger.error("Please ensure the directory contains a config.yaml or config.yml file") + return 1 + + # Run GameTime analysis + exit_code = run_gametime( + config_path, + clean_temp=not args.no_clean, + backend=args.backend + ) + + return exit_code + + +if __name__ == '__main__': + sys.exit(main()) + diff --git a/src/gametime.egg-info/PKG-INFO b/src/gametime.egg-info/PKG-INFO deleted file mode 100644 index fdf9c4ef..00000000 --- a/src/gametime.egg-info/PKG-INFO +++ /dev/null @@ -1,3 +0,0 @@ -Metadata-Version: 2.1 -Name: gametime -Version: 0.1.0 diff --git a/src/gametime.egg-info/SOURCES.txt b/src/gametime.egg-info/SOURCES.txt deleted file mode 100644 index 196a1f5c..00000000 --- a/src/gametime.egg-info/SOURCES.txt +++ /dev/null @@ -1,20 +0,0 @@ -README.md -setup.py -src/backend/__init__.py -src/backend/backend.py -src/backend/generate_executable.py -src/backend/arm_backend/__init__.py -src/backend/arm_backend/arm_backend.py -src/backend/flexpret_backend/__init__.py -src/backend/flexpret_backend/flexpret_backend.py -src/backend/x86_backend/__init__.py -src/backend/x86_backend/x86_backend.py -src/gametime.egg-info/PKG-INFO -src/gametime.egg-info/SOURCES.txt -src/gametime.egg-info/dependency_links.txt -src/gametime.egg-info/top_level.txt -src/smt_solver/__init__.py -src/smt_solver/extract_klee_input.py -src/smt_solver/extract_labels.py -src/smt_solver/smt.py -src/smt_solver/to_klee_format.py \ No newline at end of file diff --git a/src/gametime.egg-info/dependency_links.txt b/src/gametime.egg-info/dependency_links.txt deleted file mode 100644 index 8b137891..00000000 --- a/src/gametime.egg-info/dependency_links.txt +++ /dev/null @@ -1 +0,0 @@ - diff --git a/src/gametime.egg-info/top_level.txt b/src/gametime.egg-info/top_level.txt deleted file mode 100644 index 92b3fb0b..00000000 --- a/src/gametime.egg-info/top_level.txt +++ /dev/null @@ -1,2 +0,0 @@ -backend -smt_solver diff --git a/src/smt_solver/smt.py b/src/smt_solver/smt.py index 4abc1dd8..914ef17e 100644 --- a/src/smt_solver/smt.py +++ b/src/smt_solver/smt.py @@ -57,7 +57,7 @@ def compile_and_run_cplusplus(modify_bit_code_cpp_file, modify_bit_code_exec_fil # Run the compiled program # TODO: change modify bc to take in bc file, not c file - run_command = ['./' + modify_bit_code_exec_file, input_bc_file, labels_file, all_labels_file, func_name] + run_command = [modify_bit_code_exec_file, input_bc_file, labels_file, all_labels_file, func_name] subprocess.run(run_command, check=True) return f"{input_bc_file[:-3]}_gvMod.bc" @@ -128,9 +128,10 @@ def run_smt(project_config: ProjectConfiguration, labels_file: str, output_dir: klee_file_path = format_for_klee(c_file, c_file_path, output_dir, number_of_labels, total_number_of_labels, project_config.func) # insert assignments of global variables - # TODO: Find a way to not hard code path - modify_bit_code_cpp_file = '../../src/smt_solver/modify_bitcode.cpp' - modify_bit_code_exec_file = '../../src/smt_solver/modify_bitcode' + # Get the path to the smt_solver directory relative to this file + smt_solver_dir = os.path.dirname(os.path.abspath(__file__)) + modify_bit_code_cpp_file = os.path.join(smt_solver_dir, 'modify_bitcode.cpp') + modify_bit_code_exec_file = os.path.join(smt_solver_dir, 'modify_bitcode') modified_klee_file_bc = 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) # run klee diff --git a/test/tacle_test/wcet_test.py b/test/tacle_test/wcet_test.py index 36d3ce7a..88493425 100644 --- a/test/tacle_test/wcet_test.py +++ b/test/tacle_test/wcet_test.py @@ -59,11 +59,11 @@ def test_wcet_analyzer(self): ##### Backend classes class TestFlexpretBackend(BaseTest): - backend_value = "Flexpret" + backend_value = "flexpret" class TestX86Backend(BaseTest): - backend_value = "X86" + backend_value = "x86" class TestARMBackend(BaseTest): - backend_value = "ARM" + backend_value = "arm" #### Benchmarks @@ -139,7 +139,9 @@ class TestDeg2RadFlexpret(TestFlexpretBackend): suite = unittest.TestSuite() #Programs - suite.addTests(loader.loadTestsFromTestCase(TestBinarysearchFlexpret)) + suite.addTests(loader.loadTestsFromTestCase(TestIfElifElseFlexpret)) + + # suite.addTests(loader.loadTestsFromTestCase(TestBinarysearchFlexpret)) # suite.addTests(loader.loadTestsFromTestCase(TestBitcnt2Flexpret)) # suite.addTests(loader.loadTestsFromTestCase(TestPrimeFlexpret)) # suite.addTests(loader.loadTestsFromTestCase(TestIfElifElseX86))