Variable sensitivity domain#5472

Merged

NlightNFotis merged 342 commits intodiffblue:developfrom

martin-cs:refactor/VSD-with-history-2

Nov 11, 2020

This pull request is big! We're only showing the most recent 250 commits

Commits on Nov 10, 2020

Fixed bug when doing a merge write to a pointer

thk123
authored and
martin
committed
Reworked the double dispatch of the merge

thk123
authored and
martin
committed
Removing default copy constructors

thk123
authored and
martin
committed
Replacing map based switch statments with chained if/elses

thk123
authored and
martin
committed
Explained why top must be used as the else clause in eval

thk123
authored and
martin
committed
Don't make copies unnecessarily when merging

thk123
authored and
martin
committed
Using enable_shared_from_this to eliminate naked pointers

thk123
authored and
martin
committed
Adding unit tests for merging of abstract objects

thk123
authored and
martin
committed
Fixed bugs revealed by unit tests

thk123
authored and
martin
committed
Adding unit tests for constant abstract object.

thk123
authored and
martin
committed
Adding tests for constant array

thk123
authored and
martin
committed
Adding unit tests for the struct abstract object

thk123
authored and
martin
committed
Corrected merge methods for pointer and struct

thk123
authored and
martin
committed
Rewriting the constant_abstract_value::merge using behaviour driven design

thk123
authored and
martin
committed
Replaced assert with __CPROVER_assert

thk123
authored and
martin
committed
Use Behaviour Driven Design testing for abstract object merge

thk123
authored and
martin
committed
Struct and array AO unit tests using behaviour driven design

thk123
authored and
martin
committed
Corrected guard on specialised merge

thk123
authored and
martin
committed
Made pointer to array name consistent

thk123
authored and
martin
committed
Constant array reading from top handled correctly

thk123
authored and
martin
committed
Completed test suite for full struct and constant array AOs

thk123
authored and
martin
committed
Correctly set up the enviroment before running tests

thk123
authored and
martin
committed
Extracted out logic for when to use a 2 value merge

thk123
authored and
martin
committed
Improved comment in the LHS simplify

thk123
authored and
martin
committed
Fixed ai_simplify in variable sensitivity domain to use new interface

thk123
authored and
martin
committed
Implemented the sensitivity domain for the union abstract object.

NlightNFotis
authored and
martin
committed
Added implementation for transition into/out of function calls

thk123
authored and
martin
committed
Adding tests for function calls

thk123
authored and
martin
committed
Added sound support for opaque functions

thk123
authored and
martin
committed
Adding reasonable behaviour for opqaue function calls

thk123
authored and
martin
committed
Moved the function call handling into a separate method for readability

thk123
authored and
martin
committed
Support for topping the global values

thk123
authored and
martin
committed
Assertion for varags

thk123
authored and
martin
committed
Made ai_simplify perform a partial simplifcation

thk123
authored and
martin
committed
Corrected lhs simplification

thk123
authored and
martin
committed
Adding tests for simplification of lhs

thk123
authored and
martin
committed
Fixed constant propogation test

thk123
authored and
martin
committed
Corrected code in base class and removed duplicate code

thk123
authored and
martin
committed
Implementing a write_stack to represent writing to a addressable location

thk123
authored and
martin
committed
Use the write_stack in the constant_pointer_abstract_object

thk123
authored and
martin
committed
Modified the write stack to not throw away certain pointers

thk123
authored and
martin
committed
Enable the write stack for pointers to structs

thk123
authored and
martin
committed
Enabling some of these assertions in tests related to arrays

thk123
authored and
martin
committed
Correctly identify bitfield constants as CONSTANT values

chrisr-diffblue
authored and
martin
committed
Driveby cleanup to keep Lint happy

chrisr-diffblue
authored and
martin
committed
Add initial output functions for all sub-classes except pointer.

Daniel Neville
authored and
martin
committed
Add method to update last_written_locations and used it provisionally in ASSIGN.

Daniel Neville
authored and
martin
committed
Experimental helper functions and an attempt to note destroy information for derefs, but do destroy (and correct!) information for other LHS assigns.

Daniel Neville
authored and
martin
committed
Initial merge implementation, some new helper functions (to be moved to cpp and pruned), some notes and disabled removal of TOP elements.

Daniel Neville
authored and
martin
committed
Add erase methods and pointer handling.

Daniel Neville
authored and
martin
committed
Brief auxiliary function tidy-up

