Lab Exercise 3 - SVF-tools/Software-Security-Analysis GitHub Wiki
Lab-Exercise-3 folder layout
$tree Lab-Exercise-3
├── AEMgr.cpp
├── AEMgr.h
├── CMakeLists.txt
├── test.cpp
1. Get the latest Lab-Exercise-3 code template
cd $HOME/Software-Security-Analysis
and git pull
in your terminal to make sure you always have the latest version of the code template before coding.
* Before coding, please type If git pull
fails due to the conflict with your local changes, type git stash
to store your current code in a temporal branch and type git pull
again. If you want to retrieve your code back, type git stash pop
.
launch.json
1.1To 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
- Implement methods from
AbstractExecutionMgr::test1()
toAbstractExecutionMgr::test8()
in classAbstractExecutionMgr
inAEMgr.cpp
- Pass the test without any assertion by
test.cpp
. - Upload
AEMgr.cpp
to UNSWWebCMS
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 providedAEExampleMgr::test0()
inAEMgr.cpp
as an example to help get started.
AEMgr.cpp
only and there is NO need to modify other files under the Lab-Exercise-3 folder
*You will be working on 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;