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

Source file table.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
module Typ = Runtime.Type.Typ
module Value = Runtime.Value
open Util.Source

module Make (Spec_Func : Spec.Func.S) = struct
  module Spec = struct
    module Func = Spec_Func
  end

  (* Match-action table interface *)

  let find_table (value_arch : Value.t) (value_tableName : Value.t) : Value.t =
    let find_table_unqualified table_name_unqualified =
      let value_tableName_unqualified =
        Value.Make.text table_name_unqualified
      in
      Spec.Func.find_object_unqualified_e value_arch value_tableName_unqualified
      |> Option.get
    in
    let table_name = Value.Get.text value_tableName in
    match String.split_on_char '.' table_name with
    | [] -> assert false
    | [ table_name_unqualified ] ->
        find_table_unqualified table_name_unqualified
    | names -> (
        let typ_objectId =
          Typ.Make.var ("nameIR" $ no_region) [] |> Typ.Make.list
        in
        let values_name = List.map Value.Make.text names in
        let value_objectId = Value.Make.list typ_objectId values_name in
        match Spec.Func.find_object_qualified_e value_arch value_objectId with
        | Some value_table -> value_table
        | None ->
            let table_name_unqualified = names |> List.rev |> List.hd in
            find_table_unqualified table_name_unqualified)

  let update_table (value_arch : Value.t) (value_tableName : Value.t)
      (value_tableObject : Value.t) : Value.t =
    let update_table_unqualified table_name_unqualified =
      let value_tableName_unqualified =
        Value.Make.text table_name_unqualified
      in
      Spec.Func.update_object_unqualified_e value_arch
        value_tableName_unqualified value_tableObject
    in
    let table_name = Value.Get.text value_tableName in
    match String.split_on_char '.' table_name with
    | [] -> assert false
    | [ table_name_unqualified ] ->
        update_table_unqualified table_name_unqualified
    | names ->
        let typ_objectId =
          Typ.Make.var ("nameIR" $ no_region) [] |> Typ.Make.list
        in
        let values_name = List.map Value.Make.text names in
        let value_objectId = Value.Make.list typ_objectId values_name in
        if
          Spec.Func.find_object_qualified_e value_arch value_objectId
          |> Option.is_some
        then
          Spec.Func.update_object_qualified_e value_arch value_objectId
            value_tableObject
        else
          let table_name_unqualified = names |> List.rev |> List.hd in
          update_table_unqualified table_name_unqualified

  let add_entry (value_ctx : Value.t) (value_arch : Value.t)
      (value_tableName : Value.t) (value_tableEntryPriorityInterface : Value.t)
      (value_tableKeysetInterface : Value.t)
      (value_tableActionInterface : Value.t) : Value.t =
    (* Lookup table object *)
    let value_tableObject = find_table value_arch value_tableName in
    (* Add entry to table object *)
    let value_tableObject =
      match
        Spec.Func.tableObject_add_entry value_ctx value_tableObject
          value_tableEntryPriorityInterface value_tableKeysetInterface
          value_tableActionInterface
      with
      | Some value_tableObject -> value_tableObject
      | None ->
          (* Replace the key names of the keyset interface with those of the table,
             assuming key fields are given in order *)
          let values_nameIR_key =
            Spec.Func.key_interface_of_tableObject value_tableObject
            |> List.filter_map
                 (fun
                   (value_nameIR_key, value_nameIR_matchKind, _value_typeIR) ->
                   if Value.Get.text value_nameIR_matchKind = "selector" then
                     None
                   else Some value_nameIR_key)
          in
          let values_tableKeyInterface =
            Value.Get.list value_tableKeysetInterface
          in
          let values_tableKeyValueInterface =
            values_tableKeyInterface |> List.map Value.Get.tuple
            |> List.map (fun values -> List.nth values 1)
          in
          let typ_tableKeyInterface =
            Typ.Make.var ("tableKeyInterface" $ no_region) []
          in
          let typ_tableKeyInterfaceList = Typ.Make.list typ_tableKeyInterface in
          let value_tableKeysetInterface =
            List.map2
              (fun value_nameIR_key value_tableKeyValueInterface ->
                [ value_nameIR_key; value_tableKeyValueInterface ])
              values_nameIR_key values_tableKeyValueInterface
            |> List.map (Value.Make.tuple typ_tableKeyInterface)
            |> Value.Make.list typ_tableKeyInterfaceList
          in
          Spec.Func.tableObject_add_entry value_ctx value_tableObject
            value_tableEntryPriorityInterface value_tableKeysetInterface
            value_tableActionInterface
          |> Option.get
    in
    (* Update arch with modified table object *)
    update_table value_arch value_tableName value_tableObject

  let add_default_action (value_ctx : Value.t) (value_arch : Value.t)
      (value_tableName : Value.t) (value_tableActionInterface : Value.t) :
      Value.t =
    (* Lookup table object *)
    let value_tableObject = find_table value_arch value_tableName in
    (* Add entry to table object *)
    let value_tableObject =
      Spec.Func.tableObject_add_default_action value_ctx value_tableObject
        value_tableActionInterface
    in
    (* Update arch with modified table object *)
    update_table value_arch value_tableName value_tableObject
end