Bounded for loops with local bounds

[shyukahn]

This PR implements a local bound for each 3-clause for loop to guarantee boundedness.

Bounded for loops with local bounds

In general, 3-clause for loops are not guaranteed to terminate within a finite amount of time. To guarantee their boundedness, a local bound is implemented, which adds a constraint to the maximum number of iterations of each 3-clause for loop.

relation ForThreeClauseLoop_eval accepts one more input parameter, which indicates the current number of iterations.

relation ForThreeClauseLoop_eval:
  evalContext store nat |- typedExpressionIR statementIR forUpdateStatementListIR
                         : evalContext store statementResult
  hint(input %0 %1 %2 %3 %4 %5)

For each iteration, the number of iterations is incremented by one, and is also checked whether it exceeds the loop bound.

rule ForThreeClauseLoop_eval/cond-true-loop-cont-update-cont:
    EC_0 STO_0 n |- typedExpressionIR statementIR forUpdateStatementListIR
                  : EC_4 STO_4 statementResult
    -- ...
    -- if $(n < $loop_bound)
    -- ForThreeClauseLoop_eval: 
        EC_3 STO_3 $(n + 1) |- typedExpressionIR statementIR forUpdateStatementListIR
                             : EC_4 STO_4 statementResult

The loop bound is defined as 1000 for now.

def $loop_bound = 1000

Testcase

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

bit<32> foo()
{
    bit <32> n = 0;
    for (bit<32> i = 0; i < 500; 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();
        }
        hdr.ethernet.srcAddr[7:0] = (bit<8>) i;
        hdr.ethernet.srcAddr[15:8] = n;
        stdmeta.egress_spec = 1;
    }
}

foo() contains a for loop which iterates less than 1000 times. Calling foo() within another loop causes the loop body in foo() to be executed more than 1000 times, but since the local bound of each loop is considered independently, this is considered a legal program.