Call strings (forward and backward)

[viper-admin]

Pull request :twisted_rightwards_arrows: created by bitbucket user flurischt on 2017-07-07 00:16 Last updated on 2017-07-13 14:04 Original Bitbucket pull request id: 14

Participants:

• bitbucket user flurischt
• bitbucket user caterinaurban (reviewer)
• @dohrau (reviewer) :heavy_check_mark:

Source: https://github.com/viperproject/sample/commit/d78197bb1acc4d7692c6cfe32cd934d72b0f3ec4 on branch flurischt/sample/call-strings Destination: https://github.com/viperproject/sample/commit/cf4ea364b202a227a795d4c1c9399e5b23ef8e0d on branch master Marge commit: https://github.com/viperproject/sample/commit/135b82c34af809cb270bd130c8eca86c5a57fef7

State: MERGED

SUMMARY

This pull requests introduces interprocedural forward and backward analysis using call-strings. The forward/backward interpreters now have an optional argument CallStringLength with which the precision of the analysis can be controlled. Possible arguments are CallString.FullPrecision, CallString.ContextInsensitive and CallString.approximate(k: Int = the desired length) where k is the number of method calls in the call-string.

Instantiations for Live Variable Analysis, Integer Intervals and Octagons are included in this pull request.

OTHER REMARKS

Currently ProgramResult still consists of only one CfgResult per Method. In the last meeting we discussed that this should be changed to one CfgResult per callstring/method combination. I did not include this change in this pull request because I first want to look if this new idea of ProgramResult is sufficient for the inference task that I'm working on right now. --> I'll change the ProgramResult in a future pull request.

COMMITS

• create branch call-strings

• Add tests for context sensitive analysis

• Introduce WorklistElement

  The worklist is now a Queue[WorklistElement] and nolonger a queue of tuples. This allows us to later tag (cal string) the elements in the worklist.

• Tag worklist elements with a call-string

• Use the type instead of hardcoding Map[...]

• Switch from map to a function that looks up CfgResults. This allows to return different CfgResults depending on the call-string.

• Fix typo in context sensitive test

• WIP: Introduce call-string and make analysis more precise.

  Open points:

  • recursion example does not terminate
  • widening (in the intraproc-interpreter) possible uses the wrong states

• Make number of iterations for a position depend on call strings

• Create method call edges depending on call string. No need to exclude main methods now.

• Disable dummy-main-recursive test for the ContextSensitive implementation

  A recursive main-function will start with the range -inf to inf. With full-length call-strings and an infinite domain this program will never end and can therefore not be analyzed (without restricting the call-string length). That's why this test is disabled.

• Only enqueue successors if the whole block has been analyzed

• Only enqueue callees if inputState goes "up in the lattice"

• Implement UnaryArithmeticExpression and therefore fix the dummy-main-component test

• Add precise recursive test

• Cleanup tests

• Only enqueue predecessors if block has been fully interpreter (backward)

• Implement (full-length) call-strings for backward analysis

• Make octagon string representation better readable

• Handle +(a) in the non-relational numerical domain

• merge

• Documentation

• Fix bug introduced by merge

• Refactor call-string handling into it's own type.

• Only use the call-string to lookup up the calling context

• Add optional argument to shorten call-string to interpreter and analysis

• Implement shortening of call-strings. The (full-length call-string) context-sensitive and the (0-length call-string) context-insensitive analyses work again.

• Hide CallString implementation details

• Cache the map from ProgramPoint to BlockPosition

• Cleanup forward interpreter

• Refactoring

• Instead of always taking the least upper bound use unify() to merge two states

• Comments

• Implement UnifyCommand for octagon domain

• WIP: Preserve arg_# variables to make relational calls work

• Add calstring to arg_ variables to make relational analysis over multiple calls work

• Add functionality to backup/recover temporary argument variables. Cleanup forward analysis for relational domain

• Add (temporary) variable renaming to backward analysis too

• Add silver-implementation of interproc' (jeannet) example programs

• Add lattice test for live variable analysis

• Bugfix

• Fix Code Inspection issues

• Make IntelliJ happy

• Fix typo

• Handle the special case where two main-methods call each other in the context-insensitive analysis

• User uppercase name for CallStringLength constant

  https://stackoverflow.com/a/9752606

• Cleanup/Document InterprocHelpers trait

• Store which cfg results are already available and which aren't

• ignore docker.sh

• Spellchecker

• Major Cleanup - get rid of any "temporary variables" in the program results

• Moar cleanup

• spellchecker

• Use CallString.FullPrecision, CallString.ContextInsensitive etc. instead of Option and None

