segfault during symbolic execution

[Laplace-Demon]

https://github.com/OCamlPro/owi/blob/0c31d4355e62390ec6170f01e3e455c96d08c97b/example/c/primes2.c

Running this with owi c is ok but owi c --e-acsl will sometimes lead to a segmentation error.

It may be that in the instrumented code, pointers used for RAC are allocated, initialized and cleared using e-acsl library functions, however they are currently defined empty in our libc directory ?

[Laplace-Demon]

It's seems not related to E-ACSL, I can reproduce it with owi c

[Laplace-Demon]

#include <owi.h>
#include <stdlib.h>

void primes(int *is_prime, int n) {
    for (int i = 0; i < n; ++i) is_prime[i] = 1;
}

int main(void) {
    int *is_prime;
    is_prime = malloc(2 * sizeof(int));

    int n = owi_i32();

    owi_assume(n == 2);
    primes(is_prime, n);

    owi_assert(is_prime[0] == 0);

    free(is_prime);
    return 0;
}

Running the generated .wasm file with owi sym could lead to Segmentation fault rarely (like 2 times in 1000 executions). Either replacing the function body with is_prime[0] = is_prime[1] = 1; directly or assuming n == 1 would make segfault disappear.

I don't know the exact reason for now :( Maybe it has something to do with the symbolic engine or the memory model ?

[krtab]

@filipeom May have some clue if it has to do with the memory model.

[filipeom]

I can look into it to see if I can share any insights ☺️

[zapashcanon]

Z3 sometimes segfault randomly when generating the model. We can see it in the CI sometimes. @Laplace-Demon, if you use --debug could you confirm the crash is happening around model generation ? Also, how many workers do you use ? I guess the default, but what is it on your computer ?

[Laplace-Demon]

Z3 sometimes segfault randomly when generating the model. We can see it in the CI sometimes. @Laplace-Demon, if you use --debug could you confirm the crash is happening around model generation ? Also, how many workers do you use ? I guess the default, but what is it on your computer ?

For worker numbers, the default (twelve on my computer) and one both can reproduce segfault.

[Laplace-Demon]

@zapashcanon Does it mean that the crash is happening around model generation?

Assert failure: false
Model:
  (model
    (symbol_0 (i32 2)))

typechecking ...
typechecking ...
linking      ...
interpreting ...
stack        : [  ]
running instr: i32.const 1024
stack        : [ (i32 1024) ]
running instr: i32.const 0
stack        : [ (i32 0) ; (i32 1024) ]
running instr: i32.const 4
stack        : [ (i32 4) ; (i32 0) ; (i32 1024) ]
running instr: memory.init 0
stack        : [  ]
running instr: data.drop 0
stack        : [  ]
stack        : [  ]
running instr: call 9
calling func : func anonymous
stack        : [  ]
running instr: i32.const 0
stack        : [ (i32 0) ]
running instr: i32.const 0
stack        : [ (i32 0) ; (i32 0) ]
running instr: call 8
calling func : func anonymous
stack        : [  ]
running instr: call 7
calling func : func anonymous
stack        : [  ]
running instr: i32.const 8
stack        : [ (i32 8) ]
running instr: call 5
calling func : func anonymous
stack        : [  ]
running instr: i32.const 0
stack        : [ (i32 0) ]
running instr: i32.const -2147483648
stack        : [ (i32 -2147483648) ; (i32 0) ]
running instr: local.get 0
stack        : [ (i32 8) ; (i32 -2147483648) ; (i32 0) ]
running instr: i32.clz
stack        : [ (i32 28) ; (i32 -2147483648) ; (i32 0) ]
running instr: i32.shr_u
stack        : [ (i32 8) ; (i32 0) ]
running instr: local.tee 1
stack        : [ (i32 8) ; (i32 0) ]
running instr: i32.const 16
stack        : [ (i32 16) ; (i32 8) ; (i32 0) ]
running instr: local.get 1
stack        : [ (i32 8) ; (i32 16) ; (i32 8) ; (i32 0) ]
running instr: i32.const 16
stack        : [ (i32 16) ; (i32 8) ; (i32 16) ; (i32 8) ; (i32 0) ]
running instr: i32.lt_u
stack        : [ (i32 1) ; (i32 16) ; (i32 8) ; (i32 0) ]
running instr: select
stack        : [ (i32 8) ; (i32 0) ]
running instr: local.tee 1
stack        : [ (i32 8) ; (i32 0) ]
running instr: i32.const 0
stack        : [ (i32 0) ; (i32 8) ; (i32 0) ]
running instr: i32.load offset=1024 align=4
stack        : [ (i32 8389648) ; (i32 8) ; (i32 0) ]
running instr: local.tee 2
stack        : [ (i32 8389648) ; (i32 8) ; (i32 0) ]
running instr: local.get 1
stack        : [ (i32 8) ; (i32 8389648) ; (i32 8) ; (i32 0) ]
running instr: i32.const -1
stack        : [ (i32 -1) ; (i32 8) ; (i32 8389648) ; (i32 8) ; (i32 0) ]
running instr: i32.add
stack        : [ (i32 7) ; (i32 8389648) ; (i32 8) ; (i32 0) ]
running instr: i32.and
stack        : [ (i32 0) ; (i32 8) ; (i32 0) ]
running instr: local.tee 1
stack        : [ (i32 0) ; (i32 8) ; (i32 0) ]
running instr: i32.sub
stack        : [ (i32 8) ; (i32 0) ]
running instr: i32.const 0
stack        : [ (i32 0) ; (i32 8) ; (i32 0) ]
running instr: local.get 1
stack        : [ (i32 0) ; (i32 0) ; (i32 8) ; (i32 0) ]
running instr: select
stack        : [ (i32 0) ; (i32 0) ]
running instr: local.get 2
stack        : [ (i32 8389648) ; (i32 0) ; (i32 0) ]
running instr: i32.add
stack        : [ (i32 8389648) ; (i32 0) ]
running instr: local.tee 1
stack        : [ (i32 8389648) ; (i32 0) ]
running instr: local.get 0
stack        : [ (i32 8) ; (i32 8389648) ; (i32 0) ]
running instr: i32.add
stack        : [ (i32 8389656) ; (i32 0) ]
running instr: i32.store offset=1024 align=4
stack        : [  ]
running instr: local.get 1
stack        : [ (i32 8389648) ]
running instr: local.get 0
stack        : [ (i32 8) ; (i32 8389648) ]
running instr: call 1
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
running instr: local.set 0
stack        : [  ]
running instr: call 3
stack        : [ symbol_0 ]
running instr: local.tee 1
stack        : [ symbol_0 ]
running instr: i32.const 2
stack        : [ (i32 2) ; symbol_0 ]
running instr: i32.eq
stack        : [ (i32.of_bool (bool.eq symbol_0 (i32 2))) ]
running instr: call 4
stack        : [  ]
running instr: (block
  local.get 1
  i32.const 1
  i32.lt_s
  br_if 0
  local.get 0
  local.set 2
  (loop
    local.get 2
    i32.const 1
    i32.store align=4
    local.get 2
    i32.const 4
    i32.add
    local.set 2
    local.get 1
    i32.const -1
    i32.add
    local.tee 1
    br_if 0))
