Move promotion rule application to C front-end [blocks: #3725, #3800] #3770

tautschnig · 2019-01-12T15:21:32Z

The front-ends handle type conversion when doing arithmetic over enum types. The
case of an enum tag is not expected in goto-program conversion. That, however,
was only the case for some operators. Made the C front-end properly handle all
assignment operators.

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.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 965d458).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97133012

tautschnig · 2019-01-14T17:15:07Z

Marked work-in-progress: we should review all special-casing of ID_c_enum_tag (and indeed also ID_c_bool) in goto-programs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: aa1b446).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99429688

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 9f92ab9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101215749

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 3d01c87).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101250611

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e254a6f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101349909

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1042845).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102431450

kroening · 2019-02-27T14:26:51Z

src/ansi-c/c_typecheck_expr.cpp

+
+      // increment/decrement on underlying type
+      expr.op0() = typecast_exprt(expr.op0(), enum_type.subtype());
+      expr.type() = enum_type.subtype();


I would make that an implicit typecast.

I have added implicit_typecast_arithmetic(expr); - is that what you expected?

No, that's arithmetic promotion; I am not actually sure whether these are meant to happen to the underlying type of an enum.
What I meant is the ID_C_implicit_typecast annotation, which is used to distinguish an explicit cast from one added by the frontend.

I can't seem to find ID_C_implicit_typecast or indeed any other annotation that the implicit_typecast code would be adding?!

kroening · 2019-02-27T14:32:43Z

src/goto-programs/goto_convert_side_effect.cpp

+
+    exprt new_lhs = skip_typecast(expr.op0());
+    rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
+    rhs.add_source_location() = expr.source_location();


This is outside the C front-end, I don't think I can use implicit_typecast(_arithmetic) here?!

Yes, you may have to add ID_C_implicit_typecast directly.

The front-ends handle type conversion when doing arithmetic over enum types. The case of an enum tag is not expected in goto-program conversion. That, however, was only the case for some operators. Made the C front-end properly handle all assignment operators. While at it, also support decrement operators over complex numbers. We already did so for increment, decrement just requires the same special case.

Doing so during goto-program conversion will ensure we can generate appropriate conversion checks. Fixes: diffblue#4208

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 25e854f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102514059

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2043025).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102521796

tautschnig added the cleanup label Jan 12, 2019

tautschnig requested review from kroening, peterschrammel, pkesseli and smowton as code owners January 12, 2019 15:21

tautschnig mentioned this pull request Jan 12, 2019

Remove unnecessary use of ns.follow in goto-programs/ #3761

Merged

3 tasks

allredj reviewed Jan 12, 2019

View reviewed changes

smowton approved these changes Jan 14, 2019

View reviewed changes

tautschnig added the work in progress label Jan 14, 2019

tautschnig self-assigned this Jan 14, 2019

tautschnig force-pushed the cleanup-promotion branch from 965d458 to d46cf18 Compare January 31, 2019 13:51

tautschnig added bugfix and removed work in progress labels Jan 31, 2019

tautschnig assigned kroening and unassigned tautschnig Jan 31, 2019

tautschnig force-pushed the cleanup-promotion branch 2 times, most recently from bb4a135 to aa1b446 Compare February 1, 2019 13:18

allredj reviewed Feb 1, 2019

View reviewed changes

tautschnig mentioned this pull request Feb 2, 2019

Replace make_typecast by typecast_exprt or typecast_exprt::conditional_cast [blocks: #3800] #3991

Merged

3 tasks

tautschnig changed the title ~~Move promotion rule application to C front-end~~ Move promotion rule application to C front-end [blocks: #3800] Feb 2, 2019

tautschnig added the blocker label Feb 2, 2019

tautschnig mentioned this pull request Feb 17, 2019

Type promotion in compound assignments is broken #4208

Closed

tautschnig force-pushed the cleanup-promotion branch from aa1b446 to 9f92ab9 Compare February 17, 2019 07:33

allredj reviewed Feb 17, 2019

View reviewed changes

peterschrammel approved these changes Feb 17, 2019

View reviewed changes

tautschnig force-pushed the cleanup-promotion branch from 9f92ab9 to 3d01c87 Compare February 18, 2019 01:54

allredj reviewed Feb 18, 2019

View reviewed changes

tautschnig force-pushed the cleanup-promotion branch from 3d01c87 to e254a6f Compare February 18, 2019 17:37

allredj reviewed Feb 18, 2019

View reviewed changes

tautschnig mentioned this pull request Feb 21, 2019

Symex-dereference: simplify after deref [blocks: #2574, #4056] #3725

Merged

4 tasks

tautschnig changed the title ~~Move promotion rule application to C front-end [blocks: #3800]~~ Move promotion rule application to C front-end [blocks: #3725, #3800] Feb 21, 2019

tautschnig force-pushed the cleanup-promotion branch from e254a6f to 1042845 Compare February 27, 2019 01:19

allredj reviewed Feb 27, 2019

View reviewed changes

kroening reviewed Feb 27, 2019

View reviewed changes

tautschnig force-pushed the cleanup-promotion branch from 1042845 to 25e854f Compare February 27, 2019 14:32

kroening approved these changes Feb 27, 2019

View reviewed changes

tautschnig added 2 commits February 27, 2019 15:17

Move LHS type casts to RHS in assign_* instructions

2043025

Doing so during goto-program conversion will ensure we can generate appropriate conversion checks. Fixes: diffblue#4208

tautschnig force-pushed the cleanup-promotion branch from 25e854f to 2043025 Compare February 27, 2019 15:17

allredj reviewed Feb 27, 2019

View reviewed changes

tautschnig merged commit ba421e0 into diffblue:develop Feb 27, 2019

tautschnig deleted the cleanup-promotion branch February 27, 2019 16:16

allredj reviewed Feb 27, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Move promotion rule application to C front-end [blocks: #3725, #3800] #3770

Move promotion rule application to C front-end [blocks: #3725, #3800] #3770

tautschnig commented Jan 12, 2019

allredj left a comment

tautschnig commented Jan 14, 2019

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

kroening Feb 27, 2019

tautschnig Feb 27, 2019

kroening Feb 27, 2019

tautschnig Feb 27, 2019

kroening Feb 27, 2019

tautschnig Feb 27, 2019

kroening Feb 27, 2019

allredj left a comment

allredj left a comment

Move promotion rule application to C front-end [blocks: #3725, #3800] #3770

Move promotion rule application to C front-end [blocks: #3725, #3800] #3770

Conversation

tautschnig commented Jan 12, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Jan 14, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

kroening Feb 27, 2019

Choose a reason for hiding this comment

tautschnig Feb 27, 2019

Choose a reason for hiding this comment

kroening Feb 27, 2019

Choose a reason for hiding this comment

tautschnig Feb 27, 2019

Choose a reason for hiding this comment

kroening Feb 27, 2019

Choose a reason for hiding this comment

tautschnig Feb 27, 2019

Choose a reason for hiding this comment

kroening Feb 27, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment