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

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

open Bos
open Syntax

let run_file ~parameters ~source_file =
  let { Symbolic_parameters.unsafe
      ; entry_point
      ; invoke_with_symbols
      ; exploration_strategy = _
      ; _
      } =
    parameters
  in
  let* modul = Compile.File.until_validate ~unsafe source_file in
  (* TODO: enable this once the smart strategy is fully implemented
  ( match exploration_strategy with
  | Smart -> Cmd_call_graph.compute_distances m entry_point
  | _ -> () );
  *)
  let* modul =
    Cmd_utils.set_entry_point entry_point invoke_with_symbols modul
  in

  let* abstract_invariant =
    if parameters.generate_abstract_invariant then
      let* env = Cmd_wasm_abs.env () in
      let+ modul, env =
        Compile.Binary.until_abstract_link ~unsafe ~name:None env modul
      in
      try
        let state = Abstract_interpreter_control_flow.modul ~env ~modul in
        state.invariant
      with Abstract_interpreter_control_flow.RecursiveFunctionCall ->
        Abstract_invariant.empty ()
    else Ok (Abstract_invariant.empty ())
  in

  let env = Env.Symbolic.empty ~context:() in
  let* env =
    Env.Symbolic.link_extern_module ~env ~name:"wasi_snapshot_preview1"
      Symbolic_wasm_ffi.wasi_snapshot_preview1
  in
  let* env =
    Env.Symbolic.link_extern_module ~env ~name:"owi" Symbolic_wasm_ffi.owi
  in
  let+ modul, env =
    (* unsafe is set to true because the module was already validated before *)
    Compile.Binary.until_symbolic_link env ~unsafe:true ~name:None modul
  in
  let module Parameters = struct
    let throw_away_trap =
      match parameters.fail_mode with
      | Assertion_only -> true
      | Both | Trap_only -> false

    let timeout = parameters.timeout

    let timeout_instr = parameters.timeout_instr

    let use_ite_for_select = parameters.use_ite_for_select

    let abstract_invariant = abstract_invariant
  end in
  let module I = Interpret.Symbolic (Parameters) in
  Benchmark.with_utime @@ fun () -> I.modul ~env ~modul

(* NB: This function propagates potential errors (Result.err) occurring
             during evaluation (OS, syntax error, etc.), except for Trap and Assert,
             which are handled here. Most of the computations are done in the Result
             monad, hence the let*. *)
let cmd ~parameters ~source_file =
  let { Symbolic_parameters.exploration_strategy
      ; fail_mode
      ; workers
      ; no_worker_isolation
      ; solver
      ; deterministic_result_order
      ; model_format
      ; no_value
      ; no_assert_failure_expression_printing
      ; seed
      ; workspace
      ; model_out_file
      ; with_breadcrumbs
      ; _
      } =
    parameters
  in

  (* deterministic_result_order implies no_stop_at_failure *)
  let no_stop_at_failure =
    parameters.deterministic_result_order || parameters.no_stop_at_failure
  in

  (* TODO: can we handle this at the cmdliner level? *)
  let* workspace =
    match workspace with
    | Some path -> Ok path
    | None -> OS.Dir.tmp "owi_sym_%s"
  in

  let* to_run, run_time = run_file ~parameters ~source_file in

  Symbolic_driver.run ~exploration_strategy ~fail_mode ~workers
    ~no_worker_isolation ~solver ~deterministic_result_order ~model_format
    ~no_value ~no_assert_failure_expression_printing ~workspace
    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~seed ~run_time to_run