Разбор результатов Clang SA и Infer

[Columpio]

flite

источник: архив из Yummy Research Team от 12 мая 2023 г.
запуск на коммите KLEE b3edd7e в дебаге
опции запуска:

                "--use-guided-search=error",
                "--mock-external-calls",
                "--posix-runtime",
                "--check-out-of-memory",
                "--suppress-external-warnings",
                "--libc=uclibc",
                "--skip-not-lazy-initialized",
                "--skip-not-symbolic-objects",
                "--external-calls=all",
                "--output-dir=/tmp/klee-out",
                "--max-time=120s",
                "--max-solver-time=5s",
                "--analysis-reproduce=/home/columpio/tmp/evaluation/flite/1.sarif",
                "/home/columpio/tmp/evaluation/flite/input.bc",

из файла удаляю всё кроме одной трассы, которую дебажу

1 трасса

Витя утверждает, что TP
В трассе 12 точек (5 unimportant), мы не достигаем даже первую

Запуск трассы полностью

Запуск начинается с этой функции:

cst_utterance *cg_synth(cst_utterance *utt)
{
    cst_cg_db *cg_db;
    cg_db = val_cg_db(utt_feat_val(utt,"cg_db"));

    cg_make_hmmstates(utt);
    cg_make_params(utt);
    // ... Columpio omitted rest of code
}

Первая точка в трассе - вызов cg_make_params(utt); (стр. 168), до него не можем дойти за 120 секунд, максимально доходим до вызова val_cg_db.
В конце возвращаем: 98.44% NullPointerException False Positive at trace 1.
Гипотеза: первый ивент не значим для трассы, можно его убрать.

Запуск трассы без первого ивента

Запуск начинается теперь с функции cg_make_params.
Опять доходим только до вызова val_cg_db на строчке
cg_db = val_cg_db(utt_feat_val(utt,"cg_db"));
В конце возвращаем: 98.05% NullPointerException False Positive at trace 1.
Гипотеза: сможем пройти дальше, если запустить в релизе

Запуск трассы без первого ивента в релизе

rm -rf /tmp/klee-out && ~/klee_build/klee_build110stp/bin/klee --use-guided-search=error --mock-external-calls --posix-runtime --check-out-of-memory --s
uppress-external-warnings --libc=uclibc --skip-not-lazy-initialized --skip-not-symbolic-objects --external-calls=all --output-dir=/tmp/klee-out --max-time=120s --max-solver-time=5s --analysis
-reproduce=/home/columpio/tmp/evaluation/flite/1_without_first_event.sarif /home/columpio/tmp/evaluation/flite/input.bc &> test1.log

KLEE просто упал:

  %20 = getelementptr inbounds %struct.cst_features_struct, %struct.cst_features_struct* %19, i32 0, i32 0, !dbg !251313 cst_features.c:55 12
  %21 = load %struct.cst_featvalpair_struct*, %struct.cst_featvalpair_struct** %20, align 8, !dbg !251313, !tbaa !251314 cst_features.c:55 12
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x7f4cb3ee142f]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7f4cb3edf762]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0xaa6905)[0x7f4cb3ee1905]
/lib/x86_64-linux-gnu/libc.so.6(+0x43090)[0x7f4cb2f59090]
/home/columpio/klee_build/klee_build110stp/bin/klee(+0xa3ecc)[0x55e4807f7ecc]

2 трасса

Витя утверждает, что TP
В трассе 7 точек (3 unimportant), мы не достигаем даже первую

Запуск трассы без первого ивента

Запуск начинается теперь с функции cg_make_hmmstates.
Всё то же, что в 1 трассе
KLEE: WARNING: 98.05% NullPointerException False Positive at trace 1
После исполнения осталось 15 состояний со следующими парами "скорость, confidence":
[[-1.0, 6.25], [-1.0, 1.5625], [-1.0, 0.78125], [-1.0, 0.390625], [-1.0, 6.25], [8.0, 0.1953125], [-1.0, 1.5625], [-8.0, 0.390625], [5.0, 0.78125], [-1.0, 0.78125], [7.0, 0.1953125], [3.0, 0.390625], [1.0, 0.1953125], [1.0, 0.1953125], [-1.0, 0.390625]]
Т.е. только 6 состояний с неотрицательной скоростью.
Сумма всех CR всех оставшихся состояний = 20.3125%
Сумма CR состояний с неотрицательной скоростью = 1.953125%
Собственно, KLEE репортит 98.05% = 100% - 1.953125%

Выводы

• KLEE просто не доходит до ивентов, вязнет в коде
• несмотря на это имеем высокий CR: >95%

Анализ состояний 2 трассы

executed ids {2, 6, 7, 8, 9, 11, 12, 15, 16, 18, 20, 21, 23}

