do not inline or_ function

[zapashcanon]

No description provided.

[zapashcanon]

@filipeom could you confirm it fixes the issue for you?

[filipeom]

I'm getting:

File "src/libc/dune", line 46, characters 0-960:
 46 | (rule
 47 |  (targets
 48 |   assert_fail.o
.....
114 |   src/unistd.c)
115 |  (action
116 |   (run ./script.exe %{deps})))
src/test-comp.c:3:8: error: unknown type name 'noinline'; did you mean 'inline'?
static noinline __attribute__((noinline)) _Bool or_(_Bool a, _Bool b) {
       ^~~~~~~~
       inline
1 error generated.

If I remove the noinline it still gives the same error.

But, locally I just removed or_ in favour of | and it fixed it

[zapashcanon]

Ooops sorry, should be good now. 😅

[filipeom]

noinline did not work. Still gave the same parsing error. Howerver, the optnone seems to do the trick 😄

[zapashcanon]

For some reason it's working for me right now ?

[filipeom]

For some reason it's working for me right now ?

Perhaps I'm doing something wrong. I'm just running it like:

➜  owi git:(fixor) dune clean && dune build @install && dune exec -- owi c bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c 
[parse exception: bad local.get index (at 0:227)]
Fatal: error parsing wasm
clang: error: linker command failed with exit code 1 (use -v to see invocation)
run ['/usr/bin/clang' '-O3' '--target=wasm32' '-m32' '-ffreestanding'
     '--no-standard-libraries' '-Wno-everything' '-flto=thin'
     '-Wl,--entry=main' '-Wl,--export=main' '-Wl,--lto-O0'
     '-Wl,-z,stack-size=8388608' '-I'
     '/home/filipe/lib/owi/_build/install/default/share/owi/libc' '-o'
     'a.out.wasm'
     '/home/filipe/lib/owi/_build/install/default/share/owi/binc/libc.wasm'
     'bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c']: exited with 1

[zapashcanon]

You have to run dune install before running the benchmark. I think I forget to tell you about this sorry. 😅 Actually, the benchmark is launching whatever version of owi is installed, not the one in the current folder.

[zapashcanon]

Aw, you're not launching test-comp, sorry. Maybe a dune install will also help dune to find the right libc?

[filipeom]

Aw, you're not launching test-comp, sorry. Maybe a dune install will also help dune to find the right libc?

It's weird, supposedly in the error log it says its using the local libc.wasm:

/home/filipe/lib/owi/_build/install/default/share/owi/binc/libc.wasm

And, removing it correctly flags it as not existing:

➜  owi git:(fixor) rm -rf /home/filipe/lib/owi/_build/install/default/share/owi/binc/libc.wasm # delete it here
➜  owi git:(fixor) dune exec -- owi c bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c 
can't find file libc.wasm                                                                                                                                                                    
➜  owi git:(fixor) dune build @install
➜  owi git:(fixor) dune exec -- owi c bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c 
[parse exception: bad local.get index (at 0:227)]
Fatal: error parsing wasm
clang: error: linker command failed with exit code 1 (use -v to see invocation)
run ['/usr/bin/clang' '-O3' '--target=wasm32' '-m32' '-ffreestanding'
     '--no-standard-libraries' '-Wno-everything' '-flto=thin'
     '-Wl,--entry=main' '-Wl,--export=main' '-Wl,--lto-O0'
     '-Wl,-z,stack-size=8388608' '-I'
     '/home/filipe/lib/owi/_build/install/default/share/owi/libc' '-o'
     'a.out.wasm'
     '/home/filipe/lib/owi/_build/install/default/share/owi/binc/libc.wasm'
     'bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c']: exited with 1%

But if it works for you great! It's probably something weird with my setup. I'll figure it out later

[zapashcanon]

@filipeom, sorry, it was a mistake on my part. I've been able to reproduce the issue and it should be fixed now. Could you confirm if it's also OK for you? If yes, feel free to merge. :)

[filipeom]

@filipeom, sorry, it was a mistake on my part. I've been able to reproduce the issue and it should be fixed now. Could you confirm if it's also OK for you? If yes, feel free to merge. :)

I does seem to compile now. However, the compilation result doesn't seem correct to me. The function below is the result of compiling __VERIFIER_nondet_bool. See how it's calling assume (call 3) with const 0. Making execution abort prematurely and terminate with All Ok.

(module
  (type (;0;) (func (param i32)))
  (type (;1;) (func (result i32)))
  (type (;2;) (func))
  (type (;3;) (func (param i32 i32) (result i32)))
  (import "symbolic" "assert" (func (;0;) (type 0)))
  (import "summaries" "abort" (func (;1;) (type 2)))
  (import "symbolic" "i32_symbol" (func (;2;) (type 1)))
  (import "symbolic" "assume" (func (;3;) (type 0)))
  (func (;4;) (type 1) (result i32)
    (local i32)
    call 2
    local.set 0
    i32.const 0  ;; <- pushes 0 to the stack
    call 3       ;; <- assume false (ends)
    local.get 0
    i32.const 0
    i32.ne)

I think we should consider using the optnone attribute instead of noinline, which yields the following compilation result:

   (func (;4;) (type 1) (result i32)
    (local i32 i32 i32)
    i32.const 8389664
    local.tee 1
    call 2                ;; symbol
    local.tee 0
    i32.eqz               ;; symbol == 0
    local.tee 2
    i32.store8 offset=14
    local.get 1
    local.get 0           ;; symbol
    i32.const 0
    i32.ne                ;; symbol != 0
    local.tee 0
    i32.store8 offset=13
    local.get 0
    local.get 2
    i32.or                ;; (symbol == 0) | (symbol != 0)
    call 3                ;; assume (symbol == 0) | (symbol != 0)
    local.get 0)

I know this is not great because it has twice as many instructions, but at least we don't loose reasoning capabilities. Also #380 will properly address this, making so we don't have to use _or.

[zapashcanon]

Indeed, thanks for the explanation! I believe I managed to get the best of both worlds (correct compilation and not too many instructions) by also adding a naked attribute. Can you confirm?

dune b @install && dune exec -- owi c bench/testcomp/sv-benchmarks/c/ldv-regression/test22-3.c ; wasm2wat ./a.out.wasm
Assert failure: false                    
Model:
  ...
Reached problem!
(module
  (type (;0;) (func (param i32)))
  (type (;1;) (func (result i32)))
  (type (;2;) (func))
  (type (;3;) (func (param i32 i32) (result i32)))
  (import "symbolic" "assert" (func (;0;) (type 0)))
  (import "summaries" "abort" (func (;1;) (type 2)))
  (import "symbolic" "i32_symbol" (func (;2;) (type 1)))
  (import "symbolic" "assume" (func (;3;) (type 0)))
  (func (;4;) (type 1) (result i32)
    (local i32)
    call 2
    local.tee 0
    i32.eqz
    local.get 0
    i32.const 0
    i32.ne
    local.tee 0
    i32.or
    call 3
    local.get 0)
  ...)

[filipeom]

The compilation result looks much better! I'm happy with this 😄