-
Notifications
You must be signed in to change notification settings - Fork 4
Commands
Convert a file containing source code to a Graph object. If a directory is passed as an argument, all source code within that directory will be converted. The recursive flag (-r) can also be used to convert all files in a given directory or any of its subdirectories.
Note - Language Support:
The REPL current supports C/C++ (using clang6), Java (JDK13), and Python 3. C/C++ and Java code yields block-level CFGs while Python 3 results in statement level CFGs. Keep in mind that only a subset of Python 3 keywords / features are supported: assignment, expressions (e.g. 'a + b'), if/else/elif, return, while, and with (NOTE: this does not include list/dictionary comprehensions, lambda expressions, or try/catch/raise).
Usage: convert <file-like>
convert -r <file-like>
convert <file-like-1> <file-like-2> ... <file-like-n>
Delete an object (type graph, metric, or klee_stat, klee_bc, klee_file, or klee) from memory. The wildcard operator * is also supported for 'type'. Using the klee type deletes all klee-related objects with that name.
Usage: delete <type> <name>
Import a .dot graph file as a graph object. Similar to convert, if a directory
of .dot files is passed as an argument, all graphs will be imported.
The recursive flag (-r) can also be used to import all graphs from a directory
and subdirectories.
Usage:
import <file-like>
import -r <file-like>
import <file-like-1> <file-like-2> ... <file-like-n>
Save an object (type graph, metric, klee_bc, klee_file, or klee) to an output file. Using type klee exports all klee-related objects with that name.
Usage: export <type> <name>
List all of the objects of a specific type (metric, graph, klee_bc, klee_stat, klee_file, or klee). The wildcard operator * is also supported for type. Using the klee type lists all klee-related objects - organized by type.
Usage: list <type>
Compute all of the complexity matrics for a Graph object. This currently computes Cyclomatic Complexity, NPath Complexity, and Path Complexity / Asymptotic Path Complexity. The wildcard operator * is supported for names.
Usage: metrics <name>
Reloads command definitions in the module (only works in debug mode) while presenting objects in the REPL. This is an easy way to verify that a change to a command works without having to restart the REPL (causing all objects to be deleted).
Usage: reload
Print out a representation of an object of some type (metric, graph, klee_bc, klee_file, klee_stat, or klee).
The wildcard operator * is spported for type and name.
Type klee will show all klee-related objects with the given name.
The object names can be obtained with list.
Usage: show <type> <name>
Quits the path complexity repl. This is the recommended way to exit as it guaranteeds that the command history will be preserved for the next time the REPL is executed.
Before KLEE can be executed on C source code, we must specify which variables are symbolic and which functions we want to test.
While this process can be done manually, which may give users more granular control of KLEE behavior, the klee utilities in the REPL
cover general use cases. The command to_klee_format looks through C source files, finds all function definitions, and creates a new
source file that contains main(), which marks of the arguments in the original function definitions as symbolic and then calls those
functions. Functions that take user input may need to be refactored. Further, functions that rely on imports must be dealt with more carefully -
i.e. ensure that KLEE can find all of the required files by adding the appropriate paths and fake headers to the path environment variable.
Once in this format, call klee_to_bc to convert this modified C source into a .bc file. Then, call klee on the output from the previous command.
Create a klee-compatible file.
Given a C file, create a new modified C file that is in the correct format to be converted to a bc file.
Given a C file in the correct format, generate a new .bc file from the given C file.
Execute a test generated by KLEE given a klee test file.
Usage: klee_replay
Execute the klee command on a .bc file.
This will generate all of the tests automatically and store the resulting metadata (e.g. number of tests generated).
Usage: klee
Many of the basic commands used for navigating around files in typical shells also work in the REPL. We currently support cd, ls, mv, rm, mkdir, and pwd.