Goto analyzer 5 part3 #966

martin-cs · 2017-05-24T17:15:14Z

The next part of the goto-analyzer grand merge. This fixes a variety of issues with the constant domain and adds a few utility functions needed to improve ait.

Problems:
*. There are test cases that show why these are needed but they are intertwined with a number of other changes (what will become part4!) and the association between test case and fix has been lost.

Mitigations:
*. This doesn't break any of the existing test cases.
*. The constant domain isn't in heavy use.
*. When we start merging in the variable sensitivity domain ( #708 dependent on this / #472 ) we will have a much better constant propagator, one that is actually correct with respect to aliasing and indirection, for example. I hope this will become the default constant domain so these changes might become largely a legacy issue.

If it would make more sense, I can squash together the constant domain fixes.

tautschnig

I'm not entirely sure about all concerns, so I'm not making this quite as firm as "request changes".

tautschnig · 2017-05-25T15:01:08Z

src/analyses/ai.h

+  virtual bool is_bottom() const=0;
+
+  // the analysis doesn't use this,
+  // and domains may refuse to implement it.


This comment just tells us why it should not be here. Maybe also explain why it is being added?

Yeah... I'm going to remove the comment because we're not using is_top() right now but ... it's the kind of thing we may well start using. As there is a make_top() method the domain must have a representation of it so it shouldn't be too great a burden on the programmer.

tautschnig · 2017-05-25T16:24:38Z

src/analyses/constant_propagator.cpp

+  // values
+  const constant_propagator_ait *cp=
+    dynamic_cast<constant_propagator_ait *>(&ai);
+  bool have_dirty=cp!=NULL;


Use nullptr

tautschnig · 2017-05-25T16:25:57Z

src/analyses/constant_propagator.cpp

-      else
-        two_way_propagate_rec(g, ns);
+      two_way_propagate_rec(g, ns);
+      assert(!values.is_bottom); // for now


If it says "for now": what will happen later?

Good question... @danpoe? @lucasccordeiro? I don't think I wrote this.

I can give a very meta-answer; this will be deprecated in favour of the variable precision domain configured to handle constants.

I think the two way propagation (which handles the variable propagation through gotos, e.g. [a == 3] goto ...) is disabled in this commit (the body of two_way_propagate_rec()) is commented out). Therefore propagating through the goto can never yield bottom which the assertion checks for. When two way propagation is enabled again in the future the assertion will not hold anymore.

Have added a comment saying this.

tautschnig · 2017-05-25T16:40:08Z

src/analyses/constant_propagator.h

@@ -106,28 +150,32 @@ class constant_propagator_domaint:public ai_domain_baset
 class constant_propagator_ait:public ait<constant_propagator_domaint>
 {
 public:
+  explicit constant_propagator_ait(const goto_functionst &goto_functions) :


Nit: no space in front of ":" I believe

tautschnig · 2017-05-25T16:40:47Z

src/analyses/constant_propagator.h

  constant_propagator_ait(
    goto_functionst &goto_functions,
-    const namespacet &ns)
+    const namespacet &ns) : dirty(goto_functions)


As above: no space around ":"

tautschnig · 2017-05-25T16:54:08Z

src/util/replace_symbol.cpp

+    if(!replace(ie.array(), replace_with_const))
+      result=false;
+
+    if(!replace(ie.index()))


Why is it not ok to replace the index by a constant?

I'm not quite sure what you mean but it seems (from the diff and context -- please confirm @danpoe) that the replace_with_const flag is to ensure that an l-value is still a valid l-value after substitution. For example if your expression is "a[i]" then substituting i for a constant results in an l-value but substituting a for a constant (array) wouldn't.

@martin-cs: Exactly.

@tautschnig: The index is always replaced here. The if is there to check the return value of replace() which indicates whether the expression was simplified.

I have documented what the flag does and why it is needed.

Ah, I just got confused by the fact the default value is true.

tautschnig · 2017-05-25T16:56:00Z

src/util/replace_symbol.cpp

-      dest=it->second;
+      const exprt &e=it->second;
+
+      if(!replace_with_const && e.is_constant())


This test could be placed even before the to_symbol_expr to spare some unnecessary lookups.

I don't think it works because you need to to_symbol_expr to get the symbol to look up in the substitution table, which gives you e (what you are substituting) and you need that for the condition (because it is only an issue if you are replacing with a constant).

tautschnig · 2017-05-25T16:56:25Z

src/util/replace_symbol.cpp

