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/p4.ml.html

Source file p4.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
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