Twig Documentation

Twig is a theorem proving tool which consists mainly of a decision procedure for deciding properties of equations involing bit-vectors with symbolic lengths.

1. Introduction
2. Meas: the input language
3. Twig: the command Line tool
4. Gtwig: the graphical user interface
5. Examples

1. Introduction

Twig is a decision procedure for properties bit-vectors of symbolic lengths. The decsion procedures that it uses have been described in my doctoral thesis: Automated Reasoning about Hardware Data Types Using Bit-vectors of symbolic lengths. The goal of this research is to provide an invaluable tool for reasoning about parametric hardware descriptions (descriptions in which the width of the bit-vectors and other structures are not fixed integers). It is hoped that the ability to determine the validity of such properties would help a designer produce a correct product.

In Twig, our goal is to produce a tool with the following top-level features (in order of decreasing importance):

Decision procedures are sound and complete.
Negative decision results are accompanied by a viewable counter-model.
Counter-models are used to interpret (or run) the description. This certifies the counter-model.
Positive decision results are accompanied by a viewable proof.
Proofs are certified in a simple proof system.
Methods for integrating the decision procedures in third party tools are available.

Twig is composed of several components. The components most visible to the user are

Meas: The strongly-typed functional input language which allows descriptions/data-types that are a natural generalization of the decidable bit-vector language. This language allows a user to specify both descriptions (functions and data) and properties.
Twig: A batch-style executable which parses meas input and attempts to run the decision procedure on the properties found within. When properties fall into the decidable class the procedure returns eith TRUE or FALSE (with a counter-model). Errors are generated for properties that do not fall into the decidable class.
Gtwig: A graphical-user interface for twig implemented for the GTK+2.0 toolkit. The primary functionality which this tool provides over the command line version (Twig), concerns error reporting and counter-model interaction. Once a counter-model has been produced, Gtwig helps a user understand how this counter-model falsifies his property.

The remainder of this manual will describe how these components work and give some examples which introduce the capabilities of Twig. To read more about the algorithms and methods used in Twig please refer to my doctoral
thesis: Automated Reasoning About Hardware Data Types Using Bit-vectors of Symbolic Length.

2. Meas: the input language

The Meas language is modelled after pure ML with a syntax similar to that of OCaml. Only the core of the lanugage is available: lambda abstraction, let-bindings, recursive functions, and explicit type restrictions.
A BNF grammar describing Meas syntax is available. We describe below a much simplified account of the Meas grammar which is more useful for a first glance.

2.1 Types

Types in Meas are partitioned according to characteristic: data, address or function. Data characteristic is associated with types that are meant to be data structures in the model. Address characteristic is associated with vector domains. Ranges are described by types with data characteristic. Function charactistic is associated with types for functions (higher-order and otherwise).

address_type_expression ::=

##### length_type_expression

#####| address_type_expression ** address_type_expression

#####| address_type_variable

#####| ( address_type_expression )

length_type_expression ::=

##### NUMBER

#####| length_type_variable

#####| length_type_expression - length_type_expression

#####| length_type_expression + length_type_expression

#####| ( length_type_expression )

address_type_variable ::=

##### IDENTIFIER : address

length_type_variable ::=

##### IDENTIFIER : length

Length expressions are the most basic address types, and the consist of symbolic expressions which represent integer upper bounds for an array domain. Lengths are constructed using variables, numbers, addition and subtraction. Address types are formed using variables, length expressions, and cartesian products (**).

data_type_expression ::=

##### bool

#####| data_type_expression ** data_type_expression

#####| address_type_expression ->d data_type_expression

#####| data_type_variable

#####| ( data_type_expression )

data_type_variable ::=

##### IDENTIFIER : data

Types with characteristic data are formed using the boolean constant type (bool), cartesian product (**), array types (->d), and variables. Since booleans are the underlying constants at the bottom of the syntax of every ground type, we can view types with characteristic data as structures that contain bits. Vectors are a simple special case of a type with charateristic data (l ->d bool for any length expression l).

functional_type_expression ::=

##### data_type_expression ->f data_type_expression

#####| address_type_expression ->f data_type_expression

#####| functional_type_expression ->f data_type_expression

