Several transformations rely on boolean and integer expressions that have a known value, known as opaque predicates and expressions. To construct these, data structures with precise invariants are added to the code.
At a minimum, you must create one or more opaque invariant data structures:
| Option | Arguments | Description |
|---|---|---|
| --Transform | InitOpaque | Add opaque initialization code. This initialization code has to be added to a function that gets called before any uses of opaque predicates, usually, but not necessarily, to main. |
| --InitOpaqueStructs | list, array, input, env, * | Comma-separated list of the kinds of opaque constructs to add. Default=list,array.
|
| --InitOpaqueCount | INTSPEC | How many opaque data structures (lists or arrays) to add to the program. They will be split roughly evenly between the different declared opaque structures. Default=1. |
| --InitOpaqueTrace | update, use, check | Trace opaque structures and values as they are generated during execution. This used to be a boolean, but from version 3.3, it can take on multiple values. Default=NONE.
|
| --InitOpaqueDebug | BOOLSPEC | If true, then we store all opaque values in a temporary variable. This can help with debugging when looking at the generated code. For example, if you see a variable named _OPAQUE_Array_42_expected_128, it means: 1)this is opaque expression number 42; 2) it is computed based on an Array opaque kind; and 3) it should always have the value 128. Default=FALSE. |
| --InitOpaqueSize | INTSPEC | Size of opaque arrays. Default=30. |
To frustrate analysis, updates that maintain the invariants should
be sprinkled throughout the program. This is done by the --Transform=UpdateOpaque
option:
| Option | Arguments | Description |
|---|---|---|
| --Transform | UpdateOpaque | Add code that makes updates to opaque predicates. |
| --UpdateOpaqueCount | INTSPEC | How many updates to opaque data structures to add to the function. Default=1. |
| --UpdateOpaqueTrace | BOOLSPEC | Print the updated structure. Default=false. |
| --UpdateOpaqueDebug | BOOLSPEC | If true, then we store all opaque values in a temporary variable that reveals its expected value. Default=FALSE. |
| --UpdateOpaqueAllowAddNodes | bool | Is it safe to malloc new nodes for the opaque data structure in this function? Only set to true if the function is called sparingly. Default=false. |
Note: In --Transform=InitOpaque --Functions=foo, the function foo
must execute before any use of an opaque expression. Easiest is to set
--Transform=InitOpaque --Functions=main but this is best avoided since it
is very obvious.
Tigress will generate copious numbers of extra local
variables and statements of the form _*__BARRIER_* = 1,
_*__BEGIN_* = 1, _*__END_* = 1. They
will be removed by any competent compiler, or by the
--Transform=CleanUp --CleanUpKinds=annotations
transformation.