Copper User Manual

Introduction
Usage
Options

Introduction

The general goal of Copper is to verify that an implementation conforms to its specification. The implementation is always a C program and hence quite standard. However, Copper can be used to play around with several kinds of specifcations and notions of conformance. For a quick overview of how to start using Copper, check out the tutorial.

Back to Top

Usage

Copper is a command line tool. It is invoked with a set of options and input file names. The input files are either pre-processed C files with extension .pp or specification files with extension .spec. The C files must be pre-processed with CIL. The specification files must obey this grammar. The most basic way to run Copper is as follows:

copper --default --specification <specification name> <filenames>

The above invocation will cause Copper to check simulation conformance between the FSP specification identified by "specification name" and the program defined by the input C files. To verify SE-LTL specifications, use the following command line:

    copper --default --ltl --specification <specification name> <filenames>

Other common types of verification tasks are: (1) checking trace containment between a program and an FSP specification, and (2) checking for the unreachability of ERROR states in an FSP specification. These are achieved, respectively, by the following two command lines:

    copper --default --trace --specification <specification name> <filenames>

    copper --default --reach --specification <specification name> <filenames>

In reality, "--default" is just a synonym for the following set of options which, most often, appear to work best in practice:

    --useAllSpecs --ceShowAll --stat --cegar --symbolic

The general usage of Copper is:

    copper <option | filename> <option | filename> ...

In general, anything on the command line that begins with a minus sign is treated as an option. Everything else is treated either as an argument of the preceeding option or a filename. Later options take precedence over earlier ones whenever applicable. Thus, "--trace --reach" is equivalent to "--reach". Thus, "--default" should be one of the first options you supply to Copper. We now describe the set of all available Copper options in more detail. Options are grouped together into broad categories. Options within the same category are more closely related to each other than options belonging to a different category.

Back to Top

Options

In the following we write "by default" to mean the situation when no command line options are supplied to Copper, and not the situtation when the option "--default" is provided. The following options affect the global behavior of Copper.

--help or -h: Generate this help message and exit.
--specification <name>: The name of the specification to be verified.
--copperHome <copper home directory>: Home directory of the copper distribution. This value overwrites the COPPER environment variable, if set.
--parse: Only parse input files and exit.
--echo: Print characters as they are being parsed. This is helpful for debugging parse errors.
--stat: Display statistics at the end. Implied by "--default".
--verbose <level>: Set the verbosity level. Default is 2.
--timeLimit <number>: Time limit in seconds. Default value is 10000 hours.

The following options control the type of verification to be carried out. By default, Copper checks simulation between the C program and the specification.

--reach: Check ERROR state reachability instead of simulation.
--trace: Check trace containment instead of simulation.
--ltl: Do SE-LTL model checking.
--deadlock: Do deadlock detection.
--assert: Check iteratively for reachability of assertions of the form "assert(0)" in the program. In each iteration, Copper checks for the possible reachability of one such assertion.

In the rest of this document, we refer to trace containment, ERROR state reachability, and the detection of assertion failure collectively as "safety" verifications since all of them boil down to model checking safety properties. The following options control the verification mechanism used by Copper. By default, Copper uses a HORNSAT based model checker for simulation and safety verification, and an explicit state model checker for SE-LTL model checking and deadlock detection.

--explicit: Use explicit state model checking instead of HORNSAT for verification.
--symbolic: Use symbolic predicate abstraction to reduce the number of theorem prover calls. Implied by "--default". Use only for safety verification and SE-LTL model checking.
--bp: Generate boolean programs via abstraction and use BDDs for verification. Use only for safety verification and SE-LTL model checking.

The following options control the type of Assume-Guarantee reasoning done by Copper. By default, Copper does not perform Assume-Guarantee reasoning. Also, Assume-Guarantee reasoning is only supported for simulation, safety verification, and deadlock detection.

--ag: Do assume-guarantee reasoning with learning for verification.
--agc1a: Use circular rule 1A for assume-guarantee style reasoning.
--noAGReuse: Do not reuse counterexamples to candidate queries. This may increase the number of candidate queries.
--agOpt: Assume-guarantee reasoning with minimal assumption alphabet.
--agLazy: Assume-guarantee reasoning with lazy alphabet extension.

The following options control the degree of inlining used by Copper. By default, Copper inlines according to the "inline" directives in the specification files.

--inline: Inline all library routines whose code is available.
--pds: Use pushdown system models instead of inlining. Only use for safety verification and do not combine with "--bp".

The following options control the initial set of "seed" predicates used by Copper. Seed predicates are essentially branch conditions from which other predicates are inferred at various control flow points by propagating weakest preconditions. By default, there are no initial seed predicates and the only initial predicates are those appearing in the specification.

--autoPred: Automatically add all branches in the code as seed predicates.
--specSeed: Obtain initial seed predicates from spec files.

The following options control the abstraction refinement used by Copper. By default, Copper does no refinement and will terminate with the model checking result on the first abstract model.

