FermaT

The FermaT Maintenance Environment

The FermaT Maintenance Environment is an interactive front-end to the FermaT Program Transformation System (see below), and includes a copy of the system along with compiled executables for Linux, Windows and Mac.

Click here for a screenshot.

Click here for the tutorial.

The left window shows the parse tree for the current program, the middle window shows the pretty-printed WSL code and the right window shows the transformation catalogue. A statement or expression can be selected by clicking in the left or middle window, and a transformation applied to the selected statement by clicking in the right window.

Linux and Mac Users

You will need a recent version of java installed, see http://www.java.com/en/download/ if necessary.

Unpack the downloaded archive with the command:

% tar zxvf fme.tar.gz

% cd fme
% perl fme.pl

Windows Users

You will need a recent version of java installed, see http://www.java.com/en/download/ if necessary.

You will also need a recent verson of perl. See http://www.activestate.com/ActivePerl/ or http://www.perl.org for a Windows version of perl.

Unpack the downloaded archive with a suitable utility. (Tugzip, PowerArchiver 6.1 and Winzip can all unpack tar.gz files). This creates a directory called fme.

Double-click on the file fme.bat to run it.

The FermaT Program Transformation System

The FermaT Transformation System is a powerful industrial-strength program transformation system based on the WSL language.

FermaT has been used sucessfully in several major assembler to C and assembler to COBOL migration projects involving the conversion of millions of lines of hand-written assembler code to efficient and maintainable C or COBOL code.

See the WSL Reference Manual for more information. The mathematical foundations can be found in my DPhil thesis and published papers.

FermaT is now available as free software under the GNU General Public License (GPL).

Requirements

1. Perl 5.6.1 or later. The command "perl -v" will tell you which version of perl you have.
2. Bit::Vector, a perl module for efficient sets of integers (by Steffen Beyer). This is included in recent releases of ActivePerl, and the 32 bit Intel Linux version of this module is now included in the distribution.
3. Set::IntRange, a perl module (based on Bit::Vector) for sets of integers in a given range (also by Steffen Beyer). This is a pure perl module, a copy of which is included in the distribution.
4. gcc or a compatible C compiler.

Unix/Linux Installation Instructions

1. If you do not have Bit::Vector installed, and you are not running Linux on a 32 bit Intel system, then you can install Bit::Vector with this command:

   perl -MCPAN -e 'CPAN::Shell->install(Bit::Vector)'
   

2. Download the gzipped tar file fermat3.tar.gz.
3. Unpack the archive:

   % tar zxvf fermat3.tar.gz
   

   This creates a directory called fermat3.
4. Change to the fermat3 directory and source the appropriate DOIT script (DOIT.sh, DOIT.csh or DOIT.bash) into your shell:

   % cd fermat3
   % source DOIT.csh
   

5. Type "make test" to compile, install and test FermaT (this runs make-fermat to compile and install scmfmt and then runs test-fermat and test-trans to test the result):

   % make test
   

6. You should (eventually) see the message "All files passed!"

Windows Installation Instructions

To install perl and the modules from ActiveState and the MinGW (Minimalist GNU for Windows) version of gcc:

1. Download a recent version of perl from http://www.activestate.com/ActivePerl/ and double click on it to install perl. (This should include the module Bit::Vector, and Set:ÏntRange is now included in the distribution).
2. Download the current version of the automated MinGW Installer from http://www.mingw.org/ and double click on it to install gcc.
3. Reboot...

1. Download the gzipped tar file fermat3.tar.gz to directory C:\fermat (edit the batch file DOIT.bat if you want to use a different directory).
2. Unpack the archive with a suitable utility. (Tugzip, PowerArchiver and Winzip can both unpack tar.gz files). This creates a directory called fermat3.
3. Open a Windows DOS box, change to the fermat3 directory and run the DOIT.bat batch file:

   C: cd C:\fermat\fermat3
   C: doit
   

4. Run these commands to build and test FermaT:

   C: make-fermat
   C: test-fermat
   C: test-trans
   

5. You should (eventually) see the message "All files passed!"

