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

Source file trace.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
open Domain.Lib
open Lang
module Value = Runtime.Value

(* Verbosity level *)

type level = Simple | Full

(* String utilities *)

let normalize_whitespace (s : string) : string =
  let buf = Buffer.create (String.length s) in
  let in_space = ref false in
  String.iter
    (fun c ->
      if c = ' ' || c = '\t' || c = '\n' || c = '\r' then (
        if not !in_space then Buffer.add_char buf ' ';
        in_space := true)
      else (
        Buffer.add_char buf c;
        in_space := false))
    s;
  Buffer.contents buf

let summarize_value ?(max_len = 100) (value : Value.t) : string =
  let summarize ?(max_len = 100) (s : string) : string =
    if String.length s <= max_len then s
    else String.sub s 0 (max_len - 3) ^ "..."
  in
  value |> Value.to_string |> summarize ~max_len

let format_values (values : Value.t list) : string =
  match values with
  | [] -> ""
  | _ ->
      let svalues = List.map summarize_value values in
      Format.sprintf "  [in: %s]" (String.concat ", " svalues)

let make ?(level = Simple) ?(fmt = Format.std_formatter) () =
  let depth = ref 0 in
  let indent () =
    Format.sprintf "[%2d] %s" !depth (String.make (max 0 (!depth * 2)) ' ')
  in
  let module H : Handler.HANDLER = struct
    include Handler.Default

    let init_spec _ = depth := 0

    (* Common events *)

    let on_rel_enter (rid : RId.t) (values : Value.t list) : unit =
      Format.fprintf fmt "%s-> %s\n%!" (indent ()) rid.it;
      if level = Full && values <> [] then
        Format.fprintf fmt "%s%s\n%!" (indent ())
          (format_values values |> normalize_whitespace);
      incr depth

    let on_rel_exit (rid : RId.t) : unit =
      decr depth;
      Format.fprintf fmt "%s<- %s\n%!" (indent ()) rid.it

    let on_func_enter (fid : FId.t) (values : Value.t list) : unit =
      Format.fprintf fmt "%s-> $%s\n%!" (indent ()) fid.it;
      if level = Full && values <> [] then
        Format.fprintf fmt "%s%s\n%!" (indent ())
          (format_values values |> normalize_whitespace);
      incr depth

    let on_func_exit (fid : FId.t) : unit =
      decr depth;
      Format.fprintf fmt "%s<- $%s\n%!" (indent ()) fid.it

    (* IL events *)

    let on_prem (prem : Il.prem) : unit =
      if level = Full then
        Format.fprintf fmt "%s  | -- %s\n%!" (indent ())
          (Il.Print.string_of_prem prem |> normalize_whitespace)

    (* SL events *)

    let on_instr (instr : Sl.instr) : unit =
      if level = Full then
        Format.fprintf fmt "%s  | %s\n%!" (indent ())
          (Sl.Print.string_of_instr ~short:true instr |> normalize_whitespace)
  end in
  (module H : Handler.HANDLER)