[bpt/coccinelle.git] / docs / options.tex

\documentclass{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{ifthen}
\usepackage[geometry]{ifsym}
\title{Coccinelle Usage (version 0.1.4)}
\newcommand{\minimum}[2]{\paragraph*{\makebox[0in][r]{\FilledBigDiamondshape\,\,} {{#1}}} {#2}}
\newcommand{\normal}[2]{\paragraph*{\makebox[0in][r]{\BigLowerDiamond\,\,} {{#1}}} {#2}}
\newcommand{\rare}[2]{\paragraph*{\makebox[0in][r]{\BigDiamondshape\,\,} {{#1}}} {#2}}
\newcommand{\developer}[2]{\paragraph*{{#1}} {#2}}

% Very convenient to add comments on the paper. Just set the boolean
% to false before sending the paper:
\newboolean{showcomments}
\setboolean{showcomments}{true}
\ifthenelse{\boolean{showcomments}}
{ \newcommand{\mynote}[2]{
    \fbox{\bfseries\sffamily\scriptsize#1}
    {\small$\blacktriangleright$\textsf{\emph{#2}}$\blacktriangleleft$}}}
{ \newcommand{\mynote}[2]{}}

\newcommand\jl[1]{\mynote{Julia}{#1}}

\begin{document}
\maketitle

\section{Introduction}

This document describes the options provided by Coccinelle.  The options
have an impact on various phases of the semantic patch application
process.  These are:

\begin{enumerate}
\item Selecting and parsing the semantic patch.
\item Selecting and parsing the C code.
\item Application of the semantic patch to the C code.
\item Transformation.
\item Generation of the result.
\end{enumerate}

\noindent
One can either initiate the complete process from step 1, or
to perform step 1 or step 2 individually.

Coccinelle has quite a lot of options.  The most common usages are as
follows, for a semantic match {\tt foo.cocci}, a C file {\tt foo.c}, and a
directory {\tt foodir}:

\begin{itemize}
\item {\tt spatch -parse\_cocci foo.cocci}: Check that the semantic patch
  is syntactically correct.
\item {\tt spatch -parse\_c foo.c}: Check that the C file
  is syntactically correct.  The Coccinelle C parser tries to recover
  during the parsing process, so if one function does not parse, it will
  start up again with the next one.  Thus, a parse error is often not a
  cause for concern, unless it occurs in a function that is relevant to the
  semantic patch.
\item {\tt spatch -sp\_file foo.cocci foo.c}: Apply the semantic patch {\tt
    foo.cocci} to the file {\tt foo.c} and print out any transformations as a
  diff.
\item {\tt spatch -sp\_file foo.cocci foo.c -debug}:  The same as the
  previous case, but print out some information about the matching process.
\item {\tt spatch -sp\_file foo.cocci -dir foodir}:  Apply the semantic
  patch {\tt foo.cocci} to all of the C files in the directory {\tt foodir}.
\item {\tt spatch -sp\_file foo.cocci -dir foodir -include\_headers}:  Apply
  the semantic patch {\tt foo.cocci} to all of the C files and header files
  in the directory {\tt foodir}. 
\end{itemize}

In the rest of this document, the options are annotated as follows:
\begin{itemize}
\item \FilledBigDiamondshape: a basic option, that is most likely of
  interest to all users.
\item \BigLowerDiamond: an option that is frequently used, often for better
understanding the effect of a semantic patch.
\item \BigDiamondshape: an option that is likely to be rarely used, but
  whose effect is still comprehensible to a user.
\item An option with no annotation is likely of interest only to
  developers.
\end{itemize}

\section{Selecting and parsing the semantic patch}

\subsection{Standalone options}

\normal{-parse\_cocci $\langle$file$\rangle$}{ Parse a semantic
patch file and print out some information about it.}

\subsection{The semantic patch}

\minimum{-sp\_file $\langle$file$\rangle$, -c $\langle$file$\rangle$, 
-cocci\_file $\langle$file$\rangle$}{ Specify the name of the file
  containing the semantic patch.  The file name should end in {\tt .cocci}.
All three options do the same thing; the last two are deprecated.}

\subsection{Isomorphisms}

\rare{-iso, -iso\_file}{ Specify a file containing isomorphisms to be used in
place of the standard one.  Normally one should use the {\tt using}
construct within a semantic patch to specify isomorphisms to be used {\em
  in addition to} the standard ones.}

\rare{-iso\_limit $\langle$int$\rangle$} Limit the depth of application of
isomorphisms to the specified integer.

\rare{-no\_iso\_limit} Put no limit on the number of times that
isomorphisms can be applied. This is the default.

\developer{-track\_iso}{ Gather information about isomorphism usage.}

\developer{-profile\_iso}{ Gather information about the time required for
isomorphism expansion.}

\subsection{Display options}

\rare{-show\_cocci}{Show the semantic patch that is being processed before
  expanding isomorphisms.}

\rare{-show\_SP}{Show the semantic patch that is being processed after
  expanding isomorphisms.}

\rare{-show\_ctl\_text}{ Show the representation
of the semantic patch in CTL.}

\rare{-ctl\_inline\_let}{ Sometimes {\tt let} is used to name
intermediate terms CTL representation.  This option causes the let-bound
terms to be inlined at the point of their reference.
This option implicitly sets {\bf -show\_ctl\_text}.}

\rare{-ctl\_show\_mcodekind}{ Show
transformation information within the CTL representation
of the semantic patch. This option implicitly sets {\bf -show\_ctl\_text}.}

\rare{-show\_ctl\_tex}{ Create a LaTeX files showing the representation
of the semantic patch in CTL.}

\section{Selecting and parsing the C files}

\subsection{Standalone options}

\normal{-parse\_c $\langle$file/dir$\rangle$}{ Parse a {\tt .c} file or all
  of the {\tt .c} files in a directory.  This generates information about
  any parse errors encountered.}

\normal{-parse\_h $\langle$file/dir$\rangle$}{ Parse a {\tt .h} file or all
  of the {\tt .h} files in a directory.  This generates information about
  any parse errors encountered.}

\normal{-parse\_ch $\langle$file/dir$\rangle$}{ Parse a {\tt .c} or {\tt
    .h} file or all of the {\tt .c} or {\tt .h} files in a directory.  This
  generates information about any parse errors encountered.}

\normal{-control\_flow $\langle$file$\rangle$, -control\_flow
$\langle$file$\rangle$:$\langle$function$\rangle$}{ Print a control-flow
graph for all of the functions in a file or for a specific function in a
file.  This requires {\tt dot} (http://www.graphviz.org/) and {\tt gv}.}

\rare{-type\_c $\langle$file$\rangle$}{ Parse a C file and pretty-print a
version including type information.}

\developer{-tokens\_c $\langle$file$\rangle$}{Prints the tokens in a C
  file.}

\developer{-parse\_unparse $\langle$file$\rangle$}{Parse and then reconstruct
  a C file.}

\developer{-compare\_c $\langle$file$\rangle$ $\langle$file$\rangle$,
  -compare\_c\_hardcoded}{Compares one C file to another, or compare the
file tests/compare1.c to the file tests/compare2.c.}

\developer{-test\_cfg\_ifdef $\langle$file$\rangle$}{Do some special
processing of \#ifdef and display the resulting control-flow graph.  This
requires {\tt dot} and {\tt gv}.}

\developer{-test\_attributes $\langle$file$\rangle$,
           -test\_cpp $\langle$file$\rangle$}{
Test the parsing of cpp code and attributes, respectively.}

\subsection{Selecting C files}

An argument that ends in {\tt .c} is assumed to be a C file to process.  A
directory can be specified with the option {\bf -dir}, described below.
Normally, only one C file or one directory is specified.  If multiple files
are specified, they are treated in parallel, {\em i.e.}, the first semantic
patch rule is applied to all functions in all files, then the second
semantic patch rule is applied to all functions in all files, etc.  If a
directory is specified then no files may be specified and only the
rightmost directory specified is used.

\minimum{-dir}{ Specify a directory containing C files to process.  By
  default, the include path will be set to the ``include'' subdirectory of
  this directory.  A different include path can be specified using the
  option {\bf -I}.}

\normal{-include\_headers}{ This option causes header files to be processed
independently.  This option only makes sense if a directory is specified
using {\bf -dir}.}

\normal{-use\_glimpse}{ Use a glimpse index to select the files to which
a semantic patch may be relevant.  This option requires that a directory is
specified.  The index may be created using the script {\tt
  coccinelle/scripts/ glimpseindex\_cocci.sh}.  Glimpse is available at
http://webglimpse.net/.  In conjunction with the option {\bf -patch\_cocci}
this option prints the regular expression that will be passed to glimpse.}

\developer{-kbuild\_info $\langle$file$\rangle$}{ The specified file
  contains information about which sets of files should be considered in
  parallel.}

\developer{-disable\_worth\_trying\_opt}{Normally, a C file is only
  processed if it contains some keywords that have been determined to be
  essential for the semantic patch to match somewhere in the file.  This
  option disables this optimization and tries the semantic patch on all files.}

\developer{-test $\langle$file$\rangle$}{ A shortcut for running Coccinelle
on the semantic patch ``file{\tt{.cocci}}'' and the C file ``file{\tt{.c}}''.}

\developer{-testall}{A shortcut for running Coccinelle on all files in a
  subdirectory {\tt tests} such that there are all of a {\tt .cocci} file, a {\tt
    .c} file, and a {\tt .res} file, where the {\tt .res} contains the
  expected result.}

\developer{-test\_okfailed, -test\_regression\_okfailed} Other options for
keeping track of tests that have succeeded and failed.

\developer{-compare\_with\_expected}{Compare the result of applying
  Coccinelle to file{\tt{.c}} to the file file{\tt{.res}} representing the
  expected result.}

\subsection{Parsing C files}

\rare{-show\_c}{Show the C code that is being processed.}

\rare{-parse\_error\_msg}{Show parsing errors in the C file.}

\rare{-type\_error\_msg}{Show information about where the C type checker
  was not able to determine the type of an expression.}

\developer{-use\_cache} Use preparsed versions of the C files that are
stored in a cache.

\developer{-debug\_cpp, -debug\_lexer, -debug\_etdt,
  -debug\_typedef}{Various options for debugging the C parser.}

\developer{-filter\_msg, -filter\_define\_error,
  -filter\_passed\_level}{Various options for debugging the C parser.}

\developer{-only\_return\_is\_error\_exit}{In matching ``{\tt{\ldots}}'' in
  a semantic patch or when forall is specified, a rule must match all
  control-flow paths starting from a node matching the beginning of the
  rule.  This is relaxed, however, for error handling code.  Normally, error
  handling code is considered to be a conditional with only a then branch
  that ends in goto, break, continue, or return.  If this option is set,
  then only a then branch ending in a return is considered to be error
  handling code.  Usually a better strategy is to use {\tt when strict} in
  the semantic patch, and then match explicitly the case where there is a
  conditional whose then branch ends in a return.}

\subsubsection*{Macros and other preprocessor code}

\normal{-D $\langle$file$\rangle$, -macro\_file $\langle$file$\rangle$}{
  Extra macro definitions to be taken into account when parsing the C
  files.}

\rare{-ifdef\_to\_if}{ This option constructs represents an \#ifdef in
the source code as a conditional in the control-flow graph.  This option is
unsafe, as it makes the source code unparsable when \#ifdef is used in a
way that does not directly convert to a conditional.  Nevertheless, it can
be useful when \#ifdef is used in a well-structured way.}

\rare{-use\_if0\_code}{ Normally code under \#if 0 is ignored.  If this
option is set then the code is considered, just like the code under any
other \#ifdef.}

\developer{-noadd\_typedef\_root}{This seems to reduce the scope of a
  typedef declaration found in the C code.}

\subsubsection*{Include files}

\normal{-all\_includes, -local\_includes, -no\_includes}{
These options control which include files mentioned in a C file are taken into
account.  {\bf -all\_includes} indicates that all included files will be
processed.  {\bf -local\_includes} indicates that only included files in
the current directory will be processed.  {\bf -no\_includes} indicates
that no included files will be processed.  If the semantic patch contains
type specifications on expression metavariables, then the default is {\bf
-local\_includes}.  Otherwise the default is {\bf -no\_includes}.  At most
one of these options can be specified.}

\normal{-I $\langle$path$\rangle$}{ This option specifies the directory in
  which to find non-local include files.  This option should be used only
  once, as each use will overwrite the preceding one.}

\rare{-relax\_include\_path}{This option causes the search for local
  include files to consider the directory specified using {\bf -I} if the
  included file is not found in the current directory.}

\section{Application of the semantic patch to the C code}

\subsection{Feedback at the rule level during the application of the
  semantic patch}

\normal{-show\_bindings}{
Show the environments with respect to which each rule is applied and the
bindings that result from each such application.}

\normal{-show\_dependencies}{ Show the status (matched or unmatched) of the
rules on which a given rule depends.  {\bf -show\_dependencies} implicitly
sets {\bf -show\_bindings}, as the values of the dependencies are
environment-specific.}

\normal{-show\_trying}{
Show the name of each program element to which each rule is applied.}

\normal{-show\_transinfo}{
Show information about each transformation that is performed.
The node numbers that are referenced are the number of the nodes in the
control-flow graph, which can be seen using the option {\bf -control\_flow}
(the initial control-flow graph only) or the option {\bf -show\_flow} (the
control-flow graph before and after each rule application).}

\normal{-show\_misc}{Show some miscellaneous information.}

\rare{-show\_flow $\langle$file$\rangle$, -show\_flow
  $\langle$file$\rangle$:$\langle$function$\rangle$} Show the control-flow
graph before and after the application of each rule.

\developer{-show\_before\_fixed\_flow}{This is similar to {\bf
    -show\_flow}, but shows a preliminary version of the control-flow graph.}

\subsection{Feedback at the CTL level during the application of the
  semantic patch}

\normal{-verbose\_engine}{Show a trace of the matching of atomic terms to C
  code.}

\rare{-verbose\_ctl\_engine}{Show a trace of the CTL matching process.
  This is unfortunately rather voluminous and not so helpful for someone
  who is not familiar with CTL in general and the translation of SmPL into
  CTL specifically.  This option implicitly sets the option {\bf
    -show\_ctl\_text}.}

\rare{-graphical\_trace}{Create a pdf file containing the control flow
  graph annotated with the various nodes matched during the CTL matching
  process.  Unfortunately, except for the most simple examples, the output
  is voluminous, and so the option is not really practical for most
  examples.  This requires {\tt dot} (http://www.graphviz.org/) and {\tt
  pdftk}.}

\rare{-gt\_without\_label}{The same as {\bf -graphical\_trace}, but the PDF
  file does not contain the CTL code.}

\rare{-partial\_match}{
Report partial matches of the semantic patch on the C file.  This can
  be substantially slower than normal matching.}

\rare{-verbose\_match}{
Report on when CTL matching is not applied to a function or other program
unit because it does not contain some required atomic pattern.
This can be viewed as a simpler, more efficient, but less informative
version of {\bf -partial\_match}.}

\subsection{Actions during the application of the semantic patch}

\rare{-allow\_inconsistent\_paths}{Normally, a term that is transformed
  should only be accessible from other terms that are matched by the
  semantic patch.  This option removes this constraint.  Doing so, is
  unsafe, however, because the properties that hold along the matched path
  might not hold at all along the unmatched path.}

\rare{-disallow\_nested\_exps}{In an expression that contains repeated
  nested subterms, {\em e.g.} of the form {\tt f(f(x))}, a pattern can
  match a single expression in multiple ways, some nested inside others.
  This option causes the matching process to stop immediately at the
  outermost match.  Thus, in the example {\tt f(f(x))}, the possibility
  that the pattern {\tt f(E)}, with metavariable {\tt E}, matches with {\tt
    E} as {\tt x} will not be considered.}

\rare{-pyoutput coccilib.output.Gtk, -pyoutput coccilib.output.Console}{
This controls whether Python output is sent to Gtk or to the console.  {\bf
  -pyoutput coccilib.output.Console} is the default.  The Gtk option is
currently not well supported.}

\developer{-loop}{When there is ``{\tt{\ldots}}'' in the semantic patch,
  the CTL operator {\sf AU} is used if the current function does not
  contain a loop, and {\sf AW} may be used if it does.  This option causes
  {\sf AW} always to be used.}

\developer{-steps $\langle$int$\rangle$}{
This limits the number of steps performed by the CTL engine to the
specified number.  This option is unsafe as it might cause a rule to fail
due to running out of steps rather than due to not matching.}

\developer{-bench $\langle$int$\rangle$}{This collects various information
  about the operations performed during the CTL matching process.}

\developer{-popl, -popl\_mark\_all, -popl\_keep\_all\_wits}{
These options use a simplified version of the SmPL language.  {\bf
  -popl\_mark\_all} and {\bf -popl\_keep\_all\_wits} implicitly set {\bf
  -popl}.}

\section{Generation of the result}

Normally, the only output is a diff printed to standard output.

\rare{-o $\langle$file$\rangle$}{ The output file.}

\rare{-inplace}{ Modify the input file.}

\rare{-outplace}{ Store modifications in a .cocci\_res file.}

\rare{-no\_show\_diff}{ Normally, a diff between the original and transformed
code is printed on the standard output.  This option causes this not to be
done.}

\rare{-U}{ Set number of diff context lines.}

\rare{-save\_tmp\_files}{Coccinelle creates some temporary
  files in {\tt /tmp} that it deletes after use.  This option causes these
  files to be saved.}

\developer{-debug\_unparsing}{Show some debugging information about the
  generation of the transformed code.  This has the side-effect of
  deleting the transformed code.}

\developer{-patch}{ Deprecated option.}


\section{Other options}

\subsection{Version information}

\normal{-version}{ The version of Coccinelle.  No other options are
allowed.}

\normal{-date}{ The date of the current version of Coccinelle. No other
options are allowed.}

\subsection{Help}

\minimum{-h, -shorthelp}{ The most useful commands.}

\minimum{-help, --help, -longhelp}{ A complete listing of the available
commands.}

\subsection{Controlling the execution of Coccinelle}

\normal{-timeout $\langle$int$\rangle$}{ The maximum time in seconds for
  processing a single file.}

\rare{-max $\langle$int$\rangle$}{This option informs Coccinelle of the
  number of instances of Coccinelle that will be run concurrently.  This
  option requires {\bf -index}.  It is usually used with {\bf -dir}.}

\rare{-index $\langle$int$\rangle$}{This option informs Coccinelle of
  which of the concurrent instances is the current one.  This option
  requires {\bf -max}.}

\rare{-mod\_distrib}{When multiple instances of Coccinelle are run in
  parallel, normally the first instance processes the first $n$ files, the
  second instance the second $n$ files, etc.  With this option, the files
  are distributed among the instances in a round-robin fashion.}

\developer{-debugger}{Option for running Coccinelle from within the OCaml
  debugger.}

\developer{-profile}{ Gather timing information about the main Coccinelle
functions.}

\developer{-disable\_once}{Print various warning messages every time some
condition occurs, rather than only once.}

\subsection{Miscellaneous}

\rare{-quiet}{Suppress most output.  This is the default.}

\developer{-pad, -hrule $\langle$dir$\rangle$, -xxx, -l1}{}

\end{document}