
<html>Sziasztok,<br />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).<br /><br />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.<br />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.<br /><br />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.<br /><br />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 :)<br /><br />Üdv,<br />Dániel<br /><br /><br /><br />On Wednesday, January 3, 2018 23:55 CET, Brunner Márton <brmarci@caesar.elte.hu> wrote:<br /> <blockquote type="cite" cite="eec4cce1-fd73-dd85-4e7f-ec7775b8149a@caesar.elte.hu"> </blockquote><meta http-equiv="content-type" content="text/html; charset=utf-8"><p>Sziasztok!</p><p>A mai hibákkal/hiányosságokkal kapcsolatos előrehaladások:</p><ul><li><p>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.</p></li><li><p>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>bájtkonverzió nélkül</b>, 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.</p></li></ul><p>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 <b>MODIFY_INT32_INT32_AUTO_PACKET</b> 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.</p><p>Marci</p><br /><br /><br /> </html>