pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '4689a2881d'
${ noResults }
infer_clone/sledge/test/analyze/global_vars.c

18 lines
342 B
Raw Normal View History Unescape

[sledge] Add globalopt pass to remove globals Summary: This adds a globalopt optimization pass to sledge. Consider code like: ``` const char *a_string = "I'm a string"; int an_int = 0; int c() { return an_int; } int main() { char *c1 = a_string; return c(); } ``` When compiled there are 2 levels of indirection. For example `return an_int` Get's compiled as ``` %0 = load i32, i32* an_int1 ret i32 %0 ``` Global opt reduces this (if `an_int` is internal) to just ` ret i32 0`. Similarly and more importantly `c1 = a_string;` get's compiled into ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" a_string = dso_local global i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i32 0, i32 0) %c1 = alloca i8*, align 8 %0 = load i8*, i8** a_string, align 8, !dbg !25 store i8* %0, i8** %c1, align 8, !dbg !24 ``` So there is a level of indirection between `c1` and `.str` where the string is stored. With global opt, this gets reduced to: ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" %c1 = alloca i8*, align 8 store i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i8** %c1, align 8, !dbg !23 ``` and `a_string` variable gets deleted. On sledge this has the effect of reducing the complexity of the symbolic heap significantly. Without this optimisation, running `sledge.dbg llvm analyze -trace Domain.call global_vars.bc` Gives prints the following segments: ``` ∧ %.str -[)-> ⟨13,{}⟩ * %a_string -[)-> ⟨8,%.str⟩ * %an_int -[)-> ⟨4,0⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩ ``` So there are `an_int` and `a_string` segments, which are redundant. with the optimisation, the heap looks like: `∧ %.str -[)-> ⟨13,{}⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩`, Where we only have the `.str` segment and the `c1` segment, which are the two we need. Reviewed By: ngorogiannis Differential Revision: D15649195 fbshipit-source-id: 5f71e56e8
6 years ago
/*
[copyright] Remove years Reviewed By: jvillard Differential Revision: D15771884 fbshipit-source-id: e2997e3a3
6 years ago
* Copyright (c) Facebook, Inc. and its affiliates.
[sledge] Add globalopt pass to remove globals Summary: This adds a globalopt optimization pass to sledge. Consider code like: ``` const char *a_string = "I'm a string"; int an_int = 0; int c() { return an_int; } int main() { char *c1 = a_string; return c(); } ``` When compiled there are 2 levels of indirection. For example `return an_int` Get's compiled as ``` %0 = load i32, i32* an_int1 ret i32 %0 ``` Global opt reduces this (if `an_int` is internal) to just ` ret i32 0`. Similarly and more importantly `c1 = a_string;` get's compiled into ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" a_string = dso_local global i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i32 0, i32 0) %c1 = alloca i8*, align 8 %0 = load i8*, i8** a_string, align 8, !dbg !25 store i8* %0, i8** %c1, align 8, !dbg !24 ``` So there is a level of indirection between `c1` and `.str` where the string is stored. With global opt, this gets reduced to: ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" %c1 = alloca i8*, align 8 store i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i8** %c1, align 8, !dbg !23 ``` and `a_string` variable gets deleted. On sledge this has the effect of reducing the complexity of the symbolic heap significantly. Without this optimisation, running `sledge.dbg llvm analyze -trace Domain.call global_vars.bc` Gives prints the following segments: ``` ∧ %.str -[)-> ⟨13,{}⟩ * %a_string -[)-> ⟨8,%.str⟩ * %an_int -[)-> ⟨4,0⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩ ``` So there are `an_int` and `a_string` segments, which are redundant. with the optimisation, the heap looks like: `∧ %.str -[)-> ⟨13,{}⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩`, Where we only have the `.str` segment and the `c1` segment, which are the two we need. Reviewed By: ngorogiannis Differential Revision: D15649195 fbshipit-source-id: 5f71e56e8
6 years ago
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
const char* a_string = "I'm a string";
int an_int = 0;
[sledge] Update tests Reviewed By: jvillard Differential Revision: D25756547 fbshipit-source-id: eecb98e6a
4 years ago
int idx() { return an_int; }
[sledge] Add globalopt pass to remove globals Summary: This adds a globalopt optimization pass to sledge. Consider code like: ``` const char *a_string = "I'm a string"; int an_int = 0; int c() { return an_int; } int main() { char *c1 = a_string; return c(); } ``` When compiled there are 2 levels of indirection. For example `return an_int` Get's compiled as ``` %0 = load i32, i32* an_int1 ret i32 %0 ``` Global opt reduces this (if `an_int` is internal) to just ` ret i32 0`. Similarly and more importantly `c1 = a_string;` get's compiled into ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" a_string = dso_local global i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i32 0, i32 0) %c1 = alloca i8*, align 8 %0 = load i8*, i8** a_string, align 8, !dbg !25 store i8* %0, i8** %c1, align 8, !dbg !24 ``` So there is a level of indirection between `c1` and `.str` where the string is stored. With global opt, this gets reduced to: ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" %c1 = alloca i8*, align 8 store i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i8** %c1, align 8, !dbg !23 ``` and `a_string` variable gets deleted. On sledge this has the effect of reducing the complexity of the symbolic heap significantly. Without this optimisation, running `sledge.dbg llvm analyze -trace Domain.call global_vars.bc` Gives prints the following segments: ``` ∧ %.str -[)-> ⟨13,{}⟩ * %a_string -[)-> ⟨8,%.str⟩ * %an_int -[)-> ⟨4,0⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩ ``` So there are `an_int` and `a_string` segments, which are redundant. with the optimisation, the heap looks like: `∧ %.str -[)-> ⟨13,{}⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩`, Where we only have the `.str` segment and the `c1` segment, which are the two we need. Reviewed By: ngorogiannis Differential Revision: D15649195 fbshipit-source-id: 5f71e56e8
6 years ago
int main() {
[sledge] Update tests Reviewed By: jvillard Differential Revision: D25756547 fbshipit-source-id: eecb98e6a
4 years ago
const char* str = a_string;
[sledge] Add globalopt pass to remove globals Summary: This adds a globalopt optimization pass to sledge. Consider code like: ``` const char *a_string = "I'm a string"; int an_int = 0; int c() { return an_int; } int main() { char *c1 = a_string; return c(); } ``` When compiled there are 2 levels of indirection. For example `return an_int` Get's compiled as ``` %0 = load i32, i32* an_int1 ret i32 %0 ``` Global opt reduces this (if `an_int` is internal) to just ` ret i32 0`. Similarly and more importantly `c1 = a_string;` get's compiled into ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" a_string = dso_local global i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i32 0, i32 0) %c1 = alloca i8*, align 8 %0 = load i8*, i8** a_string, align 8, !dbg !25 store i8* %0, i8** %c1, align 8, !dbg !24 ``` So there is a level of indirection between `c1` and `.str` where the string is stored. With global opt, this gets reduced to: ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" %c1 = alloca i8*, align 8 store i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i8** %c1, align 8, !dbg !23 ``` and `a_string` variable gets deleted. On sledge this has the effect of reducing the complexity of the symbolic heap significantly. Without this optimisation, running `sledge.dbg llvm analyze -trace Domain.call global_vars.bc` Gives prints the following segments: ``` ∧ %.str -[)-> ⟨13,{}⟩ * %a_string -[)-> ⟨8,%.str⟩ * %an_int -[)-> ⟨4,0⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩ ``` So there are `an_int` and `a_string` segments, which are redundant. with the optimisation, the heap looks like: `∧ %.str -[)-> ⟨13,{}⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩`, Where we only have the `.str` segment and the `c1` segment, which are the two we need. Reviewed By: ngorogiannis Differential Revision: D15649195 fbshipit-source-id: 5f71e56e8
6 years ago
[sledge] Update tests Reviewed By: jvillard Differential Revision: D25756547 fbshipit-source-id: eecb98e6a
4 years ago
return str[idx()];
[sledge] Add globalopt pass to remove globals Summary: This adds a globalopt optimization pass to sledge. Consider code like: ``` const char *a_string = "I'm a string"; int an_int = 0; int c() { return an_int; } int main() { char *c1 = a_string; return c(); } ``` When compiled there are 2 levels of indirection. For example `return an_int` Get's compiled as ``` %0 = load i32, i32* an_int1 ret i32 %0 ``` Global opt reduces this (if `an_int` is internal) to just ` ret i32 0`. Similarly and more importantly `c1 = a_string;` get's compiled into ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" a_string = dso_local global i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i32 0, i32 0) %c1 = alloca i8*, align 8 %0 = load i8*, i8** a_string, align 8, !dbg !25 store i8* %0, i8** %c1, align 8, !dbg !24 ``` So there is a level of indirection between `c1` and `.str` where the string is stored. With global opt, this gets reduced to: ``` @.str = private unnamed_addr constant [13 x i8] c"I'm a string\00" %c1 = alloca i8*, align 8 store i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i8** %c1, align 8, !dbg !23 ``` and `a_string` variable gets deleted. On sledge this has the effect of reducing the complexity of the symbolic heap significantly. Without this optimisation, running `sledge.dbg llvm analyze -trace Domain.call global_vars.bc` Gives prints the following segments: ``` ∧ %.str -[)-> ⟨13,{}⟩ * %a_string -[)-> ⟨8,%.str⟩ * %an_int -[)-> ⟨4,0⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩ ``` So there are `an_int` and `a_string` segments, which are redundant. with the optimisation, the heap looks like: `∧ %.str -[)-> ⟨13,{}⟩ * %c1 -[)-> ⟨8,%.str⟩ * %retval -[)-> ⟨4,0⟩`, Where we only have the `.str` segment and the `c1` segment, which are the two we need. Reviewed By: ngorogiannis Differential Revision: D15649195 fbshipit-source-id: 5f71e56e8
6 years ago
}