Problem with narrowing strategy for nonmonotonic transformation function about ikos HOT 14 CLOSED

Hi @arthaud thanks for the response. I am looking forward to trying out your fix.

My context is mostly GCC-based builds for ARM CPU's (Cortex-M0, M3, M4, R4).

I also had a problem with the construct while (1);, used a few places as a stupid way to halt execution (the system would get reset by the hardware watchdog). I had to replace the while-loop with assert(0) to get convergence. I'm excited to see if that is remedied also :)

I am super impressed by IKOS. It's really fast and uses very little RAM compared to other tools 👍 It scales way better than any other sound analysis-tools I've tried.

from ikos.

Hi @wutianba,

Thanks for reporting this issue.

I am surprised that I've never seen this before. There is indeed an issue with the decreasing iterations (narrowing) during the fixpoint computation. It does not converge for this code.

Here is approximately what happens:

• After the increasing iterations (widening), we get the interval [INT_MIN, 10] for count at the beginning of the loop;
• Then, we start the decreasing iterations. First, we use the meet abstract operator for the first iteration, and we get [-536870912, 10] at the beginning of the loop;
• Then, we try to converge using the narrowing on itervals, as defined in the literature. Running an iteration gives us [-268435456, 10] at the beginning of the loop. Since this is not a fixpoint, we apply the narrowing and get: narrow([-536870912, 10], [-268435456, 10]) = [-536870912, 10]. Hence, the infinite loop.

I have to review my abstract interpretation materials, as I am very puzzled at the definition of the narrowing for intervals (i.e, narrow([L0, U0], [L1, U1]) = [if L0=-oo then L1 else L0, if U0=+oo then U1 else U0]). I think this is not enough to assure convergence (e.g, with your code). I don't understand why the meet operator is not used instead since there is no infinite chain of decreasing intervals anyway.

from ikos.

Thanks for your repley.
I'm not sure if it's right, but in my understanding, the narrowing operation can only be used on a widened result and a boundary. I am not sure if the subsequent narrowing operation is correct.
Therefore, I have been confused, how to narrow the results after widening, I think there is no good way to find an exact boundary.
Also, if I remove all the code of narrowing, is there any problem?
Thanks again.

from ikos.

Just to add my two cents: I have also seen a few instances where analysis did not converge.

In one case analysis did not converge on a function like shown below:

unsigned short delay(unsigned short ticks) {
  while (ticks--) {
    asm("nop");
  }
  return ticks;
}

Unfortunately I could not replicate the divergence with a small example. It only happens when scanning the whole project with the other ~100k lines of C code.

I have also had a case where I had to add --opt=aggressive or completely disable inter-procedural analysis (with --proc=intra) to get past the inter-procedural function analysis. In both cases, I used the interval value-domain.

I'm sorry if I'm asking a stupid question here, but is the analysis theoretically supposed to converge for all the abstract domains?
I think the meet-over-all-paths algorithm only guarantees convergence for distributive domains/lattices. I am pretty sure the interval domain is distributive, but not sure about the other domains.

from ikos.

Hi again,

I talked yesterday with a coworker and it is now clear to me.

The convergence of the fixpoint is assured by the narrowing operator only if it is applied on a fixpoint after a widening. The current implementation does an additional step with a meet (probably to improve the precision) before the narrowing, which breaks the convergence.

The right strategy is to apply the narrowing first until it converges, and then possibly add a fixed number of steps with meets to improve the precision.

There is also another problem: we check the convergence before applying the narrowing. This is not what the literature says and it also breaks the convergence.

I will push a fix within the day.

@wutianba: You were right that the narrowing needs to be applied right after the widening.
@wutianba: You could remove the narrowing steps as a quick fix, yes, but you might lose precision.
@kokke: Thanks for you comment. Hopefully my incoming patch should fix all your issues. If not, feel free to open a new issue on Github.
@kokke: Yes, the analysis is theoretically supposed to converge for any abstract domain, given that it provides a correct widening and narrowing. From what I know, some complex abstract domains do not provide a narrowing operator, in that case we can simply skip the decreasing iterations (This is what we do for APRON abstract domains, see interprocedural.cpp#L445)

from ikos.

I fixed the errors and improved the fixpoint iterator implementation. This issue is now fixed.

I actually added an optimization: when we reach the fixpoint during the increasing iterations new_pre.leq(pre), we can use the narrowing right away. This saves an iteration for each cycle, and gives exactly the same results. IKOS is now ~20% faster in average (in debug mode). This is great!

@kokke: Thanks! I am actually trying to write a report for my supervisors about the influence of IKOS in the industry. If you are using IKOS at work, I would really appreciate if you could tell me more about it! For instance: what is your company, in which context do you use IKOS, are you satisfied about the results, etc. Feel free to email us at [email protected]! Even a few lines would be really appreciated!

@kokke: I understand your issue with while(1);. IKOS probably tells you that the code after the loop is unreachable, which is sound wrt. the C standard. We could maybe try to add an option to ignore while(1);. Feel free to open an issue about it ;)

from ikos.

By the way, we will release a new version soon, including:

• ikos-scan (a tool to replace wllvm);
• upgrade to llvm 7;
• support for Windows using msys2.

from ikos.

@arthaud
Supporting windows is a great idea, I spent too much effort to get ikos1.3 compiled with msvc or let ikos2.0 run on windows xp. I think Cygwin-2.5.2 might be better, it might be the last version of Cygwin or msys that can compile ikos2 for window xp(32bit).

from ikos.

I will try to see if I can support Cygwin as well. I don't know if it's easy to get all the dependencies (e.g, llvm).

from ikos.

Hi @arthaud - that fixed my convergence problems :) Thank you very much for the fast support.

I would be glad if I could help you. I will send an email to the IKOS-list, detailing what our company does, how we use IKOS (and static analysis in general) and what we think of IKOS compared to other tools.

from ikos.

Hi @arthaud

I was a bit too fast there - I still have problems getting analysis to converge on this function:

uint32_t CLKPWR_GetCLK (uint8_t ClkType)
{
    switch(ClkType)
    {
        case CLKPWR_CLKTYPE_CPU:
            return SystemCoreClock;

        case CLKPWR_CLKTYPE_PER:
            return PeripheralClock;

        case CLKPWR_CLKTYPE_EMC:
            return EMCClock;

        case CLKPWR_CLKTYPE_USB:
            return USBClock;

        default:
            while(1); //error loop
    }
}

SystemCoreClock, PeripheralClock, EMCClock and USBClock are all uint32_t-variables.

I run IKOS like this:
ikos --entry-points=CLKPWR_GetCLK whole_program.bc

It seems the problem is with the while(1);-loop, since analysis converges immediately if I replace with assert(0);.

from ikos.

Thanks. I was able to reproduce it and this is a bug in the dead code checker. I will have a patch soon.

Could you create a separate issue since this is not related to the narrowing?

Thank you.

from ikos.

Sorry for hijacking this issue-thread :$ I have submitted a separate issue here: #9

IKOS will be run on a few million lines of our industrial code the coming days and weeks :)

from ikos.

Thank you.

I am closing this since the issue is solved.

Feel free to open issues for any other bugs or questions.

from ikos.