stack        : [  ]
running instr: local.get 1
stack        : [ symbol_0 ]
running instr: i32.const 1
stack        : [ (i32 1) ; symbol_0 ]
running instr: i32.lt_s
stack        : [ (i32.of_bool (i32.lt symbol_0 (i32 1))) ]
running instr: br_if 0
stack        : [  ]
running instr: local.get 0
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
running instr: local.set 2
stack        : [  ]
running instr: (loop
  local.get 2
  i32.const 1
  i32.store align=4
  local.get 2
  i32.const 4
  i32.add
  local.set 2
  local.get 1
  i32.const -1
  i32.add
  local.tee 1
  br_if 0)
stack        : [  ]
running instr: local.get 2
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
running instr: i32.const 1
stack        : [ (i32 1) ; (Ptr (i32 8389648) (i32 0)) ]
running instr: i32.store align=4
stack        : [  ]
running instr: local.get 2
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
running instr: i32.const 4
stack        : [ (i32 4) ; (Ptr (i32 8389648) (i32 0)) ]
running instr: i32.add
stack        : [ (Ptr (i32 8389648) (i32 4)) ]
running instr: local.set 2
stack        : [  ]
running instr: local.get 1
stack        : [ symbol_0 ]
running instr: i32.const -1
stack        : [ (i32 -1) ; symbol_0 ]
running instr: i32.add
stack        : [ (i32.add symbol_0 (i32 -1)) ]
running instr: local.tee 1
stack        : [ (i32.add symbol_0 (i32 -1)) ]
running instr: br_if 0
stack        : [  ]
running instr: local.get 2
stack        : [ (Ptr (i32 8389648) (i32 4)) ]
running instr: i32.const 1
stack        : [ (i32 1) ; (Ptr (i32 8389648) (i32 4)) ]
running instr: i32.store align=4
stack        : [  ]
running instr: local.get 2
stack        : [ (Ptr (i32 8389648) (i32 4)) ]
running instr: i32.const 4
stack        : [ (i32 4) ; (Ptr (i32 8389648) (i32 4)) ]
running instr: i32.add
stack        : [ (Ptr (i32 8389648) (i32 8)) ]
running instr: local.set 2
stack        : [  ]
running instr: local.get 1
stack        : [ (i32.add symbol_0 (i32 -1)) ]
running instr: i32.const -1
stack        : [ (i32 -1) ; (i32.add symbol_0 (i32 -1)) ]
running instr: i32.add
stack        : [ (i32.add symbol_0 (i32 -2)) ]
running instr: local.tee 1
stack        : [ (i32.add symbol_0 (i32 -2)) ]
running instr: br_if 0
stack        : [  ]
stack        : [  ]
stack        : [  ]
running instr: local.get 0
stack        : [ (Ptr (i32 8389648) (i32 0)) ]
running instr: i32.load align=4
stack        : [ (i32 1) ]
running instr: i32.eqz
stack        : [ (i32 0) ]
running instr: call 0
Reached problem!Segmentation fault (core dumped)

[zapashcanon]

It looks like it is happening after model generation yes. Let's keep it open to track the issue.

[Laplace-Demon]

Ok, thanks! @zapashcanon @filipeom @krtab