LLVM nyt

Slides fra LLVM's developer meeting er nu online.

Læg særligt mærke til "Softbound" projektet: Endelig nogen der opfatter compileren som et værktøj.

De fleste programmører opfatter en compiler som en uforanderlig og ofte uhjælpsom klods.

Tænk hvis man kunne sige til sin compiler: "lav lige noget kode til at holde lige ekstra øje med den pointer der hedder *p i foobar() funktionen, den ma aldrig blive NULL eller invalid." istedet for at plastre kildeteksten til med asserts()...

Softbound er bestemt på vej i den rigtige retning.

phk

Kommentarer (20)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Erik Cederstrand

Slides fra LLVM's developer meeting er nu online.

På grund af en eller anden hjerneblødning hos Apple PR måtte slides lavet af Apple-ansatte i første omgang ikke offentliggøres. Rimelig usmart når 80% af LLVM-udviklerne sidder hos Apple, og LLVM skulle forestille at være open source. Så det er glædeligt, at de har ombestemt sig.

  • 0
  • 0
Lars Lundin

Jeg har noget kode, der eksponerer en bug i llvm, llvms fejl-besked sender mig til http://developer.apple.com/bugreporter med besked om at oprette en bug report der. Men hos Apples bugreporter skal man have et login, som jeg ikke lige kan se hvordan jeg får.

Er der nogen der har en nemmere metode til at oprette en llvm bug-report?

PS.
stderr fra llvm ser sådan ud:
Terminate called after throwing an instance of 'std::bad_alloc'
what(): std::bad_alloc
*** glibc detected *** /usr/lib/llvm/gcc-4.2/libexec/gcc/i486-linux-gnu/4.2.1/cc1: free(): invalid pointer: 0x089122fe ***
llvm-gcc: Internal error: Aborted (program cc1)
Please submit a full bug report.
See <URL:http://developer.apple.com/bugreporter&gt; for instructions.

  • 0
  • 0
Baldur Norddahl

Øv, jeg læste forkert og troede det handlede om statisk check.

Jeg har længe drømt om en "assert/ensure" lignende konstruktion, men som oversætteren kan verificere ved oversættelsestidspunktet.

Så i stedet for at sige "hold lige øje med at pointeren aldrig bliver NULL", så siger man "giv fejl ved oversættelsen, hvis det ikke kan bevises, at pointeren aldrig kan blive NULL".

Dermed kan man få et program som man er sikker på virker, i stedet for et program hvor man blot er sikker på at det afsluttes ved fejl.

  • 0
  • 0
Nikolaj Brinch Jørgensen

Så i stedet for at sige "hold lige øje med at pointeren aldrig bliver NULL", så siger man "giv fejl ved oversættelsen, hvis det ikke kan bevises, at pointeren aldrig kan blive NULL".

Dermed kan man få et program som man er sikker på virker, i stedet for et program hvor man blot er sikker på at det afsluttes ved fejl.

Det giver da ikke sikkerhed for at programmet virker?

  • 0
  • 0
Poul-Henning Kamp Blogger

Det er meget sødt at ville bevise programmers korrekthed og jeg skal være den første til at tage hatten af for Søren Lausen og Brinch-Hansens RC4000 monitor på det punkt.

Men i praksis virker det ikke, fordi programmer tygger sig igennem data og hvad der sker i programmer afhænger ofte af data.

Der er også det problem, at man har ringe glæde af at bevise a et program er korrekt, hvis det er linket imod biblioteker der ikke er.

Derfor foretrækker jeg at mine programmer er robuste og fylder dem rask væk med asserts() der skal fortælle mig hvis der sker noget uventet.

Når en assert fyrer, ville det være rart hvis compileren kunne give en hånd med at finde ud af hvorfor, når den nu alligevel har fat i koden.

Poul-Henning

  • 0
  • 0
Erik Cederstrand

Men i praksis virker det ikke, fordi programmer tygger sig igennem data og hvad der sker i programmer afhænger ofte af data. Der er også det problem, at man har ringe glæde af at bevise a et program er korrekt, hvis det er linket imod biblioteker der ikke er.

Vi er enige om, at vi nok aldrig når til komplet bevisførelse for komplekse programmer, men som et supplement til statisk analyse, unit tests, stress tests, assert()s osv. synes jeg det har sin plads.

Eksemplet på side 3 i http://llvm.org/pubs/2008-12-OSDI-KLEE.pdf virker i hvert fald ret overbevisende:

