UPPAAL Warns Expression does not have any effect for FFI functions.

[senevoldsen]

Describe the bug The compiler does not recognize that external functions may indeed have side effects and thus warns that an expression (e.g. a statement with just a call to a function with void return type) does not have any effect.

To Reproduce

import "mylib.so" {
    void sendState(int32_t state);
};

Then using the statement sendState(42); gives the warning.

Expected behavior External function may (indeed is likely to) have side effects. Since the compiler presumably handles external calls in a special manner it seems it like it could perhaps internally tag the expression as having a side effect.

Version(s) of UPPAAL tested UPPAAL 5.0.0-rc1

[Kurtoid]

I get this too. My workaround is to convert all void functions to int and save the result (just return 0) to an unused variable. The only place this workaround fails is in special functions like __ON_CREATE__, where side-effects aren't allowed, so it seems calling FFI from __ON_CREATE__ is impossible.

[petergjoel]

A more appropriate warning is "No visible side-effect in the model.".

Having side-effects with external C-functions is really useful, but it is fairly easy to make the modelchecking algorithms unsound.

@Kurtoid you should be able to use FFI in __ON_CREATE__, it is treated exactly in the same way as any other Uppaal function (except that it is hooked on an internal event also). Could you supply a small example demonstrating this issue?

[Kurtoid]

I re-created the example at https://docs.uppaal.org/language-reference/system-description/declarations/external-functions/ on UPPAAL 4.1.20-stratego-11. example.h and example.cpp contain the text from the linked page, and minimal_ffi.xml tries to run set_number(2) in __ON_CREATE__ minimal_ffi_demo.zip

Build with

g++ -std=c++17 -Wpedantic -Wall -Wextra -fPIC -g -Og -o external.o -c external.cpp
gcc -shared -o libexternal.so external.o

Edit the path in minimal_ffi.xml to reflect the built library location. Open minimal_ffi.xml in UPPAAL, and press F5. The side-effect error should appear

Tested in UPPAAL 4.1.20-stratego-11 and UPPAAL 5.0.0

[mikucionisaau]

I think the original report was about the unnecessary warning, which is fair.

Whereas @Kurtoid's minimal_ffi_demo uses __ON_CREATE__() which is not called because it is not a special function. When I rename it into __ON_CONSTRUCT__() (as documented) then it works. In the following declaration I get value = 2 (when the number inside the library is initialized to 42):

import "/home/marius/Desktop/uppaal/issue-230/minimal_ffi_demo/libexternal.so" {
    int32_t get_number();
    void set_number(int32_t n);
    int32_t get_sqrt(int32_t n);
    is_safe = bool is_the_world_safe();
};

void __ON_CONSTRUCT__(){
    set_number(2);
}

int value = get_number();

I am not sure where __ON_CREATE__() comes from, but could you please use __ON_CONSTRUCT__() instead?

I noticed that after pressing F7 the value gets lost:

Pressing F5 (Reloads the engine, which is more radical than syntax check) brings 2 again. So it looks like during syntax check the library gets reloaded but the system representation is not rebuild (because the model did not change) -- so that's a bug!

[Kurtoid]

Got it. Thanks for catching my __ONCONSTRUCT_\ mix-up, I'll be more careful