Documentation
¶
Overview ¶
Souffle-based static race detector for Go.
The program iterates through the SSA for the given Go module or Go source file, and produces fact files that encode various information about the Go source program. These fact files are later consumed by Souffle Datalog when computing other facts, e.g., the point-to information between memory allocations, which functions are reachable, possible data races. Finally, the Souffle-generated facts are read back into the driver which prints user-friendly analysis results onto screen.
For easier debugging, a _generated_facts.log file is also created when the analysis driver runs, that illustrate the line-by-line correspondence between an original SSA instruction and the generated facts about it.
Usage:
go run main.go [flags] [source ...]
The flags are:
-mod The path to the Go module to be analyzed.
-ssaline Print the line-by-line SSA and the generated fact, for debugging.
-ssafunc Before printing the debugging information for each instruction in a function, print SSA for the whole function using the Go ssa package.
-souffle-path Path to the souffle executable.
-souffle-analysis Path to the main souffle analysis (.dl).
-output Path to a directory used to store the generated facts.
-roots-path Provide a csv file for the entry functions to analyze. Each function is on a separate line. A default root file would be a csv with just one line that indicates analysis starts with the main function in the main package, or "main.main".
-threads Provide number of threads that is used to run the Souffle engine.
Source Files