symbolic interpretation of several modules in one file

[epatrizio]

(module
  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))

  (func $start
    (local $x i32)
    (local.set $x (call $i32_symbol))
    (if (i32.lt_s (i32.const 5) (local.get $x))
    (then unreachable)))

  (start $start)
)

(module
  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))

  (func $start
    (local $x i32)
    (local.set $x (call $i32_symbol))
    (if (i32.lt_s (i32.const 5) (local.get $x))
    (then unreachable)))

  (start $start)
)

Symbolic interpretation of this file launches the following trace :

Trap: unreachable                      
Model:
  (model
    (symbol_0 i32 (i32 6)))
Trap: unreachable
Model:
  (model
    (symbol_0 i32 (i32 -2147483642))
    (symbol_1 i32 (i32 6)))
Reached 2 problems!

instead of :

Trap: unreachable                      
Model:
  (model
    (symbol_0 i32 (i32 6)))
Trap: unreachable
Model:
  (model
    (symbol_0 i32 (i32 6)))
Reached 2 problems!

It seems a status initialization problem after the first module interpretation ?

[filipeom]

This doesn't appear to be trivial, so it might not be a straightforward answer. However, I'll try to give you my best interpretation of why I believe the first output is correct.

From my current understanding of the interpreter, I would expect that the execution follows this semantics: First, execute the module at the top, and if we do not trap, then execute the one at the bottom.

To help us understand this, let me concretize the inputs for three test cases:

1. Both ok: No trap in any module.
2. First bad: Trap in the first module.
3. Second bad: Trap in the second module.

Both ok:

First module: x = 5 -> Execution success, proceed to the second module Second module: x = 5 -> Execution success

First bad:

First module: x = 6 -> Trap

Second bad:

First module: x = 5 -> Execution success, proceed to the second module Second module: x = 6 -> Trap

And so, you can see that to observe the second trap, you would need to be in a case where we did not trap in the first module (i.e., (i32.not (i32.lt (i32 5) symbol_0))).

If you print the path conditions of the program, you can see this more clearly:

PATH CONDITION:
(i32.lt (i32 5) symbol_0)
Trap: unreachable
Model:
  (model
    (symbol_0 i32 (i32 6)))
(* Filipe: Second path starts here ->*)
PATH CONDITION:
(i32.lt (i32 5) symbol_1)
(i32.not (i32.lt (i32 5) symbol_0))
Trap: unreachable
Model:
  (model
    (symbol_0 i32 (i32 -2147483642))
    (symbol_1 i32 (i32 6)))
PATH CONDITION:
(i32.not (i32.lt (i32 5) symbol_1))
(i32.not (i32.lt (i32 5) symbol_0))
Reached 2 problems!

[epatrizio]

Thanks for the detailed answer. My first feeling: in one file, all the modules are independent (> separate interpretations). But your feeling makes sense! What's the best approach ? Cc. @zapashcanon @chambart

[filipeom]

My first feeling: in one file, all the modules are independent (> separate interpretations).

This makes sense to me as well. I think I also prefer it this way, as it allows symbolic execution to scale better within the same file.

Additionally, the module execution order probably doesn't make sense and might introduce some misconceptions about having certain preconditions for a module to fail. For example, in the second module to observe the failure, we don't actually care about the result of the first module?

[redianthus]

I believe we should think about how we could reuse the script language to write this kind of tests more easily. It needs to be designed but I'm going to think about it.

[redianthus]

I believe we are now using a nice workaround with a table of functions and a call_indirect on a symbolic value which is good enough for us. :-)