Code

Partial expression simplification#1020

Code

Closed

thk123 wants to merge 130 commits intodiffblue:developdiffblue/cbmc:developfrom

thk123:bugfix/partial-expression-simplificationthk123/cbmc:bugfix/partial-expression-simplificationCopy head branch name to clipboard

Commits

Commits on Jun 15, 2017

• Fix constant propagator.

  

  martin

  committed
  08a2f8a

  Copy full SHA for 08a2f8a

• disable two-way propagation for now

  

  danpoe

  authored and

  martin

  committed
  956225f

  Copy full SHA for 956225f

• Addressing constant domain review comments by Daniel Poetzl.

  

  martin

  committed
  1b13114

  Copy full SHA for 1b13114

• constant propagator fix

  

  danpoe

  authored and

  martin

  committed
  e2fdcbf

  Copy full SHA for e2fdcbf

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

  

  martin

  committed
  3178f1b

  Copy full SHA for 3178f1b

• Use is_bottom() to catch unreachable functions.

  

  martin

  committed
  5606ce5

  Copy full SHA for 5606ce5

• Refactor goto-analyzer so that task, analysis, domain and output can be picked independently.

  

  martin

  committed
  7cee75e

  Copy full SHA for 7cee75e

• Remove the special case handling of --show-intervals.

  Show description for 5f6ecbe
  

  Martin Brain

  authored and

  martin

  committed
  5f6ecbe

  Copy full SHA for 5f6ecbe

• Add support for dependency graph display.

  

  martin

  committed
  93b8f8c

  Copy full SHA for 93b8f8c

• Program simplification now removes unused instructions.

  

  martin

  committed
  d0b728a

  Copy full SHA for d0b728a

• Catch exceptions thrown in doit() in goto analyzer.

  

  martin

  committed
  427580d

  Copy full SHA for 427580d

• Fix merging issues in goto analyzer.

  

  martin

  committed
  ce669c3

  Copy full SHA for ce669c3

• Fix whitespace to match coding guidelines

  

  danpoe

  authored and

  martin

  committed
  8db8121

  Copy full SHA for 8db8121

• Whitespace fixes in goto-analyzer.

  

  martin

  committed
  7193056

  Copy full SHA for 7193056

• regression test changes

  

  danpoe

  authored and

  martin

  committed
  cb54f29

  Copy full SHA for cb54f29

• Addressing goto analyzer review comments by Daniel Poetzl.

  

  martin

  committed
  42e603c

  Copy full SHA for 42e603c

• option to ignore unresolved functions in the constant propagator

  

  danpoe

  authored and

  martin

  committed
  74170fd

  Copy full SHA for 74170fd

• Test that requires is_bottom() and is_top().

  

  martin

  committed
  ec808bd

  Copy full SHA for ec808bd

• Improve status output.

  

  martin

  committed
  f1c62f2

  Copy full SHA for f1c62f2

• enable failed tests printer for goto-analyzer regression tests

  

  danpoe

  authored and

  martin

  committed
  7ca4e94

  Copy full SHA for 7ca4e94

• enable assertions in is_threadedt

  

  danpoe

  authored and

  martin

  committed
  ca7d8ab

  Copy full SHA for ca7d8ab

• Update the use of ai_simplify for the introduction of ai_simplify_lhs.

  

  martin

  committed
  3565cc6

  Copy full SHA for 3565cc6

• Check in of basic variable sensitivity framework.

  Show description for 5abec1e
  

  thk123

  authored and

  thk123

  committed
  5abec1e

  Copy full SHA for 5abec1e

• Added constant_abstract_value implementation

  Show description for 29b5a82
  

  thk123

  authored and

  thk123

  committed
  29b5a82

  Copy full SHA for 29b5a82

• Use variable in the constant_propogation checks

  

  thk123

  authored and

  thk123

  committed
  1eae6e0

  Copy full SHA for 1eae6e0

• Adding debug guarded output to the variable sensitivity domain

  

  thk123

  authored and

  thk123

  committed
  341b619

  Copy full SHA for 341b619

