[DMS-31] motoko-san: enable viper tests

[int-index]

Tested locally, seems to work

$ nix-build --no-out-link
/nix/store/9x3vc2cv8pgjbxjm7bj785jiy2bm29r5-all-systems-go
/nix/store/hkr5phdyirqxvh5mbs28q1jsh8p188ag-base-doc
/nix/store/dvyb9zkkqxb8fw8cqa7z934cip7s88z1-base-src
/nix/store/iszz00c5jz6gpzbw689zw0c2l43hxva0-base-tests
/nix/store/masy6n95vhm63rxz123wsj4pin89m968-candid-tests
/nix/store/n68ly0c4p3wgsbk9rnfkrzxxzbs325jk-check-error-codes
/nix/store/vwarw7wa2nj7hg93wdb48hnjjrlrs4s9-check-formatting
/nix/store/saxijxm4jnhz6yvwaqkbwpsxnp47rfk1-check-generated
/nix/store/a404wn7q3y44nwyqxm6gg80j3f97617n-check-grammar
/nix/store/j3x3fmx0b959hl0rgkmqih109mzr4vgi-check-rts-formatting
/nix/store/1s6asj4pmq0ac8kab0lqlr8bwcmv9ry9-deser
/nix/store/c4lxl2q8svhnyvm77xxcw890fk5h8i40-didc
/nix/store/50cawwzwwp25zwc8kl45p7gfw2w57ahs-docs
/nix/store/syfkxkdx1pjd2h0krvmh9jv1z0ykyh7r-drun
/nix/store/5byid93lrx7vzy2zm9s8x0hp37p8yly9-FileCheck
/nix/store/f7b2yl226nbikiv6sbdhmaxg2452c8h5-git-minimal-2.42.0
/nix/store/dn79lzfcya3m1wf7sxqn9zqydjy06cyh-guid-examples-tc
/nix/store/21fmmsfzl2hng9p3fn9my9q13fn8ymas-ic-ref-run
/nix/store/6pbyzwdkm0wyscg3kpvmhwlf425ayls0-ic-wasm
/nix/store/5bxa2mb38qb6zdr992zif74wiq51i7rp-didc.js
/nix/store/fx8c59769m8i0wqk55ldpz9m80vhhqrk-moc.js
/nix/store/j0x2835bagd2aqhcrysgbg5p4vb6bzp8-moc_interpreter.js
/nix/store/vawdxf952bjbipknzqyn8wyb89dw43xy-lsp-int-0
/nix/store/alrn5kfzdpn9xyh4w3jz5wy2naw5rybb-mo-doc
/nix/store/jzxiydbpi35xp75xfz7l7qd5p73bmgj0-mo-ide
/nix/store/d4jizwff3g5ppl8bakbqph3kjiqhq7zj-mo-ld
/nix/store/7nxibc4s3byblb3292ik01il308yfz3m-moc
/nix/store/iaq4ap1a9bkpm6r2j5gwbsmgh7wi8f38-nix-update-1.0.0
/nix/store/x20jscfaw4ds6jdryc3li6jhhbk66bnm-qc-motoko-1
/nix/store/qss2gakqxny6yj76hwcnljpmqxih8sq7-report-site
/nix/store/28g624zni7g138mlbbdw6bng0qyhsxpz-moc-rts
/nix/store/mf8qaa50y9q0cm67g6dsxvbby7ypgpqg-samples
/nix/store/3lhj515v6j529hjxaggcvl6ix3ich8lr-motoko-shell
/nix/store/dhvxjpmr8sc39lp2pnfwxg2hbrl6hrlq-test-bench
/nix/store/9msba1f8049vakskgxi3z979yxy99z6n-test-candid
/nix/store/jz71pj7fqcb3f1zcd9ifk3zbfkkbg7xd-test-coverage
/nix/store/8kyjiq7wkpam2590avbf0pslcadi6cl6-test-drun
/nix/store/z99xaaxmfkvv1lkg8j27ff9lb793ksv2-test-drun-compacting-gc
/nix/store/iny46hbnxi6ir88xv19c3ry7vc5s0fk5-test-drun-dbg
/nix/store/k8hgg00q3sz07nb37g35sc4sfdgpfdzk-test-drun-generational-gc
/nix/store/7nf25kmh6misw4kch14qv8pwfa7nn5na-test-drun-incremental-gc
/nix/store/0p3jc2wj7x67n9d7v17nrc70zqcscycx-test-fail
/nix/store/xh08mnqwf9axmvxdxcgw1394iq65kb9g-test-idl
/nix/store/p1xzc35wdbycvn720nxj68ma3ri4p9x1-test-ld
/nix/store/s92dp2pf5insdy1xn6nykpp70bp32r61-test-lsp
/nix/store/yxbbgpxznq9lbid7gxfl7ajfqd4cy1lg-test-mo-idl
/nix/store/3csjfnmi77sm8ypd1yqq24v50kq0k5xx-test-perf
/nix/store/hs54wkxazp45irgj993r7g7jsxz9p06n-test-profiling-graphs
/nix/store/rd3iv78zyzsk133pbdx62i73g6ci9ylg-test-qc
/nix/store/7f4pwx9df5wqmlv5zg90m0y3jiri36r6-test-repl
/nix/store/qhydw08wyl3243kcd43dpxigf97d2nxd-test-run
/nix/store/jhy2m1mpipmr3f95qkpa4rr6zxhp2arp-test-run-dbg
/nix/store/3cbvr41rz2xdnbcpbwrbglq4pxyc57jp-test-run-deser
/nix/store/rcd7rs45s9195bg9sxg8fvcgfqij8lna-test-trap
/nix/store/vwkvjf3aa64zk63nb3wdzx4f5bc51c8h-test-unit
/nix/store/xg9x9w4i4252fn4s80c3bapbgi7i4mkm-test-viper
/nix/store/hxn39kq9jhgvydp1x1cfpwna40snd81s-viperserver.jar
/nix/store/vx5z7aglsmb8xn4x7h6nmhbnc1q6sdd5-wabt-1.0.34
/nix/store/5k94slxs3blljl6wa3bmn9aa0y0i46fs-ocaml4.12.1-wasm-1.1.1
/nix/store/wzlwr5qbwskdl47z3g16zr2422f3f8hs-wasmtime-15.0.1