{6: 50.0, 7: 25.0, 8: 6.25, 9: 1.5625, 10: 3.125, 11: 0.78125, 12: 6.25, 13: 3.125, 14: 0.78125, 15: 0.1953125, 16: 0.1953125, 17: 0.390625, 18: 0.1953125, 19: 0.390625, 20: 0.02441406, 21:
0.78125, 22: 0.390625, 23: 0.04882812, 24: 0.09765625, 25: 0.09765625, 26: 0.1953125, 27: 0.04882812, 28: 0.02441406, 29: 0.04882812}
99.99999997999998
states in the end (12): [(28, 1.0, 0.02441406), (20, 12.0, 0.02441406), (27, -1.0, 0.04882812), (23, 5.0, 0.04882812), (29, -1.0, 0.04882812), (25, 3.0, 0.09765625), (24, 3.0, 0.09765625), (
18, 8.0, 0.1953125), (26, 1.0, 0.1953125), (22, -1.0, 0.390625), (19, -1.0, 0.390625), (13, -1.0, 3.125)]
number of positive states in the end: 7

baseRemovedStates states with reasons: [(6, 29), (8, 29), (9, 29), (10, 16), (11, 29), (14, 16), (15, 29), (16, 29), (17, 16)]
all states in the end {13, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29}
left without target forest in the end {12, 21, 7}
not mentioned in the log ids: set()
reasons for states to be removed: [(2, 29), (4, 29), (6, 29), (7, 29), (8, 29), (9, 29), (10, 16), (11, 29), (12, 29), (13, 2), (14, 16), (15, 29), (16, 29), (17, 16), (18, 29), (19, 2), (20
, 29), (21, 29), (22, 2), (23, 29), (24, 29), (25, 29), (26, 29), (27, 2), (28, 29), (29, 2)]

sum of baseRemovedStates states: 63.28125
sum of all states in the end: 4.68749998
sum of positive states in the end: 0.6835937400000001
sum of left without target forest in the end: 32.03125
not in baseRemovedStates and with targetForest [13, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29]

• Состояния 7, 12, 21 были очищены от таргетов, потому что прошли "мимо" по CFG, и унесли с собой 32% уверенности
  • в серчёре они были обработаны при вызове: current = 7 (или 12, или 21), added = пусто, removed = пусто
  • именно поэтому их уверенность просто "пропала", если бы хоть что-то было бы в added, уверенность бы перераспределилась на другие состояния и была бы "жива"
• По ходу исполнения были удалены состояния: [(6, 29), (8, 29), (9, 29), (10, 16), (11, 29), (14, 16), (15, 29), (16, 29), (17, 16)]
  • почти у всех причина - 29 - SilentExit, как, например, здесь
    • в этом месте состояние убивается, потому что происходит чтение из символьного массива, прибивает форк, где массив может быть равен нулю
    • т.к. до сёрчера это даже не доходит, мы просто теряем здесь состояние с его уверенностью
  • унесли с собой 63% уверенности
• Из оставшихся состояний есть с отрицательной скоростью, но они почти все остановлены сёрчером
  • например, из-за того, что превышено число раскруток циклов
  • они несут 4%
• В итоге при остановке оставшиеся положительные состояния несут только 0.68% уверенности
• Таким образом, мы говорим пользователю 99% уверенность из первых двух пунктов, хотя мы не дошли даже до первого таргета в трассе

[Columpio]

На чём тормозится исполнение?

Код вызывает val_cg_db, который вызывает feat_find_featpair здесь, где просто цикл по списку

• 240 секунд - то же самое
• 120 секунд и search=dfs - то же самое
• 120 секунд и search=random-path - то же самое

[Columpio]

Трасса такая:

1. Вызов val_cg_db на символьной структуре
2. Вызов feat_val на символьном списке со строчками
3. Вызов feat_find_featpair на символьном списке со строчками
4. В этой функции происходит обход символьного связного списка со строчками

[Columpio]

Почему в searcher.update может прийти 1 состояние, из которого недостижим таргет?

Такое может быть в следующем случае.

assume(x == 0) # target is reachable from here via CFG
if x == 0: # here we get only one state from fork, so searcher.update will get just one state
  exit(0) # target is unreachable from here, so we drop the state and lose confidence rate
else:
  target()

[Columpio]

Почему удалённые состояния, возникшие из internal fork'ов, учитываются в рассчёте confidence rate?

Типический пример лога:

6$  %43 = load %struct.cst_features_struct*, %struct.cst_features_struct** %42, align 8, !dbg !251688, !tbaa !251689 cst_cg.c:227 23
forked 6 into 6 7
Executor.removedStates.add 6 because 29
forked 7 into 7 0
UPDATE enter: 6 1.000000e+02
UPDATE exit: 6 5.000000e+01 7 5.000000e+01

Состояние 6 учитывается в рассчёте CR, хотя не должно.

[Columpio]

Нужно ли вообще учитывать removedStates в Searcher::update при рассчёте CR?

Гипотеза: сейчас состояние попадает в removedStates только если:

