Running PathFinder

The following contains instructions for the usage of PathFinder. You will find the pathfinder binaries at the root of the install folder.

Basic use

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.

  • -3 is the most recent, best module. It uses modular analysis with composable states and has all the latest developments.

  • -2 does not make use of contextual analysis, but uses a similar abstract interpretation domain as -3.

  • -1 purely 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

Options are documented if you run pathfinder -h. You are most likely only interested in the following:

Complexity control

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

  • --automerge, -a let 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:

  • --merge, -m merge 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:

  • --clamp_predicates, --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):

  • --maf, --merge-after-apply (optimization) allow the algorithm to merge immediately after applying

If you are not interested in the infeasible paths output:

  • --slice slice 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 -p.

Verbose

  • --s0, --vv, -V: high verbose, run with maximal output

  • --s1, -s low verbose, only display results

  • --s2, -S zero verbose, run with no output

  • --progress, -p display analysis progress (forces --s1 or higher)

Other

  • --nc, --no-color, --no-colors do not use colors. PathFinder is very colorful by default

  • --src-info, -i print file/line number info

  • --nir, --no-ip-results do not print the list of IPs found

  • --nl, --no-line-nb do not number lines of the output

  • --detailed-stats, --ds display detailed stats, including average length of infeasible_paths found etc.

  • --loop-bounds, -l ONLY 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, -o output the result of the analysis to a FFX file

You may also want to get some stats in a .tsv file:

  • --graph-output, -g also output as a gnuplot .tsv graph file (requires -o)

Other

If you are running into crashes due to irregular loops:

  • --reduce reduce irregular loops

If you want to run quickly through the program without the infeasible path detection bit:

  • --dry, -d dry run (no solver calls)

If you need to provide additional flow facts to PathFinder, use this OTAWA-inherited option:

  • --flowfacts, -f PATH select the flowfacts to load

If you run into assert failures:

  • --dasp, --dont-assume-id-sp do not assume sp = SP0 at the end of a function

  • --deterministic, -D Ensure 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-critical Abort analysis on loss of SP info
Last updated on Sep 9, 2018