ensuring(rec <= ...) -- big verification time variation

BLepers commented 8 years ago

Using 624e5a728ddde77b6ca707300be4cdbfc7173627

I am trying to prove that a function terminates by ensuring that "rec <= someValue". The time to check the postcondition varies a lot : checking the exact same file, it might take between 30s and 700s to validate the property (I might also have had some runs in which the validator never ends).

I know that this is a pretty vague issue, but if you have any idea on how to report more precise data, I can try it :)

Scheduler.txt

leon Scheduler.scala --functions=testEvolutionSimpleProofRec

Run1: [  Info  ] ║ Scheduler.testEvolutionSimpleProofRec  postcondition                                         348:14  valid      Z3-f  701.587 ║
Run2: [  Info  ] ║ Scheduler.testEvolutionSimpleProofRec  postcondition                                         348:14  valid  Z3-f  139.560 ║

Some timings also surprise me:

def testEvolutionSimple(...) {
   if(timer(c).current == Some(e)) {
      c
    } else if (find(doubleTimer(c,e).tasks, e).get == find(c.tasks, e).get - 1) {
      doubleTimer(c,e)
    } else if(rec <= maxSumBeforeSorted(c.tasks, e)) {
       testEvolutionSimple(c2, e);
    } else {
       error[Core]("Cannot happen :)"); 
    }
} ensuring(rec <= maxSumBeforeSorted(c.tasks, e) + 1)

On that code, the body assertion is always much faster than checking the postcondition, while the postcondition seems easier to check (it derives directly from the ifs). Any insight on why this is the case?

All tests are done on a fairly recent desktop machine with 8 cores.

ravimad commented 8 years ago

Sorry for the delayed reponse. Can you send me the source file Scheduler.scala ? Btw, you may have try out the latest updates to the Orb (resource bounds) inference engine, which fixes a major performance bug that crept in due to the changes to the SMT solving APIs.

BLepers commented 8 years ago

File attached. Scheduler.txt

Now I have the following error: :)

../leon/leon Scheduler.scala --functions=testEvolutionSimpleProofRec

scala.MatchError: rec$0 (of class leon.purescala.Expressions$FunctionInvocation)
    at leon.transformations.SerialInstrumenter.mapInstCallWithArgs(SerialInstrumentationPhase.scala:261)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:575)
    at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:480)
    at leon.transformations.ExprInstrumenter.tupleify(SerialInstrumentationPhase.scala:446)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:687)
    at leon.transformations.ExprInstrumenter$$anonfun$54.apply(SerialInstrumentationPhase.scala:639)
    at leon.transformations.ExprInstrumenter$$anonfun$54.apply(SerialInstrumentationPhase.scala:638)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:671)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:654)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:654)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:626)
    at leon.transformations.ExprInstrumenter.apply(SerialInstrumentationPhase.scala:697)
    at leon.transformations.SerialInstrumenter.leon$transformations$SerialInstrumenter$$mapBody$1(SerialInstrumentationPhase.scala:287)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:337)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:323)
    at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
    at scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
    at leon.transformations.SerialInstrumenter.apply(SerialInstrumentationPhase.scala:323)
    at leon.transformations.InstrumentationPhase$.apply(SerialInstrumentationPhase.scala:42)
    at leon.TransformationPhase.run(LeonPhase.scala:22)
    at leon.TransformationPhase.run(LeonPhase.scala:17)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:278)
    at leon.Main$.main(Main.scala:262)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

ravimad commented 8 years ago

At line 396, the code uses 'rec' in the body of the function. Instrumentation variables rec and steps, alloc should be used only in the postcondition (only then they have well defined semantics.) Can you let me know why do you have to do that ?

ravimad commented 8 years ago

Btw, if for some reason you need to count the number of recursions in the implementation, you have to maintain a counter say c and use it instead. However, in the postcondition you can state that rec == c

BLepers commented 8 years ago

What I would like to prove is:

def testEvolutionSimpleProofRec(c: Core, e:Task): Core = {
    require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined && find(c.tasks,e).isDefined && !c.tasks.isEmpty);

    val c2 = doubleTimer(c,e) // see doubleTimer def to know why we don't use timer directly
    if(timer(c).current == Some(e)) {
      c
    } else if (find(doubleTimer(c,e).tasks, e).get == find(c.tasks, e).get - 1) {
      doubleTimer(c,e)
    } else { // otherwise recursive call
       testEvolutionSimpleProofRec(c2, e);
    }
  } ensuring(res => (rec <= maxSumBeforeSorted(c.tasks, e) + ?));

But for some reason Leon was not able to prove it. So I added a "if rec <= max else error" and it seemed to work, but really this is not necessary (in fact I would prefer not to do it) :)

I tried to rerun leon with the function above (i.e., without the rec <= condition), but now I have this error :)

../leon/leon Scheduler.scala --functions=testEvolutionSimpleProofRec --instrument
java.util.NoSuchElementException: key not found: @library
@isabelle.typ
def get$4[T$423](thiss$108 : Option$0[T$423]): T$423 = {
  require(thiss$108.isDefined$1)
  val Some$0(x$244) = thiss$108
  x$244
}
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.MapLike$class.apply(MapLike.scala:141)
    at scala.collection.AbstractMap.apply(Map.scala:59)
    at leon.transformations.ExprInstrumenter.tupleifyCall(SerialInstrumentationPhase.scala:499)
    at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:469)
    at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:487)
    at leon.transformations.ExprInstrumenter.tupleify(SerialInstrumentationPhase.scala:446)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:687)
    at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:480)
    at leon.transformations.ExprInstrumenter.tupleify(SerialInstrumentationPhase.scala:446)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:687)
    at leon.transformations.ExprInstrumenter$$anonfun$54.apply(SerialInstrumentationPhase.scala:639)
    at leon.transformations.ExprInstrumenter$$anonfun$54.apply(SerialInstrumentationPhase.scala:638)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:671)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:654)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:626)
    at leon.transformations.ExprInstrumenter.apply(SerialInstrumentationPhase.scala:697)
    at leon.transformations.SerialInstrumenter.leon$transformations$SerialInstrumenter$$mapBody$1(SerialInstrumentationPhase.scala:287)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:337)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:323)
    at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
    at scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
    at leon.transformations.SerialInstrumenter.apply(SerialInstrumentationPhase.scala:323)
    at leon.transformations.InstrumentationPhase$.apply(SerialInstrumentationPhase.scala:42)
    at leon.TransformationPhase.run(LeonPhase.scala:22)
    at leon.TransformationPhase.run(LeonPhase.scala:17)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:278)
    at leon.Main$.main(Main.scala:262)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

BLepers commented 8 years ago

Here is a higher level view of what I try to prove, if it might help:

I have two values: a and b. doubleTimer either increments a if a < max, or decrements b, or changes the state to the final state.

I try to prove that this function finishes (it does because a cannot grow unbounded, so we will eventually be in the final state or decrease b):

recursiveFunction(c) {
    c2 = doubleTimer(c)
    if(c2 in final state) {
      // ok
    } else if(c2.b == c.b - 1) {
      // ok
    } else {
      // do a recursive call: recursiveFunction(c2)
    }
}

Thanks :)

BLepers commented 8 years ago

Here is a minimal example that corresponds to the logic of what I want to prove (but for some reason I have a compile error due to rec? Am I missing something?)

import leon.collection._
import leon.lang._
import scala.Any
import leon.annotation._
import leon.proof._
import leon.instrumentation._
import leon.invariant._
import leon.util.Random

object Scheduler {
   case class Core(a:BigInt, b:BigInt, max:BigInt) {
   }

   def doubleTimer(c:Core):Core = {
      if(c.a < c.max) {
         Core(c.a + 1, c.b, c.max)
      } else {
         Core(0, c.b - 1, c.max)
      }
   }

   def rec(c:Core):Core = {
      val c2 = doubleTimer(c);
      if(c2.b == c.b - 1) {
         c
      } else {
         rec(c);
      }
   } ensuring(res => (rec <= c.max));
}

[ Error  ] test2.scala:29:23: error: missing argument list for method rec in object Scheduler
[ Error  ] Unapplied methods are only converted to functions when a function type is expected.
[ Error  ] You can make this conversion explicit by writing `rec _` or `rec(_)` instead of `rec`.
              } ensuring(res => (rec <= c.max));
                                 ^
[ Fatal  ] There were errors.

ravimad commented 8 years ago

The minimal example is much better for me to debug. In your example, there is a function called rec so Scala compiler thinks you are referring to the function rec in the postcondition. I renamed rec to recFun and got the following counter-example: c -> Core(608, 450, -1)

ravimad commented 8 years ago

As the counter-example indicates: c.a could be greater than c.max and hence the function may not terminate

ravimad commented 8 years ago

There is one subtle issue here. The above function is non-terminating since you are making the recursive call with the same argument. Did you mean rec(c2) ? In any case, you need to make sure all functions are terminating before proving properties with leon. This is also true for rec. But, unfortunately, for various reasons, termination is not checked by "rec" function itself So try fixing the code and retry.

BLepers commented 8 years ago

Indeed :) With this function it works :)

def recF(c:Core):Core = {
      val c2 = doubleTimer(c);
      if(c2.b == c.b - 1) {
         c
      } else {
         recF(c);
      }
   } ensuring(res => ((c.max < 0) || (rec <= c.max)));