When KLEE runs on tr, it finds a buffer overflow error at line 18 in Figure 1 and then produces a concrete test case (tr [ "" "") that hits it.

  • 0
  • 0
Anonym

Men i praksis virker det ikke, fordi programmer tygger sig igennem data og hvad der sker i programmer afhænger ofte af data.

Jeg synes nu at bevisførelse er utroligt nyttigt, når jeg skriver programmer. Beviser for fravær af aritmetisk overflow og buffer overflow eliminerer rigtig mange potentielle fejl og beviser for at pre-betingelser er opfyldte gør, at jeg ikke behøver at lave defensiv kode, der kun svært kan dækkes under test.

Derfor foretrækker jeg at mine programmer er robuste og fylder dem rask væk med asserts() der skal fortælle mig hvis der sker noget uventet.

Jeg foretrækker at robustheden opnås ved statisk analyse.

Når en assert fyrer, ville det være rart hvis compileren kunne give en hånd med at finde ud af hvorfor, når den nu alligevel har fat i koden.

En fyret assert er lig med en inkonsistent programtilstand, hvilket igen kan være lig med kolliderende fly, fejlsignalering af tog, farlige maskiner, der ikke bringes til standsning og andre situationer, der kan medføre tab af menneskeliv.

Jeg tror man skal vænne sig lidt til tanken om bevisførelse, men når først man har fået smag for det, så er det faktisk frustrerende, når man skal leve uden.

  • 0
  • 0
Simon Shine

En fyret assert er lig med en inkonsistent programtilstand, hvilket igen kan være lig med kolliderende fly, fejlsignalering af tog, farlige maskiner, der ikke bringes til standsning og andre situationer, der kan medføre tab af menneskeliv.

Vi lever i et kaotisk rum hvor der kan gå flere ting galt end vi kan tage forbehold for. Når et program anvendes i en missionskritisk situation betyder det at nogen har fæstet tillid til forfatterne selvom de ikke fuldt ud forstår programmet. Den tillid kan være svær at kvantificere på trods af at forfatterne kan argumentere for at garantier fra statisk analyse er bedre end ved køretid.

Det eneste en udenforstående kan gøre er at spørge en hel masse programmer og vælge det mest populære eller prioritere kilder som er mindst kontroversielle.

Jeg tror man skal vænne sig lidt til tanken om bevisførelse, men når først man har fået smag for det, så er det faktisk frustrerende, når man skal leve uden.

Jeg tror også at man vænner sig til det, men det er i sig selv kun en fordel for folk som er vant til det. :-P

  • 0
  • 0
Poul-Henning Kamp Blogger

Jeg tror man skal vænne sig lidt til tanken om bevisførelse, men når først man har fået smag for det, så er det faktisk frustrerende, når man skal leve uden.

Jeg siger ikke at beviser er uden værdi, men at de ikke er nok. Jeg bruger selv statisk analyse af forskellig observans når jeg kan komme til det.

Men asserts er en anden klasse, for de lever op til "end-to-end" princippet: De tester min antagelse imod den virkelige situation og fanger compilerfejl, datafejl og upalidelig hardware.

Det kan beviser aldrig gøre for mig.

Poul-Henning

  • 0
  • 0
Torben Mogensen Blogger

Men asserts er en anden klasse, for de lever op til "end-to-end" princippet: De tester min antagelse imod den virkelige situation og fanger compilerfejl, datafejl og upalidelig hardware.

Det kan beviser aldrig gøre for mig.

Det kan asserts vel heller ikke. Compileren kan oversætte dine asserts forkert, og datafejl og upålidelig hardware kan få dine asserts til at regne galt.

Men du har helt ret i, at statisk check ikke kan garantere, at inddata er uden fejl. Men her kan man lave en test/assertion på datakonsistens og sidenhen bruge denne test til statisk at vise, at data efterfølgende er konsistent. Med andre ord bruger man assertions, nar man får data fra en ikke-verificeret kilde, men efter data har passeret dette filter, behøver man ikke længere at teste det igen, og selv ved ændringer, kan invarianter sikres alene ved statisk verifikation.

Hvis hardwaren er upålidelig, er asserts ikke nok. Så skal man bruge en oversætter, der genererer redundant kode, så man opdager enhver afvigelse fra forventet opførsel. Lidt ligesom fejlkorrigerende koder.

  • 0
  • 0
Poul-Henning Kamp Blogger

Jeg elsker disse svar fra akademikere: korrekt i alle detaljer og stadig fuldstændigt ubrugeligt i praksis :-)

Eller som Holberg ville have skrevet: Et er algoritme at bevise, et andet computer at føre...

Asserts fanger flere hw-fejl en du tror, hvis du bruger dem fornuftigt.

Poul-Henning

  • 0
  • 0
Baldur Norddahl

Asserts fanger flere hw-fejl en du tror, hvis du bruger dem fornuftigt.

Men hvis du kombinerer det med statisk analyse, og du får en assert som oversætteren har bevist er umulig, så ved du med sikkerhed at det enten er en hardwarefejl eller fejl i oversætteren. Det må også have en værdi at kunne udelukke fejl i dit eget program.

  • 0
  • 0
Log ind eller Opret konto for at kommentere