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/p4spectec.backend_boot/build.ml.html

Source file build.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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
module Run = Runtime.Dynamic_Runner.Signature
open Error

(* Building a tower *)

let build_target ?(cache = true) ?(det = false) ?(guard = false)
    (level : Config.level) =
  (* Create the target runner *)
  let (module Runner_target) =
    match level.interface with
    | P4_interface -> (module P4.Make () : Run.RUNNER)
    | AL_interface ->
        let module Interface_SpecTec = Interface.SpecTec_AL in
        (module Runner.Make.Make_rec
                  (Interface_SpecTec)
                  (Spectec.Make_null (Interface_SpecTec))
                  (Interp_al.Interp.Make)
                  (Interp_sl.Interp.Make)
                  (Interp_pl.Interp.Make) : Run.RUNNER)
    | SL_interface ->
        let module Interface_SpecTec = Interface.SpecTec_SL in
        (module Runner.Make.Make_rec
                  (Interface_SpecTec)
                  (Spectec.Make_null (Interface_SpecTec))
                  (Interp_al.Interp.Make)
                  (Interp_sl.Interp.Make)
                  (Interp_pl.Interp.Make) : Run.RUNNER)
  in
  (* Initialize the target runner, as an SL spec *)
  let spec =
    let spec_sl = Pass.structure ~final:true [ level.layer.specdir ] in
    (SL spec_sl : Run.spec)
  in
  Runner_target.init ~cache ~det ~guard spec;
  (module Runner_target : Run.RUNNER)

let build_interm ?(cache = true) ?(det = false) ?(guard = false)
    (module Runner_above : Run.RUNNER) (level : Config.level) =
  (* Create the intermediate runner *)
  let (module Interface_SpecTec) =
    match level.interface with
    | P4_interface ->
        error_no_region "P4 interface not supported outside of target level"
    | AL_interface -> (module Interface.SpecTec_AL : Spectec.INTERFACE_SPECTEC)
    | SL_interface -> (module Interface.SpecTec_SL : Spectec.INTERFACE_SPECTEC)
  in
  let (module Runner) =
    (module Runner.Make.Make_nonrec
              (Interface_SpecTec)
              (Spectec.Make_parametric (Runner_above) (Interface_SpecTec))
              (Interp_al.Interp.Make)
              (Interp_sl.Interp.Make)
              (Interp_pl.Interp.Make) : Run.RUNNER)
  in
  (* Initialize the runner, as an SL spec *)
  let spec =
    let spec_sl = Pass.structure ~final:true [ level.layer.specdir ] in
    (SL spec_sl : Run.spec)
  in
  Runner.init ~cache ~det ~guard spec;
  (module Runner : Run.RUNNER)

let build_boot ?(cache = true) ?(det = false) ?(guard = false)
    (module Runner_above : Run.RUNNER) (mode : Run.mode) (level : Config.level)
    =
  (* Create the booter *)
  let (module Interface_SpecTec) =
    match level.interface with
    | P4_interface ->
        error_no_region "P4 interface not supported outside of target level"
    | AL_interface -> (module Interface.SpecTec_AL : Spectec.INTERFACE_SPECTEC)
    | SL_interface -> (module Interface.SpecTec_SL : Spectec.INTERFACE_SPECTEC)
  in
  let (module Booter) =
    (module Runner.Make.Make_nonrec
              (Interface_SpecTec)
              (Spectec.Make_parametric (Runner_above) (Interface_SpecTec))
              (Interp_al.Interp.Make)
              (Interp_sl.Interp.Make)
              (Interp_pl.Interp.Make) : Run.RUNNER)
  in
  (* Initialize the booter, as mode *)
  let spec =
    match mode with
    | AL_mode ->
        let spec_al = Pass.algo [ level.layer.specdir ] in
        (AL spec_al : Run.spec)
    | SL_mode ->
        let spec_sl = Pass.structure ~final:true [ level.layer.specdir ] in
        (SL spec_sl : Run.spec)
    | PL_mode ->
        let spec_pl = Pass.annotate [ level.layer.specdir ] in
        (PL spec_pl : Run.spec)
    | Empty_mode -> assert false
  in
  Booter.init ~cache ~det ~guard spec;
  (spec, (module Booter : Run.RUNNER))

let build_tower ?(cache = true) ?(det = false) ?(guard = false)
    (tower : Config.tower) =
  (* Build the target runner *)
  let runner_target = build_target ~cache ~det ~guard tower.level_target in
  (* Reverse the levels, so that we build levels from the target to boot *)
  let levels = tower.level_boot :: tower.levels_interm |> List.rev in
  let spec_boot = ref None in
  let booter, runners_interm =
    levels
    |> List.mapi (fun idx level ->
           if idx = List.length levels - 1 then (true, level) else (false, level))
    |> List.fold_left
         (fun ((module Runner_above : Run.RUNNER), runners) (last, level) ->
           if not last then
             let runner_interm =
               build_interm ~cache ~det ~guard (module Runner_above) level
             in
             (runner_interm, runner_interm :: runners)
           else
             let spec, booter =
               build_boot ~cache ~det ~guard
                 (module Runner_above)
                 tower.mode level
             in
             spec_boot := Some spec;
             (booter, runners))
         (runner_target, [])
  in
  let spec_boot =
    match !spec_boot with Some spec -> spec | None -> assert false
  in
  (spec_boot, runner_target, runners_interm, booter)

let build_null ?(cache = true) ?(det = false) ?(guard = false) (mode : Run.mode)
    (interface : Config.interface) (paths_spec : string list) =
  let (module Interface_SpecTec) =
    match interface with
    | P4_interface ->
        error_no_region "P4 interface not supported outside of target level"
    | AL_interface -> (module Interface.SpecTec_AL : Spectec.INTERFACE_SPECTEC)
    | SL_interface -> (module Interface.SpecTec_SL : Spectec.INTERFACE_SPECTEC)
  in
  let (module Runner) =
    (module Runner.Make.Make_rec
              (Interface_SpecTec)
              (Spectec.Make_null (Interface_SpecTec))
              (Interp_al.Interp.Make)
              (Interp_sl.Interp.Make)
              (Interp_pl.Interp.Make) : Run.RUNNER)
  in
  let spec =
    match mode with
    | AL_mode ->
        let spec_al = Pass.algo paths_spec in
        (AL spec_al : Run.spec)
    | SL_mode ->
        let spec_sl = Pass.structure ~final:true paths_spec in
        (SL spec_sl : Run.spec)
    | PL_mode ->
        let spec_pl = Pass.annotate paths_spec in
        (PL spec_pl : Run.spec)
    | Empty_mode -> assert false
  in
  Runner.init ~cache ~det ~guard spec;
  (spec, (module Runner : Run.RUNNER))