Goto analyzer 5 part2 #961

martin-cs · 2017-05-23T19:56:37Z

Low risk changes needed for the goto-analyze branch. Mostly additions.

Note that an earlier version of this has been reviewed as part of #472, there have been some changes.

tautschnig

There are a few bits where I'd ask for clarification.

tautschnig · 2017-05-24T07:34:52Z

src/analyses/ai.cpp

+}
+
+/*******************************************************************\
+Function: variable_sensitivity_domaint::ai_simplify_lhs


In case the automatic documentation conversion script relies on this: there should be a blank line before "Function:"

tautschnig · 2017-05-24T07:37:47Z

src/analyses/ai.cpp

+  }
+  else if(condition.id()==ID_member)
+  {
+    member_exprt me = to_member_expr(condition);


No whitespace around =

I thought the lint script flagged these. Oh well; fixed.

tautschnig · 2017-05-24T07:41:07Z

src/analyses/ai.cpp

+    {
+      ie.index() = index;
+      condition = simplify_expr(ie, ns);
+    }


Why not use references in all the above, and thus even avoid the extra ie.index()=index; (for it would be simplified in place)? I think the same applies below.

tautschnig · 2017-05-24T07:47:43Z

src/analyses/ai.h


 #include <util/json.h>
 #include <util/xml.h>
+#include <util/expr.h>
+#include <util/simplify_expr.h>


Why is this include required here? (I'd also debate the expr.h as it could be replaced by a forward declaration class exprt; but that's minor.)

Good point; have moved the simplify_expr.h into ai.cpp. I'm mildly reluctant to forwards declare instead of include except where necessary.

tautschnig · 2017-05-24T07:48:19Z

src/analyses/constant_propagator.cpp

@@ -331,6 +331,29 @@ void constant_propagator_domaint::assign(
  dest.set_to(lhs, rhs);
 }

+/*******************************************************************    \


That final \ seems way off. (I'm being picky about comments to make sure automated conversion works.)

tautschnig · 2017-05-24T07:51:20Z

src/analyses/interval_domain.cpp

+    if(!a.join(d))
+    {
+      unchanged=condition.is_true();
+      condition.make_true();


Why does this make sense? (I may not yet have sufficient context, but maybe a comment could be added.)

I've added some comments to explain the flow of the logic.

tautschnig · 2017-05-24T07:52:08Z

src/analyses/interval_domain.cpp

+  }
+  else
+  {
+    d.assume(not_exprt(condition), ns);


Why is this the only other case; what about, e.g., disjunction?

That is the disjunction case :-) There are three things going on here:

We want to implement this primarily to be able to check assertions, so reducing to true is sufficient. We can do better and in the new interval domain we are writing, we will, so there is a limit to how much code we want to write here.

We could work through all of the cases of exprt here but that code has to be in assume as well to handle branching. So rather than have a wonky duplication, we really want to implement this using assume, merge, top, bottom, etc. which is sufficient to reduce to true.

But converting the expression to a domain and doing domain things means we are limited to what the domain can express. Thus disjuncts are a problem. 1 <= a && a <= 2 can be repesented exactly but a < 1 || a > 2 can't. The logic for "put this expression into the most representable normal form" should be in assume a it will be needed there anyway. Thus this call, with the negation, is meant to help it in the case of disjunctions.

How much of that should have been in the comments? :-)

Have added a shortened version of this to explain why it is implemented in the way it is.

tautschnig · 2017-05-24T07:54:10Z

src/analyses/interval_domain.h

@@ -40,10 +40,15 @@ class interval_domaint:public ai_domain_baset
    const ai_baset &ai,
    const namespacet &ns) const final;

+  bool join(const interval_domaint &b);


Why is "join" being introduced here, i.e., why not implement this functionality in merge?

Merge's signature is fixed and requires location arguments. It seemed better to split merge into two (the common interface and join, what is actually does the update) and use join when I wanted to compute the join of two abstract domains, independently of having their location, rather than make up false locations.

Using join (outside of merge) is to help compute ai_simplify in the conjunctive case.

Ok, seems fair. What irritated me a bit about this was the two verbs with very similar meaning (in this context). Using different verbs suggests that they do different things, but then the difference is very hard to find out (especially when merge just calls join). Can we maybe only use one of the two, or else have a comment that explains the difference?

Join is the mathematical operation on the domains. We use this (in merge) to merge together different states. There are uses of join that are not merging (as in ai_simplify) and ways of merging (like delayed joins) that are not (just) join.

... and no-one who hasn't read that or a lot of AI literature will understand that so I'll add it to the comments :-)

…i.cpp. This means that <sstream> is no longer included in ai.h as requested in review.

… domain operation.

tautschnig · 2017-05-24T09:11:13Z

FWIW, will approve once the changes have been pushed (and I get back to my desk).

martin-cs · 2017-05-24T09:20:54Z

I have fixed / responded to all of the review comments and pushed the new version.

tautschnig · 2017-05-24T09:26:39Z

Looks ok to me. I'm assuming @danpoe and @peterschrammel have been closely involved anyway, as documented in #472.

peterschrammel · 2017-05-24T09:31:50Z

src/analyses/interval_domain.cpp

+    a.make_top();                         // a is everything
+    a.assume(condition, ns);              // restrict a to an over-approximation
+                                          // of when condition is true
+


Remove one blank line.

martin-cs · 2017-05-24T09:33:57Z

@danpoe and @thk123 wrote some parts and have been involved (I have tried to preserve authorship but I've had to split / merge / re-order commits and it can get lost). @peterschrammel has reviewed some of it and is ... aware... of what is going on.

martin-cs · 2017-05-24T09:37:40Z

PS There are test cases for these but they depend on the front-end refactoring and are thus in part .. N where N > 2.

martin-cs · 2017-05-24T09:47:41Z

For full correctness, there might still be some bits of code that @lucasccordeiro wrote in some of these parts as well. I've tried to preserve authorship; sorry if it's got lost.

peterschrammel · 2017-05-24T11:31:48Z

@martin-cs, is this ready to go or do you want to amend this PR?

martin-cs · 2017-05-24T11:32:16Z

@peterschrammel 2 mins?

martin-cs · 2017-05-24T11:39:16Z

I've pushed a version with more comments to address @tautschnig 's concerns. Assuming that passes all of the tests, then it should be good to go.

martin-cs mentioned this pull request May 23, 2017

Goto analyzer #472

Closed

tautschnig mentioned this pull request May 24, 2017

Goto analyzer 5 part1 #953

Merged

tautschnig requested changes May 24, 2017

View reviewed changes

martin and others added 4 commits May 24, 2017 09:16

Add a utility function to replace_symbol.

8486086

Add function header that was omitted in the previous merge.

7468205

Move the default implementations of output_json and output_xml into a…

ef406a0

…i.cpp. This means that <sstream> is no longer included in ai.h as requested in review.

Make evaluation and/or simplification of conditions/expressions an ai…

050cc59

… domain operation.

martin-cs force-pushed the goto-analyzer-5-part2 branch from fa35016 to ff112c8 Compare May 24, 2017 09:17

tautschnig approved these changes May 24, 2017

View reviewed changes

peterschrammel approved these changes May 24, 2017

View reviewed changes

martin-cs force-pushed the goto-analyzer-5-part2 branch from ff112c8 to 15f628e Compare May 24, 2017 10:34

martin and others added 2 commits May 24, 2017 12:36

Implement ai_simplify for intervals.

409d6ef

Implement ai_simplify for the constant domain.

c64448b

martin-cs force-pushed the goto-analyzer-5-part2 branch from 15f628e to c64448b Compare May 24, 2017 11:37

peterschrammel assigned kroening May 24, 2017

peterschrammel added enhancement Static Analyses labels May 24, 2017

kroening merged commit fe7b88a into diffblue:master May 24, 2017

thk123 mentioned this pull request Jul 3, 2017

Fixing simplification of LHS #1070

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Goto analyzer 5 part2 #961

Goto analyzer 5 part2 #961

martin-cs commented May 23, 2017

tautschnig left a comment

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig May 24, 2017

martin-cs May 24, 2017

tautschnig commented May 24, 2017

martin-cs commented May 24, 2017

tautschnig commented May 24, 2017

peterschrammel May 24, 2017

martin-cs May 24, 2017

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017

peterschrammel commented May 24, 2017

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017

Goto analyzer 5 part2 #961

Goto analyzer 5 part2 #961

Conversation

martin-cs commented May 23, 2017

tautschnig left a 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

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

tautschnig commented May 24, 2017

martin-cs commented May 24, 2017

tautschnig commented May 24, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017

peterschrammel commented May 24, 2017

martin-cs commented May 24, 2017

martin-cs commented May 24, 2017