Opaque Predicates

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:

OptionArgumentsDescription
--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.
  • list = Generate opaque expressions using linked lists
  • array = Generate opaque expressions using arrays
  • input = Generate opaque expressions that depend on input. Requires --Inputs to set invariants over input.
  • env = Generate opaque expressions from entropy. Requires --InitEntropy.
  • * = Same as list,array,input,env
--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.
  • update = Print the generated structure
  • use = Print every use of an opaque value
  • check = Print only if an opaque value is wrong
--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:

OptionArgumentsDescription
--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.

 

Issues

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.

 

References