epfl-lara / inox Goto Github PK
View Code? Open in Web Editor NEWSolver for higher-order functional programs, used by Stainless
License: Apache License 2.0
Solver for higher-order functional programs, used by Stainless
License: Apache License 2.0
Hello,
Is this an issue? In the tutorial, you say for the size funciton
if_ (ls.isInstOf(T(list)(tp))) {
... /* `1 + size(ls.tail)` */
} else_ {
... /* 0 */
}
But instead of list, shouldn't it be cons?
Especially in the remaining, there is no more reference to the consConstructor or cons anymore.
/* The `E(BigInt(i))` calls correspond to `IntegerLiteral(i)` ASTs. */
if_ (ls.isInstOf(T(list)(tp))) {
/* The recursive call to `size` written `E(size)(tp)(...)` corresponds to
* the AST `FunctionInvocation(size, Seq(tp), Seq(...))`.
* Note that we refer to the symbol `tail` of the `consConstructor`'s second
* field when building the selector AST. */
E(BigInt(1)) + E(size)(tp)(ls.asInstOf(T(list)(tp)).getField(tail))
} else_ {
E(BigInt(0))
}
If this is perfectly valid, can you explain me why and maybe I will update the tutorial to reflect that.
Background: epfl-lara/stainless#432
This problem should be "unsat" (unless I wrote it wrong?), but inox reports "sat"
version: 5a8f96e
backends z3 and cvc4 both trigger the error.
; UNSAT
; the classic "pigeonhole" principle: trying to fit 5 pigeons
; into 4 holes is bound to fail.
(declare-sort hole 0)
(declare-fun h1 () hole)
(declare-fun h2 () hole)
(declare-fun h3 () hole)
(declare-fun h4 () hole)
(declare-fun p1 () hole)
(declare-fun p2 () hole)
(declare-fun p3 () hole)
(declare-fun p4 () hole)
(declare-fun p5 () hole)
(assert
(and
(not (= h1 h2))
(not (= h1 h3))
(not (= h1 h4))
(not (= h2 h3))
(not (= h2 h4))
(not (= h3 h4))
))
(assert
(and
(not (= p1 p2))
(not (= p1 p3))
(not (= p1 p4))
(not (= p1 p5))
(not (= p2 p3))
(not (= p2 p4))
(not (= p2 p5))
(not (= p3 p4))
(not (= p3 p5))
(not (= p4 p5))
))
; map pigeons to holes
(assert
(forall ((p hole)) (or (= p h1) (= p h2) (= p h3) (= p h4))))
(check-sat)
Inox reports a wrong answer on the following problem. The problem is about synthesizing a function f
and an initial accumulator acc
such that List.fold f acc
that can discriminate between some lists.
inox foo.smt2 --checkmodels
[Warning ] - Model leads to runtime error: Forall model check failed
[ Error ] Something went wrong. The model should have been valid, yet we got this: Map() for formula a0 ≠ a1 && ∀x: acc. (x == a0 || x == a1) && ¬¬(fold(acc_init, l0) ≠ fold(acc_init, l1) && fold(acc_init, l2) ≠ fold(acc_init, l3))
[ Info ] => UNKNOWN
; SAT
; distinguish between lists of booleans using only `fold`
; the solver must synthesize a function and an initial accumulator
(declare-datatypes () ((nat (s (select_s_0 nat))
(z))))
(declare-datatypes
()
((list (cons (select_cons_0 Bool) (select_cons_1 list)) (nil))))
(declare-sort acc 0)
(declare-fun acc_init () acc)
(declare-fun f (acc Bool) acc)
; force card(acc) to be 2
(declare-fun a0 () acc)
(declare-fun a1 () acc)
(assert (not (= a0 a1)))
(assert (forall ((x acc)) (or (= x a0) (= x a1))))
(define-fun-rec
fold
((a acc) (l list)) acc
(match l
(case nil a)
(case (cons x tail)
(let ((a2 (f a x)))
(fold a2 tail)))))
(define-fun l0 () list (cons false (cons false (cons true (cons false nil)))))
(define-fun l1 () list (cons false (cons true (cons false (cons false nil)))))
(define-fun l2 () list (cons false (cons false (cons false (cons false (cons true (cons false nil)))))))
(define-fun l3 () list (cons false (cons false (cons false (cons true (cons false (cons false nil)))))))
(assert-not
(not
(and
(not (= (fold acc_init l0) (fold acc_init l1)))
(not (= (fold acc_init l2) (fold acc_init l3)))
)))
(check-sat)
I might have missed something in inox --help
, but is there an option to print the model when the solver states "SAT"?
When I run sbt clean compile
I get the following error, simillar to #97 :
[info] Running (fork) tut.TutMain /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md /home/stevan/Documents/master_project/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md
[error] WARNING: An illegal reflective access operation has occurred
[error] WARNING: Illegal reflective access by z3.Z3Wrapper (file:/home/stevan/Documents/master_project/inox/unmanaged/scalaz3-unix-64-2.12.jar) to field java.lang.ClassLoader.sys_paths
[error] WARNING: Please consider reporting this to the maintainers of z3.Z3Wrapper
[error] WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
[error] WARNING: All illegal access operations will be denied in a future release
[error] null
[error] java.lang.NullPointerException
[error] at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2646)
[error] at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:830)
[error] at java.base/java.lang.System.loadLibrary(System.java:1870)
[error] at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:110)
[error] at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:49)
[error] at inox.solvers.SolverFactory$.liftedTree1$1(SolverFactory.scala:29)
[error] at inox.solvers.SolverFactory$.hasNativeZ3$lzycompute(SolverFactory.scala:28)
[error] at inox.solvers.SolverFactory$.hasNativeZ3(SolverFactory.scala:28)
[error] at inox.solvers.SolverFactory$.$anonfun$fallbacks$1(SolverFactory.scala:78)
[error] at inox.solvers.SolverFactory$.getFromName(SolverFactory.scala:100)
[error] at inox.solvers.SolverFactory$.apply(SolverFactory.scala:356)
[error] at inox.solvers.SolverFactory$.apply(SolverFactory.scala:364)
[error] at inox.package$$anon$1$$anon$2.createSolver(package.scala:76)
[error] at inox.Semantics.$anonfun$getSolver$1(Semantics.scala:31)
[error] at inox.utils.Cache.cached(Caches.scala:14)
[error] at inox.utils.Cache.cached$(Caches.scala:11)
[error] at inox.utils.LruCache.cached(Caches.scala:20)
[error] at inox.Semantics.getSolver(Semantics.scala:31)
[error] at inox.Semantics.getSolver$(Semantics.scala:28)
[error] at inox.package$$anon$1$$anon$2.getSolver(package.scala:65)
[error] at inox.Program.getSolver(Program.scala:60)
[error] at inox.Program.getSolver$(Program.scala:57)
[error] at inox.Program$$anon$1.getSolver(Program.scala:93)
[error] at $line22.$read$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$.<init>(<console>:27)
[error] at $line22.$read$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$.<clinit>(<console>)
[error] at $line22.$eval$.$print$lzycompute(<console>:7)
[error] at $line22.$eval$.$print(<console>:6)
[error] at $line22.$eval.$print(<console>)
[error] at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[error] at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[error] at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[error] at java.base/java.lang.reflect.Method.invoke(Method.java:566)
[error] at scala.tools.nsc.interpreter.IMain$ReadEvalPrint.call(IMain.scala:742)
[error] at scala.tools.nsc.interpreter.IMain$Request.loadAndRun(IMain.scala:1018)
[error] at scala.tools.nsc.interpreter.IMain.$anonfun$interpret$1(IMain.scala:574)
[error] at scala.reflect.internal.util.ScalaClassLoader.asContext(ScalaClassLoader.scala:41)
[error] at scala.reflect.internal.util.ScalaClassLoader.asContext$(ScalaClassLoader.scala:37)
[error] at scala.reflect.internal.util.AbstractFileClassLoader.asContext(AbstractFileClassLoader.scala:41)
[error] at scala.tools.nsc.interpreter.IMain.loadAndRunReq$1(IMain.scala:573)
[error] at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:600)
[error] at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:570)
[error] at tut.Tut$.$anonfun$interp$6(Tut.scala:56)
[error] at tut.felix.IO$Primitive.unsafePerformIO(IO.scala:76)
[error] at tut.felix.IO$Compute.loop$1(IO.scala:117)
[error] at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error] at tut.felix.Syntax$IOOps.$anonfun$withOut$2(Syntax.scala:34)
[error] at scala.util.DynamicVariable.withValue(DynamicVariable.scala:62)
[error] at scala.Console$.withOut(Console.scala:167)
[error] at tut.felix.Syntax$IOOps.$anonfun$withOut$1(Syntax.scala:34)
[error] at tut.felix.IO$Primitive.unsafePerformIO(IO.scala:76)
[error] at tut.felix.IO$Compute.loop$1(IO.scala:121)
[error] at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error] at tut.TutMain$.main(TutMain.scala:8)
[error] at tut.TutMain.main(TutMain.scala)
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:203
[error] java.lang.NullPointerException
[error] at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2646)
[error] at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:830)
[error] at java.base/java.lang.System.loadLibrary(System.java:1870)
[error] at com.microsoft.z3.Native.<clinit>(Native.java:13)
[error] at z3.Z3Wrapper.z3VersionString(Z3Wrapper.java:75)
[error] at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:51)
[error] at inox.solvers.SolverFactory$.liftedTree1$1(SolverFactory.scala:29)
[error] at inox.solvers.SolverFactory$.hasNativeZ3$lzycompute(SolverFactory.scala:28)
[error] at inox.solvers.SolverFactory$.hasNativeZ3(SolverFactory.scala:28)
[error] at inox.solvers.SolverFactory$.$anonfun$fallbacks$1(SolverFactory.scala:78)
[error] at inox.solvers.SolverFactory$.getFromName(SolverFactory.scala:100)
[error] at inox.solvers.SolverFactory$.apply(SolverFactory.scala:356)
[error] at inox.solvers.SolverFactory$.apply(SolverFactory.scala:364)
[error] at inox.package$$anon$1$$anon$2.createSolver(package.scala:76)
[error] at inox.Semantics.$anonfun$getSolver$1(Semantics.scala:31)
[error] at inox.utils.Cache.cached(Caches.scala:14)
[error] at inox.utils.Cache.cached$(Caches.scala:11)
[error] at inox.utils.LruCache.cached(Caches.scala:20)
[error] at inox.Semantics.getSolver(Semantics.scala:31)
[error] at inox.Semantics.getSolver$(Semantics.scala:28)
[error] at inox.package$$anon$1$$anon$2.getSolver(package.scala:65)
[error] at inox.Program.getSolver(Program.scala:60)
[error] at inox.Program.getSolver$(Program.scala:57)
[error] at inox.Program$$anon$1.getSolver(Program.scala:93)
[error] ... 31 elided
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:204
[error] <console>:28: error: not found: value solver
[error] solver.assertCnstr(Not(prop))
[error] ^
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:205
[error] <console>:27: error: not found: value solver
[error] solver.check(SolverResponses.Simple) // Should return `Unsat`
[error] ^
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:206
[error] <console>:27: error: not found: value solver
[error] solver.free()
[error] ^
[error] Exception in thread "main" tut.TutException: Tut execution failed.
[error] at tut.TutMain$.$anonfun$runl$6(TutMain.scala:17)
[error] at tut.felix.IO$Compute.loop$1(IO.scala:121)
[error] at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error] at tut.TutMain$.main(TutMain.scala:8)
[error] at tut.TutMain.main(TutMain.scala)
[error] java.lang.RuntimeException: Nonzero exit code returned from runner: 1
[error] at scala.sys.package$.error(package.scala:26)
[error] at tut.TutPlugin$.$anonfun$tutOne$1(TutPlugin.scala:149)
[error] at scala.util.Success.foreach(Try.scala:249)
[error] at tut.TutPlugin$.tutOne(TutPlugin.scala:149)
[error] at tut.TutPlugin$.$anonfun$tutAll$1(TutPlugin.scala:157)
[error] at scala.collection.immutable.List.flatMap(List.scala:334)
[error] at tut.TutPlugin$.tutAll(TutPlugin.scala:157)
[error] at tut.TutPlugin$.handleUpdate$1(TutPlugin.scala:106)
[error] at tut.TutPlugin$.$anonfun$projectSettings$29(TutPlugin.scala:111)
[error] at sbt.util.FileFunction$.$anonfun$cached$4(FileFunction.scala:147)
[error] at sbt.util.Difference.apply(Tracked.scala:313)
[error] at sbt.util.Difference.apply(Tracked.scala:293)
[error] at sbt.util.FileFunction$.$anonfun$cached$3(FileFunction.scala:143)
[error] at sbt.util.Difference.apply(Tracked.scala:313)
[error] at sbt.util.Difference.apply(Tracked.scala:288)
[error] at sbt.util.FileFunction$.$anonfun$cached$2(FileFunction.scala:142)
[error] at tut.TutPlugin$.$anonfun$projectSettings$25(TutPlugin.scala:111)
[error] at scala.Function1.$anonfun$compose$1(Function1.scala:44)
[error] at sbt.internal.util.$tilde$greater.$anonfun$$u2219$1(TypeFunctions.scala:40)
[error] at sbt.std.Transform$$anon$4.work(System.scala:67)
[error] at sbt.Execute.$anonfun$submit$2(Execute.scala:269)
[error] at sbt.internal.util.ErrorHandling$.wideConvert(ErrorHandling.scala:16)
[error] at sbt.Execute.work(Execute.scala:278)
[error] at sbt.Execute.$anonfun$submit$1(Execute.scala:269)
[error] at sbt.ConcurrentRestrictions$$anon$4.$anonfun$submitValid$1(ConcurrentRestrictions.scala:178)
[error] at sbt.CompletionService$$anon$2.call(CompletionService.scala:37)
[error] at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[error] at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
[error] at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[error] at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[error] at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[error] at java.base/java.lang.Thread.run(Thread.java:834)
[error] (tutQuick) Nonzero exit code returned from runner: 1
[error] Total time: 82 s, completed May 4, 2020, 5:56:43 PM
The readme says Leon still. The content also does not seem any different at 1st glance.
The following program:
package object exError {
def foo(x: Boolean=true): Boolean = x
def bar(): Unit = {
require(foo())
()
}
}
Yields the following error:
[ Error ] bar$0 depends on missing dependencies: foo$default$1$0.
[Internal] Missing some nodes in Registry: foo$default$1$0
[Internal] Please inform the authors of Inox about this message
(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (let ((g f)) (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ g r2))) g) 22) 5))))
(check-sat)
(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ f r2))) f) 22) 5)))
(check-sat)
The first file is reported as SAT (--check-models
invalidates the model) while the second one (where the let g
has been removed) is correctly reported as UNSAT.
The SMT file generated by Inox is:
; Options: -in -smt2
(set-option :produce-unsat-assumptions true)
(declare-fun start!1 () Bool)
(assert start!1)
(declare-fun bs!1 () Bool)
(declare-fun b!8 () Bool)
(assert (= bs!1 (and b!8 start!1)))
(declare-fun lambda!5 () Int)
(declare-fun lambda!4 () Int)
(assert (=> bs!1 (not (= lambda!5 lambda!4))))
(assert (=> b!8 true))
(declare-fun order!1 () Int)
(declare-fun dynLambda!0 (Int Int) Int)
(assert (=> b!8 (< (dynLambda!0 order!1 lambda!4) (dynLambda!0 order!1 lambda!5))))
(declare-fun c!4 () Bool)
(assert (=> start!1 (= c!4 true)))
(declare-fun e!5 () Int)
(declare-fun dynLambda!1 (Int Int) Int)
(assert (=> start!1 (not (= (dynLambda!1 e!5 22) 5))))
(assert (=> b!8 (= e!5 lambda!5)))
(declare-fun b!9 () Bool)
(assert (=> b!9 (= e!5 lambda!4)))
(assert (= (and start!1 c!4) b!8))
(assert (= (and start!1 (not c!4)) b!9))
(declare-fun b_lambda!1 () Bool)
(assert (=> (not b_lambda!1) (not start!1)))
(declare-fun m!1 () Bool)
(assert (=> start!1 m!1))
(check-sat (not b_lambda!1))
(check-sat)
(get-model)
(declare-fun b_lambda!3 () Bool)
(assert (= b_lambda!1 (or start!1 b_lambda!3)))
(declare-fun bs!2 () Bool)
(declare-fun d!1 () Bool)
(assert (= bs!2 (and d!1 start!1)))
(assert (=> bs!2 (= (dynLambda!1 lambda!4 22) 0)))
(assert (=> start!1 d!1))
(check-sat (not b_lambda!3))
(get-model)
The variable b_lambda!3
from the end only appears in the assertion (= b_lambda!1 (or start!1 b_lambda!3))
, and is unconstrained because start!1
must be true
.
Can this be due to #105 (which touched let's
)?
The following code fails, even with the z3 solver.
Basically, I'm solving the equation var === "\n"
but the result is strangely .n.n
import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._
import SolverResponses._
val prog = InoxProgram(
Context.empty.copy(options = Options(Seq(Main.optDebug(Set(solvers.DebugSectionSolver)), optSelectedSolvers(Set("smt-cvc4"))))), Nil, List()
)
val solver = prog.getSolver.getNewSolver
val r = Variable(FreshIdentifier("r"), StringType, Set())
solver.assertCnstr(r === StringLiteral("\n"))
val rValue = solver.check(SolverResponses.Model) match {
case SatWithModel(model) => model.vars(r.toVal : inox.trees.ValDef) match {
case StringLiteral(s) =>s
}
}
assert(rValue == "\n", s"$rValue did not equal \\n")
In a verification condition on the Stainless side, I have a term that contains this:
if (thiss.order.leq(thiss.array((n - 1))._1, elemRef(0)._1)) {
Return[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit]((false, thiss, elemRef))
} else {
Proceed[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit](())
}
After using --debug=tip
, we get a tip file where the type instantiations on Return
and Proceed
are lost, so Inox understands the expression in the tip file as (and this leads to a type error):
if (thiss!108.order!107.leq!6(thiss!108.array!122.arr!2((n!29 - 1))._1!0, elemRef!41.arr!2(0)._1!0)) {
Return!1[tuple3!0[Boolean, SortedArray!5[K!37, T!91], array!118[tuple2!0[K!37, T!91]]], Cur!0](tuple3!1[Boolean, SortedArray!5[K!37, T!91], array!118[tuple2!0[K!37, T!91]]](false, thiss!108, elemRef!41))
} else {
Proceed!1[Ret!0, Unit!1](Unit!3)
}
Can we add the type instantiations (with _
) in Printer.scala
? (If so, what term should I use?) Can Inox parse it back?
Running inox --solvers=
creates a NullPointerException
(with or without a specific solver)
The following Stainless testcase crashes both Inox master and latest release with a key not found
exception. Check the comments for a few variants which do not crash Inox (but yield invalid models).
import stainless.lang._
import stainless.annotation._
object SetMapExternBug {
@extern // Without @extern: OK but invalid model
def map(set: Set[BigInt])(f: BigInt => BigInt): Set[BigInt] = {
(??? : Set[BigInt])
} ensuring { res =>
forall((a: BigInt) => set.contains(a) == res.contains(f(a)))
}
def test(set: Set[BigInt]) = {
require(set == Set[BigInt](1, 2))
// val res = map(set)(x => x) // OK but invalid model
val res = map(map(set)(x => x))(x => x) // CRASH
assert(res == set)
}
}
Here is the TIP for the VC, which when fed to Inox CLI, does not output anything.
(declare-const set!1 (Set Int))
(define-fun map!6 ((set!0 (Set Int)) (f!30 (=> Int Int))) (Set Int) (choose res!36 (Set Int) (forall ((a!6 Int)) (= (member a!6 set!0) (member (@ f!30 a!6) res!36)))))
(assert (not (or (not (= set!1 (insert (as emptyset Int) 1 2))) (= (map!6 (map!6 set!1 (lambda ((x!81 Int)) x!81)) (lambda ((x!82 Int)) x!82)) set!1))))
The error arises here:
inox/src/main/scala/inox/tip/Printer.scala
Line 164 in 7752948
tuples
map is empty.
I guess declareStructuralSort
isn't called on that Tuple
beforehand. The Stainless example (I can minimize and post the example if needed) contains an ADT with two type parameters and an array of pairs inside MyADT[A, B](a: Array[(A, B)], ...)
.
inox foo.smt2 --timeout=30
can happily run for dozens of minutes, where foo.smt2
is a TIP problem.
On the following TIP problem, inox foo.smt2
answers SAT (both using nativez3 and smt-cvc4 as solvers), but the problem is unsatisfiable.
; UNSAT
; find a sorted list of length 3, that is a palindrome, and has sum 1
; this is impossible because the 1 should be in the middle (palindrome),
; but then the list is not sorted anymore
(declare-datatypes () ((nat (s (select_s_0 nat))
(z))))
(define-funs-rec
((plus ((x nat) (y nat)) nat))
((match x (case (s x2) (s (plus x2 y)))
(case z y))))
(define-funs-rec
((mult ((x_1 nat) (y_1 nat)) nat))
((match x_1 (case (s x2_1) (plus y_1 (mult x2_1 y_1)))
(case z z))))
(define-funs-rec
((leq ((x_2 nat) (y_2 nat)) Bool))
((match x_2
(case (s x2_2) (match y_2 (case (s y2) (leq x2_2 y2))
(case z false)))
(case z true))))
(declare-datatypes
()
((list (cons (select_cons_0 nat) (select_cons_1 list))
(nil))))
(define-funs-rec
((append ((x_3 list) (y_3 list)) list))
((match x_3 (case (cons n tail) (cons n (append tail y_3)))
(case nil y_3))))
(define-funs-rec
((rev ((l list)) list))
((match l
(case (cons x_4 xs) (append (rev xs) (cons x_4 nil)))
(case nil nil))))
(define-funs-rec
((length ((l_1 list)) nat))
((match l_1 (case (cons x_5 tail_1) (s (length tail_1)))
(case nil z))))
(define-funs-rec
((sum ((l_2 list)) nat))
((match l_2 (case (cons x_6 tail_2) (plus x_6 (sum tail_2)))
(case nil z))))
(define-funs-rec
((sorted ((l_3 list)) Bool))
((match l_3
(case (cons x_7 l2)
(match l2
(case (cons y_4 l3) (and (leq x_7 y_4) (sorted (cons y_4 l3))))
(case nil true)))
(case nil true))))
(define-funs-rec ((num_3 () nat)) ((s (s (s z)))))
(assert-not
(forall
((l_5 list))
(not (and
(and (and (sorted l_5) (= l_5 (rev l_5))) (= (sum l_5) (s z)))
(= (length l_5) num_3)))))
(check-sat)
Since both Z3 [0] and CVC4 [1] apparently support interpreted conversions between bit vectors and integers (via bv2int
, int2bv
and bv2nat
, nat2bv
respectively), perhaps we could add support for such conversions in Inox, with a fallback for other solvers via recursive conversion procedures implemented as a theory encoder?
I have a PR for ScalaZ3 with a test for such Int<->BigInt conversions at epfl-lara/ScalaZ3#73.
In this PR epfl-lara/stainless#946, I changed the way VCs are generated in the type-checker, and the following file is now valid:
https://github.com/epfl-lara/stainless/blob/965b0ec485e62715003738e73605bd4dbb5da1da/frontends/benchmarks/verification/invalid/Equations1.scala
But I was expecting the second equations to fail, because the makeEqual(x, y)
evidence shouldn't "leak".
I've narrowed the issue to this tip file, on which Inox returns UNSAT
(I've tried z3 and cvc4 1.8).
Surprisingly, removing the assertion on eq2
makes Inox return SAT
. (removing the assertion on eq1
makes Inox return SAT
as well)
(declare-datatypes (A B) ((RAEquations (RaCons (lhs (=> A)) (rhs (=> A)) (ev (=> B))))))
(datatype-invariant (par (A B) this (RAEquations A B) (= (@ (lhs this)) (@ (rhs this)))))
(declare-datatypes () ((Unit (Uu))))
(define-fun makeEqual ((x Int) (y Int)) Unit (choose unused Unit (= x y)))
(declare-const x Int)
(declare-const y Int)
(declare-const eq1 (RAEquations Int Unit))
(declare-const eq2 (RAEquations Int Unit))
(assert (= eq1 (RaCons (lambda () x) (lambda () x) (lambda () (makeEqual x y)))))
(assert (= eq2 (RaCons (lambda () x) (lambda () x) (lambda () Uu))))
(assert (not (= y x)))
(check-sat)
I don't know how to solve this. I don't know why there is a pattern matching error - I checked in the source, and there is nothing but a basic pattern matching on "Implies", which if it failed, should move on to the next one. I'm using inox 1.0.1 for scala 2.11
Can you please help me with that?
scala.MatchError: String (of class inox.ast.Types$ADTType)
[info] at inox.solvers.smtlib.SMTLIBTarget$class.toSMT(SMTLIBTarget.scala:356)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.inox$solvers$smtlib$Z3Target$$super$toSMT(SolverFactory.scala:176)
[info] at inox.solvers.smtlib.Z3Target$class.toSMT(Z3Target.scala:212)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.toSMT(SolverFactory.scala:176)
[info] at inox.solvers.smtlib.SMTLIBTarget$class.toSMT(SMTLIBTarget.scala:354)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.inox$solvers$smtlib$Z3Target$$super$toSMT(SolverFactory.scala:176)
[info] at inox.solvers.smtlib.Z3Target$class.toSMT(Z3Target.scala:212)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.toSMT(SolverFactory.scala:176)
[info] at inox.solvers.smtlib.SMTLIBTarget$$anonfun$toSMT$8.apply(SMTLIBTarget.scala:428)
[info] at inox.solvers.smtlib.SMTLIBTarget$$anonfun$toSMT$8.apply(SMTLIBTarget.scala:428)
Is there any particular reason why SymbolTransformer.transform(FunDef)
and SymbolTransformer.transform(ADTSort)
are marked final
?
It would be nice to be able to override them when defining a new transformer instead of having to define a custom def transformFunction(FunDef)
function within the transformer.
Tests are currently not going through for me on master with Z3 4.6.0 or Z3 4.7.1. With Z3 4.5.0 they're ok. (different error than #57)
[info] - 133: size(x) > 0 is satisfiable solvr=smt-z3 lucky=false check=false assum=true assck=false model=0 *** FAILED *** (27 milliseconds)
[info] inox.package$FatalError: Unexpected error from z3 solver: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (15, 2). Expected: [SymbolLitKind]. Found: OParen
simplifyExpr
on
l match {
case Cons(x, xs) if (x == y) => true
case Cons(x, xs) => false
case _ => true
}
returns
l match {
case Cons(x, xs) if x == y => true
case _ => true
}
On this example:
(define-fun f () Int (choose res Int true))
(define-fun g () Bool (choose res Bool (not (= f 0))))
(assert (not (let ((res g)) (not (= f 0)))))
(check-sat)
I'm opening this issue so that we remember that the isPure
check in
inox/src/main/scala/inox/ast/SymbolOps.scala
Line 1332 in 082081b
After doing some tests, it looks like the problem comes from the fact that
purity is checked by simplifying the whole formula. More precisely, the slowdown
seem to be coming from the simplification of Let's in simplify
(https://github.com/epfl-lara/inox/blob/082081b77e80a0e95696c8649bdfb3d7f25a9d1d/src/main/scala/inox/transformers/SimplifierWithPC.scala lines 295-342).
Following the discussion in epfl-lara/stainless#104:
@jad-hamza:
For the general case with free variables, we could take inspiration from the Coq "simpl" tactic. This tactic simplifies the terms that appear in your goal (or in your premises) by applying reductions rules (beta-reduction, etc.). But it doesn't evaluate blindly, and tries to only apply reductions that make the terms more readable (and to avoid non-termination).For instance, given the definitions in #96, plus(n,m) would not be simplified further (even though there is a valid beta-reduction rule that can be applied), but plus(S(n),m) would be simplified to S(plus(n,m)).
@samarion:
For simplifications of non-ground terms, I also agree with @jad-hamza. Note that Inox actually already does this pretty extensively in SimplifierWithPC. However, no beta-reduction is performed for named functions, so that could be an interesting new simplification to consider. The challenge is to choose good heuristics about when a function inlining can be considered 'useful'. Possibly basing ourselves off the simp tactic could indeed be useful, but I would prefer automatic this as much as possible.
It fails without any error. Something strange is that it sees three modules and their corresponding build modules. And then I just don't have any source directory.
$ cvc4 --version
This is CVC4 version 1.8-prerelease [git master 7988675c]
With CVC4 above, every benchmark I have thrown to Inox has yielded:
Internal solver error in cvc4: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (9, 1). Expected: [OParen]. Found: unsat
I am unable to build latest CVC4 master at the moment, so I only tested with commit 7988675c
.
I wanted to compile inox on windows by using sbt publish-local
. However, I get the following problem:
[info] Compiling 122 Scala sources to C:\...\inox\target\scala-2.11\classes...
[info] Wrote C:\...\inox\target\scala-2.11\inox_2.11-1.0.2-55-g499e6bc.pom
[info] Main Scala API documentation to C:\...\inox\target\scala-2.11\api...
[info] :: delivering :: ch.epfl.lara#inox_2.11;1.0.2-55-g499e6bc :: 1.0.2-55-g499e6bc :: integration :: Thu Apr 06 19:40:27 CEST 2017
[info] delivering ivy file to C:\...\inox\target\scala-2.11\ivy-1.0.2-55-g499e6bc.xml
[error] C:\...\inox\src\main\scala\inox\solvers\z3\NativeZ3Optimizer.scala:8: object Z3Optimizer is not a member of package z3.scala
[error] import z3.scala.{Z3Optimizer => ScalaZ3Optimizer, _}
[error] ^
I looked into the provided JAR file, but the Z3Optimizer class is indeed not present in the windows version of unmanaged/scalaz3-win-64-2.11.jar
, whereas it appears correctly in the unix version of the same file.
What should I do to update this file?
This warning should be fixed and tests added to ensure the feature is acting as expected.
[warn] inox/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala:880: comparing values of types (inox.ast.Identifier, Seq[ModelWrapper.this.model.program.trees.Type]) and inox.ast.Identifier using `==' will always yield false
[warn] def getChoose(id: Identifier): Option[t.Expr] = model.chooses.find(_._1 == id).map(_._2)
When executing stainless on the following program:
package object exError {
sealed abstract class T[A]
case class C_T[A](x: E[A => Boolean]) extends T[A]
sealed abstract class E[A]
case class C_E[A](x: A) extends E[A => Boolean]
}
I get the following error message:
[Internal] Error: Type error: x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })), expected Boolean,
[Internal] found <untyped>
[Internal]
[Internal] Typing explanation:
[Internal] x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal] x is C_T is of type Boolean
[Internal] x is of type T[A]
[Internal] isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal] x.x is of type <untyped>
[Internal] x is of type T[A]
[Internal] (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] x is Function1 is of type <untyped>
[Internal] x is of type Object
[Internal] ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] } is of type <untyped>
[Internal] true is of type Boolean
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal] x$96 is of type A
[Internal] @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal] @unchecked x.value(x$95) is of type <untyped>
[Internal] @unchecked x.value is of type <untyped>
[Internal] x.value is of type <untyped>
[Internal] x is of type Object
[Internal] x$95 is of type Object because isE was instantiated with with type (Object,(Object) => Boolean) => Boolean. Trace:
[Internal] - inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:22)
[Internal] - inox.ast.TypeOps$class.typeCheck(TypeOps.scala:89)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.typeCheck(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedFunction(Definitions.scala:215)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedFunction(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
[Internal] - scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:210)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.stainless$extraction$oo$Definitions$AbstractSymbols$$super$ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:135)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply$mcV$sp(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.utils.Lazy.get(Lazy.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormed(Definitions.scala:206)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormed(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.TypeEncoding$class.extractSymbols(TypeEncoding.scala:1168)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.CachingPhase$class.extract(ExtractionPipeline.scala:91)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extract(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - stainless.extraction.utils.DebugPipeline$class.extract(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anon$1.extract(DebugPipeline.scala:98)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.ComponentRun$class.extract(Component.scala:75)
[Internal] - stainless.verification.VerificationRun.extract(VerificationComponent.scala:37)
[Internal] - stainless.ComponentRun$class.apply(Component.scala:86)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:37)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:174)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - stainless.frontend.StainlessCallBack.processSymbols(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack.apply(StainlessCallBack.scala:59)
[Internal] - stainless.frontends.scalac.StainlessExtraction$Phase.apply(StainlessExtraction.scala:34)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$applyPhase$1.apply$mcV$sp(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase.withCurrentUnit(Global.scala:431)
[Internal] - scala.tools.nsc.Global$GlobalPhase.applyPhase(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.tools.nsc.Global$GlobalPhase.run(Global.scala:398)
[Internal] - scala.tools.nsc.Global$Run.compileUnitsInternal(Global.scala:1501)
[Internal] - scala.tools.nsc.Global$Run.compileUnits(Global.scala:1486)
[Internal] - scala.tools.nsc.Global$Run.compileSources(Global.scala:1481)
[Internal] - scala.tools.nsc.Global$Run.compile(Global.scala:1582)
[Internal] - stainless.frontends.scalac.ScalaCompiler$Factory$$anon$1.onRun(ScalaCompiler.scala:127)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:31)
[Internal] - java.lang.Thread.run(Thread.java:748)
[Internal] Type error: x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })), expected Boolean,
[Internal] found <untyped>
[Internal]
[Internal] Typing explanation:
[Internal] x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal] x is C_T is of type Boolean
[Internal] x is of type T[A]
[Internal] isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal] x.x is of type <untyped>
[Internal] x is of type T[A]
[Internal] (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] x is Function1 && ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] x is Function1 is of type <untyped>
[Internal] x is of type Object
[Internal] ∀x$96: A. (true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] }) is of type <untyped>
[Internal] true ==> {
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean
[Internal] } is of type <untyped>
[Internal] true is of type Boolean
[Internal] val x$95: Object = x$96
[Internal] @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal] x$96 is of type A
[Internal] @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal] @unchecked x.value(x$95) is of type <untyped>
[Internal] @unchecked x.value is of type <untyped>
[Internal] x.value is of type <untyped>
[Internal] x is of type Object
[Internal] x$95 is of type Object because isE was instantiated with with type (Object,(Object) => Boolean) => Boolean
[Internal] Please inform the authors of Inox about this message
Stainless program which calls set.toList inside a lambda errors out with Key not found
error. Inside the example.zip is the example program and the tip and smt session outputs.
[ Info ] - Inferring measure for contains...
[ Info ] => Found measure for contains.
[ Info ] - Inferring measure for forall...
[ Info ] => Found measure for forall.
[ Info ] - Inferring measure for noDuplicates...
[ Info ] => Found measure for noDuplicates.
[ Info ] - Checking cache: 'precond. (call head[T]({ assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[ Info ] Cache miss: 'precond. (call head[T]({ assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[ Info ] - Now solving 'precond. (call head[T]({ assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[Internal] Error: key not found: x$135. Trace:
[Internal] - scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:101)
[Internal] - scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:99)
[Internal] - inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprStructure$12(TemplateGenerator.scala:143)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:97)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:51)
[Internal] - scala.collection.SetLike.map(SetLike.scala:104)
[Internal] - scala.collection.SetLike.map$(SetLike.scala:104)
[Internal] - scala.collection.AbstractSet.map(Set.scala:51)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprStructure(TemplateGenerator.scala:143)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprStructure$(TemplateGenerator.scala:78)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.mkExprStructure(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.LambdaTemplates$LambdaTemplate$.apply(LambdaTemplates.scala:63)
[Internal] - inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:384)
[Internal] - inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprClauses$9(TemplateGenerator.scala:434)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.immutable.List.map(List.scala:298)
[Internal] - inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:434)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprClauses(TemplateGenerator.scala:437)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprClauses$(TemplateGenerator.scala:237)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.mkExprClauses(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.$anonfun$apply$1(FunctionTemplates.scala:49)
[Internal] - scala.collection.MapLike.getOrElse(MapLike.scala:131)
[Internal] - scala.collection.MapLike.getOrElse$(MapLike.scala:129)
[Internal] - scala.collection.AbstractMap.getOrElse(Map.scala:63)
[Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.apply(FunctionTemplates.scala:36)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$38(FunctionTemplates.scala:240)
[Internal] - scala.Option.getOrElse(Option.scala:189)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$11(FunctionTemplates.scala:240)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:97)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$8(FunctionTemplates.scala:163)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$8$adapted(FunctionTemplates.scala:161)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.IterableLike.foreach(IterableLike.scala:74)
[Internal] - scala.collection.IterableLike.foreach$(IterableLike.scala:73)
[Internal] - scala.collection.AbstractIterable.foreach(Iterable.scala:56)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.unroll(FunctionTemplates.scala:161)
[Internal] - inox.solvers.unrolling.Templates.$anonfun$unroll$4(Templates.scala:82)
[Internal] - scala.collection.TraversableLike.$anonfun$flatMap$1(TraversableLike.scala:245)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.flatMap(TraversableLike.scala:245)
[Internal] - scala.collection.TraversableLike.flatMap$(TraversableLike.scala:242)
[Internal] - scala.collection.immutable.List.flatMap(List.scala:355)
[Internal] - inox.solvers.unrolling.Templates.unroll(Templates.scala:82)
[Internal] - inox.solvers.unrolling.Templates.unroll$(Templates.scala:78)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.unroll(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$36(UnrollingSolver.scala:815)
[Internal] - scala.runtime.java8.JFunction1$mcVI$sp.apply(JFunction1$mcVI$sp.java:23)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.immutable.Range.foreach(Range.scala:158)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$33(UnrollingSolver.scala:814)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$2(UnrollingSolver.scala:810)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$1(UnrollingSolver.scala:554)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions(UnrollingSolver.scala:836)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions$(UnrollingSolver.scala:553)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions(TimeoutSolver.scala:47)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions$(TimeoutSolver.scala:39)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.tip.TipDebugger.checkAssumptions(TipDebugger.scala:101)
[Internal] - inox.tip.TipDebugger.checkAssumptions$(TipDebugger.scala:99)
[Internal] - inox.solvers.SolverFactory$$anon$6.checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check$(UnrollingSolver.scala:87)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:200)
[Internal] - inox.solvers.combinators.TimeoutSolver.check(TimeoutSolver.scala:35)
[Internal] - inox.solvers.combinators.TimeoutSolver.check$(TimeoutSolver.scala:28)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:200)
[Internal] - inox.tip.TipDebugger.check(TipDebugger.scala:96)
[Internal] - inox.tip.TipDebugger.check$(TipDebugger.scala:94)
[Internal] - inox.solvers.SolverFactory$$anon$6.check(SolverFactory.scala:200)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVC$2(VerificationChecker.scala:233)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:228)
[Internal] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:214)
[Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:345)
[Internal] - stainless.verification.VerificationCache.$anonfun$checkVC$1(VerificationCache.scala:87)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationCache.checkVC(VerificationCache.scala:52)
[Internal] - stainless.verification.VerificationCache.checkVC$(VerificationCache.scala:42)
[Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:345)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVCs$2(VerificationChecker.scala:107)
[Internal] - scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:850)
[Internal] - scala.collection.TraversableOnce.$anonfun$foldLeft$1(TraversableOnce.scala:160)
[Internal] - scala.collection.TraversableOnce.$anonfun$foldLeft$1$adapted(TraversableOnce.scala:160)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.IterableLike.foreach(IterableLike.scala:74)
[Internal] - scala.collection.IterableLike.foreach$(IterableLike.scala:73)
[Internal] - scala.collection.AbstractIterable.foreach(Iterable.scala:56)
[Internal] - scala.collection.TraversableOnce.foldLeft(TraversableOnce.scala:160)
[Internal] - scala.collection.TraversableOnce.foldLeft$(TraversableOnce.scala:158)
[Internal] - scala.collection.AbstractTraversable.foldLeft(Traversable.scala:108)
[Internal] - scala.concurrent.Future$.traverse(Future.scala:850)
[Internal] - stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:97)
[Internal] - stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:90)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:336)
[Internal] - stainless.verification.VerificationChecker.verify(VerificationChecker.scala:81)
[Internal] - stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:77)
[Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:336)
[Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:350)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:111)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:44)
[Internal] - stainless.ComponentRun.apply(Component.scala:105)
[Internal] - stainless.ComponentRun.apply$(Component.scala:97)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:44)
[Internal] - stainless.ComponentRun.apply(Component.scala:112)
[Internal] - stainless.ComponentRun.apply$(Component.scala:111)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:44)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processFunctionSymbols$3(SplitCallBack.scala:179)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processFunctionSymbols$2(SplitCallBack.scala:179)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.immutable.List.map(List.scala:298)
[Internal] - stainless.frontend.SplitCallBack.processFunctionSymbols(SplitCallBack.scala:178)
[Internal] - stainless.frontend.SplitCallBack.processFunction(SplitCallBack.scala:154)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3(SplitCallBack.scala:138)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3$adapted(SplitCallBack.scala:137)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:137)
[Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:67)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:38)
[Internal] - java.base/java.lang.Thread.run(Thread.java:834)
This is an issue eg. in epfl-lara/stainless#274 (comment).
With --feeling-lucky
and --check-models
on, this test fails because Inox reports an invalid (unlucky) model:
> stainless-scalac/run --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala
[info] Running stainless.Main --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala
[info] [Warning ] Parallelism is disabled.
[info] [ Info ] - Now solving 'body assertion' VC for test @43:5...
[info] [ Info ] - Result for 'body assertion' VC for test @43:5:
[info] [ Info ] => VALID
[info] [ Info ] - Now solving 'body assertion' VC for test @44:5...
[info] [ Error ] Something went wrong. The model should have been valid, yet we got this:
[info] [ Error ] res: TrieMapWrapper[BigInt, BigInt] -> TrieMapWrapper[BigInt, BigInt](0)
[info] [ Error ]
[info] [ Error ] contains[BigInt,BigInt](thiss: TrieMapWrapper[K, V], k: K) -> if (thiss == TrieMapWrapper[BigInt, BigInt](0) && k == 1) {
[info] [ Error ] false
[info] [ Error ] } else {
[info] [ Error ] choose((res$226: Boolean) => true)
[info] [ Error ] }
[info] [ Error ] for formula ∀k: BigInt. ¬contains[BigInt, BigInt](res, k)
[info] [ Info ] - Result for 'body assertion' VC for test @44:5:
[info] [ Info ] => VALID
[info] [ Info ] ┌───────────────────┐
[info] [ Info ] ╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════════════════╗
[info] [ Info ] ║ └───────────────────┘ ║
[info] [ Info ] ║ test body assertion valid nativez3 ../benchmarks/verification/valid/IgnoredField.scala:43:5 0.179 ║
[info] [ Info ] ║ test body assertion valid nativez3 ../benchmarks/verification/valid/IgnoredField.scala:44:5 0.218 ║
[info] [ Info ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[info] [ Info ] ║ total: 2 valid: 2 (0 from cache) invalid: 0 unknown: 0 time: 0.397 ║
[info] [ Info ] ╚════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[info] [ Info ] Shutting down executor service.
[success] Total time: 6 s, completed Aug 15, 2018 1:09:36 PM
I have tried without success so far to prevent Inox from reporting invalid lucky models, perhaps you could give it a look yourself? A simple test for that is to run stainless in my ignore-field
branch with stainless-scalac/run --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala
, and check that no invalid model is reported.
2.13 has been released a few days ago.
To reproduce this problem, use the following self-contained script in a console having inox:
import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._
val prog = InoxProgram(
Context.empty.copy(options = Options(Seq(Main.optDebug(Set(solvers.DebugSectionSolver)), optSelectedSolvers(Set("smt-cvc4"))))), Nil, List()
)
val solver = prog.getSolver.getNewSolver
implicit class StringVars(sc: StringContext) {
def l() = StringLiteral(sc.parts.mkString(""))
}
implicit class Cct(s: Expr) {
def +&(other: Expr) = StringConcat(s, other)
}
val f4 = Variable(FreshIdentifier("f4"), FunctionType(Seq(StringType), StringType), Set())
val cstr = f4 === \("x"::StringType)(x => x +& l" ?")
solver.assertCnstr(cstr)
solver.check(SolverResponses.Model)
Although the formula is trivial, the result is unexpected:
java.lang.ClassCastException: inox.ast.Types$StringType$ cannot be cast to inox.ast.Types$ADTType
at inox.ast.TreeDeconstructor$$anonfun$deconstruct$50.apply(Extractors.scala:126)
at inox.ast.TreeDeconstructor$$anonfun$deconstruct$50.apply(Extractors.scala:126)
at inox.ast.TreeTransformer$class.transform(TreeOps.scala:145)
at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:102)
at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:133)
at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:132)
at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
at scala.collection.immutable.List.foreach(List.scala:381)
at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
at scala.collection.immutable.List.map(List.scala:285)
at inox.ast.TreeTransformer$class.transform(TreeOps.scala:132)
at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:102)
at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:238)
at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:257)
at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:238)
at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:257)
at inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
at inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
at inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:64)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.decode(SolverFactory.scala:248)
at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:540)
at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:540)
at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:178)
at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:178)
at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
at scala.collection.immutable.Map$Map3.foreach(Map.scala:161)
at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
at scala.collection.AbstractTraversable.map(Traversable.scala:104)
at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:178)
at inox.solvers.unrolling.UnrollingSolver$ModelWrapper.getModel(UnrollingSolver.scala:848)
at inox.solvers.unrolling.AbstractUnrollingSolver$class.extractTotalModel(UnrollingSolver.scala:540)
at inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:667)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:248)
at inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:248)
at inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:62)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.checkAssumptions(SolverFactory.scala:248)
at inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:87)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:248)
at inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:248)
at inox.tip.TipDebugger$class.check(TipDebugger.scala:57)
at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.check(SolverFactory.scala:248)
The error is the same if I use z3 instead of CVC4.
cc: @samuelchassot
We found an example where the code simplification becomes very slow, probably due to a code explosion in mergeCalls
:
// before mergeFunctions: 339 lines of code
// after liftCalls: 649 lines of code
// after mergeCalls: 30341 lines of code
Can be reproduced with the Stainless code below and the command:
stainless --watch File.scala --debug=solver,verification --functions=problem
import stainless.annotation._
import stainless.collection._
import stainless.equations._
import stainless.lang._
import stainless.proof.check
import scala.annotation.tailrec
import scala.collection.immutable
object MutableLongMap {
private final val IndexMask: Int = 0x07ffffff // = Integer.MAX_VALUE/8
private final val MissingBit = 0x80000000
private final val VacantBit = 0x40000000
private final val MissVacant = 0xc0000000
private final val EntryNotFound = 0x20000000
private final val MAX_ITER = 2048 // arbitrary
@mutable
case class LongMapLongV(
var mask: Int = IndexMask,
var extraKeys: Int = 0,
var zeroValue: Long = 0,
var minValue: Long = 0,
var _size: Int = 0,
var _keys: Array[Long] = Array.fill(IndexMask + 1)(0),
var _values: Array[Long] = Array.fill(IndexMask + 1)(0),
val defaultEntry: Long => Long = (x => 0),
var repackingKeyCount: Int = 0
) {
@inline
def valid: Boolean = {
mask == IndexMask &&
_values.length == mask + 1 &&
_keys.length == _values.length &&
mask >= 0 &&
_size >= 0 &&
_size < mask + 1 &&
size >= _size &&
extraKeys >= 0 &&
extraKeys <= 3 &&
arrayCountValidKeysTailRec(_keys, 0, _keys.length) == _size
}
@inline
def inRange(i: Int): Boolean = {
i >= 0 && i < mask + 1
}
@inline
def validKeyIndex(k: Long, i: Int): Boolean = {
require(valid)
if (inRange(i)) _keys(i) == k else false
}
@inline
def validZeroKeyIndex(i: Int): Boolean = {
require(valid && inRange(i))
inRange(i) && _keys(i) == 0
}
def size: Int = {
_size + (extraKeys + 1) / 2
}
def isEmpty: Boolean = {
require(valid)
_size == 0
}.ensuring(_ => valid)
private def toIndex(k: Long): Int = {
require(valid)
val h = ((k ^ (k >>> 32)) & 0xffffffffL).toInt
val x = (h ^ (h >>> 16)) * 0x85ebca6b
(x ^ (x >>> 13)) & mask
}.ensuring(res => valid && res < _keys.length)
@inline
def getCurrentListMap(from: Int): ListMapLongKey[Long] = {
require(valid && from >= 0 && from <= _keys.length)
val res = if ((extraKeys & 1) != 0 && (extraKeys & 2) != 0) {
(getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)) + (Long.MinValue, minValue)
} else if ((extraKeys & 1) != 0 && (extraKeys & 2) == 0) {
getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)
} else if ((extraKeys & 2) != 0 && (extraKeys & 1) == 0) {
getCurrentListMapNoExtraKeys(from) + (Long.MinValue, minValue)
} else {
getCurrentListMapNoExtraKeys(from)
}
if (from < _keys.length && validKeyInArray(_keys(from))) {
ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
}
res
}.ensuring(res =>
valid &&
(if (from < _keys.length && validKeyInArray(_keys(from))) res.contains(_keys(from)) && res(_keys(from)) == _values(from) else true) &&
(if ((extraKeys & 1) != 0) res.contains(0) && res(0) == zeroValue else !res.contains(0)) &&
(if ((extraKeys & 2) != 0) res.contains(Long.MinValue) && res(Long.MinValue) == minValue else !res.contains(Long.MinValue))
)
def getCurrentListMapNoExtraKeys(from: Int): ListMapLongKey[Long] = {
require(valid && from >= 0 && from <= _keys.length)
decreases(_keys.length + 1 -from)
if (from >= _keys.length) {
ListMapLongKey.empty[Long]
} else if (validKeyInArray(_keys(from))) {
ListMapLongKeyLemmas.addStillNotContains(getCurrentListMapNoExtraKeys(from + 1), _keys(from), _values(from), 0)
getCurrentListMapNoExtraKeys(from + 1) + (_keys(from), _values(from))
} else {
getCurrentListMapNoExtraKeys(from + 1)
}
}.ensuring(res => valid &&
!res.contains(0) && !res.contains(Long.MinValue) &&
(if (from < _keys.length && validKeyInArray(_keys(from)))
res.contains(_keys(from)) && res(_keys(from)) == _values(from)
else if (from < _keys.length) res == getCurrentListMapNoExtraKeys(from + 1)
else res.isEmpty)
)
@pure
def problem(): Unit = {
require(valid)
val from = 0
val res = getCurrentListMap(from)
}.ensuring(_ => valid && (if ((extraKeys & 1) != 0) getCurrentListMap(0).contains(0) else !getCurrentListMap(0).contains(0)))
}
@extern
def assume(b: Boolean): Unit = {}.ensuring(_ => b)
@inline
def validKeyInArray(l: Long): Boolean = {
l != 0 && l != Long.MinValue
}
@tailrec
@pure
def arrayCountValidKeysTailRec(
a: Array[Long],
from: Int,
to: Int
): Int = {
require(
from <= to && from >= 0 && to <= a.length && a.length < Integer.MAX_VALUE
)
decreases(a.length-from)
if (from >= to) {
0
} else {
if (validKeyInArray(a(from))) {
1 + arrayCountValidKeysTailRec(a, from + 1, to)
} else {
arrayCountValidKeysTailRec(a, from + 1, to)
}
}
}.ensuring(res => res >= 0 && res <= a.length - from)
}
case class ListMapLongKey[B](toList: List[(Long, B)]) {
require(TupleListOps.isStrictlySorted(toList))
@inline
def isEmpty: Boolean = toList.isEmpty
@inline
def head: (Long, B) = {
require(!isEmpty)
toList.head
}
@inline
def tail: ListMapLongKey[B] = {
require(!isEmpty)
ListMapLongKey(toList.tail)
}
@inlineOnce @extern
def contains(key: Long): Boolean = {
TupleListOps.containsKey(toList, key)
}.ensuring(res => !res || this.get(key).isDefined)
@inline
def get(key: Long): Option[B] = {
TupleListOps.getValueByKey(toList, key)
}
@inline
def keysOf(value: B): List[Long] = {
TupleListOps.getKeysOf(toList, value)
}
@inline
def apply(key: Long): B = {
require(contains(key))
get(key).get
}
@inline
def +(keyValue: (Long, B)): ListMapLongKey[B] = {
val newList = TupleListOps.insertStrictlySorted(toList, keyValue._1, keyValue._2)
ListMapLongKey(newList)
}.ensuring(res => res.contains(keyValue._1) && res.get(keyValue._1) == Some(keyValue._2))
// @inlineOnce
def ++(keyValues: List[(Long, B)]): ListMapLongKey[B] = {
decreases(keyValues)
keyValues match {
case Nil() => this
case Cons(keyValue, rest) => (this + keyValue) ++ rest
}
}
// @inlineOnce
def -(key: Long): ListMapLongKey[B] = {
ListMapLongKey(TupleListOps.removeStrictlySorted(toList, key))
}.ensuring(res => !res.contains(key))
// @inlineOnce
def --(keys: List[Long]): ListMapLongKey[B] = {
decreases(keys)
keys match {
case Nil() => this
case Cons(key, rest) => (this - key) -- rest
}
}
@inline
def forall(p: ((Long, B)) => Boolean): Boolean = {
toList.forall(p)
}
}
object TupleListOps {
@inline
def invariantList[B](l: List[(Long, B)]): Boolean = {
isStrictlySorted(l)
}
@extern
def getKeysOf[B](l: List[(Long, B)], value: B): List[Long] = {
require(invariantList(l))
decreases(l)
l match {
case head :: tl if (head._2 == value) => {
head._1 :: getKeysOf(tl, value)
}
case head :: tl if (head._2 != value) => {
val r = getKeysOf(tl, value)
getKeysOf(tl, value)
}
case Nil() => Nil[Long]()
}
}.ensuring(res => res.forall(getValueByKey(l, _) == Some(value)))
def getValueByKey[B](l: List[(Long, B)], key: Long): Option[B] = {
require(invariantList(l))
decreases(l)
l match {
case head :: tl if (head._1 == key) => Some(head._2)
case head :: tl if (head._1 != key) => getValueByKey(tl, key)
case Nil() => None[B]
}
}
def insertStrictlySorted[B](l: List[(Long, B)], newKey: Long, newValue: B): List[(Long, B)] = {
require(invariantList(l))
decreases(l)
l match {
case head :: tl if (head._1 < newKey) => head :: insertStrictlySorted(tl, newKey, newValue)
case head :: tl if (head._1 == newKey) => (newKey, newValue) :: tl
case head :: tl if (head._1 > newKey) => (newKey, newValue) :: head :: tl
case Nil() => (newKey, newValue) :: Nil()
}
}.ensuring(res => invariantList(res) && containsKey(res, newKey) && res.contains((newKey, newValue)))
def removeStrictlySorted[B](l: List[(Long, B)], key: Long): List[(Long, B)] = {
require(invariantList(l))
decreases(l)
l match {
case head :: tl if (head._1 == key) => tl
case head :: tl if (head._1 != key) => head :: removeStrictlySorted(tl, key)
case Nil() => Nil[(Long, B)]()
}
}.ensuring(res => invariantList(res) && !containsKey(res, key))
def isStrictlySorted[B](l: List[(Long, B)]): Boolean = {
decreases(l)
l match {
case Nil() => true
case Cons(_, Nil()) => true
case Cons(h1, Cons(h2, _)) if (h1._1 >= h2._1) => false
case Cons(_, t) => isStrictlySorted(t)
}
}
def containsKey[B](l: List[(Long, B)], key: Long): Boolean = {
require(invariantList(l))
decreases(l)
l match {
case head :: tl if(head._1 == key) => true
case head :: tl if(head._1 > key) => false
case head :: tl if(head._1 < key) => containsKey(tl, key)
case Nil() => false
}
}
}
object ListMapLongKey {
def empty[B]: ListMapLongKey[B] = ListMapLongKey[B](List.empty[(Long, B)])
}
object ListMapLongKeyLemmas {
import ListSpecs._
@opaque
def addValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long, b: B): Unit = {
require(lm.forall(p) && p(a, b))
decreases(lm.toList.size)
if (!lm.isEmpty)
addValidProp(lm.tail, p, a, b)
}.ensuring { _ =>
val nlm = lm + (a, b)
nlm.forall(p)
}
@opaque
def removeValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long): Unit = {
require(lm.forall(p))
decreases(lm.toList.size)
if (!lm.isEmpty)
removeValidProp(lm.tail, p, a)
}.ensuring { _ =>
val nlm = lm - a
nlm.forall(p)
}
@opaque
def insertAllValidProp[B](lm: ListMapLongKey[B], kvs: List[(Long, B)], p: ((Long, B)) => Boolean): Unit = {
require(lm.forall(p) && kvs.forall(p))
decreases(kvs)
if (!kvs.isEmpty) {
addValidProp(lm, p, kvs.head._1, kvs.head._2)
insertAllValidProp(lm + kvs.head, kvs.tail, p)
}
}.ensuring { _ =>
val nlm = lm ++ kvs
nlm.forall(p)
}
@opaque
def removeAllValidProp[B](lm: ListMapLongKey[B], l: List[Long], p: ((Long, B)) => Boolean): Unit = {
require(lm.forall(p))
decreases(l)
if (!l.isEmpty) {
removeValidProp(lm, p, l.head)
removeAllValidProp(lm - l.head, l.tail, p)
}
}.ensuring { _ =>
val nlm = lm -- l
nlm.forall(p)
}
@opaque @extern
def addApplyDifferent[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
require(lm.contains(a0) && a0 != a)
}.ensuring(_ => (lm + (a -> b))(a0) == lm(a0))
@opaque @extern
def addStillContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
require(lm.contains(a0))
}.ensuring(_ => (lm + (a, b)).contains(a0))
@opaque @extern
def addStillNotContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
require(!lm.contains(a0) && a != a0)
}.ensuring(_ => !(lm + (a, b)).contains(a0))
@opaque
def applyForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
require(lm.forall(p) && lm.contains(k))
decreases(lm.toList.size)
if (!lm.isEmpty && lm.toList.head._1 != k)
applyForall(lm.tail, p, k)
}.ensuring(_ => p(k, lm(k)))
@opaque
def getForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
require(lm.forall(p))
decreases(lm.toList.size)
if (!lm.isEmpty && lm.toList.head._1 != k)
getForall(lm.tail, p, k)
}.ensuring(_ => lm.get(k).forall(v => p(k, v)))
@opaque
def uniqueImage[B](lm: ListMapLongKey[B], a: Long, b: B): Unit = {
require(lm.toList.contains((a, b)))
}.ensuring(_ => lm.get(a) == Some[B](b))
@opaque
def keysOfSound[B](lm: ListMapLongKey[B], value: B): Unit = {
}.ensuring(_ => lm.keysOf(value).forall(key => lm.get(key) == Some[B](value)))
}
¬(thiss.mask ≠ IndexMask || thiss._values.size ≠ thiss.mask + 1 || thiss._keys.size ≠ thiss._values.size || thiss.mask < 0 || thiss._size < 0 || thiss._size >= thiss.mask + 1 || size(thiss) < thiss._size || thiss.extraKeys < 0 || thiss.extraKeys > 3 || arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) ≠ thiss._size || from ≠ 0 || res ≠ {
val cond: Boolean = (thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0) && from <= thiss._keys.size
val res: ListMapLongKey[Long] = {
val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
val inlined: ListMapLongKey[Long] = {
val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
assume({
val res: Boolean = choose((empty$140: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
res
} && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
ListMapLongKey[Long](newList)
}
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$141: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
assume({
val res: Boolean = choose((empty$142: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
res
} else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$143: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else {
getCurrentListMapNoExtraKeys(thiss, from)
}
val t: Unit = if (from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) {
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
} else {
()
}
t
}
assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) || {
val res: Boolean = choose((empty$144: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
res
} && {
val key: Long = thiss._keys.arr(from)
val cond: Boolean = {
val res: Boolean = choose((empty$145: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
{
val res: Boolean = choose((empty$146: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
res
} && {
val key: Long = 0
val cond: Boolean = {
val res: Boolean = choose((empty$147: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.zeroValue
} else {
val res: Boolean = choose((empty$148: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
res
}
})) && (if ((thiss.extraKeys & 2) ≠ 0) {
{
val res: Boolean = choose((empty$149: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
} && {
val key: Long = -9223372036854775808
val cond: Boolean = {
val res: Boolean = choose((empty$150: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.minValue
} else {
val res: Boolean = choose((empty$151: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
}
}))
res
} || x$2 ≠ () || thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (if ((thiss.extraKeys & 1) ≠ 0) {
val from: Int = 0
val inlined: ListMapLongKey[Long] = {
val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
val res: ListMapLongKey[Long] = {
val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 2) ≠ 0) {
val inlined: ListMapLongKey[Long] = {
val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
assume({
val res: Boolean = choose((empty$152: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
res
} && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
ListMapLongKey[Long](newList)
}
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$153: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else if ((thiss.extraKeys & 2) == 0) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
assume({
val res: Boolean = choose((empty$154: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
res
} else if (false) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$155: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else {
getCurrentListMapNoExtraKeys(thiss, from)
}
val t: Unit = if (from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) {
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
} else {
()
}
t
}
assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) || {
val res: Boolean = choose((empty$156: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
res
} && {
val key: Long = thiss._keys.arr(from)
val cond: Boolean = {
val res: Boolean = choose((empty$157: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss._values.arr(from))) && {
val res: Boolean = choose((empty$158: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
res
} && {
val key: Long = 0
val cond: Boolean = {
val res: Boolean = choose((empty$159: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.zeroValue) && (if ((thiss.extraKeys & 2) ≠ 0) {
{
val res: Boolean = choose((empty$160: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
} && {
val key: Long = -9223372036854775808
val cond: Boolean = {
val res: Boolean = choose((empty$161: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.minValue
} else {
val res: Boolean = choose((empty$162: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
}
}))
res
}
val res: Boolean = choose((empty$163: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
res
} else {
val from: Int = 0
val inlined: ListMapLongKey[Long] = {
val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
val res: ListMapLongKey[Long] = {
val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
val inlined: ListMapLongKey[Long] = {
val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
assume({
val res: Boolean = choose((empty$164: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
res
} && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
ListMapLongKey[Long](newList)
}
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$165: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
assume({
val res: Boolean = choose((empty$166: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
res
} else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
assume({
val res: Boolean = choose((empty$167: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
res
} && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
res
} else {
getCurrentListMapNoExtraKeys(thiss, from)
}
val t: Unit = if (from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) {
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
} else {
()
}
t
}
assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
val l: Long = thiss._keys.arr(from)
l ≠ 0.toLong && l ≠ -9223372036854775808
}) || {
val res: Boolean = choose((empty$168: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
res
} && {
val key: Long = thiss._keys.arr(from)
val cond: Boolean = {
val res: Boolean = choose((empty$169: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
{
val res: Boolean = choose((empty$170: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
res
} && {
val key: Long = 0
val cond: Boolean = {
val res: Boolean = choose((empty$171: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.zeroValue
} else {
val res: Boolean = choose((empty$172: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
res
}
})) && (if ((thiss.extraKeys & 2) ≠ 0) {
{
val res: Boolean = choose((empty$173: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
} && {
val key: Long = -9223372036854775808
val cond: Boolean = {
val res: Boolean = choose((empty$174: Boolean) => true)
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
res
}
get[Long](getValueByKey[Long](res.toList, key))
} == thiss.minValue
} else {
val res: Boolean = choose((empty$175: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
res
}
}))
res
}
val res: Boolean = choose((empty$176: Boolean) => true)
¬{
assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
res
}
}))
Inox consistently finishes in 1 or 2 seconds for inox fast.tip
(the VC is false and Inox finds a counter-example), but may timeout 5 minutes for inox slow.tip
, or sometimes finish in ~20 sec. For context, fast.tip
was generated by a standard command-line call of Stainless, while slow.tip
was generated by going through the ComponentTestSuite
.
Some notable differences: fast.tip
doesn't refer to Mapping
, and the ContractInterface
datatype declaration is much shorter in fast.tip
fast.tip
(declare-datatypes () ((State!3 (Default!2) (Default1!2) (Default2!2) (Default3!2) (Finished!2) (WaitingForData!2) (WaitingForLender!2) (WaitingForPayback!2))))
(declare-datatypes (T!12) ((List!3 (Cons!2 (h!47 T!12) (t!57 (List!3 T!12))) (Nil!2))))
(declare-datatypes () ((Address!2 (Address!3 (id!4 Int)))))
(declare-datatypes () ((ContractInterface!1 (ERC20Token!2 (s!19 Int)) (LoanContract!2 (borrower!2 Address!2) (wantedAmount!2 (_ BitVec 256)) (premiumAmount!2 (_ BitVec 256)) (tokenAmount!2 (_ BitVec 256)) (tokenName!2 String) (tokenContractAddress!2 ContractInterface!1) (daysToLend!2 (_ BitVec 256)) (currentState!2 State!3) (start!3 (_ BitVec 256)) (lender!2 Address!2) (visitedStates!2 (List!3 State!3))) (Open!2 (x!99 Int)) (Open!3 (x!100 Int)))))
(declare-const thiss!28 ContractInterface!1)
(define-fun (par (T!42) (isEmpty!1 ((thiss!29 (List!3 T!42))) Bool (ite (is-Nil!2 thiss!29) true false))))
(define-fun-rec (par (T!40) (isPrefix!0 ((l1!12 (List!3 T!40)) (l2!10 (List!3 T!40))) Bool (ite (is-Nil!2 l1!12) true (ite (and (is-Cons!2 l1!12) (is-Cons!2 l2!10) (= (h!47 l1!12) (h!47 l2!10))) (isPrefix!0 (t!57 l1!12) (t!57 l2!10)) false)))))
(define-fun-rec (par (T!44) (size!1 ((thiss!31 (List!3 T!44))) Int (let ((x$1!4 (ite (is-Nil!2 thiss!31) 0 (+ 1 (size!1 (t!57 thiss!31)))))) (assume (>= x$1!4 0) x$1!4)))))
(define-fun-rec (par (T!45) (content!4 ((thiss!32 (List!3 T!45))) (Set T!45) (ite (is-Nil!2 thiss!32) (as emptyset T!45) (union (insert (as emptyset T!45) (h!47 thiss!32)) (content!4 (t!57 thiss!32)))))))
(define-fun-rec (par (T!46) (|:+!0| ((thiss!33 (List!3 T!46)) (t!7 T!46)) (List!3 T!46) (let ((res!8 (ite (is-Nil!2 thiss!33) (Cons!2 t!7 thiss!33) (Cons!2 (h!47 thiss!33) (|:+!0| (t!57 thiss!33) t!7))))) (assume (assume (is-Cons!2 res!8) (and (= (size!1 res!8) (+ (size!1 thiss!33) 1)) (= (content!4 res!8) (union (content!4 thiss!33) (insert (as emptyset T!46) t!7))))) res!8)))))
(define-fun-rec (par (T!43) (reverse!0 ((thiss!30 (List!3 T!43))) (List!3 T!43) (let ((res!9 (ite (is-Nil!2 thiss!30) thiss!30 (|:+!0| (reverse!0 (t!57 thiss!30)) (h!47 thiss!30))))) (assume (and (= (size!1 res!9) (size!1 thiss!30)) (= (content!4 res!9) (content!4 thiss!30))) res!9)))))
(define-fun expected!0 () (List!3 State!3) (Cons!2 (let ((v!70 WaitingForData!2)) (assume (is-WaitingForData!2 v!70) v!70)) (Cons!2 (let ((v!71 WaitingForLender!2)) (assume (is-WaitingForLender!2 v!71) v!71)) (as Nil!2 (List!3 State!3)))))
(datatype-invariant thiss!16 ContractInterface!1 (=> (is-LoanContract!2 thiss!16) (is-ERC20Token!2 (tokenContractAddress!2 thiss!16))))
(assert (not (=> (and (is-LoanContract!2 thiss!28) (not (isEmpty!1 (visitedStates!2 thiss!28)))) (not (isPrefix!0 (reverse!0 (visitedStates!2 thiss!28)) expected!0)))))
(check-sat)
; check-assumptions required here, but not part of tip standard
slow.tip
(declare-datatypes () ((Address!3 (Address!4 (id!10 Int)))))
(declare-datatypes (A!47 B!33) ((Mapping!5 (Mapping!6 (underlying!12 (=> A!47 B!33))))))
(declare-datatypes (T!10) ((List!8 (Cons!5 (h!94 T!10) (t!111 (List!8 T!10))) (Nil!5))))
(declare-datatypes () ((State!5 (Default!2) (Default1!2) (Default2!2) (Default3!2) (Finished!2) (WaitingForData!2) (WaitingForLender!2) (WaitingForPayback!2))))
(declare-datatypes () ((ContractInterface!2 (BasicContract1!3 (other!6 Address!3)) (BasicInterface1!3) (CallWithEther1!3 (other!7 ContractInterface!2)) (DuplicateIdentifier1!3 (i!35 (_ BitVec 256))) (DuplicateIdentifier2!3 (i!36 (_ BitVec 256))) (DynRequire1!3) (ERC20Token!2 (s!24 Int)) (EtherTransfer1!3 (other!8 Address!3)) (LoanContract!2 (borrower!2 Address!3) (wantedAmount!2 (_ BitVec 256)) (premiumAmount!2 (_ BitVec 256)) (tokenAmount!2 (_ BitVec 256)) (tokenName!2 String) (tokenContractAddress!2 ContractInterface!2) (daysToLend!2 (_ BitVec 256)) (currentState!2 State!5) (start!4 (_ BitVec 256)) (lender!2 Address!3) (visitedStates!2 (List!8 State!5))) (MappingType1!3 (m!4 (Mapping!5 Address!3 (_ BitVec 256)))) (MappingType2!3 (m!5 (Mapping!5 Address!3 (Mapping!5 Address!3 (_ BitVec 256))))) (Open!3 (x!179 Int)) (Open!4 (x!180 Int)) (Open!5 (x!181 Int)) (PositiveUint!3) (VotingToken!3 (rewardToken!2 ContractInterface!2) (opened!2 Bool) (closed!2 Bool) (votingAddresses!2 (List!8 Address!3)) (numberOrAlternatives!2 (_ BitVec 256)) (owner!2 Address!3) (name!2 String) (symbol!2 String) (decimals!2 (_ BitVec 8)) (totalSupply!5 (_ BitVec 256)) (balances!8 (Mapping!5 Address!3 (_ BitVec 256))) (allowed!2 (Mapping!5 Address!3 (Mapping!5 Address!3 (_ BitVec 256)))) (participants!7 (List!8 Address!3))))))
(declare-const thiss!5 ContractInterface!2)
(define-fun (par (T!82) (isEmpty!1 ((thiss!31 (List!8 T!82))) Bool (ite (is-Nil!5 thiss!31) true false))))
(define-fun-rec (par (T!38) (isPrefix!0 ((l1!12 (List!8 T!38)) (l2!10 (List!8 T!38))) Bool (ite (is-Nil!5 l1!12) true (ite (and (is-Cons!5 l1!12) (is-Cons!5 l2!10) (= (h!94 l1!12) (h!94 l2!10))) (isPrefix!0 (t!111 l1!12) (t!111 l2!10)) false)))))
(define-fun-rec (par (T!85) (size!0 ((thiss!34 (List!8 T!85))) Int (let ((x$1!4 (ite (is-Nil!5 thiss!34) 0 (+ 1 (size!0 (t!111 thiss!34)))))) (assume (>= x$1!4 0) x$1!4)))))
(define-fun-rec (par (T!83) (content!4 ((thiss!32 (List!8 T!83))) (Set T!83) (ite (is-Nil!5 thiss!32) (as emptyset T!83) (union (insert (as emptyset T!83) (h!94 thiss!32)) (content!4 (t!111 thiss!32)))))))
(define-fun-rec (par (T!84) (|:+!0| ((thiss!33 (List!8 T!84)) (t!7 T!84)) (List!8 T!84) (let ((res!5 (ite (is-Nil!5 thiss!33) (Cons!5 t!7 thiss!33) (Cons!5 (h!94 thiss!33) (|:+!0| (t!111 thiss!33) t!7))))) (assume (assume (is-Cons!5 res!5) (and (= (size!0 res!5) (+ (size!0 thiss!33) 1)) (= (content!4 res!5) (union (content!4 thiss!33) (insert (as emptyset T!84) t!7))))) res!5)))))
(define-fun-rec (par (T!86) (reverse!0 ((thiss!35 (List!8 T!86))) (List!8 T!86) (let ((res!6 (ite (is-Nil!5 thiss!35) thiss!35 (|:+!0| (reverse!0 (t!111 thiss!35)) (h!94 thiss!35))))) (assume (and (= (size!0 res!6) (size!0 thiss!35)) (= (content!4 res!6) (content!4 thiss!35))) res!6)))))
(define-fun expected!0 () (List!8 State!5) (Cons!5 (let ((v!101 WaitingForData!2)) (assume (is-WaitingForData!2 v!101) v!101)) (Cons!5 (let ((v!102 WaitingForLender!2)) (assume (is-WaitingForLender!2 v!102) v!102)) (as Nil!5 (List!8 State!5)))))
(datatype-invariant thiss!41 ContractInterface!2 (and (=> (is-CallWithEther1!3 thiss!41) (is-CallWithEther1!3 (other!7 thiss!41))) (=> (is-LoanContract!2 thiss!41) (is-ERC20Token!2 (tokenContractAddress!2 thiss!41))) (=> (is-VotingToken!3 thiss!41) (is-Open!5 (rewardToken!2 thiss!41)))))
(assert (not (=> (and (is-LoanContract!2 thiss!5) (not (isEmpty!1 (visitedStates!2 thiss!5)))) (not (isPrefix!0 (reverse!0 (visitedStates!2 thiss!5)) expected!0)))))
(check-sat)
The inox test suite fails when run against Z3 4.6, as it seems like Z3 now requires explicitly enabling unsat assumption construction.
For instance:
[info] - 158: simple theorem solvr=smt-z3 lucky=true check=true assum=true assck=false model=1 *** FAILED *** (39 milliseconds)
[info] inox.package$FatalError: Unexpected error from z3 solver: line 22 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)
I'm getting the following error when running sbt compile
on Inox:
[info] Compiling 158 Scala sources to ~/inox/target/scala-2.12/classes ...
[info] Done compiling.
[info] Running (fork) tut.TutMain ~/inox/src/main/doc/trees.md ~/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: ~/inox/src/main/doc/trees.md
[info] Running (fork) tut.TutMain ~/inox/src/main/doc/interpolations.md ~/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: ~/inox/src/main/doc/interpolations.md
[error] Exception in thread "main" scala.reflect.internal.Symbols$CyclicReference: illegal cyclic reference involving <refinement of inox.ast.SimpleSymbols with inox.ast.Trees>
[error] java.lang.RuntimeException: Nonzero exit code returned from runner: 1
[error] at scala.sys.package$.error(package.scala:26)
[error] at tut.TutPlugin$.$anonfun$tutOne$1(TutPlugin.scala:149)
[error] at scala.util.Success.foreach(Try.scala:249)
[error] at tut.TutPlugin$.tutOne(TutPlugin.scala:149)
[error] at tut.TutPlugin$.$anonfun$tutAll$1(TutPlugin.scala:157)
[error] at scala.collection.immutable.List.flatMap(List.scala:334)
[error] at tut.TutPlugin$.tutAll(TutPlugin.scala:157)
[error] at tut.TutPlugin$.handleUpdate$1(TutPlugin.scala:106)
[error] at tut.TutPlugin$.$anonfun$projectSettings$29(TutPlugin.scala:111)
[error] at sbt.util.FileFunction$.$anonfun$cached$4(FileFunction.scala:147)
[error] at sbt.util.Difference.apply(Tracked.scala:313)
[error] at sbt.util.Difference.apply(Tracked.scala:293)
[error] at sbt.util.FileFunction$.$anonfun$cached$3(FileFunction.scala:143)
[error] at sbt.util.Difference.apply(Tracked.scala:313)
[error] at sbt.util.Difference.apply(Tracked.scala:288)
[error] at sbt.util.FileFunction$.$anonfun$cached$2(FileFunction.scala:142)
[error] at tut.TutPlugin$.$anonfun$projectSettings$25(TutPlugin.scala:111)
[error] at scala.Function1.$anonfun$compose$1(Function1.scala:44)
[error] at sbt.internal.util.$tilde$greater.$anonfun$$u2219$1(TypeFunctions.scala:40)
[error] at sbt.std.Transform$$anon$4.work(System.scala:67)
[error] at sbt.Execute.$anonfun$submit$2(Execute.scala:269)
[error] at sbt.internal.util.ErrorHandling$.wideConvert(ErrorHandling.scala:16)
[error] at sbt.Execute.work(Execute.scala:278)
[error] at sbt.Execute.$anonfun$submit$1(Execute.scala:269)
[error] at sbt.ConcurrentRestrictions$$anon$4.$anonfun$submitValid$1(ConcurrentRestrictions.scala:178)
[error] at sbt.CompletionService$$anon$2.call(CompletionService.scala:37)
[error] at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[error] at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
[error] at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[error] at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[error] at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[error] at java.lang.Thread.run(Thread.java:748)
[error] (tutQuick) Nonzero exit code returned from runner: 1
There are some mismatches between hasInstance
and simplestValue
inox/src/main/scala/inox/ast/SymbolOps.scala
Line 906 in 7752948
hasInstance
returns true
on types defined outside of Inox (such as ArrayType
)ADTType
, as hasInstance
doesn't visit constructor fields?TypeParameter
, I guess that's expected?Should we make them just one function (returning an Option
), or is the distinction necessary?
And we should override these functions in Stainless for ArrayType
? (always true
?)
Working with stainless to verify a heap sort. Let me know if you need to be able to reproduce this.
stainless verified/src/main/scala/verified.scala --timeout=30 --debug=verification
[Warning ] Parallelism is disabled.
[Internal] Error: Lookup failed for function with symbol `apply$13`. Trace:
[Internal] - inox.ast.Definitions$AbstractSymbols.$anonfun$getFunction$1(Definitions.scala:197)
[Internal] - scala.Option.getOrElse(Option.scala:189)
[Internal] - inox.ast.Definitions$AbstractSymbols.getFunction(Definitions.scala:197)
[Internal] - inox.ast.Definitions$AbstractSymbols.getFunction$(Definitions.scala:196)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.getFunction(ClassSymbols.scala:18)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:53)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.$anonfun$traverse$5(GhostTraverser.scala:62)
[Internal] - stainless.transformers.GhostTraverser.$anonfun$traverse$5$adapted(GhostTraverser.scala:61)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:61)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:22)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2$adapted(GhostTraverser.scala:21)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:21)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.$anonfun$traverse$1(Traverser.scala:18)
[Internal] - stainless.transformers.Traverser.$anonfun$traverse$1$adapted(Traverser.scala:15)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:15)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:22)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2$adapted(GhostTraverser.scala:21)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:21)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:51)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:34)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:28)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:28)
[Internal] - scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.withLocalFuns(GhostTraverser.scala:16)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:28)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:21)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:30)
[Internal] - scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.withLocalClasses(GhostTraverser.scala:18)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:30)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:23)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.$anonfun$sanitize$15(TreeSanitizer.scala:245)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.$anonfun$sanitize$15$adapted(TreeSanitizer.scala:245)
[Internal] - scala.collection.immutable.Stream.foreach(Stream.scala:533)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.sanitize(TreeSanitizer.scala:245)
[Internal] - stainless.extraction.xlang.TreeSanitizer.$anonfun$check$1(TreeSanitizer.scala:42)
[Internal] - scala.collection.immutable.List.flatMap(List.scala:338)
[Internal] - stainless.extraction.xlang.TreeSanitizer.check(TreeSanitizer.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer.check$(TreeSanitizer.scala:30)
[Internal] - stainless.extraction.xlang.TreeSanitizer$$anon$1.check(TreeSanitizer.scala:434)
[Internal] - stainless.extraction.xlang.TreeSanitizer.enforce(TreeSanitizer.scala:48)
[Internal] - stainless.extraction.xlang.TreeSanitizer.enforce$(TreeSanitizer.scala:45)
[Internal] - stainless.extraction.xlang.TreeSanitizer$$anon$1.enforce(TreeSanitizer.scala:434)
[Internal] - stainless.frontend.SplitCallBack.processFunctionSymbols(SplitCallBack.scala:160)
[Internal] - stainless.frontend.SplitCallBack.processFunction(SplitCallBack.scala:154)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3(SplitCallBack.scala:138)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3$adapted(SplitCallBack.scala:137)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:137)
[Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:67)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:38)
[Internal] - java.base/java.lang.Thread.run(Thread.java:834)
[Internal] Lookup failed for function with symbol `apply$13`
[Internal] Please inform the authors of Inox about this message
bash-3.2$
Stainless throws this exception when running the termination checker (stainless --solvers=nativez3 --termination
) over this benchmark:
import stainless.lang._
import stainless.annotation._
import stainless.collection._
object index {
val xs = List("a" -> 1, "b" -> 2, "c" -> 3, "d" -> 4)
def test(map: Map[String, Int]) = {
val res = xs.foldLeft(map) {
case (acc, (k, v)) => acc.updated(k, v)
}
res.get("d") == Some(4)
}.holds
}
The string it is apparently attempting unescape is: !0!
[Internal] Error: String index out of range: 0. Trace:
[Internal] - java.lang.String.charAt(String.java:658)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$class.inox$solvers$theories$ASCIIStringEncoder$$decodeFirstByte(ASCIIStringEncoder.scala:51)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:89)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:103)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:106)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:274)
[Internal] - inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:293)
[Internal] - inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
[Internal] - inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:65)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.decode(SolverFactory.scala:122)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Map$Map3.foreach(Map.scala:161)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:179)
[Internal] - inox.solvers.z3.Z3Unrolling$ModelWrapper.getModel(Z3Unrolling.scala:66)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:671)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:552)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:552)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44)
[Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:43)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:122)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32)
[Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:31)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:122)
[Internal] - inox.tip.TipDebugger$class.check(TipDebugger.scala:56)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.check(SolverFactory.scala:122)
[Internal] - inox.solvers.SimpleSolverAPI$class.solveVALID(SimpleSolverAPI.scala:22)
[Internal] - inox.solvers.SimpleSolverAPI$$anon$1.solveVALID(SimpleSolverAPI.scala:57)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:46)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:45)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Set$Set2.foreach(Set.scala:128)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
[Internal] - scala.collection.SetLike$class.map(SetLike.scala:92)
[Internal] - scala.collection.AbstractSet.map(Set.scala:47)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:45)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:44)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
[Internal] - scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:44)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:21)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - stainless.termination.RelationProcessor$class.run(RelationProcessor.scala:21)
[Internal] - stainless.termination.TerminationChecker$$anon$1$lexicographicProcessor$.run(TerminationChecker.scala:110)
[Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:204)
[Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:197)
[Internal] - scala.collection.Iterator$$anon$13.hasNext(Iterator.scala:462)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - stainless.termination.ProcessingPipeline$class.runPipeline(ProcessingPipeline.scala:232)
[Internal] - stainless.termination.ProcessingPipeline$class.terminates(ProcessingPipeline.scala:156)
[Internal] - stainless.termination.TerminationChecker$$anon$1.terminates(TerminationChecker.scala:39)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:60)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:59)
[Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418)
[Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418)
[Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1233)
[Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1223)
[Internal] - scala.collection.immutable.Stream.foreach(Stream.scala:595)
[Internal] - scala.collection.TraversableOnce$class.toMap(TraversableOnce.scala:316)
[Internal] - scala.collection.AbstractTraversable.toMap(Traversable.scala:104)
[Internal] - stainless.termination.TerminationComponent$$anon$2.<init>(TerminationComponent.scala:69)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:67)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8)
[Internal] - stainless.SimpleComponent$class.apply(Component.scala:87)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8)
[Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:28)
[Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:12)
[Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:191)
[Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:190)
[Internal] - java.util.concurrent.FutureTask.run(FutureTask.java:266)
[Internal] - java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[Internal] - java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[Internal] - java.lang.Thread.run(Thread.java:748)
This happened in Stainless in PR epfl-lara/stainless#1016 in CodeGenVerificationSuite
on InnerClasses5
72: verification/valid/InnerClasses5 type-checker=false codegen *** FAILED *** (567 milliseconds)
[info] inox.package$FatalError: Missfomed SMT source in (str.++ (seq.unit #x54) (seq.unit #x54) (seq.unit #x65) (seq.unit #x65) (seq.unit #x73) (seq.unit #x73) (seq.unit #x74) (seq.unit #x74)):
[info] Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication
On latest master
(3c23a86), running sbt clean compile
yields the following error:
[info] [tut] compiling: /Users/romac/Code/@epfl-lara/inox/src/main/doc/tutorial.md
[error] Exception in thread "main" scala.reflect.internal.Symbols$CyclicReference: illegal cyclic reference involving <refinement of inox.ast.SimpleSym
Landing the rust-interop
features on master
would have enormous benefits for the epfl-lara/rust-stainless project in terms of less maintenance for getting updates. This is under the condition that the features added/changed on the rust-interop branch can co-exist with the current master.
@samarion suggested the following changes to rust-interop
before a potential merge:
After having sbt package publish-local
Inox, I naively add the following line to my build.sbt:
libraryDependencies += "ch.epfl.lara" %% "inox" % "1.0"
sbt then complains that `princess#princess_2.11;2016-07-01`` is unavailable.
Shouldn't Inox install its hand-managed dependencies ?
Is there an easy way to publish the hand-managed dependencies locally ?
Is it possible to retrieve the encoded string for an Inox program before it gets sent off to a solver?
I.e.: the script where higher order functions, dependent types, etc have been removed (or at least rewritten to be FO compatible)
I know if I set debug flags a certain way it will write the .smt2 files to an 'smt-sessions' folder-- though as far as I know this only gets written once the solver is invoked. Is there some native way to programmatically get a string (or at least a File) corresponding to a converted program?
(Apologies if this is in the wrong place; wasn't sure whether to post this on StackOverflow or here)
I'm using Z3 4.5.1 and getting many errors when running sbt test it:test
. Is it perhaps because of some change in Z3? (It doesn't seem to be because of #31)
For example:
[info] - 295: flatMap is associative solvr=smt-z3-opt lucky=false check=false assum=true model=0 *** FAILED *** (85 milliseconds)
[info] inox.package$FatalError: Unexpected error from z3 solver: line 284 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)
$ sbt "it:testOnly *StringSuite* -- -z 28"
[info] Loading project definition from /path/inox/project
[info] Set current project to inox (in build file:/path/inox/)
[info] StringSuite:
[info] - 28: Non-ASCII string encoding solvr=smt-z3 *** FAILED *** (472 milliseconds)
[info] scala.MatchError: WrappedArray(-17, -65, -125) (of class scala.collection.mutable.WrappedArray$ofByte)
[info] at inox.solvers.theories.ASCIIStringEncoder$class.inox$solvers$theories$ASCIIStringEncoder$$decodeFirstByte(ASCIIStringEncoder.scala:35)
[info] at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:68)
[info] at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:84)
[info] at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:84)
[info] at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:87)
[info] at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:291)
[info] at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:310)
[info] at inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
[info] at inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:63)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.decode(SolverFactory.scala:198)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$class.decodeOrSimplest$1(UnrollingSolver.scala:455)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[info] at scala.collection.immutable.Map$Map1.foreach(Map.scala:116)
[info] at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[info] at scala.collection.AbstractTraversable.map(Traversable.scala:104)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:184)
[info] at inox.solvers.unrolling.UnrollingSolver$ModelWrapper.getModel(UnrollingSolver.scala:783)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:461)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:597)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:472)
[info] at scala.util.Try$.apply(Try.scala:192)
[info] at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[info] at inox.utils.TimerStorage.run(Timer.scala:88)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:472)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:198)
[info] at inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:198)
[info] at inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.checkAssumptions(SolverFactory.scala:198)
[info] at inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:86)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:198)
[info] at inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$tip$TipDebugger$$super$check(SolverFactory.scala:198)
[info] at inox.tip.TipDebugger$class.check(TipDebugger.scala:56)
[info] at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.check(SolverFactory.scala:198)
[info] at inox.solvers.SimpleSolverAPI$class.solveSAT(SimpleSolverAPI.scala:35)
[info] at inox.solvers.SimpleSolverAPI$$anon$1.solveSAT(SimpleSolverAPI.scala:57)
[info] at inox.solvers.unrolling.StringSuite$$anonfun$6.apply(StringSuite.scala:57)
[info] at inox.solvers.unrolling.StringSuite$$anonfun$6.apply(StringSuite.scala:54)
[info] at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply$mcV$sp(TestSuite.scala:57)
[info] at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply(TestSuite.scala:57)
[info] at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply(TestSuite.scala:57)
[info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85)
[info] at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
[info] at org.scalatest.Transformer.apply(Transformer.scala:22)
[info] at org.scalatest.Transformer.apply(Transformer.scala:20)
[info] at org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:186)
[info] at org.scalatest.TestSuite$class.withFixture(TestSuite.scala:196)
[info] at org.scalatest.FunSuite.withFixture(FunSuite.scala:1560)
[info] at org.scalatest.FunSuiteLike$class.invokeWithFixture$1(FunSuiteLike.scala:183)
[info] at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
[info] at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
[info] at org.scalatest.SuperEngine.runTestImpl(Engine.scala:289)
[info] at org.scalatest.FunSuiteLike$class.runTest(FunSuiteLike.scala:196)
[info] at org.scalatest.FunSuite.runTest(FunSuite.scala:1560)
[info] at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
[info] at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
[info] at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:396)
[info] at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:384)
[info] at scala.collection.immutable.List.foreach(List.scala:381)
[info] at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:384)
[info] at org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:379)
[info] at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:461)
[info] at org.scalatest.FunSuiteLike$class.runTests(FunSuiteLike.scala:229)
[info] at org.scalatest.FunSuite.runTests(FunSuite.scala:1560)
[info] at org.scalatest.Suite$class.run(Suite.scala:1147)
[info] at org.scalatest.FunSuite.org$scalatest$FunSuiteLike$$super$run(FunSuite.scala:1560)
[info] at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
[info] at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
[info] at org.scalatest.SuperEngine.runImpl(Engine.scala:521)
[info] at org.scalatest.FunSuiteLike$class.run(FunSuiteLike.scala:233)
[info] at org.scalatest.FunSuite.run(FunSuite.scala:1560)
[info] at org.scalatest.tools.Framework.org$scalatest$tools$Framework$$runSuite(Framework.scala:314)
[info] at org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:480)
[info] at sbt.TestRunner.runTest$1(TestFramework.scala:76)
[info] at sbt.TestRunner.run(TestFramework.scala:85)
[info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
[info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
[info] at sbt.TestFramework$.sbt$TestFramework$$withContextLoader(TestFramework.scala:185)
[info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
[info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
[info] at sbt.TestFunction.apply(TestFramework.scala:207)
[info] at sbt.Tests$.sbt$Tests$$processRunnable$1(Tests.scala:239)
[info] at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
[info] at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
[info] at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
[info] at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
[info] at sbt.std.Transform$$anon$4.work(System.scala:63)
[info] at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
[info] at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
[info] at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:17)
[info] at sbt.Execute.work(Execute.scala:237)
[info] at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
[info] at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
[info] at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:159)
[info] at sbt.CompletionService$$anon$2.call(CompletionService.scala:28)
[info] at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[info] at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
[info] at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[info] at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[info] at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[info] at java.lang.Thread.run(Thread.java:748)
[info] Run completed in 1 second, 38 milliseconds.
[info] Total number of tests run: 1
[info] Suites: completed 1, aborted 0
[info] Tests: succeeded 0, failed 1, canceled 0, ignored 0, pending 0
[info] *** 1 TEST FAILED ***
[error] Failed tests:
[error] inox.solvers.unrolling.StringSuite
[error] (it:testOnly) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 3 s, completed 13 sept. 2018 13:41:11
Test case:
import inox._
import inox.trees._
import inox.trees.dsl._
import inox.evaluators.EvaluationResults
val ap = ValDef(FreshIdentifier("a"), StringType, Set())
val bp = ValDef(FreshIdentifier("b"), StringType, Set())
val body =
Application(
Application(
Lambda(Seq(ap),
Lambda(Seq(bp),
StringConcat(StringConcat(ap.toVariable, StringLiteral(":")), bp.toVariable)
)
), Seq(StringLiteral("Winner"))), Seq(StringLiteral("Mikael")))
val main = FreshIdentifier("main")
val funDef = mkFunDef(main)()(_ => (Seq(), StringType, _ => body))
val prog = InoxProgram(
Context.empty,
funDef::Nil, List()
)
prog.getEvaluator.eval(FunctionInvocation(main, Seq(), Seq())) match {
case EvaluationResults.Successful(e) => println(e);e
}
Run and you get:
"Winner:Winner:"
instead of
"Winner:Mikael"
On the tip file below, Z3 4.8.5 produces an output which contains this let
binding:
(let ((a!1 (lambda ((x!1 T!83!10)) (or (= x!1 (T!83!11 1)) (= x!1 (T!83!11 6))))))
(WithProof!4!1 a!1 0 true true)))
When Inox extracts lambdas, it needs to know whether it is extracting a Set, a Map, or a Bag. With this untyped, let
binding, the information is missing. In the model produced by Z3 4.7.1, there is no let
binding and variable a!1
is inlined in the body of the let
. This gives enough context information for Inox
to know which type to expect and how to extract the lambda.
One quick workaround is to inline let
's before extracting, but not sure if this is ok? I'll try tomorrow and see how it goes.
(declare-datatypes () ((ProofOps!8 (ProofOps!9 (prop!31 Bool)))))
(declare-const thiss!36 ProofOps!8)
(declare-datatypes (T!37) ((LList!20 (LCons!18 (h!78 T!37) (t!89 (LList!20 T!37))) (LNil!18))))
(declare-const (par (T!83) (ls!12 (LList!20 (LList!20 T!83)))))
(declare-datatypes (A!10 B!6) ((WithProof!3 (WithProof!4 (x!145 A!10) (r!14 (=> A!10 B!6 Bool)) (proof!17 Bool) (prop!32 Bool)))))
(declare-const (par (T!83) (thiss!38 (WithProof!3 (Set T!83) (Set T!83)))))
(declare-datatypes (A!0) ((RelReasoning!7 (RelReasoning!8 (x!146 A!0) (prop!33 Bool)))))
(define-fun (par (A!95) (==$pipe!0 ((thiss!31 (RelReasoning!7 A!95)) (proof!2 Bool)) (WithProof!3 A!95 A!95) (WithProof!4 (x!146 thiss!31) (lambda ((x$1!0 A!95) (x$2!0 A!95)) (= x$1!0 x$2!0)) proof!2 (prop!33 thiss!31)))))
(define-fun (par (A!4) (any2RelReasoning!0 ((x!3 A!4)) (RelReasoning!7 A!4) (RelReasoning!8 x!3 true))))
(define-fun-rec (par (T!49) (content!7 ((thiss!3 (LList!20 T!49))) (Set T!49) (ite (is-LNil!18 thiss!3) (as emptyset T!49) (union (insert (as emptyset T!49) (h!78 thiss!3)) (content!7 (t!89 thiss!3)))))))
(define-fun-rec (par (T!48) (++!1 ((thiss!2 (LList!20 T!48)) (that!18 (LList!20 T!48))) (LList!20 T!48) (let ((res!33 (ite (is-LNil!18 thiss!2) that!18 (LCons!18 (h!78 thiss!2) (++!1 (t!89 thiss!2) that!18))))) (assume (and (= (content!7 res!33) (union (content!7 thiss!2) (content!7 that!18))) (or (not (= that!18 (as LNil!18 (LList!20 T!48)))) (= res!33 thiss!2))) res!33)))))
(define-fun-rec (par (T!44) (flatten!1 ((ls!6 (LList!20 (LList!20 T!44)))) (LList!20 T!44) (ite (is-LCons!18 ls!6) (++!1 (h!78 ls!6) (flatten!1 (t!89 ls!6))) (as LNil!18 (LList!20 T!44))))))
(define-fun (par (T!82) ($colon$colon!2 ((thiss!24 (LList!20 T!82)) (t!57 T!82)) (LList!20 T!82) (LCons!18 t!57 thiss!24))))
(define-fun trivial!0 () Bool true)
(declare-const (par (T!83) (that!25 (RelReasoning!7 (Set T!83)))))
(assert (par (T!83) (not (or (not (= thiss!36 (ProofOps!9 true))) (is-LNil!18 (as ls!12 (LList!20 (LList!20 T!83)))) (not (= (as thiss!38 (WithProof!3 (Set T!83) (Set T!83))) (==$pipe!0 (any2RelReasoning!0 (content!7 (flatten!1 ($colon$colon!2 (t!89 (as ls!12 (LList!20 (LList!20 T!83)))) (h!78 (as ls!12 (LList!20 (LList!20 T!83)))))))) trivial!0))) (not (= (as that!25 (RelReasoning!7 (Set T!83))) (any2RelReasoning!0 (as emptyset T!83)))) (and (prop!32 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (or (not (proof!17 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83))))) (@ (r!14 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (x!145 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (x!146 (as that!25 (RelReasoning!7 (Set T!83)))))))))))
(check-sat)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.