-
Notifications
You must be signed in to change notification settings - Fork 142
Example uses
After deciding about the type of the analysis, we run it on some code. The code, on which the analysis runs, is LLVM IR instead of original code. You can find details on obtaining LLVM IR from C/C++ source code here and here.
We start with analyzing an easy code example.
First let us consider some short C/C++ code, saved in a file called main.cpp
that a user would like to analyze:
// main.cpp:
int main() {
int i = 1;
int j = 2;
int k = i + j;
return 0;
}
Since PhASAR's analyses run on the LLVM IR, we first generate the IR representation of the above C++ code. (The LLVM Language Reference Manual can be found here). It is very useful to make yourself familiar with the LLVM intermediate representation that all our infrastructure is based on!
Using below command, we call the clang compiler and ask it to emit the LLVM IR code, giving us the corresponding LLVM IR code of main.cpp.
Note: This command will give us the human readable version of the LLVM IR. If you don't want to inspect the IR manually, you can omit the -S
flag to get a more compact binary representation (.bc
).
$ clang++ -emit-llvm -S main.cpp
After running this command a file named main.ll
can be found within the current directory. The main.ll
should contain code similar to:
; ModuleID = './main.cpp'
source_filename = "./main.cpp"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"
; Function Attrs: mustprogress noinline norecurse nounwind optnone uwtable
define dso_local noundef i32 @main() #0 {
%1 = alloca i32, align 4
%2 = alloca i32, align 4
%3 = alloca i32, align 4
%4 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 1, i32* %2, align 4
store i32 2, i32* %3, align 4
%5 = load i32, i32* %2, align 4
%6 = load i32, i32* %3, align 4
%7 = add nsw i32 %5, %6
store i32 %7, i32* %4, align 4
ret i32 0
}
attributes #0 = { mustprogress noinline norecurse nounwind optnone uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
!llvm.module.flags = !{!0, !1, !2}
!llvm.ident = !{!3}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{i32 7, !"uwtable", i32 1}
!2 = !{i32 7, !"frame-pointer", i32 2}
!3 = !{!"clang version 14.0.6 (https://github.com/llvm/llvm-project.git f28c006a5895fc0e329fe15fead81e37457cb1d1)"}
The file to be analyzed by our commandline tool can be specified using the -m
flag. PhASAR starts the analysis at the very first instruction of the main()
function by default.
An example call to an analysis is:
$ phasar-cli -m path/to/your/main.ll -D ifds-solvertest
The above command runs an IFDS solver test on the IR contained in main.ll
.
Let us consider this slightly more complex C++ program (one that involves a function call).
int function(int x) {
return x + 1;
}
int main() {
int i = 42;
int j = function(i);
return 0;
}
The above program translates into the following IR code:
; ModuleID = './main.cpp'
source_filename = "./main.cpp"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"
; Function Attrs: mustprogress noinline nounwind optnone uwtable
define dso_local noundef i32 @_Z8functioni(i32 noundef %0) #0 {
%2 = alloca i32, align 4
store i32 %0, i32* %2, align 4
%3 = load i32, i32* %2, align 4
%4 = add nsw i32 %3, 1
ret i32 %4
}
; Function Attrs: mustprogress noinline norecurse nounwind optnone uwtable
define dso_local noundef i32 @main() #1 {
%1 = alloca i32, align 4
%2 = alloca i32, align 4
%3 = alloca i32, align 4
store i32 0, i32* %1, align 4
store i32 42, i32* %2, align 4
%4 = load i32, i32* %2, align 4
%5 = call noundef i32 @_Z8functioni(i32 noundef %4)
store i32 %5, i32* %3, align 4
ret i32 0
}
attributes #0 = { mustprogress noinline nounwind optnone uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
attributes #1 = { mustprogress noinline norecurse nounwind optnone uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" }
!llvm.module.flags = !{!0, !1, !2}
!llvm.ident = !{!3}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{i32 7, !"uwtable", i32 1}
!2 = !{i32 7, !"frame-pointer", i32 2}
!3 = !{!"clang version 14.0.6 (https://github.com/llvm/llvm-project.git f28c006a5895fc0e329fe15fead81e37457cb1d1)"}
Running the ifds-solvertest
analysis on the above IR produces the following IFDS/IDE results (which are quite different from the intra/inter monotone framework results that are completely self-explaining. For that reason, we omit their explanation here.):
$ ./tools/phasar-cli/phasar-cli -m main.ll -D ifds-solvertest --emit-raw-results
PhASAR v0323
A LLVM-based static analysis framework
No text report available!
***************************************************************
* Raw IDESolver results *
***************************************************************
============ Results for function '_Z8functioni' ============
N: %2 = alloca i32, align 4, !psr.id !4 | ID: 0
-----------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: store i32 %0, i32* %2, align 4, !psr.id !5 | ID: 1
-----------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %3 = load i32, i32* %2, align 4, !psr.id !6 | ID: 2
------------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %4 = add nsw i32 %3, 1, !psr.id !7 | ID: 3
---------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: ret i32 %4, !psr.id !8 | ID: 4
---------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
============ Results for function 'main' ============
N: %1 = alloca i32, align 4, !psr.id !9 | ID: 5
-----------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %2 = alloca i32, align 4, !psr.id !10 | ID: 6
------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %3 = alloca i32, align 4, !psr.id !11 | ID: 7
------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: store i32 0, i32* %1, align 4, !psr.id !12 | ID: 8
-----------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: store i32 42, i32* %2, align 4, !psr.id !13 | ID: 9
------------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %4 = load i32, i32* %2, align 4, !psr.id !14 | ID: 10
--------------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: %5 = call noundef i32 @_Z8functioni(i32 noundef %4), !psr.id !15 | ID: 11
----------------------------------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: store i32 %5, i32* %3, align 4, !psr.id !16 | ID: 12
-------------------------------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
N: ret i32 0, !psr.id !17 | ID: 13
----------------------------------
D: @zero_value = constant i2 0, align 4 | ID: -1 | V: BOTTOM
In the IFDS/IDE results, for each program statement
Note: When running IFDS analysis, only BOTTOM
is shown that just indicates the presence of the dataflow fact as IFDS (in contrast to IDE) does not allow for computing values on dataflow edges.
Additionally to the results, PhASAR is able to record all edges from the exploded super-graph that the computation is based on. The edges reside in two edge recorders (for intra- and inter-procedural edges) inside the IDESolver implementation.
Here is a visualization of an exploded super-graph of a different analysis to give you an impression of how it looks like.
More examples can be found here.
- Home
- Reference Material
- Getting Started:
- Building PhASAR
- Using PhASAR with Docker
- A few uses of PhASAR
- Coding Conventions
- Contributing to PhASAR
- Errors and bug reporting
- Update to Newer LLVM Versions
- OS Support