sys

SYS: статический/символический инструмент для поиска хороших ошибок в хорошем (браузер) коде

Если вам интересно, проверьте (очень очень) новую повторную переосмысление здесь!

Установить

Установить зависимости

Если вы хотите установить SYS на местном уровне:

• LLVM-9, LLVM-9-Tools
• Boolector настроен с опцией --shared . См. Функции build() и package() в этом файле в качестве примера того, как установить Boolector после того, как вы его клонируете. На Arch Linux вы можете просто установить boolector-git из AUR.
• Стек инструментов Haskell

В качестве альтернативы вы можете использовать Dockerfile от Ralf-Philipp Weinmann.

Строительство проекта

Как только у вас установлены все зависимости, вы сможете просто создать инструмент:

 stack build

Тест

После того, как вы создаете инструмент, вы можете создать и запустить наши тесты с помощью:

 stack test

Это будет выполнять более или менее полную версию нашего тестового набора, а также регрессионные тесты для каждой ошибки, которую мы перечисляем в статье. Набор занимает чуть более двух минут на ноутбуке с 64 ГБ оперативной памяти и 8 потоков. Все тесты с одним исключением-ошибка, у которого источник, у нас возникают проблемы с отслеживанием-должны пройти. Если что-то еще терпит неудачу, попробуйте повторно выполнить тесты; Решатель, возможно, был рассчитан на время (этого не произошло на наших машинах, но, поскольку мы не можем дать вам вход в систему для аннонимности, это вероятно, что это произойдет на вашей машине).

Если вы просто хотите воспроизвести результаты бумаги и ничего другого, запустите:

 stack test --ta '-p End-to-end'

Бегать

После того, как вы создали инструмент, теперь вы можете использовать его, чтобы найти ошибки!

 stack exec sys

Инструмент принимает несколько вариантов:

  -d DIR    --libdir=DIR   directory (or file) to analyze
  -e EXTN   --extn=EXTN    file extension
  -c CHECK  --check=CHECK  checker to run

• Опция -d используется для указания каталога (содержащего файлы LLVM) или одного файла LLVM.
• Опция -e используется для указания расширения файлов для проверки. Это полезно при создании вашего проекта с различными уровнями оптимизации (например, .ll-O0 для отладочной сборки с -O0 и .ll-O0_p для производства).
  • ll соответствует всем файлам *.ll
  • O0 соответствует *.ll-O0_p файлам *.ll-O0
  • O1 соответствует всем *.ll-O1 и *.ll-O1_p
  • O2 совпадает с файлами *.ll-O2 и *.ll-O2_p
  • O3 совпадает с файлами *.ll-O3 и *.ll-O3_p
  • Og соответствует всем *.ll-Og и *.ll-Og_p файлы
  • Os соответствует всем *.ll-Os и *.ll-Os_p файлы
  • Oz совпадает со всеми *.ll-Oz и *.ll-Os_z файлы
  • prod соответствует всем *_p -файлам
  • any совпадают со всеми файлами
• Параметр -c используется для указания шашки для запуска, один из:
  • uninit : ненициализованная проверка памяти
  • heapoob : Malloc oob Checker
  • concroob : отрицательный индекс oob checker
  • userinput : Пользовательский шахер ввода

Пример

Чтобы найти ненициализованную ошибку доступа к памяти, которую наш инструмент найден в библиотеке Firefox Prio:

 $ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p

Инструментальный флаги два ошибки. Давайте посмотрим на первое:

 Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]

Если вы осмотрите функцию serial_read_mp_array (), путем блока Buggy - %4 (первый блок) до %71 , где мы используем [ %73 ].

Помощь

Мы не тестировали (и, вероятно, не протестируем) SYS на что -либо, кроме Arch Linux. Мы рады интегрировать патчи, которые добавляют поддержку других систем OSES и сборки!

Структура каталога

 ├── app            -- Executable used to run the checkers
├── src
│   ├── Checkers   -- Static and symbolic checkers
│   ├── Control    -- Logging helpers
│   ├── LLVMAST    -- LLVM AST interface
│   ├── InternalIR -- Internal IR used to represent paths for both static and symex
│   ├── Static     -- Static checker DSL
│   └── Symex      -- Symbolic DSL and execution engine
├── community      -- Community files
└── test           -- Tests