• нашли TP
• нашли FN
• был сделан какой-то internal fork и он привёл к ошибочному состоянию, мы его закрываем через terminateState с SilentExit

Тогда removedStates учитывать вообще не нужно.

[Columpio]

Если не учитывать, итоговый CR понижается с 98.49% до 91.02%

[Columpio]

Можно ли дойти до этой строки?

• Непосредственно из этой функции: да, достижима
• Из функции feat_val: да, достижима
• Если брать исходную 2 трассу и первым ивентом в неё добавить эту строку: нет, не достижима, но CR упал до 28.12%

[Columpio]

cg_make_hmmstates вызывает item_feat_string на 234 строке, которая вызывает feat_string, которая вызывает feat_val.
Поэтому даже когда вызов utt_feat_val(utt,"cg_db") в cg_make_hmmstates проходит мимо нужного ретёрна в feat_val, ветка не обрубается сёрчером.

[Columpio]

Если вручную поставить отметки на cst_features.c:57, cst_features.c:176, cst_val.c:210 (ненулевые ретёрны по пути к нужному месту), то с 240 секундным TL доходим до cst_cg:228, а без отметок с тем же TL -- нет.

Как следствие, генерация таргетов в ретёрнах "на лету" кажется осмысленной.

[Columpio]

Запуск на релизе с TL 240 секунд, в первом столбце миллисекунды, которые заняло исполнение инструкции.

234.751 seconds all instructions execution
5468 instructions total
42.931784930504755 msec/instruction
(763, '[no debug info]$  %11 = tail call i32 @__klee_posix_wrapped_main(i32 %8, i8** %9, i8** %2) #8')
(296, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(257, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(224, '[no debug info]$  %20 = load i8, i8* %17, align 1, !tbaa !245360')
(210, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(203, 'cst_val.c:260 12$  %15 = load i32, i32* %14, align 8, !dbg !245380, !tbaa !245381')
(201, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(189, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(178, 'cst_val.c:114 17$  %18 = load %struct.cst_val_struct*, %struct.cst_val_struct** %17, align 8, !dbg !245378, !tbaa !245380')
(166, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(165, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(164, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(164, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(163, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(161, 'cst_val.c:114 17$  %18 = load %struct.cst_val_struct*, %struct.cst_val_struct** %17, align 8, !dbg !245378, !tbaa !245380')
(160, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(160, 'cst_val.c:209 9$  br i1 %23, label %24, label %31, !dbg !245385')
(158, 'cst_val.c:259 9$  %12 = bitcast %struct.cst_val_struct* %11 to %struct.cst_val_atom_struct*, !dbg !245376')
(158, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(156, 'cst_val.c:260 12$  %15 = load i32, i32* %14, align 8, !dbg !245380, !tbaa !245381')
(155, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(155, 'cst_val.c:259 31$  %11 = load %struct.cst_val_struct*, %struct.cst_val_struct** %3, align 8, !dbg !245375, !tbaa !245368')
(151, 'cst_alloc.c:112 9$  br i1 %42, label %43, label %60, !dbg !245396')
(150, 'cst_val.c:260 12$  %15 = load i32, i32* %14, align 8, !dbg !245380, !tbaa !245381')
(148, 'cst_features.c:136 17$  %59 = load %struct.cst_val_struct*, %struct.cst_val_struct** %58, align 8, !dbg !245420, !tbaa !245421')
(145, 'cst_val.c:114 17$  %18 = load %struct.cst_val_struct*, %struct.cst_val_struct** %17, align 8, !dbg !245378, !tbaa !245380')
(145, 'cst_relation.c:48 23$  br label %12, !dbg !245375')
(144, 'cst_features.c:130 10$  %40 = load i8*, i8** %39, align 8, !dbg !245402, !tbaa !245404')
(144, 'cst_val.c:260 12$  %15 = load i32, i32* %14, align 8, !dbg !245380, !tbaa !245381')
(143, 'cst_features.c:135 15$  store %struct.cst_featvalpair_struct* %53, %struct.cst_featvalpair_struct** %55, align 8, !dbg !245418, !tbaa !245399')
(142, 'cst_val.c:259 9$  %12 = bitcast %struct.cst_val_struct* %11 to %struct.cst_val_atom_struct*, !dbg !245376')
(140, '[no debug info]$  %9 = load i8, i8* %7, align 1, !tbaa !245360')
(137, 'cst_val.c:260 12$  %15 = load i32, i32* %14, align 8, !dbg !245380, !tbaa !245381')
(137, 'cst_features.c:127 19$  %29 = load %struct.cst_featvalpair_struct*, %struct.cst_featvalpair_struct** %28, align 8, !dbg !245388, !tbaa !245389')
(133, 'cst_features.c:135 15$  store %struct.cst_featvalpair_struct* %53, %struct.cst_featvalpair_struct** %55, align 8, !dbg !245418, !tbaa !245399')