Mimic GCC/Clang simplification behaviour when type checking ?: #7959

tautschnig · 2023-10-13T10:30:53Z

Neither GCC nor Clang simplify expressions involving symbols even when the result would always be 0, which our simplifier figure out.

Fixes: #7927

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2023-10-13T11:39:47Z

Codecov Report

Attention: 39 lines in your changes are missing coverage. Please review.

Comparison is base (3777fa9) 79.08% compared to head (2d5adef) 79.07%.

Files	Patch %	Lines
src/ansi-c/c_typecheck_expr.cpp	52.43%	39 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7959      +/-   ##
===========================================
- Coverage    79.08%   79.07%   -0.02%     
===========================================
  Files         1698     1698              
  Lines       196491   196519      +28     
===========================================
+ Hits        155404   155406       +2     
- Misses       41087    41113      +26

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

kroening · 2023-10-15T10:47:21Z

We will eventually need explicit constant folding logic in the C frontend, as opposed to relying on the simplifier. I expect that the latter will always be able to simplify more.

kroening · 2023-10-18T08:01:43Z

This PR needs more contemplation. The PR changes the typing, but would appear to be about constant folding.
Maybe the presence of symbols doesn't change the typing, but does affect constant folding.

tautschnig · 2023-11-16T09:22:21Z

This PR needs more contemplation. The PR changes the typing, but would appear to be about constant folding. Maybe the presence of symbols doesn't change the typing, but does affect constant folding.

@kroening: Please take another look, I hope to have adjusted this in line with your feedback as it now uses (compile-time) constant folding rules.

src/ansi-c/c_typecheck_expr.cpp

kroening · 2023-12-13T14:02:23Z

regression/ansi-c/sizeof6/main.c

+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(i ? 0ll : 0ll)) : (int *)1)), "");
+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(0 ? i : 0ll)) : (int *)1)), "");


These appear to assert that some part of the subexpression is a compile time constant. May I suggest to use __builtin_constant_p for that. The sizeof assertion is a distraction.

This, I'm afraid, just uncovered another challenge: the above "true" cases aren't deemed null-pointer constants by the compilers (and, therefore, the type of the ?: is void* rather than int*). __builtin_constant_p, however, does return 1 for the very same expressions!

I have added a commit that better exercises (and extends) an existing test to also document (and test) these differences.

Might be worth filing a bug report with those compilers.

kroening · 2023-12-13T18:20:48Z

Apologies that the scope of this PR is getting pushed larger, by me. Does it make sense to replace the minimal case split done for __builtin_constant_p by an invocation of is_compile_time_constantt(ns) plus some special cases for when they differ?

tautschnig · 2023-12-13T22:26:16Z

Apologies that the scope of this PR is getting pushed larger, by me. Does it make sense to replace the minimal case split done for __builtin_constant_p by an invocation of is_compile_time_constantt(ns) plus some special cases for when they differ?

I'll take care of this!

This is useful in various methods and should be available to all of them.

Neither GCC nor Clang simplify expressions involving symbols even when the result would always be 0, which our simplifier figure out. Fixes: diffblue#7927

C11 Section 6.6 "Constant expressions" defines what are required to be constant expressions, and permits implementations to pick additional constant expressions.

tautschnig · 2023-12-14T20:07:29Z

Apologies that the scope of this PR is getting pushed larger, by me. Does it make sense to replace the minimal case split done for __builtin_constant_p by an invocation of is_compile_time_constantt(ns) plus some special cases for when they differ?

I'll take care of this!

I believe this is now done.

src/ansi-c/c_typecheck_expr.cpp

kroening · 2023-12-14T20:55:26Z

src/ansi-c/c_typecheck_expr.cpp

    }
    else
