goto_symex: rename type symbols only when needed [blocks: #3652] #3633

kroening · 2018-12-28T21:04:14Z

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/
n/a 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.

kroening · 2018-12-28T21:05:19Z

This fails on jbmc regressions -- apparently types created by the Java object factory are sometimes expanded to ID_struct.

tautschnig · 2018-12-28T21:09:42Z

This fails on jbmc regressions -- apparently types created by the Java object factory are sometimes expanded to ID_struct.

This might as well be something that the simplifier does. See some of the commits in #2064.

tautschnig · 2018-12-28T21:14:00Z

src/goto-symex/goto_symex_state.cpp

+           !array_type.size().is_constant();
+  }
+  else if(
+    type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class)


I don't think type.id() == ID_class should ever evaluate to true. A class is represented as ID_struct with ID_C_class set to true. If I'm wrong in saying this then we've got a lot more work to do elsewhere.

Yes, these should be cleaned out.

kroening · 2018-12-28T21:17:45Z

Note #3634 -- the assertion there catches this problem.

tautschnig · 2018-12-29T21:51:41Z

I think it would be good to factor out the individual commits into PRs of their own. They need proper justifications, but seem to be useful in their own right. And also at least the first one also appears in another PR.

kroening · 2018-12-30T09:58:18Z

The bugfixes are now in separate PRs.
For this to work in jbmc, the problem in the Java object factory needs to be fixed first, as part of #3634.

tautschnig · 2019-01-10T18:39:29Z

@kroening Are all the depended-on changes now PR'ed, or is there more work necessary?

tautschnig

Approving, but this PR now includes commits of my own so @kroening (and other reviewers as other code is now being touched) should please comment as well.

smowton · 2019-01-23T18:04:50Z

Any chance of unifying the make-change and check-if-change-needed paths? For example, by passing a const typet & and a typet * in parallel, which is null in the check-if-needed case and non-null otherwise?

Just like symbol or enum tags, we need to look into the expanded tags.

The regular expressions now accept both the tag names as well as the expanded types/class names.

Until we have resolved partial tag expansion everywhere we need to use base_type_eq for cases where both tags and expanded types may occur.

struct tags need to be expanded.

Renaming a type is rarely needed: this is necessary only if the type contains a struct that contains a variable-sized member, which is a gcc extension. The key benefit of not renaming in all other cases is that struct and union tag types no longer get expanded.

tautschnig · 2019-01-23T18:17:41Z

Any chance of unifying the make-change and check-if-change-needed paths?

Good point, but I'm a bit hesitant here: not doing the renaming also spares us putting anything in l1_types, which we'd otherwise likely want to be doing lookups in. Doable, but I'd for now prefer to keep this one simple until profiling tells us that it is one of the bottlenecks worth tackling.

allredj

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

romainbrenguier · 2019-01-24T08:52:39Z

src/goto-symex/goto_symex_state.cpp

