Cyclone

Cyclone
Tipus	llenguatge de programació
Data de creació	2002
Disseny	AT&T Labs
Desenvolupador	AT&T
Influenciat per	C
Pàgina web	cyclone.thelanguage.org

El Cyclone és un llenguatge de programació derivat del llenguatge C creat per tal de 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 va començar com un projecte conjunt entre AT&T Labs Research^[2] i el grup de Greg Morrisett a la universitat Cornell, el 2001. La versió 1.0 va sortir el 8 de maig de 2006

Noves característiques

El 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

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

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

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

espai de noms

 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

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

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

llista per comprensió

{ 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

Estructures anònimes, per ex.:

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

unions etiquetades

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

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

 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

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

 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

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 existencials

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

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

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) dona 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

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

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

allotjament dinàmic al munt

(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

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

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

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

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

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)

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

buildlib (adaptació a biblioteques C)

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

↑ Univ. de Maryland - Cyclone: Un dialecte de C amb seguretat en els tipus (anglès)
↑ AT&T - Cyclone - Un dialecte de C amb tipus segurs (anglès)
↑ Cyclone - Descàrrega i instal·lació (anglès)
↑ Pointers(anglès)
↑ Pointer subtyping(anglès)
↑ Cyclone - Subtipus de punters
↑ Pointer coercions(anglès)
↑ Switch statements(anglès)
↑ Tagged Unions and Datatypes(anglès)
↑ Datatypes(anglès)
↑ Extensible Datatypes(anglès)
↑ Polymorphism(anglès)
↑ Pattern matching(anglès)
↑ Cyclone - La instrucció switch
↑ Existential types(anglès)
↑ Greg Morrisset - Static Extended Checking Arxivat 2007-10-13 a Wayback Machine. Verificació estàtica
↑ Type-checking Regions(anglès)
↑ Univ. d'Edimburgh - Avenços en llenguatges: regions(anglès)
↑ Cyclone - Efectes, capacitats i restriccions de subconjunts d'efectes
↑ M. Tofte and J.-P. Talpin: Implementation of the Typed Call-by-Value lambda-calculus using a Stack of Regions Arxivat 2011-06-09 a Wayback Machine. (anglès)
↑ Restricted Pointer Aliasing(anglès)
↑ Cyclone - buildlib (anglès)

Enllaços externs

Cyclone - Lloc web oficial

[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)

[subtipus-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 Arxivat 2007-10-13 a Wayback Machine. 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 Arxivat 2011-06-09 a Wayback Machine. (anglès)

[21] Restricted Pointer Aliasing(anglès)

[22] Cyclone - buildlib (anglès)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]