Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Tips for Debugging

While writing or updating a spec, you will run into errors. This chapter collects the techniques that help narrow the gap between a failing run and a root cause.

The two worked examples below use the exercises from Section 3.1 and Section 3.2. You may complete those exercises yourself or walk through them here.

How P4-SpecTec Executes Rules

Before diving into the techniques, it helps to understand how the interpreter runs. This is covered in How Rules are Executed in Chapter 1.

Tip 1: Read the Error Message Carefully

The default error output looks like this:

runtime error: relation Program_ok failed
│ ··· omitting 1 traces ···
nano-p4/spec/5.08-typing-declaration.watsup:191.8-191.16
relation Decls_ok failed
└── nano-p4/spec/5.08-typing-declaration.watsup:190.8-190.15
    relation Decl_ok failed

The tree is printed bottom-up: Program_ok called Decls_ok, which called Decl_ok, which failed. The file and line number on each line identifies the premise that invoked the child relation. Navigate there to see what the parent was trying to prove and under what conditions.

Tip 2: Use -trace-full to See Values at Each Step

Pass -trace-full to print the actual values being matched at each step:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p program.p4 -trace-full

Each [in: ...] line shows the concrete values a relation or function received. This is most useful when a rule silently fails due to a pattern mismatch: you can see exactly what shape the value has and compare it against the patterns written in the spec.

Tip 3: Insert debug Premises

The debug <expr> premise prints the value of <expr> and always succeeds. It is the spec equivalent of console.log. Place it inside a function or rule definition to inspect intermediate values:

def $find_var_t(BLOCK, TC, id) = varTypeIR
  -- debug id            ;; prints the id being looked up
  -- if typeFrame = TC.BLOCK.FRAME
  -- if varTypeIR = $find_map<id, varTypeIR>(typeFrame, id)

The output line includes the source location so you know which premise fired:

nano-p4/spec/5.00-typing-context.watsup:196.12-196.14: id
pass

You can debug any expression, not just variables. debug TC.BLOCK.FRAME prints the entire block frame; debug (TC.LOCAL.FRAMES) prints the local stack. Remove all debug premises before committing: they do not affect correctness but add noise to every run.

Tip 4: Navigate to the Syntax Definition to Check Pattern Matching

When a rule silently fails without calling any sub-relation, the usual cause is an if premise whose pattern does not match the actual value: the value exists and is well-formed, but the pattern is wrong.

-trace-full shows the actual value going into each -- if. Compare it against the pattern written in the spec. Common mismatches:

  • Using STRUCT where the value is HEADER (or vice versa).
  • Forgetting a constructor variant in a rulegroup.
  • Matching on a tag that only covers one branch of a union type.

When you spot a suspicious pattern, look up its type in the spec to see all variants. For example, typeIR is defined across several constructors in 2.1-ir.watsup. If a rulegroup handles STRUCT but not HEADER, types that are headers will fall through every branch and the relation will fail.

Worked Example: Exercise 3.1

This example uses the exercise program from Section 3.1:

control Filter(inout Header hdr, out bool pass) {
    apply {
        pass = true;
    }
}

Step 1: Run and narrow down the declaration

$ ./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.1.p4
runtime error: relation Program_ok failed
...
relation Decl_ok failed

Decl_ok failed somewhere inside one of the declarations, but the message does not say which one. Between nano_core.p4, nano_model.p4, and the program itself, there are many declarations in scope: Nanonet, Header, packet_in, NoAction, parse, filter, NanoSwitch, Parser, Filter, and main. This tells you almost nothing about where to look.

Add a debug before the Decl_ok premise in Decls_ok/cons in 5.08-typing-declaration.watsup:

rule Decls_ok/cons:
  TC_0 |- declaration_h :: declaration_t* -| TC_2
  -- debug declaration_h
  -- Decl_ok: TC_0 |- declaration_h -| TC_1
  -- Decls_ok: TC_1 |- declaration_t* -| TC_2

Because debug always succeeds and prints before Decl_ok runs, the last declaration printed before the error is the one that failed:

...
nano-p4/spec/5.08-typing-declaration.watsup:190.14-190.27: declaration_h
nano-p4/testdata/exercise/3.1.p4:9.1-13.2: CONTROL _ID Filter `( ... `) `{ ... `}
runtime error: relation Program_ok failed

The Filter control declaration is the culprit. Remove the debug line and move on.

Step 2: Narrow down with debug

The error is somewhere inside Filter. Your job now is to find which rule in the call stack actually fails. The call stack for type-checking pass = true looks like this:

Decl_ok/controlDeclaration
  Block_ok
    Statement_ok/assignmentStatement
      Lvalue_ok/referenceExpression
        $find_var_t

You need to find where execution halts. The technique is to bracket a suspicious premise with two debug lines: one before and one after. If the second never prints, that premise is the culprit.

pass = true is an assignment. The right-hand side true is a boolean literal and is unlikely to be the source of error. The suspicious part is the left-hand side: pass is a control parameter, and variable lookup is what could plausibly fail. Open Statement_ok/assignmentStatement in 5.05-typing-statement.watsup and wrap the Lvalue_ok premise:

