boogie

NAME

boogie - compiler for the Boogie programming language

boogie is a compiler for Microsoft Research's Boogie programming language, an imperative compiler intermediate language with built-in specification constructs. The integrated static analyzer can verify functional correctness as part of the compilation process.

OPTIONS

boogie accepts a number of different types of options.

File macros

A number of boogie options accept a file argument, which may contain the following macros:

@FILE@: Expands to the last filename specified on the command line.

@PREFIX@: Expands to the concatenation of strings given by /logPrefix options.

@TIME@: Expands to the current time.

General options

/env:n: Control printing of command-line arguments. Accepted values for n are:

0: Suppress printing of command-line arguments.

1: (default) Print command-line arguments during BPL print and prover log.

2: Print command-line arguments during BPL print and prover log, and also to standard output.

/noLogo: Suppress printing of the version number and copyright message.

/wait: Wait for a carriage return from the keyboard before exiting.

/xml:file: Also produce output in XML format to file.

Boogie options

Multiple .bpl files supplied on the command line are concatenated into one Boogie program.

/enhancedErrorMessages:n: Control printing of enhanced error messages. Accepted values for n are:

0: (default) Do not print enhanced error messages.

1: Print Z3 error model enhanced error messages.

/loopUnroll:n: Unroll loops, following up to n back edges (and then some).

/mv:file: Save the model in BVD format to the specified file.

/noResolve: Parse only.

/noTypecheck: Parse and resolve only.

/overlookTypeErrors: Skip any implementation with resolution or type checking errors.

/print:file: Print Boogie program to the specified file after parsing it. Specify /print:- to print to standard output.

/printCFG:prefix: Print the control flow graph of each implementation in dot(1) format to files named prefix.procedurename.dot.

/printDesugared: With /print, desugar calls.

/printModel:n: Control printing of Z3's error model. Accepted values for n are:

0: (default) Do not print Z3's error model.

1: Print Z3's error model.

2: Print Z3's error model and reverse mappings.

3: Print Z3's error model in a more human-readable way.

/printModelToFile:file: With /print, print Z3's error model to file instead of standard output.

/printUnstructured: With /print, desugar all structured statements.

/printWithUniqueIds: Print augmented information that uniquely identifies variables.

/proc:p: Only check procedures matched by the pattern p. This option may be specified multiple times to match multiple patterns. The pattern p matches the whole procedure name (e.g., a pattern "foo" will only match a procedure called "foo", not one called "fooBar"). The pattern p may contain * wildcards which match any character zero or more times. For example, the pattern "ab*d" would match "abd", "abcd", and "abccd", but not "Aabd" or "abdD". The pattern "*ab*d*" would match "abd", "abcd", "abccd", "Abd", and "abdD".

/soundLoopUnrolling: Enable sound loop unrolling.

/useBaseNameForFileName: When parsing, use the base name of the file for tokens instead of the path supplied on the command line.

Inference options

/checkInfer: Instrument inferred invariants as asserts to be checked by the theorem prover.

/contractInfer: Perform procedure contract inference.

/infer[:domains]: Use abstract interpretation to infer invariants. domains may be any of the following:

c: constant propagation

d: dynamic type

i: intervals

j: stronger intervals (cannot be combined with other domains)

n: nullness

p: polyhedra for linear inequalities

t: trivial bottom/top lattice (cannot be combined with other domains)

: You may also specify the following options as pseudo-domains:

s: debug statistics

0...9: number of iterations before applying a widen (default: 0)

: The default is /infer:i. With /infer (and no domains), all domains will be used.

/instrumentInfer:flag: Control when inferred invariants are instrumented. Accepted values for flag are:

h: (default) Instrument inferred invariants only at the beginning of loop headers.

e: Instrument inferred invariants at the beginning and end of every block. This mode is intended for use in debugging abstract domains.

/noinfer: Turn off the default inference, and override any previous /infer flags.

/printInstrumented: Print Boogie program after it has been instrumented with invariants.

Debugging and tracing options

/break: Launch and break into the debugger.

/log[:method]: Print debug output during translation.

/trace: Blurt out various debug trace information. Implies /tracePOs.

/tracePOs: Output information about the number of proof obligations.

