Skip to content

Commit 358829c

Browse files
author
Daniel Kroening
authored
Merge pull request #1510 from tautschnig/always-inline
Fully process always_inline
2 parents 3e77dd6 + 2afe377 commit 358829c

13 files changed

+159
-2
lines changed
+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// this is a GCC extension
2+
3+
#ifdef __GNUC__
4+
static inline __attribute__((always_inline))
5+
_Bool __is_kfree_rcu_offset(unsigned long offset)
6+
{
7+
return offset < 4096;
8+
}
9+
10+
static inline __attribute__((always_inline))
11+
void kfree_rcu(unsigned long offset)
12+
{
13+
((void)sizeof(char[1 - 2*!!(!__builtin_constant_p(offset))]));
14+
15+
((void)sizeof(char[1 - 2*!!(!__is_kfree_rcu_offset(offset))]));
16+
}
17+
18+
static inline __attribute__((always_inline))
19+
void unused(unsigned long offset)
20+
{
21+
((void)sizeof(char[1 - 2*!!(!__builtin_constant_p(offset))]));
22+
}
23+
#endif
24+
25+
int main()
26+
{
27+
#ifdef __GNUC__
28+
kfree_rcu(42);
29+
#endif
30+
31+
return 0;
32+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

src/ansi-c/ansi_c_convert_type.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
155155
c_storage_spec.is_register=true;
156156
else if(type.id()==ID_weak)
157157
c_storage_spec.is_weak=true;
158+
else if(type.id()==ID_always_inline)
159+
c_storage_spec.is_always_inline=true;
158160
else if(type.id()==ID_auto)
159161
{
160162
// ignore

src/ansi-c/ansi_c_declaration.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,8 @@ void ansi_c_declarationt::output(std::ostream &out) const
8181
out << " is_extern";
8282
if(get_is_static_assert())
8383
out << " is_static_assert";
84+
if(get_is_always_inline())
85+
out << " is_always_inline";
8486
out << "\n";
8587

8688
out << "Type: " << type().pretty() << "\n";
@@ -164,6 +166,9 @@ void ansi_c_declarationt::to_symbol(
164166
symbol.is_extern=false;
165167
else if(get_is_extern()) // traditional GCC
166168
symbol.is_file_local=true;
169+
170+
if(get_is_always_inline())
171+
symbol.is_macro=true;
167172
}
168173
}
169174
}

src/ansi-c/ansi_c_declaration.h

+10
Original file line numberDiff line numberDiff line change
@@ -195,6 +195,16 @@ class ansi_c_declarationt:public exprt
195195
set(ID_is_weak, is_weak);
196196
}
197197

198+
bool get_is_always_inline() const
199+
{
200+
return get_bool(ID_is_always_inline);
201+
}
202+
203+
void set_is_always_inline(bool is_always_inline)
204+
{
205+
set(ID_is_always_inline, is_always_inline);
206+
}
207+
198208
void to_symbol(
199209
const ansi_c_declaratort &,
200210
symbolt &symbol) const;

src/ansi-c/c_storage_spec.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ void c_storage_spect::read(const typet &type)
3232
is_register=true;
3333
else if(type.id()==ID_weak)
3434
is_weak=true;
35+
else if(type.id()==ID_always_inline)
36+
is_always_inline=true;
3537
else if(type.id()==ID_auto)
3638
{
3739
// ignore

src/ansi-c/c_storage_spec.h

+4-1
Original file line numberDiff line numberDiff line change
@@ -35,13 +35,14 @@ class c_storage_spect
3535
is_register=false;
3636
is_inline=false;
3737
is_weak=false;
38+
is_always_inline=false;
3839
alias.clear();
3940
asm_label.clear();
4041
section.clear();
4142
}
4243

4344
bool is_typedef, is_extern, is_static, is_register,
44-
is_inline, is_thread_local, is_weak;
45+
is_inline, is_thread_local, is_weak, is_always_inline;
4546

