<div dir="ltr"><div>Thanks! The SyGuS is fresh to me. I'll check them out. <br></div><div><br></div><div>I searched Rosette and got lots of food results, and I hope this rosette[1] is the right one:</div><div>[1] <a href="https://github.com/emina/rosette">https://github.com/emina/rosette</a></div><div><br></div><div>Please correct me if I looked at the wrong repo.<br></div><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 17, 2021 at 6:29 PM Nuno Lopes <<a href="mailto:nunoplopes@sapo.pt">nunoplopes@sapo.pt</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;" lang="EN-US"><div class="gmail-m_6214696881666759473WordSection1"><p class="MsoNormal">STOKE & Souper are the most well supported & maintained superoptimization tools out there. They are very different: STOKE does genetic search, while Souper uses only SMT solvers for (symbolic) search.<u></u><u></u></p><p class="MsoNormal">There<span style="font-family:"Times New Roman",serif">’</span>s also Rosette, which does a hybrid of concrete & symbolic search (mixing concrete search with other techniques seems to be the way to go).<u></u><u></u></p><p class="MsoNormal"><u></u> <u></u></p><p class="MsoNormal">I would also look at the SyGuS competition (syntax-guided synthesis). These tools, such as CVC4, can be used for superoptimization as well.<u></u><u></u></p><p class="MsoNormal"><u></u> <u></u></p><p class="MsoNormal">In terms of tools, I think that<span style="font-family:"Times New Roman",serif">’</span>s it. In terms of papers, there are plenty of research groups working on synthesis in general.<u></u><u></u></p><p class="MsoNormal"><u></u> <u></u></p><p class="MsoNormal">Nuno<u></u><u></u></p><p class="MsoNormal"><u></u> <u></u></p><p class="MsoNormal"><u></u> <u></u></p><div style="border-color:rgb(225,225,225) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm"><p class="MsoNormal"><b>From:</b> Wei Wu<u></u><u></u></p><p class="MsoNormal"><b>Sent:</b> 17 February 2021 09:54<br><b>To:</b> llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>><br><b>Subject:</b> [llvm-dev] Fwd: Superoptimization for RISC-V: What is the state of the art now?<u></u><u></u></p></div><p class="MsoNormal"><u></u> <u></u></p><div><div><p class="MsoNormal">Hi all,<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">I appreciate it if you can drop some information/papers/open source project urls that are related to superoptimization. Although I am targeting RISC-V ISA, there might be some other research works / open source projects available in the LLVM community.<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">(Sorry for the duplicate email.)<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p><div><div><p class="MsoNormal">---------- Forwarded message ---------<br>From: <b>Wei Wu (</b><b><span style="font-family:"MS Gothic"">吴</span></b><b><span style="font-family:"Microsoft JhengHei",sans-serif">伟</span>)</b> <<a href="mailto:lazyparser@gmail.com" target="_blank">lazyparser@gmail.com</a>><br>Date: Wed, Feb 17, 2021 at 12:26 PM<br>Subject: Superoptimization for RISC-V: What is the state of the art now?<br>To: RISC-V SW Dev <<a href="mailto:sw-dev@groups.riscv.org" target="_blank">sw-dev@groups.riscv.org</a>><u></u><u></u></p></div><p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p><div><p class="MsoNormal">Hi all,<u></u><u></u></p><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">In the last code optimization meeting (formly code-size-reduction and code-speed-opt), the idea of using superoptimization[4] for RISC-V had been discussed. I'm interested in this area. After a quick search I found very few results, though. GNU/Embecosm had a superopt [1] but I am not sure it still works either for GCC 10 or RISC-V backend. Google open sourced a LLVM-IR level tool named souper[2] would help. STOKE[3] is yet another optimizer which targets x86 only.<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">I appreciate it if you can drop some information/papers/open source project urls that are related to superoptimization. I am going to stand on the basis of gnu-superopt[1], and not sure it is the right/effective way to go.<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">Thanks.<u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">[1] <a href="https://github.com/embecosm/gnu-superopt" target="_blank">https://github.com/embecosm/gnu-superopt</a><u></u><u></u></p></div><div><p class="MsoNormal">[2] <a href="https://github.com/google/souper" target="_blank">https://github.com/google/souper</a><u></u><u></u></p></div><div><p class="MsoNormal">[3] <a href="https://github.com/StanfordPL/stoke" target="_blank">https://github.com/StanfordPL/stoke</a><u></u><u></u></p></div><div><p class="MsoNormal">[4] <a href="https://en.wikipedia.org/wiki/Superoptimization" target="_blank">https://en.wikipedia.org/wiki/Superoptimization</a><u></u><u></u></p></div><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal">-- <u></u><u></u></p></div><div><p class="MsoNormal">Best wishes,<br>Wei Wu (<span style="font-family:"MS Gothic"">吴</span><span style="font-family:"Microsoft JhengHei",sans-serif">伟</span>)<u></u><u></u></p></div></div></div></div></div></div></div></blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature">Best wishes,<br>Wei Wu (吴伟)<br></div>