+    {
+      // be careful, or it might get cyclic
+      if(component.type().id() != ID_pointer)
+        return requires_renaming(component.type(), ns);


This only looks at the first non-pointer component of the struct, which is strange, but I cannot say whether this is correct because the function is not documented, so please document.

Oooh, I missed that, @kroening pretty sure this is a real bug

(suggests a new test -- AFAIK GCC allows such variable-size structs?)

I think I've found a way to construct a failing test, I'll post a follow-up PR to include a test, a fix, and the suggested documentation.

The failure I thought I had found was one caused by integer overflow - I haven't actually managed to produce a proper failure. See #3918 for my attempt and the cleanup.

kroening · 2019-01-24T13:40:18Z

The base_type_eq shouldn't be needed; however, this is a step in the right direction.

tautschnig · 2019-01-24T13:52:31Z

The base_type_eq shouldn't be needed; [...]

Yes, it shouldn't be, but thus far it strictly is needed for Java input programs (as regression tests confirm).

kroening assigned romainbrenguier Dec 28, 2018

kroening requested review from allredj, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners December 28, 2018 21:04

kroening changed the title ~~Symex type renaming3~~ @kroening goto_symex: rename type symbols only when needed Dec 28, 2018

kroening changed the title ~~@kroening goto_symex: rename type symbols only when needed~~ goto_symex: rename type symbols only when needed Dec 28, 2018

tautschnig reviewed Dec 28, 2018

View reviewed changes

tautschnig assigned kroening and unassigned romainbrenguier Dec 29, 2018

kroening force-pushed the symex-type-renaming3 branch from 64c7d39 to db3ebcb Compare December 30, 2018 09:52

kroening added the work in progress label Dec 30, 2018

tautschnig changed the title ~~goto_symex: rename type symbols only when needed~~ goto_symex: rename type symbols only when needed [blocks: #3652] Jan 10, 2019

tautschnig added the blocker label Jan 10, 2019

kroening force-pushed the symex-type-renaming3 branch from db3ebcb to 649abde Compare January 11, 2019 09:02

kroening force-pushed the symex-type-renaming3 branch from 649abde to 41c7d83 Compare January 19, 2019 13:01

tautschnig force-pushed the symex-type-renaming3 branch from 41c7d83 to 4949535 Compare January 23, 2019 16:05

kroening requested review from chrisr-diffblue, pkesseli and smowton as code owners January 23, 2019 16:05

tautschnig approved these changes Jan 23, 2019

View reviewed changes

tautschnig assigned smowton and romainbrenguier Jan 23, 2019

tautschnig removed the work in progress label Jan 23, 2019

tautschnig force-pushed the symex-type-renaming3 branch from 4949535 to abd6508 Compare January 23, 2019 16:37

tautschnig and others added 5 commits January 23, 2019 18:12

has_subtype: handle struct/union tag types

abdbbbc

Just like symbol or enum tags, we need to look into the expanded tags.

Make tests oblivious to tag type expansion

3d9af8e

The regular expressions now accept both the tag names as well as the expanded types/class names.

Accept base type equality

fe03ab9

Until we have resolved partial tag expansion everywhere we need to use base_type_eq for cases where both tags and expanded types may occur.

String refinement: handle both struct and struct tag types

7e74b97

struct tags need to be expanded.

tautschnig force-pushed the symex-type-renaming3 branch from abd6508 to 74d1548 Compare January 23, 2019 18:13

allredj reviewed Jan 23, 2019

View reviewed changes

romainbrenguier reviewed Jan 24, 2019

View reviewed changes

kroening merged commit 8c1ae4c into develop Jan 24, 2019

kroening deleted the symex-type-renaming3 branch January 24, 2019 13:40

tautschnig mentioned this pull request Jan 24, 2019

Check all struct members for possible need for renaming #3918

Merged

4 tasks

tautschnig mentioned this pull request Feb 21, 2019

requires_renaming must not recurse into array subtypes in structs #4233

Merged

3 tasks

goto_symex: rename type symbols only when needed [blocks: #3652] #3633

goto_symex: rename type symbols only when needed [blocks: #3652] #3633

Uh oh!

Conversation

kroening commented Dec 28, 2018

Uh oh!

kroening commented Dec 28, 2018

Uh oh!

tautschnig commented Dec 28, 2018

Uh oh!

tautschnig Dec 28, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Dec 28, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Dec 28, 2018

Choose a reason for hiding this comment

Uh oh!

kroening commented Dec 28, 2018

Uh oh!

tautschnig commented Dec 29, 2018

Uh oh!

kroening commented Dec 30, 2018

Uh oh!

tautschnig commented Jan 10, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jan 23, 2019

Uh oh!

tautschnig commented Jan 23, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 24, 2019

Uh oh!

tautschnig commented Jan 24, 2019

Uh oh!

Uh oh!

tautschnig Jan 24, 2019 •

edited

Loading