Refactoring, Specification Inference & JSON Export

[viper-admin]

Pull request :twisted_rightwards_arrows: created by bitbucket user flurischt on 2017-07-19 12:38 Last updated on 2017-07-26 12:33 Original Bitbucket pull request id: 15

Participants:

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

Source: https://github.com/viperproject/sample/commit/e453c549af45986faf96c95b48aa0f7ba4c2fe90 on branch flurischt/sample/inference Destination: https://github.com/viperproject/sample/commit/dfcce74b5c0c9efe319018dfd0dff17b764eb1fe on branch master Marge commit: https://github.com/viperproject/sample/commit/45c5d4aff521a0579c4765f971bfe81c1788bb90

State: MERGED

OVERVIEW

This pull request consists of the following parts:

• Refactor ProgramResults to allow multiple CfgResults per identifier. A result can be tagged (for example with a call-string).
• Add a Bottom-Up (forward) Analysis-Runner and interpreter. Bottom-Up uses a topological ordering of the methods (based on the call-graph) to decided what to analyze next.
• Implement interprocedural integer octagon specification inference (bottom-up and top-down)
• Add functionality to export inferred specifications in JSON format. See InterproceduralIntegerOctagonBottomUpInferenceWithJsonExport

COMMENTS

• This adds a dependency on the lift-json library to sample-silver
• The current inference implementations all run a verifier on the extended programs. When exporting a JSON for the IDE the verifier is currently not run.

COMMITS

• create branch inference

• Add silver inference runners for the interprocedural (octagon) case

• Extend ProgramResult to allow multiple (tagged) CfgResults per method

• Switch interpreters to use the new tagged ProgramResult feature

  Will fix the failing tests later

• Refactor CfgResultsType

• Hacky prototype of inference in callees

• Cleanup some leftovers that cause a compiler warning

• Backed out changeset https://github.com/viperproject/sample/commit/5927bfb57a614ff5169123de5f864984243ec6b8

• Some cleanup

• Prototype of interproc inference with octagons

• update hgignore

• Infer the a disjunction of all calling-states as precondition

• Infer invariants as "method-precondition => invariant" for each available CfgResult

• Add bottom-up analysis runner

• Patch together the skeleton for a bottom-up octagon inference

• Implement bottom-up interpreter trait for inference

• Pass "method" to pre-/postcondition() helpers to be able to filter specifications for irrelevant identifiers.

  (For callers) it is for example not useful to speak about local variables in a methods postcondition.

• Infer postconditions to make the verifier happy.

• Add prototype that collects changes in program inference

• Fix backward analysis tests that were broken due to ProgramResult changes (tagged results)

• Implement JSON export of inferred specifications

• Cleanup

• Pass around a reference to the loop statement to get the position where to add invariants

• Switch to lowercase keywords in json export

• Cleanup

• Fix wrong documentation

• Cleanup

• Use the TopologicalOrderOfCallGraph to enqueue tasks in bottom up

• Make sure bottom-up inference ignores CfgResults tagged with a call-string

• Add library dependency for lift-json

[viper-admin]

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

I just pushed the changes to the JSON output format. The following message-types / error-tags are used:

private val SampleInferenceTag = "SpecificationInference" and private val SampleInferenceErrorTag = "sample.error.inferenceOmitted"

Example messages are:

{
  "type":"Error",
  "file":"sample-silver/src/test/resources/silver/example.sil",
  "errors":[
    {
      "start":"6:5",
      "end":"15:6",
      "tag":"sample.error.inferenceOmitted",
      "message":"Inference omitted since some already exist."
    }
  ]
}

{
  "type":"SpecificationInference",
  "file":"sample-silver/src/test/resources/silver/example.sil",
  "preconditions":[],
  "postconditions":[],
  "invariants":[
    {
      "position":"6:5",
      "specifications":[
        "invariant 0 <= i",
        "invariant j <= 10",
        "invariant i + j == 10",
        "invariant -10 <= i - j"
      ]
    }
  ]
}

position points to the { at the beginning of the loop or method body. The specifications should be inserted directly before that location.

Main class

ch.ethz.inf.pm.sample.abstractdomain.InterproceduralIntegerOctagonBottomUpInferenceWithJsonExport provides a demo implementation

First argument to the program should be the silver program to analyze/extend. Make sure the logger does not print to stdout when only the json is expected.

Humand friendly JSON output

Change SpecificationsJsonExporter.render to prettyRender to get a human friendly formatted JSON.

[viper-admin]

@dohrau commented on 2017-07-24 14:27

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

If we pass the method as an argument, then there is no need to pass the existing preconditions as a separate argument since we can get them via method.pres.

[viper-admin]

@dohrau commented on 2017-07-24 14:27

Outdated location: line 153 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

Same as for preconditions.

[viper-admin]

@dohrau commented on 2017-07-24 14:28

Outdated location: line 161 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

Same as for preconditions.

[viper-admin]

@dohrau commented on 2017-07-24 14:29

Outdated location: line 171 of sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

To be consistent with the preconditions, postconditions, and loop invariants, we probably want to pass the new-statement instead of the existing fields here.

[viper-admin]

@dohrau commented on 2017-07-24 15:20

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

Is there a particular reason why you use Java sets? There are also mutable sets in Scala.

[viper-admin]

@dohrau commented on 2017-07-24 16:34

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

To me it seems odd to have topological order as an argument to the analyze method. If I understand correctly it's something you only need for the bottom up analysis and can be computed from the call graph anyway. Unless there is a good reason to compute the topological order at this point I would defer it to a later point and remove the argument here.

[viper-admin]

@dohrau commented on 2017-07-24 16:47

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

Is there a particular reason why you use Java sets? There are also mutable sets in Scala.

I just saw that you use some existing Java code to compute the strongly connected components. It might be nicer to do the conversion between Java/Scala at the point where you call this code.

[viper-admin]

@dohrau commented on 2017-07-24 19:01

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

This is a minor thing (probably) but the bottom up inference crashes on the empty input.

[viper-admin]

@dohrau commented on 2017-07-24 19:07

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

The top down inference also adds constraints on method parameters to the postcondition. This is a bit redundant since it is not allowed to assign to parameters. E.g., in the output below ensures b == 7 && a == 5 ==> b == 7 and ensures b == 7 && a == 5 ==> a == 5 can be removed (they are tautologies anyway).

#!scala

method main()
{
  var r: Int
  r := add(5, 7)
}

method add(a: Int, b: Int) returns (r: Int)
  requires b == 7 && a == 5
  ensures b == 7 && a == 5 ==> b == 7
  ensures b == 7 && a == 5 ==> r == 12
  ensures b == 7 && a == 5 ==> a == 5
{
  r := a + b
}

[viper-admin]

@dohrau commented on 2017-07-24 19:13

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalInference.scala

The top down inference also adds constraints on method parameters to the postcondition. This is a bit redundant since it is not allowed to assign to parameters. E.g., in the output below ensures b == 7 && a == 5 ==> b == 7 and ensures b == 7 && a == 5 ==> a == 5 can be removed (they are tautologies anyway).

#!scala

method main()
{
  var r: Int
  r := add(5, 7)
}

method add(a: Int, b: Int) returns (r: Int)
  requires b == 7 && a == 5
  ensures b == 7 && a == 5 ==> b == 7
  ensures b == 7 && a == 5 ==> r == 12
  ensures b == 7 && a == 5 ==> a == 5
{
  r := a + b
}

Now that I look at this, I wonder whether we actually want to add the precondition. The postcondition is still true without the precondition and the precondition just unnecessarily restricts under what circumstances the method can be called.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 07:19

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/abstractdomain/NumericalInference.scala

This is a minor thing (probably) but the bottom up inference crashes on the empty input.

Empty file.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 07:30

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/SilverAnalysis.scala

To me it seems odd to have topological order as an argument to the analyze method. If I understand correctly it's something you only need for the bottom up analysis and can be computed from the call graph anyway. Unless there is a good reason to compute the topological order at this point I would defer it to a later point and remove the argument here.

We'll move the topological ordering into the interpreter.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 11:48

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

To be consistent with the preconditions, postconditions, and loop invariants, we probably want to pass the new-statement instead of the existing fields here.

:white_check_mark:

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 11:48

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

Same as for preconditions.

:white_check_mark:

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 11:48

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

Same as for preconditions.

:white_check_mark:

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 11:48

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/oorepresentation/silver/SilverExtender.scala

If we pass the method as an argument, then there is no need to pass the existing preconditions as a separate argument since we can get them via method.pres.

:white_check_mark:

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 13:10

Outdated location: sample-silver/src/main/scala/ch/ethz/inf/pm/sample/execution/SilverAnalysis.scala

To me it seems odd to have topological order as an argument to the analyze method. If I understand correctly it's something you only need for the bottom up analysis and can be computed from the call graph anyway. Unless there is a good reason to compute the topological order at this point I would defer it to a later point and remove the argument here.

:white_check_mark:

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 13:14

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

I just saw that you use some existing Java code to compute the strongly connected components. It might be nicer to do the conversion between Java/Scala at the point where you call this code.

:white_check_mark:

buildCallGraph() now works with a DirectedGraph[mutable.Set[...]].

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 13:50

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

This is a minor thing (probably) but the bottom up inference crashes on the empty input.

:white_check_mark:

For an empty file we get the following json output:

{"type":"SpecificationInference","file":"sample-silver/src/test/resources/silver/example.sil","preconditions":[],"postconditions":[],"invariants":[]}

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 17:13

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

The top down inference also adds constraints on method parameters to the postcondition. This is a bit redundant since it is not allowed to assign to parameters. E.g., in the output below ensures b == 7 && a == 5 ==> b == 7 and ensures b == 7 && a == 5 ==> a == 5 can be removed (they are tautologies anyway).

#!scala

method main()
{
  var r: Int
  r := add(5, 7)
}

method add(a: Int, b: Int) returns (r: Int)
  requires b == 7 && a == 5
  ensures b == 7 && a == 5 ==> b == 7
  ensures b == 7 && a == 5 ==> r == 12
  ensures b == 7 && a == 5 ==> a == 5
{
  r := a + b
}

Note to self: we agreed in the meeting to leave it as is for now.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 17:14

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

The top down inference also adds constraints on method parameters to the postcondition. This is a bit redundant since it is not allowed to assign to parameters. E.g., in the output below ensures b == 7 && a == 5 ==> b == 7 and ensures b == 7 && a == 5 ==> a == 5 can be removed (they are tautologies anyway).

#!scala

method main()
{
  var r: Int
  r := add(5, 7)
}

method add(a: Int, b: Int) returns (r: Int)
  requires b == 7 && a == 5
  ensures b == 7 && a == 5 ==> b == 7
  ensures b == 7 && a == 5 ==> r == 12
  ensures b == 7 && a == 5 ==> a == 5
{
  r := a + b
}

I did not add any filtering. But I fixed the case where requires c == 0 || c == 0 || c ==0 || c == 0 was inferred.

[viper-admin]

Bitbucket user flurischt commented on 2017-07-25 17:15

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

I did not add any filtering. But I fixed the case where requires c == 0 || c == 0 || c ==0 || c == 0 was inferred.

:white_check_mark:

[viper-admin]

@dohrau approved :heavy_check_mark: the pull request on 2017-07-26 12:31