CODEWITHSUNDEEP
frama-c
Trúc Nguyễn Lâm
Trúc Nguyễn Lâm

Reputation: 371

slevel option in value analysis of FramaC

I do not quite understand the slevel option in FramaC. Could anyone please explain more about how the value of slevel relates to user assertions (e.g. //@assert ...;) or states, and what factors cause the number of states go up?

For example, I have a program which does not contain loop, but containing if..else branches, go to statements, and there are also some user assertions in some points of the program, such as: 

...
a = Frama_C_unsigned_int_interval(0, 100);
//@ assert a == 0 || a == 1 || a == 2 || a == 3 || ... || a == 100;
...
b = Frama_C_unsigned_int_interval(a, 200);
//@ assert b == 0 || b == 1 || b == 2 || b == 3 || ... || b == 200;
...

In the output from the analysis (in which I set slevel to ~100000), there may be some like: Semantic level unrolling superposing up to 100 states, then this statement may repeat several times with larger number of states. Could anyone please explain how is this semantic level unrolling computed and how can I obtain the optimal slevel for the analysis. Thanks.

Upvotes: 2

Views: 355

Answers (1)

Virgile
Virgile

Reputation: 10148

Value analysis performs an abstract execution of the program. Instead of testing the program with arbitrary values, it executes it with abstract values encompassing all possible concrete execution. For instance, the abstract state associates x with the interval [0;10]. When arriving at an if statement, for instance if (x<=5) y = 1; else y=2;, the abstract state is split according to the condition. For instance, the then branch will be executed with an interval [0;5] and the else branch with an interval [6;10]. Conversely, at the end of the whole if, you have to join the two abstract states. This means that we will associate to each variable the smallest interval that contain all possible values coming from both (or more in case of a switch for instance) parent states. For instance, after the if, we have x in [0;10] and y in [1;2]. In addition, note that Value sees a normalized version of the C code, in which you always have to branches for an if ({ if (c) { s }} in the source in seen by Value as if (c) { s } else { }).

Setting -slevel to N means that Value will not join states as above, but instead propagate up to N separate states. In our example, this means that we now have two states, one in which x is in [0;5] and y==1 and one in which x is in [6;10] and y==2. This allows for more precision (for instance it rules out states such as x==0 && y == 2), but at the expense of computation time and memory consumption. In addition, the number of possible distinct states grows exponentially with the number of points of choice in your program. Indeed, if you have a second, unrelated, if, both states coming from the first one will be split, resulting in 4 states afterwards (assuming N>=4). Value gives you an indication of the number of distinct states that it is using so that you can see in the log where the slevel is spent, and possibly adjust it to meet a better precision/computation time ratio.

Finally, if are not the only constructions that will separate states. Any branching statement, in particular loops, will result in a state separation. Similarly, ACSL annotations expressed as disjunctions, as the one shown in your question will have the same effect: you end up with a state per element of the disjunction, provided you have enough slevel.

Upvotes: 6

Related Questions