iAI icon indicating copy to clipboard operation
iAI copied to clipboard

Clarify meaning of https://github.com/secure-software-engineering/phasar/wiki/Writing-an-Inter-Procedural-Monotone-Framework-Analysis-(Using-Call-Strings)

Open blipper opened this issue 3 years ago • 1 comments

There is a comment her that "An example for an analysis that is not distributive is full-constant propagation. In simple words a flow function is not distributive if a data-flow fact's validity depends on two or more other data-flow facts (at the same time)"

Can you please expand upon this restriction? I am interested in writing an IFDS that is similar to the https://checkerframework.org/manual/#constant-value-checker. Basicaly I want to have a analysis that aggregates a set of values for each variable if they are determinable during the analysis and kills the fact if not (e.g. Read in from filesystem or network or set to random value). The above statement makes me think that I need to use Monotone?

blipper avatar Jul 28 '21 04:07 blipper

This depends on how you want to implement your analysis. In very simplified terms, only linear constant propagation is distributive. Which means, you can only propagate constants with expressions CC = a * C + b, with C and CC being variables for which we know a constant values and a and b trivially constant factors. Expressions such as CCC = CC + C will lead to CCC being overapproximated.

MMory avatar May 06 '22 13:05 MMory