Goto analyzer 6 part2 #1487

martin-cs · 2017-10-16T10:12:07Z

Additions to the ai_domain_baset and ai_baset interfaces as well as some general fixes to the abstract interpreter. Best reviewed as a series of independent commits. Contains some work by @danpoe although somehow he is no longer attached to the commit messages.

Thoughts from @thk123 @peterschrammel @tautschnig @chrisr-diffblue would be most appreciated.

Hopefully only one more goto-analyzer PR to go after this!

thk123

A few suggestions that you might want to look at but on the whole looks good.

thk123 · 2017-10-17T12:25:44Z

src/analyses/interval_domain.h

  {
    make_top();
  }

+  bool is_bottom() const override final
+  {
+    // This invariant should hold but is not correct enforced at the moment.


Nit: correct->correctly.

If it is known, explaining when it is not correctly enforced would greatly improve this comment.

Fixed.

I don't know for sure. My guess is that merge or transform for assume/goto is setting it to bottom in some way that isn't expected / correct. I know Lucas was chasing some issues like that. The patch that adds this originally came from @danpoe and he had added it commented out. Given that there are design issues with this domain (like, it doesn't handle pointers, at all) and we are writing a replacement (which will) I'm not inclined to spend too much time on this. So I'm content for it to be documented as a design aim but not enforced.

thk123 · 2017-10-17T12:28:35Z

src/analyses/ai.h

@@ -162,6 +162,17 @@ class ai_baset
    fixedpoint(goto_function.body, goto_functions, ns);
  }

+  /// \brief Returns the abstract state before the given instruction
+  virtual const ai_domain_baset & abstract_pre(


Nit: The \brief tag isn't actually required here (just /// Returns the abstract state before the given instruction is sufficent).

You might consider giving this function a more meaningful name abstract_state_pre_instruction? get_state_pre_instruction? Or perhaps taking an enum state_when { BEFORE_INSTRUCTION, AFTER_INSTRUCTION }?

Fixed and renamed to abstract_precondition and abstract_postcondition.

thk123 · 2017-10-17T12:29:52Z

unit/analyses/ai/ai_simplify_lhs.cpp

@@ -33,6 +33,10 @@ class constant_simplification_mockt:public ai_domain_baset
  {}
  void make_entry() override
  {}
+  bool is_bottom() const override
+  { return true; }


Probably this should be return false so the mock is at least consistent? Alternatively, an UNREACHABLE so that the test isn't using it.

It is not, formally speaking, wrong for an abstraction to be both top and bottom at the same time. It means that it is an abstraction that only has one possible state.

But, yeah, UNREACHABLE as well would be good.

martin-cs · 2017-10-18T15:51:46Z

I believe I have addressed all of thk123's comments. @peterschrammel , @tautschnig or @kroening any chance you could have a look and merge if you are happy.

thk123

Approving again to confirm my changes have been applied

thk123 · 2017-10-18T16:32:14Z

unit/analyses/ai/ai_simplify_lhs.cpp

+  bool is_bottom() const override
+  {
+    UNREACHABLE;
+    return true;


I think in general we do not need to return after unreachable since this is considered at least an exception if not an abort.

True; although i don't see the harm in doing so. It should avoid some over-zealous compiler warnings.

peterschrammel · 2017-10-19T19:54:10Z

src/analyses/ai.h

@@ -158,6 +162,17 @@ class ai_baset
    fixedpoint(goto_function.body, goto_functions, ns);
  }

+  /// Returns the abstract state before the given instruction
+  virtual const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett l) const = 0;


l and 1 are almost indistinguishable. Maybe use t

peterschrammel · 2017-10-19T19:57:16Z

src/analyses/interval_domain.h

+  bool is_bottom() const override final
+  {
+    // This invariant should hold but is not correctly enforced at the moment.
+    // DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),


Use #ifdef 0 to deactivate code

Since we are finding a fixed point we do the same things we do for loops when we find a recurssive function - we descend into it and carry on. Previously we were never doing the transforms from the recurssive function call to the start of the function meaning we would not realise it can be called with multiple parameters. Further, we weren't doing the transform from after the recursive function call onwards, meaning for some inputs it would incorrectly conclude the function never returned. Now we just do the transforms ignoring the fact it could be recursive. For the constants domain this is OK as a fixed point will be found quickly. For other domains we will need to implement some sort of widening. Included a test for recursion.

…sitivity domain. This change was cherry-picked from much later in the variable-sensitivity patch set. It makes sense to include it here as the changes are independent and apply to many domains. However the test case requires options that have not been added yet and so is disabled for now.

…ation. Previously, to access the domain for at a particular location, you had to use the operator[] interface in ait<domainT> (or subclass), which meant that the code had to be written / templated / duplicated for each domainT, even when the only interface that was being used was the ai_base_domaint one. This is the case for various tasks in goto-analyzer. This interface should also support flow-insensitive or context-dependent AI engines.

martin-cs · 2017-10-19T22:48:39Z

Should be all good now.

mgudemann · 2017-10-20T07:07:12Z

src/analyses/ai.h

+  virtual const ai_domain_baset & abstract_state_after(
+    goto_programt::const_targett l) const
+  {
+    return abstract_state_before(std::next(l));


this is probably because I don't know enough details about AI, but doesn't next; before point to l again ?

The domains are conceptually stored "between" instructions, so moving to the next instruction and asking for the state before it is the same as asking for the state after an instruction.

mgudemann · 2017-10-20T08:13:15Z

src/analyses/interval_domain.h

  {
    make_top();
  }

+  bool is_bottom() const override final
+  {
+    // This invariant should hold but is not correctly enforced at the moment.


could this be marked as TODO to be easily found? or is there already an issue?

There isn't directly an issue because there are many things wrong with the interval domain. For example, the majority of the transformers are not implemented, it will produce unsound results in the presence of writes to pointers, etc. The goal is to implement an interval abstraction within the variable sensitivity domain which doesn't have these design-level problems and then deprecate this. There are various PRs for that and I am reluctant to spend too much more time on this interval domain as it cannot be developed to the level of correctness that the other one can.

mgudemann · 2017-10-20T08:14:41Z

src/analyses/interval_domain.h

+
+  bool is_top() const override final
+  {
+    return !bottom && int_map.empty() && float_map.empty();


with the above, is this then correct?

That is an interesting question. It seems to work for the use cases it has currently been deployed for but ... TBH ... I am kinda suspicious about this domain and would not recommend it's use.

739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table 429c13f Merge pull request diffblue#1520 from smowton/smowton/fix/symbol_table_writer_erase d9f3a2f Revert "Disable OSX builds" 81bb39c Symbol-table writer: fix use of map key after erasure 021fe8f Merge pull request diffblue#1492 from tautschnig/perf-test 0729e3d Merge pull request diffblue#1517 from NathanJPhillips/bugfix/journaling-symbol-table-constructor 93ae9f3 Merge pull request diffblue#1527 from diffblue/revert-1510-always-inline c4ed1ae Revert security-scanner version of recording symbol table e83e307 Fixed scope of moved symbol 535f1df Revert "Fully process always_inline" 0096451 Replace broken copy constructor with move constructor a6adb19 Fix more catch std::string occurances 22a876f Merge pull request diffblue#1523 from reuk/reuk/update-compiling-instructions 8fe258b Update COMPILING with cmake setup instructions 99592b3 Merge pull request diffblue#1504 from andreast271/update-windows-build dff22b8 Make Windows compilation instructions more prescriptive bc3bc8f Merge pull request diffblue#1511 from tautschnig/fix-graphml 358829c Merge pull request diffblue#1510 from tautschnig/always-inline 3e77dd6 Merge pull request diffblue#1496 from smowton/smowton/feature/symbol_table_writer d115b4e catch by const ref instead of by value or non-const ref 444d824 Fix graphml output of concurrency witnesses 08c512d Make Windows compilation instructions more prescriptive bcf8ff3 Update documentation for building cbmc on windows. Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line. 728dbb5 Merge pull request diffblue#1508 from smowton/smowton/1420-fragments/value_set_debugging 9d9e50d Merge pull request diffblue#1507 from smowton/smowton/1420-fragments/factor_java_object_init b2104b0 Merge pull request diffblue#1506 from smowton/smowton/1420-fragments/typecheck_expr_cleanup 7175efe Merge pull request diffblue#1505 from smowton/smowton/1420-fragments/invariants 7537302 Adding a java_lang_object_init function 86513ee Merge pull request diffblue#1324 from reuk/reuk/clang-format ea4a777 Merge pull request diffblue#1503 from reuk/reuk/rebuild-ansi-c-when-necessary d9c0598 [pointer-analysis] Better debugging information in pointer analysis 3146336 Remove unnecessary includes in java-typecheck 10b5c8e [java-bytecode/typecheck] Style: Changing assertions in preconditions 2afe377 Fully interpret __attribute__((always_inline)) 8eaf89e Apply symbol replacement in type_arg members 13a7553 Rebuild ansi-c library if non-source dependencies change b97a766 Merge pull request diffblue#1403 from karkhaz/kk-regenerate-arch-flags-binaries a4dc986 Merge pull request diffblue#1484 from diffblue/interpreter_size_t 9d4e0ca Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs c3e6726 Script to automate performance evaluation of CBMC on AWS 912ee38 Improve symbol table style 6b1a49d Add missing goto-statistics file to Makefile d512204 Add cbmc and jbmc as install targets bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019 c5c77ac Merge pull request diffblue#1495 from diffblue/codeowners2 f154d16 Merge pull request diffblue#1487 from martin-cs/goto-analyzer-6-part2 4955417 initialize_goto_model now returns a goto_model 56f924c Merge pull request diffblue#1483 from diffblue/signature_initialize_goto_model eef32db Methods for ai_baset to allow access to the ai_base_domaint for a location. aae984a Disable the regression test for now as it depends on the variable sensitivity domain. 3050c53 Don't stop when recursion found 93f2e1f Use is_bottom() to catch unreachable functions. 5b604ae Update the mock domain with the new ai_domain_baset interface. f9ca353 Add is_bottom() and is_top() to ai_domain_baset and derived domains. 88d8673 Rename the XML output to something a bit more meaningful. 2110cd1 Make formatting stage non-blocking on Travis a24ac3d Fixup compiling.md with more clang-format install instructions c3c24e2 Add symbol table writer 98643d7 initialize_goto_model now returns a goto_model fd6acc5 initial proposal for owners of code f39ae5c use mp_integer for addresses f6ae635 use std::size_t in interpreter 55e6594 Fixup cpplint.py 9d4b827 Update coding standard 8482b35 Add information about using clang-format 1dcc82c Convert COMPILING to markdown format 554cb54 Adjust cpplint to disable whitespace checks by default 6ce0dba Add travis style check f18979a Add clang-format config 622e2e3 Merge branch 'develop' into show_functions_dfs bea696a Regenerated cross-compiled arch flag test binaries 1fab1c1 Fixed show-call-sequences deature of goto instrument; added test suite git-subtree-dir: cbmc git-subtree-split: 739c7f5

martin-cs force-pushed the goto-analyzer-6-part2 branch 2 times, most recently from afa4670 to b06727c Compare October 16, 2017 10:59

martin-cs mentioned this pull request Oct 16, 2017

Goto analyzer #472

Closed

martin-cs force-pushed the goto-analyzer-6-part2 branch from b06727c to 4a6c553 Compare October 16, 2017 13:51

thk123 approved these changes Oct 17, 2017

View reviewed changes

martin-cs force-pushed the goto-analyzer-6-part2 branch from 4a6c553 to 0a429ae Compare October 18, 2017 15:49

thk123 approved these changes Oct 18, 2017

View reviewed changes

peterschrammel approved these changes Oct 19, 2017

View reviewed changes

Rename the XML output to something a bit more meaningful.

88d8673

martin-cs force-pushed the goto-analyzer-6-part2 branch from 0a429ae to 666b9ef Compare October 19, 2017 22:45

martin and others added 6 commits October 19, 2017 23:47

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

f9ca353

Update the mock domain with the new ai_domain_baset interface.

5b604ae

Use is_bottom() to catch unreachable functions.

93f2e1f

martin-cs force-pushed the goto-analyzer-6-part2 branch from 666b9ef to eef32db Compare October 19, 2017 22:47

mgudemann reviewed Oct 20, 2017

View reviewed changes

mgudemann merged commit f154d16 into diffblue:develop Oct 20, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Goto analyzer 6 part2 #1487

Goto analyzer 6 part2 #1487

martin-cs commented Oct 16, 2017

thk123 left a comment

thk123 Oct 17, 2017

martin-cs Oct 18, 2017

thk123 Oct 17, 2017

martin-cs Oct 18, 2017

thk123 Oct 17, 2017

martin-cs Oct 17, 2017

martin-cs Oct 18, 2017

martin-cs commented Oct 18, 2017

thk123 left a comment

thk123 Oct 18, 2017

martin-cs Oct 18, 2017

peterschrammel Oct 19, 2017

martin-cs Oct 19, 2017

martin-cs Oct 19, 2017

peterschrammel Oct 19, 2017

martin-cs Oct 19, 2017

martin-cs Oct 19, 2017

martin-cs commented Oct 19, 2017

mgudemann Oct 20, 2017

martin-cs Oct 20, 2017

mgudemann Oct 20, 2017

martin-cs Oct 20, 2017

mgudemann Oct 20, 2017

martin-cs Oct 20, 2017

Goto analyzer 6 part2 #1487

Goto analyzer 6 part2 #1487

Conversation

martin-cs commented Oct 16, 2017

thk123 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

martin-cs commented Oct 18, 2017

thk123 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

martin-cs commented Oct 19, 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