Daniel Neville
authored and
martin
committed
Finished prior to clean.

Daniel Neville
authored and
martin
committed
Implemented "last written location" tracking abstract objects

Daniel Neville
authored and
martin
committed
Correction of Thomas's comments.

Daniel Neville
authored and
martin
committed
Extracted the output method for locationst (into environment class, discuss)

Daniel Neville
authored and
martin
committed
To provide a fix for recursive assignments.

Daniel Neville
authored and
martin
committed
Initial set of tests with manual human inspection. Moved static output method to abstract_object and using output in appropriate sub-classes

Daniel Neville
authored and
martin
committed
Correction of formatting (function call over multiple lines).

Daniel Neville
authored and
martin
committed
First version of the function that searches two environments for modified symbols.

NlightNFotis
authored and
martin
committed
[WIP] Added more tests.

NlightNFotis
authored and
martin
committed
Temporary commit for using the modified values

thk123
authored and
martin
committed
Implementing a write_stack to represent writing to a addressable location

thk123
authored and
martin
committed
Another temp checkin of where we've got to

thk123
authored and
martin
committed
Adding get_modified_symbols to other domainTs

thk123
authored and
martin
committed
Restored the correct modified symbols

thk123
authored and
martin
committed
[WIP] Added the restore domain function.

NlightNFotis
authored and
martin
committed
Use the restore_domain function to do context sensitive func return

thk123
authored and
martin
committed
Added a test for the variable sensitivity assign aware merge, for the function pointer_function.

NlightNFotis
authored and
martin
committed
Added more tests for variable sensitivity assign aware merge for function simple_test.

NlightNFotis
authored and
martin
committed
Added more tests for variable sensitivity assign aware merge for function global_test.

NlightNFotis
authored and
martin
committed
Added a basic file for array tests. Need thomas to config its validity before I author the test.desc

NlightNFotis
authored and
martin
committed
Added a struct c test file, and made some changes to the array testing code.

NlightNFotis
authored and
martin
committed
Added some changes that thomas made on my machine to test arrays modified by functions.

NlightNFotis
authored and
martin
committed
Added the test.desc files for tests of arrays and structs.

NlightNFotis
authored and
martin
committed
Fixing comment

thk123
authored and
martin
committed
Correctly escaping braces

thk123
authored and
martin
committed
Delete incorrect comment and fixing whitespace bug

thk123
authored and
martin
committed
Update the last written location for structs

thk123
authored and
martin
committed
Fixed typo introduced in test

thk123
authored and
martin
committed
Add any elements that are only in the second map since this is modified

thk123
authored and
martin
committed
Updated array test to test exactly what we want

thk123
authored and
martin
committed
Fixed the struct test.desc

NlightNFotis
authored and
martin
committed
Three way merge initial checkin

thk123
authored and
martin
committed
Added tests for goto after function.

NlightNFotis
authored and
martin
committed
Added tests for the non-terminating function case.

NlightNFotis
authored and
martin
committed
Reworked three way merge that works when enabled and not

thk123
authored and
martin
committed
Tidied up the changes introduced by context aware merging

thk123
authored and
martin
committed
Tweak to cope with missing utility function.

martin
authored and
martin
committed
Fix up the last written location sensitivity tests.

martin
authored and
martin
committed
Add a common interface for read/write operations on abstract_objectt's

chrisr-diffblue
authored and
martin
committed
Avoid direct manipulation of abstract_objectt::top

chrisr-diffblue
authored and
martin
committed
Factor out last_written_location into it's own abstract_objectt

chrisr-diffblue
authored and
martin
committed
Factor out 'is_modified' logic into to the abstract_object implementations

chrisr-diffblue
authored and
martin
committed
Refactor and rename update_last_written_locations to be more generic

chrisr-diffblue
authored and
martin
committed
Fixup variable-sensitivity unit tests to build after the giant rebase.

chrisr-diffblue
authored and
martin
committed
Convert assertions to invariants.

martin
authored and
martin
committed
Fix a crashing bug with type comparison.

martin
authored and
martin
committed
Allows simplification of expressions containing non-const

hannes-steffenhagen-diffblue
authored and
martin
committed
Test case for the evaluation of (false && x) in the variable sensitivity domain.

martin
authored and
martin
committed
Crashing test cases due to pointer arithmetic issues.

martin
authored and
martin
committed
Use sharing_mapt instead of std::map in full_struct_abstract_object

