# Cyclone

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. El seu desenvolupament va començar com un projecte conjunt entre AT&T Labs Research 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ó
Compilació i execució

## Restriccions i comprovacions

Cyclone introdueix les següents restriccions i comprovacions:
* El maneig de punters 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, é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:;

   ### *@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.
* 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.

## Característiques de més alt nivell

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

### subtipus estructurals

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

### llista per comprensió

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

### tuples

Estructures anònimes, per ex.:

### unions etiquetades

Vegeu ref.

### datatypes a l'estil de ML

Vegeu ref.

### funcions polimòrfiques

Vegeu ref.
* les variables de tipus es prefixen amb la cometa revessa (accent greu seguit d'espai) `
* cal fer servir `a en lloc de (void *)

### encaixos de patrons

Vegeu ref.
En un switch:

### tipus existencials

Vegeu ref. 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.

### tipus dependents de valors i relació amb predicats

Per ex. el tipus de int A[n]. Vegeu "Verificació estàtica"
Les crides han de satisfer la precondició @requires estàticament

### allotjament

Vegeu ref. L'allotjament es materialitza en regions: à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.
    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

#### 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.

##### 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.

##### allotjament amb multiplicitat de referències (punters) restringida

Vegeu ref. 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 = ...

##### 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

##### 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

##### 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. 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.
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.

## 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