#####| address_type_expression ->f functional_type_expression

#####| data_type_expression ->f functional_type_expression

#####| functional_type_expression ->f functional_type_expression

#####| functional_type_variable

#####| ( functional_type_expression )

Types with functional characteristic are formed using allowable combinations of the other characteristic and the function arrow (->f). Types with address characteristic are not allowed to be the range of a type with functional type. The reason for this is that we do not deal with address types as first class items. They are only important in so far as they are part of a type with characteristic data. The denotational semantics of the arrow operators ->d and ->f are the same if we consider only terminating functions.

2.2 Operators and variables

With the rudimentary description of the type system in the previous section, we are ready to describe the functions that are available in Twig. The first functions we will describe are familiar the familiar boolean operations and constants. These are polymorphic, in the sense that they are well defined
for any type of characteristic data (we use a colon ':' as a separator between an expression and its type):

0 : data_type_expression

1 : data_type_expression

For example, 0 : 3 ->d bool is a vector of three boolean values.

not : data_type_expression ->f data_type_expression

Negation is done via the 'not' function which returns the same type as it takes.
For instance, we expect that the expression 'not ( 0 : bool)' and '1: bool',
refer to the same thing. For more complicated types, the obvious recursion is done
to negate all the boolean values contained within the data structure.

and : data_type_expression ->f data_type_expression ->f data_type_expression

Conjunction (via the 'and' function) takes two operands with the same type and returns
the conjunction we expect. As in the case of negation, types more complicated
than bool are handled by performing elementwise conjunction recursively.

or : data_type_expression ->f data_type_expression ->f data_type_expression

The function 'or' is used for disjunction.

xor : data_type_expression ->f data_type_expression ->f data_type_expression

eq : data_type_expression ->f data_type_expression ->f data_type_expression

Binary functions for equality ('eq') and exclusive-or ('xor') are also available, and they are defined in a similar way to the other boolean operators.

After boolean operations, we have structural operations which enable us to move information around, rather than form relations. Combining structural operations with boolean operations in an unrestricted fashion allows us to express properties about general Turing machines. Only for restricted use of structural operations, do we have a decidable fragment which Twig implements.

The first structural operation is concatenation. It allows two vectors with the same range type to be "stuck together" to form a vector containing both original vectors.

con : (length_type_expression1 ->d data_type_expression) ->f (length_type_expression2 ->d data_type_expression) ->f (length_type_expression1 + length_type_expression2) ->d data_type_expression

The semantics of concatenation are as follows: 'con x y' begins with the 'x' values starting from 0, and past the length of 'x', the 'y' values are found. So the length of the resulting vector is the sum of the lengths of the argument vectors.

In addition to sticking vectors together with concatenation, we are able to pull them apart with extraction. Extraction takes a subrange of a vector's domain to form a subvector from the original vector.

extr : (length_type_expression1 ->d data_type_expression) ->f length_type_expression2 ->f length_type_expression3 ->f (length_type_expression3 - length_type_expression1) ->d data_type_expression

To stretch a single bit to a vector by repeating the value, we emply repetition.

rep : (length_type_expression ->f data_type_expression ->f (length_type_expression ->d data_type_expression))

To reduce a vector to a single bit, we use the reduction operations andred and orred. Andred computes the conjunction of all the bits in its argument vector and is 1 when applied to the empty vector. Orred computes the disjunction of all the bits in its argument vector and is 0 when applied to the empty vector.

andred : (length_type_expression ->d data_type_expression) ->f data_type_expression

orred : (length_type_expression ->d data_type_expression) ->f data_type_expression

The only other constant other than 0 and 1 is the empty vector:

eps : 0 ->d data_type_expression

Variables can be declared as global unknowns:

unknown variable_identifier

unknown ( variable_identifier : type_expression )

Variables can also be declared as arguments or local variables by referencing
their name and (possibly) their type.

variable_identifier

( variable_identifier : type_expression )

2.3 Properties and expressions

Properties are stated by giving their name and definition. Free variables and functions must have been previously declared (using a definition or as unknowns). Forcing this upon the user prevents the introduction of unexpected behaviors due to the fact that some variable was unintentionally misspelled.

