package p4spectec

  1. Overview
  2. Docs
P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (2)

Authors

  1. K
    KAIST PLRG

Maintainers

  1. 9
    99jaehyunlee@kaist.ac.kr

Sources

v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

doc/src/inst/hook.ml.html

Source file hook.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
open Domain.Lib
open Lang
module Value = Runtime.Value
module Dep = Runtime.Testgen_neg.Dep
open Handler

(* Registered handlers *)

let handlers : (module HANDLER) list ref = ref []
let register (handlers_ : (module HANDLER) list) = handlers := handlers_

(* Activity *)

let is_active () : bool = !handlers <> []

(* Initialization and finalization *)

let init_spec (spec : spec) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.init_spec spec) !handlers

let finish () : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.finish ()) !handlers

(* Backup and restore *)

let backup () : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.backup ()) !handlers

let restore () : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.restore ()) !handlers

(* Common events *)

let on_program (value_program : Value.t) : unit =
  match !handlers with
  | [] -> ()
  | _ ->
      List.iter
        (fun (module H : HANDLER) -> H.on_program value_program)
        !handlers

let on_value (value : Value.t) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.on_value value) !handlers

let on_value_dependency (value : Value.t) (value_dep : Value.t)
    (label : Dep.Edges.label) : unit =
  match !handlers with
  | [] -> ()
  | _ ->
      List.iter
        (fun (module H : HANDLER) ->
          H.on_value_dependency value value_dep label)
        !handlers

let on_rel_enter (rid : RId.t) (values_input : Value.t list) : unit =
  match !handlers with
  | [] -> ()
  | _ ->
      List.iter
        (fun (module H : HANDLER) -> H.on_rel_enter rid values_input)
        !handlers

let on_rel_exit (rid : RId.t) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.on_rel_exit rid) !handlers

let on_func_enter (fid : FId.t) (values_input : Value.t list) : unit =
  match !handlers with
  | [] -> ()
  | _ ->
      List.iter
        (fun (module H : HANDLER) -> H.on_func_enter fid values_input)
        !handlers

let on_func_exit (fid : FId.t) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.on_func_exit fid) !handlers

(* IL events *)

let on_prem (prem : Il.prem) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.on_prem prem) !handlers

(* SL events *)

let on_instr (instr : Sl.instr) : unit =
  match !handlers with
  | [] -> ()
  | _ -> List.iter (fun (module H : HANDLER) -> H.on_instr instr) !handlers

let on_instr_dangling (cond : bool) (iid : IId.t) (value : Value.t) : unit =
  match !handlers with
  | [] -> ()
  | _ ->
      List.iter
        (fun (module H : HANDLER) -> H.on_instr_dangling cond iid value)
        !handlers