How to Write a Transformation

(See the files in fermat3/example for example files implementing this transformation).

Suppose you want to write a transformation to reverse the branches of an IF statement, for example to turn this:

IF x = 0 THEN y := 1 ELSE y := 2 FI

IF x <> 0 THEN y := 2 ELSE y := 1 FI

We will call this transformation Reverse_If.

1. First you need to write two files:
   1. reverse_if.wsl contains the definitions of two procedures: @Reverse_If_Test and @Reverse_If_Code plus any supporting code.

      @Reverse_If_Test tests if the transformation is valid at the currently selected point of the current program. It calls @Pass if the transformation is valid, and @Fail("failure message...") otherwise.

      @Reverse_If_Code contains the code to implement the transformation. It can assume that the test succeeded.

   2. reverse_if_d.wsl contains supporting definitions which set up the integer variable TR_Reverse_If and put the @Reverse_If_Test and @Reverse_If_Code functions into the TRs_Test and TRs_Code arrays.
2. Check the syntax of the WSL files with:

   wslsyn reverse_if.wsl
   wslsyn reverse_if_d.wsl
   

3. Translate the WSL to Scheme with:

   wsl2scm reverse_if.wsl
   wsl2scm reverse_if_d.wsl
   

4. Write a patch file "patch.tr" containing the lines:

   (define //T/R_/Reverse_If '())
   (load "reverse_if.scm")
   (load "reverse_if_d.scm")
   

   NOTE that all upper case letters in WSL symbols must be preceded with a slash (/) and there must be an initial slash added to convert a WSL symbol to the equivalent Scheme symbol. This is because Scheme is case-insensitive and also because we want to avoid clashes between WSL symbols and Scheme symbols.
5. Write a sample input file, test_reverse_if-1.wsl containing the line:

   IF x = 0 THEN y := 1 ELSE y := 2 FI
   

6. Test the transformation with:

   dotrans test_reverse_if-1.wsl test_reverse_if-2.wsl TR_Reverse_If type=Cond
   

   This should generate the file test_reverse_if-2.wsl containing the line:

   IF x <> 0 THEN y := 2 ELSE y := 1 FI
   

   NOTE: The type of an IF statement is T_Cond (the initial T_ can be omitted in a type=... argument to dotrans). The type of an IF expression (conditional expression) is T_If.

News

17th December 2001: This release includes perl modules for fast computation of immediate dominators, control dependencies and Static Single Assignment form. It also includes new transformations for computing SSA form and for forwards and backwards slicing of WSL using dataflow analysis.

20th December 2001: Added Rename_Defns transformation and improved the slicer.

2nd January 2002: Updated to the latest version of SCM (scm5d4) and removed non-essential Scheme files from the distribution.

11th March 2002: FermaT now builds on Windows platforms as well as Linux, Solaris and other Unix platforms. You need a recent version of perl plus the GNU C compiler. See the Windows Installation Instructions below for details.

25th November 2002: FermaT can now be installed in a path with spaces in it. The environment variables are no longer required, provided you pass the apprporiate options to the scripts (see the Makefile for the required options).

30th June 2003: Added @Transitive_Closure function to utility.wsl

8th March 2004: This release includes a new function @WP(P, R) which takes a WSL program P and condition R and returns a WSL condition equivalent to the weakest precondition of P on R. Note: @WP is not defined for programs which contain loops of recursion since the weakest precondition for such programs is infinitely long. This release also extends the simplifier with some computationally intensive simplifications for simplifying weakest preconditions. Call @Simplify directly with a budget larger than 12 to invoke these simplifications (@WP itself calls @Simplify with a budget of 20).

15th August 2007: This release adds several new transformations including Semantic_Slice, as described in the paper: Slicing as a Program Transformation (ACM Transactions on Programming Languages and Systems, Vol 29, Issue 2, March 2007).

21st July 2008: The WSL Reference Manual has been converted to PDF format.

7th August 2008: Updated to use the latest version of SCM

2nd March 2009: Simplified installation requirements.

23rd July 2009: New IFMATCH and FILL syntax

Back to my home page