Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2017-01-04

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #divine
02:48 Topic for #divine is now DIVINE | http://divine.fi.muni.cz | http://irclog.perlgeek.de/divine/
18:58 yaqwsx joined #divine
19:13 xstill mornfall: podle mě můžeme staticky očíslovat instrukce v každé funkci (celkem jedno jak, nemusí to být sekveční) a registry identifikovat pomocí frame pointru + toto číslo
19:13 xstill tj. transformace by to očíslovala a do trace by šli ty čísla
19:14 xstill příjde mi to skoro smysluplnější než zjišťovat lokace slotů, protože to bude komplikované a je to vlastně jedno
19:14 xstill + na konec funkce je potřeba dát něco co ty atomy zničí
19:19 xstill (zničí = označí za neporovnávací věc)
19:20 mornfall no to má zase tu stejnou nevýhodu, že když z toho frame-u uděláš load tak nepoznáš že to je symbolická hodnota
19:22 mornfall ne že by se to zrovna teď dělo, ale je to trochu nášlapná mina
19:23 xstill aha, to mi nedošlo, pak to musíš idetifikovat slotem, jenže ty se blbě počítají (musíš je počítat dynamicky)
19:24 xstill blbý je, že už jen zjistit program counter operandu nejde staticky pokud vím
19:24 xstill (operandu instrukce)
19:24 mornfall nejde protože by to musela být poslední transformace
19:24 mornfall jako obvykle
19:26 mornfall navíc teda by to vyrobilo dost velkej konflikt s případným alokátorem registrů
19:26 mornfall furt mi přijde nejrozumnější mít trace kterej bere registry a nechat eval přeložit je na haldový ukazatele a klíčovat to tím
19:27 mornfall to je aspoň uniformní ve smyslu že proměnná je jednoznačně identifikovaná svojí adresou, ať je to alloca, malloc nebo registr
19:28 xstill aha, to mě nenapadlo, že to vlastně můžu natranformovat přímo jako argumenty toho trace a ten už si s tím poradí
19:28 xstill to se mi líbí
19:39 xstill hm, až na to, že nemůžeme každou instrukci která pracuje se symbolickými hodnotami nahradit tracem, protože trace nemá žádný výsledek a my potřebujem něco co bude reprezentovat ten výsledek
19:40 xstill na void hodnutu se v llvm odkázat nedá, že?
19:45 mornfall no to by stejně nefungovalo, někdo musí kontrolovat jestli náhodou není explicitní a tak
19:46 mornfall trace se klidně může přidat před/za příslušný intrinsic call
19:46 mornfall nebo jej spíš vytvářet při nahrazování těch intrinsiců
19:47 mornfall tzn. intrinsic → call trace + call implementace
19:47 xstill no počkej, ale implementace je v podstatě jen ten trace
19:47 xstill ne?
19:47 xstill pro instrukce jiné než load/store
19:48 xstill tím pádem by vlastně mohlo stačit to co jsem říkal já, protože ty instrukce které tam zůstanou nebudou mít žádné hodnoty v registrech
19:49 xstill tj. symboliká instrukce se nahradí za trace, až teda na lifty, ty je potřeba nějak pořešit
19:50 xstill jo a problém je pokud by někde vznikla v trasformaci nebo jinak konkretizace
19:50 xstill i když, to by mohl být nějaký specielní choice
19:50 xstill choice stejně řeší kontext
19:51 mornfall no to teda nevim jak by mělo fungovat celý :)
19:51 mornfall ta symbolická hodnota musí někde bydlet, i kdyby to měl být jen jeden bajt
19:52 xstill ne, stačí ji umět identifikovat jednoznačně myslím
19:52 xstill tj. dát jí něco jako adresu
19:53 xstill ale to něco nemusí být reálně alokovaná paměť, protože do toho nikdy nikdo nebude psát ani z toho číst
19:56 xstill to je právě vtip té symbolické reprezentace, že symbolická paměť je v jistém smyslu externí a nezávislá na haldě, halda ji jen může identifikovat
20:11 mornfall tzn. že ten trace nebude tracovat konjunkty / formule ale instrukce
20:11 mornfall a někde v algoritmu bude interpret kterej z toho bude ty formule tvořit
20:12 xstill jo, protože tohle totiž už v podstatě není symbolizovaný program ve smyslu programu, který si sám počítá formuli. To je v podstatě spíš implemetace toho co dělá symdivine, jen evaluátor se stará jen o explictní hodnoty a operace se symbolickými posouvá algoritmu
20:12 mornfall něco jako IO monáda, jen z ní nejde vytahovat hodnoty jinak než že se výpočet uřízne jako infeasible
20:13 xstill vytahovat by se případně dalo pomocí __vm_choose kdyby se trochu rozšířil
20:13 mornfall plus teda magickej choice, protože bez toho to asi nejde
20:13 xstill nebo možná neví co myslíš tím vytahovat
20:14 xstill nevím, příjde mi to implementačně snažší, než si počítat formuli nebo konjukty uvnitř
20:14 mornfall symbolickou proměnnou nejde přečíst, jen s ní dělat další symbolický operace a někdy vznikne nesplnitelná path condition a uřízne se to
20:15 xstill jen to už není asi tak hezké z teoretického hlediska (není to specieltní případ abstrakcí v podstatě, jen to sdílí nějakou část infrastruktury)
20:15 mornfall no mně spíš trápí to peklo s pamětí pak
20:15 xstill číst by šlo pomocí choice asi kdyby se nám chtělo (něco jako __vm_choose( sym_id ) by vrátilo to co může být reprezentované atomem sym_id)
20:17 xstill no s pamětí problém není, load dělal něco jako - ověř že je hodnota explcitní, pokud ano pokračuj explicitní částí funkce; pokud ne, tak se udělá sym load (což je opět jen trace), případně se některé hodnoty liftnou a pokračuje se symbolizovanou verzí funkce (tj. symbolizovaná kopie basic bloků)
20:18 xstill explicitní store musí zničit symbolickou hodnotu a označit paměť jako explcitní, sym store musí označit paměť jako sym a vytracovat hodnotu
20:18 xstill ne hodnotu ale vztah
20:18 mornfall instrukci
20:18 xstill jo
20:26 mornfall ono to asi bude ale výrazně víc práce takhle
20:26 mornfall a nevim jestli to má přesvědčivý výhody
20:27 mornfall místo weak pointrů a udržování formule v implementaci domény to bude všechno v divinu
20:27 mornfall kterej si to bude muset nakonec stejně pamatovat někde ve stavu
20:31 xstill víc práce si nemyslím, protože ta část, která bude držet formuli bude podobná ať si ji drží vevnitř nebo venku, porovnání stavu bude vyžadovat zipovat odpovídající pointry v obou případech asi, a zbavím se vyčítání formule ze stavu. Na druhou stranu ztratím to, že pokud by formule byla uvnitř tak by mě DIVINE kontroloval, že ji nerozdrbu
20:32 mornfall hlavně mít to venku obnáší další interpret
20:34 xstill tam už není moc co interpretovat, jen to sypeš do formule. respektive pokud toto chápeš jako interpret tak ten byl v tom předchozím modelu uvnitř DIVINE
20:36 xstill ta abstrakce tam v podstatě pořád je, jen se implementace domény přesunula ven z programu
20:48 xstill mě to právě přijde implementačně zvládnutelnější
21:15 mornfall co takhle: symbolické hodnoty jsou ukazatele (s flagy weak, abstract), při zipování stavů se (abstract) pointry přeloží na srovnávací část formule... hodnoty samotné jsou reprezentované jako graf (a + 1) * (b + 2), kde a, b jsou volné (anonymní) proměnné... formule se nikam neukládá, je součástí haldy, verzování není potřeba, protože 'live' množina je prostě výčet všech míst
21:15 mornfall v paměti který drží (abstract) ukazatel
21:17 mornfall prostě bona fide symbolický výpočet
21:27 mornfall (abstraktní hodnoty který se musí vejít do bajtu by tak teoreticky snad mohla vyřešit podpora ve VM pro fragmentovaný normální ukazatele)
21:44 mornfall divine 4 už dneska nebude... tak snad zítra
21:52 yaqwsx joined #divine

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary