diff --git a/backends/p4tools/modules/testgen/CMakeLists.txt b/backends/p4tools/modules/testgen/CMakeLists.txt index 16c06fe905..ab64f513f3 100644 --- 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 new file mode 100644 index 0000000000..b3c7daf375 --- /dev/null +++ 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/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4 b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4 index fe81def062..98e47968c7 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4 +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_1.p4 @@ -1,4 +1,5 @@ #include +#include 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/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4 b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4 index 35d0c6cc43..ec810cbaa0 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4 +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_2.p4 @@ -1,4 +1,5 @@ #include +#include 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/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4 b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4 index 2c901ceb92..5cbd67c6a7 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4 +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_1.p4 @@ -1,4 +1,5 @@ #include +#include 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/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4 b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4 index ed3c0d256c..846543ca07 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4 +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_2.p4 @@ -1,4 +1,5 @@ #include +#include 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/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4 b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4 index 689c77d33b..df641513ad 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4 +++ b/backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/assert_assume_tests/bmv2_testgen_assert_assume_3.p4 @@ -1,4 +1,5 @@ #include +#include 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);