A. Compilation of a SmartMIPS cross-compiler and cross-debugger
---------------------------------------------------------------

The installation described below has been sucessful on MacOS X,
Ubuntu, and Cygwin.

We will put the cross-compilation environment into the directory
SMIPS=/cygdrive/c/affeldt/install/cross.
In particular, the sources for the binutils, gcc, newlib, and gdb will
go into $SMIPS/src.

1. binutils 2.20

In the source directory, do:
./configure --target=mips-elf --program-prefix=mips-elf- --prefix=$SMIPS
make
make install

2. gcc 4.4.1 (1st part)

This requires development versions of gmp and mpfr, often available
as packages (libgmp3-dev and libmpfr-dev on Ubuntu,
libmpfr-devel and libgmp-devel in cygwin).

./configure --target=mips-elf --prefix=${SMIPS}  --with-mpc=${SMIPS} --with-newlib --without-headers --disable-shared --enable-interwork --enable-multilib --enable-languages=c
make -j4 CFLAGS="-O2" all-gcc
make install-gcc

3. newlib 1.17

(Available as package newlib-source in Ubuntu.)
At this point, put the mips executables in the PATH:
export PATH=${PATH}:${SMIPS}/bin

./configure --prefix=${SMIPS} --target=mips-elf CFLAGS_FOR_TARGET="-g -O2 -mips32" --enable-interwork --enable-multilib
make
make install

3. gcc (2nd part)

Same as 1st part above but without "--without-headers".
An intermediate build directory is necessary to avoid the following error:
"libgcc.mvars: No Such File (since gcc-4.3.0)".

mkdir build; cd build;
../configure --target=mips-elf --prefix=${SMIPS} --with-mpc=${SMIPS} --with-newlib --disable-shared --enable-interwork --enable-multilib --enable-languages=c CFLAGS_FOR_TARGET="-g -O2 -mips32"
make CFLAGS="-O2"
make install

4. gdb 7.0.1

This requires the development version of ncurses (libncurses-dev package
in Ubuntu).

The SmartMIPS support is buggy. Here is how to fix it.
In file src/sim/mips/mips.igen, the semantics of MADDU is wrong.
At two places (lines 2485 and 2508), change the assignment to ACX: 
"< temp" becomes "> temp".
The semantics of MULT is also wrong.
In function do_mult, erase line 2807 ("ACX = 0").
In the definition of MULT, erase line 2847 ("ACX = 0").
Finally, MULTU is also wrong. 
In function do_multu, after line 2869, add line "ACX = 0;".
In the definition of MULTU, in the conditional at line 2911, add
a line "ACX = 0;". 
A patch for the above can be founed at:
http://permalink.gmane.org/gmane.comp.gdb.patches/55961

./configure --disable-werror --prefix=${SMIPS} -with-mpc=${SMIPS} --target=mipsisa32-elf --program-prefix=mips-elf-
make
make install

5. compilation

mips-elf-gcc -T nullmon.ld -msmartmips -Wa, -mips32 filename.S

6. execution

mips-elf-gdb
target sim (to build the simulator)
set architecture mips:isa32
file a.out
load
break end_
run

or

mips-elf-gdb -x filenamedbg.txt

where filenamedbg.txt contains the above

B. Extraction and execution of BBS in assembly
----------------------------------------------

1. Coq extraction

using Asm.v file

2. Automatic generation of test cases

209 = 11 * 19 is a Blum integer.

bbs_asm_gen.rb takes as input:
1. a random seed
2. the modulus
3. the word length of x
4. the word length of the result

For instance:

ruby bbs_asm_gen.rb 2 209 4 5 > bbs.generated_2_209_4_5.S

3. Gdb script

mips-elf-gcc -mips32 -msmartmips -Wl,-Tnullmon.ld bbs.generated_2_209_4_5.S

mips-elf-gdb a.out -x bbsdbg.txt 

with

$ cat bbsdbg.txt 
target sim
set architecture mips:isa32
file a.out
load

break end_

run

printf "X: %08x %08x %08x %08x %08x\n", ((int*)&X)[0], ((int*)&X)[1], ((int*)&X)[2], ((int*)&X)[3], ((int*)&X)[4]
printf "M: %08x %08x %08x %08x %08x\n", ((int*)&M)[0], ((int*)&M)[1], ((int*)&M)[2], ((int*)&M)[3], ((int*)&M)[4]
printf "L: %08x %08x %08x %08x %08x\n", ((int*)&L)[0], ((int*)&L)[1], ((int*)&L)[2], ((int*)&L)[3], ((int*)&L)[4]
printf "Y: %08x %08x %08x %08x %08x\n", ((int*)&Y)[0], ((int*)&Y)[1], ((int*)&Y)[2], ((int*)&Y)[3], ((int*)&Y)[4]
printf "B: %08x %08x %08x %08x\n", ((int*)&B)[0], ((int*)&B)[1], ((int*)&B)[2], ((int*)&B)[3]
info registers