Calculate the range of an input which results in satisfying a predicate

Question

Lets say we have the following C code:

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

I'd like to calculate using static analysis the bounds on the variable x at initialization which result in a satisfied predicate. In this example, the interval of x at the start of main should be [8, 12].

TL;DR: What would be the best way to calculate these ranges given an assertion somewhere in the code?

What I tried so far:

I think the best way to approach this is using a weakest precondition calculator. Iv'e tried toying around with the wp plugin of frama-c but since it is built for verification purposes, I am not sure how useful it is in this use case. When applying the plugin on the following code:

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;
}

I get the following predicate sent to the alt-ergo solver:

  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))

If you look carefully, it is possible to identify the required interval on the input by following the bounds on the variable i which don't result in (i_1 = 0). Iv'e marked these bounds. This is not very robust, for example if the assertion changes to && n <= 13, the 'left side' of the implies predicate stays the same as none of the conditions changed. Also i'm not sure how useful this is in other scenarios, for example altering my assertion to a requires statement when calling a function, I can't understand the resulting predicate:

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

And adding a requires statement to the function:

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

I get:

    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

You are right that WP (or Jessie), being based on the “weakest precondition” paradigm, are the right tools to use here. What they do, however, is to build the implication:

precondition given by the specification ==> computed weakest precondition

The external prover(s) then attempt to prove the above implication, with (in the general case) a true/false/timeout answer only being provided.

You could do it by trial and error, using “LOWER_BOUND ≤ x ≤ UPPER_BOUND” as post-condition of user_input(*), and seeing whether the implication gets proved or not. Using the tools you have as black boxes, you would arrive by dichotomy to the interval in a few steps. You'll never know if you have the optimal interval or if the prover just ceased to be able to prove a property that still held, but that's life.

Or you could let the prover do the simplification work for you, but that requires a more complex kind of interaction than just “is this property true?”. Some provers will let you have access to that information more easily that others. It's all in the prover's hand, really, after WP has done its job, and your question is really about “a prover that reduces a logical formula to bounds on x that make the formula true”, rather than about Frama-C.

This study involved the question “just give me the best interval you can” in some places. It is about floating-point but since floating-point is only more difficult that integers to reason about, the tools and techniques used there might apply to your problem as well. In particular, the “Gappa” prover, the speciality of which is floating-point, works natively with intervals and IIRC was the prover that provided the “best” intervals where necessary in that study (page 11, “For example, how did we determine the bound 1/16 in our illustrative example?”)

---

(*) Note that after having added the call to user_input() to clarify the meaning, what you are looking for is really the post-condition of that function, rather than the pre-condition of the main function.

Answer 2

assert takes a Boolean expression and if FALSE, aborts the application with a message. assert is generally a macro and in the non-debug version of your program, calls to these macros are removed during preprocessing.

Your Boolean expression contains constants. If you replace those with variables, then you have your flexible assert.