Skip to content

Commit e367768

Browse files
author
bjjwwang
committed
update ass4
1 parent 2eb6e28 commit e367768

File tree

5 files changed

+90
-45
lines changed

5 files changed

+90
-45
lines changed

‎Assignment-4/Tests/testcases/sse/test3.c‎

Lines changed: 8 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,13 @@
1-
2-
// CHECK: ^sat$
3-
4-
extern int nd(void);
5-
61
#include "stdbool.h"
7-
2+
//ADDR, LOAD, STORE, CAST(COPY)
83
extern void svf_assert(bool);
94

10-
int main() {
11-
int x, y;
12-
x = 1;
13-
y = 1;
5+
void foo(int* p) {
6+
*p = 1;
7+
}
148

15-
if (nd()) {
16-
x++;
17-
y++;
18-
}
19-
svf_assert(x == y);
20-
return 0;
9+
int main() {
10+
int a = 0;
11+
foo(&a);
12+
svf_assert(a == 1);
2113
}

‎Assignment-4/Tests/testcases/sse/test3.ll‎

Lines changed: 27 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,38 @@
1-
; ModuleID = 'test14.ll'
2-
source_filename = "test14.c"
3-
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
4-
target triple = "arm64-apple-macosx14.0.0"
1+
; ModuleID = 'test5.ll'
2+
source_filename = "test5.c"
3+
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
4+
target triple = "aarch64-unknown-linux-gnu"
55

6-
; Function Attrs: noinline nounwind ssp uwtable(sync)
7-
define i32 @main() #0 {
6+
; Function Attrs: noinline nounwind uwtable
7+
define dso_local void @foo(ptr noundef %p) #0 {
88
entry:
9-
%call = call i32 @nd()
10-
%tobool = icmp ne i32 %call, 0
11-
br i1 %tobool, label %if.then, label %if.end
12-
13-
if.then: ; preds = %entry
14-
%inc = add nsw i32 1, 1
15-
%inc1 = add nsw i32 1, 1
16-
br label %if.end
9+
store i32 1, ptr %p, align 4
10+
ret void
11+
}
1712

18-
if.end: ; preds = %if.then, %entry
19-
%x.0 = phi i32 [ %inc, %if.then ], [ 1, %entry ]
20-
%y.0 = phi i32 [ %inc1, %if.then ], [ 1, %entry ]
21-
%cmp = icmp eq i32 %x.0, %y.0
22-
call void @svf_assert(i1 noundef zeroext %cmp)
13+
; Function Attrs: noinline nounwind uwtable
14+
define dso_local i32 @main() #0 {
15+
entry:
16+
%a = alloca i32, align 4
17+
store i32 0, ptr %a, align 4
18+
call void @foo(ptr noundef %a)
19+
%0 = load i32, ptr %a, align 4
20+
%cmp = icmp eq i32 %0, 1
21+
call void @svf_assert(i1 noundef %cmp)
2322
ret i32 0
2423
}
2524

26-
declare i32 @nd() #1
27-
28-
declare void @svf_assert(i1 noundef zeroext) #1
25+
declare void @svf_assert(i1 noundef) #1
2926

30-
attributes #0 = { noinline nounwind ssp uwtable(sync) "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+sha3,+sm4,+v8.1a,+v8.2a,+v8.3a,+v8.4a,+v8.5a,+v8a,+zcm,+zcz" }
31-
attributes #1 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+sha3,+sm4,+v8.1a,+v8.2a,+v8.3a,+v8.4a,+v8.5a,+v8a,+zcm,+zcz" }
27+
attributes #0 = { noinline nounwind uwtable "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="generic" "target-features"="+fp-armv8,+neon,+outline-atomics,+v8a,-fmv" }
28+
attributes #1 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="generic" "target-features"="+fp-armv8,+neon,+outline-atomics,+v8a,-fmv" }
3229

33-
!llvm.module.flags = !{!0, !1, !2, !3}
34-
!llvm.ident = !{!4}
30+
!llvm.module.flags = !{!0, !1, !2, !3, !4}
31+
!llvm.ident = !{!5}
3532

3633
!0 = !{i32 1, !"wchar_size", i32 4}
3734
!1 = !{i32 8, !"PIC Level", i32 2}
38-
!2 = !{i32 7, !"uwtable", i32 1}
39-
!3 = !{i32 7, !"frame-pointer", i32 1}
40-
!4 = !{!"Homebrew clang version 16.0.6"}
35+
!2 = !{i32 7, !"PIE Level", i32 2}
36+
!3 = !{i32 7, !"uwtable", i32 2}
37+
!4 = !{i32 7, !"frame-pointer", i32 1}
38+
!5 = !{!"clang version 16.0.4 (https://github.com/bjjwwang/LLVM-compile aed81d25b4818ed2645b53ffaed7664c1437b458)"}

‎Assignment-4/Tests/testcases/sse/test4.c‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include "stdbool.h"
2+
//ADDR, LOAD, STORE, CAST(COPY)
3+
extern void svf_assert(bool);
4+
5+
int main(){
6+
int x = 1, y = 1;
7+
int a = 1, b = 2;
8+
if (a > b) {
9+
y++;
10+
} else {
11+
x++;
12+
svf_assert (x == 2);
13+
}
14+
return 0;
15+
}

‎Assignment-4/Tests/testcases/sse/test4.ll‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
; ModuleID = 'test6.ll'
2+
source_filename = "test6.c"
3+
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
4+
target triple = "aarch64-unknown-linux-gnu"
5+
6+
; Function Attrs: noinline nounwind uwtable
7+
define dso_local i32 @main() #0 {
8+
entry:
9+
%cmp = icmp sgt i32 1, 2
10+
br i1 %cmp, label %if.then, label %if.else
11+
12+
if.then: ; preds = %entry
13+
%inc = add nsw i32 1, 1
14+
br label %if.end
15+
16+
if.else: ; preds = %entry
17+
%inc1 = add nsw i32 1, 1
18+
%cmp2 = icmp eq i32 %inc1, 2
19+
call void @svf_assert(i1 noundef %cmp2)
20+
br label %if.end
21+
22+
if.end: ; preds = %if.else, %if.then
23+
ret i32 0
24+
}
25+
26+
declare void @svf_assert(i1 noundef) #1
27+
28+
attributes #0 = { noinline nounwind uwtable "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="generic" "target-features"="+fp-armv8,+neon,+outline-atomics,+v8a,-fmv" }
29+
attributes #1 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="generic" "target-features"="+fp-armv8,+neon,+outline-atomics,+v8a,-fmv" }
30+
31+
!llvm.module.flags = !{!0, !1, !2, !3, !4}
32+
!llvm.ident = !{!5}
33+
34+
!0 = !{i32 1, !"wchar_size", i32 4}
35+
!1 = !{i32 8, !"PIC Level", i32 2}
36+
!2 = !{i32 7, !"PIE Level", i32 2}
37+
!3 = !{i32 7, !"uwtable", i32 2}
38+
!4 = !{i32 7, !"frame-pointer", i32 1}
39+
!5 = !{!"clang version 16.0.4 (https://github.com/bjjwwang/LLVM-compile aed81d25b4818ed2645b53ffaed7664c1437b458)"}

‎Assignment-4/test-sse.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ int main(int argc, char** argv) {
5050
icfg->dump(moduleNameVec[0] + ".icfg");
5151

5252
SSE* sse = new SSE(svfir, icfg);
53+
sse->addToSolver(sse->getZ3Expr(0) == 0);
5354
sse->analyse();
5455

5556
SVF::LLVMModuleSet::releaseLLVMModuleSet();

0 commit comments

Comments
 (0)