V dnešním díle bych chtěl blíže pohovořit o tom, proč považuji používání naší funkce filter() za bezpečné a rozebrat ji z pohledu jednoho z kritérií správnosti kódu. Předpokládejme, že tzv. Murphyho zákony platí a tudíž není obecně možné projít zdrojový kód celé aplikace, dokonale mu porozumět ve všech souvislostech a odhalit všechny potenciální chyby. Pokud tedy za takovýchto podmínek chceme provádět audit kódu, ať už pomocí „zkušeného oka“ nebo pomocí nějakého nástroje pro statickou analýzu, musíme si stanovit kritéria správnosti.
Správný kód
1. Dělá všechno, co dělat má a přesně tak, jak má. Například kalkulačka umí správně sčítat, odčítat, násobit a dělit.
2. Nedělá nic, co dělat nemá
Zatímco ke zhodnocení správnosti provádění výpočtu slouží různé metody testování, otestování toho, že program za žádných okolnosttí nedělá, co nemá, není snadné. Příkladem může být například „trojský kůň“, který za normálních okolností funguje jako kalkulačka, ale 29. února ve 13:00 zaplní celý disk, sežere celý výpočetní výkon procesoru nebo pošle obsah souborů /etc/passwd a /etc/shadow na nějaký FTP server.
Příklady nežádoucího chování programu mohou být:
1. Program zapisuje, kam nemá (disk, paměť, TCP/IP…)
2. Program zneužívá nějaký známý exploit a získává přístup na úrovni uživatele root
3. Výpočet se dostane do nekonečného cyklu
4. Program za nějakých okolností vyvolá výjimku
5. Výpočet trvá v některých případech neúnosně dlouho
Jak si poradit s hrozbou nekonečného cyklu
V tomto díle bych se chtěl zaměřit na tzv. halting problem (česky problém zastavení), což je statická analýza programového kódu, která má rozhodnout, zda se celý program nebo jeho část (procedura nebo funkce) někdy zastaví. Alan Turing už v roce 1936 dokázal, že obecný algoritmus, který toto umí pro každý program, nelze sestrojit.
Rozhodně ale lze sestavit algoritmus, který toto dokáže rozhodnout pro některé programy. Existují operace, o kterých víme (resp. předpokládáme na základě znalosti výstupu kompilátoru nebo funkce interpretu), že skončí. Např. sčítání dvou celých čísel. Následující kód zcela jistě skončí a není nutné to dále dokazovat:
int i = 1; int j = 2; i = j + i;
Pokud si vystačíme s takovýmto jednoduchým programem, není co řešit. Pokud ale potřebujeme rozhodnout o zastavení výpočtu obecné procedury nebo funkce, dostáváme se zpátky k algoritmicky neřešitelnému problému. Pokud si nepomůžeme jinak. Problém představují cykly (které obecně nemusí skončit nikdy) a rekurze (které skončí až tenkrát, když vyčerpají prostředky programu přidělené, typicky maximální velikost zásobníku). Problém je, že bez cyklů nebo rekurzí se ve složitějších programech těžko obejdeme, ale cykly používat nesmíme, protože jinak nedokážeme obecně zjistit, zda se program zastaví.
Funkce typu filter() tento náš problém řeší. U těchto funkcí dokážeme relativně snadno rozhodnout, za jakých okolností se jejich výpočet zastaví. Šabloně funkce filter() prohlédneme a vystavíme certifikát, který prohlásí, za jakých okolností se funkce zastaví. A statický analyzátor na základě takového certifikátu snadno zjistí, zda se volání takové funkce někdy zastaví. Představme si následující kód:
HALTS("halts(func)") template<typename T> list<T> filter(const list<T> &originalList, bool (* func)(const T &)) { list<T> newList; typename list<T>::const_iterator it; for (it = originalList.begin(); it != originalList.end(); it++) { if (func(*it)) newList.push_back(*it); } return newList;
}
Naše stará dobrá šablona funkce filter() dostala certifikát, který říká, že se výpočet zastaví v případě, že se zastaví callback funkce, kterou do funkce filter() posíláme jako parametr. Pokud tedy analyzátor dokáže analyzovat volání funkce s takovýmto certifikátem a dokáže ověřit, zda se funkce func zastaví, dokáže také určit, zda se zastaví kterékoliv konkrétní volání funkce filter().
Naše volání v minulém díle vypadalo následovně:
filter(l, isEven)
takže zbývá analyzovat funkci isEven(), která vypadala takto:
bool isEven(const int &i) { return ((i % 2) == 0); }
Jak je vidět, funkce provádí triviální operaci modulo, porovnání dvou celých čísel a vrací výsledek tohoto porovnání. S takovou funkcí si i velmi primitivní statický analyzátor poradí. Pokud analyzátor nezná zdrojový kód funkce isEven(), například proto, že je umístěna v nějaké knihovně, můžeme mu opět napovědět:
HALTS("true") extern bool isEven(const int &i);
Statický analyzátor rozumí deklaraci certifikátu, takže teď zbývá pouze vytvořit makro, které zařídí, že takovýto certifikát bude kompilátor jazyka C++ ignorovat. Makro může vypadat následovně:
#define HALTS(x)
Používání funkce filter() je bezpečný programátorský idiom, který zajistí, že program nebude dělat, co nemá (minimálně z hlediska hrozby nekonečného zacyklení). O této funkci můžeme ale prohlásit i to, že nezapisuje nikam jinam, než do svých lokálních proměnných, nezneužívá žádný exploit, nemá tendenci k vyvolání výjimky (v úvahu připadá vyčerpání volné paměti) a dobu výpočtu lze předvídat, protože je funkcí délky seznamu a výpočetní náročnosti callback funkce. Podobným způsobem, jakým jsme udělili certifikát garance zastavení výpočtu funkce, můžeme vydat certifikát paměťové náročnosti, výpočetní složitosti, absence vedlejších efektů funkce (tedy že funkce nezapisuje, kam nemá) atd. Důsledné používání podobných idiomů nám zajistí velmi dobrou předvidatelnost chování programu, která je srovnatelná s kódem ve funkcionálních jazycích a nesrovnatelně lepší, než je předvídatelnost obecného programu v C# nebo v Javě, tedy jazycích, které pan LO stavěl na vyšší úroveň než C++.
nejako to nechapem. V com sa akoze dokazanost spravnosti programu zlepsila? (neberiem do uvahy kvalitu kodu). Transformaciou jedneho cyklu na iny? Ale mozno len nechapem dobre vasu ideu ale nevidim tam nejaky velky posun k celkovej dokazatelnosti programu (tj. lubovolny realny program ktory robi viac ako scitava 2 cisla)
Ja fakt strasne nerad kritizuji, ale tohle bylo fakt podivne zvolene. Nekonecny cyklus je vec, kterou v dnesni dobe (bohuzel zatim jako jednu z male veci) dokazou verifikovat automaticke nastroje.
Radeji bych se zameril na design by contract, nebo dukladne probrat automaticke ukazatele, pripadne funktory nebo dukladne pouzivani const.
Pripadne to vsechno ukazat na nejakem hezkem prikladu, treba na implementaci koherentni cache.
Zakladni vyhodou C++ neni to ze jde psat bezpecne, ale to ze v C++ jde psat bezpecne bez vyrazneho dopadu na vykon programu. Silna podpora pro statickou kontrolu primo v jazyce a slusna podpora pro externi staticke analyzatory diky jednoduche extenzibilite jazyka jsou presne to co dela z C++ velice bezpecny jazyk.
Díky všem za odpovědi.
[1] Ten statický analyzátor musí, žel, někdo napřed napsat. Můj seriálek je o principech a ne o konkrétních nástrojích.
[2] Když udělám jednu funkci a tu zavolám právě jednou, zlepšení je poměrně zanedbatelné. Pokud ale vytvořím nějaký bezpečný idiom, který lze používat znova a znova, situace je výrazně lepší.
[3] Já jsem za kritiku naopak vděčný! Hlavním účelem mého seriálu je rozproudění diskuse a rozšíření obzorů. U prvního článku byla diskuse poměrně bohatá, ale nechtěně jsem ji zazdil, když jsem nevypnul moderování příspěvků. To mě dost mrzí.
Rád věřím tomu, že triviální nekonečný cyklus typu while(true){} lze snadno detekovat, ale o ten mi ani tolik nešlo. Složitý cyklus s podmínkou, která je závislá na komplikovaném výpočtu, to je tvrdší oříšek. Jsem přesvědčen o tom, že i takovým případům lze zatrhnout típec podobnými technikami, jaké jsem zatím naznačil.
Za tipy děkuji, design by contract a používání const jsou směry, kterými se moje myšlenky už zaobírají.
Jinak souhlasím.
[4] Nejenom SPARK. O tomto jazyce jsem dosud neslyšel, díky za tip!
"Naše stará dobrá šablona funkce filter() dostala certifikát, který říká, že se výpočet zastaví v případě, že se zastaví callback funkce, kterou do funkce filter() posíláme jako parametr."
Smělá hypotéza :-) Obávám se, že C a C++ dávají mnoho neuvěřitelných možností, proto podobným úvahám nepůjde nikdy plně důvěřovat. Co když:
1) je chyba v metodě begin (neskončí)?
2) je chyba v metodě end (neskončí)?
3) je chyba v begin, nebo end a operátor ++ "posunující" iterátor nikdy nedojde z begin na end?
3) je chyba v operátoru ++ pro iterátor (neskončí, nebo se neposune na další prvek)?
Asi se bude jednat o list z STL. Opravdu tomu standardu tak věříte? Psali ho obyčejní lidé :-) Kdo ví jakým překladačem to bude překládáno a tedy jaká implementace STL bude použita.
Kdyby jsme brali v úvahu, že STL je důvěryhodné, co když funkce, která příjde jako parametr je špatně napsaná. Sice skončí, ale zapíše něco do paměti tam, kam nemá. Při troše štěstí zapíše něco přesně na místo, kde je iterátor "it" a to tak, že ho posune zpět. Operátor++ a volaná funkce budou posouvat iterátor do nekonečna tam a zpět.
Myslím, že potenciálních problémů je dost a to jsme ještě ani nevzali v úvahu fakt, že proces může mít více vláken, která sdílejí adresní prostor.
[6] Nemám pocit, že bychom se s LO úplně míjeli, ale pokud snad (a to nevylučuju) někdy sepíšu nějaký delší text na základě tohoto seriálku, určitě se tam náš oblíbený troll nedostane. A ten text bude vypadat zřejmě výrazně jinak (docela zajímavé srovnání nabízí původní draft knihy Programming in Scala (Odersky a spol.) a výsledná podoba).
Děkuju za reakci.
[8] No tak kdybychom byli takhle důslední, mohli bychom se ptát, kde je jistota, že kompilátor vygeneruje odpovídající kód, že procesor správně počítá (známá FDIV chyba starých Pentií) atd. Kde je jistota, že správně funguje JVM, CLR, GHC, ocamlc, SBCL...?
Ale dobrá, zpátky k STL. Samozřejmě, že by bylo vhodné mít danou implementaci ověřenou. Jak vyplývá z 1. dílu, jedná se o Linux a tedy v úvahu připadá v podstatě jenom gcc a implementace, která se normálně přidává do distribucí. Ale obecně je třeba říct, že kontrola, kterou jsem měl na mysli, se týká aplikačního kódu a ověření jeho správnosti při znalosti specifikace chování používaných knihoven.
Vlákna bych do této úvahy naopak netahal. Vyšetřovat chování jednotlivých stavebních bloků aplikace lze opět jenom za předpokladu, že je nahlížíme izolovaně. Ověření správnosti předávání dat mezi vlákny a toho, že si vzájemně nelezou do zelí (např. důsledné používání nějaké obdoby aktorového modelu s předáváním konstantních objektů) je třeba tak jako tak vyšetřit zvlášť.
Díky za reakci.
[8] [10] Plus existuje moznost, ze pro nejakou tridu T existuje "divoka" specializace std::list (proto je asi lepsi predpokladat o std::list, ze kazda je well-behaved a resit jenom filter()).
Pro model checking existuje spousta nastroju a logik, jenze a) je to (casove) narocny b) overi to urcite vlastnosti a o jinych to nic nerekne. Proto treba existuji dokazatelne bezpecne algoritmy (za danych predpokladu), ktere je mozne naborit side-channel utokem (timing attack etc.).
Zdanlive nesouvisejici vec: dokumentace. Podle ni se da celkem dobre odhadnout kvalita kodu/frameworku. Pokud nevite, kdo ktery objekt vlastni (manual cleanup/auto_ptr/shared_ptr), kto ma jen weak pointer, jake predpoklady ma metoda o parametrech, pak prinejlepsim vzniknou memory leaky, v horsim pripade "mrtvy" objekt muze delat co chce.
Jinak chvalim temu (mne by se to psat nechtelo protoze vim jak je to slozity ;-)), ale vic bych se soustredil na navrhove vzory nez na dokazovani.
BTW nekdo v minulem dile uvedl boost::lambda - pekna vec, dokud nepotrebujete volat nejakou metodu/funkci (jinak boost::lambda::bind() polovinu elegance a citelnosti ubere). Lambda funkce v C0x budou super ale chvili to potrva...
Důsledné používání podobných idiomů nám zajistí velmi dobrou předvidatelnost chování programu. To jistě ano, ale musíte nějak *zajistit*, že v kódu nebudou použité nebezpečné konstrukce, které jazyk C++ umožňuje.
V C# nebo Javě má kód automaticky zaručenou řadu vlastností, které vyplývají z vlastností daného jazyka a jeho knihoven. Síla managed jazyků je právě v tom, že ať nakrmíte kompilátor čímkoliv, tak nedojde například k přístupu mimo hranice pole, invarianty zůstanou určitě invarianty atd.
Abyste dosáhl podobného výsledku v C++, musel byste z jazyka úplně *odstranit* řadu features (včetně odstranění možnosti používat pointerovou aritmetiku), zahodit kompatibilitu s POSIX a ANSI C, a vytvořit knihovny, které by podporovaly rysy nového jazyka. Ovšem proč to dělat, když už to udělali autoři Javy a C#, a po pár stovkách člověko-let byste zřejmě došel k dost podobnému výsledku.
To co popisujete u C++ je možné provést ad absurdum u assembleru. Prostě budete používat vybrané bezpečné konstrukce (třeba nějaká makra), a spoléhat na to, že žádné nebezpečné konstrukce nikdo nepoužil. Jenže je asi zjevné, že to problém neřeší.
[12] to, ze se z jazyka odebere par potencialne nebezpecnych featur ho jeste nedela bezpecny. ...zustava tu spousta krasnych veci jako preteceni hodnot nebo fakt, ze kazda _funkce_ muze vyhodit vyjimku (nebo provest jiny side effect), aniz by to programator tusil,...
on je totiz rozdil mezi programem o kterem si myslite, ze je bezpecny a programem u nehoz je to dokazane...
[13] scheme rulez! zajimavym jazykem, bezpochyby inspirovanym schemem, je bitc, ktery by mel umet dokazovat, ze program je korektni... zatim jsem to nezkousel, ale uz par let si na to delam cas... ;-]
[14] Přetečení hodnoty v .NETu i v Javě vyvolá výjimku. Když dojde k výjimce, opravdu se nestane, že by o tom programátor nevěděl, protože postupně bude propadávat kódem, a pokud jí nikdo neošetří, tak program sletí. Srovnejte se situací v dnešním C/C++, kde autor aplikace musí testovat návratové hodnoty po každém volání API, což ale v praxi nedělá.
Samozřejmě statická analýza je další level. Jenže jak chcete dělat statickou analýzu nad kódem, kde strcpy() může znamenat "zkopíruj string", nebo také "přepiš v paměti aplikace cokoliv a kdekoliv"? Tam vás side effects netrápí?
[15] Přetečení hodnoty v .NETu i v Javě vyvolá výjimku. --- tak jakou vyjimku v jave vyhodi nasledujici kod: ,,int x = Integer.MAX_VALUE + 1;''
Srovnejte se situací v dnešním C/C++, kde autor aplikace musí testovat návratové hodnoty po každém volání API, což ale v praxi nedělá. --- to neni problem jazyka, ale programatora
Jenže jak chcete dělat statickou analýzu nad kódem, kde strcpy() může znamenat "zkopíruj string", nebo také "přepiš v paměti aplikace cokoliv a kdekoliv"? --- naprosto jednoduse... ;-]
Díky za další spršku reakcí (no, bez některých bych se obešel, ale stejně dík ;)
[11] Návrhové vzory jsou fajn téma, tento díl vznikl hlavně proto, že pod 1. dílem byly pochybnosti o užitečnosti a bezpečnosti funkce filter(). A taky mě zajímalo, jak zmíněná metoda analýzy kódu obstojí v diskusi. Děkuju za podnětný příspěvek a podporu.
[12] Bezpečnost je proces, to tvrdí i Microsoft. ;) Namísto Javy bych preferoval Scalu a namísto C# bych sáhnul třeba po F#, když už. Nemyslím, že by bylo nutné odstraňovat nějaké vlastnosti C++, stačí je eliminovat v kódu nebo jim věnovat obzvláštní pozornost. Podobný přístup používá i C#, ne? V asembleru by to bylo velice obtížné až nemožné, protože nemá typovou kontrolu apod. C++ je o několik úrovní výše a ten "Lisp" (jak někdo napsal pod minulým dílem) se z něj dá udělat poměrně komfortně.
[13] Takhle snad přece jenom ne... Kdybych chtěl (nedej Bůh) psát o Scheme, psal bych o Scheme. Já jsem chtěl z nějakého důvodu psát o C++, tak to zkuste respektovat.
[15] Minimálně se dá zjistit, že někdo strcpy vůbec volá. V C++ k tomu není důvod a i v C jsou lepší možnosti, jak pracovat s řetězci. Výjimka je lepší, než když program tiše hnije, ale výjimky neřeší zdaleka všechno. Hlavní problém shledávám v divokém imperativním kódu, kterého nás automaticky nezbaví ani C# ani Java.
[14, 16] Díky za podporu. ;)
[8] Samozřejmě by bylo možné HALTS upravit tak, aby to certifikovalo i STL konstrukce. Ale vzhledem k tomu, že STL je součást ISO standardu jazyka, tak bychom rovnou nemuseli věřit ani kompilátoru a interpreteru (také je napsali lidé) a kde jsme s tou bezpečností v C# a Javě?
Ta funkce func samozřejmě důvěryhodná není, proto je také uvedeno v HALTS, že na ní závisí důvěryhodnost funkce filter.
Pokud se bude každé vlákno chovat správně, pak se bude chovat správně i ve vícevláknovém prostředí (záměrně opomíjím komunikaci mezi vlákny, protože té se funkce filter netýká).
[12] Nebezpečné konstrukce mohou být použity, pokud lze zaručit, že nevykonají nic špatného, třeba operátor++ u většiny iterátorů udělá to, že inkrementuje svůj vnitřní ukazatel, přitom konstrukce it != end zaručuje, že nepřeteče mimo svoje pole (u std::list to zrovna nedělá kvůli povaze listu).
Z C++ se nemusí nic odstraňovat. Je nutné si být vědom, co děláš, ne programovat jako zběsilý (jak to dělá spousta javovských pisálků).
[14] .NET neznám, ale přetečení hodnoty v Javě výjimku opravdu nevyhodí. Pokud programátor netestuje návratové hodnoty, je prase. V C++ jsou také výjimky.
Pořád pleteš C a C++. V C++ se strcpy nepoužívá (a ani tam není explicitně definované, je pouze uvedeno, že je v cstring), v C++ jsou std::stringy (a ani ty strcpy nepoužívají). Ale i kdyby strcpy bylo vhodné použít, pořád lze ověřit, že bude kopírovat správně, pokud je použita ve správném kontextu (víme, co je na vstupu i na výstupu).
[8, 18] Ono to s tím certifikátem HALTS může být ještě horší - pokud by "func" měnila it, znamenalo by to nedefinované chování, což se dá ověřit a vyloučit. Pokud by ale func měnila přímo ten seznam (originalList), například tak, že něco přidá na konec, tak se nemusí dopustit žádného nedefinovaného chování, pokaždé skončí a přesto filter(originalList, func) nikdy neskončí.
[17] Jestli mluvíte o pre-processoru, který nebezpečné konstrukce nepustí dál, tak to by šlo. Jinak to nemá smysl, protože zase spoléháte jen na to, že programátor něco neudělá. Jenže programátoři jsou lidi, a dělají velkou spoustu chyb. Tomu nelze nijak zabránit. Jinak C# se mi líbí, a nevidím důvod používat okrajový jazyk typu F#.
Výjimky samozřejmě neřeší vše, ale je to potřebný mechanismus. Právě to, že C/C++ programy tiše hnijí, když se něco nepovede, je příčinou velké spousty problémů.
Strcpy budete těžko ověřovat, když máte například pointery na funkce. Prostě při analýze nebudete tušit, kdo nebo s jakými parametry zavolá kód, který strcpy použije. Naproti tomu v .NETu/Javě to není problém, protože neexistuje možnost, že by došlo k nepravostem.
Jak jsem psal, C++ by blyo možné použít, pokud byste zajistil, že se nebezpečné konstrukce nebudou vyskytovat (ano, preprocessor může být řešení), zahodil POSIX, zahodil kompatibilitu s ANSI C, a napsal nové frameworky používající bezpečné konstrukce. Ovšem výsledkem by spíše něco jako MS C++/CLI.
Co konkrétně máte na mysli "divokým imperativním kódem"?
Děkuji za další reakce, píšu v provizorních podmínkách, takže zatím jenom krátce:
[19, 21] Žádné bingo se nekoná. Funkce func() má jakožto parametr konstantní referenci na list. To znamená, že přidat prvrk na konec listu zase tak snadno nelze. Nedefinované chování neřešíme, jde o to, že určité operace jsou v některých kontextech nepřípustné.
[22] Bohužel, bingo se koná, protože to, že funkce filter() bere konstantní refernci na list ani to, že func() bere konstantní refernci na objekt, nezaručuje že se během volání funkce func() nezmění. Nedefinováné chování zmiňuji proto, že dost příspěvků tady mluví o měnění it, přetečení mezí polí, přetečení integeru (jen znaménkové typy) - a to je právě nedefinované chování. MMCH, funkce func() může filter() donutit k nedefinovanému chování, konkrétně porovnání iterátorů z různých seznamů a následně dereference past-the-end iterátoru, přičemž func() se nedefinovaného chování nedopustí. Víte jak?
[21] Ale v Javě by to bylo úplně stejné. Jediné, co by pomohlo, by byla referenční integrita ve smyslu funkcionálních jazyků.
[23] Pokud použijeme přetypování ukazatelů, lze dosáhnout lecčehos, pamatuju si, že ve Visual C++ 6.0 například bylo možné přistupovat pomocí přetypování přistupovat i k chráněným atributům třídy. Nemám teď po ruce g++, takže nemůžu tyhle věci vyzkoušet. Předpokládám, že se i pro tu fintu s iterátorem iterátor použije nějaká vypečená finta s ukazateli. Koneckonců, pokud znám pořadí uložení atributů třídy v paměti, mohu změnit cokoliv, včetně ukazatelů v listu.
[10] [18] Nechtěl jsem přímo zpochybnit STL.Je jasné, že něčemu věřit musíme. Hardware, operační systém, u některých programovacích jazyků i běhové prostředí (JRE) atd... Já jen, že i na to je potřeba myslet a navíc z toho příkladu nejde poznat jestli se jedná o standardní kontejner z STL v prostoru jmen std, nebo nějaký jiný se stejným rohraním.
Šlo mi ale hlavně o to, že v čláku je:
"Naše stará dobrá šablona funkce filter() dostala certifikát, který říká, že se výpočet zastaví v případě, že se zastaví callback funkce, kterou do funkce filter() posíláme jako parametr."
což není pravda. Může být splněn předpoklad (funkce func se zastaví) a nesplněn důsledek (funkce filtr se nezastaví). Ať už za cenu nedefinovaného chování func (jak jsem psal), nebo jak je v [19] a [23]. Těch předpokladů musí být splněno více. Obávám se, že tak hodně (protože C i C++ dává programátorovi velkou svobodu), že nezbyde, než říct nějakou obecnou nic neříkající frázi třeba: "Funkce func musí být naprogramována bezchybně, aby funkce filtr skončila". Jenomže bezchbyně se snažíme dělat přece všechno. Ale kde vzít jistotu, že je opravdu bezchybná?
[18]
"V C++ se strcpy nepoužívá (a ani tam není explicitně definované, je pouze uvedeno, že je v cstring), v C++ jsou std::stringy (a ani ty strcpy nepoužívají)."
Takže tam strcpy deklarována je. Stačí #include a jedem :-) A nejhorší je, že i kdyby nebyla, tak tam je například šablona std::copy, která jako parametry může mít i ukazatele a ty se mohou odkazovat kdoví kam.