• Better stub for assigning to non-trivial symbol

  

  thk123

  authored and

  thk123

  committed
  b10f621

  Copy full SHA for b10f621

• Created skeleton classes for the array, pointer, struct

  Show description for e922362
  

  thk123

  authored and

  thk123

  committed
  e922362

  Copy full SHA for e922362

• Adding a 2 element implemention of sturct abstract object

  

  thk123

  authored and

  thk123

  committed
  b5fda65

  Copy full SHA for b5fda65

• Modifications to struct_abstract_object

  Show description for b6ab6e6
  

  thk123

  authored and

  thk123

  committed
  b6ab6e6

  Copy full SHA for b6ab6e6

• Readded broken protected

  Show description for d4cb43d
  

  thk123

  authored and

  thk123

  committed
  d4cb43d

  Copy full SHA for d4cb43d

• Implementation of simplify

  Show description for a3654e3
  

  thk123

  authored and

  thk123

  committed
  a3654e3

  Copy full SHA for a3654e3

• Don't use static for the map as means wrong this is captured

  

  thk123

  authored and

  thk123

  committed
  2d8cb48

  Copy full SHA for 2d8cb48

• Added handler for logical == expression

  

  thk123

  authored and

  thk123

  committed
  e562e9d

  Copy full SHA for e562e9d

• Cleaned up the variable sensitivity framework

  Show description for 5257140
  

  thk123

  authored and

  thk123

  committed
  5257140

  Copy full SHA for 5257140

• Corrected the logic for non-trivial assigns

  

  thk123

  authored and

  thk123

  committed
  292673b

  Copy full SHA for 292673b

• Fixied potential dangling pointer in the struct abstract oject

  

  thk123

  authored and

  thk123

  committed
  c41d65f

  Copy full SHA for c41d65f

• Basic implementations for abstract pointer and abstract array

  

  thk123

  authored and

  thk123

  committed
  e26e7c3

  Copy full SHA for e26e7c3

• Moved the logic for resolving logical expressions into abstract_value

  Show description for 57c1e1b
  

  thk123

  authored and

  thk123

  committed
  57c1e1b

  Copy full SHA for 57c1e1b

• Fixed bug that would have occured for struct/pointer/array assigns

  

  thk123

  authored and

  thk123

  committed
  df28677

  Copy full SHA for df28677

• Removed the requirement on two operands

  Show description for 44b69ed
  

  thk123

  authored and

  thk123

  committed
  44b69ed

  Copy full SHA for 44b69ed

• Simplify the expression before storing

  Show description for f2323f2
  

  thk123

  authored and

  thk123

  committed
  f2323f2

  Copy full SHA for f2323f2

• Fixed issue where writing to a top value

  Show description for af2c1d3
  

  thk123

  authored and

  thk123

  committed
  af2c1d3

  Copy full SHA for af2c1d3

• Add previously written design documentation to the relevant parts of the code.

  

  martin

  authored and

  thk123

  committed
  0b8bff4

  Copy full SHA for 0b8bff4

• Improve the documentation of various methods.

  

  martin

  authored and

  thk123

  committed
  4717f58

  Copy full SHA for 4717f58

• Give a generic implementation of assume.

  

  martin

  authored and

  thk123

  committed
  6175996

  Copy full SHA for 6175996

• Enable the use of assume for branches.

  

  martin

  authored and

  thk123

  committed
  4a294f3

  Copy full SHA for 4a294f3

• Basic implementation of the sensitive pointer

  Show description for 12f8d7e
  

  thk123

  authored and

  thk123

  committed
  12f8d7e

  Copy full SHA for 12f8d7e

• Fixing comments in pointer_abstract_object

  

  thk123

  authored and

  thk123

  committed
  8471785

  Copy full SHA for 8471785

• Adding merge state

  

  thk123

  authored and

  thk123

  committed
  de8af33

  Copy full SHA for de8af33

• Supporting stack when writing

  Show description for 28b0139
  

  thk123

  authored and

  thk123

  committed
  28b0139

  Copy full SHA for 28b0139

• Changed the pointer abstract object to store an expression

  Show description for 92698fc
  

  thk123

  authored and

  thk123

  committed
  92698fc

  Copy full SHA for 92698fc

• Implementing a configurable abstract object factory

  Show description for 5492310
  

  Owen Jones

  authored and

  thk123

  committed
  5492310

  Copy full SHA for 5492310

• Fixed crash bug in writing to dereference of pointer to pointer

  Show description for 70ae194
  

  thk123

  authored and

  thk123

  committed
  70ae194

  Copy full SHA for 70ae194

• Improved exception message for unreasonable write

  

  thk123

  authored and

  thk123

  committed
  6c89bf2

  Copy full SHA for 6c89bf2

• Checking in a demo script containg the things that currently work

  Show description for 079eed9
  

  thk123

  authored and

  thk123

  committed
  079eed9

  Copy full SHA for 079eed9

• Added writing to pointer to demo

  

  thk123

  authored and

  thk123

  committed
  c0c7c0d

  Copy full SHA for c0c7c0d

• Added flags so the factory reads the flags correctly

  

  thk123

  authored and

  thk123

  committed
  1843fec

  Copy full SHA for 1843fec

• Enable pointer sensitivity in the factory

  Show description for 847a2af
  

  thk123

  authored and

  thk123

  committed
  847a2af

  Copy full SHA for 847a2af

• Added documentation to the demo script

  

  thk123

  authored and

  thk123

  committed
  23e19cc

  Copy full SHA for 23e19cc

• Fixing up formatting

  Show description for 80f7153
  

  Owen Jones

  authored and

  thk123

  committed
  80f7153

  Copy full SHA for 80f7153

• Add simplification of the left hand side of assignments.

  

  martin

  authored and

  thk123

  committed
  175e807

  Copy full SHA for 175e807

• Remove incorrect comment.

  

  martin

  authored and

  thk123

  committed
  dc82227

  Copy full SHA for dc82227

• Review comments and TODOs.

  

  martin

  authored and

  thk123

  committed
  1209922

  Copy full SHA for 1209922

• Mark unreachable assertions as satisfied.

  

  martin

  authored and

  thk123

  committed
  4cbf595

  Copy full SHA for 4cbf595

• Document various of the key ideas behind how goto-analyze works.

  

  martin

  authored and

  thk123

  committed
  d7893d6

  Copy full SHA for d7893d6

• Renamed methods to provide a more consistent interface

  Show description for b6e03bd
  

  martin

  authored and

  thk123

  committed
  b6e03bd

  Copy full SHA for b6e03bd

• Protect top and bottom as much as possible.

  Show description for e6064b6
  

  martin

  authored and

  thk123

  committed
  e6064b6

  Copy full SHA for e6064b6

• Output should be const-clean.

  

  martin

  authored and

  thk123

  committed
  d17f3a7

  Copy full SHA for d17f3a7

• Implementing sensitive struct abstract object

  Show description for 90fcdc9
  

  danpoe

  authored and

  thk123

  committed
  90fcdc9

  Copy full SHA for 90fcdc9

• If anything is assigned the value bottom, the whole domain should be set to bottom.

  

  martin

  authored and

  thk123

  committed
  cd53637

  Copy full SHA for cd53637

• A missing case in the factory code means that constant assertions were not being

  Show description for 96eef7d
  

  martin

  authored and

  thk123

  committed
  96eef7d

  Copy full SHA for 96eef7d

• Fix overwrite for CLONE and MERGE

  Show description for 0d147a3
  

  Owen Jones

  authored and

  thk123

  committed
  0d147a3

  Copy full SHA for 0d147a3

• In abstract objects the state should be private and merge_state protected.

  Show description for 20b2936
  

  martin

  authored and

  thk123

  committed
  20b2936

  Copy full SHA for 20b2936

