Cyclone

De Viquipèdia
Dreceres ràpides: navegació, cerca

Cyclone és un llenguatge de programació derivat del llenguatge C que té per finalitat superar les vulnerabilitats d'aquest sense perdre la potència i el control dels recursos que el caracteritzen per a la programació de sistemes.[1]

El seu desenvolupament començà com un projecte conjunt de AT&T Labs Research[2] i el grup de Greg Morrisett a la universitat de Cornell el 2001. La versió 1.0 va sortir el 8 de maig de 2006

Cyclone millora la seguretat, introdueix subtipus (estructurals, d'allotjament, etc), incorpora un allotjament dinàmic insòlit (per regions lèxiques (gestió automàtica), dinàmiques (gestió directa) i al munt amb recol·lector de brossa opcional) i afegeix característiques de llenguatges de més alt nivell del tipus de ML.

Programa Hola món[modifica | modifica el codi]

Descàrrega i instal·lació[3]

 // fitxer hola-mon.cyc
 
 #include <stdio.h>
 #include <core.h>
 
 using Core ; // importa espai de noms Core
 
 int main(int argc, string_t ? args)
 {
   if (argc <= 1) {
      printf("Ús: %s <nom>\n", args[0]);
      return 1;
   }
   printf("Hola des de Cyclone, %s\n", args[1]);
   return 0;
 }
 // fi de fitxer

Compilació i execució

cyclone hola-mon.cyc -o hola-mon
./hola-mon

Restriccions i comprovacions[modifica | modifica el codi]

Cyclone introdueix les següents restriccions i comprovacions:

  • El maneig de punters[4] es controla amb anotacions específiques, per ex.: int *@notnull
    En una crida a funció que admet punters d'un tipus, se n'hi pot posar un que en sigui subtipus,[5] és a dir, amb extensió addicional.
*@nullable abreviat *
insereix comprovació de NULL en ésser desreferenciat
*@notnull abreviat @
punter que no serà mai NULL, comprovació només a l'entrada o en un cast
  • T*@notnull és subtipus de T*@nullable:;[6] *@numelts(n) abreviat *{n} : punter a vector de n elements
    insereix comprovació de límits a les expressions que l'indexen
    excepte si introduïm assercions que assegurin que l'índex és < numelts (punter)
    o que el topall de l'índex en una clàusula for és <= numelts (punter)
  • T*@numelts(m) és subtipus de T*@numelts(n) si m >= n perquè proporciona igual o major nombre d'elements
*@zeroterm 
tires acabades en zero (per defecte als char*)
insereix comprovacions que l'adreçament no sobrepassi el caràcter zero final
*@nozeroterm 
no comprovació
*@fat abreviat ?
punter que vindrà amb informació de límits
insereix comprovació de límits en l'aritmètica de punters.
*@thin (tipus per defecte) 
punter amb la mateixa representació que al 'C'. No se'n permet aritmètica de punters excepte que vagi acompanyat de @zeroterm
*@region(`r) abreviat *`r 
punter amb especificació de regió d'allotjament. Un punter a una regió és segur si la regió és viva.
  • T*@region(`r) és subtipus de T*@region(`s) si la vida de la regió `r inclou la vida de `s, la sobreviu (és segur tractar un punter a `r com si ho fos a `s).
  • Els punters han d'ésser inicialitzats abans de fer-los servir. (en comprova la precedència en l'arbre del flux del control)
  • Els punters penjants (a zones alliberades o inadequades) es prevenen mitjançant l'anàlisi de regions i limitacions a free().
  • Coercions de tipus (ang.:cast): només es permeten si es poden comprovar.[7]
  • Els goto's que saltin a dins d'un altre àmbit estan prohibits.
  • En una clàusula switch, els salts al case següent han de ser explicitats mitjançant fallthru.[8]

...

Característiques de més alt nivell[modifica | modifica el codi]

Cyclone introdueix les següents característiques de llenguatges de més alt nivell

espai de noms[modifica | modifica el codi]

 namespace Pep {
   int x = 0;
   int f() { return x; }
 }
 
 namespace Jan {
 
    using Pep {  // importa els identificadors de l'espai Pep
      int g() { return f(); 
              }
    }
    // ara estem fora de l'àmbit del using, caldrà qualificar amb "espai::"
 
    int h() { return Pep::f(); }  
 }

subtipus estructurals[modifica | modifica el codi]

Estructura igual amb camps addicionals, permet l'ús de punters al subtipus en el lloc de punters d'un tipus.

 #include <stdio.h>
 
 typedef struct Punt {float x,y;} *punt_t;
 typedef struct PuntAcolorit {float x,y; int color;} *cpunt_t;
 
 float xcoord ( punt_t p ) {
   return p→x;
 }
 
 int main() {
 
   cpunt_t cpunt = new PuntAcolorit {1.0, 2.0, 15} ;
 
   float x = xcoord( cpunt) ;
 
   printf ("la x és %.2f\n", x) ;
   return 0 ;
 }

inferència de tipus a l'estil de ML per a variables locals[modifica | modifica el codi]

_ a = 1000 ;  // el compilador infereix tipus int

llista per comprensió[modifica | modifica el codi]

{ for i < topall : expr(i) }  

equival a un inicialitzador de vector, amb valors { expr(i) | i = 0 .. (topall - 1) }

int dobles[100] = { for i < 100 : 2*i }

tuples[modifica | modifica el codi]

Estructures anònimes, per ex.:

$(int, char*) parell = $( 10, "abc") ;

unions etiquetades[modifica | modifica el codi]

Vegeu ref.[9]

 @tagged union T {
   int Integer;
   const char *@fat String;
 };
 
 union T x = {.Integer = 3};
 union T y = {.String = "hola"};
 
 bool printT(union T w) {
 
   if (tagcheck( w.Integer))
    printf("%d",w);
  else
    printf("%s",w);
 }

datatypes a l'estil de ML[modifica | modifica el codi]

Vegeu ref.[10][11]

 datatype T {
   Integer( int);
   String( const char *@fat);
 };
 
 // equivalent aprox. en llenguatge SML: datatype T = Integer of int | String of string
 
 datatype T.Integer x = Integer(3);
 datatype T.String y = String("hola");
 
 void printT( datatype T *@notnull a) {
   switch (a) {
     case &Integer(i): printf("%d",i); return;
     case &String(s): printf("%s",s); return;
   }
 }

excepcions[modifica | modifica el codi]

 FILE *f = fopen("nom_fitxer","r");
 int c;
 
 try {
   c = getc( (FILE *@notnull) f );
 }
 catch {
 
   case &Null_Exception:
     printf("Error en obrir nom_fitxer\n");
     exit(1);
 
   case &Invalid_argument( msg):
     printf("Error: argument invàlid(%s)\n", msg);
     exit(1);
 }
 
 @extensible datatype exn {
   Excepcio_meva(char *@fat);
 };
 
 throw new Excepcio_meva( "tururut");

funcions polimòrfiques[modifica | modifica el codi]

Vegeu ref.[12]

  • les variables de tipus es prefixen amb la cometa revessa (accent greu seguit d'espai) `
  • cal fer servir `a en lloc de (void *)
// funció que intercanvia elements d'una tupla2

$(`b,`a) intercanvia( $(`a,`b) x) {  

  return $(x[1],x[0]);
}

estructures de dades polimòrfiques[modifica | modifica el codi]

 struct List<`a> {`a hd; struct List<`a> * tl; };
 
 typedef struct List<`a> *list_t<`a>;
 
 list_t<int> ilist = new List{1,new List{2,null}};
 
 list_t<string_t> slist = new List{.hd = "primera",
                                   .tl = new List{"segona",null}};

encaixos de patrons[modifica | modifica el codi]

Vegeu ref.[13]

 int suma( $(int,int,int) args) {
   let $(x,y,z) = args;
   return (x+y+z);
 }

En un switch:[14]

 extern int f(int);
 
 int g(int x, int y) {    // retorna f(x)*f(y)
 
   switch( $(f(x),f(y)) ) {
 
   case $(0,_) : fallthru;   // salta al case següent
   case $(_,0) : return 0;
   case $(1,b) : fallthru(b+1-1);  // salta, assignant (b+1-1) al primer elem. de la tupla2
   case $(a,b) && b == 1 : return a;   // amb guardes
   case $(a,b) : return a*b; // és un error si els case no són exhaustius.
   }
 }

tipus abstractes[modifica | modifica el codi]

tipus existencials[modifica | modifica el codi]

Vegeu ref.[15] Tipus d'estructura tal que ∃ un tipus `a per a la signatura especificada. Les estructures amb tipus explícit que concorden en són subtipus.

struct T { <`a> `a f1; `a f2; };

tipus dependents de valors i relació amb predicats[modifica | modifica el codi]

Per ex. el tipus de int A[n]. Vegeu "Verificació estàtica" [16]

Les crides han de satisfer la precondició @requires estàticament

 int f(const int n, int *A)
          @requires(n == numelts(A))        // precondició
          @ensures(0 <= return_value < n)  // postcondició
 {...}

allotjament[modifica | modifica el codi]

Vegeu ref.[17] L'allotjament es materialitza en regions:[18] àmbits locals a la pila, lèxiques (allotj. dinàmic que mor amb el bloc), dinàmiques (vida controlable) o al munt (vida universal). Per què un punter a una regió sigui segur la regió ha d'estar viva.

subtipus
Un punter de tipus T*@region(`r) és subtipus de T*@region(`s) si la vida de la regió `r inclou (sobreviu a) la de `s. Per tant és segur tractar els punters a `r com si ho fossin a `s.
efecte
S'anomena efecte (ang:effect) al conjunt de regions afectades a un tipus que han de ser vives per passar les comprovacions de tipus.[19]
L'efecte buit {} inclou el munt (ang.:heap) quina vida és universal: tot el temps d'execució.
Si e1 i e2 són efectes, e1 + e2 indica el conjunt unió.
regions()
regions(Tipus) dóna l'efecte unió de les regions esmentades a Tipus.
capacitat
S'anomena capacitat (ang:capability) al conjunt de regions vives en un punt del programa.
A l'inici de la funció, la capacitat és la de la funció: la unió dels efectes dels tipus dels paràmetres i el tipus del retorn.
En un bloc, la capacitat és la de l'àmbit que l'engloba més la regió local (pila) i, en cas que n'hi hagi, la lèxica.
restriccions
En una crida a funció, si `r1 i `r2 són variables de regió, es poden especificar relacions dels efectes designats per aquestes variables en forma de restriccions.
El codi següent especifica la restricció que `r ha de sobreviure a `s. Per tant és segur tractar els punters a `r com si ho fossin a `s
void bar( int *@region(`r) x,
          int *@region(`s) y : {`s} > `r) {
...
}

// la restricció admet una llista sep. per comes
{`r1, `r2, .. ,`rn} > `r   // indica que `r ha de sobreviure a totes les de la llista

allotjament local a la pila[modifica | modifica el codi]

Els àmbits d'allotjament local constitueixen una regió cadascun.

L'àmbit principal d'una funció porta per nom de regió la cometa revessa seguida del nom de la funció, per ex. void fun (..) {...} tindrà per nom de regió, `fun

En un sub-àmbit delimitat per claus {} podem fer referència a la regió local posant una etiqueta a l'àmbit, per ex. L:{...} serà la regió `L

allotjament dinàmic[modifica | modifica el codi]

Cada regió en allotjament dinàmic és una llista encadenada de pàgines.

allotjament dinàmic al munt[modifica | modifica el codi]

(ang.: heap) (regió `H) amb recol·lector de memòria brossa.

// new tipus expr_inicialitzadora 
// new inicialitzador_de_vector

// new allotja al Heap, rnew (regió) .. ho fa en una regió específica

struct Punt {float x,y;} ;

Punt *p = new Punt {1.0, 2.0} ;    

// [r]malloc ([regió,] mida) i [r]calloc(..) suportats però desaconsellats
allotjament dinàmic a regions lèxiques LIFO (apilades) associades als àmbits[modifica | modifica el codi]

anomenades LIFO (Last In First Out) o lèxiques, són a l'estil de Tofte & Talpin amb temps de vida associat a l'àmbit corresp.[20]

 #include <stdio.h>
 
 struct Punt {float x,y;} ;
 
 int main() {
   _ a = 1 ;
   { // inici de l'àmbit
   region lifo ; // creació de la regió lèxica d'allotj. dinàmic.
 
   _ p = rnew( lifo) Punt {1.0, 2.0} ; // hi allotjem un objecte
   printf ("la x és %.2f\n", p→x) ;
 
   } // en sortir de l'àmbit es desallotja automàticament la regió lèxica 
 
 
   return 0 ;
 }
allotjament amb multiplicitat de referències (punters) restringida[modifica | modifica el codi]

Vegeu ref.[21] Denominada en l'original "Restricted Pointer Aliasing" (capacitat d'obtenir còpies d'un punter) amb valors ALIASABLE, UNIQUE, REFCNT.

Els dos darrers valors permeten alliberar l'espai allotjat individualment sense esperar que s'alliberi tota una regió

allotjament amb punter de còpia única[modifica | modifica el codi]
  • es crea amb rnew(regió, UNIQUE) .. ; al munt (ang:heap) amb qnew(UNIQUE) ..
  • es desallotja amb [r]ufree([regió,] punter)
  • no se'n permet aritmètica de punters
  • si se'n fa la còpia dins un subàmbit {}, en sortir se'n recupera la capacitat anterior
  • per fer-ne còpies d'ús temporal existeix una construcció let alias<`r>tipus x = ...
int *@aqual(UNIQUE) p = rnew( regio, UNIQUE) tipus expr_inicialitzadora
int *\U p = ...       // notació curta equivalent
allotjament amb comptador de referències[modifica | modifica el codi]
  • es crea amb rnew(regió, REFCNT) .. ; al munt amb qnew(REFCNT) ..
  • [r]drop_refptr([regió,] punter) descompta les referències i allibera en esgotar-les, i el compilador no permet l'ús del punter en el mateix àmbit a continuació
  • no se'n permet aritmètica de punters
  • per fer-ne còpies d'ús temporal existeix alias_refptr
int *@aqual(REFCNT) p = rnew( regio, REFCNT) tipus expr_inicialitzadora
int *\RC p = ...       // notació curta equivalent
allotjament a regions dinàmiques de vida controlable[modifica | modifica el codi]

amb temps de vida controlable, comprovant-ne l'existència en temps d'execució en fer-ne ús.

  • new_ukey(): crea una nova regió dinàmica amb punter únic; free_ukey() per desallotjar la regió
  • new_rckey(): crea una nova regió dinàmica amb punter amb comptador de referències; free_rckey() per desallotjar la regió
  • open: comprova que la regió no ha estat desallotjada i en garanteix l'accés
 #include <core.h>
 
 struct List<`a, `r> {`a hd; struct List<`a, `r> *`r tl; };
 
 typedef struct List<`a, `r> *`r list_t<`a, `r>;
 
 int main() {
   // Creem una regió dinàmica
   let Core::NewDynamicRegion{<`r> key} = Core::new_ukey();
 
   // En aquest punt, ens referirem a la regió `r per
   // especificar tipus, però encara no hi podem accedir
 
   list_t<int,`r> x = NULL; // allotjament a la regió `r obtinguda a la instrucció ''let''
 
   // utilitzem open per a accedir-hi en el sub-àmbit següent
   { region h = open(key);   // consumeix l'única còpia del punter únic key
     x = rnew(h) List(3,x);
   }                       // en sortir descompta la còpia del punter únic key
 
   // en un altre sub-àmbit tornem a treballar-hi
   { region h = open(key);
     int i = x→hd + 1;
     x = rnew (h) List(i,x);
   }
   // Finalment destruïm la clau i la regió
   Core::free_ukey(key);
   return 0 ;
 }
