Add the eBPF back end for tools.

.github/workflows/ci-p4tools.yml

@@ -39,4 +39,4 @@ jobs:
       # this is needed to create network namespaces for the ebpf tests.
     - name: Run tests (Ubuntu Linux)
       run: |
-        sudo docker run --privileged -w /p4c/build -e $CTEST_PARALLEL_LEVEL p4c ctest -R testgen-p4c-bmv2 -j2 --output-on-failure --schedule-random
+        sudo docker run --privileged -w /p4c/build -e $CTEST_PARALLEL_LEVEL p4c ctest -R testgen-p4c -j2 --output-on-failure --schedule-random

CMakeLists.txt

@@ -188,7 +188,11 @@ find_python_module (re REQUIRED)
 # other packages
 find_package (Doxygen)
 find_package (BMV2)
-
+# If we have found simple switch or psa switch, we also need scapy and ipaddr.
+if(SIMPLE_SWITCH OR PSA_SWITCH)
+    find_python_module (scapy REQUIRED)
+    find_python_module (ipaddr REQUIRED)
+endif()
 # enable CTest
 enable_testing ()
 

backends/ebpf/run-ebpf-test.py

@@ -51,7 +51,10 @@
                     "default is test")
 PARSER.add_argument("-e", "--extern-file", dest="extern", default="",
                     help="Specify path additional file with C extern function definition")