-      is_constant=tmp1.is_constant();
+    {
+      // try to produce constant


is_compile_time_constantt is too far off in the GCC/MSVC case?

__builtin_constant_p doesn't exist with MSVC, so it'd be GCC only. For that, however, the simplifier appears to be much closer: GCC happily takes x - x, x * 0 as constants. But then we could still do what I now (in my latest push to this PR) ended up doing: produce a variant of is_compile_time_constantt for a specific compiler (clang_is_constant_foldedt).

We previously only compile-time tested what required a run-time check of assertions, so move this to the "cbmc" regression test suite. Also, extend it by behaviour that distinguishes it from actual C-standard specified constant expressions. Finally, fix the behaviour for string literals.

tautschnig added the C Front End label Oct 13, 2023

tautschnig assigned kroening Oct 13, 2023

tautschnig requested review from kroening, peterschrammel and remi-delmas-3000 as code owners October 13, 2023 10:30

tautschnig mentioned this pull request Oct 13, 2023

Goto-cc doesn't handle BUILD_BUG_ON_ZERO macro in Linux #7927

Open

tautschnig force-pushed the features/gcc-clang-ite-simp branch from 506cd0d to 6f82cc7 Compare November 16, 2023 09:20

kroening reviewed Nov 20, 2023

View reviewed changes

src/ansi-c/c_typecheck_expr.cpp Show resolved Hide resolved

kroening reviewed Nov 20, 2023

View reviewed changes

src/ansi-c/c_typecheck_expr.cpp Show resolved Hide resolved

tautschnig assigned tautschnig and unassigned kroening Nov 20, 2023

tautschnig force-pushed the features/gcc-clang-ite-simp branch from 6f82cc7 to 3421bfd Compare December 13, 2023 13:58

tautschnig assigned kroening and unassigned tautschnig Dec 13, 2023

kroening reviewed Dec 13, 2023

View reviewed changes

tautschnig force-pushed the features/gcc-clang-ite-simp branch 2 times, most recently from 433de81 to 4076a22 Compare December 13, 2023 15:41

tautschnig self-assigned this Dec 13, 2023

tautschnig added 3 commits December 14, 2023 20:06

Move is_compile_time_constantt to top of file

bab1341

This is useful in various methods and should be available to all of them.

Mimic GCC/Clang simplification behaviour when type checking ?:

7d0523f

Neither GCC nor Clang simplify expressions involving symbols even when the result would always be 0, which our simplifier figure out. Fixes: diffblue#7927

Expand documentation of is_compile_time_constantt

8430887

C11 Section 6.6 "Constant expressions" defines what are required to be constant expressions, and permits implementations to pick additional constant expressions.

tautschnig force-pushed the features/gcc-clang-ite-simp branch from 4076a22 to d39db8f Compare December 14, 2023 20:07

tautschnig removed their assignment Dec 14, 2023

tautschnig self-assigned this Dec 14, 2023

kroening reviewed Dec 14, 2023

View reviewed changes

src/ansi-c/c_typecheck_expr.cpp Outdated Show resolved Hide resolved

kroening reviewed Dec 14, 2023

View reviewed changes

tautschnig force-pushed the features/gcc-clang-ite-simp branch 3 times, most recently from 0c1b2f7 to 5d04507 Compare December 14, 2023 21:12

tautschnig removed their assignment Dec 14, 2023

tautschnig force-pushed the features/gcc-clang-ite-simp branch from 5d04507 to f86884c Compare December 14, 2023 22:31

tautschnig force-pushed the features/gcc-clang-ite-simp branch from f86884c to 2d5adef Compare December 14, 2023 23:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Mimic GCC/Clang simplification behaviour when type checking ?: #7959

Mimic GCC/Clang simplification behaviour when type checking ?: #7959

tautschnig commented Oct 13, 2023

codecov bot commented Oct 13, 2023 •

edited

Loading

kroening commented Oct 15, 2023

kroening commented Oct 18, 2023

tautschnig commented Nov 16, 2023

kroening Dec 13, 2023

tautschnig Dec 13, 2023

tautschnig Dec 13, 2023

kroening Dec 13, 2023

kroening Dec 13, 2023

kroening commented Dec 13, 2023

tautschnig commented Dec 13, 2023

tautschnig commented Dec 14, 2023

kroening Dec 14, 2023

tautschnig Dec 14, 2023

Mimic GCC/Clang simplification behaviour when type checking ?: #7959

Are you sure you want to change the base?

Mimic GCC/Clang simplification behaviour when type checking ?: #7959

Conversation

tautschnig commented Oct 13, 2023

codecov bot commented Oct 13, 2023 • edited Loading

Codecov Report

kroening commented Oct 15, 2023

kroening commented Oct 18, 2023

tautschnig commented Nov 16, 2023

kroening Dec 13, 2023

Choose a reason for hiding this comment

tautschnig Dec 13, 2023

Choose a reason for hiding this comment

tautschnig Dec 13, 2023

Choose a reason for hiding this comment

kroening Dec 13, 2023

Choose a reason for hiding this comment

kroening Dec 13, 2023

Choose a reason for hiding this comment

kroening commented Dec 13, 2023

tautschnig commented Dec 13, 2023

tautschnig commented Dec 14, 2023

kroening Dec 14, 2023

Choose a reason for hiding this comment

tautschnig Dec 14, 2023

Choose a reason for hiding this comment

codecov bot commented Oct 13, 2023 •

edited

Loading