• Enforced const interface for abstract objects

  Show description for 6ff3ee7
  

  martin

  authored and

  thk123

  committed
  6ff3ee7

  Copy full SHA for 6ff3ee7

• Fix crash

  Show description for e25d082
  

  Owen Jones

  authored and

  thk123

  committed
  e25d082

  Copy full SHA for e25d082

• Minimal reproducer for struct problem

  

  Owen Jones

  authored and

  thk123

  committed
  4a38df0

  Copy full SHA for 4a38df0

• Use the correct abstract object when performing a transform

  

  thk123

  committed
  7db370c

  Copy full SHA for 7db370c

• Corrected merge action in the abstract enviroment

  

  thk123

  committed
  4e5a3ad

  Copy full SHA for 4e5a3ad

• Correct struct write for unknown component

  

  thk123

  committed
  01dbc41

  Copy full SHA for 01dbc41

• Correcting type check in struct abstract object

  Show description for b83a34b
  

  thk123

  committed
  b83a34b

  Copy full SHA for b83a34b

• Fix for crash

  Show description for 41cb817
  

  Owen Jones

  authored and

  thk123

  committed
  41cb817

  Copy full SHA for 41cb817

• Basic implementation of the constant_array_abstract_object

  Show description for ca9d708
  

  thk123

  committed
  ca9d708

  Copy full SHA for ca9d708

• Array initialization now works with the abstract object

  Show description for 9b47072
  

  thk123

  committed
  9b47072

  Copy full SHA for 9b47072

• Added merge_state to constant_array_abstract_object

  Show description for b23b7de
  

  thk123

  committed
  b23b7de

  Copy full SHA for b23b7de

• Adding function header comments

  

  thk123

  committed
  006b812

  Copy full SHA for 006b812

• Removed unnecessary copies

  

  thk123

  committed
  1b5c81e

  Copy full SHA for 1b5c81e

• Updating the demo script

  

  thk123

  committed
  af4a943

  Copy full SHA for af4a943

• Adding output function to struct

  Show description for 3cbc98b
  

  thk123

  committed
  3cbc98b

  Copy full SHA for 3cbc98b

• Made verify stricter

  Show description for e453bef
  

  thk123

  committed
  e453bef

  Copy full SHA for e453bef

• Fixed bug where top wasn't being cleared

  Show description for 0187b77
  

  thk123

  committed
  0187b77

  Copy full SHA for 0187b77

• Bug fixes for the array abstract object

  Show description for d466c89
  

  thk123

  committed
  d466c89

  Copy full SHA for d466c89

• Corrected and simplified constructor for the pointer abstract object

  Show description for 987ec23
  

  thk123

  committed
  987ec23

  Copy full SHA for 987ec23

• Corrected implementation of flow sensitivity

  Show description for f1436e5
  

  thk123

  committed
  f1436e5

  Copy full SHA for f1436e5

• Tidy up includes

  Show description for edacc16
  

  thk123

  committed
  edacc16

  Copy full SHA for edacc16

• Correcting implemenations of the write methods for pointer and struct

  Show description for 06f5a58
  

  thk123

  committed
  06f5a58

  Copy full SHA for 06f5a58

• Refactor the ai_simplify into a lhs function

  

  thk123

  committed
  21cc2dc

  Copy full SHA for 21cc2dc

• Corrected constructing object for failed evaluation

  Show description for b1e2cc6
  

  thk123

  committed
  b1e2cc6

  Copy full SHA for b1e2cc6

• Fixing constant propogation test

  Show description for 6a305a5
  

  thk123

  committed
  6a305a5

  Copy full SHA for 6a305a5

• Linting fixes

  

  thk123

  committed
  aafe2fa

  Copy full SHA for aafe2fa

• Modified lambda to compile under Windows compiler.

  

  thk123

  committed
  a8f1ae7

  Copy full SHA for a8f1ae7

• Improved the removing top elements in map merge

  Show description for c49b533
  

  thk123

  committed
  c49b533

  Copy full SHA for c49b533

