products/sources/formale Sprachen/PVS/analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: coq_fix_code.c   Sprache: C

Untersuchung 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);
}

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff