Symbolic fuzzing

[epatrizio]

Symbolic execution fuzzing first step : concrete context
Wasm modules have only concrete values and fuzzing checks that symbolic execution has the same behavior as concrete execution

[zapashcanon]

IIUC, all the complexity with the new weird operators is here to allow ignoring some instructions in the symbolic case ? I guess it is because they have not been implemented yet ?

If that is the case, I'd prefer them to be actually implemented (even in an inefficient way) rather than adding all this complex machinery..

[zapashcanon]

OK so, before merging, I'd like some things to be fixed:

• let's implement all basics instructions (either waiting for them to be in encoding or adding them in Owi when possible) like rotl, rotr etc. (https://github.com/formalsec/encoding/pull/80 has been merged so it should be easy :-))
• once this is done, I believe most of the complexity added in the PR from cond.ml can be removed (even without supporting tables in symbolic mode);
• let's try to see if completing the table support is hard or not (complete symbolic table implementation #190), I expect it to be quite straightforward, but if it's not, I'm fine about merging without it.

[filipeom]

let's implement all basics instructions (either waiting for them to be in encoding or adding them in Owi when possible) like rotl, rotr etc.

I fixed rotl, rotr, and trunc here: https://github.com/formalsec/encoding/pull/80.

ctz and popcnt are still missing in owi and in the encoding, so I suggest that for the time being we just concretely evaluate them in symbolic_value.ml.

[krtab]

ctz and popcnt are still missing in owi and in the encoding, so I suggest that for the time being we just concretely evaluate them in symbolic_value.ml.

There may even be clever tricks where we make a decision tree based on Choice.choose to compute those.

[filipeom]

ctz and popcnt are still missing in owi and in the encoding, so I suggest that for the time being we just concretely evaluate them in symbolic_value.ml.

There may even be clever tricks where we make a decision tree based on Choice.choose to compute those.

Yes, this can be an efficient way to solve this. I'm worried it could cause too much branching? I can think of one unclever way to implement it without branching; we'd create massive if-then-else expressions:

 ; ctz summary for I32
 (ite (n = 0) 
   32
   (ite (not (n & 1 = 0))
     31
     (ite (not (n & 2 = 0)) 
       30
       ... 
         0))))

But this would probably grind z3 to a halt 😅

[krtab]

Before merging, could you rebase it as one single commit ?

[zapashcanon]

Thanks!