The Coq mailing list

[Moshe Tenenbaum <moe45673 AT gmail.com>]

Gabriel and Enrico, thank you very much for your responses! Good step forward for me.

My next question regards if there is any possible way to go a bit further with the code. FOr example, in the coq_interp.c code you mention, on line 1300, there is an instruction that looks like this:

Instruct (TAIL0INT31) {
    int r = 0;
        uint32 x;
        print_instr("TAIL0INT31");
    x = (((uint32) accu >> 1) | 0x80000000);
        if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
        if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
        if (!(x & 0x000F)) { x >>= 4;  r += 4; }
        if (!(x & 0x0003)) { x >>= 2;  r += 2; }
        if (!(x & 0x0001)) { x >>=1;   r += 1; }
        if (!(x & 0x0001)) {           r += 1; }
        accu = value_of_uint32(r);
        Next;
      }

Can this be transformed using mnemonics like uint64 instead of uint32? And can it be extended for TAIL0INT63 for proper memory allocation?

Thanks again!

Moe

On Fri, Mar 21, 2014 at 2:57 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

On recent versions of Coq, the code is actually in kernel/byterun/coq_interp.c:
  https://github.com/coq/coq/blob/trunk/kernel/byterun/coq_interp.c#L89

It comes from the code of the OCaml virtual machine:
  https://github.com/ocaml/ocaml/blob/trunk/byterun/interp.c#L107

the latter has already been updated to support arm64 hosts, with the
following piece of code:

#ifdef __aarch64__
#define PC_REG asm("%x19")
#define SP_REG asm("%x20")
#define ACCU_REG asm("%x21")
#define JUMPTBL_BASE_REG asm("%x22")
#endif

On Fri, Mar 21, 2014 at 6:23 PM,  <moe45673 AT gmail.com> wrote:
> Hello
>
> Off the bat, I'm a student. Currently, I'm in a course where our focus is the
> LINARO project to port existing programs to Arm64. Our focus is on converting
> assembly code into machine-portable code.
>
> I've chosen COQ to look at and the main assembly code is in the above file
> (installed on Fedora). This code mainly declares specific registers (using
> #define CONSTANT) which is then passed through to, from what I can tell,
> system functions (in the coq*/interp directory).
>
> My question is: why not just allow gcc to set the registers?
>
> Any assistance given with which to point me in a direction would be awesome.
>
> Cheers,
> Moe