chrisr-diffblue
authored and
martin
committed
Use sharing_mapt for abstract environment

hannes-steffenhagen-diffblue
authored and
martin
committed
Fix a silly double call of visitor.visit() in full_struct_abstract_objectt

chrisr-diffblue
authored and
martin
committed
Use sharing_mapt in constant_array_abstract_objectt

Chris Ryder
authored and
martin
committed
Remove deprecated call to negate.

martin
authored and
martin
committed
Avoid unnecessarily breaking sharing

hannes-steffenhagen-diffblue
authored and
martin
committed
CLEANUP: Correct indentation

chrisr-diffblue
authored and
martin
committed
CLEANUP: Remove unneeded include of full_struct_abstract_object.h

chrisr-diffblue
authored and
martin
committed
CLEANUP: Correct authorship of dependency_context_abstract_object

chrisr-diffblue
authored and
martin
committed
CLEANUP: Make constant_array_abstract_object match full_struct_abstract_object

chrisr-diffblue
authored and
martin
committed
CLEANUP: Move dump_map utility functions to the correct .cpp file

chrisr-diffblue
authored and
martin
committed
REFACTOR: Rename dependency_context_abstract_object to write_location_context

chrisr-diffblue
authored and
martin
committed
REFACTOR: Refactor variable sensitivity write_location_context

chrisr-diffblue
authored and
martin
committed
Record struct initialisation when field sensitivity is turned on

chrisr-diffblue
authored and
martin
committed
Adjust float expression in variable sensitivity domain

hannes-steffenhagen-diffblue
authored and
martin
committed
Try all rounding modes when rounding mode is unknown

hannes-steffenhagen-diffblue
authored and
martin
committed
Add floating point simplifcation test

hannes-steffenhagen-diffblue
authored and
martin
committed
Add data-dependency-context to variable sensitivity as commandline option

chrisr-diffblue
authored and
martin
committed
Add variable sensitivity data dependency graph

chrisr-diffblue
authored and
martin
committed
[DO NOT MERGE] Track which expressions give rise to data dependencies

chrisr-diffblue
authored and
martin
committed
Avoid breaking sharing in usage of sharing_mapt in full_struct_abstract_object

chrisr-diffblue
authored and
martin
committed
Avoid breaking sharing in usage of sharing_mapt in constant_array_abstract_object

chrisr-diffblue
authored and
martin
committed
Add data dependency context and variable sensitivity dependence graph to Makefile

danpoe
authored and
martin
committed
Remove stray ; in context abstract object

danpoe
authored and
martin
committed
Interval values
martin
committed
Add regression tests for interval abstract values

hannes-steffenhagen-diffblue
authored and
martin
committed
Various code style fixes in intervals code
martin
committed
Move interval value constructors to .cpp

hannes-steffenhagen-diffblue
authored and
martin
committed
Fix interval abstract value constructor

NlightNFotis
authored and
martin
committed
Fix infinite loop in interval values

NlightNFotis
authored and
martin
committed
Moved rounding mode aware arithmetic to constant abstract value

danpoe
authored and
martin
committed
Calling eval_expression on top abstract object

danpoe
authored and
martin
committed
Escape curly braces in variable sensitivity float regression test

danpoe
authored and
martin
committed
Add struct case to abstract environment eval

danpoe
authored and
martin
committed
Basic interval arithmetic

danpoe
authored and
martin
committed
Interval arithmetic regression tests

danpoe
authored and
martin
committed
use eval to evaluate binary operators in interval abstract object

danpoe
authored and
martin
committed
Handle typecasts in constant_interval_exprt
martin
committed
Typecast from ID_bool to integer types

danpoe
authored and
martin
committed
Addressing review comments

danpoe
authored and
martin
committed
Mark failing dependence graph test as FUTURE

danpoe
authored and
martin
committed
Make constant_array_abstract_object::eval_index virtual

hannes-steffenhagen-diffblue
authored and
martin
committed
Move interval value constructors to .cpp

hannes-steffenhagen-diffblue
authored and
martin
committed
Interval operations
martin
committed
Add interval arrays to variable sensitivity

hannes-steffenhagen-diffblue
authored and
martin
committed
Clang format

hannes-steffenhagen-diffblue
authored and
martin
committed
Return top in case of min/max indices in interval arrays

hannes-steffenhagen-diffblue
authored and
martin
committed
Exit loops in interval arrays early if result becomes top

