02/11/2020, Peter Sovietov¶
Очередная работа от John Regehr со товарищи на тему супероптимизации.
Dataflow-based Pruning for Speeding up Superoptimization https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf
Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы – иначе SMT-решателю справиться будет тяжело.
Ключевая идея авторов – прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
21/10/2020, Peter Sovietov¶
Очередное подтверждение тому факту, что работа над компиляторами – это не только известные проекты-бегемоты в духе LLVM/GCC для 2-3 популярных архитектур и виртуальных машин.
Вы слышали о BPF? Впрочем, что я говорю, если читаете внимательно PLComp, то, конечно, слышали. Но, в любом случае, есть замечательная заметка, которая вводит в предмет:
BPF, XDP, Packet Filters and UDP https://fly.io/blog/bpf-xdp-packet-filters-and-udp/
Посмотрите, сколько всего интересного! Узкая предметная область, виртуальные машины, JIT-компиляция, статический анализ кода, верификация.
В заметке есть ссылка на хорошую статью 1999 года:
BPF+: Exploiting Global Data-flow Optimization in a Generalized Packet Filter Architecture https://andrewbegel.com/papers/bpf.pdf
Ничего себе, да? Такие-то технологии для, вроде бы, заурядной задачи фильтрации пакетов!
И вот кульминация, статья уже совсем свежая:
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel https://unsat.cs.washington.edu/papers/nelson-jitterbug.pdf
Складывается ощущение, что BPF – своеобразный полигон для обкатки перспективных технологий компиляции. Это объяснимо: на исходный язык и вычисления накладываются жесткие ограничения, сама виртуальная машина простая – есть где развернуться и применить что-нибудь изощренное. И, разумеется, интересны перспективы использования BPF в специализированных аппаратных решениях.
P.S. Вообще, в области обработки сетевых пакетов компиляторные технологии в целом развиваются очень интересным образом, существуют работающие подходы из области синтеза программ и я к этой теме еще обязательно вернусь.
#bpf #analysis #verification #jit #vm
16/10/2020, Peter Sovietov¶
Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.
Refinement Types: A Tutorial https://arxiv.org/abs/2010.07763 https://github.com/ranjitjhala/sprite-lang
08/08/2020, Peter Sovietov¶
Formulog – выразительный DSL для задач статического анализа. Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
23/06/2020, Peter Sovietov¶
Два небольших доклада об инструментах статического анализа, основанных на Datalog.
DOOP https://www.youtube.com/watch?v=FQRLB2xJC50
Soufflé https://www.youtube.com/watch?v=Qp3zfM-JSx8
15/06/2020, Peter Sovietov¶
Подход к выявлению “семантического клонов” в программе. Основан на насыщении равенствами и забытой концепции Programmer’s Apprentice. Утверждается, что работает лучше, чем популярное в этой области представление PDG.
Semantic Code Search via Equational Reasoning https://dl.acm.org/doi/pdf/10.1145/3385412.3386001
10/06/2020, alekum¶
Unsupervised Translation of Programming Languages Довольно любопытная статья на тему создания транскомпилятора от исследователей из Facebook AI Research. Путем тренировки модели, на корпусе программ из Github, транслируют код языков C++, Java, Python.
Авторы показывают, что их модель превосходит работы в данной области, основанные на подходе использования правил. Из интересного, прямой цитатой из статьи:
• We introduce a new approach to translate functions from a programming language to another, that is purely based on monolingual source code. • We show that TransCoder successfully manages to grasp complex patterns specific to each language, and to translate them to other languages. • We show that a fully unsupervised method can outperform commercial systems that leverage rule-based methods and advanced programming knowledge. • We build and release a validation and a test set composed of 852 parallel functions in 3 languages, along with unit tests to evaluate the correctness of generated translations. • We will make our code and pretrained models publicly available.
В видео можно послушать комментарии.
Paper: https://arxiv.org/pdf/2006.03511
Video: https://www.youtube.com/watch?v=xTzFJIknh7E&app=desktop
10/06/2020, Peter Sovietov¶
Авторы оценивают верхнюю и нижнюю границы вычислительной сложности статического анализа указателей Андерсена (APA) и приводят свои варианты реализации APA.
The Fine-Grained Complexity of Andersen’s Pointer Analysis https://arxiv.org/pdf/2006.01491.pdf
10/06/2020, Peter Sovietov¶
Автоматическое извлечение КС-грамматики на основе динамического анализа управляющего графа программы на примерах входных данных. Любопытно, что авторы не стали даже упоминать грамматическое сжатие.
Mining Input Grammars from Dynamic Control Flow https://publications.cispa.saarland/3101/1/fse2020-mimid.pdf
07/06/2020, Peter Sovietov¶
Любопытная заметка от Intel на тему использования внешнего решателя задач целочисленного программирования в LLVM. Речь идет об оптимальной расстановке команды LFENCE в управляющем графе. Это нужно для предотвращения LVI-атак.
An Optimized Mitigation Approach for Load Value Injection https://software.intel.com/security-software-guidance/insights/optimized-mitigation-approach-load-value-injection
ILP-решатель для автоматической вставки fence применяли и ранее. См., например, работу Don’t sit on the fence. A static analysis approach to automatic fence insertion: https://arxiv.org/pdf/1312.1411.pdf
28/05/2020, Peter Sovietov¶
SSA в историческом контексте. Очень хорошая систематизация знаний по теме. Program Analisys and Transformation Survey and Links https://github.com/pfalcon/awesome-program-analysis
22/05/2020¶
Возможно, вы уже слышали новость о древнем GW-BASIC. Компания Microsoft выложила исходники интерпретатора на github: https://devblogs.microsoft.com/commandline/microsoft-open-sources-gw-basic/
В заметке по ссылке есть одна интригующая фраза: “Microsoft was able to generate a substantial amount of the code for a port from the sources of a master implementation. (Alas, sorry, we’re unable to open-source the ISA translator.)”. И действительно, текст на языке ассемблера для 8088 был получен автоматически с помощью специального транслятора. При этом даже комментарии в коде остались нетронутыми, там речь идет, судя по всему, о 8080.
В статье из журнала Byte за 1982 год сравниваются возможности трех трансляторов, которые автоматически преобразуют код 8-битных процессоров 8080/Z80 для CP/M в 16-битный код 8088/8086 для MS-DOS: https://tech-insider.org/personal-computers/research/acrobat/8206-b.pdf
Особенно выделяется среди этих трансляторов XLT86 (8080 -> 8086) от компании Digital Research. Этот транслятор — детище Гэри Килдалла, о котором специально говорить, наверное, нет необходимости. В области построения компиляторов Килдалл известен своей работой A unified approach to global program optimization (1973): https://dl.acm.org/doi/pdf/10.1145/512927.512945
Статья Килдалла до сих пор находится в числе самых цитируемых по компиляторной тематике и речь идет об алгоритме анализа потока данных, который позже был описан во множестве учебников и применяется в самых современных компиляторах: http://compcert.inria.fr/doc-1.6/html/Kildall.html
Вернемся, однако, к XLT86. К счастью, сохранилась документация к транслятору: http://www.s100computers.com/Software%20Folder/Assembler%20Collection/Digital%20Research%20XLT86%20Manual.pdf
Из нее можно узнать, в частности, что:
- Трансляция состоит из 5 фаз.
- В начале определяются линейные участки и строится граф потока управления. Затем проводится глобальный анализ потока данных для определения “живых” регистров и флагов процессора.
- Сам процесс “выбора команд” элегантно описан табличным образом. Некоторые правила преобразований являются условными и зависят от ранее полученных результатов анализа потока данных.
- Транслятор написан на ЯП PL/I-80 и имеет ограничение на размер входной программы — не более 6 Kбайт.
12/05/2020¶
Program Analysis Свежий (весна 2020) курс по анализу программ, с неплохим выбором тем. https://cmu-program-analysis.github.io/