Add a testgen.p4 file with custom extern definitions such as testgen_…

…assert and testgen_assume. (#4214)
p4lang · Nov 2, 2023 · 14a64e4 · 14a64e4
1 parent 0ba4abc
commit 14a64e4
Show file tree

Hide file tree

Showing 7 changed files with 23 additions and 27 deletions.
diff --git a/backends/p4tools/modules/testgen/CMakeLists.txt b/backends/p4tools/modules/testgen/CMakeLists.txt
@@ -120,11 +120,13 @@ target_link_libraries(
 
 add_custom_target(
   linkp4testgen
-  # Add some convenience links for invoking p4testgen.
-  # TODO: How to best handle includes?
+  # Add some convenience links for invoking P4Testgen.
   COMMAND ${CMAKE_COMMAND} -E create_symlink ${CMAKE_CURRENT_BINARY_DIR}/p4testgen ${P4C_BINARY_DIR}/p4testgen
+  COMMAND ${CMAKE_COMMAND} -E make_directory ${P4C_BINARY_DIR}/p4include &&
+          ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/p4include/*.p4 ${P4C_BINARY_DIR}/p4include
   COMMAND ${CMAKE_COMMAND} -E create_symlink ${P4C_BINARY_DIR}/p4include ${CMAKE_CURRENT_BINARY_DIR}/p4include
   DEPENDS update_includes
+  COMMENT "Setting P4Testgen include and binary symlinks."
 )
 
 add_dependencies(p4testgen linkp4testgen)

diff --git a/backends/p4tools/modules/testgen/p4include/testgen.p4 b/backends/p4tools/modules/testgen/p4include/testgen.p4
@@ -0,0 +1,14 @@
+#ifndef _TOOLS_TESTGEN_P4_
+#define _TOOLS_TESTGEN_P4_
+
+/// Add @param check as a necessary path constraint for all subsequent executions in the program.
+/// Enabled by default, unless `--disable-assumption-mode` is toggled.
+extern void testgen_assume(in bool assumption);
+
+/// Add @param check as a necessary path constraint for all subsequent executions in the program.
+/// Enabled by default, unless `--disable-assumption-mode` is toggled.
+/// If `--assertion-mode` is toggled, P4Testgen will not apply the condition to the path
+/// constraints, but instead will try to only generate tests that violate this assumption.
+extern void testgen_assert(in bool assumption);
+
+#endif
diff --git a/...odules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4 b/...odules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4
@@ -1,4 +1,5 @@
 #include <v1model.p4>
+#include <testgen.p4>
 
 header ethernet_t {
     bit<48> dst_addr;
@@ -19,11 +20,6 @@ struct Headers {
 
 struct Meta {}
 
-// Custom extern definitions.
-extern void testgen_assert(in bool check);
-extern void testgen_assume(in bool check);
-
-
 parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
     state start {
         pkt.extract(h.eth_hdr);

diff --git a/...odules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4 b/...odules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4
@@ -1,4 +1,5 @@
 #include <v1model.p4>
+#include <testgen.p4>
 
 header ethernet_t {
     bit<48> dst_addr;
@@ -19,11 +20,6 @@ struct Headers {
 
 struct Meta {}
 
-// Custom extern definitions.
-extern void testgen_assert(in bool check);
-extern void testgen_assume(in bool check);
-
-
 parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
     state start {
         pkt.extract(h.eth_hdr);

diff --git a/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4 b/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4
@@ -1,4 +1,5 @@
 #include <v1model.p4>
+#include <testgen.p4>
 
 header ethernet_t {
     bit<48> dst_addr;
@@ -19,11 +20,6 @@ struct Headers {
 
 struct Meta {}
 
-// Custom extern definitions.
-extern void testgen_assert(in bool check);
-extern void testgen_assume(in bool check);
-
-
 parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
     state start {
         pkt.extract(h.eth_hdr);

diff --git a/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4 b/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4
@@ -1,4 +1,5 @@
 #include <v1model.p4>
+#include <testgen.p4>
 
 header ethernet_t {
     bit<48> dst_addr;
@@ -19,11 +20,6 @@ struct Headers {
 
 struct Meta {}
 
-// Custom extern definitions.
-extern void testgen_assert(in bool check);
-extern void testgen_assume(in bool check);
-
-
 parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
     state start {
         pkt.extract(h.eth_hdr);

diff --git a/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4 b/...testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4
@@ -1,4 +1,5 @@
 #include <v1model.p4>
+#include <testgen.p4>
 
 header ethernet_t {
     bit<48> dst_addr;
@@ -19,11 +20,6 @@ struct Headers {
 
 struct Meta {}
 
-// Custom extern definitions.
-extern void testgen_assert(in bool check);
-extern void testgen_assume(in bool check);
-
-
 parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
     state start {
         pkt.extract(h.eth_hdr);