So I guess it should work too for my "real" example. So far I still have an error, but it seems unrelated to the "recursive checking": Scheduler.txt

java.util.NoSuchElementException: key not found: @library
@isabelle.typ
def get$4[T$423](thiss$108 : Option$0[T$423]): T$423 = {
  require(thiss$108.isDefined$1)
  val Some$0(x$244) = thiss$108
  x$244
}
    at scala.collection.MapLike$class.default(MapLike.scala:228)

ravimad commented 8 years ago

Actually, it is somewhat unsound in your example because your example does not terminate on all inputs. As I had mentioned, you must make sure that all functions terminate. Run termination phase as well, everytime you check properties with Leon.

ravimad commented 8 years ago

I will look into the crash

ravimad commented 8 years ago

I have fixed the crash in your example. Can you try it again. But, remember that you need to check termination of all functions as well.

BLepers commented 8 years ago

Yes, the functions I check in the real example terminate :) (Actually in the small example the function should have too... I wanted to do the recursion with c2 as parameter, not c... well...)

Anyways, now I get the following error, I am missing something? (Using e516634fc1e2fdf0d1608f106fef2a88e309139f)

../leon/leon Scheduler.scala --functions=testEvolutionSimpleProofRec 

scala.MatchError: rec$0 (of class leon.purescala.Expressions$FunctionInvocation)
    at leon.transformations.SerialInstrumenter.mapInstCallWithArgs(SerialInstrumentationPhase.scala:263)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:577)
    at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:482)
    at leon.transformations.ExprInstrumenter.tupleify(SerialInstrumentationPhase.scala:448)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:689)
    at leon.transformations.ExprInstrumenter$$anonfun$55.apply(SerialInstrumentationPhase.scala:641)
    at leon.transformations.ExprInstrumenter$$anonfun$55.apply(SerialInstrumentationPhase.scala:640)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:673)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:656)
    at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:628)
    at leon.transformations.ExprInstrumenter.apply(SerialInstrumentationPhase.scala:699)
    at leon.transformations.SerialInstrumenter.leon$transformations$SerialInstrumenter$$mapBody$1(SerialInstrumentationPhase.scala:289)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:339)
    at leon.transformations.SerialInstrumenter$$anonfun$apply$9.apply(SerialInstrumentationPhase.scala:325)
    at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
    at scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
    at leon.transformations.SerialInstrumenter.apply(SerialInstrumentationPhase.scala:325)
    at leon.transformations.InstrumentationPhase$.apply(SerialInstrumentationPhase.scala:42)
    at leon.TransformationPhase.run(LeonPhase.scala:22)
    at leon.TransformationPhase.run(LeonPhase.scala:17)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:278)
    at leon.Main$.main(Main.scala:262)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

ravimad commented 8 years ago

I don't get this error. Did you compile the build ? Also, can you run without --functions option. Also send me the Scheduler.scala file you are using.

BLepers commented 8 years ago

The file I use is: https://github.com/epfl-lara/leon/files/383971/Scheduler.txt

I did

$ git pull
$ sbt clean compile (3 warnings, no error)
$ sbt script
$ wget https://github.com/epfl-lara/leon/files/383971/Scheduler.txt
$ ./leon ./Scheduler.txt
#Same error, even when --functions is not set

$ java -version
java version "1.8.0_91"
Java(TM) SE Runtime Environment (build 1.8.0_91-b14)
Java HotSpot(TM) 64-Bit Server VM (build 25.91-b14, mixed mode)

Also I run the code on an 8-core machine (I don't know what you use, I might have more concurrency issues?).

Thanks :)

ravimad commented 8 years ago

Sorry for the delayed response. I investigated this error. It is due to the use of "rec" in the body of function testEvolution. As I mentioned in my earlier post, "Instrumentation variables rec and steps, alloc should be used only in the postcondition (only then they have well defined semantics.) ". Commenting it out runs leon without crashes.

ravimad commented 8 years ago

Were you able to fix this ? I am back at EPFL. If you want we can meet in person.

BLepers commented 8 years ago

Without rec it compiles now :)

The only issue I currently have is that Leon is not able to prove functions that it used to be able to prove (e.g., insertTask in https://github.com/epfl-lara/leon/files/383971/Scheduler.txt ), but I've not investigated the issue fully. I've got a deadline on the 15th, but I'll get back to proofs seriously after that! ;)

Thanks :)

ravimad commented 8 years ago

Okay. Just one comment. The instrumentation for rec does create some blow up, but only for functions that need to be instrumented. Run leon with --instrument option it will dump the instrumented code. Check if the function that doesn't verify with Leon now (but did earlier) is blown up by the instrumentation.

epfl-lara / leon

ensuring(rec <= ...) -- big verification time variation #214