• Cleanup

[viper-admin]

@dohrau commented on 2017-07-09 16:05

Outdated location: line 353 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

The interprocedural integer interval analysis and the interprocedural integer octagon analysis both seem to not terminate on the following input program:

#!scala

method factorial(i: Int) returns (r: Int)
{
    if (i == 0) {
        r := 1
    } else {
        r := factorial(i - 1)
        r := r * i
    }
}

[viper-admin]

@dohrau commented on 2017-07-10 08:24

Outdated location: line 839 of sample/src/ch/ethz/inf/pm/sample/abstractdomain/State.scala

I'm not entirely sure, but is this assumption correct? Isn't it the case that we use the unify command to merge two states with overlapping sets of variables in order to get the desired relational information? Or am I missing something? If the assumption is correct, then you should add a remark to the InterpocHelpers.unify method. If the assumption is wrong, then you probably have to adjust the IntegerOctagonAnalysisState.command method.

[viper-admin]

@dohrau commented on 2017-07-10 08:28

Outdated location: line 142 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

This is a minor comment, but I would remove this subclass and implement everything directly in the CallString trait (you have to make it a case class for this, of course). The apply method for CallString, which is also used by the interpreter, creates a SimpleCallString object which somehow couples these two classes and also makes it difficult to "inject" other implementations of CallString.

[viper-admin]

@dohrau commented on 2017-07-10 08:47

Outdated location: line 314 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

I guess it's intentional that we do nothing here. If so, add a short comment when this happens and why we don't want to do anything. If this case should not occur, add ??? or, even better, throw an exception.

[viper-admin]

@dohrau commented on 2017-07-10 08:50

Outdated location: line 297 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

It seems a bit cumbersome that the worklist is always passed as an argument. If I see it correctly, it's always a reference to the same worklist. I think it is worth considering moving it to a "global" place. For example, you could move it to InterprocHelpers where you already have the methodTransferStates, programResult etc.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-10 10:28

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

This is a minor comment, but I would remove this subclass and implement everything directly in the CallString trait (you have to make it a case class for this, of course). The apply method for CallString, which is also used by the interpreter, creates a SimpleCallString object which somehow couples these two classes and also makes it difficult to "inject" other implementations of CallString.

I moved this into a private class becuase I wanted the SimpleCallString(callStack: List..) constructor to be private. My goal was to everyone either use the apply function (which takes the call and the MethodDeclaration) or CallString.Empty to create objects. If I make this public then someone can pass in any List as callStack and that messes with the rest of the implementation (e.g. assumption that callStack.head is the current method, callStack.head.head is the last caller etc).

Is there another way to make the constructor private and force everyone to use the apply method?

[viper-admin]

Bitbucket user flurischt commented on 2017-07-10 10:32

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

The interprocedural integer interval analysis and the interprocedural integer octagon analysis both seem to not terminate on the following input program:

#!scala

method factorial(i: Int) returns (r: Int)
{
    if (i == 0) {
        r := 1
    } else {
        r := factorial(i - 1)
        r := r * i
    }
}

Let's discuss this in our meeting tomorrow. The current implementation for octagon and integer interval uses full-length call-strings. Full length call-strings for an infinite domain and unbounded recursion is (in my opinion) expected to not terminate. The analysis of this program terminates if either a main function with some actual values for i are provided or if the length of the call-string is bounded (by passing CallString.approximate(k) to the analysis)

[viper-admin]

Bitbucket user flurischt commented on 2017-07-10 10:33

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

Let's discuss this in our meeting tomorrow. The current implementation for octagon and integer interval uses full-length call-strings. Full length call-strings for an infinite domain and unbounded recursion is (in my opinion) expected to not terminate. The analysis of this program terminates if either a main function with some actual values for i are provided or if the length of the call-string is bounded (by passing CallString.approximate(k) to the analysis)

Btw: What is the expected result for negative i for this program?

[viper-admin]

Bitbucket user flurischt commented on 2017-07-10 10:33

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

It seems a bit cumbersome that the worklist is always passed as an argument. If I see it correctly, it's always a reference to the same worklist. I think it is worth considering moving it to a "global" place. For example, you could move it to InterprocHelpers where you already have the methodTransferStates, programResult etc.

Right. I'll change that.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-10 10:35

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

I guess it's intentional that we do nothing here. If so, add a short comment when this happens and why we don't want to do anything. If this case should not occur, add ??? or, even better, throw an exception.

This case can occur (for example if a main-method does not contain method calls). I'll document this.

[viper-admin]

@dohrau commented on 2017-07-10 13:17

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