/traceTimes: Output timing information at certain points in the pipeline.

Verification condition generation options

/alwaysAssumeFreeLoopInvariants: Include free loop invariants as assumptions in checking contexts. Usually, a free loop invariant (or assume statement in that position) is ignored in checking contexts (like other free things).

/causalImplies: Translate Boogie's A ==> B into prover's A ==> A && B.

/coalesceBlocks:n: Control when to coalesce blocks. Accepted values for n are:

0: Do not coalesce blocks.

1: (default) Coalesce blocks.

/fixedPointEngine:engine: Use the specified fixed point engine for inference.

/inferLeastForUnsat:prefix: Infer the least number of constants (whose names are prefixed by prefix) that need to be set to true for the program to be correct. Implies /stratifiedInline:1.

/inline:strategy: Use the specified inlining strategy for procedures with the :inline attribute. Accepted strategies are none, assume (the default), assert, and spec.

/lazyInline:1: Use the lazy inlining algorithm.

/liveVariableAnalysis:n: Control when and how to perform live variable analysis. Accepted values for n are:

0: Do not perform live variable analysis.

1: (default) Perform live variable analysis.

2: Perform interprocedural live variable analysis.

/monomorphize: Do not abstract map types in the encoding. This is an experimental feature which will not do the right thing if the program uses polymorphism.

/noVerify: Skip verification condition generation and invocation of the theorem prover.

/printInlined: Print the implementation after inlining calls to procedures with the :inline attribute.

/recursionBound:n: Set the recursion bound for stratified inlining to n. By default, n is 500.

/reflectAdd: In the verification condition, generate an auxiliary symbol, elsewhere defined to be +, instead of +.

/removeEmptyBlocks:n: Control whether to remove empty blocks during verification condition generation. Accepted values for n are:

0: Do not remove empty blocks.

1: (default) Remove empty blocks.

/smoke: Run the soundness smoke test: try to stick assert false; in some places in the BPL and see if we can still prove it.

/smokeTimeout:n: Set the timeout, in seconds, for a single theorem prover invocation during the smoke test. By default, n is 10.

/stratifiedInline:1: Use the stratified inlining algorithm.

/subsumption:n: Control when subsumption is applied to asserted conditions. Accepted values for n are:

0: Never apply subsumption.

1: Do not apply subsumption for quantifiers.

2: (default) Always apply subsumption.

/traceverify: Print debug output during verification condition generation.

/typeEncoding:method: Control how to encode types when sending the verification condition to the the theorem prover. Allowed methods are:

a: arguments

m: monomorphic

n: none (unsound)

p: (default) predicates

/vc:variety: Specify the verification condition variety. Accepted varieties are:

b: flat block

d: (default) DAG

doomed: doomed

l: local

m: nested block reach

n: nested block

r: flat block reach

s: structured

/verifySeparately: Verify each input program separately.

/verifySnapshots:n: Verify several program snapshots (named filename.v0.bpl to filename.vN.bpl), possibly using verification result caching. Accepted values for n are:

0: (default) Do not use any verification result caching.

1: Use basic verification result caching.

2: Use advanced verification result caching.

3: Use advanced verification result caching, and report errors according to the new source locations for errors and their related locations (but not /errorTrace and CaptureState locations).

Verification condition splitting

/vcsCores:n: Try to verify n verification conditions at once. Defaults to 1.

/vcsDumpSplits: For the nth split, dump split.n.dot and split.n.bpl. Note that this affects error reporting.

/vcsFinalAssertTimeout:n: Set the timeout, in seconds, for the single last assertion in keep-going mode. By default, n is 30.

/vcsKeepGoingTimeout:n: Set the timeout, in seconds, for a single theorem prover invocation in keep-going mode, except for the final single-assertion case. By default, n is 1.

/vcsLoad:f: Like /vcsCores:n, where n is the machine's processor count multiplied by f and rounded to the nearest integer. f must be in the range [0.0, 3.0]. This will never set n less than 1.

/vcsMaxCost:f: Verification conditions will not be split unless the cost of a verification condition exceeds f. f defaults to 2000.0. This does not apply in the keep-going mode after the first round of splitting.

