| products/sources/formale Sprachen/Coq/kernel/byterun/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: coq_fix_code.h Sprache: COriginal von: Coq© |
|
||||||
|
/***********************************************************************/
/* */ /* Coq Compiler */ /* */ /* Benjamin Gregoire, projets Logical and Cristal */ /* INRIA Rocquencourt */ /* */ /* */ /***********************************************************************/ /* Arnaud Spiwack: expanded the virtual machine with operators used for fast computation of bounded (31bits) integers */ #include <stdio.h> #include <stdlib.h> #include <stdint.h> #include <caml/config.h> #include <caml/misc.h> #include <caml/mlvalues.h> #include <caml/fail.h> #include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" #ifdef THREADED_CODE char ** coq_instr_table; char * coq_instr_base; int arity[STOP+1]; void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= arity[ISINT]=arity[AREINT2]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= arity[BRANCH]=arity[ENSURESTACKCAPACITY]= arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]= arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]= arity[CHECKMULINT63]=arity[CHECKMULCINT63]= arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]= arity[CHECKDIV21INT63]= arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]= arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; } #endif /* THREADED_CODE */ void * coq_stat_alloc (asize_t sz) { void * result = malloc (sz); if (result == NULL) raise_out_of_memory (); return result; } value coq_makeaccu (value i) { CAMLparam1(i); CAMLlocal1(res); code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); res = caml_alloc_small(1, Abstract_tag); Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); CAMLreturn(res); } value coq_pushpop (value i) { CAMLparam1(i); CAMLlocal1(res); code_t q; res = caml_alloc_small(1, Abstract_tag); int n = Int_val(i); if (n == 0) { q = coq_stat_alloc(sizeof(opcode_t)); Code_val(res) = q; *q = VALINSTR(STOP); CAMLreturn(res); } else { q = coq_stat_alloc(3 * sizeof(opcode_t)); Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); CAMLreturn(res); } } value coq_is_accumulate_code(value code){ code_t q = Code_val(code); int res; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } #ifdef ARCH_BIG_ENDIAN #define Reverse_32(dst,src) { \ char * _p, * _q; \ char _a, _b; \ _p = (char *) (src); \ _q = (char *) (dst); \ _a = _p[0]; \ _b = _p[1]; \ _q[0] = _p[3]; \ _q[1] = _p[2]; \ _q[3] = _a; \ _q[2] = _b; \ } #define COPY32(dst,src) Reverse_32(dst,src) #else #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ value coq_tcode_of_code (value code) { CAMLparam1 (code); CAMLlocal1 (res); code_t p, q; asize_t len = (asize_t) caml_string_length(code); res = caml_alloc_small(1, Abstract_tag); q = coq_stat_alloc(len); Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; COPY32(&instr,p); p++; if (instr < 0 || instr > STOP){ instr = STOP; }; *q++ = VALINSTR(instr); if (instr == SWITCH) { uint32_t i, sizes, const_size, block_size; COPY32(q,p); p++; sizes=*q++; const_size = sizes & 0xFFFFFF; block_size = sizes >> 24; sizes = const_size + block_size; for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; }; } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) { uint32_t i, n; COPY32(q,p); p++; /* ndefs */ n = 3 + 2*(*q); /* ndefs, nvars, start, typlbls,lbls*/ q++; for(i=1; i<n; i++) { COPY32(q,p); p++; q++; }; } else { uint32_t i, ar; ar = arity[instr]; for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } CAMLreturn(res); } ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