4647
// __attribute__((alias("foo")))
4748
irep_idt alias;
@@ -59,6 +60,7 @@ class c_storage_spect
5960
is_thread_local==other.is_thread_local &&
6061
is_inline==other.is_inline &&
6162
is_weak==other.is_weak &&
63+
is_always_inline==other.is_always_inline &&
6264
alias==other.alias &&
6365
asm_label==other.asm_label &&
6466
section==other.section;
@@ -78,6 +80,7 @@ class c_storage_spect
7880
is_inline |=other.is_inline;
7981
is_thread_local |=other.is_thread_local;
8082
is_weak |=other.is_weak;
83+
is_always_inline|=other.is_always_inline;
8184
if(alias.empty())
8285
alias=other.alias;
8386
if(asm_label.empty())

src/ansi-c/c_typecheck_base.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -688,6 +688,7 @@ void c_typecheck_baset::typecheck_declaration(
688688
declaration.set_is_register(full_spec.is_register);
689689
declaration.set_is_typedef(full_spec.is_typedef);
690690
declaration.set_is_weak(full_spec.is_weak);
691+
declaration.set_is_always_inline(full_spec.is_always_inline);
691692

692693
symbolt symbol;
693694
declaration.to_symbol(*d_it, symbol);

src/ansi-c/c_typecheck_expr.cpp

+71-1
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/std_expr.h>
2525
#include <util/pointer_offset_size.h>
2626
#include <util/pointer_predicates.h>
27+
#include <util/replace_symbol.h>
2728

2829
#include "c_typecast.h"
2930
#include "c_qualifiers.h"
@@ -1913,7 +1914,10 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
19131914
if(entry!=asm_label_map.end())
19141915
identifier=entry->second;
19151916

1916-
if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1917+
symbol_tablet::symbolst::const_iterator sym_entry=
1918+
symbol_table.symbols.find(identifier);
1919+
1920+
if(sym_entry==symbol_table.symbols.end())
19171921
{
19181922
// This is an undeclared function. Let's just add it.
19191923
// We do a bit of return-type guessing, but just a bit.
@@ -1945,6 +1949,72 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
19451949
warning().source_location=f_op.find_source_location();
19461950
warning() << "function `" << identifier << "' is not declared" << eom;
19471951
}
1952+
else if(sym_entry->second.type.get_bool(ID_C_inlined) &&
1953+
sym_entry->second.is_macro &&
1954+
sym_entry->second.value.is_not_nil())
1955+
{
1956+
// calling a function marked as always_inline
1957+
const symbolt &func_sym=sym_entry->second;
1958+
const code_typet &func_type=to_code_type(func_sym.type);
1959+
1960+
replace_symbolt replace;
1961+
1962+
const code_typet::parameterst &parameters=func_type.parameters();
1963+
auto p_it=parameters.begin();
1964+
for(const auto &arg : expr.arguments())
1965+
{
1966+
if(p_it==parameters.end())
1967+
{
1968+
err_location(f_op);
1969+
error() << "function call has additional arguments, "
1970+
<< "cannot apply always_inline" << eom;
1971+
throw 0;
1972+
}
1973+
1974+
irep_idt p_id=p_it->get_identifier();
1975+
if(p_id.empty())
1976+
p_id=
1977+
id2string(func_sym.base_name)+"::"+
1978+
id2string(p_it->get_base_name());
1979+
replace.insert(p_id, arg);
1980+
1981+
++p_it;
1982+
}
1983+
1984+
if(p_it!=parameters.end())
1985+
{
1986+
err_location(f_op);
1987+
error() << "function call has missing arguments, "
1988+
<< "cannot apply always_inline" << eom;
1989+
throw 0;
1990+
}
1991+
1992+
codet body=to_code(func_sym.value);
1993+
replace(body);
1994+
1995+
side_effect_exprt side_effect_expr(
1996+
ID_statement_expression, func_type.return_type());
1997+
body.make_block();
1998+
1999+
// simulates parts of typecheck_function_body
2000+
typet cur_return_type=return_type;
2001+
return_type=func_type.return_type();
2002+
typecheck_code(body);
2003+
return_type.swap(cur_return_type);
2004+
2005+
// replace final return by an ID_expression
2006+
codet &last=to_code_block(body).find_last_statement();
2007+
2008+
if(last.get_statement()==ID_return)
2009+
last.set_statement(ID_expression);
2010+
2011+
side_effect_expr.copy_to_operands(body);
2012+
typecheck_side_effect_statement_expression(side_effect_expr);
2013+
2014+
expr.swap(side_effect_expr);
2015+
2016+
return;
2017+
}
19482018
}
19492019