--cegar: Do abstraction refinement without predicate optimization. Implied by "--default".
--optPred: Do pseudo-boolean constraint based predicate optimization.
--greedy: Do greedy predicate optimization. In some cases, this leads to quicker termination compared to "--optPred".
--usefulPred: Use only useful predicates for predicate discovery. A useful predicate is one appearing in a "predicate" directive in the specification files. This option enables the user to guide abstraction refinement by only allowing Copper to pick new "seed" predicates from those specified in the "predicate" directives. However, this mechanism is only useful if the user has some idea about the kinds of "seed" predicates on which the program's correctness is based.
--ceDag <number>: Use this many counterexamples in each iteration for refinement. Default is 1. If the argument after "--ceDag" is "n" then Copper generates "n" counterexamples during model checking and checks each of them for validity. If even one counterexample is found to be valid, Copper terminates with that real "bug". Otherwise, if all the counterexamples are found to be spurious, Copper refines the abstraction to eliminate all of them. Larger values of "n" may lead to quicker termination, but also to increased resource consumption.
--predLoop <number>: Number of times to go through a loop during predicate discovery. Default value is 1. Larger values will lead to more predicates being inferred from the same set of "seed" predicates, and hence a more precise model and more effective abstraction refinement. However, this may also lead to increased resource consumption.

The following options control the theorem prover used by Copper. The default theorem prover is Simplify.

--cprover: Use CProver as the theorem prover. This is the only appropriate option if you want support for full bit-level semantics and all C operators.
--cvc: Use CVC as the theorem prover. Only available on Linux.
--ics: Use ICS as the theorem prover. Only available on Linux.
--svc: Use SVC as the theorem prover. Only available on Linux.
--cvcl: Use CVC Lite as the theorem prover. Only available on Linux.
--vampyre: Use Vampyre as the theorem prover. This is experimental and only available on Linux.
--cogent: Use Cogent as the theorem prover. This is experimental.
--TPCache: Cache theorem prover queries and their results. This could increase memory requirement.
--TPCacheSize <size>: The size of the theorem prover cache. The cache is cleared if this size is exceeded. Default is 1000.

The following options control the SAT solvers used by Copper. By default, Copper uses ZChaff.

--sato: Use Sato as the SAT solver.
--grasp: Use FGrasp as the SAT solver.
--chaff: Use ZChaff as the SAT solver.

The following options control the information displayed as part of the counterexamples. By default, only the sequence of the control locations from the program that appear in the counterexample are displayed.

--ceShowAct: Show actions when displaying counterexamples.
--ceShowCons: Show propositional constraints when displaying counterexamples.
--ceShowAll: Show actions and propositional constraints when displaying counterexamples. Implied by "--default".

The following options control various statespace reduction techniques used by Copper for efficient verification.

--silentTrans: Don't eliminate silent transitions. By default, Copper eliminates silent transitions before model checking to make verification more efficient. A silent transition is defined to be one that does not change the value of any specification proposition, and is not labeled by any specification action. Eliminating silent transitions leads to a type of partial-order reduction by avoiding many possible thread interleavings during model checking.
--noParAssign: Disable parallel assignments. By default, Copper transforms a sequence of simple assignments into a single semantically equivalent parallel assignment. A parallel assignment is essentially a set of assignments executed concurrently. For example Copper translates the following sequence of assignments "temp = x; x = y; y = temp" into the parallel assignment "x = y || y = x || temp = x". Be aware that parallel assignments may lead to unsound results when the specification has propositions, and should be disabled in such cases.
--simParAssign: Use naive (but correct, even with pointers) strategy for parallelizing assignments.
--eager: Complete abstraction before model checking. The default is to abstract lazily on-the-fly during model checking.

The following options achieve miscellaneous purposes.

--checkCE: Check validity of counterexample if not doing abstraction refinement. This enables you to detect if the counterexample found by verifying the first abstract model is valid or spurious.
--useAllSpecs: Inline all library routine specifications. Overrides the default rule that only library specifications that contain synchronization or global specification actions are inlined. Implied by "--default".
--invariant: Compute invariants via static analysis. Invariants are used for subsequent abstraction and verification.
--pointers: Handle aliasing due to pointers.
--noSyntactic: No syntactic checks before calling theorem prover.
--assign: Assignment actions are not replaced by epsilons.
--return: Return actions are not replaced by epsilons.

The following options control the aspects of Copper related to proof generation.

--proof: Generate proofs when the specification is found to be valid. Use only for safety verification and SE-LTL model checking.

The following options control the aspects of Copper related to proof-carrying code. For these options to work, a version of gcc that generates PowerPC binaries must be installed as "gcc-ppc". Also, the target C program must be called "pcc-test.c".

--pcc: Generate and prove verification conditions for a specific procedure in "pcc-test.c", which must be annotated with invariants. An invariant is simply a side-effect free C expression and is specified using the distinguished procedures "__begin__" and "__inv__". Specifically, a control flow point "Loc" is annotated with an invariant "X" by inserting the code "__begin__(); __inv__(X);" just before "Loc". It is recommended that you have as many control flow points annotated with invariants as possible. In particular, every loop in the control flow graph of the relevant procedure must contain at least one control flow point annotated with an invariant. Otherwise, Copper will not terminate. In practice, Copper first compiles "pcc-test.c" into PowerPC assembly using "gcc-ppc" and then generates and proves the verification conditions on the assembly level.
--pccProc <procedure_name>: Procedure to check with "--pcc". Default is "main". Use only in combination with "--pcc".
--noPccAsm: Skip compiling "pcc-test.c" to assembly. Use an existing assembly program, which must be called "pcc-test.s" and must have been generated previously by Copper using "--pcc". Use only in combination with "--pcc".

Copper User Manual

Table of Contents

Introduction

Usage

Options