/vcsMaxKeepGoingSplits:n: If n is set to more than 1, this activates keep-going mode, where after the first round of splitting, verification conditions that time out are split into n pieces and retried until either proving them is successful or there is only one assertion on a single path and it times out. (In such a case, boogie reports an error for that assertion). By default, n is 1 (that is, keep-going mode is disabled).

/vcsMaxSplits:n: Set the maximal number of verification conditions generated per method. In keep-going mode, this only applies to the first round. By default, n is 1.

/vcsPathCostMult:f1, /vcsAssumeMult:f2: Controls the cost of a block. Block cost is computed according to the formula

: ( assert-cost + f2 × assume-cost) × (1 + f1 × entering-paths)

: where f1 defaults to 1.0 and f2 defaults to 0.01. The cost of a single assertion or assumption is always 1.0.

/vcsPathJoinMult:f: Sets a scale factor which boogie will multiply by the number of paths in a block if more than one path join at a block. This is intended to reflect the fact that the prover will learn something on one path before proceeding to the next. By default, f is 0.8.

/vcsPathSplitMult:f: If the best path split of a verification condition of cost A is into verification conditions of cost B and C, then the split is applied if A ≥ f × (B + C). Otherwise, assertion splitting will be applied. By default, f is 0.5 (that is, always do path splitting if possible). Increase f to do less path splitting and more assertion splitting.

Prover options

/errorLimit:n: Limit the number of errors produced for each procedure. By default, n is 5, but some provers may only support 1.

/errorTrace:n: Control whether or not trace labels appear in the error output. Accepted values for n are:

0: Print no trace labels in the error output.

1: (default) Print useful trace labels in error output.

2: Print all trace labels in error output.

/logPrefix:prefix: Define the expansion of the macro @PREFIX@.

/p:key[:value], /proverOpt:key[: value]: Provide a prover-specific option.

/platform:ptype,location: Set the platform type and location. ptype may be v11, v2, or cli1, and location should be the platform libraries directory.

/prover:p: Use theorem prover p. p may be a full path to a prover DLL, or it may be one of the following standard provers:

ContractInference

Simplify: This implies /vc:n and /vcBrackets:1.

SMTLib: (default) Use the SMTLib2 format, and call Z3.

Z3: Z3 with the Simplify format.

Z3api: Z3 with the managed (CLI) API.

/proverLog:file: Log input for the theorem prover.

: In addition to the standard file name macros, file can use the @PROC@ macro, which causes boogie to generate one prover log file per verification condition, expanding @PROC@ to the name of the procedure that the verification condition is for.

/proverLogAppend: Append (do not overwrite) the specified prover log file.

/proverMemorylimit:n: Limit the prover to n megabytes of virtual memory before forcing it to restart. n defaults to 100.

/proverShutdownLimitn: Set the time, in seconds, between closing the stream to the prover and killing the prover process. n defaults to 0.

/proverWarnings:n: Control warning output from the prover. Accepted values for n are:

0: (default) Don't print warning output from the prover.

1: Print warnings to standard output.

2: Print warnings to standard error.

/restartProver: Restart the prover after each query.

/timeLimit:n: Limit the number of seconds spent trying to verify each procedure.

/vcBrackets:n: Control whether or not odd-charactered identifier names will be bracketed with pipe characters ('|'). Accepted values for n are:

0: (default) Do not bracket odd-charactered identifier names.

1: Bracket odd-charactered identifier names.

Prover options (Simplify)

/simplifyMatchDepth:n: Set Simplify's matching depth limit.

Prover options (Z3)

/useArrayTheory: Use Z3's native array theory, as opposed to axioms. Implies /monomorphize.

/useSmtOutputFormat: Output a model in SMTLib2 format.

/z3exe:path: Set the path to the Z3 executable. On Debian systems, this defaults to /usr/bin/z3.

/z3lets:n: Configure use of LETs in Z3. Accepted values for n are:

0: Do not use LETs.

1: Use only LET TERM.

2: Use only LET FORMULA.

3: (default) Use any LET.

/z3multipleErrors: Report multiple counterexamples for each error.

/z3opt:option: Set an additional Z3 option.

/z3types: Generate a multi-sorted verification condition that makes use of Z3 types.

COPYRIGHT

2016-08-17

Git snapshot 1f2d6c1