-
+PARSER.add_argument("-tf", "--testfile", dest="testfile",
+                    help="Provide the path for the stf file for this test. "
+                    "If no path is provided, the script will search for an"
+                    " stf file in the same folder.")
 
 def import_from(module, name):
     """ Try to import a module and class directly instead of the typical
@@ -83,6 +86,7 @@ def __init__(self):
         self.cleanupTmp = True          # Remove tmp folder?
         self.compiler = ""              # Path to the P4 compiler binary
         self.p4Filename = ""            # File that is being compiled
+        self.testfile = ""              # path to stf test file that is used
         self.verbose = False            # Enable verbose output
         self.replace = False            # Replace previous outputs
         self.target = "test"            # The name of the target compiler
@@ -91,8 +95,8 @@ def __init__(self):
         self.extern = ""                # Path to C file with extern definition
 
 
-def run_model(ebpf, stffile):
-    result = ebpf.generate_model_inputs(stffile)
+def run_model(ebpf, testfile):
+    result = ebpf.generate_model_inputs(testfile)
     if result != SUCCESS:
         return result
 
@@ -121,13 +125,16 @@ def run_test(options, argv):
     base, ext = os.path.splitext(basename)           # Name without the type
     dirname = os.path.dirname(options.p4filename)    # Directory of the file
 
-    # We can do this if an *.stf file is present
-    stffile = dirname + "/" + base + ".stf"
-    if options.verbose:
-        print("Checking for ", stffile)
-    if not os.path.isfile(stffile):
-        # If no stf file is present just use the empty file
-        stffile = dirname + "/empty.stf"
+    testfile = options.testfile
+    # If no test file is provided, try to find it in the folder.
+    if not testfile:
+        # We can do this if an *.stf file is present
+        testfile = dirname + "/" + base + ".stf"
+        if options.verbose:
+            print("Checking for ", testfile)
+        if not os.path.isfile(testfile):
+            # If no stf file is present just use the empty file
+            testfile = dirname + "/empty.stf"
 
     template = tmpdir + "/" + "test"
     output = {}
@@ -149,13 +156,13 @@ def run_test(options, argv):
     # Compile and run the generated output
     if result == SUCCESS and not expected_error:
         # If no empty.stf present, don't try to run the model at all
-        if not os.path.isfile(stffile):
+        if not os.path.isfile(testfile):
             msg = "No stf file present!"
             report_output(output["stdout"],
                           options.verbose, msg)
             result = SUCCESS
         else:
-            result = run_model(ebpf, stffile)
+            result = run_model(ebpf, testfile)
     # Only if we did not expect it to fail
     if result != SUCCESS:
         return result
@@ -178,6 +185,8 @@ def run_test(options, argv):
     options.verbose = args.verbose
     options.replace = args.replace
     options.cleanupTmp = args.nocleanup
+    if args.testfile:
+        options.testfile = check_if_file(args.testfile)
     options.target = args.target
     options.extern = args.extern
 

backends/p4tools/cmake/FindZ3.cmake

@@ -31,6 +31,7 @@ find_package_handle_standard_args(
 )
 
 if(Z3_FOUND)
+  message(STATUS "Found Z3 includes at ${Z3_INCLUDE_DIR}.")
   file(READ "${Z3_INCLUDE_DIR}/z3_version.h" Z3_VERSION_FILE)
 
   # Major

backends/p4tools/testgen/CMakeLists.txt

@@ -5,7 +5,6 @@ include(common)
 
 project(p4testgen)
 
-
 # Source files for p4testgen.
 set(
   TESTGEN_SOURCES

backends/p4tools/testgen/core/small_step/cmd_stepper.cpp

@@ -89,7 +89,9 @@ void CmdStepper::initializeBlockParams(const IR::Type_Declaration* typeDecl,
     const auto* iApply = typeDecl->to<IR::IApply>();
     BUG_CHECK(iApply != nullptr, "Constructed type %s of type %s not supported.", typeDecl,
               typeDecl->node_type_name());
-
+    // Also push the namespace of the respective parameter.
+    nextState->pushNamespace(typeDecl->to<IR::INamespace>());
+    // Collect parameters.
     const auto* params = iApply->getApplyParameters();
     for (size_t paramIdx = 0; paramIdx < params->size(); ++paramIdx) {
         const auto* param = params->getParameter(paramIdx);
@@ -106,8 +108,8 @@ void CmdStepper::initializeBlockParams(const IR::Type_Declaration* typeDecl,
         if (const auto* ts = paramType->to<IR::Type_StructLike>()) {
             declareStructLike(nextState, paramPath, ts);
         } else if (paramType->is<IR::Type_Base>()) {
-            auto paramRef = nextState->convertPathExpr(paramPath);
-            nextState->set(paramRef, programInfo.createTargetUninitialized(paramRef->type, false));
+            const auto* paramRef = new IR::Member(paramType, paramPath, "*");
+            nextState->set(paramRef, programInfo.createTargetUninitialized(paramType, false));
         } else {
             P4C_UNIMPLEMENTED("Unsupported initialization type %1%", paramType->node_type_name());
         }

backends/p4tools/testgen/core/small_step/extern_stepper.cpp

@@ -347,6 +347,10 @@ void ExprStepper::evalInternalExternMethodCall(const IR::MethodCallExpression* c
                      generateCopyIn(nextState, fieldargRef, fieldGlobalRef, dir, forceTaint->value);
                  }
              } else if (assignType->is<IR::Type_Base>()) {
+                 globalRef = new IR::Member(assignType, globalRef, "*");
+                 if (const auto* argPath = argRef->to<IR::PathExpression>()) {
+                     argRef = nextState->convertPathExpr(argPath);
+                 }
                  generateCopyIn(nextState, argRef, globalRef, dir, forceTaint->value);
              } else {
                  P4C_UNIMPLEMENTED("Unsupported copy_out type %1%", assignType->node_type_name());
@@ -414,6 +418,10 @@ void ExprStepper::evalInternalExternMethodCall(const IR::MethodCallExpression* c
                      }
                  }
              } else if (assignType->is<IR::Type_Base>()) {
+                 globalRef = new IR::Member(assignType, globalRef, "*");
+                 if (const auto* argPath = argRef->to<IR::PathExpression>()) {
+                     argRef = nextState->convertPathExpr(argPath);
+                 }
                  if (dir == "inout" || dir == "out") {
                      nextState->set(globalRef, nextState->get(argRef));
                  }

backends/p4tools/testgen/targets/ebpf/CMakeLists.txt

@@ -0,0 +1,34 @@
+if(ENABLE_TESTING)
+  # Include the test subdirectory.
+  message("-- Adding p4testgen ebpf test suite")
+  include(test/P4Tests.cmake)
+endif()
+
+# Source files for p4testgen.
+set(
+  TESTGEN_SOURCES
+  ${TESTGEN_SOURCES}
+  ${CMAKE_CURRENT_SOURCE_DIR}/backend/stf/stf.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/ebpf.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/cmd_stepper.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/concolic.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/constants.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/expr_stepper.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/program_info.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/table_stepper.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/target.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/test_backend.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/test_spec.cpp
+  PARENT_SCOPE
+)
+
+# Link the run-ebpf-test binary
+execute_process(COMMAND ln -sfn ${P4C_SOURCE_DIR}/backends/ebpf/run-ebpf-test.py ${CMAKE_BINARY_DIR}/run-ebpf-test.py)
+
+set(
+  TESTGEN_LIBS ${TESTGEN_LIBS}
+  ${P4C_LIBRARIES}
+  ${P4C_LIB_DEPS}
+  ${CMAKE_THREAD_LIBS_INIT}
+  PARENT_SCOPE
+)