Verify member expressions [blocks: #4023] #4021

smowton · 2019-02-01T16:07:35Z

Depends on #3966

This checks that the component they refer to really exists, and the expression and component's types match.

tautschnig · 2019-02-01T17:27:43Z

src/util/std_expr.h

@@ -3933,7 +3948,6 @@ inline void validate_expr(const member_exprt &value)
  validate_operands(value, 1, "Extract member must have one operand");
 }

-


Nit pick: unrelated change?

kroening · 2019-02-01T18:07:44Z

Please no base_type_eq?

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5dd83b1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99665060
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

smowton · 2019-02-07T18:14:53Z

No can do, lots of stuff fails if we have both == and --validate-ssa-equation, I think because of type renaming. With base_type_eq everything passes but generics will be ignored, because the follow operation skips them.

So which do you prefer:

Eliminate base_type_eq (find and fix all the follows)
Augment base_type_eq a bit to verify that when both types are tags, their decorations match (i.e. like my pointer-decoration PR)

Advantage of 1: clean
Advantage of 2: can do immediately and get some soundness checking in the meantime.

smowton · 2019-02-08T10:44:52Z

Aha, this can be done once limited-type-renaming is in -- by coincidence, in Java types that require renaming (only VLA data allocations) are mutually exclusive with those that use decorated tags, and therefore lose information on type following. Therefore this now works if we first get #3966 and #4126.

Given this narrow tightrope re: type renaming vs. decorated tags, I'll also make a PR to assert that renaming doesn't discard information.

allredj

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

smowton · 2019-02-12T17:10:38Z

I expected this would be good now, but it isn't because there are cases where users of base_type_eq conflate qualified and unqualified generic types, especially symex-dereference. Therefore this needs to wait for #4056.

romainbrenguier · 2019-02-19T11:34:58Z

src/util/std_expr.cpp

+void member_exprt::validate(
+  const exprt &expr,
+  const namespacet &ns,
+  const validation_modet vm)


Avoid abbreviations

Every other validate method is doing the same thing, so I'll leave this as-is for now (change them en masse if we want to)

romainbrenguier · 2019-02-19T11:36:13Z

src/util/std_expr.cpp

+{
+  check(expr, vm);
+
+  const auto &member_expr = to_member_expr(expr);


❓ why not take a member_exprt as argument instead, and let the caller call to_member_expr if needed?

Appears to be normal for validate methods, again change en masse or not at all

romainbrenguier · 2019-02-19T11:37:50Z

src/util/std_expr.cpp

+    can_cast_type<struct_union_typet>(compound_type),
+    "member must address a struct, union or compatible type");
+
+  const auto &component = to_struct_union_type(compound_type)


❓ can't we use a try_cast_dynamic_type instead of can_cast_type + to_struct_union_type?

romainbrenguier · 2019-02-19T11:44:02Z

src/util/std_expr.h

@@ -3897,6 +3897,21 @@ class member_exprt:public unary_exprt
  {
    return op0();
  }
+
+  static void check(


The two functions you introduce should be documented

@smowton Still to be done?

Is there really any value in documenting one-liner that says "assert(ops.count == 1)"?

I'm not so sure, I was just confused by you giving a thumbs-up but then seemingly no such change was included.

I documented validate, which is much more substantial

tautschnig · 2019-03-07T06:59:14Z

@smowton This needs a rebase and addressing @romainbrenguier's comments, then it's ready to go in.

This checks that the component they refer to really exists, and the expression and component's types match (are base_type_eq).

smowton · 2019-03-07T11:08:36Z

@tautschnig done; @romainbrenguier addressed comments; have also tested current test-gen against develop+this PR and found tests passing.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 44756ee).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103522773
Status will be re-evaluated on next push.
Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).
the compatibility was already broken by an earlier merge.

