Feature/context sensitive ait merge 2 #2622

martin-cs · 2018-07-26T11:19:52Z

Part 2 of merging the context sensitive analysis patch set. Changes the signature of a newer part of the API (getting domains). This is necessary if we are going to have more than one domain per location and still want to be able to talk about "the domain at this location", because that requires a merge. I suggest reviewing one patch at a time. FAO @smowton and @chrisr-diffblue

thk123 · 2018-07-26T11:50:38Z

I think the commit ordering as got messed up here (afaict the first commit is "Update goto-analyzer tasks to take account of the ait API changes" and doesn't look like it would compile). Could you post the correct ordering (or @thomasspriggs has a command the rebases and re-timestamps the commits so they appear in the right order).

smowton · 2018-07-26T12:08:45Z

@thk123 I think the branch itself shows the right order: https://github.com/martin-cs/cbmc/commits/feature/context-sensitive-ait-merge-2

martin-cs · 2018-07-26T12:29:47Z

I'm pretty sure that it isn't the order I left the commits in :-\ Also, all of @smowton 's comments have deassociated from the lines so I don't know what they are referring to.

chrisr-diffblue

Similar general concerns as Chris, with additional query around the possibility of changed behaviour for function pointer dereference.

chrisr-diffblue · 2018-07-26T12:26:08Z

src/analyses/ai.cpp

+
+  // We can't really do this here -- we rely on
+  // these being removed by some previous analysis.
+  PRECONDITION(function.id()!=ID_dereference);


It looks like previously this function would still return if it got a dereference, where as now it's going to hit a precondition... Is that a change in behaviour? And does this somehow prevent us ever using AI to resolve function pointers?

Previously it would ignore function pointers, giving unsound results. However it was always used with the implicit (undocumented!) precondition that function pointers and returns had been removed.

It doesn't prevent us handling function pointers; we'd just need to add the branch back in, once we'd dealt with the return removal issues.

smowton · 2018-07-26T12:35:50Z

Heh, ok I commented a bit wrong. @martin-cs go to https://github.com/martin-cs/cbmc/commits/feature/context-sensitive-ait-merge-2 and click through the commits to see them properly.

The ordering problem stems from Github listing by author date here, which gets messed with by rebasing. The git log default order is usually better, which AFAIK is what the branch commits view uses.

martin-cs · 2018-07-26T12:37:07Z

@smowton Thanks : will work through and respond there.

martin-cs · 2018-07-26T14:15:48Z

I've pushed a new version that addresses all of @smowton 's comments, clangs things and adds a separate patch to restrict to function.id() == ID_symbol.

smowton · 2018-07-26T14:16:40Z

@martin-cs did you get to the bottom of the unit test that broke the function-must-be-symbol invariant?

martin-cs · 2018-07-26T14:17:07Z

... and now with the squash @smowton requested.

martin-cs · 2018-07-26T14:17:41Z

@smowton : CI test results were weird; will review the latest set.

martin-cs · 2018-07-26T15:27:56Z

All comments addressed; let's see if we can pass CI...

peterschrammel · 2018-07-26T12:43:36Z

src/analyses/ai.h

@@ -82,15 +82,22 @@ class ai_baset
    finalize();
  }

+  /// Accessing individual domains at particular domains


at particular domains??

peterschrammel · 2018-07-26T12:44:45Z

src/analyses/ai.h

-  virtual const ai_domain_baset & abstract_state_before(
-    goto_programt::const_targett t) const = 0;
+  /// PRECONDITION(l is dereferenceable)
+  virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;


I'm wondering whether this shouldn't use optional?

What would be the use-case for it not returning anything?

Why can't it just return a const ref? I'm unsure where the return value comes from.

In this case it could and used to return a constant ref. However if we are going to break the 1-to-1 link between location and domain (which is the whole point of this patch set) then we have to be able to support cases where the abstract interpreter may not have the domain and may have to compute it in this function. For example : merging all of the different contexts that reach this point or dynamically recomputing the domain from the last merge point. That's why the API needs to change.

peterschrammel · 2018-07-26T16:33:57Z

src/analyses/ai.cpp

