Add option to show verbose verifier output (#38)

Fixes #20

Signed-off-by: Dave Thaler <dthaler@ntdev.microsoft.com>

docs/tutorial.md

@@ -373,39 +373,58 @@ joins.
 
 **Step 4)** View verifier verbose output
 
-(TODO: this section needs to be updated for netsh)
 We can view verbose output to see what the verifier is actually doing,
-using the `-v` argument:
+using the "level=verbose" option to "show verification":
 
 ```
-> Release\check.exe -v ..\bpf.o
+> netsh ebpf show verification bpf.o level=verbose
 
-{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0]
-}
-Numbers -> {}
+Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[0]
+ }
+Stack: Numbers -> {}
+entry:
+  goto 0;
+
+Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[1]
+ }
+Stack: Numbers -> {}
+
+Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[1]
+ }
+Stack: Numbers -> {}
 0:
   r0 = 0;
   goto 1;
 
-{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4]
-}
-Numbers -> {}
+Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[3], r0.value=[0], r0.type=number
+ }
+Stack: Numbers -> {}
 
-{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4]
-}
-Numbers -> {}
+Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[3], r0.value=[0], r0.type=number
+ }
+Stack: Numbers -> {}
 1:
-  assert r0 : num;
+  assert r0 is number;
   exit;
+  goto exit;
+
+Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[6], r0.value=[0], r0.type=number
+ }
+Stack: Numbers -> {}
+
+Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[6], r0.value=[0], r0.type=number
+ }
+Stack: Numbers -> {}
+exit:
 
 
-{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4]
-}
-Numbers -> {}
+Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[7], r0.value=[0], r0.type=number
+ }
+Stack: Numbers -> {}
 
 
-0 warnings
-1,0.029,6692
+0 errors
+Verification succeeded
 ```
 
 Normally we wouldn't need to do this, but it is illustrative to see how the
