Fix skeleton in shift_indexed_access_to_lhs #4895

romainbrenguier · 2019-07-12T10:58:22Z

If a byte_extract operation is added to the lhs, then the invert
operation must be performed on the skeleton so that
new_skeleton[new_lhs] is equivalent to skeleton[lhs].

This requires adding a method revert_byte_extract on skeletont.
Unit tests are added for this method and for convert assign symbol.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] 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).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

The function only has an effect if the byte_extract expression can be simplified. So there is no point for the caller to call it with do_simplify=false.

Since the type of expression to simplify is known, we avoid several intermediary calls by calling directly the function that would eventually be called.

If the expression e itself is nil then it would be incorrect to return a pointer to that, so we special case that and return nullptr to denote failure.

This makes it clear from the start of the function that this will only modify byte_update_expressions.

The name of the variable does not add any information to the reader.

tautschnig

Could I please ask for a an explanation why we shouldn't instead just revert #4841? If a bugfix requires +584/-94 changes then we've got a serious problem in our architecture. This doesn't scale.

This allows checking we are replacing the missing part by an appropriate one. This will also make some manipulation easier, like reverting a byte extract operation on a member_expr skeleton.

This is meant to revert the effect of a byte extract on a skeleton. This can be used in symex when assignments are transformed, by switching byte_update/extract operations from one side of the assignment to the other.

Function defined in the header should be marked inline (except for template which are inline by default).

Tests we function works as expected on skeleton containing member and index access.

If a byte_extract operation is added to the lhs, then the revert operation must be performed on the skeleton so that new_skeleton[new_lhs] is equivalent to skeleton[lhs].

This tests the case where a byte_extract expression is assigned.

Since we change the lhs it does not make sense to keep the same skeleton and we have to start from a fresh one.

romainbrenguier · 2019-07-12T13:49:02Z

@tautschnig

Could I please ask for a an explanation why we shouldn't instead just revert #4841? If a bugfix requires +584/-94 changes then we've got a serious problem in our architecture. This doesn't scale.

The problem is not with #4841, this was a refactoring to makes things clearer. The bug was already there before. It was introduced when shift_indexed_access_to_lhs was added, but there are other places with similar problems.

tautschnig · 2019-07-12T14:48:07Z

The problem is not with #4841, this was a refactoring to makes things clearer. The bug was already there before. It was introduced when shift_indexed_access_to_lhs was added, but there are other places with similar problems.

So which bug does it fix? I cannot seem to see a single regression test. I think this is the third PR on the expr_skeletont stuff, which tells me that we are not testing this properly.

smowton · 2019-07-15T14:10:58Z

src/goto-symex/symex_assign.cpp

-                         byte_update.offset(),
-                         byte_update.value().type()},
-      ns);
+    exprt byte_extract = simplify_exprt{ns}


Let's not -- simplify can decide how to do whatever simplification seems appropriate; we shouldn't lift the lid in one place.

smowton · 2019-07-15T16:12:00Z

After staring at this for a while, thoughts:

shift_indexed_access_to_lhs's documentation is not quite right: it seems designed to usually turn x = byte_update y offset z <- w into x = x with .field = (x.field with x.field[1] = w) or similar. That's assuming the while(byte_extract.id() == ID_index || byte_extract.id() == ID_member) loop is expected to terminate when it hits the original x symbol again, and it can't generate something like (byte_extract struct A from x offset (z-2)).field. I'm quite surprised there are situations where the byte_extract operation transferred to the LHS will simplify into array-cell or field accesses but the byte_update operation on the RHS won't simplify into with expressions! @tautschnig ?
Regardless of what shift_indexed_access_to_lhs is doing, it doesn't affect the real lhs (the one recorded in the GOTO program), which is I think what full_lhs is supposed to be tracking. Therefore to my mind it should not change the skeleton.
The same line of reasoning applies to rewrite_with_to_field_symbols -- yes, that should turn x = x with .field = value into x..field = value, but again the actual operation happening at GOTO level is unchanged, only the way symex is encoding it has changed. Therefore I think this function should also not touch the skeleton.
On the other hand, line const exprt l2_full_lhs = state.rename(assignment.original_lhs_skeleton.apply(l2_lhs), ns).get(); in symex_assign.cpp seems highly suspicious -- during the symex_assign_rec loop we might have recorded various index and member operations which were undone by rewrite_with_to_field_symbols, then we proceed the blithely stick the ssa expressions together regardless. I think all the dancing around with the skeleton in rewrite_with_to_field_symbols and shift_indexed_access_to_lhs is just trying to make that step go as we hope it might, and instead we should take l2_lhs's root symbol, which should be the same as that of the lhs passed into assign_non_struct_symbol, then rename as at present.

