diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
| commit | f4586d1e8b1116340574d9660117f93e7a1e4e3b (patch) | |
| tree | 15b7dff4ed22b762446e4ae1f426e8f8aa2de52c /kernel/byterun | |
| parent | 4708506ca1b34e93835b163db102f6860c89190c (diff) | |
ajout de head0 et tail0 en natif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 30 |
3 files changed, 32 insertions, 0 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 961c49785..55b907adf 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -45,6 +45,7 @@ void init_arity () { arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]= arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]= arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]= + arity[HEAD0INT31]=arity[TAIL0INT31]= arity[COMPINT31]=arity[DECOMPINT31]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 00156ebe8..8a45e9739 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -42,6 +42,7 @@ enum instructions { SUBINT31, SUBCINT31, SUBCARRYCINT31, MULCINT31, MULINT31, DIV21INT31, DIVINT31, ADDMULDIVINT31, COMPAREINT31, + HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, /* /spiwack */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e7eb1bc8d..ccfb2515a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1255,6 +1255,36 @@ value coq_interprete Next; } + Instruct (HEAD0INT31) { + int r = 0; + uint32 x; + print_instr("HEAD0INT31"); + x = (uint32) accu; + if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; } + if (!(x & 0xFF000000)) { x <<= 8; r += 8; } + if (!(x & 0xF0000000)) { x <<= 4; r += 4; } + if (!(x & 0xC0000000)) { x <<= 2; r += 2; } + if (!(x & 0x80000000)) { x <<=1; r += 1; } + if (!(x & 0x80000000)) { r += 1; } + accu = value_of_uint32(r); + Next; + } + + 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; + } + Instruct (ISCONST) { /* Branches if the accu does not contain a constant (i.e., a non-block value) */ |