Ugens bommert
En af glæderne ved at have en blog er, at man få lov at udstille sine egne bommerter. Måske i håbet om, at nogle af jer andre derude kan genkende det, fordi I også kvajer jer en gang imellem? Nå, eneste lyspunkt er, at jeg i det mindste selv nåede at opdage ugens bommert inden den blev releaset.
En hurtig quiz:
Hvad er der galt med følgende stykke java-kode:
public static Integer getValue(int start, int end, int step, int iteration) { int val = start + iteration * step; if (val > end) { return null; } return val; }
hvorom man ved, at start, end og step er positive tal, iteration er ikke-negativt og start < end.
Nå, har du tænkt over det?
Umiddelbart virkede det jo meget tilforladeligt, synes jeg. Men men men... Hvis der kommer nogen og kalder metoden med et meget højt tal for f.eks. iteration, så laver start + iteration * step overflow, og da en int i Java er signed, kan val ende med at blive et negativt tal. Og så duer testen for om val > end jo ikke til at finde ud af, om den pågældende iteration findes eller ej.
Suk.
Mere kaffe, anyone?
Om Anne-Sofie NielsenAnne-Sofie Nielsen er udviklingschef hos Kapow Software og har en baggrund som civilingeniør i informatik fra DTU. Har aldrig helt fået besluttet sig for at være en nørd eller ej.
Follow @femalenerdKommentarer (29)
Hvis step<0 kan du få en værdi tilbage, der er mindre end start.
[edit: jeg havde overset, at man ved at step>=0.]
-
0 -
0
Så i øvrigt lige, at artiklen "Her er de 25 kodefejl, du absolut skal undgå" (http://www.version2.dk/artikel/13922-her-er-de-25-kodefejl-du-absolut-sk...) har Integer overflow som nr. 17...
I øvrigt lidt pudsigt, synes jeg, at Java - som ellers er meget flink til at kaste exceptions hvis man f.eks. får indekseret udenfor et array, ikke giver en lyd fra sig, hvis man med almindelige aritmetiske operationer får lavet overflow.
-
0
-
0
I øvrigt lidt pudsigt, synes jeg, at Java - som ellers er meget flink til at kaste exceptions hvis man f.eks. får indekseret udenfor et array, ikke giver en lyd fra sig, hvis man med almindelige aritmetiske operationer får lavet overflow.
C# har et 'checked'-nøgleord, som specificerer, at compileren skal kontrollere for overflow og kaste en exception hvis det er tilfældet. '/checked' er desuden en compiler option, som betyder at operationer på integral types altid bliver kontrolleret - med mindre man specificerer 'unchecked' for en kodeblok.
Findes der ikke noget tilsvarende i Java?
-
0
-
0
Ideelt set bør defaulttypen for heltal være ubegrænsede heltal. Det er det f.eks. i Scheme og Haskell.
Hvis man gerne vil have en bestemt størrelse (til f.eks. bitvektorer eller til at regne modulo 2^n), kan man specificere dette eksplicit.
Det følger princippet om, at default er den sikre, overløbsfri datatype, og at man skal gøre noget aktivt for at bruge den usikre datatype. Dermed markerer man, at man har tænkt over det.
-
0
-
0
... er at der mangler en assert(start <= val && val <= end); inden return val. ;)
-
0
-
0
Ideelt set bør defaulttypen for heltal være ubegrænsede heltal. Det er det f.eks. i Scheme og Haskell.
Hov, Torben, det var jo min ide til et indlæg du stjal. Men, det er også default-typen i Erlang. Jeg mener at Joe Armstrongs Ph.d. thesis har eksemplet hvor det at fixe en overflow-bug er for dyrt. Det er nemmere hvis fejlen ikke kan opstå og så tage det eventuelle performance-drop.
-
0
-
0
Fejlen bunder jo i manglende brug af værdi-begrænsende undertyper. Alle formelle parametre er af typen 'int' og så er det jo svært at vise noget som helst, udover at overflow let kan forekomme.
At "man ved", at 'start', 'end' og 'step' er positive tal, 'iteration' er ikke-negativt og 'start' < 'end' hjælper jo ikke meget, hvis der skal stilles garantier.
Mere kaffe, anyone?
Nej tak, men et ordetligt programmeringssprog, der ikke tillader sådanne fejl vil da ikke være at foragte. Det er ikke nok at være omhyggelig.
-
0
-
0
Spec# kommer tæt på. Her bliver assertions statisk checket, og du får en warning, hvis en assertion ikke kan verificeres statisk. Du kan så vælge at markere den assertion som dynamisk (hvorved den bliver checket på køretid) eller indsætte flere statiske assertions for at hjælpe bevissystemet.
-
0
-
0
I øvrigt lidt pudsigt, synes jeg, at Java - som ellers er meget flink til at kaste exceptions hvis man f.eks. får indekseret udenfor et array, ikke giver en lyd fra sig, hvis man med almindelige aritmetiske operationer får lavet overflow.
Det er egentligt et spørgsmål, om hvad "int" betyder. I Java og C betyder det en heltalsring modulo 2^n (hvor n er ordstørrelsen), og her er overflow ikke passende, og -x == 2^n-x gælder, hvilket ikke er tilfældet for "rigtige" heltal. Man skal dog være lidt varsom med x<y, som i givet fald betyder, at 0 <= y-x < 2^(n-1).
Egentlig synes jeg ikke, at det er et problem: Det giver god mening at regne modulo 2^n. Men typenavnet bør selvfølgelig ikke være "int", men "Z32", "Z64" eller lignende. "int" eller "integer" bør kun bruges til ubegrænsede heltal. Derudover kan man have typer af formen "min..max", hvor min og max er heltal. Disse typer kan indeholde alle tal fra min til max og skal give fejlmeddelelse, hvis man gemmer et tal undenfor intervallet i en variabel af denne type. Pascal har den slags typer, men desværre også en maskinafhængig type "integer". Det havde været perfekt, hvis "integer" var defineret til ubegrænsede heltal, og man skulle bruge min..max, hvis man ville have begrænsede tal.
-
0
-
0
Spec# kommer tæt på. Her bliver assertions statisk checket, og du får en warning, hvis en assertion ikke kan verificeres statisk. Du kan så vælge at markere den assertion som dynamisk (hvorved den bliver checket på køretid) eller indsætte flere statiske assertions for at hjælpe bevissystemet.
Jeg foretrækker stadig SPARK :-)
Det virker som om Spec# er ret "hot" i de akademiske miljøer - måske fordi Microsoft Research står bag.
-
0
-
0
Det er egentligt et spørgsmål, om hvad "int" betyder. I Java og C betyder det en heltalsring modulo 2^n (hvor n er ordstørrelsen), og her er overflow ikke passende, og -x == 2^n-x gælder, hvilket ikke er tilfældet for "rigtige" heltal. Man skal dog være lidt varsom med x<y, som i givet fald betyder, at 0 <= y-x < 2^(n-1).
Der er utroligt mange C-programmører, der er overraskede over, at nedenstående medfører en udefineret værdi af 'i':
int i = INT_MAX;
i++;
-
0
-
0
Er det ikke mere korrekt at sige at integer overflow fører til udefineret opførsel (eller hvordan man nu oversætter "undefined behavior")? Det kan vel (i princippet) være andet end værdien af i, det vedrører.
Det tror jeg du har fuldstændig ret i!
I praksis vil det dog nok være et spørgsmål om overflow vs. wrap-around semantik, der skiller de forskellige C oversættere.
-
0
-
0
Jeg er ked af at spamme tråden, men hvis nogen vil se det tilsvarende eksempel i SPARK og beviset for korrekthed, skal jeg nok konstruere et og poste det.
-
0
-
0
Jeg er ret interesseret i SPARK (til brug i embedded software til et medicoteknisk apparat), og blev rigtig glad da jeg så hvor meget SPARK, og en Ada compiler kan forbedre ens kode ved at udelukke hele grupper af fejl-muligheder som findes i andre sprog.
-
0
-
0
Det er det på langt de fleste systemer; men det er op til implementationen (CPU/kompiler), om den vil lave overflow check (trap) eller modulus.
Jeg blamerede mig på Linux kerne mailing listen om det for et godt stykke tid siden (http://marc.info/?l=linux-kernel&m=117862019507067&w=2) da jeg også gik ud fra, at alle C implementationer var standeard 2-complement.
-
0
-
0
[code=c]
#include <qapplication.h>
#include <qpushbutton.h>
int main(int argc, char **argv)
{
QApplication a(argc, argv);
QPushButton hello("Hello world!", 0); /* Make a
hello.resize(100, 30); small
window
a.setMainWidget(&hello); with a
hello.show(); small
return a.exec(); button */
}
[/code]
Ren begynderfejl som jeg måtte hjælpe en medstuderende med at gennemskue! :-) PS: Det her er før IDE og farver - så det er faktisk lige til at se her! :-( :-)
-
0
-
0
Ja, man skal passe på med multilinje kommentarer. :-)
Men man burde få en warning om, at main ikke returnerer en eksplicit værdi.
-
0
-
0
Det her var også før seriøse compiler warnings (koden er bare noget jeg har klippet - det var mere konceptet!
-
0
-
0
Så har jeg lavet et lille eksempel på en tilsvarende function i SPARK. Jeg undskylder på forhånd, hvis indlægget bliver lidt langt.
Først skal vi lige have terminologien på plads. Et SPARK program skal analyseres og ved analysen genereres Verification Conditions (VC'ere), der består af en række hypoteser (navngivet H1, H2, ...) og en række konklusioner (navngivet C1, C2, ...). Disse VC'ere skal bevises, dvs. det skal vises at hypoteserne medfører konklusionerne.
Så til det første forsøg på at skrive funktionen med de prebetingelser, som nævnes i blogindlægget.
[code=ada]
function Get_Value
(Start_Value : Integer;
End_Value : Integer;
Step : Integer;
Iteration : Integer)
return Integer;
--# pre Start_Value > 0 and
--# End_Value > 0 and
--# Step > 0 and
--# Iteration >= 0 and
--# Start_Value < End_Value;
[/code]
Det er generelt god stil at definere subtyper, der begrænser de mulige værdier, så jeg prøver at gøre min kode lidt pænere:
[code=ada]
function Get_Value
(Start_Value : Positive;
End_Value : Positive;
Step : Positive;
Iteration : Natural)
return Natural;
--# pre Start_Value < End_Value;
[/code]
Ovenstående er stadig ikke god stil, da der benyttes predefinerede typer, men las os bibeholde det for det dårlige eksempels skyld.
Kroppen af funktionen er som følger:
[code=ada]
function Get_Value
(Start_Value : Positive;
End_Value : Positive;
Step : Positive;
Iteration : Natural)
return Positive
is
Result : Natural;
Val : Integer;
begin
Val := Start_Value + Iteration * Step; -- Line 15
if Val > End_Value then
Result := Null_Value;
else
Result := Val;
end if;
return Result;
end Get_Value;
[/code]
Efter analyse viser det sig at der er et run-time check ved linie 15, der resulterer i VC'ere, der ikke kan bevises automatisk:
[code=text]
VCs for function_get_value :
| | | -----Proved In----- | | |
# | From | To | vcg | siv | plg | prv | False | TO DO |
1 | start | rtc check @ 15 | | | | | | YES |
2 | start | rtc check @ 18 | | YES | | | | |
3 | start | rtc check @ 20 | | YES | | | | |
4 | start | assert @ finish | | YES | | | | |
5 | start | assert @ finish | | YES | | | | |
[/code]
Lad os kigge på den problematiske VC:
[code=text]
For path(s) from start to run-time check associated with statement of line 15:
function_get_value_1.
H1: start_value < end_value .
H2: start_value >= 1 .
H3: end_value <= 2147483647 .
H4: step >= 1 .
H5: step <= 2147483647 .
H6: iteration >= 0 .
H7: iteration <= 2147483647 .
H8: integer__size >= 0 .
H9: natural__size >= 0 .
H10: positive__size >= 0 .
->
C1: start_value + iteration * step <= 2147483647 .
C2: iteration * step <= 2147483647 .
[/code]
Det potentielle overflow problem afsløres nådesløst! Der er faktisk to steder, hvor der er et potentielt problem: ved multiplikationen og ved additionen. Vi kan selvfølgelig løse problemet ved at definere prebetingelsen
[code=ada]
--# pre Iteration * Step in Integer and
--# Start_Value + Iteration * Step in Integer;
[/code]
men det er nok lidt uacceptabelt for brugeren af funktionen, da vi blot flytter bevisbyrden til brugeren.
Vi ser på vores domæne og gør hvad vi burde have gjort fra starten nemlig begrænser parameterne Step og Iteration med subtyper (vi kunne også tilføje prebetingelser, men det er som sagt dårlig stil).
[code=ada]
subtype Steps is Integer range 1 .. 1000;
subtype Iterations is Integer range 0 .. 10_000;
function Get_Value
(Start_Value : Positive;
End_Value : Positive;
Step : Steps;
Iteration : Iterations)
return Natural;
--# pre Start_Value < End_Value;
[/code]
Resultatet er:
[code=text]
For path(s) from start to run-time check associated with statement of line 15:
function_get_value_1.
H1: start_value < end_value .
H2: start_value >= 1 .
H3: end_value <= 2147483647 .
H4: step >= 1 .
H5: step <= 1000 .
H6: iteration >= 0 .
H7: iteration <= 10000 .
H8: integer__size >= 0 .
H9: positive__size >= 0 .
H10: steps__size >= 0 .
H11: iterations__size >= 0 .
->
C1: start_value + iteration * step <= 2147483647 .
[/code]
Ikke dårligt! Nu er der kun et enkelt potentielt overflow problem tilbage. Vi kan igen begrænse de resterende parametre med subtyper, men lad os for eksemplets skyld sige at de skal kunne antage samtlige positive heltalsværdier. Vi skal altså kigge lidt på funktionens krop og se hvad der kan gøres.
Løsningen er at lave et check i programkoden og i tilfælde af overflow, foretage noget fejlhåndtering. Jeg vælger blot at returnere null-værdien:
[code=ada]
function Get_Value
(Start_Value : Positive;
End_Value : Positive;
Step : Steps;
Iteration : Iterations)
return Natural
is
Result : Natural;
Val : Positive;
Increase : Natural;
begin
Increase := Iteration * Step;
if Positive'Last - Start_Value >= Increase then
Val := Start_Value + Increase;
if Val > End_Value then
Result := Null_Value;
else
Result := Val;
end if;
else
-- Error handling
Result := Null_Value;
end if;
return Result;
end Get_Value;
[/code]
Resultatet er:
[code=text]
VCs for function_get_value :
| | | -----Proved In----- | | |
# | From | To | vcg | siv | plg | prv | False | TO DO |
1 | start | rtc check @ 16 | | YES | | | | |
2 | start | rtc check @ 18 | | YES | | | | |
3 | start | rtc check @ 19 | | YES | | | | |
4 | start | rtc check @ 22 | | YES | | | | |
5 | start | rtc check @ 24 | | YES | | | | |
6 | start | rtc check @ 27 | | YES | | | | |
7 | start | assert @ finish | | YES | | | | |
8 | start | assert @ finish | | YES | | | | |
9 | start | assert @ finish | | YES | | | | |
[/code]
Sådan! Funktionen er nu beviseligt fri for run-time fejl.
Spørgsmålet er om den nu også gør det rigtige. Den nye version er lidt mere komplikeret og introducerer noget fejlhåndtering, og det kan måske være svært lige at gennemskue, om den gør det rigtige. Det problem kan man prøve at teste sig ud af, eller man kan i simple tilfælde som ovenstående bevise sig ud af. Vi skulle måske fra starten have skrevet, hvad vi egentlig forventer af funktionen, så lad os da gøre det:
[code=ada]
function Get_Value
(Start_Value : Positive;
End_Value : Positive;
Step : Steps;
Iteration : Iterations)
return Natural;
--# pre Start_Value < End_Value;
--# return R => (Start_Value + Iteration * Step <= End_Value ->
--# R = Start_Value + Iteration * Step) and
--# (Start_Value + Iteration * Step > End_Value -> R = 0);
[/code]
Altså, hvis Start_Value + Iteration * Step <= End_Value så returner Start_Value + Iteration * Step ellers returner 0. Læg mærke til at overflow tilfældet ikke er nævnt - det er en implementationsdetalje.
Resultatet er:
[code=text]
VCs for function_get_value :
| | | -----Proved In----- | | |
# | From | To | vcg | siv | plg | prv | False | TO DO |
1 | start | rtc check @ 16 | | YES | | | | |
2 | start | rtc check @ 18 | | YES | | | | |
3 | start | rtc check @ 19 | | YES | | | | |
4 | start | rtc check @ 22 | | YES | | | | |
5 | start | rtc check @ 24 | | YES | | | | |
6 | start | rtc check @ 27 | | YES | | | | |
7 | start | assert @ finish | | YES | | | | |
8 | start | assert @ finish | | YES | | | | |
9 | start | assert @ finish | | YES | | | | |
[/code]
Alle VC'ere kunne bevises inkl. postbetingelsen og funktionen er dermed bevist korrekt (hvis vi altså stoler på vores postbetingelse!).
Læg mærke til at hvis vi fjerner prebetingelsen
[code=text]
--# pre Start_Value < End_Value;
[/code]
får vi et uændret resultat.
-
0
-
0
Der er jo ikke fejl i koden som sådan, der er fejl i input til funktionen.
Alternativt kan du lave mellemberegningen i long, så kræver det endnu større inputtal for at lave overflow.
Alternativt skal du have fat i en klasse der håndterer meget store tal.
-
0
-
0
Der er jo ikke fejl i koden som sådan, der er fejl i input til funktionen.
Givet typerne af de formelle parametre, er der fejl i koden, da den ikke tager hensyn til overflow.
Alternativt kan du lave mellemberegningen i long, så kræver det endnu større inputtal for at lave overflow.
Ja det er en måde at løse problemet på i det specifikke tilfælde, men hvad hvis typerne af de formelle parametre er long (eller long long osv.)?
Det er flere måder at løse fejlen på, men det grundlæggende problem er, at fejlen ikke blev opdaget under statisk analyse (i dette tilfælde oversættelse). Jo senere en fejl opdages, jo dyrere er det at rette den. Typisk skal man regne med en faktor 10 for hvert trin i udviklingsprocessen. Husk også at en test kun afdækker et meget begrænset del at programmets tilstandsrum.
Alternativt skal du have fat i en klasse der håndterer meget store tal.
Det kan være en løsning i mange tilfælde, hvor der ikke er tale om kritisk software. Men det grundlæggende problem består: fejlen bliver måske først opdaget under test eller (endnu værre) under drift.
Ham her stoler på softwaren, når han hiver i håndtaget: http://www.youtube.com/watch?v=49VgccPwC_U
-
0
-
0
Der er jo ikke fejl i koden som sådan, der er fejl i input til funktionen
Det kan man jo ikke gøre noget ved, når det skal passe ind i et skummelt framework, som kan finde på at komme rendende med Integer.MAX_VALUE som iteration-værdi...
Alternativt kan du lave mellemberegningen i long, så kræver det endnu større inputtal for at lave overflow.
Det er også hvad jeg har gjort; faktisk kan man regne ud, at man ved at gange to positive 32-bit ints sammen + addere endnu en positiv 32-bit int ikke kan lave større tal end der kan være i en signed 64-bit long.
-
0
-
0
Nu er det mit første møde med Spark#, meeen.... Er det Anders Heilsberg, der står bag? Syntaksen smager meget af gode gamle Pascal. :-)
- Carsten
-
0
-
0
Nååh nu LMGTFY jeg lige lidt om sproget. Pascal er for Spark hvad chimpanser er for mennesker. :-)
- Carsten
-
0
-
0
Nu er det mit første møde med Spark#, meeen.... Er det Anders Heilsberg, der står bag? Syntaksen smager meget af gode gamle Pascal. :-)
SPARK er en ægte delmængde af Ada 95 med annoteringer i Ada kommentarer. Ethvert SPARK program kan således oversættes med en Ada 95 oversætter. Programmeringssproget Pascal var en stor inspirationskilde til en første Ada standard (der blev designed af Honeywell med Jean Ichbiah som chefdesigner) og derfor ligner sprogenes syntaks hinanden.
http://en.wikipedia.org/wiki/SPARK_%28programming_language%29
http://en.wikipedia.org/wiki/Ada_%28programming_language%29
-
0
-
0
Ideelt set bør defaulttypen for heltal være ubegrænsede heltal. Det er det f.eks. i Scheme og Haskell.
og Perl... ;-)
-
0
-
0
I øvrigt lidt pudsigt, synes jeg, at Java - som ellers er meget flink til at kaste exceptions hvis man f.eks. får indekseret udenfor et array, ikke giver en lyd fra sig, hvis man med almindelige aritmetiske operationer får lavet overflow.
Der er da siden Java 1.4 assert (og før det lavede man selv assert).
Derudover er der JUnit.
:-)
-
0
-
0
Tilføj kommentar