To sum up: l2_full_lhs should be tracking the GOTO-level operation, not how symex chooses to represent it, therefore it should take no part in the field-sensitivity dance in symex_assignt::assign_non_struct_symbol. I'll put together an alternative PR tomorrow morning to test this solution.

smowton · 2019-07-17T15:11:38Z

Here's my rival PR: #4917

Long story short: do all the LHS rvalue renaming and simplifying right at the start of symex_assign, that way we can delete shift_indexed_access_to_lhs and rewrite_with_to_field_symbols entirely and thus the skeleton manipulations get much simpler.

romainbrenguier · 2019-07-29T06:59:36Z

#4917 makes this irrelevant

romainbrenguier added 5 commits July 12, 2019 11:52

Remove do_simplify argument of shift_indexed_access_to_lhs

e172012

The function only has an effect if the byte_extract expression can be simplified. So there is no point for the caller to call it with do_simplify=false.

Use specialized version of simplify on byte_extract

df6821b

Since the type of expression to simplify is known, we avoid several intermediary calls by calling directly the function that would eventually be called.

deepest_not_nil returns nullptr when called on nil

f951e73

If the expression e itself is nil then it would be incorrect to return a pointer to that, so we special case that and return nullptr to denote failure.

Return early for non byte_update in shift_indexed_access_to_lhs

7d98c66

This makes it clear from the start of the function that this will only modify byte_update_expressions.

Inline variable used only once

e643b83

The name of the variable does not add any information to the reader.

romainbrenguier added the In progress label Jul 12, 2019

romainbrenguier requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners July 12, 2019 10:58

tautschnig requested changes Jul 12, 2019

View reviewed changes

tautschnig assigned romainbrenguier Jul 12, 2019

romainbrenguier force-pushed the bugfix/shift-indexed-access-to-lhs branch from a7a7542 to a5971b2 Compare July 12, 2019 12:42

romainbrenguier added 7 commits July 12, 2019 14:30

Add type of missing part information to skeleton

70b1740

This allows checking we are replacing the missing part by an appropriate one. This will also make some manipulation easier, like reverting a byte extract operation on a member_expr skeleton.

Add a expr_skeletont revert_byte_extract method

dcc361f

This is meant to revert the effect of a byte extract on a skeleton. This can be used in symex when assignments are transformed, by switching byte_update/extract operations from one side of the assignment to the other.

Add forgotten inline

63eafd9

Function defined in the header should be marked inline (except for template which are inline by default).

Add unit-tests for revert_byte_extract

363fc18

Tests we function works as expected on skeleton containing member and index access.

Synchronize skeleton with lhs in shift_indexed_access_to_lhs

86b9b12

If a byte_extract operation is added to the lhs, then the revert operation must be performed on the skeleton so that new_skeleton[new_lhs] is equivalent to skeleton[lhs].

Unit test for assign_symbol with byte_extract

d240f3e

This tests the case where a byte_extract expression is assigned.

Correct skeleton in assign_from_struct

504262b

Since we change the lhs it does not make sense to keep the same skeleton and we have to start from a fresh one.

romainbrenguier force-pushed the bugfix/shift-indexed-access-to-lhs branch from a5971b2 to 504262b Compare July 12, 2019 13:31

smowton reviewed Jul 15, 2019

View reviewed changes

romainbrenguier closed this Jul 29, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fix skeleton in shift_indexed_access_to_lhs #4895

Fix skeleton in shift_indexed_access_to_lhs #4895

Uh oh!

romainbrenguier commented Jul 12, 2019

Uh oh!

tautschnig left a comment

Uh oh!

romainbrenguier commented Jul 12, 2019

Uh oh!

tautschnig commented Jul 12, 2019

Uh oh!

smowton Jul 15, 2019

Uh oh!

smowton commented Jul 15, 2019

Uh oh!

smowton commented Jul 17, 2019

Uh oh!

romainbrenguier commented Jul 29, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Fix skeleton in shift_indexed_access_to_lhs #4895

Fix skeleton in shift_indexed_access_to_lhs #4895

Uh oh!

Conversation

romainbrenguier commented Jul 12, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Jul 12, 2019

Uh oh!

tautschnig commented Jul 12, 2019

Uh oh!

smowton Jul 15, 2019

Choose a reason for hiding this comment

Uh oh!

smowton commented Jul 15, 2019

Uh oh!

smowton commented Jul 17, 2019

Uh oh!

romainbrenguier commented Jul 29, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants