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

Source file runner.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
open Lang
open Sl
module DCov_single = Coverage.Dangling.Single
module DCov_multi = Coverage.Dangling.Multi
module Dep = Runtime.Testgen_neg.Dep
module Sim = Runtime.Sim.Signature

(* Spec runners *)

let run_program_with_dangling (module Simulator : Sim.SIM) (spec : Sim.spec)
    (relname : string) (includes_p4 : string list) (filename_p4 : string) :
    Sim.program_result * DCov_single.t =
  let (module DH : Inst.Handler.HANDLER), read_coverage_dangling =
    Inst.Coverage_dangling.make ()
  in
  Inst.Hook.register [ (module DH : Inst.Handler.HANDLER) ];
  Inst.Hook.init_spec spec;
  let program_result =
    Simulator.Interp.eval_program relname includes_p4 filename_p4
  in
  Inst.Hook.finish ();
  let cover = read_coverage_dangling () in
  (program_result, cover)

let run_programs_with_dangling (module Simulator : Sim.SIM) (spec : Sim.spec)
    (relname : string) (includes_p4 : string list) (filenames_p4 : string list)
    : DCov_multi.t =
  let cover_multi =
    match spec with SL spec -> DCov_multi.init spec | _ -> assert false
  in
  List.fold_left
    (fun cover_multi filename_p4 ->
      let program_result, cover_single =
        run_program_with_dangling
          (module Simulator)
          spec relname includes_p4 filename_p4
      in
      let wellformed, welltyped =
        match program_result with
        | Pass _ -> (true, true)
        | Fail (`Syntax _) -> (false, false)
        | Fail (`Runtime _) -> (true, false)
      in
      DCov_multi.extend cover_multi filename_p4 wellformed welltyped
        cover_single)
    cover_multi filenames_p4

let run_program_internal_with_dangling (module Simulator : Sim.SIM)
    (spec : Sim.spec) (relname : string) (value_program : value) :
    Sim.rel_result * DCov_single.t =
  let (module DH : Inst.Handler.HANDLER), read_coverage_dangling =
    Inst.Coverage_dangling.make ()
  in
  Inst.Hook.register [ (module DH : Inst.Handler.HANDLER) ];
  Inst.Hook.init_spec spec;
  let rel_result = Simulator.Interp.eval_rel relname [ value_program ] in
  Inst.Hook.finish ();
  let cover = read_coverage_dangling () in
  (rel_result, cover)

let run_program_with_dangling_and_vdg ~(derive : bool)
    (module Simulator : Sim.SIM) (spec : Sim.spec) (relname : string)
    (includes_p4 : string list) (filename_p4 : string) :
    Sim.program_result * DCov_single.t * Dep.Graph.t =
  let (module DH : Inst.Handler.HANDLER), read_coverage_dangling =
    Inst.Coverage_dangling.make ()
  in
  let (module VH : Inst.Handler.HANDLER), read_vdg =
    Inst.Value_dependency.make ~derive ~cache_on:Simulator.Cache.cache_on
      ~cache_off:Simulator.Cache.cache_off
  in
  let handlers =
    [ (module DH : Inst.Handler.HANDLER); (module VH : Inst.Handler.HANDLER) ]
  in
  Inst.Hook.register handlers;
  Inst.Hook.init_spec spec;
  let program_result =
    Simulator.Interp.eval_program relname includes_p4 filename_p4
  in
  Inst.Hook.finish ();
  let cover = read_coverage_dangling () in
  let vdg = read_vdg () in
  (program_result, cover, vdg)