The following contains instructions for the usage of PathFinder. You will find the
pathfinder binaries at the root of the install folder.
Calls to PathFinder must follow the
pathfinder [OPTIONS] PROGRAM [FUNCTION] pattern. Options can be nested as long as they are one letter. Example:
pathfinder -3pa benchmarks/if_then_else_2seq.elf
Abstract interpretation modules
PathFinder comes with three abstract interpretation modules, named by their chronological order of development. Older versions are kept for academic interest.
-3is the most recent, best module. It uses modular analysis with composable states and has all the latest developments.
-2does not make use of contextual analysis, but uses a similar abstract interpretation domain as
-1purely uses symbolic predicates to represent program states. Warning: in order to run with
-1, you must configure the pathfinder build with
bam config v1=true.
You can run
pathfinder with no other options on binary files supported by OTAWA.
Options are documented if you run
pathfinder -h. You are most likely only interested in the following:
You will quickly find that PathFinder runs too slow (or runs out of memory) on even most basic programs. This is normal, because it does not by default use any merge algorithm to cope with the exponential complexity of the representation of the program it uses. Thankfully, there are options that allows PathFinder to make a tradeoff between precision and complexity and run on reasonably-sized programs.
You can set merge points using
-alet the algorithm decide when to merge
--automerge applies a merge when it runs into 250 or more states. You can adjust this number with the following option:
-mmerge when exceeding X states at a control point
On some of the largest benchmarks, another factor of complexity explosion is the size of predicates. If
--automerge does not suffice, add this option:
--cp(optimization) clamp predicates size (12 operands max)
If the analysis still takes too long, or too much memory, when using
-3, add this option (I think I did not have to use this on any of the Mälardalens):
--merge-after-apply(optimization) allow the algorithm to merge immediately after applying
If you are not interested in the infeasible paths output:
--sliceslice away instructions that do not impact the control flow (warning: removes infeasible paths!). This requires PathFinder to be configured with
bam config slice=true
Console output control
PathFinder comes with many options to control the console output, which is quite verbose and colorful by default. On larger benchmarks, I like using
-V: high verbose, run with maximal output
-slow verbose, only display results
-Szero verbose, run with no output
-pdisplay analysis progress (forces
--no-colorsdo not use colors. PathFinder is very colorful by default
--src-info, -iprint file/line number info
--no-ip-resultsdo not print the list of IPs found
--no-line-nbdo not number lines of the output
--dsdisplay detailed stats, including average length of infeasible_paths found etc.
-lONLY print loop bounds (no infeasible paths)
Outputting FFX results
PathFinder can output its results in a
***_ips.ffx file. You must set this flag for this:
--output, -ooutput the result of the analysis to a FFX file
You may also want to get some stats in a
-galso output as a gnuplot .tsv graph file (requires
If you are running into crashes due to irregular loops:
--reducereduce irregular loops
If you want to run quickly through the program without the infeasible path detection bit:
-ddry run (no solver calls)
If you need to provide additional flow facts to PathFinder, use this OTAWA-inherited option:
-f PATHselect the flowfacts to load
If you run into assert failures:
--dont-assume-id-spdo not assume sp = SP0 at the end of a function
-DEnsure deterministic output (two executions give the same output).
For debugging, as it is interesting to know when you lose the stack pointer (you probably won’t get any result afterwards):
--sp-criticalAbort analysis on loss of SP info