StackOverflow in silicon not catched and causes stuck execution

[sakehl]

So I encountered the following. I tried to verify a large C file. (this one: conv_layer_0.txt) with vercors using silicon.

I executed it with vct conv_layer_0.c > allout3.txt 2>&1
And it gave the following output:
allout3.txt

Now after 26min I just cancelled the execution:

lars@hp:~/data/HaliVerExperiments/build$ time vct conv_layer_0.c > allout3.txt 2>&1
^C

real    26m24,994s
user    3m23,979s
sys     0m5,116s

Now I changed the stack size option of java towards '-Xss32m' (at several places, since was not sure where it was picked up). And the file verified.

lars@hp:~/data/HaliVerExperiments/build$ time vct conv_layer_0.c
[INFO] Starting verification
[WARN] Silicon has explored 1000 branch traces for entity conv_layer_0.
[INFO] Current branch information:
[INFO]  - alternative 1 of 2
[INFO]  - At conv_layer_0.c:332: _relu_s0_n < 5
[INFO]  - alternative 1 of 2
[INFO]  - At conv_layer_0.c:350: _relu_s0_y < 80
[INFO]  - alternative 1 of 2
[INFO]  - At conv_layer_0.c:367: _relu_s0_x < 100
[INFO]  - At generated: !(0 <= _0 && _0 < 128)
[INFO] Verification completed successfully.

real    2m30,242s
user    3m3,136s
sys     0m4,522s

This leads me to believe that if a StackOverflow error occurs, we do not notice this, and VerCors keeps on executing.

Note: This was on my C-branch:
https://github.com/sakehl/vercors/tree/better-c-support

[pieter-bos]

Yes I've noticed this before, my best guess is that the main thread does terminate (after printing the crash trace), but somehow a non-daemon thread sticks around, which the JVM then waits for.

On a side note, quite the achievement that you managed a stack overflow with presumably -Xss20m, never seen that before...