Feature/context sensitive ait merge 1 #2596

martin-cs · 2018-07-24T13:09:43Z

Part 1 of merging the context sensitive analysis patch set. This is just boring refactoring at this stage. I suggest reviewing one patch at a time. FAO @smowton and @chrisr-diffblue

chrisr-diffblue · 2018-07-24T13:18:00Z

src/analyses/ai_domain.cpp

+
+Module: Abstract Interpretation
+
+Author: Martin Brain, [email protected]


IANL - but given that mostly these two new files contain code moved from other files, should the Author list at least still contain the Author from the original file? (Assuming that was accurate, which is likely debatable...)

This doesn't seem to be fixed?

@thk123 Fixed in one place but not the other. One sec...

chrisr-diffblue

Other than the one question regarding Author headers, LGTM

smowton

Except yeah, don't steal the boss' thunder ;)

smowton · 2018-07-24T13:27:48Z

Also @chrisr-diffblue I will start using IANL from now on. "Am not lawyer. Am ogre! Gnaw bones!" ;)

martin-cs · 2018-07-24T14:00:47Z

Now with bonus clang-format! Can I ask @thk123 or @peterschrammel for a merge?

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 608e310).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/79852753
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

thk123

Sorry to be a pain - I think Chris's comment isn't actually fixed and new comment should be doxygen

thk123 · 2018-07-24T14:15:20Z

src/analyses/ai_domain.cpp

+
+Module: Abstract Interpretation
+
+Author: Martin Brain, [email protected]


This doesn't seem to be fixed?

thk123 · 2018-07-24T14:19:15Z

src/analyses/ai_domain.h

+/// The interface offered by a domain, allows code to manipulate domains without
+/// knowing their exact type.
+// don't use me -- I am just a base class
+// please derive from me


Feel free to disregard as out of scope, but rather than pleading, why not just make the constructor protected? In fact - I suspect no need at all for this comment since there is a pure virtual function here anyway.

I'd originally meant to keep this as direct a "copy and paste" as I could but as I've clang formatted it... why not?

thk123 · 2018-07-24T14:19:56Z

src/analyses/ai_domain.h

+  // Simplifies the expression but keeps it as an l-value
+  virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
+
+  // Gives a Boolean condition that is true for all values represented by the


Use /// to turn this into doxygen

I have doxygen'd all of the things.

ai.{h,cpp} is already crowded with two different interfaces. The following patch set will make this much worse, thus we start by refactoring.

… API. This allows the domain to be converted to an assumption or an assertion amongst other applications.

martin-cs · 2018-07-24T14:38:43Z

@thk123 I think I have addressed all of the issues; just rebuilding / re-CI-ing.

martin-cs · 2018-07-24T15:36:44Z

@thk123 Please check my resolutions of your review comments. If you're happy then I think we are good to merge.

allredj

