Appending to a slice of a struct

[rayman2000]

It looks like appending a struct to a slice crashes Gobra. I was trying stuff out and the Gobra IDE kept crashing. I reduced it down to this fairly simple example.

type MyType struct {
	x int
}

func myFunc() {
	mySlice := make([]MyType, 0)
	append(perm(1/2), mySlice, MyType{1})
}

Should this be a supported? If so we should fix it. If not then we should somehow have a more graceful way of failing.

Error message in the IDE:

An exception occurred during execution of Gobra: 
java.lang.ClassCastException: class viper.gobra.ast.internal.Old cannot be cast to class viper.gobra.ast.internal.Location
(viper.gobra.ast.internal.Old and viper.gobra.ast.internal.Location are in unnamed module of loader 'app')

Running Gobra manually gives the long and fairly unhelpful (at least for me) stacktrace:

[info] An unknown Exception was thrown.
[info] java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info] java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
[info]  at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
[info]  at viper.silicon.Silicon.verify(Silicon.scala:202)
[info]  at viper.silicon.Silicon.verify(Silicon.scala:160)
[info]  at viper.gobra.backend.Silicon.$anonfun$verify$1(Silicon.scala:27)
[info]  at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:672)
[info]  at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:431)
[info]  at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[info]  at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[info]  at java.base/java.lang.Thread.run(Thread.java:829)
[info] Caused by: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at java.base/java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1006)
[info]  at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$13(DefaultMainVerifier.scala:275)
[info]  at scala.collection.immutable.List.flatMap(List.scala:293)
[info]  at scala.collection.immutable.List.flatMap(List.scala:79)
[info]  at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:275)
[info]  at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:242)
[info]  at viper.silicon.Silicon$$anon$1.call(Silicon.scala:196)
[info]  at viper.silicon.Silicon$$anon$1.call(Silicon.scala:195)
[info]  at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[info]  ... 3 common frames omitted
[info] Caused by: viper.silicon.reporting.ProverInteractionFailed: Unexpected output of prover. Expected 'success' but found: (error "line 2161 column 312: unknown constant ShStructget0of1<Ref> (Tuple1<Int>) 
[info]  at viper.silicon.decider.ProverStdIO.readSuccess(ProverStdIO.scala:394)
[info]  at viper.silicon.decider.ProverStdIO.assertUsingPushPop(ProverStdIO.scala:246)
[info]  at viper.silicon.decider.ProverStdIO.assert(ProverStdIO.scala:232)
[info]  at viper.silicon.decider.ProverStdIO.assert(ProverStdIO.scala:225)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.proverAssert(Decider.scala:284)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.deciderAssert(Decider.scala:266)
[info]  at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:247)
[info]  at viper.silicon.rules.evaluator$.$anonfun$eval2$4(Evaluator.scala:249)
[...]
[info]  at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:141)
[info]  at java.base/java.util.concurrent.RecursiveTask.exec(RecursiveTask.java:94)
[info]  at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290)
[info]  at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020)
[info]  at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656)
[info]  at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594)
[info]  at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:183)
[info] Writing report to .gobra/stats.json
[info] Could not write to the file .gobra/stats.json. Check whether the permissions to the file allow writing to it.
[info] The verification of member .. - error.myFunc() did not terminate
[info] 
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 8 s, completed Feb 9, 2023, 12:46:15 PM

[rayman2000]

If I do the same thing with a point to the struct instead of the struct itself everything is fine.

[ti-m-o]

I am currently verifying a piece of code that uses slices of structs heavily, and the issue that @rayman2000 reported above still persists. Is there a plan to have full support of append in gobra anytime soon?

[ArquintL]

@ti-m-o I've just pushed a fix for the type error that causes the stack trace posted by @rayman2000.
We use the following specification (in pseudo-code) for func append<T>(p perm, dst, src []T) (res []T) that might be helpful as a reference:

gobra/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala

Lines 437 to 446 in 91344bb

	/**
	* requires p > 0
	* requires forall i int :: { &dst[i] } 0 <= i && i < len(dst) ==> acc(&dst[i])
	* requires forall i int :: { &src[i] } 0 <= i && i < len(src) ==> acc(&src[i], p)
	* ensures len(res) == len(dst) + len(src)
	* ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i])
	* ensures forall i int :: { &src[i] } 0 <= i && i < len(src) ==> acc(&src[i], p)
	* ensures forall i int :: { &res[i] } 0 <= i && i < len(dst) ==> res[i] === old(dst[i])
	* ensures forall i int :: { &res[i] } len(dst) <= i && i < len(res) ==> res[i] === src[i - len(dst)]
	*/

In particular, we still require that the input slices dst and src are disjoint, which is not necessarily the case in Go.

[ti-m-o]

Hi @ArquintL, thanks for the quick fix!
(and, more generally, thanks for the great work the team is doing on gobra - really happy this tool is available!)