hannes-steffenhagen-diffblue
authored and
martin
committed
Use from_integer instead of constant_exprt constructor

hannes-steffenhagen-diffblue
authored and
martin
committed
Adapt dependence graph regression test to new output format

danpoe
authored and
martin
committed
Fixups to enable building after rebase

chrisr-diffblue
authored and
martin
committed
Add function to get statistics about variable sensitivity domain

hannes-steffenhagen-diffblue
authored and
martin
committed
Add counts of various object types to environment statistics

hannes-steffenhagen-diffblue
authored and
martin
committed
Add an estimation of memory usage to object statistics

hannes-steffenhagen-diffblue
authored and
martin
committed
Remove INVARIANT in full_struct_abstract_object copy constructor

chrisr-diffblue
authored and
martin
committed
Make variable-sensitivity dependence graph produce control dependencies

chrisr-diffblue
authored and
martin
committed
Add support for bit field and enums intervals.cpp

chrisr-diffblue
authored and
martin
committed
Avoid creating interval_abstract_valuet's for float types

chrisr-diffblue
authored and
martin
committed
Add a basic implementation of to_constant for interval_abstract_valuet

chrisr-diffblue
authored and
martin
committed
Crude ability to expression_transform mixed interval and non-intervals

chrisr-diffblue
authored and
martin
committed
Added regression test for variable sensitivity intervals with mixed float/bool expressions

chrisr-diffblue
authored and
martin
committed
Include function call arguments in variable sensitivity dependency graph

chrisr-diffblue
authored and
martin
committed
Move ai configuration to separate config object
martin
committed
Add option to print statistics about the VS domain
martin
committed
Disable currently broken dependence graph tests

hannes-steffenhagen-diffblue
authored and
martin
committed
Disable interval float test

hannes-steffenhagen-diffblue
authored and
martin
committed
Fix variable sensitivity unit test

hannes-steffenhagen-diffblue
authored and
martin
committed
Apply bandaid fix to variable sensitivity
martin
committed
Add control dependencies from function call to function entry point for new dependency graph

danpoe
authored and
martin
committed
Fix write_stack to correctly complete types for index_exprt expressions

chrisr-diffblue
authored and
martin
committed
Avoid breaking fixpoint when merging data_dependency_context

chrisr-diffblue
authored and
martin
committed
Add specialised ai domain methods for variable sensitivity dependence graph

danpoe
authored and
martin
committed
Control dependencies of function body instructions to function calls for variable sensitivity dependence graph

danpoe
authored and
martin
committed
Include GOTO guard expressions in variable sensitivity data dependencies

chrisr-diffblue
authored and
martin
committed
Fix variable sensitivity dependence graph regression test

danpoe
authored and
martin
committed
Ensure constant_array_abstract_object is in a valid state after calling make_top

chrisr-diffblue
authored and
martin
committed
Fix variable sensitvity to build with XCode 9

chrisr-diffblue
authored and
martin
committed
Unconditional control dependency fix

chrisr-diffblue
authored and
martin
committed
Track only immediate dependencies in variable sensitivity dependence graph.

chrisr-diffblue
authored and
martin
committed
Fix dependence graph precondition failure in VSB dependence graph

chrisr-diffblue
authored and
martin
committed
Initialise is_bottom in abstract_environmentt

hannes-steffenhagen-diffblue
authored and
martin
committed
Fixup incorrect itterator comparison in data_dependency_context

chrisr-diffblue
authored and
martin
committed
Add a module_dependencies.txt to variable sensitivity domain

chrisr-diffblue
authored and
martin
committed
Tools to build intersection of intervals satisfying bool expressions

Petr Bauch
authored and
martin
committed
Added regression test for PR #295

Petr Bauch
authored and
martin
committed
Extend interval multiplication for extremes
martin
committed
Record data dependencies for functions with missing bodies

chrisr-diffblue
authored and
martin
committed
Avoid setting domain to TOP when calling functions with const pointer arguments

chrisr-diffblue
authored and
martin
committed
Merge when reading from array with unknown index.

Chris Ryder
authored and
martin
committed
Fixups post-rebase

hannes-steffenhagen-diffblue
authored and
martin
committed
Fix interval construction

petr-bauch
authored and
martin
committed
Support interval expressions containing ?: operations

chrisr-diffblue
authored and
martin
committed
Extend the interface with hashing and equality for unordered-sets.

