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

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

open Syntax
module I = Abstract_interpreter_control_flow

let unsafe = false

type host_externref = int

let ty : host_externref Type.Id.t = Type.Id.make ()

let do_action env = function
  | Wast.Invoke (module_name, func_name, args) -> begin
    Log.info (fun m ->
      m "invoke %a %s %a..."
        (Fmt.option ~none:Fmt.nop Fmt.string)
        module_name func_name Wast.pp_consts args );
    let* f = Env.Abstract.get_exported_func ~env ~module_name ~func_name in
    let ctx = Env.Abstract.get_context ~env in
    let stack =
      List.rev_map (Abstract_value.of_script_const ctx ~ty) args
      |> List.mapi (fun i v -> (i, v))
    in
    let locals = Abstract_locals.of_list stack in
    I.exec_vfunc_from_outside ~ctx ~locals ~env f
    end
  | Get (_module_name, _name) ->
    Log.info (fun m -> m "get...");
    assert false
(* let* global = Link.get_global_from_module env mod_id name in *)
(* let v = Abstract_value.of_concrete ctx global.value in *)
(* Ok [ v ] *)

let run_one ~no_exhaustion:_ (state : Env.Abstract.t Result.t) cmd =
  let* env = state in
  match cmd with
  | Wast.Text_module (false, m) ->
    let* modul, env =
      Compile.Text.until_abstract_link env ~unsafe ~name:None m
    in
    let _state = I.modul_with_ctx ~env ~modul in
    (* TODO: set context in env? Or isn't it necessary as it's supposed to be mutable? *)
    Ok env
  | Assert (Assert_return (action, res)) ->
    let* state = do_action env action in
    let stack = List.rev state.stack in
    if
      List.compare_lengths res stack <> 0
      || not
           (List.for_all2
              (Abstract_value.equal_script_result
                 (Env.Abstract.get_context ~env)
                 ~ty )
              res stack )
    then begin
      (* Log.err (fun m -> *)
      (*   m "got:      %a@.expected: %a" Stack.pp stack Wast.pp_results res ); *)
      Error `Bad_result
    end
    else Ok env
  | _ -> assert false

let run ~no_exhaustion script =
  let context = Abstract_domain.root_context () in
  let env = Env.Abstract.empty ~context in
  let* state =
    Env.Abstract.link_extern_module ~env ~name:"spectest_extern"
      Spectest.abstract_extern_m
  in
  let script = Spectest.m :: Register ("spectest", Some "spectest") :: script in

  List.fold_left
    (fun acc cmd -> run_one ~no_exhaustion acc cmd)
    (Ok state) script

let exec ~(no_exhaustion : bool) (script : Wast.script) =
  let res = run ~no_exhaustion script in
  (* match Symex.Monad.run to_run (Thread.init ()) with *)
  match res with
  | Error _e -> Error (`Msg "script failed!")
  | Ok _ -> Ok ()