Fully process always_inline (second attempt) #1898

tautschnig · 2018-03-01T15:41:38Z

This was previously proposed and merged in #1510, but had to be reverted in #1527. #1519 then provided an additional test, which is now included (together with the fix).

smowton

Some questions inline. Also, why do we have this at all? Surely always-inline is an optimisation that we could reasonably ignore?

smowton · 2018-03-03T15:44:43Z

regression/ansi-c/always_inline1/main.c

+// this is a GCC extension
+
+#ifdef __GNUC__
+static inline __attribute__((always_inline)) _Bool


Could you minimise this test-case so it's clearer which parts are crucial to the test and which is unrelated stuff the kernel's RCU code happens to do? If you want to keep the real-world example you could include this as a block comment, then use a simplified version for the actual test?

Actually everything is necessary here, but I'll add comments to explain why/what it is testing.

smowton · 2018-03-03T15:45:27Z

regression/ansi-c/always_inline1/test.desc

+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$


Add a comment to the test specifying why we expect an error

smowton · 2018-03-03T15:49:18Z

src/ansi-c/c_typecheck_expr.cpp

+      sym_entry->second.type.get_bool(ID_C_inlined) &&
+      sym_entry->second.is_macro && sym_entry->second.value.is_not_nil())
+    {
+      // calling a function marked as always_inline


Or, presumably, a macro? Or is the is_macro flag only used for functions that are not in fact macros?

Yes, is_macro isn't ever used with (preprocessor) macros.

smowton · 2018-03-03T15:50:12Z

src/ansi-c/c_typecheck_expr.cpp

+        if(p_it == parameters.end())
+        {
+          err_location(f_op);
+          error() << "function call has additional arguments, "


More arguments than parameters, i.e. varargs?

smowton · 2018-03-03T15:52:57Z

src/ansi-c/c_typecheck_expr.cpp

+      typecheck_code(body);
+      return_type.swap(cur_return_type);
+
+      // replace final return by an ID_expression


Could there be other returns? If so what happens?

It's unsupported - now it's being tested for and reported.

smowton · 2018-03-03T15:54:58Z

src/ansi-c/c_typecheck_expr.cpp

+      }
+
+      codet body = to_code(func_sym.value);
+      replace(body);


So this will replace formal parameters with actuals, but not actually cause locals to alias because they retain the qualified names (f::1::x vs. g::1::x) they had originally? That seems right for inlining but wrong for macros?

As said above, we don't actually do preprocessor macros in this way, so it should be fine.

smowton · 2018-03-03T16:03:33Z

Gah, sorry, I understand now -- this code is trying to cause a compile error if it can't prove something is constant?

tautschnig · 2018-03-04T16:42:17Z

Gah, sorry, I understand now -- this code is trying to cause a compile error if it can't prove something is constant?

Yes, I believe that's the way that some code in the Linux kernel uses it.

tautschnig · 2018-03-04T16:44:15Z

@smowton Thanks a lot for all the comments, I will carefully review my code to come up with proper answers or fixes.

smowton

This looks good except that using "macro" to refer to things that are not macros, and never to refer to things that are macros, is maddening. Please change this if at all possible.

smowton · 2018-04-17T11:30:07Z

src/ansi-c/ansi_c_declaration.cpp

@@ -164,6 +166,9 @@ void ansi_c_declarationt::to_symbol(
          symbol.is_extern=false;
        else  if(get_is_extern()) // traditional GCC
          symbol.is_file_local=true;
+
+        if(get_is_always_inline())
+          symbol.is_macro = true;


Can we please rename this then? It's really confusing that things annotated is_macro and things that are macros are disjoint (!)

I also note we have symbolt::is_function which returns false if is_macro is set!

Upon further thought I'm inclined to say that is_macro actually is the right terminology for all the current uses: all of them (typedefs, enum values, linker aliases, always-inline functions) are names with some value (which might be code) behind them and need to be expanded in place in order to evaluate the expression or statement they are involved in. We currently consume code after the C/C++ preprocessor has been run, so those kinds of "macros" are not currently seen - but actually, if they were, they would fit the very same definition and would likely be marked as such.

This is used int the precursor of a typechecked sizeof expression.

The Linux kernel uses tests on __builtin_constant_p that are required to evalute to true for compilationt to succeed. These can only evaluate to true when inlining is actually done (and expressions are simplified).

Macros are as local as types; we use macros for always-inlined functions, and contained symbols never end up in the symbol table. Thus macros must be removed before attempting to recurse into them for the purpose of symbol-table cleanup.

allredj

Passed Diffblue compatibility checks (cbmc commit: 688a0ab).

Partial revert of #1898 (always_inline support, second attempt)

8a7893c Merge pull request diffblue#2375 from diffblue/unit-dependencies 9258284 fix build depenencies of unit test binary f7cd161 Merge pull request diffblue#2371 from diffblue/fix-tests2 82753bc make test independent of index type f5f32da Merge pull request diffblue#2364 from smowton/smowton/fix/autodetect-default-cxx-dialect d437f60 Merge pull request diffblue#2368 from polgreen/doc_replace_func_bodies 6048517 Merge pull request diffblue#2353 from tautschnig/g++8-fixes2 e2e6d82 Merge pull request diffblue#2190 from tautschnig/more-stats 7210136 Make it clearer that <=> will always be stringified 560f82b Travis: test more g++ and clang versions d46a55c Add new goto-instrument option print-global-state-size 961b29a Silence GCC 8's warning about using realloc/memmove on non-POD ca1b03c Documentation wording for replace function bodies d8c5a98 Cleanup options handling of count-eloc, list-eloc, print-path-lengths 6cd6d31 Unit test framwork: use references when catching exceptions 6882da6 Merge pull request diffblue#2367 from diffblue/fix-tests bcc3bef make regression/cbmc/bounds_check1 independent of types used 4de4538 switch regression/cbmc/Typecast2 to preprocessed code 91a9c64 Amend two tests that explicitly target C++98 2b2b797 goto-gcc: select default language standard depending on emulated compiler 52a8afc Merge pull request diffblue#1898 from tautschnig/always-inline cbe691b Merge pull request diffblue#2363 from diffblue/Makefile-TAR 9d40a9e Merge pull request diffblue#2365 from diffblue/solaris_errno 9efd705 add model for ___errno for Solaris 11 eaa2e05 update Solaris instructions 2f142d5 allow customizing the tar command for solver download 8cc1848 Merge pull request diffblue#1860 from tautschnig/restore-irept-sharing fea5db0 Merge pull request diffblue#2361 from diffblue/fix-goto2 7c0d750 Merge pull request diffblue#2362 from smowton/smowton/fix/tolerate-cxx-namespace-attribute e440a25 introduce INCOMPLETE_GOTO and turn guarded goto into a stateless pass 1f1835b C++ frontend: tolerate namespace attributes cbce4bc Unit test of irept's public API abdb044 Unit test to check that irept implements sharing d58fd18 Silence the linter on assert in irep.h 3d64070 Partially revert "Use small intrusive pointer in irep" 688a0ab Macros are not needed outside translation units 9c93f59 Fully interpret __attribute__((always_inline)) d1f617b Apply symbol replacement in type_arg members git-subtree-dir: cbmc git-subtree-split: 8a7893c

tautschnig requested review from kroening, peterschrammel and smowton as code owners March 1, 2018 15:41

tautschnig mentioned this pull request Mar 1, 2018

functions marked always inline fail typechecking if they are not static #1519

Closed

tautschnig force-pushed the always-inline branch 3 times, most recently from 313a2be to a614345 Compare March 2, 2018 09:31

tautschnig added the C Front End label Mar 2, 2018

tautschnig assigned smowton, kroening and peterschrammel Mar 3, 2018

smowton reviewed Mar 3, 2018

View reviewed changes

tautschnig assigned tautschnig and unassigned smowton, kroening and peterschrammel Mar 4, 2018

tautschnig force-pushed the always-inline branch 3 times, most recently from 0ee1b0c to 99c12c6 Compare April 16, 2018 18:47

tautschnig assigned smowton, kroening and peterschrammel and unassigned tautschnig Apr 16, 2018

smowton approved these changes Apr 17, 2018

View reviewed changes

tautschnig unassigned smowton and peterschrammel Apr 19, 2018

tautschnig unassigned kroening Jun 1, 2018

tautschnig self-assigned this Jun 1, 2018

tautschnig force-pushed the always-inline branch from 99c12c6 to a10dd0c Compare June 5, 2018 10:37

tautschnig assigned kroening and unassigned tautschnig Jun 5, 2018

tautschnig added 3 commits June 14, 2018 07:59

Apply symbol replacement in type_arg members

d1f617b

This is used int the precursor of a typechecked sizeof expression.

Fully interpret __attribute__((always_inline))

9c93f59

The Linux kernel uses tests on __builtin_constant_p that are required to evalute to true for compilationt to succeed. These can only evaluate to true when inlining is actually done (and expressions are simplified).

Macros are not needed outside translation units

688a0ab

Macros are as local as types; we use macros for always-inlined functions, and contained symbols never end up in the symbol table. Thus macros must be removed before attempting to recurse into them for the purpose of symbol-table cleanup.

tautschnig force-pushed the always-inline branch from a10dd0c to 688a0ab Compare June 14, 2018 07:59

allredj reviewed Jun 14, 2018

View reviewed changes

kroening approved these changes Jun 19, 2018

View reviewed changes

kroening merged commit 52a8afc into diffblue:develop Jun 19, 2018

tautschnig deleted the always-inline branch June 19, 2018 17:33

tautschnig mentioned this pull request Jul 7, 2018

Partial revert of #1898 (always_inline support, second attempt) #2553

Merged

kroening pushed a commit that referenced this pull request Jul 8, 2018

Merge pull request #2553 from tautschnig/always-inline-partial-revert

c6f9231

Partial revert of #1898 (always_inline support, second attempt)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fully process always_inline (second attempt) #1898

Fully process always_inline (second attempt) #1898

tautschnig commented Mar 1, 2018 •

edited

Loading

smowton left a comment

smowton Mar 3, 2018

tautschnig Apr 16, 2018

smowton Mar 3, 2018

tautschnig Apr 16, 2018

smowton Mar 3, 2018

tautschnig Apr 16, 2018

smowton Mar 3, 2018

smowton Mar 3, 2018

tautschnig Apr 16, 2018

smowton Mar 3, 2018

tautschnig Apr 16, 2018

smowton commented Mar 3, 2018

tautschnig commented Mar 4, 2018

tautschnig commented Mar 4, 2018

smowton left a comment

smowton Apr 17, 2018

smowton Apr 17, 2018

tautschnig Apr 19, 2018

allredj left a comment

Fully process always_inline (second attempt) #1898

Fully process always_inline (second attempt) #1898

Conversation

tautschnig commented Mar 1, 2018 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Mar 3, 2018

tautschnig commented Mar 4, 2018

tautschnig commented Mar 4, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Mar 1, 2018 •

edited

Loading