owen-mc-diffblue
authored and
martin
committed
Implement value sets

owen-mc-diffblue
authored and
martin
committed
If there is no context to wrap - don't wrap the objects

thk123
authored and
martin
committed
Only enable location context if value set is turned off

thk123
authored and
martin
committed
Produce an error if value set is used with a context tracking argument

thk123
authored and
martin
committed
Remove unusued boolean flag

thk123
authored and
martin
committed
Remove the way to set configuration options using only optionst

thk123
authored and
martin
committed
Introduce some sensible config defaults

thk123
authored and
martin
committed
Use the config to simplify the code

thk123
authored and
martin
committed
Make value set entries human-readable

owen-mc-diffblue
authored and
martin
committed
Delete write_stack unit test

owen-mc-diffblue
authored and
martin
committed
Various miscellaneous fixes

owen-mc-diffblue
authored and
martin
committed
Add tests for value-set domain

thk123
authored and
martin
committed
Fix test and add reference to github issue.

NlightNFotis
authored and
martin
committed
Make variable_sensitivity_domaint::eval public from protected

NlightNFotis
authored and
martin
committed
Add stub implementations for value set classes

hannes-steffenhagen-diffblue
authored and
martin
committed
clang-format everything
martin
committed
Update test description for the move to __CPROVER_assert
martin
committed
Rather than change existing tests, create new test descriptions
martin
committed
Three way merge is not being added to ai_domaint so no override
martin
committed
Use brace initialisation instead of parentheses

hannes-steffenhagen-diffblue
authored and
martin
committed
Implement merge for value_set_abstract_valuet

hannes-steffenhagen-diffblue
authored and
martin
committed
Implement output for value-set abstract values

hannes-steffenhagen-diffblue
authored and
martin
committed
Implement value_set_abstract_valuet::to_constant

hannes-steffenhagen-diffblue
authored and
martin
committed
Update the use of exprts so that it is more type safe
martin
committed
Disable stats collection until the necessary changes are merged to ait
martin
committed
Replace call to a utility function that is not in the patch set
martin
committed
Remove an unreachable fall back case
martin
committed
Another update for the change in how three_way_merge is integrated
martin
committed
Port over some of the changes to dependence_graph to the VS version
martin
committed
fixup the unreachable thing
martin
committed
Tweak the update to VSDG
martin
committed
Refactor the VS dependency graph analysis to use the domain factory
martin
committed
Fix all of the linting errors
martin
committed
Fix a very subtle bug in the initialisation of VSD domain objects
martin
committed
Integrate VSD so that it can be called from goto-analyzer
martin
committed
Update the regression tests for the new arguments
martin
committed
Re-enable dependency graph tests that were disabled at some point
martin
committed
Tidy up, fix and update the constant propagation tests (VSD and not)
martin
committed
Make tests independent of the exact line numbers for assertions
martin
committed
Create a new abstract interpreter that does a three-way merge
martin
committed
Enable three-way merge for the tests that need it
martin
committed
Update line numbers for domains that track changes
martin
committed
Use three-way merge in the VSD dependency graph
martin
committed
Update the VSD dependency graph tests for line number changes
martin
committed
Update unit tests for the improved, type safe(r) exprts
martin
committed
Tweak the VSDG to fix a clang specific warning about get_state
martin
committed
One of the new unit tests was omitted from the source list
martin
committed
Update unit test for the bug fix to abstract_environmentt
martin
committed
Correct a typo in the creation of an interval
martin
committed
Remove reference to non-public issue tracker
martin
committed
Convert comments to the new(er) doxygen format
martin
committed
Reformat so that comments pass linting
martin
committed
Apply Peter Schrammel's review comments
martin
committed
Move doxygen comments from .cpp to .h files
martin
committed
Fix issues and warnings raised by doxygen
martin
committed
Update regression tests to cope with changes to initialisation
martin
committed
s/const auto/const auto &/ in loops
martin
committed

Variable sensitivity domain#5472NlightNFotis merged 342 commits intodiffblue:developdiffblue/cbmc:developfrom martin-cs:refactor/VSD-with-history-2martin-cs/cbmc:refactor/VSD-with-history-2Copy head branch name to clipboard

Commits

Commits on Nov 10, 2020

Variable sensitivity domain#5472
NlightNFotis merged 342 commits intodiffblue:developfrom
martin-cs:refactor/VSD-with-history-2