Lab Exercise 3 Python

1.1 launch.json

You can open Lab3.ipynb as shown in the image below. For more details, see Configuration & Debugging.

2. Lab Exercise 3 task

1. Implement methods from test1() to test8() in AEMgr.ipynb
2. Before running the test methods, execute the code cell above them to define the AEState and AbstractExecutionMgr classes
3. Upload Lab3.ipynb to UNSW WebCMS for your submission when you are finished with this lab. Your implementation will be evaluated against our internal tests. You will get the full marks if your code can pass them all. We have provided test0() as an example to help get started.

*You will be working on test code cell only and there is NO need to modify other files under the Lab-Exercise-3 folder

SVF-Python AEMgr APIs to help with your implementation SVF-Python AEMgr API.

3. Debugging

If you want to see the value of AbstractValue. You can also call toString() to print the value (either Interval Value or Address Value).

a = IntervalValue(1,1)
print(a.toString())

4. Widening and Narrowing implementation for the below loop example in lecture slides

int a = 0;
while (a < 10){
   a++;
}

def test():
    mgr = AbstractExecutionMgr()
    a = mgr.get_node_id("a")

    entry_as = AEState()
    cur_head_as = AEState()
    body_as = AEState()
    exit_as = AEState()
    widen_delay = 3
    increasing = True

    # Compose 'entry_as' (a = 0)
    entry_as[a] = IntervalValue(0, 0)

    for cur_iter in range(100):  # Upper bound to ensure fixpoint
        if cur_iter >= widen_delay:
            prev_head_as = cur_head_as.clone()

            # Join entry_as and body_as into cur_head_as
            cur_head_as = entry_as.clone()
            cur_head_as.join_with(body_as)

            if increasing:
                ae_after_widening = prev_head_as.widening(cur_head_as)
                cur_head_as = ae_after_widening.clone()

                if cur_head_as.equals(prev_head_as):
                    increasing = False
                    continue
            else:
                ae_after_narrowing = prev_head_as.narrowing(cur_head_as)
                cur_head_as = ae_after_narrowing.clone()

                if cur_head_as.equals(prev_head_as):
                    break
        else:
            cur_head_as = entry_as.clone()
            cur_head_as.join_with(body_as)

        # Loop body: condition a < 10 and then a++
        body_as = cur_head_as.clone()
        body_as[a].meet_with(IntervalValue(BoundedInt.minus_infinity(), 9))
        body_as[a] = body_as[a].getInterval() + IntervalValue(1, 1)

    # Handle loop exit: a >= 10
    exit_as = cur_head_as.clone()
    exit_as[a].meet_with(IntervalValue(10, BoundedInt.plus_infinity()))

    exit_as.print_abstract_state()

    return exit_as