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
open Runtime.Dynamic_Runner.Signature
open Error
open Util.Source
module Make () : RUNNER = struct
module Spec_ = Backend_sim.Spec.Make ()
module Placeholder = Backend_sim.Placeholder.Make (Spec_)
module MakeExtern
(Interp_AL : INTERP_AL)
(Interp_SL : INTERP_SL)
(Interp_PL : INTERP_PL) : EXTERN = struct
let init_mode mode_ =
let call_func name typs values =
(match mode_ with
| AL_mode -> Interp_AL.eval_func name typs values
| SL_mode -> Interp_SL.eval_func name typs values
| PL_mode -> Interp_PL.eval_func name typs values
| Empty_mode -> assert false)
|> function
| Pass value -> value
| Fail (at, msg) -> error at msg
in
let call_rel name values =
(match mode_ with
| AL_mode -> Interp_AL.eval_rel name values
| SL_mode -> Interp_SL.eval_rel name values
| PL_mode -> Interp_PL.eval_rel name values
| Empty_mode -> assert false)
|> function
| Pass values -> values
| Fail (at, msg) -> error at msg
in
let call_pgm relname includes filename =
(match mode_ with
| AL_mode -> Interp_AL.eval_program relname includes filename
| SL_mode -> Interp_SL.eval_program relname includes filename
| PL_mode -> Interp_PL.eval_program relname includes filename
| Empty_mode -> assert false)
|> function
| Pass [ value_ctx; value_arch ] -> (value_ctx, value_arch)
| Pass _ -> error no_region "unexpected number of return values"
| Fail (`Syntax (at, msg) | `Runtime (at, msg)) -> error at msg
in
Spec_.Func.register call_func;
Spec_.Rel.register call_rel;
Spec_.Pgm.register call_pgm
let checkpoint () : int = 0
let seff (before : int) (after : int) : bool = before <> after
let clear () = ()
module Cache = struct
let cache_on () = ()
let cache_off () = ()
end
let eval_extern_rel = Placeholder.eval_extern_rel
let eval_extern_func = Placeholder.eval_extern_func
end
include (
Runner.Make.Make_rec (Interface.P4) (MakeExtern) (Interp_al.Interp.Make)
(Interp_sl.Interp.Make)
(Interp_pl.Interp.Make) :
RUNNER)
end