Генерация слабейших предусловий программ с динамической памятью в символьном исполнении
Аннотация:
Предмет исследования. Символьное исполнение — широко известный метод систематического исследования путей исполнения программ. Метод позволяет решить ряд важных задач, связанных с контролем корректности: поиск ошибок и уязвимостей, автоматическая генерация тестов и др. Основная идея символьного исполнения — порождение и использование символьных логических выражений при анализе программ в прямом порядке, т. е. от входной точки к точкам интереса. Хорошо известен метод обратного символьного исполнения, когда условия попадания в точку интереса распространяются ко входной точке программы за счет итеративного вычисления слабейших предусловий. Реализовать этот метод, как правило, намного труднее, чем прямое символьное исполнение, так что даже артефакты последнего не удается использовать при реализации. Метод. Исследована связь между прямым и обратным символьными исполнениями на основе вычисления слабейших предусловий. В частности показано, как обратное исполнение может быть реализовано на базе прямого. Основные результаты. Приведено формальное описание процедуры символьного исполнения с ленивой инициализацией для программ с динамической памятью. Предложен алгоритм вычисления слабейших предусловий для произвольных ветвей исполнения программы. Механизм ленивой инициализации и алгоритм вычисления слабейших предусловий реализованы в символьной виртуальной машине KLEE, работающей на базе широко известной платформы LLVM. Практическая значимость. Представленный метод позволяет выполнять обратный символьный анализ при помощи прямого символьного исполнения. Это важно для реализации двунаправленного исполнения программ, которое может быть применено для верификации программ и автоматического порождения тестовых покрытий.
Ключевые слова:
Постоянный URL
Статьи в номере
- Влияние размерности, геометрии и ориентации наноструктур на распределение электрического поля в вопросах усиления комбинационного рассеяния света
- Оптические свойства планарных плазмон-активных поверхностей, модифицированных золотыми нанозвездами
- Применение методов биорадиофотоники для обработки биоэлектрических сигналов
- Автоматическое распознавание структур в полупрозрачных движущихся объектах на основе голографической муаровой интерферометрии
- Применение технологий нейронных сетей и компьютерного зрения для анализа изображений кожных новообразований
- Применение метода цифровой голографической интерферометрии для исследования низкотемпературной импульсной плазмы
- Полихромный источник света для реализации многоспектрального метода обработки изображений кожных новообразований
- Уменьшение влияния амплитудных искажений LiNbO3 фазового модулятора на сигнал волоконно-оптического гироскопа за счет применения дополнительной модуляции
- Расчет и оптимизация оптической схемы фотоприемного модуля спектрального диапазона 1,3–1,6 мкм
- Анализ остаточных признаков с декомпозицией по эмпирическим модам для извлечения пространственных последовательных шаблонов из серийных изображений дистанционного зондирования
- Формирование траектории цифрового двойника многозвенного механизма с использованием адаптивного алгоритма оценки параметров нелинейного движения
- Исследование спектрально-люминесцентных свойств квантовых точек CsPb(BrCl)3 во фторфосфатных стеклах
- Исследование оптических явлений в мультиспектральном матричном фотоприемнике на основе кремния
- Исследование влияния отклонения от стехиометрии иттрий алюминиевого граната на эффективность конверсии ионов хрома в четырехвалентное состояние
- Влияние низких температур и термического отжига на оптические свойства квантовых точек InGaPAs
- Контроль динамики экструзии при трехмерной печати изделий
- Подход к обнаружению сообщества в динамических сетях, основанный на принудительной неотрицательной матричной факторизации
- Система визуального отображения изменения физиологического состояния пациентов с хроническим нарушением сознания и передачи данных по беспроводной оптической связи
- Обработка данных ледовой разведки при условии низкого качества исходных изображений
- Прогнозирование летального исхода у пациентов с установленным диагнозомCOVID-19
- О возможности расширения исследуемых динамических диапазонов в термоанемометрии
- Эффект биений в одноосноориентированных полимерных материалах
- Численная методика расчета тяги сопла широкодиапазонного ракетного двигателя
- Численное моделирование характеристик высоконесущих профилей с энергетическими методами увеличения подъемной силы