Fix Symbolic.concretize

[krtab]

Fixes: #168
Fixes: #169

@filipeom This changes the output of some of the C tests so I'm requiring your review as well

[filipeom]

Wow, this looks great! And much more concise. However, in concretizing, we still need to pattern match on the Ptr value. Otherwise, select_i32 will start discharging concrete queries to the solver like: fix_symbol: (i32.eq choice_i32_271 (Ptr (i32 8389712) (i32 20))). And, we lose the chunks' bounds information in the function check_within_bounds just below, making it unable to identify memory bugs (the C tests that changed).

So, making concretize something like:

    let concretize (a : Expr.t) : int32 Choice_monad.t =
      let open Choice in
      match a.node.e with
      | Ptr (base, offset) ->
        let+ offset = select_i32 offset in
        Expr.(Ptr (base, Value.const_i32 offset) @: Ty_bitv S32)
      | _ ->
        let+ v = select_i32 a in
        Value.const_i32 v

Should be enough to solve both issues 😀

EDIT: Or perhaps like this to avoid unecessary hashconsig:

    let concretize (a : Expr.t) : int32 Choice_monad.t =
      let open Choice in
      match a.node.e with
      | Val _ | Ptr (_, { node = { e = Val _; _ }; _ }) -> return a
      | Ptr (base, offset) ->
        let+ offset = select_i32 offset in
        Expr.(Ptr (base, Value.const_i32 offset) @: Ty_bitv S32)
      | _ ->
        let+ v = select_i32 a in
        Value.const_i32 v

[zapashcanon]

@krtab, I rebased your PR as I merged a big refactoring. EDIT: oups, looks like this do not build anymore after my rebase (a module needs to be opened, but I'll let you fix this while updating the PR, sorry!)

Otherwise, I'm fine with merging with Filipe's review being applied if it allows to recover the finding of the bugs in the tests.

[krtab]

Should be good to do.
I had to deactivate the store.wat test that will just enumerate all possible i32.

[zapashcanon]

Thanks!