Btw: What is the expected result for negative i for this program?

The most precise result for the exit state is bottom (since it is not reachable). This is actually what the analysis returns when you bound the length of the call-string.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-11 15:58

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

The interprocedural integer interval analysis and the interprocedural integer octagon analysis both seem to not terminate on the following input program:

#!scala

method factorial(i: Int) returns (r: Int)
{
    if (i == 0) {
        r := 1
    } else {
        r := factorial(i - 1)
        r := r * i
    }
}

Fixed

(The fixed comment(s) are for me to keep track of the status. I'll send you an email when everything is ready for review)

[viper-admin]

Bitbucket user flurischt commented on 2017-07-11 16:02

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalAnalysis.scala

Fixed

(The fixed comment(s) are for me to keep track of the status. I'll send you an email when everything is ready for review)

I set length 5 as a default for now. With five the analysis of the program above terminates immediately and McCarthy91 and Ackermann are analysed within seconds.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-11 20:36

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

It seems a bit cumbersome that the worklist is always passed as an argument. If I see it correctly, it's always a reference to the same worklist. I think it is worth considering moving it to a "global" place. For example, you could move it to InterprocHelpers where you already have the methodTransferStates, programResult etc.

Fixed. The worklist is now a global attribute.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-11 20:59

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

I guess it's intentional that we do nothing here. If so, add a short comment when this happens and why we don't want to do anything. If this case should not occur, add ??? or, even better, throw an exception.

Fixed

[viper-admin]

Bitbucket user flurischt commented on 2017-07-11 21:27

Location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/InterproceduralSilverInterpreter.scala

This is a minor comment, but I would remove this subclass and implement everything directly in the CallString trait (you have to make it a case class for this, of course). The apply method for CallString, which is also used by the interpreter, creates a SimpleCallString object which somehow couples these two classes and also makes it difficult to "inject" other implementations of CallString.

Fixed. No hidden private implementation anymore.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-12 23:48

Location: sample/src/ch/ethz/inf/pm/sample/abstractdomain/State.scala

I'm not entirely sure, but is this assumption correct? Isn't it the case that we use the unify command to merge two states with overlapping sets of variables in order to get the desired relational information? Or am I missing something? If the assumption is correct, then you should add a remark to the InterpocHelpers.unify method. If the assumption is wrong, then you probably have to adjust the IntegerOctagonAnalysisState.command method.

This assumption is not correct. --> Comment removed.

Both states share {arg_#1, arg_#2...} ids. For NonRelational domains those ids have the same abstract value in both states This is why lub works to unify integer-intervals. For relational domains one state only contains constraints relating arg_# to ret_# variables and the other state contains relationships between arg_# and the actual arguments in the method call. Here the implementation in IntegerOctagonAnalysisState.command does what it should (even though Octagons.unify has a comment that the environments are assumed to be disjoint...).

[viper-admin]

@dohrau commented on 2017-07-13 06:47

Location: sample/src/ch/ethz/inf/pm/sample/abstractdomain/State.scala

This assumption is not correct. --> Comment removed.

Both states share {arg_#1, arg_#2...} ids. For NonRelational domains those ids have the same abstract value in both states This is why lub works to unify integer-intervals. For relational domains one state only contains constraints relating arg_# to ret_# variables and the other state contains relationships between arg_# and the actual arguments in the method call. Here the implementation in IntegerOctagonAnalysisState.command does what it should (even though Octagons.unify has a comment that the environments are assumed to be disjoint...).

Are you saying that it works "by accident" or that the implementation of Octagons.unify does not exploit/need the assumption that the environments are disjoint?

[viper-admin]

Bitbucket user flurischt commented on 2017-07-13 11:46

Location: sample/src/ch/ethz/inf/pm/sample/abstractdomain/State.scala

Are you saying that it works "by accident" or that the implementation of Octagons.unify does not exploit/need the assumption that the environments are disjoint?

It works "by accident". Octagons.unify does need the assumption. But in this case the only identifiers that exist in both states are the temporary arguments. They will be removed after the call to unify anyway and only exist to preserve the relationship between the actual argument and the callee-returns.

I now did the following:

• More documentation what the UnifyCommand is expected to do: https://bitbucket.org/flurischt/sample/commits/https://github.com/viperproject/sample/commit/6873f4aefae021683e57854ecbaed3cd8bc8a220?at=default
• Implement unify directly in the (Integer)Octagons so that we don't rely on Octagons.unify for this special case.

[viper-admin]

@dohrau approved :heavy_check_mark: the pull request on 2017-07-13 12:49