Passed Diffblue compatibility checks (cbmc commit: 3e0b2a5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/79867118

kroening · 2018-07-24T19:24:52Z

This is a disruptive API change; good reasons?

martin-cs · 2018-07-25T08:12:55Z

@kroening The only change to the API of ai_domain_baset is adding one method with a correct and viable default implementation. Everything else will stay as it is. Anything that includes "ai.h" will compile as before. This is mostly just a re-organisation and reformatting.

Why? ai.h is already crowded with two different interfaces (ai_baset and ai_domain_baset) as well as implementations of these. Later in this patch set a third will be added and the implementations expanded. I thought it best to keep the header file under 1000 lines and so I thought it would be good to start be refactoring things as cleanly and clearly as possible.

thk123

LGMT @kroening please hit merge if you are happy with Martin's comment - seems to me the API isn't changing (being moved file and extended in a backwards compatible way)

peterschrammel

LGTM

martin-cs · 2018-07-26T07:53:09Z

@kroening Are you happy with this one? If so I will continue with the rest of the stack.

54f3731 Merge pull request diffblue#2610 from smowton/smowton/fix/ssa-trace-unreachable-values 6397f62 Merge pull request diffblue#2626 from qaphla/local_bitvector_analysis_fix 0c0e288 Merge pull request diffblue#2423 from tautschnig/vs-negation e90b61b Transform float_utils unit test to use CATCH and enable it 8b2bd7b Convert to signed type to make negation meaningful 7823d9c Merge pull request diffblue#2606 from diffblue/ms_cl_options 0f60b26 Merge pull request diffblue#2627 from diffblue/cleanup-ansi-c-scanner f33459f Merge pull request diffblue#2529 from tautschnig/debian1 1927fb2 remove bitvector and bitvector_u rules 1e07546 Fixed secondary issues arising from local_bitvector_analysis fix. 131e525 Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID. 501546a SSA trace: don't concretise steps that will subsequently be dropped 709b45f Merge pull request diffblue#2591 from allredj/log-suffix-in-testpl f3630f0 Merge pull request diffblue#2612 from svorenova/multidim_arrays_tg3821_util c010edb Merge pull request diffblue#2623 from diffblue/cbmc-empty-message d5adef5 Merge pull request diffblue#2624 from diffblue/va_arg_mode 3e3303d symbols for va_args need a mode 398dd39 cbmc: avoid an empty message during result reporting 8bca5cd Merge pull request diffblue#2585 from smowton/smowton/admin/java-clean-deref-tests a0e339d Disable broken string test d0cf433 Strengthen local_safe_pointers to handle common Java operations e7b1a8a Merge pull request diffblue#2616 from smowton/smowton/admin/ai-unit-test 738ecad Merge pull request diffblue#2621 from diffblue/amazon-linux-instructions 4156283 Add test for ait framework 08bd1a8 Merge pull request diffblue#2596 from martin-cs/feature/context-sensitive-ait-merge-1 c572866 Use can_cast_type instead of raw type id check a1ab7a6 Improve documentation for java array types 745670b instructions for Amazon Linux 299417b Merge pull request diffblue#2614 from chrisr-diffblue/is_zero_bitfield_support 0c8eff6 Merge pull request diffblue#2598 from mmuesly/feature_posix_memalign fad7735 Merge pull request diffblue#2613 from NathanJPhillips/cleanup/irep_ids-def-not-h e34fc57 Merge pull request diffblue#2600 from peterschrammel/doxygen-graphviz 54cc818 clang-format fixups 9986ea1 Make exprt::is_zero() support bitfields dbf4384 Merge pull request diffblue#2605 from NathanJPhillips/feature/cast-for-code_typet 7798aaa Updated comment for the fact that IDs are defined in def files now b72b968 Remove unused function e66f76f Add a check functions for (multi-dimensional) array types f4f4190 Added can_cast_type implementation for code_typet f6c34f2 Merge pull request diffblue#2603 from smowton/smowton/fix/stub-string-lengths 9c9c375 two further Visual Studio CL options 05bebb7 Merge pull request diffblue#2595 from thk123/doc/use-can-cast 9a75c65 Merge pull request diffblue#2597 from allredj/update-jbmc-gitignore c98688b Fix stub string lengths 819560f Merge pull request diffblue#2601 from owen-jones-diffblue/owen-jones-diffblue/update-codeowners-3 39323e0 Remove code owners from low-risk files 8f8052a Make directories match from root 1a36a21 Install graphviz for doxygen job on travis 3e0b2a5 Doxygen the comments describing the abstract domain interface. 4f8d445 Upgrade from a warning in the comments to a protected constructor. 2b9c880 Clang format the domain files. 028d8b6 Add a method to convert the domain to a predicate to the basic domain API. 918e947 Expand the comments describing the base domain interface. f60027b Move the interface of domains to it's own header file. 15aa61f Adding support for posix_memalign from the stdlib in c. ba01589 Add guidelines for using irepts in the code base 37fc4e6 Update jbmc gitignore ec79bdd Merge pull request diffblue#2385 from polgreen/aggressive_slicer_v2 78b7119 Merge pull request diffblue#2491 from diffblue/std_code_constructors a99c4ff Merge pull request diffblue#2497 from diffblue/simplify_byte_extract_fix 8c7dc17 make comment // not /* ea085d3 move aggressive slicer options into macro aa4848d Apply clang format to includes in goto_instrument_parse_options 4ac9199 Aggressive slicer 2954205 aggressive slicer regression tests de7e1af call graph helper functions 357358d remove mistake in grapht c7457fb Merge pull request diffblue#2543 from tautschnig/vs-unsigned-byte-swap 0e72433 Merge pull request diffblue#2516 from polgreen/cbmc_trace_options 2e90035 Merge pull request diffblue#2590 from peterschrammel/use-proper-irep-ids a354235 Merge pull request diffblue#2592 from NathanJPhillips/cleanup/fix-typo-in-comment 59b1a9e Fix a small typo in a comment that I happened to come across 282468c Print log suffix when running tests c98c9df Merge branch 'develop' into cbmc_trace_options 12e970b Use irep ids for #comments 569c854 Merge pull request diffblue#2489 from diffblue/fix-empty-indexset 993735b Merge pull request diffblue#2507 from mgudemann/bugfix/java/keep-typecasts-on-stack a63212e Add regression test for stack variables with typecasts 6f63050 Simplify stack element replacement loop 731c69e Keep expressions unchanged when adding temporary variables d10e44d Merge pull request diffblue#2586 from hannes-steffenhagen-diffblue/fix-json_unit_test 8d6bfdd Merge pull request diffblue#2575 from nmanthey/upstream-ls_parse 2d14b22 Merge pull request diffblue#2545 from tautschnig/vs-unnecessary ff0414e Merge pull request diffblue#2546 from tautschnig/vs-wmm-int ed48122 Make json parser unit tests independent of working directory 14dc11e Merge pull request diffblue#2495 from diffblue/aws-codebuild-windows-jbmc-tests cefdc21 Merge pull request diffblue#2579 from peterschrammel/clean-up-java-options 64a63a0 Merge pull request diffblue#2584 from diffblue/fp-constant-folding 44cfeb9 Clean up redundant specification of CBMC option 38fe61e Trim JBMC help text width to 80 chars 080fc91 Break overlong lines in help text ebae090 Deactivate smt1 option in JBMC 04fcc5b Check that string options are used with strings turned on 0520732 Use default options in JBMC e4cfb04 Remove built-in-assertions option from JBMC 0d924ce Remove error-label option from JBMC 35f69f0 Remove GOTO_CHECK options from JBMC 86d4fec Remove --refine-strings from tests 7ef8a0e Remove obsolete string-max-length option e5e5e9e remove unneeded NOLINT 9449ac7 Encapsulate constraints for equals d74672b Use const references in string_constraintt fdf14f5 Add invariants on the sign of string_constraintt bounds 16052f8 Move string_constraintt constructor to cpp f01c03c Fix string_constraintt bound values 8edc5ee C front-end: constant folding for floating-point f795ef9 Remove trailing newlines that trip up regex on Windows 53d24e5 the jbmc tests now work on Windows f9c5faf adjust_float_expressions can now take a rounding mode argument 6ccce5b Merge pull request diffblue#2521 from svorenova/array_element_type_util 201ba8c Merge pull request diffblue#2581 from romainbrenguier/refactor/to_code e4b8c44 Clean-up in gen_nondet_instruction_info bb7ea78 Merge pull request diffblue#2528 from tautschnig/dev-null f10badb Add functions to retrieve a reference to the java array element type 7f8b2be Merge pull request diffblue#2582 from jeannielynnmoulton/jeannie/parse-bridge-flag-for-thk123 1f62596 Clean-up get_return_lhs 8966f09 Merge pull request diffblue#2560 from tautschnig/force-inline cb587a9 Adding unit test for checking bridge methods attribute is parsed correctly efadba2 Read the bride flag for methods 26781a6 Remove unnecessary cast to_code a18b32d Merge pull request diffblue#2571 from jeannielynnmoulton/jeannie/InnerClassAccessibility c959c3f Tests get_outer_class with deeply nested classes. 8201c19 Parse and capture outer class for inner classes. 87c2a68 Merge pull request diffblue#2577 from owen-jones-diffblue/owen-jones-diffblue/make-linter-happier a1b9e07 Fix whitespace errors and a typo from diffblue#2505 45eae64 Merge pull request diffblue#2505 from owen-jones-diffblue/owen-jones-diffblue/fix/convert-nondet 6d9e805 Make convert_java_nondet more general 70887e2 Merge pull request diffblue#2564 from tautschnig/vs-java-parse-tree 6c5ecec Merge pull request diffblue#2570 from johnnonweiler/doc-git-submodule-update d5ea306 ls_parse: improve debugging by printing a trace 17bc726 ls_parse: Allow handling unknown blocks aad1692 Add minisat download to jbmc/README.md f7ddb02 Remove --recursive from git submodule update 206f7fb Include submodule update in jbmc/README.md d5f3c32 Fix a typo JMBC->JBMC b5075d7 Document git submodule update in COMPILING.md 9b9aecf Remove unused macro BUFSIZE 0146874 Make all unicode operations use native endianness 8d93087 Move unicode unit test to CATCH and enable it 680227e Explicit unsigned -> uint16_t casts to avoid conversion warnings ea9dc15 goto-gcc: run original compiler even when output is /dev/null 0a990ef Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests 0c15fed Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required 36d13f7 Support Visual Studio's __forceinline 5953f6a goto-instrument/wmm: explicit conversion of bool to 0/1 6dc6ea9 Avoid unncessary signed/unsigned conversion 081f743 use proper constructor for code_assertt 8e44191 use proper constructor for code_expressiont 47f5405 use proper constructor for side_effect_expr_function_callt bf02ec7 use proper constructor for code_declt 9fa0733 use proper constructor for codet dbbd568 mark various 'partial constructors' as deprecated, and introduce complete ones 180e066 add option to show code in CBMC trace 4fbc10d Add option to show function calls and returns in CBMC trace f532b4b allow unsigned long instead of unsigned in regression test for hex_trace 94cacc6 represent numerical values in CBMC trace in hex fc4aab3 avoid non-termination of simplify_exprt::simplify_byte_extract when given array_of git-subtree-dir: cbmc git-subtree-split: 54f3731

martin-cs requested review from chrisr-diffblue, peterschrammel, smowton and thk123 as code owners July 24, 2018 13:09

chrisr-diffblue reviewed Jul 24, 2018

View reviewed changes

chrisr-diffblue approved these changes Jul 24, 2018

View reviewed changes

smowton approved these changes Jul 24, 2018

View reviewed changes

martin-cs force-pushed the feature/context-sensitive-ait-merge-1 branch from 4454d5c to 608e310 Compare July 24, 2018 13:31

allredj reviewed Jul 24, 2018

View reviewed changes

thk123 reviewed Jul 24, 2018

View reviewed changes

martin added 6 commits July 24, 2018 15:27

Move the interface of domains to it's own header file.

f60027b

ai.{h,cpp} is already crowded with two different interfaces. The following patch set will make this much worse, thus we start by refactoring.

Expand the comments describing the base domain interface.

918e947

Add a method to convert the domain to a predicate to the basic domain…

028d8b6

… API. This allows the domain to be converted to an assumption or an assertion amongst other applications.

Clang format the domain files.

2b9c880

Upgrade from a warning in the comments to a protected constructor.

4f8d445

Doxygen the comments describing the abstract domain interface.

3e0b2a5

martin-cs force-pushed the feature/context-sensitive-ait-merge-1 branch from 2be63b4 to 3e0b2a5 Compare July 24, 2018 14:35

allredj reviewed Jul 24, 2018

View reviewed changes

thk123 approved these changes Jul 25, 2018

View reviewed changes

peterschrammel approved these changes Jul 25, 2018

View reviewed changes

peterschrammel assigned martin-cs Jul 25, 2018

martin-cs merged commit 08bd1a8 into diffblue:develop Jul 26, 2018

martin-cs deleted the feature/context-sensitive-ait-merge-1 branch July 26, 2018 11:12


		Module: Abstract Interpretation

		Author: Martin Brain, [email protected]

Feature/context sensitive ait merge 1 #2596

Feature/context sensitive ait merge 1 #2596

Uh oh!

Conversation

martin-cs commented Jul 24, 2018

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jul 24, 2018

Uh oh!

martin-cs commented Jul 24, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 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!

martin-cs commented Jul 24, 2018

Uh oh!

martin-cs commented Jul 24, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jul 24, 2018

Uh oh!

martin-cs commented Jul 25, 2018

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Jul 26, 2018

Uh oh!

Uh oh!