@@ -416,8 +435,7 @@ Each instruction is shown as before, but is preceded by its preconditions
 
 "oo" means infinity, "r0" through "r10" are registers (r10 is the stack
 pointer, r0 is used for return values, r1-5 are used to pass args to other
-functions, r6 is the 'ctx' pointer, etc., "t0" through "t10" contains the
-type of value in the associated register, where -4 means an integer, etc.
+functions, r6 is the 'ctx' pointer, etc.
 
 "meta_offset" is the number of bytes of packet metadata preceding (i.e.,
 with negative offset from) the start of the packet buffer.

scripts/.check-license.ignore

@@ -2,6 +2,7 @@
 
 # File extensions that don't support embedding license info
 .*\.md$
+.*\.rc$
 .*\.sln$
 
 # Other Files

src/ebpf/include/ebpf_api.h

@@ -226,13 +226,15 @@ extern "C"
      * @brief Convert an eBPF program to human readable byte code.
      * @param[in] file Name of ELF file containing eBPF program.
      * @param[in] section The name of the section to query.
+     * @param[in] verbose Obtain additional information about the programs.
      * @param[out] report Points to a text section describing why the program
      *  failed verification.
      * @param[out] error_message On failure points to a text description of
      *  the error.
      */
     uint32_t
-    ebpf_api_elf_verify_section(const char* file, const char* section, const char** report, const char** error_message);
+    ebpf_api_elf_verify_section(
+        const char* file, const char* section, bool verbose, const char** report, const char** error_message);
 
     /**
      * @brief Free a TLV returned from ebpf_api_elf_enumerate_sections

src/ebpf/libs/api/Verifier.cpp

@@ -219,7 +219,8 @@ ebpf_api_elf_disassemble_section(
 }
 
 uint32_t
-ebpf_api_elf_verify_section(const char* file, const char* section, const char** report, const char** error_message)
+ebpf_api_elf_verify_section(
+    const char* file, const char* section, bool verbose, const char** report, const char** error_message)
 {
     std::ostringstream error;
     std::ostringstream output;
@@ -227,6 +228,7 @@ ebpf_api_elf_verify_section(const char* file, const char* section, const char**
         const ebpf_platform_t* platform = &g_ebpf_platform_windows;
         ebpf_verifier_options_t verifier_options = ebpf_verifier_default_options;
         verifier_options.check_termination = true;
+        verifier_options.print_invariants = verbose;
         verifier_options.print_failures = true;
         verifier_options.mock_map_fds = true;
 

src/test/end_to_end/end_to_end.cpp

@@ -360,7 +360,7 @@ TEST_CASE("verify section", "[verify section]")
     REQUIRE(ebpf_api_initiate() == ERROR_SUCCESS);
     ec_initialized = true;
 
-    REQUIRE(ebpf_api_elf_verify_section(SAMPLE_PATH "droppacket.o", "xdp", &report, &error_message) == 0);
+    REQUIRE(ebpf_api_elf_verify_section(SAMPLE_PATH "droppacket.o", "xdp", false, &report, &error_message) == 0);
     REQUIRE(report != nullptr);
     REQUIRE(error_message == nullptr);
 }

src/tools/netsh/ebpfnetsh.rc

@@ -199,6 +199,7 @@ BEGIN
                             "Shows results of trying to verify an eBPF program.\n"
     HLP_EBPF_SHOW_VERIFICATION_EX "\
 \nUsage: %1!s! [filename=]<string> [[section=]<string>]\
+\n                     [[level=]normal|verbose]\
 \n\
 \nParameters:\
 \n\
@@ -207,9 +208,12 @@ BEGIN
 \n      section   - Optionally the name of the section containing the\
 \n                  program.  If not specified, the default is to use the\
 \n                  first code section.\
+\n      level     - One of the following values:\
+\n                   normal: Only display details of errors. This is the\
+\n                           default.\
+\n                   verbose: Display details on every instruction.\
 \n\
-\nRemarks: Shows the verbose verifier results of the specified eBPF\
-\n         program.\
+\nRemarks: Shows the verifier results of the specified eBPF program.\
 \n"
 
 END

src/tools/netsh/elf.cpp

@@ -197,12 +197,14 @@ handle_ebpf_show_verification(
     TAG_TYPE tags[] = {
         {TOKEN_FILENAME, NS_REQ_PRESENT, FALSE},
         {TOKEN_SECTION, NS_REQ_ZERO, FALSE},
+        {TOKEN_LEVEL, NS_REQ_ZERO, FALSE},
     };
     ULONG tag_type[_countof(tags)] = {0};
 
     ULONG status =
         PreprocessCommand(nullptr, argv, current_index, argc, tags, _countof(tags), 0, _countof(tags), tag_type);
 
+    VERBOSITY_LEVEL level = VL_NORMAL;
     std::string filename;
     std::string section = ""; // Use the first code section by default.
     for (int i = 0; (status == NO_ERROR) && ((i + current_index) < argc); i++) {
@@ -217,6 +219,14 @@ handle_ebpf_show_verification(
             section = down_cast_from_wstring(std::wstring(argv[current_index + i]));
             break;
         }
+        case 2: // LEVEL
+        {
+            status = MatchEnumTag(NULL, argv[current_index + i], _countof(g_LevelEnum), g_LevelEnum, (PULONG)&level);
+            if (status != NO_ERROR) {
+                status = ERROR_INVALID_PARAMETER;
+            }
+            break;
+        }
         default:
             status = ERROR_INVALID_SYNTAX;
             break;
@@ -229,9 +239,10 @@ handle_ebpf_show_verification(
     const char* report;
     const char* error_message;
 
-    status = ebpf_api_elf_verify_section(filename.c_str(), section.c_str(), &report, &error_message);
+    status =
+        ebpf_api_elf_verify_section(filename.c_str(), section.c_str(), level == VL_VERBOSE, &report, &error_message);
     if (status == ERROR_SUCCESS) {
-        std::cout << "\nVerification succeeded\n";
+        std::cout << report;
         return NO_ERROR;
     } else {
         if (error_message) {