-    if(it==goto_functions.function_map.end())
-      throw "failed to find function "+id2string(identifier);
+  if(it == goto_functions.function_map.end())
+    throw "failed to find function " + id2string(identifier);


Shouldn't that be an INVARIANT?

Yes; yes it probably should be. Fixed.

martin-cs · 2018-07-26T17:26:27Z

@smowton : the unit test is looking to be an interesting case. I think what is happening is the program that is produced directly by the unit test is not well formed ( as ever #751 ) and this is causing a failure as I tighten up the invariants in ait. I fear this may be a question of how we maintain the code in unit/ that builds programs directly.

smowton · 2018-07-27T08:29:39Z

@martin-cs what did the unit test do wrong?

martin-cs · 2018-07-27T09:17:24Z

@smowton : just working on that...

martin-cs · 2018-07-27T12:03:02Z

@smowton : It is a well-formed-ness invariant issue, but not the one I thought.

The unit test is calling the "analyze one function" interface of ait which is not widely used elsewhere.
It works by creating an arbitrary, empty goto_functions structure and then continuing as normal. This is fine because, apart from function calls, completely ignores the goto_functions structure.
My patch checks some "obvious" invariants on the well-structured-ness of the goto_functions structure, which fail because of how it was created.

My solution is to patch ait so that when it builds a goto_functions structure, it builds one that is at least vaguely correctly structured.

martin-cs · 2018-07-27T12:38:23Z

Except, ofcourse, it's not that simple. To build a faintly correctly structured goto_functions we are going to have to (deep) copy or move the goto_program. This means that once the analysis is finished, the results will be inaccessible as the locationt's will have died along with the goto_functions.

So I'm going to remove the invariants for now, as they are just checking well-structured-ness properties of the goto-program; nothing to do with the abstract interpretation itself. Once we have some progress on #751 I think we should re-visit whether:

void operator()(const goto_programt &goto_program, const namespacet &ns)
void operator()(const goto_functionst::goto_functiont &goto_function, const namespacet &ns)

are really interfaces we want or whether they should be goto_modelt plus irep_idt for the function to analyze.

This allows us to be a lot more flexible about the relationship between location and domain rather than assuming it is a 1-to-1 map.

This is mostly using accessor functions rather than directly using inherited members but it allows a slightly greater degree of independence.

martin-cs · 2018-07-27T13:19:17Z

The only blocking thing is cmake, which seems to die without any kind of useful information. Is this a known travis glitch? Can anyone who understands it help?

martin-cs · 2018-07-27T13:48:05Z

With my thanks to @chrisr-diffblue CI is now complete and all comments from reviews have been applied. @smowton @chrisr-diffblue @peterschrammel and @thk123 : more thoughts / requests / changes?

allredj

Passed Diffblue compatibility checks (cbmc commit: 28ba192).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80219976

5d3ea03 Merge pull request diffblue#2693 from zhixing-xu/fix_rw_range_upper 2b40338 Update test.desc c6d0427 Merge pull request diffblue#2674 from diffblue/msvc-link 318474f Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3 c63030f Regression test for goto-link personality 64fedd0 Microsoft LINK personality d9f9dd9 Merge pull request diffblue#2688 from tautschnig/concat-dir-file 99946fc Merge pull request diffblue#2675 from diffblue/goto-cl-echo-file 252d857 Merge pull request diffblue#2687 from tautschnig/fo-directory 0d7ebd5 Fixed a problem where the rw_set range's upper bound not set correctly 29eab32 goto-cl: Fail invocation of trying to compile multiple files to non-directory 7f587c4 Fix concat_dir_file for Windows and unit-test it a44468b Document string_builtin_function::eval ecc0e43 Document eval_is_upper_case a345d30 Document eval_string 58307a0 Tests for String.toUpperCase 71de2e3 Tests for String.toLowerCase 579d00c Remove redundant function application ID check e2961b5 Add builtin class for string_to_upper_case fe9071b Make to_upper_case work for Latin-1 supplement 53ccd3f Refactor string_to_upper_case be477c9 Remove assumptions that input char are < 0x100 836cbad Extract an is_upper_case function 1137ffd Improve documentation of add_axioms_for_to_lower_case a71f2c0 Implement builtin string_to_lower_case function fae6a48 Merge pull request diffblue#2467 from tautschnig/vs-except 24de513 Merge pull request diffblue#2474 from tautschnig/vs-identifier e14f2f2 Merge pull request diffblue#2685 from diffblue/clcache-again 08698cc Merge pull request diffblue#2681 from diffblue/remove-aig d42020b remove --aig option cd4a163 AWS codebuild windows: set clcache base directory 1ba928c cleanup unnecessary path from configuration file 8c4801b Refactor add_axioms_for_to_lower_case 4291232 Merge pull request diffblue#2686 from diffblue/buildspec-apt-cache 3adb717 AWS codebuild: cache apt lists and packages 0efb169 remove AIGs 3a9c825 Merge pull request diffblue#2682 from diffblue/fix-clcache b9b5660 Merge pull request diffblue#2483 from tautschnig/vs-java-parameters a66ab1e CL prints the name of the file that's compiled onto stdout 0698a5f Merge pull request diffblue#2673 from diffblue/goto-cl-Fo 75855bf Java front-end: remove unused parameters 4df2187 debugging output to resolve seg fault 5bc7456 goto-cl: /Fo can set an output directory a43e4fa add is_directory to file_util.h 4ad91fb Codebuild for windows: set up cache path properly effb01b Merge pull request diffblue#2641 from diffblue/typedef-type 5ef2802 Merge pull request diffblue#2679 from tautschnig/version-string 2efea52 Refine test patterns to avoid spurious matches aa7ebbc Merge pull request diffblue#2672 from diffblue/goto-cc-multiple-source-files aaea781 Merge pull request diffblue#2671 from diffblue/fix_get_base_name 8b51faf fix get_base_name 694daaf gcc mode: error in case multiple files are given with -c and -o 09fdca3 Merge pull request diffblue#2643 from svorenova/fixup-nondet-static d42054a Merge pull request diffblue#2669 from diffblue/spurious-cover-test b391c9e introduce typedef_type in the C frontend 114030b Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2 46f6231 cbmc test no longer uses --cover daff1d1 Make nondet-static replace lines in CPROVER_init 1bca129 Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt 31366ad Tests for StringBuilder.setCharAt f4285e7 Add builtin support for string_set_char 2a8ea0f Better specify out-of-bounds case for set_char 9415a24 Refactor add_axioms_for_set_char 9762886 Refactor string_concat_char builtin function b62bf01 Make nondet-static check for ID_C_no_nondet_initialization a50562e Mark java.lang.String.Literals with ID_C_constant b3c08d3 Mark internal Java variables with ID_C_no_nondet_initialization f2dc978 Add a new comment to mark variables that should not be nondet initialized da7966c Merge pull request diffblue#2645 from mmuesly/feature_test_posix_memalign cb4a340 Merge pull request diffblue#2647 from diffblue/cleanout-jar-filet 2b27a2d Merge pull request diffblue#2622 from martin-cs/feature/context-sensitive-ait-merge-2 00b26a8 Adds a test for posix_memalign in stdlib.c 0f5a057 Merge pull request diffblue#2667 from tautschnig/slicer-cleanup 16e6462 Remove no-longer-used ifdef 96d345b Clean GCC conditional expressions in right-hand sides of declarations 086c266 Merge pull request diffblue#2651 from smowton/smowton/feature/unroll-enum-clone-loops f69b244 Merge pull request diffblue#2625 from smowton/smowton/feature/value-set-accuracy 730b3e2 Merge pull request diffblue#2655 from romainbrenguier/feature/extend-builtin-functions c4569dd remove java_class_loader_limitt from jar_filet e0f954d Merge pull request diffblue#2659 from smowton/smowton/fix/cmake-third-time-is-charm 7f547b1 Merge pull request diffblue#2656 from smowton/smowton/fix/testsuite-name 3a1593b Tests for String.valueOf(int) 7414d76 Add builtin support for string_of_int 0b44c89 Add version of make_string accepting iterators f81f082 Rename function to add_axioms_for_string_of_int 9a2a7c2 Switch version.cpp from a rule product to a byproduct 943d60c Value set: handle with, array and struct expressions more accurately 4f158a3 Mark regression tests as expecting failure for symex driven loading c9a53f9 Add regression tests for changes to JBMC enumeration support a985eae Interpreter: deal with member-of-constant-struct expressions 361469b Change source location of jump target in {table|lookup}switch 6270968 java-unwind-enum-static: also unwind clone loop in Enum.values() 714de0d Symex: expose call stack to unwinding decision making fb239ef Fix jbmc-generic-symex-driven-lazy-loading test name 28ba192 Strengthen the invariant on what are acceptable function calls. 773bc86 Convert various comments, asserts and throws into invariants. e65f027 Add comments to the abstract interpreter interface. 1fe0796 Convert various older domains to use the more recent ait API. afe32b7 Refactor the methods that access "the abstract domain at a location". aa743b3 Remove unused exception name from catch statement 5703504 Remove unused parameter identifier git-subtree-dir: cbmc git-subtree-split: 5d3ea03

martin-cs requested review from chrisr-diffblue, peterschrammel, smowton and thk123 as code owners July 26, 2018 11:19

chrisr-diffblue reviewed Jul 26, 2018

View reviewed changes

martin-cs force-pushed the feature/context-sensitive-ait-merge-2 branch from 9b2a98a to 179dda9 Compare July 26, 2018 14:14

martin-cs force-pushed the feature/context-sensitive-ait-merge-2 branch from 179dda9 to 6b0f65b Compare July 26, 2018 14:16

martin-cs force-pushed the feature/context-sensitive-ait-merge-2 branch from 6b0f65b to c13efe0 Compare July 26, 2018 15:26

martin-cs force-pushed the feature/context-sensitive-ait-merge-2 branch 2 times, most recently from 072b8cd to 5d08a02 Compare July 26, 2018 15:52

peterschrammel reviewed Jul 26, 2018

View reviewed changes

martin and others added 4 commits July 27, 2018 13:46

Refactor the methods that access "the abstract domain at a location".

afe32b7

This allows us to be a lot more flexible about the relationship between location and domain rather than assuming it is a 1-to-1 map.

Convert various older domains to use the more recent ait API.

1fe0796

This is mostly using accessor functions rather than directly using inherited members but it allows a slightly greater degree of independence.

Add comments to the abstract interpreter interface.

e65f027

Convert various comments, asserts and throws into invariants.

773bc86

Strengthen the invariant on what are acceptable function calls.

28ba192

martin-cs force-pushed the feature/context-sensitive-ait-merge-2 branch from 5d08a02 to 28ba192 Compare July 27, 2018 12:47

allredj reviewed Jul 27, 2018

View reviewed changes

peterschrammel approved these changes Jul 27, 2018

View reviewed changes

smowton approved these changes Jul 30, 2018

View reviewed changes

martin-cs merged commit 2b27a2d into diffblue:develop Aug 2, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feature/context sensitive ait merge 2 #2622

Feature/context sensitive ait merge 2 #2622

martin-cs commented Jul 26, 2018

thk123 commented Jul 26, 2018

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

chrisr-diffblue left a comment

chrisr-diffblue Jul 26, 2018

martin-cs Jul 26, 2018

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

peterschrammel Jul 26, 2018

martin-cs Jul 26, 2018

peterschrammel Jul 26, 2018

martin-cs Jul 26, 2018

peterschrammel Jul 26, 2018 •

edited

Loading

martin-cs Jul 26, 2018

peterschrammel Jul 26, 2018

martin-cs Jul 26, 2018

martin-cs commented Jul 26, 2018

smowton commented Jul 27, 2018

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018 •

edited

Loading

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018

allredj left a comment

Feature/context sensitive ait merge 2 #2622

Feature/context sensitive ait merge 2 #2622

Conversation

martin-cs commented Jul 26, 2018

thk123 commented Jul 26, 2018

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

smowton commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

martin-cs commented Jul 26, 2018

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

peterschrammel Jul 26, 2018 • edited Loading

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 Jul 26, 2018

smowton commented Jul 27, 2018

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018 • edited Loading

martin-cs commented Jul 27, 2018

martin-cs commented Jul 27, 2018

allredj left a comment

Choose a reason for hiding this comment

peterschrammel Jul 26, 2018 •

edited

Loading

martin-cs commented Jul 27, 2018 •

edited

Loading