[P4] ?==?utf-8?q? ?==?utf-8?q? Hibajavítások

[Lukács Dániel]

Sziasztok,
Dolgoztam ma a C kód és a K összehangolásán. Néhány probléma kiküszöbölése után sikerült lefordítanom az oopsla16 és a runtime verificiation (RV) verzióval is. Az RV futtatni is tudja (viszont ebben nincsenek bizonyítások), az oopsla16-on még dolgozom (printf, memcpy stb... nincs támogatva).

Leginkább olyasmik miatt panaszkodott a fordító, amikre léteznek gcc warningok is, de volt amit csak az RV-vel találtam meg, mert az oopsla csak egy NullPointerException-t dobott.
Ha eljutok a specifikáció írás kezdetéig, írok majd egy összefoglalót a panaszokról, és kommitolom a panaszokhoz tartozó változtatásokat is.

Marci szerintem jó lett a függetlenített C kód: könnyen átlátható, lehet vele dolgozni, a main függvény is sokat segített.

A 250000 karakteres sorból a fordítás és futtatás során nem volt gond. Az oopsla-val a fordítás: 90s, futtatás: 15s (a hello world is ilyesmi). Az RV még gyorsabb. Lehet, hogy ügyesen optimalizál a szemantika, de ezt jobb talán csak akkor kimondani, ha már a bizonyítás is fut :)

Üdv,
Dániel



On Wednesday, January 3, 2018 23:55 CET, Brunner Márton <brmarci at caesar.elte.hu> wrote:
  
Sziasztok!
A mai hibákkal/hiányosságokkal kapcsolatos előrehaladások:
 * 
Konstanssal nem lehet módosítani 32 bitnél nagyobb mezőt: kijavítva. Bár szokásos módon nem teszteltem agyon, de látszólag jól működik. * 
A verifikációhoz használandó C kódban a GET_INT32_AUTO_PACKET makró nem jól működik: nem a példa kód volt a hibás, hanem tényleg a makró nem működött jól. Ha olyan mező értékét kérdeztük le vele, ami nem metadata és nem hosszabb mint 16 bit, bájtkonverzió nélkül, akkor nullát kaptunk eredményül. (Mintha Sanyi korábban jelezte is volna, hogy találtak valami ilyesmi hibát a makrók működésében.) Remélem, hogy sikerült most úgy kijavítanom, hogy a javítás nem vezet be újabb hibát. Fun fact: ez a kód másfél éve hibás.
Ezen kívül a C-s verifikációhoz kapcsolódóan van egy aggasztó megfigyelésem. Nem tudom, hogy jutottatok-e már bármire a modify_field C-s verifikációjával, de én ma kíváncsiságból megnéztem, hogy mit kapunk a preprocesszálás után. A MODIFY_INT32_INT32_AUTO_PACKET makró feloldása után egy 250 000 karakteres sort kapunk. (Az optimalizáció után ebből valójában csak egy értékadás marad.) Nem tudom, hogy a C K-s szemantikája milyen formában várja a kódot, de valószínűleg ebben a formában nem örülne neki túlságosan.
Marci


 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://plc.inf.elte.hu/pipermail/p4/attachments/20180104/16d1516d/attachment.html>