Рассчитать диапазон входных данных, который приводит к удовлетворению предиката

Question

Допустим, у нас есть следующий C-код:

int my_main(int x){
    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                //@(x >= 9 && x <= 14);
            }
        }   
    }
    return 0;
}

Я хотел бы вычислить с помощью статического анализа границы переменной x при инициализации, которые приводят к удовлетворенному предикату. В этом примере интервал x в начале main должен быть [8, 12].

TL; DR: Как лучше всего рассчитать эти диапазоны, учитывая утверждение где-то в коде?

Что я пробовал до сих пор:

Я думаю, что лучший способ приблизиться к этому - использовать самый слабый калькулятор предусловий. Iv'e пытался поиграться с плагином wp frama-c, но, поскольку он создан для целей проверки, я не уверен, насколько он полезен в этом случае использования. При применении плагина на следующий код:

int main(void){
    int n = 0;
    int x;

    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                n = x;
            }
        }   
    }
    //@ assert p: n >= 9 && n <= 14;
    return 0;
}

Я получаю следующий предикат, посланный в решатель alt-ergo:

  goal main_assert_p:
    forall i_1,i : int.
    is_sint32(i) ->
    is_sint32(i_1) ->
    (((i < 6) -> (0 = i_1)) and
     (**(6 <= i)** ->
      (((i < 8) -> (0 = i_1)) and
       (**(8 <= i)** ->
        (((12 < i) -> (0 = i_1)) and (**(i <= 12)** -> (i_1 = (2 + i)))))))) ->
    ((9 <= i_1) and (i_1 <= 14))

Если вы посмотрите внимательно, можно определить требуемый интервал на входе, следуя границам переменной i, которые не приводят к (i_1 = 0). Я отметил эти границы. Это не очень надежно, например, если утверждение изменяется на && n <= 13, "левая сторона" предиката подразумевает, что он остается неизменным, так как ни одно из условий не изменилось. Также я не уверен, насколько это полезно в других сценариях, например, при изменении моего утверждения на оператор require при вызове функции, я не могу понять полученный предикат:

if (x < 15){
      sum(x);
}

И добавление оператора require в функцию:

//@requires (n >= 6 && n <= 11);
int sum(int n){

Я получил:

    goal main_call_sum_pre:
  forall i : int.
  (6 <= i) ->
  (8 <= i) ->
  (i <= 12) ->
  is_sint32(i) ->
  is_sint32(1 + i) ->
  is_sint32(2 + i) ->
  ((4 <= i) and (i <= 9))

Answer 1

Вы правы в том, что WP (или Jessie), основанная на парадигме "самого слабого предусловия", является подходящими инструментами для использования здесь. Что они делают, однако, чтобы создать смысл:

предварительное условие, заданное спецификацией ==> вычисленное самое слабое предварительное условие

Затем внешние проверяющие лица пытаются доказать вышеуказанное значение, при этом (в общем случае) предоставляется только ответ истина / ложь / время ожидания.

Вы можете сделать это методом проб и ошибок, используя "LOWER_BOUND ≤ x ≤ UPPER_BOUND" в качестве пост-условия user_input(*), и увидеть, доказано ли это или нет. Используя инструменты, которые вы используете в качестве черных ящиков, вы дойдете до дихотомии до интервала за несколько шагов. Вы никогда не узнаете, есть ли у вас оптимальный интервал, или же испытатель просто перестал иметь возможность доказывать свойство, которое все еще удерживалось, но это жизнь.

Или вы можете позволить проверяющему выполнить работу по упрощению за вас, но для этого требуется более сложный тип взаимодействия, чем просто "верно ли это свойство?". Некоторые проверяющие позволят вам иметь доступ к этой информации легче, чем другие. Это все в руках проверяющего, действительно, после того, как WP выполнил свою работу, и ваш вопрос действительно о "проверяющем, который сводит логическую формулу к пределам x что делает формулу истинной ", а не о Frama-C.

Это исследование включало вопрос "просто дайте мне лучший интервал, который вы можете" в некоторых местах. Речь идет о плавающей точке, но поскольку целые числа с плавающей точкой сложнее рассуждать, используемые там инструменты и методы могут также применяться к вашей проблеме. В частности, прувер "Гаппа", специальность которого является плавающей точкой, изначально работает с интервалами, а IIRC был прувером, предоставившим "лучшие" интервалы, где это необходимо в этом исследовании (стр. 11, "Например, как мы определить границу 1/16 в нашем иллюстративном примере? ")

---

(*) Обратите внимание, что после добавления вызова user_input() Чтобы прояснить смысл, то, что вы ищете, на самом деле является пост-условием этой функции, а не предварительным условием основной функции.

Answer 2

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

Ваше логическое выражение содержит константы. Если вы замените их на переменные, то у вас будет гибкое утверждение.