Re: [Caml-list] Native compilation for today's MIPS

[rixed@happyleptic.org]

Done !

At least, now coq compiles and seams to run OK.

I encountered a strange bug, anyway, and would like some advice about
my fix. Also, this bug do not seams related to my particular
architecture and, as far as I can tell, would hit any MIPS.

At various occasions the coqtop program jumped in the wrong places.
This was due to the code emited for some tail calls :

    | Lop(Itailcall_imm s) ->
        if s = !function_name then begin
          `	b	{emit_label !tailrec_entry_point}\n`
        end else begin
          let n = frame_size() in
          if !contains_calls then
            `	lw	$31, {emit_int(n - 4)}($sp)\n`;
          if !uses_gp then
            `	lw	$gp, {emit_int(n - 8)}($sp)\n`;
          if n > 0 then
            `	addu	$sp, $sp, {emit_int n}\n`;
          `	la	$25, {emit_symbol s}\n`;
          liveregs i live_25;
          `	j	$25\n`
        end

Now when !uses_gp is true, then the gp register is restored.
Only then the address of symbol s is fetched into register $25, and
jumped to. The problem is : the pseudo instruction 'la' may result 
in some code that uses gp to reach the global offset table and read the
address from there. The assembler will then assume that the gp is the
one that was setup at the begening of the function, and not the one
that's just restored from the stack. Maybe for small programs the value
of gp is always the same (I only vaguely understand this global pointer
thing) but it is not the case for coq.

So I merely moved upward the 'la' instruction, before the 'lw gp,stack'.
And it works, apparently.

What do you think ?