property property_identifier : expression

Sensible properties (for the moment) are properties whose types are bits (and therefore definitively of characteristic data.

At this point it is useful to describe expressions. Expressions are formed by composing the operators and variables in the source to form larger terms:

expression ::=
       fun variable_term -> expression
     | let variable_term variable_term_list = expression in expression
     | let rec variable_term variable_term_list = expression in expression
     | if condition_on_length_type_expression then expression else expression
     | variable_term_typeless
     | expression expression
     | ( expression )
     | operator

Most of this syntax and its intended semantics is taken from the functional language OCaml. The names of each of these compositions are as follows (in order): Lambda terms, let-bindings, recursive let-bindings, conditionals, variables instances, applications, parenthesized expressions and operators (these were described in the previous section).

At the moment, recursive function descriptions are not yet supported and conditional expressions are only meant to deal with conditions on length variables (used in the types). The intention is to use conditionals from this built-in syntax to distinguish the base cases of recursively defined functions (once support for these is implemented). Variable instances are typeless since type constraints can only be placed on them where they are declared (as described in the previous section).

Defined functions and constants can be defined outside of property definitions. This allows the sharing of these definitions amongst several properties. We are now ready to describe the top-level BNF for (?.twig) source files:

source_file ::=
          epsilon
    | declaration source_file
    | property source_file

3. Twig: command line tool

Usage:

    twig [options] file.twig

General Remarks:
    Twig runs by opening the text file specified, parsing it, and attempting
to prove all properties (unless it otherwise specified in the arguments). As a side-effect of running twig, a file (file.dat) is written which allows inspection of the results in Gtwig (the GUI part of the Twig project).

Options:

    --single propertyname
       The property specified is the only property that twig will attempt to prove. Other properties are

    --time
       This option causes Twig to produce a time report which describes the amount of computation time that each part of Twig uses.

    --bdd
       This option chooses the Bdd-based algorithm (replacing the relatively naive tableau algorithm).

Evironment variables:

You must set the LD_LIBRARY_PATH environment variable to include the path to the shared library (typically /usr/local/lib/dllmuddy.so).

4. Gtwig: graphical-user interface

The graphical user interface is implemented in GTK+ using the lablgtk libraries for OCaml. The interface consists of an upper half which displays the source of a file.twig file. The GUI interface implements all the functionality of the command line command twig. This functionality is accessed via the menus at the top of the main window.

Fig 1. GTwig Main Window

The lower panel consists of several tabs which display information in reaction to user commands. The three tabs are called Log, Properties and Countermodel. Below we systematically describe the user commands that are possible from the menus:

File Menu:

New file clears the source text region and loses the source in the text region. Open file pops up a file chooser dialog which allows the user to specify which new source file will be opened. Save file saves the file to the filename specified in the window title bar; if none is yet specified, the user is prompted to supply one using a file chooser dialog. Save As... functions much the same way except that the file dialog comes up regardless of whether the name of the current source file is known. Parse File causes the twig parser to analyze the file. The parser will report syntactic errors in the source file displayed in the source text region. Type errors are also reported. The user is notified of this operation's success or failure via the log tab in the lower half of the window. In the case of an error a link is produced that allows the user to jump to the error location in the source file text region. A side effect of the parsing operation is the population of the combobox with the names of the properties described in the source file. Quit causes the GUI to quit.

Edit Menu:

Copy copies the user-highlighted text in the source file text region to the system clipboard. Cut copies and removes the user-highlighted text in the source file text region (again the copy is kept in the system clipboard). Paste causes the last clipboard entry to be placed at the user cursor position in the source file text region.

Properties Menu:

The verify operations in the properties menu are meant to be executed after the source text is parsed. If the source text has not been parsed, then it is silently parsed before the verify operation is done. Verify All Properties causes all of the properties in the source file to be verified. Verify Selected Property causes the verification of the single selected property in the combobox to occur. The verification of a property causes a line to be added to the Properties tab below. Successful verification is signalled with TRUE and failure with FALSE. When the user highlights a line (property) in the Properties tab that is false, the Countermodel tab is activated and the user can view the associated countermodel. Clear Results resets the results in the Properties tab below. Halt does nothing.