Paper

Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering

Note: This work has been merged into SVF.

Guidance

Step 1: Clone SVF Repository and Build

Run this script to clone SVF to your local machine:

git clone https://github.com/SVF-tools/SVF.git
cd SVF

Run the build script to set up the LLVM and Z3 environments and build SVF:

source ./build.sh

• By default, the build is in release mode.
• For debug mode, run:

source ./build.sh debug

Note: Ensure the script is executed with source to properly configure the environment.

Step 2: Clone RecTopo Repository

Clone the RecTopo repository to your local machine:

git clone https://github.com/JoelYYoung/RecTopo.git
cd RecTopo

Step 3: Analyzing bc using ae executable

There are three recursion handling modes:

1. widen-narrow: Applies both widening and narrowing at the cycle head of recursive functions.
2. widen-only: Applies only widening at the cycle head of recursive functions.
3. top: Assigns the top value to return values and any stored object pointed by q at *q = p in recursive functions.

Analyze programs involving recursive functions:

ae -handle-recur=<recursion handling mode> <bc path>

Example 1: Analyzing recur.c program

Source Code

#include "stdbool.h"
extern void svf_print(int, char*);

int demo(int a) {
    if (a >= 10000)
        return a;
    demo(a+1);
}

int main() {
    int result = demo(0);
    svf_print(result, "result");
}

Analysis

Analyze recur.bc in widen-narrow mode:

ae -handle-recur=widen-narrow ./recur.bc

Output

In this mode, the analysis yields:

Text: result, Value: ValVar ID: 55
   %3 = load i32, ptr %1, align 4 , PrintVal: [10000, 10000], Loc:CallICFGNode: 

The output indicates that in this mode, the interval for result is [10000, 10000]. The interval of parameter a is first widened to [10000, +∞], and then narrowed to [10000, 10000] based on the path condition of the second if branch. For comparison:

• In widen-only mode, the interval for result is [10000, +∞].
• In top mode, the interval for result is [-∞, +∞].

Example 2: Analyzing mc91.c program

Source Code

#include "stdbool.h"
extern void svf_print(int, char*);

int mc91(int p){
    if(p > 100){
        return p - 10;
    }else{
        int p1 = p + 11;
        int p2 = mc91(p1);
        int result = mc91(p2);
        return result;
    }
}

int main(){
    int result = mc91(40);
    svf_print(result, "result");
}

Analysis

Analyze mc91.bc in widen-narrow mode:

ae -handle-recur=widen-narrow ./mc91.bc

Output

In this mode, the analysis yields:

Text: result, Value: ValVar ID: 74
   %3 = load i32, ptr %1, align 4 , PrintVal: [91, +∞], Loc:CallICFGNode: 

The output indicates that the interval for result is [91, +∞].

Example 3: Analyzing id.c program

Source Code

#include "stdbool.h"
#include "stdio.h"
extern void svf_print(int, char*);

unsigned int id(unsigned int x) {
    if (x==0) return 0;
    unsigned int ret = id(x-1) + 1;
    if (ret > 2) return 2;
    return ret;
}

int main(){
    int x;
    scanf("%ud", &x);

    int result = id(x);
    svf_print(result, "result");
}

Analysis

Analyze id.bc in widen-narrow mode:

ae -handle-recur=widen-narrow ./id.bc

Output

In this mode, the analysis yields:

Text: result, Value: ValVar ID: 77
   %6 = load i32, ptr %2, align 4 , PrintVal: [0, 2], Loc:CallICFGNode:

The output indicates that the interval for result is [0, 2].