+  else
+  {
+    Forall_operands(it, dest)
+      if(!replace(*it))


Why not forward the second parameter here?

I don't think this is needed as it's only the "outermost" address-of, index, member, etc. that you need to catch. The logic is similar to:

https://github.com/diffblue/cbmc/blob/master/src/analyses/ai.cpp#L83

I guess I now understand why I have once been told that default values should not be used. (Yes, I do also use them, but reading code with limited context is a lot harder when default values are used.)

danpoe · 2017-05-27T15:24:26Z

I've had a look through the diff and it all looks good to me.

martin-cs · 2017-05-28T16:57:11Z

I have addressed all comments and pushed an updated version.

martin-cs · 2017-06-09T12:11:01Z

Rebased to deal with documentation changes.

peterschrammel · 2017-06-09T16:10:23Z

src/analyses/constant_propagator.cpp


-  if(r_it != replace_const.expr_map.end())
+Function: constant_propagator_domaint::valuest::set_dirty_to_top


Adapt to doxygen comments.

peterschrammel · 2017-06-09T16:12:26Z

src/util/replace_symbol.h

@@ -38,7 +38,21 @@ class replace_symbolt
    type_map.insert(std::pair<irep_idt, typet>(identifier, type));
  }

-  virtual bool replace(exprt &dest) const;
+  /* If you are replacing symbols with constants in an l-value, you can


Adapt to doxygen comments.

peterschrammel · 2017-06-25T22:27:50Z

src/analyses/constant_propagator.cpp

    out << "  bottom\n";
+    assert(replace_const.expr_map.empty());


use INVARIANT etc (whole PR)

peterschrammel · 2017-06-25T22:47:41Z

src/analyses/constant_propagator.h

-    const namespacet &ns) const override;
+    const namespacet &ns) const final override;
+
+  virtual void make_bottom() final override


virtual not needed (and other functions below)

peterschrammel · 2017-06-25T22:48:16Z

src/analyses/constant_propagator.h

  {
    operator()(goto_function, ns);
    replace(goto_function, ns);
  }

+  dirtyt dirty;


Why should this be public?

peterschrammel · 2017-07-03T19:45:18Z

@martin-cs, @danpoe, @thk123, action required here to unblock a whole lot of dependent PRs...
The next steps after that seem to be: #472 -> #708 -> #1020 -> #1070 -> ...

martin-cs · 2017-10-16T11:08:46Z

Obsoleted by #1475

martin-cs mentioned this pull request May 24, 2017

Goto analyzer #472

Closed

tautschnig reviewed May 25, 2017

View reviewed changes

martin-cs force-pushed the goto-analyzer-5-part3 branch from 45c564f to 7c0f038 Compare May 28, 2017 16:54

tautschnig approved these changes May 30, 2017

View reviewed changes

martin-cs force-pushed the goto-analyzer-5-part3 branch from 7c0f038 to aad0591 Compare June 9, 2017 12:09

martin and others added 6 commits June 15, 2017 15:04

Fix constant propagator.

08a2f8a

disable two-way propagation for now

956225f

Addressing constant domain review comments by Daniel Poetzl.

1b13114

constant propagator fix

e2fdcbf

Add is_bottom() and is_top() to ai_domain_baset and derived domains.

3178f1b

Use is_bottom() to catch unreachable functions.

5606ce5

martin-cs force-pushed the goto-analyzer-5-part3 branch from aad0591 to 5606ce5 Compare June 15, 2017 14:08

peterschrammel requested changes Jun 25, 2017

View reviewed changes

peterschrammel mentioned this pull request Jun 26, 2017

Fix constant propagator merge operator #1057

Closed

thk123 mentioned this pull request Jul 3, 2017

Fixing simplification of LHS #1070

Merged

tautschnig assigned martin-cs Aug 20, 2017

tautschnig changed the base branch from master to develop August 22, 2017 12:24

martin-cs mentioned this pull request Oct 12, 2017

Goto analyzer 6 part1 #1475

Merged

martin-cs closed this Oct 16, 2017


		if(r_it != replace_const.expr_map.end())
		Function: constant_propagator_domaint::valuest::set_dirty_to_top

Goto analyzer 5 part3 #966

Goto analyzer 5 part3 #966

Uh oh!

Conversation

martin-cs commented May 24, 2017

Uh oh!

tautschnig left a comment

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!

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!

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!

danpoe commented May 27, 2017

Uh oh!

martin-cs commented May 28, 2017

Uh oh!

martin-cs commented Jun 9, 2017

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!

peterschrammel commented Jul 3, 2017

Uh oh!

martin-cs commented Oct 16, 2017

Uh oh!

Uh oh!