allotjament a regions dinàmiques "reap" (amb desallotjament individual d'objectes)[modifica | modifica el codi]
  • new_reap_ukey(): crea una nova regió dinàmica amb punter únic; free_ukey() per desallotjar la regió
  • new_reap_rckey(): crea una nova regió dinàmica amb punter amb comptador de referències; free_rckey() per desallotjar la regió
  • open: comprova que la regió no ha estat desallotjada i en garanteix l'accés

...

Eines[modifica | modifica el codi]

buildlib (adaptació a biblioteques C)[modifica | modifica el codi]

Vegeu.[22] Extreu informació de tipus, d'arxius capçaleres de C instal·lades al sistema i les converteix a capçaleres de Cyclone incorporant els tipus que intervinguin en les definicions.

Cal crear un arxiu d'especificació especif.cys amb indicacions per a cada capçalera.

sys/types.h: 
  include {tipusA tipusB ...}
  ;
els_meus/biblio.h:
  include {tipusD tipusE ...}
  ;

Els arxius de capçalera a tractar han d'estar a /usr/include o /usr/local/include (si vols fer-ho amb un arxiu de capçalera en un altre directori, has d'establir i exportar la var. d'entorn C_INCLUDE_PATH o CPLUS_INCLUDE_PATH) i el nom de directori dins l'arxiu no pot tenir especificació de versió, per ex. "-2.0" (caldrà posar-lo directament a C_INCLUDE_PATH). El resultat va al directori ./BUILDLIB.OUT o al directori especificat a l'opció -d

Cal executar amb l'opció -v (verbose) per comprovar si hi ha hagut errors.

buildlib -v especif.cys

Referències[modifica | modifica el codi]

  1. Univ. de Maryland - Cyclone: Un dialecte de C amb seguretat en els tipus (anglès)
  2. AT&T - Cyclone - Un dialecte de C amb tipus segurs (anglès)
  3. Cyclone - Descàrrega i instal·lació (anglès)
  4. Pointers(anglès)
  5. Pointer subtyping(anglès)
  6. Cyclone - Subtipus de punters
  7. Pointer coercions(anglès)
  8. Switch statements(anglès)
  9. Tagged Unions and Datatypes(anglès)
  10. Datatypes(anglès)
  11. Extensible Datatypes(anglès)
  12. Polymorphism(anglès)
  13. Pattern matching(anglès)
  14. Cyclone - La instrucció switch
  15. Existential types(anglès)
  16. Greg Morrisset - Static Extended Checking Verificació estàtica
  17. Type-checking Regions(anglès)
  18. Univ. d'Edimburgh - Avenços en llenguatges: regions(anglès)
  19. Cyclone - Efectes, capacitats i restriccions de subconjunts d'efectes
  20. M. Tofte and J.-P. Talpin: Implementation of the Typed Call-by-Value lambda-calculus using a Stack of Regions (anglès)
  21. Restricted Pointer Aliasing(anglès)
  22. Cyclone - buildlib (anglès)

Enllaços externs[modifica | modifica el codi]