Любопытная заметка от 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
#solver #analysis
Речь идет об оптимальной расстановке команды 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
#solver #analysis
Автоматическое извлечение КС-грамматики на основе динамического анализа управляющего графа программы на примерах входных данных. Любопытно, что авторы не стали даже упоминать грамматическое сжатие.
Mining Input Grammars from Dynamic Control Flow
https://publications.cispa.saarland/3101/1/fse2020-mimid.pdf
#analysis #parsing
Mining Input Grammars from Dynamic Control Flow
https://publications.cispa.saarland/3101/1/fse2020-mimid.pdf
#analysis #parsing
Авторы оценивают верхнюю и нижнюю границы вычислительной сложности статического анализа указателей Андерсена (APA) и приводят свои варианты реализации APA.
The Fine-Grained Complexity of Andersen’s Pointer Analysis
https://arxiv.org/pdf/2006.01491.pdf
#analysis
The Fine-Grained Complexity of Andersen’s Pointer Analysis
https://arxiv.org/pdf/2006.01491.pdf
#analysis
Unsupervised Translation of Programming Languages
Довольно любопытная статья на тему создания транскомпилятора от исследователей из Facebook AI Research.
Путем тренировки модели, на корпусе программ из Github, транслируют код языков C++, Java, Python.
Авторы показывают, что их модель превосходит работы в данной области, основанные на подходе
использования правил. Из интересного, прямой цитатой из статьи:
Paper:
https://arxiv.org/pdf/2006.03511
Video:
https://www.youtube.com/watch?v=xTzFJIknh7E&app=desktop
#ml #analysis #transpilation
Довольно любопытная статья на тему создания транскомпилятора от исследователей из 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
#ml #analysis #transpilation
YouTube
TransCoder: Unsupervised Translation of Programming Languages (Paper Explained)
Code migration between languages is an expensive and laborious task. To translate from one language to the other, one needs to be an expert at both. Current automatic tools often produce illegible and complicated code. This paper applies unsupervised neural…
Подход к выявлению "семантического клонов" в программе. Основан на насыщении равенствами и забытой концепции Programmer’s Apprentice. Утверждается, что работает лучше, чем популярное в этой области представление PDG.
Semantic Code Search via Equational Reasoning
https://dl.acm.org/doi/pdf/10.1145/3385412.3386001
#analysis
Semantic Code Search via Equational Reasoning
https://dl.acm.org/doi/pdf/10.1145/3385412.3386001
#analysis
Два небольших доклада об инструментах статического анализа, основанных на Datalog.
DOOP
https://www.youtube.com/watch?v=FQRLB2xJC50
Soufflé
https://www.youtube.com/watch?v=Qp3zfM-JSx8
#analysis #datalog
DOOP
https://www.youtube.com/watch?v=FQRLB2xJC50
Soufflé
https://www.youtube.com/watch?v=Qp3zfM-JSx8
#analysis #datalog
Formulog -- выразительный DSL для задач статического анализа.
Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT
http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
#analysis #datalog #smt
Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT
http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
#analysis #datalog #smt
Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.
Refinement Types: A Tutorial
https://arxiv.org/abs/2010.07763
https://github.com/ranjitjhala/sprite-lang
#analysis #smt
Refinement Types: A Tutorial
https://arxiv.org/abs/2010.07763
https://github.com/ranjitjhala/sprite-lang
#analysis #smt
Очередное подтверждение тому факту, что работа над компиляторами -- это не только известные проекты-бегемоты в духе 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. Вообще, в области обработки сетевых пакетов компиляторные технологии в целом развиваются очень интересным образом, существуют работающие подходы из области синтеза программ и я к этой теме еще обязательно вернусь.
#jit #analysis #vm #verification #bpf
Вы слышали о 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. Вообще, в области обработки сетевых пакетов компиляторные технологии в целом развиваются очень интересным образом, существуют работающие подходы из области синтеза программ и я к этой теме еще обязательно вернусь.
#jit #analysis #vm #verification #bpf
Очередная работа от 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 и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
#smt #analysis #synthesis
Dataflow-based Pruning for Speeding up Superoptimization
https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf
Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы -- иначе SMT-решателю справиться будет тяжело.
Ключевая идея авторов -- прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
#smt #analysis #synthesis
Тем не менее несколько моментов вызывают вопросы, если не к подходу в целом, то к его реализации в JastAdd.
Во-первых, как упоминалось ранее, отношения (Relations) задаются "внешним" по отношению к дереву образом, и авторы для этого используют обычный императивный код на Java, да ещё и опирающийся на неявные, генерируемые фреймворком методы. Мне такой способ не кажется декларативным и особо высокоуровневым.
Во-вторых, несмотря на то, что дерево разбора превращается в направленный граф общего вида, возможность реализации Control Flow Analysis и Data Flow Analysis остаётся под вопросом. Возможно, этому мешают ограничения на неизменяемость графа, связанные с мемоизацией (в свою очередь, необходимой для эффективной работы алгоритмов). В частности, это накладывает ограничения на построение отношений между "обычными" и узлами в NTA.
В любом случае, для прояснения деталей предлагаемого подхода читателю предлагается ознакомиться со статьёй, благо, она достаточно проста для понимания. Механизм Relational RAGs весьма мощный и универсальный – его полезно иметь в виду при реализации самых разных аспектов работы с языками программирования, не только статического анализа. 😊
#dsl #rag #static #analysis
Во-первых, как упоминалось ранее, отношения (Relations) задаются "внешним" по отношению к дереву образом, и авторы для этого используют обычный императивный код на Java, да ещё и опирающийся на неявные, генерируемые фреймворком методы. Мне такой способ не кажется декларативным и особо высокоуровневым.
Во-вторых, несмотря на то, что дерево разбора превращается в направленный граф общего вида, возможность реализации Control Flow Analysis и Data Flow Analysis остаётся под вопросом. Возможно, этому мешают ограничения на неизменяемость графа, связанные с мемоизацией (в свою очередь, необходимой для эффективной работы алгоритмов). В частности, это накладывает ограничения на построение отношений между "обычными" и узлами в NTA.
В любом случае, для прояснения деталей предлагаемого подхода читателю предлагается ознакомиться со статьёй, благо, она достаточно проста для понимания. Механизм Relational RAGs весьма мощный и универсальный – его полезно иметь в виду при реализации самых разных аспектов работы с языками программирования, не только статического анализа. 😊
#dsl #rag #static #analysis
👍11
Я и мой студент, Кирилл Павлов, опубликовали статью "Библиотека llvm2py для анализа промежуточного представления LLVM и её применение в оценке степени распараллеливания линейных участков кода".
Чем может быть интересна работа студента второго курса бакалавриата? Анализ распараллеливания делается для варианта LLVM IR, где линейные участки заданы ярусно-параллельной формой (ЯПФ). Автоматическое построение ЯПФ позволяет узнать минимальное число шагов, за которое неограниченно параллельный LLVM-процессор может выполнить код линейного участка.
В реальных процессорах число параллельно работающих вычислительных элементов конечно. Поэтому важно экономить ресурсы: получить минимальную ширину ЯПФ, при которой достигается минимальное число шагов параллельной LLVM-машины. Так можно предварительно оценить выбор того или иного аппаратного ускорителя или же узнать, какой "шириной" должен обладать проектируемый нами ускоритель. В статье эта задача сводится к задаче программирования в ограничениях и эффективно решается с помощью инструментария Google OR-Tools.
P.S. Сама библиотека llvm2py, предназначенная для создания такого рода статических анализаторов кода LLVM IR, была полностью реализована Кириллом.
#llvm #analysis #solver
Чем может быть интересна работа студента второго курса бакалавриата? Анализ распараллеливания делается для варианта LLVM IR, где линейные участки заданы ярусно-параллельной формой (ЯПФ). Автоматическое построение ЯПФ позволяет узнать минимальное число шагов, за которое неограниченно параллельный LLVM-процессор может выполнить код линейного участка.
В реальных процессорах число параллельно работающих вычислительных элементов конечно. Поэтому важно экономить ресурсы: получить минимальную ширину ЯПФ, при которой достигается минимальное число шагов параллельной LLVM-машины. Так можно предварительно оценить выбор того или иного аппаратного ускорителя или же узнать, какой "шириной" должен обладать проектируемый нами ускоритель. В статье эта задача сводится к задаче программирования в ограничениях и эффективно решается с помощью инструментария Google OR-Tools.
P.S. Сама библиотека llvm2py, предназначенная для создания такого рода статических анализаторов кода LLVM IR, была полностью реализована Кириллом.
#llvm #analysis #solver
👍56