…ype-consistency Test for member type consistency [depends-on: #4021]

smowton requested review from kroening, peterschrammel, pkesseli and tautschnig as code owners February 1, 2019 16:07

smowton force-pushed the smowton/feature/verify-member-expressions branch from 1b24efd to 35b677b Compare February 1, 2019 16:13

smowton mentioned this pull request Feb 1, 2019

Test for member type consistency [depends-on: #4021] #4023

Merged

smowton force-pushed the smowton/feature/verify-member-expressions branch from 35b677b to cb4b80e Compare February 1, 2019 16:41

tautschnig approved these changes Feb 1, 2019

View reviewed changes

tautschnig changed the title ~~Verify member expressions~~ Verify member expressions [blocks: #4023] Feb 1, 2019

tautschnig added the blocker label Feb 1, 2019

tautschnig assigned smowton Feb 2, 2019

peterschrammel approved these changes Feb 2, 2019

View reviewed changes

smowton force-pushed the smowton/feature/verify-member-expressions branch from cb4b80e to 5dd83b1 Compare February 4, 2019 15:41

allredj reviewed Feb 4, 2019

View reviewed changes

smowton force-pushed the smowton/feature/verify-member-expressions branch from 5dd83b1 to db9e4f3 Compare February 7, 2019 17:54

tautschnig assigned kroening and unassigned smowton Feb 7, 2019

smowton requested review from cesaro, cristina-david, NathanJPhillips and thk123 as code owners February 8, 2019 10:13

smowton added the dependent - do not merge label Feb 8, 2019

smowton changed the title ~~Verify member expressions [blocks: #4023]~~ Verify member expressions [blocks: #4023, depends-on: #3966, #4126] Feb 8, 2019

allredj reviewed Feb 8, 2019

View reviewed changes

smowton changed the title ~~Verify member expressions [blocks: #4023, depends-on: #3966, #4126]~~ Verify member expressions [blocks: #4023, depends-on: #3966] Feb 8, 2019

smowton changed the title ~~Verify member expressions [blocks: #4023, depends-on: #3966]~~ Verify member expressions [blocks: #4023, depends-on: #4056] Feb 12, 2019

smowton mentioned this pull request Feb 13, 2019

Remove base_type_eq #4056

Closed

3 tasks

romainbrenguier reviewed Feb 19, 2019

View reviewed changes

tautschnig changed the title ~~Verify member expressions [blocks: #4023, depends-on: #4056]~~ Verify member expressions [blocks: #4023] Mar 7, 2019

tautschnig removed the dependent - do not merge label Mar 7, 2019

tautschnig assigned smowton and unassigned kroening Mar 7, 2019

tautschnig added the Needs rebase label Mar 7, 2019

smowton force-pushed the smowton/feature/verify-member-expressions branch from 7fb60d7 to cfc1c60 Compare March 7, 2019 10:40

Verify member expressions

44756ee

This checks that the component they refer to really exists, and the expression and component's types match (are base_type_eq).

smowton force-pushed the smowton/feature/verify-member-expressions branch from cfc1c60 to 44756ee Compare March 7, 2019 10:52

tautschnig removed the Needs rebase label Mar 7, 2019

allredj reviewed Mar 7, 2019

View reviewed changes

tautschnig merged commit a57d53c into diffblue:develop Mar 7, 2019

tautschnig added a commit that referenced this pull request Mar 7, 2019

Merge pull request #4023 from smowton/smowton/admin/test-for-member-t…

9a8dab9

…ype-consistency Test for member type consistency [depends-on: #4021]

		@@ -3933,7 +3948,6 @@ inline void validate_expr(const member_exprt &value)
		validate_operands(value, 1, "Extract member must have one operand");
		}

Verify member expressions [blocks: #4023] #4021

Verify member expressions [blocks: #4023] #4021

Uh oh!

Conversation

smowton commented Feb 1, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 1, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Feb 7, 2019

Uh oh!

smowton commented Feb 8, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Feb 12, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 7, 2019

Uh oh!

smowton commented Mar 7, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

smowton commented Feb 1, 2019 •

edited

Loading

smowton commented Feb 12, 2019 •

edited

Loading