Lab Exercise 3 CPP

1.1 launch.json

To enable debugging and running, switch your executable by setting the program and args fields as described here or follow the below screenshot.

2. Lab Exercise 3 task

1. Implement methods from AbstractExecutionMgr::test1() to AbstractExecutionMgr::test8() in class AbstractExecutionMgr in AEMgr.cpp
2. Pass the test without any assertion by test.cpp.
3. Upload AEMgr.cpp 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 AEExampleMgr::test0() in AEMgr.cpp as an example to help get started.

*You will be working on AEMgr.cpp only and there is NO need to modify other files under the Lab-Exercise-3 folder

SVF AEMgr APIs to help with your implementation SVF 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).

int main() {
    AbstractValue a = IntervalValue(1, 1);
    std::cout << a.toString() << std::end;
}

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

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

		AEState entry_as;
		AEState cur_head_as;
		AEState body_as;
		AEState exit_as;
		u32_t widen_delay = 3;

		// Compose 'entry_as' (a = 0)
		NodeID a = getNodeID("a");
		entry_as[a] = IntervalValue(0, 0);
		bool increasing = true;

		for (int cur_iter = 0;; ++cur_iter) {

			if (cur_iter >= widen_delay) {
				// Handle widening and narrowing after widen_delay
				AEState prev_head_as = cur_head_as;

				// Update head's state by joining with 'entry_as' and 'body_as'
				cur_head_as = entry_as;
				cur_head_as.joinWith(body_as);
				if (increasing) { // Widening phase
					AEState as_after_widening = prev_head_as.widening(cur_head_as);
					cur_head_as = as_after_widening;

				    if (cur_head_as == prev_head_as) {
					    increasing = false;
					    continue;
				    }

				} else { // Narrow phase after widening
					AEState as_after_narrowing = prev_head_as.narrowing(cur_head_as);
					cur_head_as = as_after_narrowing;
					if (cur_head_as == prev_head_as) { //fix-point reached
						break;
					}
				}
			}
			else { // Handle widen delay
				// Handle widen_delay,update cycle head's state
				// via joining entry_as and body_as
				cur_head_as = entry_as;
				cur_head_as.joinWith(body_as);
			}
			// Handle loop body
			// Propagate head_as to loop body
			body_as = cur_head_as;
			// process loop body (a <10)
			body_as[a].meet_with(IntervalValue(IntervalValue::minus_infinity(),9));
			body_as[a] = body_as[a].getInterval() + IntervalValue(1, 1);

		}
		// Handle loop exit
		// Propagate head_as to loop exit
		exit_as = cur_head_as;
		// process the loop exit condition (a>=10)
		exit_as[a].meet_with(IntervalValue(10,IntervalValue::plus_infinity()));

		exit_as.printAbstractState();
		return exit_as;