LibSL - декларативный язык для формализации поведения библиотечных функций и API. Упрощает создание статических/динамических анализаторов, верификаторов и тестовых средств за счет единого описания семантики.
- Анализ программ требует понимания внешних библиотек, но ручное моделирование их поведения для каждого инструмента трудоемко и ненадежно.
- Отсутствие универсального формата спецификаций ведет к дублированию и рассогласованию моделей между платформами.
Решение LibSL: декларативное описание семантики один раз с генерацией моделей для разных анализаторов.
- Декларативные спецификации: сигнатуры функций, побочные эффекты (память, ресурсы), контракты (пред-/постусловия).
- Модели состояний: контекст (heap, файлы, сеть) и его изменения при вызовах (выделение/освобождение памяти, операции ввода-вывода).
- Инструментарий: парсер (
.libsl→ AST → IR), генератор моделей для JVM, Rust, C/C++, валидатор спецификаций.
library stdlib {
function malloc(size: size_t) -> ptr {
ensures result != null;
effect allocate(heap, result, size);
}
function free(p: ptr) -> void {
requires p in allocated(heap);
effect deallocate(heap, p);
}
}
- Унификация и гибкость: одна спецификация для разных инструментов, расширяемый DSL.
- Снижение ошибок: исключение дублирования моделей, формальная проверка спецификаций.
- Переносимость: поддержка JVM, Rust, C/C++.
- Анализ утечек памяти, гонок потоков.
- Верификация критических систем (медицина, авиация).
- Генерация тестов, рефакторинг кода при смене библиотек.
LibSL устраняет ручное моделирование библиотек, обеспечивая декларативное описание семантики с автоматической генерацией моделей. Интеграция с C/C++-инструментарием расширит применение языка и повысит надежность анализа.