Bounded for loops with global bounds

[shyukahn]

This PR implements a global bound for 3-clause for loops to guarantee boundedness.

Bounded for loops with global bounds

In general, 3-clause for loops are not guaranteed to terminate within a finite amount of time. To guarantee their boundedness, a global bound is implemented. This adds a constraint to the total number of iterations of all 3-clause for loops in a P4 program execution.

To keep track of the total number of iterations, a loop counter variable is added to evalContext:

syntax evalContext =
  { GLOBAL globalEvalLayer,
    BLOCK blockEvalLayer,
    LOCAL localEvalLayer,
    COUNT nat }

The loop bound is defined as 1000 for now.

def $loop_bound = 1000

update_loop_count_e() is a helper function that increments the loop counter in the context. It also checks whether the counter exceeds the global bound.

dec $update_loop_count_e(evalContext) : evalContext?

def $update_loop_count_e(EC) = EC[ .COUNT = $(EC.COUNT + 1) ]
  -- if $(EC.COUNT < $loop_bound)
def $update_loop_count_e(EC) = eps
  -- otherwise

relation ForThreeClauseLoop_eval calls this function on each iteration.

rule ForThreeClauseLoop_eval/cond-true-loop-cont-update-cont:
    EC_0 STO_0 |- typedExpressionIR statementIR forUpdateStatementListIR
                : EC_5 STO_4 statementResult
    -- ...
    -- if EC_4 = $update_loop_count_e(EC_3)
    -- ForThreeClauseLoop_eval:
        EC_4 STO_3 |- typedExpressionIR statementIR forUpdateStatementListIR
                    : EC_5 STO_4 statementResult

Additionally, rules implementing the relation Call_eval are modified to capture the iterations executed in callees' bodies by using the helper function $merge_loop_count_e().

Testcase

testdata/custom/for-global-bound.p4 is a testcase that satisfies the constraints.

bit<32> foo()
{
    bit <32> n = 0;
    for (bit<32> i = 0; i < 10; i = i + 1) {
        n = n + i;
    }
    return n;
}

control ingressImpl(inout headers_t hdr,
                    inout metadata_t meta,
                    inout standard_metadata_t stdmeta)
{
    bit<8> n = hdr.ethernet.srcAddr[15:8];
    bit<8> i;
    apply {
        for (i = 0; i < 5; i = i + 1) {
            n = (bit<8>) foo();
        }
        for (i = 0; i < 5; i = i + 1) {
            for (bit<8> j = 0; j < 5; j = j + 1) {
                n = (bit<8>) foo();
            }
        }
        hdr.ethernet.srcAddr[7:0] = (bit<8>) i;
        hdr.ethernet.srcAddr[15:8] = n;
        stdmeta.egress_spec = 1;
    }
}

Since the number of total iterations is less than 1000, this is considered a legal program. However, for example, if the for loop in foo() is modified to iterate 100 times instead of 10, the number of total iterations would be greater than 1000 and this would be considered as an error.