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

Source file call.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
module Fresh_ = Fresh
open Lang
open Il
module Typ = Runtime.Type.Typ
module Value = Runtime.Value
module Run = Runtime.Dynamic_Runner.Signature
open Error
open Util.Source

(* Extensibility point: extra or override builtins per interface *)

type impl = (Value.t -> unit) -> region -> Typ.t list -> Value.t list -> Value.t

module type EXT = sig
  val entries : (string * impl) list
end

module No_ext : EXT = struct
  let entries = []
end

(* Create a BUILTIN from an EXT module containing extensions *)

module Make (Ext : EXT) () = struct
  (* States for builtins *)

  let ctr : int ref = ref 0

  (* Initializer *)

  let init () : unit = ctr := 0

  (* State management *)

  let checkpoint () : int = !ctr
  let seff (before : int) (after : int) : bool = before <> after

  (* Builtin calls *)

  module Funcs = Map.Make (String)

  let funcs =
    Funcs.empty
    (* Nats *)
    |> Funcs.add "sum_nat" Nats.sum_nat
    |> Funcs.add "max_nat" Nats.max_nat
    |> Funcs.add "min_nat" Nats.min_nat
    (* Ints *)
    |> Funcs.add "sum_int" Ints.sum_int
    |> Funcs.add "max_int" Ints.max_int
    |> Funcs.add "min_int" Ints.min_int
    (* Texts *)
    |> Funcs.add "text_to_int" Texts.text_to_int
    |> Funcs.add "int_to_text" Texts.int_to_text
    |> Funcs.add "split_text" Texts.split_text
    |> Funcs.add "strip_prefix" Texts.strip_prefix
    |> Funcs.add "strip_suffix" Texts.strip_suffix
    |> Funcs.add "strip_all_whitespace" Texts.strip_all_whitespace
    (* Lists *)
    |> Funcs.add "rev_" Lists.rev_
    |> Funcs.add "concat_" Lists.concat_
    |> Funcs.add "distinct_" Lists.distinct_
    |> Funcs.add "partition_" Lists.partition_
    |> Funcs.add "assoc_" Lists.assoc_
    |> Funcs.add "sort_" Lists.sort_
    |> Funcs.add "transpose_" Lists.transpose_
    (* Sets *)
    |> Funcs.add "intersect_set" Sets.intersect_set
    |> Funcs.add "union_set" Sets.union_set
    |> Funcs.add "unions_set" Sets.unions_set
    |> Funcs.add "diff_set" Sets.diff_set
    |> Funcs.add "sub_set" Sets.sub_set
    |> Funcs.add "eq_set" Sets.eq_set
    (* Maps *)
    |> Funcs.add "find_map" Maps.find_map
    |> Funcs.add "find_maps" Maps.find_maps
    |> Funcs.add "add_map" Maps.add_map
    |> Funcs.add "adds_map" Maps.adds_map
    |> Funcs.add "update_map" Maps.update_map
    (* Fresh type id *)
    |> Funcs.add "fresh_typeId" (Fresh_.fresh_typeId ctr)
    (* Numerics *)
    |> Funcs.add "shl" Numerics.shl
    |> Funcs.add "shr" Numerics.shr
    |> Funcs.add "shr_arith" Numerics.shr_arith
    |> Funcs.add "pow2" Numerics.pow2
    |> Funcs.add "bitstr_to_int" Numerics.bitstr_to_int
    |> Funcs.add "int_to_bitstr" Numerics.int_to_bitstr
    |> Funcs.add "bits_to_int_unsigned" Numerics.bits_to_int_unsigned
    |> Funcs.add "bits_to_int_signed" Numerics.bits_to_int_signed
    |> Funcs.add "int_to_bits_unsigned" Numerics.int_to_bits_unsigned
    |> Funcs.add "int_to_bits_signed" Numerics.int_to_bits_signed
    |> Funcs.add "bneg" Numerics.bneg
    |> Funcs.add "band" Numerics.band
    |> Funcs.add "bxor" Numerics.bxor
    |> Funcs.add "bor" Numerics.bor
    |> Funcs.add "bitacc" Numerics.bitacc
    |> Funcs.add "bitacc_replace" Numerics.bitacc_replace
    (* Ext entries merged last — allow interface-specific overrides *)
    |> fun m ->
    List.fold_left (fun acc (k, v) -> Funcs.add k v acc) m Ext.entries

  let invoke (add : value -> unit) (id : id) (targs : targ list)
      (args : value list) : value =
    let func = Funcs.find_opt id.it funcs in
    check (Option.is_some func) id.at
      (Format.asprintf "implementation for builtin %s is missing" id.it);
    let func = Option.get func in
    func add id.at targs args
end