[int-index]

Not sure what to make of this test failure:

test-drun-compacting-gc> Some tests failed:
test-drun-compacting-gc> destabilization-crash.drun
test-drun-compacting-gc> make: *** [Makefile:4: all] Error 1
test-drun-compacting-gc> make: Leaving directory '/private/tmp/nix-build-test-drun-compacting-gc.drv-0/test-run-drun-src/run-drun'
error: builder for '/nix/store/5g72fjpcs53sr2fqllhk268s1561xy8z-test-drun-compacting-gc.drv' failed with exit code 2;
       last 25 log lines:
       >  debug.print: postupgrade!
       > -ingress Err: IC0503: Canister rwlgt-iiaaa-aaaaa-aaaaa-cai trapped explicitly: assertion failed at destabilization-crash.mo:41.6-41.18
       > life-mut: [life-v1.drun.comp] [life-v2.drun.comp] [life-v3.drun.comp] [drun]
       > life: [life-v1.drun.comp] [life-v2.drun.comp] [drun]
       > live-upgrade:skipped (no ic-ref-run)
       >  [live-upgrade.drun.comp] [drun]
       > map-upgrades:skipped (no ic-ref-run)
       >  [map0.drun.comp] [map1.drun.comp] [drun]
       > reinstall:skipped (no ic-ref-run)
       >  [a.drun.comp] [b.drun.comp] [drun]
       > self-upgrade:skipped (no ic-ref-run)
       >  [self-upgrade.drun.comp] [drun]
       > stable-mutable:skipped (no ic-ref-run)
       >  [canister1.drun.comp] [canister2.drun.comp] [drun]
       > stable-region-migration: [actor0.drun.comp] [actor1.drun.comp] [drun]
       > tailpositions-actor:skipped (no ic-ref-run)
       >  [actor1.drun.comp] [actor2.drun.comp] [drun]
       > upgrade-hooks:skipped (no ic-ref-run)
       >  [upgrade-hook.drun.comp] [upgrade-hook0.drun.comp] [upgrade-hook1.drun.comp] [upgrade-hook2.drun.comp] [drun]
       > upgrades:skipped (no ic-ref-run)
       >  [upgrade.drun.comp] [upgrade0.drun.comp] [upgrade1.drun.comp] [upgrade2.drun.comp] [upgrade3.drun.comp] [upgrade4.drun.comp] [drun]
       > Some tests failed:
       > destabilization-crash.drun
       > make: *** [Makefile:4: all] Error 1
       > make: Leaving directory '/private/tmp/nix-build-test-drun-compacting-gc.drv-0/test-run-drun-src/run-drun'
       For full logs, run 'nix log /nix/store/5g72fjpcs53sr2fqllhk268s1561xy8z-test-drun-compacting-gc.drv'.

