Отсутствует определение операторов if / else при статическом анализе - PullRequest
Новая
       73

Отсутствует определение операторов if / else при статическом анализе

3 голосов
/ 17 февраля 2011

Я пытаюсь поймать пропущенные необработанные условия выражения g внутри операторов if.

Первый пример 

if (a < 5) {
    // Do something
} else {
    // handled else condition
}

Второй пример 

if (a < 5) {
    // Do something
} else if (a >= 5){
    // handled else if condition
}

эти два примера верны и все возможности обрабатываются.

Но я пытаюсь разобраться в таких условиях, как 

if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
}

Но это условие не обрабатывает все возможности, и отсутствует условие 

} else if ((a >= 5) && (b <= 10)) {
   // missing condition which is not handled
}

Я пытаюсь найти такого рода уязвимости с помощью статического анализа и использования абстрактного синтаксического дерева исходных кодов. Есть ли какой-нибудь алгоритм, подход или какой-либо документ, который изучается по этой проблеме?

Ответы [ 2 ]

3 голосов
/ 17 февраля 2011

Если вы хотите уменьшить проблему до более общей проблемы, вы можете преобразовать код 

<code>
if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
}

в 

<code>
if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
} else {
/*@ assert false ; */
}

Разумный компилятор будет выдавать тот же код для преобразованной версии, что и для исходной версии, и теперь вы можете использовать статический анализ или генерацию тестов для проверки того, что assert выполняется, что аналогично проверке того, что последний else никогда не берется, и это именно то, что вас интересует.

Инструменты существуют, если приведенный выше код является Java (assert может быть аннотацией JML), C (assert может быть аннотацией ACSL) или C # (assert может быть аннотацией Spec #). Алгоритм Элиана Эббинга хорош, но я предлагаю вариант, чтобы автоматические средства проверки теорем, используемые в качестве серверной части для этих инструментов, выполняли свою работу без повторной реализации колеса, которое определяет, является ли данное логическое предложение тавтологией. Скорее всего, существующие колеса работают лучше, чем когда-либо.

Пример на C, с использованием Frama-C и Jessie: 

int a, b;

main(){
  if ((a < 5) && b > 10) {
    // Do something
  } else if ((a >= 5) && (b > 10)){
    // handled else condition
  } else if((a < 5) && (b <= 10)) {
    // handled else condition
  } else {
    /*@ assert \false ; */
  } 
}

Утверждение не подтверждено, что указывает на то, что Джесси не смогла проверить, что последний случай был недоступен. При добавлении } else if ((a >= 5) && (b <= 10)) { утверждение подтверждается.

3 голосов
/ 17 февраля 2011

Если у вас есть код, подобный 

if(A) { ... }
else if (B) { ... }
else if (C) { ... }

, и вы хотите убедиться, что все возможности обработаны, то вам нужно доказать, что формула A or B or C всегда оценивается как true.Если все, что вы делаете, это проверяете диапазоны, то я бы преобразовал эту формулу в конъюнктивную нормальную форму .

После этого преобразования у вас есть формула вида 

(F1 or F2 or ...) and (G1 or G2 or G3) and (H1 or H2 or H3) ...

, где каждое атомарное суждение имеет форму (x < c), (x ≤ c), (x > c) или (x ≥ c), где x - переменная, а c - постоянная.Эти предложения можно объединить, используя следующие преобразования:

  1. (x < c1) вместе с (x > c2) преобразуется в true, если (c1 > c2)
  2. (x < c1) вместе с (x ≥ c2) преобразуется в true, если (c1 ≥ c2)
  3. (x ≤ c1) вместе с (x > c2) преобразуется в true, если (c1 ≥ c2)
  4. (x ≤ c1) вместе с (x ≥ c2) преобразуется в true если (c1 ≥ c2)

Теперь посмотрите на пункт (F1 or F2 or ...).Как только вы сможете выполнить одно из этих преобразований, тогда все предложение будет действительным, и вы сможете начать проверку следующего предложения.

Если все предложения действительны, то все возможности обрабатываются.

Общее решение (где условия в операторах if могут быть любыми) не так тривиально.Например, если вы хотите проверить if(f(x) || g(x)), возможно, что f() или g() имеют побочные эффекты, или выполните очень сложные вычисления.

...