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.Univ. de Maryland - Cyclone: Un dialecte de C amb seguretat en els tipus El seu desenvolupament va començar com un projecte conjunt entre AT&T Labs ResearchAT&T - Cyclone - Un dialecte de C amb tipus segurs 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óCyclone - Descàrrega i instal·lació
// 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); return 1; } printf("Hola des de Cyclone, %s\n", args); 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 puntersPointers es controla amb anotacions específiques, per ex.: int *@notnullEn una crida a funció que admet punters d'un tipus, se n'hi pot posar un que en sigui subtipus,Pointer subtyping é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:;Cyclone - Subtipus de punters *@numelts(n) abreviat *{n} punter a vector de n elements insereix comprovació de límits a les expressions que l'indexenexcepte 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.Pointer coercions 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.Switch statements ...
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 = { for i < 100 : 2*i }
tuples Estructures anònimes, per ex.:
$(int, char*) parell = $(10, "abc") ;
unions etiquetades Vegeu ref.Tagged Unions and Datatypes @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.DatatypesExtensible Datatypes 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.Polymorphism
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,x);
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.Pattern matching
int suma($(int,int,int) args) { let $(x,y,z) = args; return (x+y+z);
En un switch:Cyclone - La instrucció switch
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.Existential types 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"Greg Morrisset - Static Extended Checking Verificació estàtica
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.Type-checking Regions L'allotjament es materialitza en regions:Univ. d'Edimburgh - Avenços en llenguatges: 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.Cyclone - Efectes, capacitats i restriccions de subconjunts d'efectes
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.M. Tofte and J.-P. Talpin: Implementation of the Typed Call-by-Value lambda-calculus using a Stack of Regions
#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.Restricted Pointer Aliasing 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ó