[int-index]

I've restarted CI to see if it was a fluke.

[int-index]

OK, now the failure is different, and it seems to affect macOS only

test-viper> +Verification aborted exceptionally: java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Interaction with prover yielded null. This might indicate that the prover crashed.
test-viper> +java.util.concurrent.ExecutionException: viper.silicon.reporting.ProverInteractionFailed: Interaction with prover yielded null. This might indicate that the prover crashed.
test-viper> +   at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
test-viper> +   at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
test-viper> +   at viper.silicon.Silicon.verify(Silicon.scala:201)
test-viper> +   at viper.silicon.Silicon.verify(Silicon.scala:155)
test-viper> +   at viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:267)
test-viper> +   at viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:265)
test-viper> +   at viper.silicon.SiliconFrontend.viper$silver$frontend$SilFrontend$$super$verification(Silicon.scala:336)
test-viper> +   at viper.silver.frontend.SilFrontend.verification(SilFrontend.scala:215)
test-viper> +   at viper.silver.frontend.SilFrontend.verification$(SilFrontend.scala:214)
test-viper> +   at viper.silicon.SiliconFrontend.verification(Silicon.scala:336)
test-viper> +   at viper.silver.frontend.DefaultPhases.$anonfun$Verification$1(Frontend.scala:117)
test-viper> +   at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
test-viper> +   at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
test-viper> +   at scala.collection.immutable.List.foreach(List.scala:333)
test-viper> +   at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
test-viper> +   at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
test-viper> +   at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:336)
test-viper> +   at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:170)
test-viper> +   at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:147)
test-viper> +   at viper.silicon.SiliconFrontend.execute(Silicon.scala:336)
test-viper> +   at viper.silicon.SiliconRunner$.main(Silicon.scala:381)
test-viper> +   at viper.silicon.SiliconRunner.main(Silicon.scala)
test-viper> +Caused by: viper.silicon.reporting.ProverInteractionFailed: Interaction with prover yielded null. This might indicate that the prover crashed.
test-viper> +   at viper.silicon.decider.ProverStdIO.readLineFromInput(ProverStdIO.scala:61)
test-viper> +   at viper.silicon.decider.ProverStdIO.readLine(ProverStdIO.scala:425)
test-viper> +   at viper.silicon.decider.ProverStdIO.saturate(ProverStdIO.scala:277)
test-viper> +   at viper.silicon.decider.ProverStdIO.saturate(ProverStdIO.scala:268)
test-viper> +   at viper.silicon.verifier.DefaultMasterVerifier$allProvers$.saturate(DefaultMasterVerifier.scala:130)
test-viper> +   at viper.silicon.verifier.DefaultMasterVerifier.verify(DefaultMasterVerifier.scala:182)
test-viper> +   at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:242)
test-viper> +   at viper.silicon.Silicon$$anon$1.call(Silicon.scala:195)
test-viper> +   at viper.silicon.Silicon$$anon$1.call(Silicon.scala:194)
test-viper> +   at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
test-viper> +   at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
test-viper> +   at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
test-viper> +   at java.base/java.lang.Thread.run(Thread.java:1589)
test-viper> +  Cause: viper.silicon.reporting.ProverInteractionFailed: Interaction with prover yielded null. This might indicate that the prover crashed.
test-viper> +  [0] Interaction with prover (instance 00) failed: Interaction with prover yielded null. This might indicate that the prover crashed.

I don't have a macOS machine so I can't investigate this problem.