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

Source file single.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
open Domain.Lib
open Lang
open Sl
open Util.Source

(* Instruction node *)

module Node = struct
  (* Enclosing relation or function id *)

  type origin = id

  (* Status *)

  type status = Hit | Miss

  (* Type *)

  type t = { origin : origin; status : status }

  (* Constructor *)

  let init (id : id) : t = { origin = id; status = Miss }

  (* Equivalence *)

  let eq (node_a : t) (node_b : t) : bool =
    node_a.origin = node_b.origin && node_a.status = node_b.status

  (* Printer *)

  let to_string (node : t) : string =
    match node.status with Hit -> "H" | Miss -> "M"
end

(* Instruction node coverage map *)

module Cover = struct
  include MakeIIdEnv (Node)

  (* Constructor *)

  let is_ignored (hints : hint list) : bool =
    Hints.Flag.init hints "cover_instr_ignore"

  let rec init_instr (cover : t) (id : id) (instr : instr) : t =
    let iid = instr.note.iid in
    let node = Node.init id in
    let cover = add iid node cover in
    match instr.it with
    | IfI (_, _, block_then, _) -> init_block cover id block_then
    | HoldI (_, _, _, holdcase) -> (
        match holdcase with
        | BothH (block_hold, block_nothold) ->
            let cover = init_block cover id block_hold in
            init_block cover id block_nothold
        | HoldH (block_hold, _) -> init_block cover id block_hold
        | NotHoldH (block_nothold, _) -> init_block cover id block_nothold)
    | CaseI (_, cases, _) ->
        let blocks = cases |> List.split |> snd in
        List.fold_left
          (fun cover block -> init_block cover id block)
          cover blocks
    | GroupI (_, _, _, block_group) -> init_block cover id block_group
    | LetI (_, _, _, block) -> init_block cover id block
    | RuleI (_, _, _, _, block) -> init_block cover id block
    | _ -> cover

  and init_block (cover : t) (id : id) (block : block) : t =
    List.fold_left (fun cover instr -> init_instr cover id instr) cover block

  let init_tablerow (cover : t) (id : id) (tablerow : tablerow) : t =
    let _, _, block = tablerow in
    init_block cover id block

  let init_tablerows (cover : t) (id : id) (tablerows : tablerow list) : t =
    List.fold_left
      (fun cover tablerow -> init_tablerow cover id tablerow)
      cover tablerows

  let init_def (cover : t) (def : def) : t =
    match def.it with
    | RelD (id, _, _, block, elseblock_opt, hints) when not (is_ignored hints)
      -> (
        let cover = init_block cover id block in
        match elseblock_opt with
        | Some elseblock -> init_block cover id elseblock
        | None -> cover)
    | FuncDecD (id, _, _, _, block, elseblock_opt, hints)
      when not (is_ignored hints) -> (
        let cover = init_block cover id block in
        match elseblock_opt with
        | Some elseblock -> init_block cover id elseblock
        | None -> cover)
    | TableDecD (id, _, _, tablerows, hints) when not (is_ignored hints) ->
        init_tablerows cover id tablerows
    | _ -> cover

  let init_spec (spec : spec) : t = List.fold_left init_def empty spec
end

(* Instruction node coverage *)

type t = Cover.t

(* Querying coverage *)

let is_hit (cover : t) (iid : iid) : bool =
  let node = Cover.find iid cover in
  match node.status with Hit -> true | Miss -> false

let is_miss (cover : t) (iid : iid) : bool =
  let node = Cover.find iid cover in
  match node.status with Hit -> false | Miss -> true

(* Hit *)

let hit (cover : t) (iid : iid) : t =
  match Cover.find_opt iid cover with
  | Some node when node.status = Node.Miss ->
      let hit_node = { node with Node.status = Node.Hit } in
      Cover.add iid hit_node cover
  | _ -> cover

(* Extending coverage *)

let extend (cover : t) (cover_extend : t) : t =
  Cover.fold
    (fun iid (node : Node.t) cover ->
      match node.status with Node.Hit -> hit cover iid | Node.Miss -> cover)
    cover_extend cover

(* Constructor *)

let init (spec : spec) : t = Cover.init_spec spec
let empty : t = Cover.empty