19502020
// typecheck it now

src/ansi-c/parser.y

+3
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,7 @@ extern char *yyansi_ctext;
142142
%token TOK_GCC_ATTRIBUTE_NORETURN "noreturn"
143143
%token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor"
144144
%token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor"
145+
%token TOK_GCC_ATTRIBUTE_ALWAYS_INLINE "always_inline"
145146
%token TOK_GCC_LABEL "__label__"
146147
%token TOK_MSC_ASM "__asm"
147148
%token TOK_MSC_BASED "__based"
@@ -1531,6 +1532,8 @@ gcc_type_attribute:
15311532
{ $$=$1; set($$, ID_constructor); }
15321533
| TOK_GCC_ATTRIBUTE_DESTRUCTOR
15331534
{ $$=$1; set($$, ID_destructor); }
1535+
| TOK_GCC_ATTRIBUTE_ALWAYS_INLINE
1536+
{ $$=$1; set($$, ID_always_inline); }
15341537
;
15351538

15361539
gcc_attribute:

src/ansi-c/scanner.l

+3
Original file line numberDiff line numberDiff line change
@@ -1537,6 +1537,9 @@ __decltype { if(PARSER.cpp98 &&
15371537
"destructor" |
15381538
"__destructor__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_DESTRUCTOR; }
15391539

1540+
"always_inline" |
1541+
"__always_inline__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_ALWAYS_INLINE; }
1542+
15401543
{ws} { /* ignore */ }
15411544
{newline} { /* ignore */ }
15421545
{identifier} { BEGIN(GCC_ATTRIBUTE4); }

src/util/irep_ids.def

+2
Original file line numberDiff line numberDiff line change
@@ -830,6 +830,8 @@ IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
830830
IREP_ID_TWO(generic_types, #generic_types)
831831
IREP_ID_TWO(type_variables, #type_variables)
832832
IREP_ID_ONE(havoc_object)
833+
IREP_ID_ONE(always_inline)
834+
IREP_ID_ONE(is_always_inline)
833835

834836
#undef IREP_ID_ONE
835837
#undef IREP_ID_TWO

src/util/replace_symbol.cpp

+16
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,16 @@ bool replace_symbolt::replace(
104104
result=false;
105105
}
106106

107+
const irept &type_arg=dest.find(ID_type_arg);
108+
109+
if(type_arg.is_not_nil())
110+
{
111+
typet &type=static_cast<typet &>(dest.add(ID_type_arg));
112+
113+
if(!replace(type))
114+
result=false;
115+
}
116+
107117
const irept &va_arg_type=dest.find(ID_C_va_arg_type);
108118

109119
if(va_arg_type.is_not_nil())
@@ -139,6 +149,12 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const
139149
if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
140150
return true;
141151

152+
const irept &type_arg=dest.find(ID_type_arg);
153+
154+
if(type_arg.is_not_nil())
155+
if(have_to_replace(static_cast<const typet &>(type_arg)))
156+
return true;
157+
142158
const irept &va_arg_type=dest.find(ID_C_va_arg_type);
143159

144160
if(va_arg_type.is_not_nil())

0 commit comments

Comments
 (0)