Fixing simplification of LHS #1070

thk123 · 2017-06-28T14:42:04Z

The simplify_lhs had the boolean flag the wrong way round.

tautschnig · 2017-06-29T08:37:06Z

Do I understand correctly that this fixes problems that only #1020 would introduce? If so, shouldn't it just become part of #1020?

thk123 · 2017-06-29T09:18:05Z

@tautschnig Actually I've just realised the bug exists in master (it must have gone in as part of the goto-analyzer PR: https://github.com/diffblue/cbmc/blob/master/src/analyses/ai.cpp#L53

There are 3 changes in this PR:

Fixing ai_simplify_lhs which should go straight into master
Removing duplicate code (that can be folded into [depends: #472] Variable Sensitivity Domain #708)
Adding tests

The adding tests ideally also wants to go straight into master - but I will need to find out what domain I can use to demonstrate the bug.

The tests for variable-sensitivity-domain are dependent on #1010 but only because of the Makefile being added in that PR. If the Makefile makes its way in earlier then the tests can just be part of #708 as well.

thk123 · 2017-06-29T10:51:40Z

@tautschnig Hmm - it seems that --simplify isn't even a command I can run on goto-analyzer on the master branch!

I can update this PR to just fix the bug with no tests and just have the tests as part of #708. I could try and write a unit test but it might be quite fiddly and since wouldn't use a real domain probably not test much. How would you like me to proceed?

tautschnig · 2017-07-03T10:24:50Z

How would you like me to proceed?

What is the overall picture of PRs and dependencies for goto-analyzer? It appears to be in a rather questionable state after some of the commits of one of the earlier PRs have been merged?

thk123 · 2017-07-03T10:38:11Z

@tautschnig I'm not sure I know exactly what you mean by "questionable state"(!), so apologies if I've got the wrong end of the stick here.

The original goto-analyzer PR (#472) is being broken down into smaller (4?) parts by @martin-cs. Parts 1 (#953) and 2 (#961) are in. Part 3 (#966) is approved in principle, though I think it needs a Doxygen pass.

This PR fixes a bug introduced by Part 2 which could be pulled out and targeted at the current master.

It also includes tests that are dependent on the variable sensitivity domain that I can't work out how I would back port to before it exists since no domain seems to exist that uses simplify functionality of ai_domain_baset though i could be wrong.

Also, Martin is away for a month so responses might be slower than usual.

tautschnig · 2017-07-03T10:52:10Z

@tautschnig I'm not sure I know exactly what you mean by "questionable state"(!), so apologies if I've got the wrong end of the stick here.

My apologies for poor wording. I think mainly it's just unclear (at least to me) what has been merged and what hasn't, plus whether goto-analyzer is currently meant to be working correctly or not.

The original goto-analyzer PR (#472) is being broken down into smaller (4?) parts by @martin-cs. Parts 1 (#953) and 2 (#961) are in. Part 3 (#966) is approved in principle, though I think it needs a Doxygen pass.

This PR fixes a bug introduced by Part 2 which could be pulled out and targeted at the current master.

PRs depending on each other can of course not always be avoided, but here we appear to be at a collection of PRs that form a DAG. It would be great if we could get to a linear sequence, where each step is as bug-free as possible. Hence I would find it great if there could be a PR that fits on top of part 2 (i.e., current master), with part 3 (#966) then placed on top of this one.

It also includes tests that are dependent on the variable sensitivity domain that I can't work out how I would back port to before it exists since no domain seems to exist that uses simplify functionality of ai_domain_baset though i could be wrong.

The usual problem of new features that are too big to go into a single pull request. We might just have to live without the tests, with some comments pointing towards "tests will be added later on, because the depend on x and y."

Does this help to clarify?

thk123 · 2017-07-03T13:21:52Z

@tautschnig sure - I'll turn this into a patch that does what you described - fixing bug in the current master branch that part 3 can go on top of.

If it is easy, I'll add a simple unit test to verify the fix doesn't get undone through any of the rebasing options. The tests for variable sensitivity domain and removing the duplicate code I'll squash back into the original variable sensitivity domain.

I don't know the validity of the current goto-analyzer. I only stared using it when implementing the variable sensitivity domain stuff, so it isn't clear to me what behaviour it should have/how to use it. I don't think the intention of the PRs was to ever move backwards, though clearly this may have happened by mistake.

thk123 · 2017-07-03T16:30:03Z

unit/analyses/ai/ai_simplify_lhs.cpp

+#endif
+  }
+}
+


Remote white space

thk123 · 2017-07-03T16:31:14Z

unit/analyses/ai/ai_simplify_lhs.cpp

+
+    // This fails since the implementation does do a constant simplification
+    // on the array part. It isn't clear to me if this is correct
+#if 0


This fails since the implementation does do a constant simplification on the array part. It isn't clear to me if this is correct . This somewhat limits I can test (if it really is supposed to be using constant simplification on all parts, can't test isn't inadvertently ai_simplifying bits it shouldn't be.

thk123 · 2017-07-03T16:38:26Z

@tautschnig Done - this should now go in ideally before part 3. The testing isn't comprehensive, as I need to know whether the behaviour for a constant array is correct. If it is correct then the mock ai_domain should probably just be setup with a bunch of hard coded expressions with corresponding values that the mock function just looks up in a map. It it isn't it can carry on using simplify_expr as its simplification.

In any case, it should be just enough testing to catch an inadvertent regression to when doing a rebase.

tautschnig · 2017-07-10T15:32:23Z

src/analyses/ai.cpp

  }
  else if(condition.id()==ID_member)
  {
    member_exprt me=to_member_expr(condition);
-    bool changed=ai_simplify_lhs(me.compound(), ns); // <-- lhs!
-    if(changed)
+    // Carry on the RHS since we still require an addressable object for the


Apologies if I'm being dense: what does "Carry on the RHS" mean?

Oops looks like it is the wrong way round! We need to carry on ai_simplify_lhs (left hand side) since we need an addressable object, is this any clearer:

// Since require an addressable object for the struct, carry on using // ai_simplify_lhs to avoid simplifying away the value

This is better, except the first part now misses a subject - who requires that addressable object?

// Since simplify_ai_lhs is required to return an addressable object // (so remains a valid left hand side), to simplify `(something_simplifiable).b` // we require that something_simplifiable must also be addressable

?

I'm happy with that :-)

tautschnig · 2017-07-10T15:33:21Z

unit/Makefile

        ../src/solvers/solvers$(LIBEXT) \
+        ../src/util/util$(LIBEXT) \
+        ../src/big-int/big-int$(LIBEXT) \


Why is the order of libraries being changed here?

For the awful reason that the order effects whether it compiles on GCC: https://stackoverflow.com/questions/45135/why-does-the-order-in-which-libraries-are-linked-sometimes-cause-errors-in-gcc -

From memory the analyses.a depends on the goto-programs.a and lots depends on util.a which depends on big-int.a. I'm not even sure this will be the last rearrangement. I would guess as the first unit tests are written for each library are added, these will fluctuate about.

While those dependencies in general are painful and we've argued about that a bit in the past: the adopted solution was for LINKBIN to use --start-group and --end-group to work around this problem. I thus wonder why this re-ordering problem is coming up here?

Ah OK, me neither! So the link command is:

clang++ -o unit_tests -Wl,--start-group unit_tests.o catch_example.o analyses/ai/ai_simplify_lhs.o -Wl,--end-group ../src/ansi-c/ansi-c.a ../src/cpp/cpp.a ../src/json/json.a ../src/linking/linking.a ../src/pointer-analysis/pointer-analysis.a ../src/langapi/langapi.a ../src/assembler/assembler.a ../src/analyses/analyses.a ../src/goto-programs/goto-programs.a ../src/solvers/solvers.a ../src/big-int/big-int.a ../src/util/util.a

So all the libs somehow end up outside of the --start-group/--end-group flags, so I suppose somehow LIBS is not put inside that group, I'll investigate but don't know src/common.

Ah, that's because that's not what LIBS is to be used for. All the entries currently placed in LIBS in unit/Makefile ought to go in OBJS. The code base uses LIBS only for libraries outside the code base. (Yes, I do agree this isn't quite the perfect set up...)

Ahha bingo! I'll apply this modification to #1111 and once that's in I'll rebase this on top of it.

thk123 · 2017-07-10T17:02:05Z

Commit e5b539d should be dropped after #1111 is merged.

The boolean flag was the wrong way round for ai_simplify_lhs - this corrects this.

These tests use a mock implementation of the `ai_domain_baset` interface just to validate that true means no simplification.

thk123 · 2017-07-19T11:51:19Z

@tautschnig since #1111 is merged, this should be ready for a review.

@kroening I think this should go in the maintenance release as it fixes a (reasonably major) bug with ai.h

tautschnig

Looks good to me!

thk123 force-pushed the bugfix/simplify-lhs branch from 2041c4d to c4a79c9 Compare July 3, 2017 16:25

thk123 commented Jul 3, 2017

View reviewed changes

thk123 force-pushed the bugfix/simplify-lhs branch from c4a79c9 to be1b573 Compare July 3, 2017 16:34

peterschrammel mentioned this pull request Jul 3, 2017

Goto analyzer 5 part3 #966

Closed

tautschnig reviewed Jul 10, 2017

View reviewed changes

thk123 force-pushed the bugfix/simplify-lhs branch from be1b573 to 3ae2e09 Compare July 10, 2017 17:01

thk123 mentioned this pull request Jul 10, 2017

Improvements to the unit tests directory #1111

Merged

thk123 added 2 commits July 19, 2017 12:46

Corrected simplify lhs in ai_domain_baset

64ab723

The boolean flag was the wrong way round for ai_simplify_lhs - this corrects this.

Added unit tests to validate the return meaning of ai_simplify_lhs

d4d976a

These tests use a mock implementation of the `ai_domain_baset` interface just to validate that true means no simplification.

thk123 force-pushed the bugfix/simplify-lhs branch from 3ae2e09 to d4d976a Compare July 19, 2017 11:49

tautschnig added the bugfix label Jul 19, 2017

tautschnig approved these changes Jul 20, 2017

View reviewed changes

tautschnig assigned kroening Jul 20, 2017

kroening merged commit e18cb15 into diffblue:master Jul 22, 2017

thk123 deleted the bugfix/simplify-lhs branch July 24, 2017 09:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fixing simplification of LHS #1070

Fixing simplification of LHS #1070

thk123 commented Jun 28, 2017 •

edited

Loading

tautschnig commented Jun 29, 2017

thk123 commented Jun 29, 2017

thk123 commented Jun 29, 2017

tautschnig commented Jul 3, 2017

thk123 commented Jul 3, 2017

tautschnig commented Jul 3, 2017

thk123 commented Jul 3, 2017

thk123 Jul 3, 2017

thk123 Jul 3, 2017

thk123 commented Jul 3, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

tautschnig Jul 10, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

thk123 commented Jul 10, 2017

thk123 commented Jul 19, 2017

tautschnig left a comment

Fixing simplification of LHS #1070

Fixing simplification of LHS #1070

Conversation

thk123 commented Jun 28, 2017 • edited Loading

tautschnig commented Jun 29, 2017

thk123 commented Jun 29, 2017

thk123 commented Jun 29, 2017

tautschnig commented Jul 3, 2017

thk123 commented Jul 3, 2017

tautschnig commented Jul 3, 2017

thk123 commented Jul 3, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Jul 3, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Jul 10, 2017

thk123 commented Jul 19, 2017

tautschnig left a comment

Choose a reason for hiding this comment

thk123 commented Jun 28, 2017 •

edited

Loading