• Modified code to not crash when writing to an pointer arithmetic on lhs

  Show description for 6297a05
  

  thk123

  committed
  6297a05

  Copy full SHA for 6297a05

• Adding tests for reading and writing to/from ararys through points

  Show description for 12f78b4
  

  thk123

  committed
  12f78b4

  Copy full SHA for 12f78b4

• Fixed bug when doing a merge write to a pointer

  Show description for fdc1f82
  

  thk123

  committed
  fdc1f82

  Copy full SHA for fdc1f82

• Reworked the double dispatch of the merge

  Show description for e334806
  

  thk123

  committed
  e334806

  Copy full SHA for e334806

• Removing default copy constructors

  Show description for be2a296
  

  thk123

  committed
  be2a296

  Copy full SHA for be2a296

• Replacing map based switch statments with chained if/elses

  Show description for d726007
  

  thk123

  committed
  d726007

  Copy full SHA for d726007

• Explained why top must be used as the else clause in eval

  Show description for 2d055ea
  

  thk123

  committed
  2d055ea

  Copy full SHA for 2d055ea

• Don't make copies unnecessarily when merging

  Show description for 7cf1446
  

  thk123

  committed
  7cf1446

  Copy full SHA for 7cf1446

• Using enable_shared_from_this to eliminate naked pointers

  Show description for 2772300
  

  thk123

  committed
  2772300

  Copy full SHA for 2772300

• Adding unit tests for merging of abstract objects

  

  thk123

  committed
  c84f11b

  Copy full SHA for c84f11b

• Fixed bugs revealed by unit tests

  Show description for d8341af
  

  thk123

  committed
  d8341af

  Copy full SHA for d8341af

• Adding unit tests for constant abstract object.

  

  thk123

  committed
  f90bf00

  Copy full SHA for f90bf00

• Adding tests for constant array

  Show description for b8a0c78
  

  thk123

  committed
  b8a0c78

  Copy full SHA for b8a0c78

• Adding unit tests for the struct abstract object

  

  thk123

  committed
  3b05fe3

  Copy full SHA for 3b05fe3

• Corrected merge methods for pointer and struct

  

  thk123

  committed
  b2ef738

  Copy full SHA for b2ef738

• Rewriting the constant_abstract_value::merge using behaviour driven design

  

  thk123

  committed
  c96f418

  Copy full SHA for c96f418

• Replaced assert with __CPROVER_assert

  Show description for ca525bd
  

  thk123

  committed
  ca525bd

  Copy full SHA for ca525bd

• Use Behaviour Driven Design testing for abstract object merge

  

  thk123

  committed
  0f51650

  Copy full SHA for 0f51650

• Struct and array AO unit tests using behaviour driven design

  Show description for 6191fb2
  

  thk123

  committed
  6191fb2

  Copy full SHA for 6191fb2

• Corrected guard on specialised merge

  

  thk123

  committed
  430f934

  Copy full SHA for 430f934

• Made pointer to array name consistent

  

  thk123

  committed
  66561d7

  Copy full SHA for 66561d7

• Constant array reading from top handled correctly

  

  thk123

  committed
  deba2a3

  Copy full SHA for deba2a3

• Completed test suite for full struct and constant array AOs

  

  thk123

  committed
  b1ac428

  Copy full SHA for b1ac428

• Correctly set up the enviroment before running tests

  Show description for d4afa61
  

  thk123

  committed
  d4afa61

  Copy full SHA for d4afa61

• Extracted out logic for when to use a 2 value merge

  Show description for f7f3db0
  

  thk123

  committed
  f7f3db0

  Copy full SHA for f7f3db0

• Improved comment in the LHS simplify

  

  thk123

  committed
  bb4f378

  Copy full SHA for bb4f378

• Fixed ai_simplify in variable sensitivity domain to use new interface

  Show description for 8601e81
  

  thk123

  committed
  8601e81

  Copy full SHA for 8601e81

• Made ai_simplify perform a partial simplifcation

  Show description for de2f979
  

  thk123

  committed
  de2f979

  Copy full SHA for de2f979