rule Statement_ok/assignmentStatement:
  scope TC |- lvalue '=' expression ';' -| TC
  -- debug lvalue                          ;; add before
  -- Lvalue_ok: scope TC |- lvalue : typeIR_lvalue
  -- debug lvalue                          ;; add after
  -- Expr_ok: scope TC |- expression : typeIR_expression
  -- Type_eq: typeIR_lvalue ~~ typeIR_expression

If the second debug lvalue never prints, Lvalue_ok is where the failure is. Once confirmed, remove the debug lines and move into Lvalue_ok/referenceExpression in 5.04-typing-lvalue.watsup. Its only meaningful premise is the call to $find_var_t, so that is where to look next.

Open 5.00-typing-context.watsup and look at the clauses for $find_var_t with the BLOCK tag. There are two: a hit clause (returns the found type) and a fallthrough clause (delegates to GLOBAL when the block frame has no match). Add a debug premise to the fallthrough clause to check whether pass is reaching it:

def $find_var_t(BLOCK, TC, id) = $find_var_t(GLOBAL, TC, id)
  -- debug id             ;; add this
  -- if typeFrame = TC.BLOCK.FRAME
  -- if eps = $find_map<id, varTypeIR>(typeFrame, id)

Run again. The output shows:

nano-p4/spec/5.00-typing-context.watsup:...: id
pass

pass does reach the fallthrough. That means pass was looked up in the block frame and treated as a miss. But pass is a control parameter, which lives in the block frame. Something about the hit clause must be preventing it from matching. Compare the hit clause against the fallthrough clause and the analogous GLOBAL hit clause above it.

Step 3: Fix

Remove the debug line and add the missing clause, by analogy with the GLOBAL hit clause directly above it:

def $find_var_t(BLOCK, TC, id) = varTypeIR
  -- if typeFrame = TC.BLOCK.FRAME
  -- if varTypeIR = $find_map<id, varTypeIR>(typeFrame, id)

Run the test again, and it will pass.

Worked Example: Exercise 3.2

This example uses the exercise program from Section 3.2, which assigns a Nanonet header variable to another variable of the same type.

Step 1: Run and narrow down the declaration

The error message is the same as before: Decl_ok failed, with no indication of which declaration. Apply the same debug declaration_h technique from Exercise 3.1. The last declaration printed before the error will be:

nano-p4/testdata/exercise/3.2.p4:10.1-16.2: CONTROL _ID Filter `( ... `) `{ ... `}

The Filter control declaration is the culprit.

Step 2: Narrow down with debug

The call stack for type-checking the body of Filter looks like this:

Decl_ok/controlDeclaration
  Block_ok
    Statement_ok/variableDeclaration   (for: Nanonet b = a)
      VarDecl_ok
        Type_ok
        Expr_ok
        Type_eq

Nanonet b = a declares a variable and initializes it. In VarDecl_ok, the suspicious premise is Type_eq: Type_ok resolves the declared type and Expr_ok infers the type of a, but Type_eq compares them and could silently fail if it has no rule for the types involved.

Wrap Type_eq in VarDecl_ok with two debug lines:

rule VarDecl_ok:
  scope TC_0 |- type name ('=' expression) ';' -| TC_1
  -- Type_ok: TC_0 |- type ~> typeIR
  -- Expr_ok: scope TC_0 |- expression : typeIR'
  -- debug typeIR                           ;; add before
  -- Type_eq: typeIR ~~ typeIR'
  -- debug typeIR                           ;; add after
  -- if id = $id(name)
  -- if varTypeIR = INOUT typeIR
  -- if TC_1 = $add_var_t(scope, TC_0, id, varTypeIR)

If the second debug typeIR never prints, Type_eq is the culprit. Remove the debug lines and move into Type_eq.

Step 3: Use -trace-full to see what Type_eq receives

Once you have confirmed Type_eq is failing, use -trace-full to see the actual values it receives:

./nano-p4spectec check nano-p4/spec -i nano-p4/include \
  -p nano-p4/testdata/exercise/3.2.p4 -trace-full 2>&1 | grep -A3 "Type_eq"

The relevant lines:

[ 8]                  [in: HEADER Nanonet `{ [...] `}, HEADER Nanonet `{ [...] `}]
[ 9]                     | Case analysis on typeIR

Type_eq receives two identical HEADER Nanonet values and immediately does a case analysis on typeIR, but no branch matches. The relation is receiving valid inputs; the problem is not the values but the rules. Open 5.02-typing-type.watsup and check which constructors Type_eq covers. Cross-reference against the dataTypeIR variants in 2.1-ir.watsup. One variant is missing, and it is exactly the constructor that appeared above.

Step 4: Fix

Add the missing rule by analogy with the STRUCT rule directly above it:

rule Type_eq/headerTypeIR:
  (HEADER typeId `{ _ `})
  ~~ (HEADER typeId `{ _ `})

Run the test, and it will pass.