src/symbolic/symbolic_wasm_ffi.ml

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130

(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

module Expr = Smtml.Expr
module Choice = Symbolic_choice_with_memory
module Memory = Symbolic.Memory

(* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
module M :
  Wasm_ffi_intf.S0
    with type 'a t = 'a Choice.t
     and type memory = Memory.t
     and module Value = Symbolic_value = struct
  type 'a t = 'a Choice.t

  type memory = Memory.t

  module Value = Symbolic_value

  let add_pc_wrapper e = Choice.add_pc e

  let assume (i : Value.int32) : unit Choice.t =
    add_pc_wrapper @@ Value.I32.to_bool i

  let assert' (i : Value.int32) : unit Choice.t =
    Choice.assertion @@ Value.I32.to_bool i

  let symbol_bool () =
    Choice.with_new_symbol (Ty_bitv 1) (fun sym ->
      Expr.cvtop (Ty_bitv 32) (Zero_extend 31) (Expr.symbol sym) )

  let symbol_i8 () =
    Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
      Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )

  let symbol_char = symbol_i8

  let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol

  let symbol_i64 () = Choice.with_new_symbol (Ty_bitv 64) Expr.symbol

  let symbol_f32 () = Choice.with_new_symbol (Ty_fp 32) Expr.symbol

  let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol

  let symbol_range (lo : Value.int32) (hi : Value.int32) =
    let open Choice in
    let* x = symbol_i32 () in
    let* () = add_pc_wrapper (Value.I32.le lo x) in
    let+ () = add_pc_wrapper (Value.I32.gt hi x) in
    x

  let abort () : unit Choice.t = Choice.stop

  let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
    Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size

  let free m (ptr : Value.int32) : Value.int32 Choice.t =
    Choice.lift_mem @@ Memory.free m ptr

  let exit (_p : Value.int32) : unit Choice.t = abort ()

  let in_replay_mode () = Choice.return @@ Smtml.Expr.value (Smtml.Value.Int 0)

  let print_char (c : Value.int32) =
    match Smtml.Expr.view c with
    | Val (Num (I32 c)) ->
      Fmt.pr "%c@?" (char_of_int (Int32.to_int c));
      Choice.return ()
    | _ -> assert false
end

type extern_func = Symbolic.Extern_func.extern_func

open M

let symbolic_extern_module =
  let functions =
    [ ( "i8_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i8) )
    ; ( "char_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_char)
      )
    ; ( "i32_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
      )
    ; ( "i64_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I64), symbol_i64)
      )
    ; ( "f32_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 F32), symbol_f32)
      )
    ; ( "f64_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
      )
    ; ( "bool_symbol"
      , Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
      )
    ; ( "range_symbol"
      , Symbolic.Extern_func.Extern_func
          (Func (Arg (I32, Arg (I32, Res)), R1 I32), symbol_range) )
    ; ( "assume"
      , Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assume) )
    ; ( "assert"
      , Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assert') )
    ; ( "in_replay_mode"
      , Symbolic.Extern_func.Extern_func
          (Func (UArg Res, R1 I32), in_replay_mode) )
    ; ( "print_char"
      , Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), print_char)
      )
    ]
  in
  { Link.functions }

let summaries_extern_module =
  let functions =
    [ ( "alloc"
      , Symbolic.Extern_func.Extern_func
          (Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
    ; ( "dealloc"
      , Symbolic.Extern_func.Extern_func
          (Func (Mem (Arg (I32, Res)), R1 I32), free) )
    ; ("abort", Symbolic.Extern_func.Extern_func (Func (UArg Res, R0), abort))
    ; ( "exit"
      , Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), exit) )
    ]
  in
  { Link.functions }